Detect unmatched lock/unlock

[hernanponcedeleon]

The following litmus test has a trivial deadlock

C lock

{
}


P0(int *a, int *b, spinlock_t *l)
{
	spin_lock(l);
	WRITE_ONCE(*a, 1);
}

P1(int *a, int *b, spinlock_t *l)
{
	spin_lock(l);
	WRITE_ONCE(*b, 1);
}

exists (a=1 /\ b=1)

Right now we cannot detect this (not even with the liveness property). There is a proposal to flag such situations. LKMM has several such sanity checks (normally in the *.bell file) which we normally implemented internally. It would make sense to add a check for this situation.

[ThomasHaas]

This is roughly the same issue as #275 .
I don't think you can do much about this. This program has not a single execution because in litmus tests we "assume" that spin locks succeed.

[hernanponcedeleon]

I was thinking we could flag executions where the write of a lock was last in co-order. However, you are right, that won't work because due to the assumption locks succeed, the formula is trivially unsat (i.e. no execution at all).

We could try to detect the problem statically, but then there might be situations with involved control-flow that might make the analysis more involved for not measurable benefit.

[ThomasHaas]

The question is if such a detection is really worthwhile for litmus tests.
Or have you seen real code that relies on spin locks as a primitive?

[hernanponcedeleon]

rt_mutex makes uses of spinlock (see e.g. here) and I use the primitive to speed up verification. However, I don't expected to encounter trivial deadlock as the one in the test in real kernel code.