add rmw axiom

cat/opencl-overhauling-scopedsc.cat

@@ -1,10 +1,11 @@
 OpenCL
 (* OpenCL Memory Model *)
+include "basic.cat"
 
 (*
 * This model is based on:
 * https://multicore.doc.ic.ac.uk/overhauling/opencl_base.cat
-* https://multicore.doc.ic.ac.uk/overhauling/opencl.cat
+* https://multicore.doc.ic.ac.uk/overhauling/opencl_scopedsc.cat
 *)
 
 // Base relations:
@@ -97,6 +98,9 @@ empty (rf; [NAL & LOCAL])\vis(lhb) as O-NaRfL
 (* Consistency of RMWs *)
 irreflexive rf | (mo;mo;rf^-1) | (mo;rf) as O-Rmw
 
+// Atomicity
+empty rmw & (fre; coe) as atomic
+
 (****************************************)
 (* Sequential consistency, simplified,  *)
 (* with scoped SC axioms                *)

cat/opencl-overhauling.cat

@@ -1,5 +1,6 @@
 OpenCL
 (* OpenCL Memory Model *)
+include "basic.cat"
 
 (*
 * This model is based on:
@@ -97,6 +98,9 @@ empty (rf; [NAL & LOCAL])\vis(lhb) as O-NaRfL
 (* Consistency of RMWs *)
 irreflexive rf | (mo;mo;rf^-1) | (mo;rf) as O-Rmw
 
+// Atomicity
+empty rmw & (fre; coe) as atomic
+
 (**************************************)
 (* Sequential consistency, simplified *)
 (**************************************)

cat/opencl.cat

@@ -1,5 +1,6 @@
 OpenCL
 (* OpenCL Memory Model *)
+include "basic.cat"
 
 (*
 * This model is based on:
@@ -110,6 +111,9 @@ irreflexive (ghb | lhb); rf; [A] as atomic_rf_consistent
 (* Consistency of RMWs *)
 irreflexive rf | (fr;co) | (co;rf) as rmw_consistent
 
+// Atomicity
+empty rmw & (fre; coe) as atomic
+
 (**************************)
 (* Sequential consistency *)
 (**************************)