summaryrefslogtreecommitdiff
path: root/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
diff options
context:
space:
mode:
authorIngo Molnar <mingo@kernel.org>2018-04-12 10:42:34 +0300
committerIngo Molnar <mingo@kernel.org>2018-04-12 10:42:34 +0300
commitef389b734691cdc8beb009dd402135dcdcb86a56 (patch)
tree9523a37db93cb7c7874a5f18b4d9a7014898b814 /tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
parenta774635db5c430cbf21fa5d2f2df3d23aaa8e782 (diff)
parentc76fc98260751e71c884dc1a18a07e427ef033b5 (diff)
downloadlinux-ef389b734691cdc8beb009dd402135dcdcb86a56.tar.xz
Merge branch 'WIP.x86/asm' into x86/urgent, because the topic is ready
Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus')
-rw-r--r--tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus35
1 files changed, 35 insertions, 0 deletions
diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
new file mode 100644
index 000000000000..6a2bc12a1af1
--- /dev/null
+++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
@@ -0,0 +1,35 @@
+C WRC+poonceonces+Once
+
+(*
+ * Result: Sometimes
+ *
+ * This litmus test is an extension of the message-passing pattern,
+ * where the first write is moved to a separate process. Note that this
+ * test has no ordering at all.
+ *)
+
+{}
+
+P0(int *x)
+{
+ WRITE_ONCE(*x, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r0;
+
+ r0 = READ_ONCE(*x);
+ WRITE_ONCE(*y, 1);
+}
+
+P2(int *x, int *y)
+{
+ int r0;
+ int r1;
+
+ r0 = READ_ONCE(*y);
+ r1 = READ_ONCE(*x);
+}
+
+exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)