This commit models the fact that compilers are not allowed to reorder
volatile accesses. This modeling is at best approximate, although it
does correctly handle C-RomanPenyaev-list-rcu-rr.litmus from the litmus
github archive. The approach is to extend control dependencies to
subsequent volatiles accesses.
Probable issues with this change:
1. It does not correctly handle the case of identical WRITE_ONCE()
invocations at the beginning of both legs of an "if" statement.
(Of course, the current state does not correctly handle this
either.)
2. It might not correctly handle the ARMv8 conditional-move instruction.
3. It is probably missing some handling of atomic RWM operations.
4. It does not insist that the initial ctrl dependency end in
a volatile access. This is not yet a problem because we
don't yet model unmarked accesses.
That said, this patch is not intended for inclusion, but rather in the
hope that it inspires someone to come up with something better.
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 882fc33274ac..f745337ba10e 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -57,7 +57,9 @@ empty rmw & (fre ; coe) as atomic
(* Preserved Program Order *)
let dep = addr | data
-let rwdep = (dep | ctrl) ; [W]
+let volatile = [Once] | [Release] | [Acquire] (* No unmarked accesses. *)
+let ctrl-volatile = ctrl ; (po ; volatile)*
+let rwdep = (dep | ctrl-volatile) ; [W]
let overwrite = co | fr
let to-w = rwdep | (overwrite & int)
let to-r = addr | (dep ; rfi)
