You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
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.
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.
The following litmus test has a trivial deadlock
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.The text was updated successfully, but these errors were encountered: