RCU-Deadlocks

[xeren]

Rcu-Sync should be treated as an await-loop, in order to model executions in programs that use it incorrectly, like C-RW-GR+RW-R+RW-R. The current encoding scheme applied to the linux-kernel memory model prohibits control paths where a deadlocking Rcu-Sync is executed. Dartagnan currently cannot find such lifeness violations.

[ThomasHaas]

I don't think this is possible that easily. The semantics of the RCU primitives are currently only defined via the .cat file in the form of consistency constraints; the primitives have no program semantics. I think not even flagging will help here, cause all executions that have incorrect usage of RCU-Sync will also be inconsistent.

This will be a general problem for all library calls that are solely defined by a .cat specification. For example, if we ever get around to express SMR in .cat, we might run into similar issues.

[hernanponcedeleon]

@xeren why do you say we should treat it as a spinloop? Which problem did you encounter?

I actually run this test with herd7 and it reports that the program has no execution

herd7 -model cat/linux-kernel.cat -I cat/ -bell cat/linux-kernel.bell -macros cat/linux-kernel.def litmus/LKMM/auto/C-RW-GR+RW-R+RW-R.litmus 
Test auto/C-RW-GR+RW-R+RW-R Allowed
States 0
No
Witnesses
Positive: 0 Negative: 0
Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1)
Observation auto/C-RW-GR+RW-R+RW-R Never 0 0
Time auto/C-RW-GR+RW-R+RW-R 0.02
Hash=fdd3d7ccf2f518dd30733131e81ff12d

[ThomasHaas]

This is exactly the problem he refers to. The real implementation would have a deadlock in this situation, but in the case of litmus tests, all such executions are considered inconsistent rather than dead. This is because the semantics are solely defined by the cat file in the form of consistency constraints.

[hernanponcedeleon]

Yes, this is the way to deal with such situations in litmus test (at least to be consistent with herd). The question is, is there an "issue" to be solved? Otherwise I think we can close this one.

[ThomasHaas]

I don't think there is an issue for litmus tests. At best it is a reminder that for actual Linux-code, treating RCU primitives via .cat without inlining their implementation may cause Dartagnan to not find any problems although the real code would certainly get stuck.

[hernanponcedeleon]

Is the following pattern the only deadlocking scenario?

rcu_read_lock();
...
synchronize_rcu();
...
rcu_read_unlock();

If so, I think it is fair to assume kernel developer will not write such kind of code.