* [PATCH 1/3] CodeSamples/formal: Separate litmus7 compatible litmus tests
@ 2017-11-10 23:39 Akira Yokosawa
2017-11-10 23:40 ` [PATCH 2/3] CodeSamples/formal: Remove 2nd parentheses in tests under herd/ Akira Yokosawa
2017-11-10 23:41 ` [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling Akira Yokosawa
0 siblings, 2 replies; 10+ messages in thread
From: Akira Yokosawa @ 2017-11-10 23:39 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 73b24a9b12ed7b9d086658a026833c09fdfe8bbe Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 11 Nov 2017 00:49:53 +0900
Subject: [PATCH 1/3] CodeSamples/formal: Separate litmus7 compatible litmus tests
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
CodeSamples/formal/herd/.gitignore | 6 ---
CodeSamples/formal/herd/C-2+2W+o-o+o-o.litmus | 22 -----------
.../formal/herd/C-2+2W+o-wmb-o+o-wmb-o.litmus | 26 ------------
.../formal/herd/C-CCIRIW+o+o+o-o+o-o.litmus | 39 ------------------
.../formal/herd/C-ISA2+o-r+a-r+a-r+a-o.litmus | 41 -------------------
.../formal/herd/C-LB+a-o+o-data-o+o-data-o.litmus | 34 ----------------
.../formal/herd/C-LB+a-r+a-r+a-r+a-r.litmus | 42 --------------------
.../herd/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 27 -------------
.../formal/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus | 41 -------------------
.../formal/herd/C-LB+o-cge-o+o-cge-o.litmus | 27 -------------
.../formal/herd/C-LB+o-cgt-o+o-cgt-o.litmus | 27 -------------
.../herd/C-LB+o-data-o+o-data-o+o-data-o.litmus | 37 -----------------
CodeSamples/formal/herd/C-LB+o-o+o-o.litmus | 26 ------------
CodeSamples/formal/herd/C-LB+o-r+a-o.litmus | 26 ------------
CodeSamples/formal/herd/C-LB+o-r+o-ctrl-o.litmus | 27 -------------
CodeSamples/formal/herd/C-LB+o-r+o-data-o.litmus | 26 ------------
CodeSamples/formal/herd/C-MP+o-o+o-rmb-o.litmus | 28 -------------
CodeSamples/formal/herd/C-MP+o-r+o-ctrl-o.litmus | 27 -------------
.../formal/herd/C-MP+o-wmb-o+ld-addr-o.litmus | 30 --------------
.../formal/herd/C-MP+o-wmb-o+o-addr-o.litmus | 30 --------------
CodeSamples/formal/herd/C-MP+o-wmb-o+o-o.litmus | 28 -------------
.../formal/herd/C-MP+o-wmb-o+o-rmb-o.litmus | 29 --------------
.../formal/herd/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 29 --------------
CodeSamples/formal/herd/C-R+o-wmb-o+o-mb-o.litmus | 26 ------------
.../formal/herd/C-S+o-wmb-o+o-addr-o.litmus | 29 --------------
CodeSamples/formal/herd/C-SB+o-mb-o+o-mb-o.litmus | 28 -------------
CodeSamples/formal/herd/C-SB+o-o+o-o.litmus | 26 ------------
.../herd/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 33 ----------------
.../formal/herd/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 38 ------------------
.../formal/herd/C-W+RWC+o-r+a-o+o-mb-o.litmus | 37 -----------------
.../formal/herd/C-WRC+o+o-data-o+o-rmb-o.litmus | 33 ----------------
CodeSamples/formal/herd/C-WRC+o+o-r+a-o.litmus | 32 ---------------
.../formal/herd/C-WWC+o+o-data-o+o-addr-o.litmus | 36 -----------------
.../formal/herd/C-WWC+o+o-r+o-addr-o.litmus | 36 -----------------
.../herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 46 ----------------------
.../formal/herd/C-WWC+o-cge-o+o-cge-o+o.litmus | 32 ---------------
.../herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 46 ----------------------
.../formal/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 32 ---------------
.../formal/herd/C-Z6.2+o-r+a-o+o-mb-o.litmus | 36 -----------------
.../formal/herd/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 40 -------------------
CodeSamples/formal/herd/Makefile | 34 ----------------
CodeSamples/formal/herd/api.h | 23 -----------
CodeSamples/formal/litmus/.gitignore | 6 +++
CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 22 +++++++++++
.../formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 26 ++++++++++++
.../formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 39 ++++++++++++++++++
.../formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 41 +++++++++++++++++++
.../litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 34 ++++++++++++++++
.../formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 42 ++++++++++++++++++++
.../litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 27 +++++++++++++
.../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 41 +++++++++++++++++++
.../formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 27 +++++++++++++
.../formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 27 +++++++++++++
.../litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 37 +++++++++++++++++
CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 26 ++++++++++++
CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 26 ++++++++++++
CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 27 +++++++++++++
CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 26 ++++++++++++
CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 28 +++++++++++++
CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 27 +++++++++++++
.../formal/litmus/C-MP+o-wmb-o+ld-addr-o.litmus | 30 ++++++++++++++
.../formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 30 ++++++++++++++
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 28 +++++++++++++
.../formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 29 ++++++++++++++
.../formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 29 ++++++++++++++
.../formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 26 ++++++++++++
.../formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 29 ++++++++++++++
.../formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 28 +++++++++++++
CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 26 ++++++++++++
.../litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 33 ++++++++++++++++
.../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 38 ++++++++++++++++++
.../formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 37 +++++++++++++++++
.../formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 33 ++++++++++++++++
CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 32 +++++++++++++++
.../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 36 +++++++++++++++++
.../formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 36 +++++++++++++++++
.../litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 46 ++++++++++++++++++++++
.../formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 32 +++++++++++++++
.../litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 46 ++++++++++++++++++++++
.../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 32 +++++++++++++++
.../formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 36 +++++++++++++++++
.../formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 40 +++++++++++++++++++
CodeSamples/formal/litmus/Makefile | 34 ++++++++++++++++
CodeSamples/formal/litmus/api.h | 23 +++++++++++
84 files changed, 1318 insertions(+), 1318 deletions(-)
delete mode 100644 CodeSamples/formal/herd/.gitignore
delete mode 100644 CodeSamples/formal/herd/C-2+2W+o-o+o-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-2+2W+o-wmb-o+o-wmb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-CCIRIW+o+o+o-o+o-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-ISA2+o-r+a-r+a-r+a-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+a-o+o-data-o+o-data-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+a-r+a-r+a-r+a-r.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-cgt-o+o-cgt-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-data-o+o-data-o+o-data-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-o+o-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-r+a-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-r+o-ctrl-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-LB+o-r+o-data-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP+o-o+o-rmb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP+o-r+o-ctrl-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP+o-wmb-o+ld-addr-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP+o-wmb-o+o-addr-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP+o-wmb-o+o-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP+o-wmb-o+o-rmb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-MP-OMCA+o-o-o+o-rmb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-R+o-wmb-o+o-mb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-S+o-wmb-o+o-addr-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-SB+o-mb-o+o-mb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-SB+o-o+o-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-W+RWC+o-r+a-o+o-mb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-WRC+o+o-data-o+o-rmb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-WRC+o+o-r+a-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-WWC+o+o-data-o+o-addr-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-WWC+o+o-r+o-addr-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
delete mode 100644 CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
delete mode 100644 CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
delete mode 100644 CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
delete mode 100644 CodeSamples/formal/herd/C-Z6.2+o-r+a-o+o-mb-o.litmus
delete mode 100644 CodeSamples/formal/herd/C-Z6.2+o-r+a-r+a-r+a-o.litmus
delete mode 100644 CodeSamples/formal/herd/Makefile
delete mode 100644 CodeSamples/formal/herd/api.h
create mode 100644 CodeSamples/formal/litmus/.gitignore
create mode 100644 CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP+o-wmb-o+ld-addr-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
create mode 100644 CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus
create mode 100644 CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
create mode 100644 CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus
create mode 100644 CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
create mode 100644 CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus
create mode 100644 CodeSamples/formal/litmus/Makefile
create mode 100644 CodeSamples/formal/litmus/api.h
diff --git a/CodeSamples/formal/herd/.gitignore b/CodeSamples/formal/herd/.gitignore
deleted file mode 100644
index a01a568..0000000
--- a/CodeSamples/formal/herd/.gitignore
+++ /dev/null
@@ -1,6 +0,0 @@
-*.out
-/@all
-/X86
-/PPC
-/ARM
-*.tar
diff --git a/CodeSamples/formal/herd/C-2+2W+o-o+o-o.litmus b/CodeSamples/formal/herd/C-2+2W+o-o+o-o.litmus
deleted file mode 100644
index 2ea8808..0000000
--- a/CodeSamples/formal/herd/C-2+2W+o-o+o-o.litmus
+++ /dev/null
@@ -1,22 +0,0 @@
-C C-2+2W+o-o+o-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- WRITE_ONCE(*x0, 1);
- WRITE_ONCE(*x1, 2);
-}
-
-
-P1(int *x0, int *x1)
-{
- WRITE_ONCE(*x1, 1);
- WRITE_ONCE(*x0, 2);
-}
-
-exists (x0=1 /\ x1=1)
diff --git a/CodeSamples/formal/herd/C-2+2W+o-wmb-o+o-wmb-o.litmus b/CodeSamples/formal/herd/C-2+2W+o-wmb-o+o-wmb-o.litmus
deleted file mode 100644
index a58e637..0000000
--- a/CodeSamples/formal/herd/C-2+2W+o-wmb-o+o-wmb-o.litmus
+++ /dev/null
@@ -1,26 +0,0 @@
-C C-2+2W+o-wmb-o+o-wmb-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- WRITE_ONCE(*x0, 1);
- smp_wmb();
- WRITE_ONCE(*x1, 2);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- WRITE_ONCE(*x1, 1);
- smp_wmb();
- WRITE_ONCE(*x0, 2);
-}
-
-exists (x0=1 /\ x1=1)
diff --git a/CodeSamples/formal/herd/C-CCIRIW+o+o+o-o+o-o.litmus b/CodeSamples/formal/herd/C-CCIRIW+o+o+o-o+o-o.litmus
deleted file mode 100644
index 49a6a52..0000000
--- a/CodeSamples/formal/herd/C-CCIRIW+o+o+o-o+o-o.litmus
+++ /dev/null
@@ -1,39 +0,0 @@
-C C-CCIRIW+o+o+o-o+o-o
-
-{
-int x = 0;
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x)
-{
- WRITE_ONCE(*x, 1);
-}
-
-P1(int *x)
-{
- WRITE_ONCE(*x, 2);
-}
-
-P2(int *x)
-{
- int r1;
- int r2;
-
- r1 = READ_ONCE(*x);
- r2 = READ_ONCE(*x);
-}
-
-P3(int *x)
-{
- int r3;
- int r4;
-
- r3 = READ_ONCE(*x);
- r4 = READ_ONCE(*x);
-}
-
-exists(2:r1=1 /\ 2:r2=2 /\ 3:r3=2 /\ 3:r4=1)
diff --git a/CodeSamples/formal/herd/C-ISA2+o-r+a-r+a-r+a-o.litmus b/CodeSamples/formal/herd/C-ISA2+o-r+a-r+a-r+a-o.litmus
deleted file mode 100644
index 343fded..0000000
--- a/CodeSamples/formal/herd/C-ISA2+o-r+a-r+a-r+a-o.litmus
+++ /dev/null
@@ -1,41 +0,0 @@
-C C-ISA2+o-r+a-r+a-r+a-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- WRITE_ONCE(*x0, 2);
- smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
- int r2;
-
- r2 = smp_load_acquire(x1);
- smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
- int r2;
-
- r2 = smp_load_acquire(x2);
- smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
- int r1;
- int r2;
-
- r1 = smp_load_acquire(x3);
- r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
diff --git a/CodeSamples/formal/herd/C-LB+a-o+o-data-o+o-data-o.litmus b/CodeSamples/formal/herd/C-LB+a-o+o-data-o+o-data-o.litmus
deleted file mode 100644
index d517dae..0000000
--- a/CodeSamples/formal/herd/C-LB+a-o+o-data-o+o-data-o.litmus
+++ /dev/null
@@ -1,34 +0,0 @@
-C C-LB+a-o+o-data-o+o-data-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = smp_load_acquire(x0);
- WRITE_ONCE(*x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
- int r2;
-
- r2 = READ_ONCE(*x1);
- WRITE_ONCE(*x2, r2);
-}
-
-P2(int *x2, int *x0)
-{
- int r2;
-
- r2 = READ_ONCE(*x2);
- WRITE_ONCE(*x0, r2);
-}
-
-exists (0:r2=2 /\ 1:r2=2 /\ 2:r2=2)
diff --git a/CodeSamples/formal/herd/C-LB+a-r+a-r+a-r+a-r.litmus b/CodeSamples/formal/herd/C-LB+a-r+a-r+a-r+a-r.litmus
deleted file mode 100644
index 9105d41..0000000
--- a/CodeSamples/formal/herd/C-LB+a-r+a-r+a-r+a-r.litmus
+++ /dev/null
@@ -1,42 +0,0 @@
-C C-LB+a-r+a-r+a-r+a-r
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = smp_load_acquire(x0);
- smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
- int r2;
-
- r2 = smp_load_acquire(x1);
- smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
- int r2;
-
- r2 = smp_load_acquire(x2);
- smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
- int r2;
-
- r2 = smp_load_acquire(x3);
- smp_store_release(x0, 2);
-}
-
-exists (0:r2=2 /\ 1:r2=2 /\ 2:r2=2 /\ 3:r2=2)
diff --git a/CodeSamples/formal/herd/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus b/CodeSamples/formal/herd/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
deleted file mode 100644
index a026e2d..0000000
--- a/CodeSamples/formal/herd/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
+++ /dev/null
@@ -1,27 +0,0 @@
-C C-LB+cmpxchg-ctrl-o+o-ctrl-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = cmpxchg(x, 2, 3);
- if (r1 >= 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 >= 0)
- WRITE_ONCE(*x, 1);
-}
-
-exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus b/CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
deleted file mode 100644
index e97b879..0000000
--- a/CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
+++ /dev/null
@@ -1,41 +0,0 @@
-C C-LB+o-cge-o+o-cge-o+dstb
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 >= 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 >= 0)
- WRITE_ONCE(*x, 1);
-}
-
-/* P2 is to disturb compiler optimization */
-P2(int *x, int *y)
-{
- int r3;
- int r4;
-
- r3 = READ_ONCE(*x);
- r4 = READ_ONCE(*y);
- if (r3 < 0)
- WRITE_ONCE(*y, -1);
- if (r4 < 0)
- WRITE_ONCE(*x, -1);
-}
-
-exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o.litmus b/CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o.litmus
deleted file mode 100644
index 14539b9..0000000
--- a/CodeSamples/formal/herd/C-LB+o-cge-o+o-cge-o.litmus
+++ /dev/null
@@ -1,27 +0,0 @@
-C C-LB+o-cge-o+o-cge-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 >= 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 >= 0)
- WRITE_ONCE(*x, 1);
-}
-
-exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/herd/C-LB+o-cgt-o+o-cgt-o.litmus b/CodeSamples/formal/herd/C-LB+o-cgt-o+o-cgt-o.litmus
deleted file mode 100644
index d442f76..0000000
--- a/CodeSamples/formal/herd/C-LB+o-cgt-o+o-cgt-o.litmus
+++ /dev/null
@@ -1,27 +0,0 @@
-C C-LB+o-cgt-o+o-cgt-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 > 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 > 0)
- WRITE_ONCE(*x, 1);
-}
-
-exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/herd/C-LB+o-data-o+o-data-o+o-data-o.litmus b/CodeSamples/formal/herd/C-LB+o-data-o+o-data-o+o-data-o.litmus
deleted file mode 100644
index 98cbe27..0000000
--- a/CodeSamples/formal/herd/C-LB+o-data-o+o-data-o+o-data-o.litmus
+++ /dev/null
@@ -1,37 +0,0 @@
-C C-LB+o-data-o+o-data-o+o-data-o
-{
-int x0=0;
-int x1=1;
-int x2=2;
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x0);
- WRITE_ONCE(*x1, r2);
-}
-
-
-P1(int *x1, int *x2)
-{
- int r2;
-
- r2 = READ_ONCE(*x1);
- WRITE_ONCE(*x2, r2);
-}
-
-P2(int *x2, int *x0)
-{
- int r2;
-
- r2 = READ_ONCE(*x2);
- WRITE_ONCE(*x0, r2);
-}
-
-exists (0:r2=2 /\ 1:r2=0 /\ 2:r2=1)
diff --git a/CodeSamples/formal/herd/C-LB+o-o+o-o.litmus b/CodeSamples/formal/herd/C-LB+o-o+o-o.litmus
deleted file mode 100644
index 8ee530d..0000000
--- a/CodeSamples/formal/herd/C-LB+o-o+o-o.litmus
+++ /dev/null
@@ -1,26 +0,0 @@
-C C-LB+o-o+o-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x1);
- WRITE_ONCE(*x0, 2);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x0);
- WRITE_ONCE(*x1, 2);
-}
-
-exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/herd/C-LB+o-r+a-o.litmus b/CodeSamples/formal/herd/C-LB+o-r+a-o.litmus
deleted file mode 100644
index bab943c..0000000
--- a/CodeSamples/formal/herd/C-LB+o-r+a-o.litmus
+++ /dev/null
@@ -1,26 +0,0 @@
-C C-LB+o-r+a-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x1);
- smp_store_release(x0, 2);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- r2 = smp_load_acquire(x0);
- WRITE_ONCE(*x1, 2);
-}
-
-exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/herd/C-LB+o-r+o-ctrl-o.litmus b/CodeSamples/formal/herd/C-LB+o-r+o-ctrl-o.litmus
deleted file mode 100644
index ab55690..0000000
--- a/CodeSamples/formal/herd/C-LB+o-r+o-ctrl-o.litmus
+++ /dev/null
@@ -1,27 +0,0 @@
-C C-LB+o-r+o-ctrl-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x1);
- smp_store_release(x0, 2);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x0);
- if (r2 >= 0)
- WRITE_ONCE(*x1, 2);
-}
-
-exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/herd/C-LB+o-r+o-data-o.litmus b/CodeSamples/formal/herd/C-LB+o-r+o-data-o.litmus
deleted file mode 100644
index 42df8bf..0000000
--- a/CodeSamples/formal/herd/C-LB+o-r+o-data-o.litmus
+++ /dev/null
@@ -1,26 +0,0 @@
-C C-LB+o-r+o-data-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x1);
- smp_store_release(x0, 2);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- r2 = READ_ONCE(*x0);
- WRITE_ONCE(*x1, r2);
-}
-
-exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/herd/C-MP+o-o+o-rmb-o.litmus b/CodeSamples/formal/herd/C-MP+o-o+o-rmb-o.litmus
deleted file mode 100644
index 4b23976..0000000
--- a/CodeSamples/formal/herd/C-MP+o-o+o-rmb-o.litmus
+++ /dev/null
@@ -1,28 +0,0 @@
-C C-MP+o-o+o-rmb-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int* x1) {
-
- WRITE_ONCE(*x0, 2);
- WRITE_ONCE(*x1, 2);
-
-}
-
-P1(int* x0, int* x1) {
-
- int r2;
- int r3;
-
- r2 = READ_ONCE(*x1);
- smp_rmb();
- r3 = READ_ONCE(*x0);
-
-}
-
-exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/herd/C-MP+o-r+o-ctrl-o.litmus b/CodeSamples/formal/herd/C-MP+o-r+o-ctrl-o.litmus
deleted file mode 100644
index 82cf629..0000000
--- a/CodeSamples/formal/herd/C-MP+o-r+o-ctrl-o.litmus
+++ /dev/null
@@ -1,27 +0,0 @@
-C C-MP+o-r+o-ctrl-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int* x1) {
-
- WRITE_ONCE(*x0, 2);
- smp_store_release(x1, 2);
-
-}
-
-P1(int* x0, int* x1) {
- int r2;
- int r3 = 0;
-
- r2 = READ_ONCE(*x1);
- if (r2 >= 0)
- r3 = READ_ONCE(*x0);
-
-}
-
-exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/herd/C-MP+o-wmb-o+ld-addr-o.litmus b/CodeSamples/formal/herd/C-MP+o-wmb-o+ld-addr-o.litmus
deleted file mode 100644
index 117a6e3..0000000
--- a/CodeSamples/formal/herd/C-MP+o-wmb-o+ld-addr-o.litmus
+++ /dev/null
@@ -1,30 +0,0 @@
-C C-MP+o-wmb-o+ld-ad-o
-
-{
-int y=1;
-int *x1 = &y;
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int** x1) {
-
- WRITE_ONCE(*x0, 2);
- smp_wmb();
- WRITE_ONCE(*x1, x0);
-
-}
-
-P1(int** x1) {
-
- int *r2;
- int r3;
-
- r2 = lockless_dereference(*x1);
- r3 = READ_ONCE(*r2);
-
-}
-
-exists (1:r2=x0 /\ 1:r3=1)
diff --git a/CodeSamples/formal/herd/C-MP+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/herd/C-MP+o-wmb-o+o-addr-o.litmus
deleted file mode 100644
index 381fea8..0000000
--- a/CodeSamples/formal/herd/C-MP+o-wmb-o+o-addr-o.litmus
+++ /dev/null
@@ -1,30 +0,0 @@
-C C-MP+o-wmb-o+o-ad-o
-
-{
-int y=1;
-int *x1 = &y;
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int** x1) {
-
- WRITE_ONCE(*x0, 2);
- smp_wmb();
- WRITE_ONCE(*x1, x0);
-
-}
-
-P1(int** x1) {
-
- int *r2;
- int r3;
-
- r2 = READ_ONCE(*x1);
- r3 = READ_ONCE(*r2);
-
-}
-
-exists (1:r2=x0 /\ 1:r3=1)
diff --git a/CodeSamples/formal/herd/C-MP+o-wmb-o+o-o.litmus b/CodeSamples/formal/herd/C-MP+o-wmb-o+o-o.litmus
deleted file mode 100644
index 57cda9e..0000000
--- a/CodeSamples/formal/herd/C-MP+o-wmb-o+o-o.litmus
+++ /dev/null
@@ -1,28 +0,0 @@
-C C-MP+o-wmb-o+o-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int* x1) {
-
- WRITE_ONCE(*x0, 2);
- smp_wmb();
- WRITE_ONCE(*x1, 2);
-
-}
-
-P1(int* x0, int* x1) {
-
- int r2;
- int r3;
-
- r2 = READ_ONCE(*x1);
- r3 = READ_ONCE(*x0);
-
-}
-
-exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/herd/C-MP+o-wmb-o+o-rmb-o.litmus b/CodeSamples/formal/herd/C-MP+o-wmb-o+o-rmb-o.litmus
deleted file mode 100644
index 61e23db..0000000
--- a/CodeSamples/formal/herd/C-MP+o-wmb-o+o-rmb-o.litmus
+++ /dev/null
@@ -1,29 +0,0 @@
-C C-MP+o-wmb-o+o-rmb-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int* x1) {
-
- WRITE_ONCE(*x0, 2);
- smp_wmb();
- WRITE_ONCE(*x1, 2);
-
-}
-
-P1(int* x0, int* x1) {
-
- int r2;
- int r3;
-
- r2 = READ_ONCE(*x1);
- smp_rmb();
- r3 = READ_ONCE(*x0);
-
-}
-
-exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/herd/C-MP-OMCA+o-o-o+o-rmb-o.litmus b/CodeSamples/formal/herd/C-MP-OMCA+o-o-o+o-rmb-o.litmus
deleted file mode 100644
index c5c0242..0000000
--- a/CodeSamples/formal/herd/C-MP-OMCA+o-o-o+o-rmb-o.litmus
+++ /dev/null
@@ -1,29 +0,0 @@
-C C-MP-OMCA+o-o-o+o-rmb-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r0;
-
- WRITE_ONCE(*x, 1);
- r0 = READ_ONCE(*x);
- WRITE_ONCE(*y, r0);
-}
-
-P1(int *x, int *y)
-{
- int r1;
- int r2;
-
- r1 = READ_ONCE(*y);
- smp_rmb();
- r2 = READ_ONCE(*x);
-}
-
-exists (1:r1=1 /\ 1:r2=0)
diff --git a/CodeSamples/formal/herd/C-R+o-wmb-o+o-mb-o.litmus b/CodeSamples/formal/herd/C-R+o-wmb-o+o-mb-o.litmus
deleted file mode 100644
index d4f000c..0000000
--- a/CodeSamples/formal/herd/C-R+o-wmb-o+o-mb-o.litmus
+++ /dev/null
@@ -1,26 +0,0 @@
-C C-R+o-wmb-o+o-mb-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- WRITE_ONCE(*x0, 1);
- smp_wmb();
- WRITE_ONCE(*x1, 1);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- WRITE_ONCE(*x1, 2);
- smp_mb();
- r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=0 /\ x1=2)
diff --git a/CodeSamples/formal/herd/C-S+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/herd/C-S+o-wmb-o+o-addr-o.litmus
deleted file mode 100644
index 1ff49b1..0000000
--- a/CodeSamples/formal/herd/C-S+o-wmb-o+o-addr-o.litmus
+++ /dev/null
@@ -1,29 +0,0 @@
-C C-S+o-wmb-o+o-ad-o
-
-{
-int y=1;
-int *x1 = &y;
-}
-
-{
-#include "api.h"
-}
-
-P0(int* x0, int** x1) {
-
- WRITE_ONCE(*x0, 2);
- smp_wmb();
- WRITE_ONCE(*x1, x0);
-
-}
-
-P1(int** x1) {
-
- int *r2;
-
- r2 = READ_ONCE(*x1);
- WRITE_ONCE(*r2, 3);
-
-}
-
-exists (1:r2=x0 /\ x0=2)
diff --git a/CodeSamples/formal/herd/C-SB+o-mb-o+o-mb-o.litmus b/CodeSamples/formal/herd/C-SB+o-mb-o+o-mb-o.litmus
deleted file mode 100644
index 1093329..0000000
--- a/CodeSamples/formal/herd/C-SB+o-mb-o+o-mb-o.litmus
+++ /dev/null
@@ -1,28 +0,0 @@
-C C-SB+o-mb-o+o-mb-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- WRITE_ONCE(*x0, 2);
- smp_mb();
- r2 = READ_ONCE(*x1);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- WRITE_ONCE(*x1, 2);
- smp_mb();
- r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=0 /\ 0:r2=0)
diff --git a/CodeSamples/formal/herd/C-SB+o-o+o-o.litmus b/CodeSamples/formal/herd/C-SB+o-o+o-o.litmus
deleted file mode 100644
index 2e45ee6..0000000
--- a/CodeSamples/formal/herd/C-SB+o-o+o-o.litmus
+++ /dev/null
@@ -1,26 +0,0 @@
-C C-SB+o-o+o-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r2;
-
- WRITE_ONCE(*x0, 2);
- r2 = READ_ONCE(*x1);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r2;
-
- WRITE_ONCE(*x1, 2);
- r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=0 /\ 0:r2=0)
diff --git a/CodeSamples/formal/herd/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus b/CodeSamples/formal/herd/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
deleted file mode 100644
index e150296..0000000
--- a/CodeSamples/formal/herd/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
+++ /dev/null
@@ -1,33 +0,0 @@
-C C-SB-OMCA+o-o-rmb-o+o-o-rmb-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- int r1;
- int r2;
-
- WRITE_ONCE(*x0, 2);
- r1 = READ_ONCE(*x0);
- smp_rmb();
- r2 = READ_ONCE(*x1);
-}
-
-
-P1(int *x0, int *x1)
-{
- int r1;
- int r2;
-
- WRITE_ONCE(*x1, 2);
- r1 = READ_ONCE(*x1);
- smp_rmb();
- r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=0 /\ 0:r2=0 /\ 1:r1=2 /\ 0:r1=2)
diff --git a/CodeSamples/formal/herd/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus b/CodeSamples/formal/herd/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
deleted file mode 100644
index 23050e6..0000000
--- a/CodeSamples/formal/herd/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
+++ /dev/null
@@ -1,38 +0,0 @@
-C C-W+RWC+o-mb-o+a-o+o-mb-o
-
-{
-int x = 0;
-int y = 0;
-int z = 0;
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- WRITE_ONCE(*x, 1);
- smp_mb();
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *y, int *z)
-{
- int r1;
- int r2;
-
- r1 = smp_load_acquire(y);
- r2 = READ_ONCE(*z);
-}
-
-P2(int *z, int *x)
-{
- int r3;
-
- WRITE_ONCE(*z, 1);
- smp_mb();
- r3 = READ_ONCE(*x);
-}
-
-exists(1:r1=1 /\ 1:r2=0 /\ 2:r3=0)
diff --git a/CodeSamples/formal/herd/C-W+RWC+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/herd/C-W+RWC+o-r+a-o+o-mb-o.litmus
deleted file mode 100644
index 527b373..0000000
--- a/CodeSamples/formal/herd/C-W+RWC+o-r+a-o+o-mb-o.litmus
+++ /dev/null
@@ -1,37 +0,0 @@
-C C-W+RWC+o-r+a-o+o-mb-o
-
-{
-int x = 0;
-int y = 0;
-int z = 0;
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- WRITE_ONCE(*x, 1);
- smp_store_release(y, 1);
-}
-
-P1(int *y, int *z)
-{
- int r1;
- int r2;
-
- r1 = smp_load_acquire(y);
- r2 = READ_ONCE(*z);
-}
-
-P2(int *z, int *x)
-{
- int r3;
-
- WRITE_ONCE(*z, 1);
- smp_mb();
- r3 = READ_ONCE(*x);
-}
-
-exists(1:r1=1 /\ 1:r2=0 /\ 2:r3=0)
diff --git a/CodeSamples/formal/herd/C-WRC+o+o-data-o+o-rmb-o.litmus b/CodeSamples/formal/herd/C-WRC+o+o-data-o+o-rmb-o.litmus
deleted file mode 100644
index 602e800..0000000
--- a/CodeSamples/formal/herd/C-WRC+o+o-data-o+o-rmb-o.litmus
+++ /dev/null
@@ -1,33 +0,0 @@
-C C-WRC+o+o-data-o+o-rmb-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x)
-{
- WRITE_ONCE(*x, 1);
-}
-
-P1(int *x, int* y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- WRITE_ONCE(*y, r1);
-}
-
-P2(int *x, int* y)
-{
- int r2;
- int r3;
-
- r2 = READ_ONCE(*y);
- smp_rmb();
- r3 = READ_ONCE(*x);
-}
-
-exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
diff --git a/CodeSamples/formal/herd/C-WRC+o+o-r+a-o.litmus b/CodeSamples/formal/herd/C-WRC+o+o-r+a-o.litmus
deleted file mode 100644
index 6d55ead..0000000
--- a/CodeSamples/formal/herd/C-WRC+o+o-r+a-o.litmus
+++ /dev/null
@@ -1,32 +0,0 @@
-C C-WRC+o+o-r+a-o
-
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x)
-{
- WRITE_ONCE(*x, 1);
-}
-
-P1(int *x, int* y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- smp_store_release(y, r1);
-}
-
-P2(int *x, int* y)
-{
- int r2;
- int r3;
-
- r2 = smp_load_acquire(y);
- r3 = READ_ONCE(*x);
-}
-
-exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
diff --git a/CodeSamples/formal/herd/C-WWC+o+o-data-o+o-addr-o.litmus b/CodeSamples/formal/herd/C-WWC+o+o-data-o+o-addr-o.litmus
deleted file mode 100644
index c0cbee8..0000000
--- a/CodeSamples/formal/herd/C-WWC+o+o-data-o+o-addr-o.litmus
+++ /dev/null
@@ -1,36 +0,0 @@
-C C-WWC+o+o-data-o+o-addr-o
-
-{
-int a = 0;
-int b = 0;
-int *c = &b;
-int *x = &a;
-int *y = &b;
-}
-
-{
-#include "api.h"
-}
-
-P0(int **x)
-{
- WRITE_ONCE(*x, x);
-}
-
-P1(int **x, int **y)
-{
- int *r1;
-
- r1 = READ_ONCE(*x);
- WRITE_ONCE(*y, r1);
-}
-
-P2(int **y, int **c)
-{
- int *r2;
-
- r2 = READ_ONCE(*y);
- WRITE_ONCE(*r2, c);
-}
-
-exists(1:r1=x /\ 2:r2=x /\ x=x)
diff --git a/CodeSamples/formal/herd/C-WWC+o+o-r+o-addr-o.litmus b/CodeSamples/formal/herd/C-WWC+o+o-r+o-addr-o.litmus
deleted file mode 100644
index 6f0a810..0000000
--- a/CodeSamples/formal/herd/C-WWC+o+o-r+o-addr-o.litmus
+++ /dev/null
@@ -1,36 +0,0 @@
-C C-WWC+o+o-r+o-addr-o
-
-{
-int a = 0;
-int b = 0;
-int *c = &b;
-int *x = &a;
-int *y = &b;
-}
-
-{
-#include "api.h"
-}
-
-P0(int **x)
-{
- WRITE_ONCE(*x, x);
-}
-
-P1(int **x, int **y)
-{
- int *r1;
-
- r1 = READ_ONCE(*x);
- smp_store_release(y, r1);
-}
-
-P2(int **y, int **c)
-{
- int *r2;
-
- r2 = READ_ONCE(*y);
- WRITE_ONCE(*r2, c);
-}
-
-exists(1:r1=x /\ 2:r2=x /\ x=x)
diff --git a/CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus b/CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
deleted file mode 100644
index 015bcd0..0000000
--- a/CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
+++ /dev/null
@@ -1,46 +0,0 @@
-C C-WWC+o-cge-o+o-cge-o+o+dstb
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 >= 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 >= 0)
- WRITE_ONCE(*x, 1);
-}
-
-P2(int *x)
-{
- WRITE_ONCE(*x, 2);
-}
-
-/* P3 is to disturb compiler optimization */
-P3(int *x, int *y)
-{
- int r3;
- int r4;
-
- r3 = READ_ONCE(*x);
- r4 = READ_ONCE(*y);
- if (r3 < 0)
- WRITE_ONCE(*y, -1);
- if (r4 < 0)
- WRITE_ONCE(*x, -1);
-}
-
-exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o.litmus b/CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
deleted file mode 100644
index 3fcd502..0000000
--- a/CodeSamples/formal/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
+++ /dev/null
@@ -1,32 +0,0 @@
-C C-WWC+o-cge-o+o-cge-o+o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 >= 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 >= 0)
- WRITE_ONCE(*x, 1);
-}
-
-P2(int *x)
-{
- WRITE_ONCE(*x, 2);
-}
-
-exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus b/CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
deleted file mode 100644
index 989d99f..0000000
--- a/CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
+++ /dev/null
@@ -1,46 +0,0 @@
-C C-WWC+o-cgt-o+o-cgt-o+o+dstb
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 > 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 > 0)
- WRITE_ONCE(*x, 1);
-}
-
-P2(int *x)
-{
- WRITE_ONCE(*x, 2);
-}
-
-/* P3 is to disturb compiler optimization */
-P3(int *x, int *y)
-{
- int r3;
- int r4;
-
- r3 = READ_ONCE(*x);
- r4 = READ_ONCE(*y);
- if (r3 < 0)
- WRITE_ONCE(*y, -1);
- if (r4 < 0)
- WRITE_ONCE(*x, -1);
-}
-
-exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus b/CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
deleted file mode 100644
index bfe5449..0000000
--- a/CodeSamples/formal/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
+++ /dev/null
@@ -1,32 +0,0 @@
-C C-WWC+o-cgt-o+o-cgt-o+o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- int r1;
-
- r1 = READ_ONCE(*x);
- if (r1 > 0)
- WRITE_ONCE(*y, 1);
-}
-
-P1(int *x, int *y)
-{
- int r2;
-
- r2 = READ_ONCE(*y);
- if (r2 > 0)
- WRITE_ONCE(*x, 1);
-}
-
-P2(int *x)
-{
- WRITE_ONCE(*x, 2);
-}
-
-exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/herd/C-Z6.2+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/herd/C-Z6.2+o-r+a-o+o-mb-o.litmus
deleted file mode 100644
index 9563e6a..0000000
--- a/CodeSamples/formal/herd/C-Z6.2+o-r+a-o+o-mb-o.litmus
+++ /dev/null
@@ -1,36 +0,0 @@
-C C-Z6.2+o-r+a-o+o-mb-o
-
-{
-int x = 0;
-int y = 0;
-int z = 0;
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x, int *y)
-{
- WRITE_ONCE(*x, 1);
- smp_store_release(y, 1);
-}
-
-P1(int *y, int *z)
-{
- int r1;
-
- r1 = smp_load_acquire(y);
- WRITE_ONCE(*z, 1);
-}
-
-P2(int *z, int *x)
-{
- int r3;
-
- WRITE_ONCE(*z, 2);
- smp_mb();
- r2 = READ_ONCE(*x);
-}
-
-exists(1:r1=1 /\ 2:r2=0 /\ z=2)
diff --git a/CodeSamples/formal/herd/C-Z6.2+o-r+a-r+a-r+a-o.litmus b/CodeSamples/formal/herd/C-Z6.2+o-r+a-r+a-r+a-o.litmus
deleted file mode 100644
index 34f7bbb..0000000
--- a/CodeSamples/formal/herd/C-Z6.2+o-r+a-r+a-r+a-o.litmus
+++ /dev/null
@@ -1,40 +0,0 @@
-C C-Z6.2+o-r+a-r+a-r+a-o
-{
-}
-
-{
-#include "api.h"
-}
-
-P0(int *x0, int *x1)
-{
- WRITE_ONCE(*x0, 2);
- smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
- int r2;
-
- r2 = smp_load_acquire(x1);
- smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
- int r2;
-
- r2 = smp_load_acquire(x2);
- smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
- int r2;
-
- r2 = smp_load_acquire(x3);
- WRITE_ONCE(*x0, 3);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r2=2 /\ x0=2)
diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile
deleted file mode 100644
index 96c4495..0000000
--- a/CodeSamples/formal/herd/Makefile
+++ /dev/null
@@ -1,34 +0,0 @@
-LITMUS := $(wildcard *.litmus)
-LITMUS_OUT = $(addsuffix .out,$(LITMUS))
-CCOPTS = -fomit-frame-pointer -O2
-CCOPTS += -I$(shell pwd)
-CUSTOM_HEADER := $(wildcard *.h)
-
-.PHONY: all clean cross-x86 cross-ppc cross-arm cross
-
-all: $(LITMUS_OUT)
-
-%.litmus.out: %.litmus $(CUSTOM_HEADER)
- litmus7 -r 1000 -carch X86 -ccopts "$(CCOPTS)" $< > $@ 2>&1
-
-cross-x86: TARGET = X86
-cross-x86: cross
-
-cross-ppc: TARGET = PPC
-cross-ppc: cross
-
-cross-arm: TARGET = ARM
-cross-arm: cross
-
-cross:
- echo > @all
- for l in $(LITMUS); do \
- echo $$l >> @all; \
- done
- mkdir -p $(TARGET)
- litmus7 -r 1000 -carch $(TARGET) -o $(TARGET) @all
- cp $(CUSTOM_HEADER) $(TARGET)
-
-clean:
- rm -f *.out
- rm -f @all
diff --git a/CodeSamples/formal/herd/api.h b/CodeSamples/formal/herd/api.h
deleted file mode 100644
index 0f14a48..0000000
--- a/CodeSamples/formal/herd/api.h
+++ /dev/null
@@ -1,23 +0,0 @@
-#ifndef __API_H__
-#define __API_H__
-#ifndef READ_ONCE
-#define READ_ONCE(x) __atomic_load_n((typeof(x) *)&(x), __ATOMIC_RELAXED)
-#define WRITE_ONCE(x, v) __atomic_store_n((typeof(x) *)&(x), (v), __ATOMIC_RELAXED)
-#define smp_mb() __atomic_thread_fence(__ATOMIC_SEQ_CST)
-#define smp_rmb() __atomic_thread_fence(__ATOMIC_ACQUIRE) /* outside std. */
-#define smp_wmb() __atomic_thread_fence(__ATOMIC_RELEASE) /* outside std. */
-#define smp_load_acquire(x) __atomic_load_n(x, __ATOMIC_ACQUIRE)
-#define smp_store_release(x, v) __atomic_store_n(x, v, __ATOMIC_RELEASE)
-#define smp_load_acquire(x) __atomic_load_n(x, __ATOMIC_ACQUIRE)
-#define cmpxchg(x, o, n) ({ \
- typeof(o) __old = (o); \
- __atomic_compare_exchange_n((x), &__old, (n), 1, __ATOMIC_SEQ_CST, __ATOMIC_RELAXED); \
- __old; \
-})
-#ifdef __alpha__
-#define lockless_dereference(x) ({ typeof(x) ___x = READ_ONCE(x); smp_mb(); ___x; })
-#else
-#define lockless_dereference(x) READ_ONCE(x)
-#endif
-#endif
-#endif
diff --git a/CodeSamples/formal/litmus/.gitignore b/CodeSamples/formal/litmus/.gitignore
new file mode 100644
index 0000000..a01a568
--- /dev/null
+++ b/CodeSamples/formal/litmus/.gitignore
@@ -0,0 +1,6 @@
+*.out
+/@all
+/X86
+/PPC
+/ARM
+*.tar
diff --git a/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus
new file mode 100644
index 0000000..2ea8808
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus
@@ -0,0 +1,22 @@
+C C-2+2W+o-o+o-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ WRITE_ONCE(*x1, 1);
+ WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
diff --git a/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus b/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
new file mode 100644
index 0000000..a58e637
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
@@ -0,0 +1,26 @@
+C C-2+2W+o-wmb-o+o-wmb-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ smp_wmb();
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ WRITE_ONCE(*x1, 1);
+ smp_wmb();
+ WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
diff --git a/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus
new file mode 100644
index 0000000..49a6a52
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus
@@ -0,0 +1,39 @@
+C C-CCIRIW+o+o+o-o+o-o
+
+{
+int x = 0;
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x)
+{
+ WRITE_ONCE(*x, 1);
+}
+
+P1(int *x)
+{
+ WRITE_ONCE(*x, 2);
+}
+
+P2(int *x)
+{
+ int r1;
+ int r2;
+
+ r1 = READ_ONCE(*x);
+ r2 = READ_ONCE(*x);
+}
+
+P3(int *x)
+{
+ int r3;
+ int r4;
+
+ r3 = READ_ONCE(*x);
+ r4 = READ_ONCE(*x);
+}
+
+exists(2:r1=1 /\ 2:r2=2 /\ 3:r3=2 /\ 3:r4=1)
diff --git a/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus b/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus
new file mode 100644
index 0000000..343fded
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus
@@ -0,0 +1,41 @@
+C C-ISA2+o-r+a-r+a-r+a-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 2);
+ smp_store_release(x1, 2);
+}
+
+
+P1(int *x1, int *x2)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x1);
+ smp_store_release(x2, 2);
+}
+
+P2(int *x2, int *x3)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x2);
+ smp_store_release(x3, 2);
+}
+
+P3(int *x3, int *x0)
+{
+ int r1;
+ int r2;
+
+ r1 = smp_load_acquire(x3);
+ r2 = READ_ONCE(*x0);
+}
+
+exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
diff --git a/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus b/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus
new file mode 100644
index 0000000..d517dae
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus
@@ -0,0 +1,34 @@
+C C-LB+a-o+o-data-o+o-data-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x0);
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x1, int *x2)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x1);
+ WRITE_ONCE(*x2, r2);
+}
+
+P2(int *x2, int *x0)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x2);
+ WRITE_ONCE(*x0, r2);
+}
+
+exists (0:r2=2 /\ 1:r2=2 /\ 2:r2=2)
diff --git a/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus b/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus
new file mode 100644
index 0000000..9105d41
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus
@@ -0,0 +1,42 @@
+C C-LB+a-r+a-r+a-r+a-r
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x0);
+ smp_store_release(x1, 2);
+}
+
+
+P1(int *x1, int *x2)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x1);
+ smp_store_release(x2, 2);
+}
+
+P2(int *x2, int *x3)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x2);
+ smp_store_release(x3, 2);
+}
+
+P3(int *x3, int *x0)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x3);
+ smp_store_release(x0, 2);
+}
+
+exists (0:r2=2 /\ 1:r2=2 /\ 2:r2=2 /\ 3:r2=2)
diff --git a/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus b/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
new file mode 100644
index 0000000..a026e2d
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
@@ -0,0 +1,27 @@
+C C-LB+cmpxchg-ctrl-o+o-ctrl-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = cmpxchg(x, 2, 3);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus
new file mode 100644
index 0000000..e97b879
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus
@@ -0,0 +1,41 @@
+C C-LB+o-cge-o+o-cge-o+dstb
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+/* P2 is to disturb compiler optimization */
+P2(int *x, int *y)
+{
+ int r3;
+ int r4;
+
+ r3 = READ_ONCE(*x);
+ r4 = READ_ONCE(*y);
+ if (r3 < 0)
+ WRITE_ONCE(*y, -1);
+ if (r4 < 0)
+ WRITE_ONCE(*x, -1);
+}
+
+exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus
new file mode 100644
index 0000000..14539b9
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus
@@ -0,0 +1,27 @@
+C C-LB+o-cge-o+o-cge-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus b/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus
new file mode 100644
index 0000000..d442f76
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus
@@ -0,0 +1,27 @@
+C C-LB+o-cgt-o+o-cgt-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 > 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 > 0)
+ WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus b/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus
new file mode 100644
index 0000000..98cbe27
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus
@@ -0,0 +1,37 @@
+C C-LB+o-data-o+o-data-o+o-data-o
+{
+int x0=0;
+int x1=1;
+int x2=2;
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x0);
+ WRITE_ONCE(*x1, r2);
+}
+
+
+P1(int *x1, int *x2)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x1);
+ WRITE_ONCE(*x2, r2);
+}
+
+P2(int *x2, int *x0)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x2);
+ WRITE_ONCE(*x0, r2);
+}
+
+exists (0:r2=2 /\ 1:r2=0 /\ 2:r2=1)
diff --git a/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus
new file mode 100644
index 0000000..8ee530d
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus
@@ -0,0 +1,26 @@
+C C-LB+o-o+o-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x1);
+ WRITE_ONCE(*x0, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x0);
+ WRITE_ONCE(*x1, 2);
+}
+
+exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus b/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus
new file mode 100644
index 0000000..bab943c
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus
@@ -0,0 +1,26 @@
+C C-LB+o-r+a-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x1);
+ smp_store_release(x0, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x0);
+ WRITE_ONCE(*x1, 2);
+}
+
+exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus b/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus
new file mode 100644
index 0000000..ab55690
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus
@@ -0,0 +1,27 @@
+C C-LB+o-r+o-ctrl-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x1);
+ smp_store_release(x0, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x0);
+ if (r2 >= 0)
+ WRITE_ONCE(*x1, 2);
+}
+
+exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus b/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus
new file mode 100644
index 0000000..42df8bf
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus
@@ -0,0 +1,26 @@
+C C-LB+o-r+o-data-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x1);
+ smp_store_release(x0, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ r2 = READ_ONCE(*x0);
+ WRITE_ONCE(*x1, r2);
+}
+
+exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus
new file mode 100644
index 0000000..4b23976
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus
@@ -0,0 +1,28 @@
+C C-MP+o-o+o-rmb-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int* x1) {
+
+ WRITE_ONCE(*x0, 2);
+ WRITE_ONCE(*x1, 2);
+
+}
+
+P1(int* x0, int* x1) {
+
+ int r2;
+ int r3;
+
+ r2 = READ_ONCE(*x1);
+ smp_rmb();
+ r3 = READ_ONCE(*x0);
+
+}
+
+exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus b/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus
new file mode 100644
index 0000000..82cf629
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus
@@ -0,0 +1,27 @@
+C C-MP+o-r+o-ctrl-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int* x1) {
+
+ WRITE_ONCE(*x0, 2);
+ smp_store_release(x1, 2);
+
+}
+
+P1(int* x0, int* x1) {
+ int r2;
+ int r3 = 0;
+
+ r2 = READ_ONCE(*x1);
+ if (r2 >= 0)
+ r3 = READ_ONCE(*x0);
+
+}
+
+exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+ld-addr-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+ld-addr-o.litmus
new file mode 100644
index 0000000..117a6e3
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+ld-addr-o.litmus
@@ -0,0 +1,30 @@
+C C-MP+o-wmb-o+ld-ad-o
+
+{
+int y=1;
+int *x1 = &y;
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int** x1) {
+
+ WRITE_ONCE(*x0, 2);
+ smp_wmb();
+ WRITE_ONCE(*x1, x0);
+
+}
+
+P1(int** x1) {
+
+ int *r2;
+ int r3;
+
+ r2 = lockless_dereference(*x1);
+ r3 = READ_ONCE(*r2);
+
+}
+
+exists (1:r2=x0 /\ 1:r3=1)
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
new file mode 100644
index 0000000..381fea8
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
@@ -0,0 +1,30 @@
+C C-MP+o-wmb-o+o-ad-o
+
+{
+int y=1;
+int *x1 = &y;
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int** x1) {
+
+ WRITE_ONCE(*x0, 2);
+ smp_wmb();
+ WRITE_ONCE(*x1, x0);
+
+}
+
+P1(int** x1) {
+
+ int *r2;
+ int r3;
+
+ r2 = READ_ONCE(*x1);
+ r3 = READ_ONCE(*r2);
+
+}
+
+exists (1:r2=x0 /\ 1:r3=1)
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus
new file mode 100644
index 0000000..57cda9e
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus
@@ -0,0 +1,28 @@
+C C-MP+o-wmb-o+o-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int* x1) {
+
+ WRITE_ONCE(*x0, 2);
+ smp_wmb();
+ WRITE_ONCE(*x1, 2);
+
+}
+
+P1(int* x0, int* x1) {
+
+ int r2;
+ int r3;
+
+ r2 = READ_ONCE(*x1);
+ r3 = READ_ONCE(*x0);
+
+}
+
+exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus
new file mode 100644
index 0000000..61e23db
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus
@@ -0,0 +1,29 @@
+C C-MP+o-wmb-o+o-rmb-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int* x1) {
+
+ WRITE_ONCE(*x0, 2);
+ smp_wmb();
+ WRITE_ONCE(*x1, 2);
+
+}
+
+P1(int* x0, int* x1) {
+
+ int r2;
+ int r3;
+
+ r2 = READ_ONCE(*x1);
+ smp_rmb();
+ r3 = READ_ONCE(*x0);
+
+}
+
+exists (1:r2=2 /\ 1:r3=0)
diff --git a/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus
new file mode 100644
index 0000000..c5c0242
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus
@@ -0,0 +1,29 @@
+C C-MP-OMCA+o-o-o+o-rmb-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r0;
+
+ WRITE_ONCE(*x, 1);
+ r0 = READ_ONCE(*x);
+ WRITE_ONCE(*y, r0);
+}
+
+P1(int *x, int *y)
+{
+ int r1;
+ int r2;
+
+ r1 = READ_ONCE(*y);
+ smp_rmb();
+ r2 = READ_ONCE(*x);
+}
+
+exists (1:r1=1 /\ 1:r2=0)
diff --git a/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus
new file mode 100644
index 0000000..d4f000c
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus
@@ -0,0 +1,26 @@
+C C-R+o-wmb-o+o-mb-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ smp_wmb();
+ WRITE_ONCE(*x1, 1);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ WRITE_ONCE(*x1, 2);
+ smp_mb();
+ r2 = READ_ONCE(*x0);
+}
+
+exists (1:r2=0 /\ x1=2)
diff --git a/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
new file mode 100644
index 0000000..1ff49b1
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
@@ -0,0 +1,29 @@
+C C-S+o-wmb-o+o-ad-o
+
+{
+int y=1;
+int *x1 = &y;
+}
+
+{
+#include "api.h"
+}
+
+P0(int* x0, int** x1) {
+
+ WRITE_ONCE(*x0, 2);
+ smp_wmb();
+ WRITE_ONCE(*x1, x0);
+
+}
+
+P1(int** x1) {
+
+ int *r2;
+
+ r2 = READ_ONCE(*x1);
+ WRITE_ONCE(*r2, 3);
+
+}
+
+exists (1:r2=x0 /\ x0=2)
diff --git a/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus
new file mode 100644
index 0000000..1093329
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus
@@ -0,0 +1,28 @@
+C C-SB+o-mb-o+o-mb-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ WRITE_ONCE(*x0, 2);
+ smp_mb();
+ r2 = READ_ONCE(*x1);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ WRITE_ONCE(*x1, 2);
+ smp_mb();
+ r2 = READ_ONCE(*x0);
+}
+
+exists (1:r2=0 /\ 0:r2=0)
diff --git a/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus
new file mode 100644
index 0000000..2e45ee6
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus
@@ -0,0 +1,26 @@
+C C-SB+o-o+o-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r2;
+
+ WRITE_ONCE(*x0, 2);
+ r2 = READ_ONCE(*x1);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r2;
+
+ WRITE_ONCE(*x1, 2);
+ r2 = READ_ONCE(*x0);
+}
+
+exists (1:r2=0 /\ 0:r2=0)
diff --git a/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus b/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
new file mode 100644
index 0000000..e150296
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
@@ -0,0 +1,33 @@
+C C-SB-OMCA+o-o-rmb-o+o-o-rmb-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ int r1;
+ int r2;
+
+ WRITE_ONCE(*x0, 2);
+ r1 = READ_ONCE(*x0);
+ smp_rmb();
+ r2 = READ_ONCE(*x1);
+}
+
+
+P1(int *x0, int *x1)
+{
+ int r1;
+ int r2;
+
+ WRITE_ONCE(*x1, 2);
+ r1 = READ_ONCE(*x1);
+ smp_rmb();
+ r2 = READ_ONCE(*x0);
+}
+
+exists (1:r2=0 /\ 0:r2=0 /\ 1:r1=2 /\ 0:r1=2)
diff --git a/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
new file mode 100644
index 0000000..23050e6
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
@@ -0,0 +1,38 @@
+C C-W+RWC+o-mb-o+a-o+o-mb-o
+
+{
+int x = 0;
+int y = 0;
+int z = 0;
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ WRITE_ONCE(*x, 1);
+ smp_mb();
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *y, int *z)
+{
+ int r1;
+ int r2;
+
+ r1 = smp_load_acquire(y);
+ r2 = READ_ONCE(*z);
+}
+
+P2(int *z, int *x)
+{
+ int r3;
+
+ WRITE_ONCE(*z, 1);
+ smp_mb();
+ r3 = READ_ONCE(*x);
+}
+
+exists(1:r1=1 /\ 1:r2=0 /\ 2:r3=0)
diff --git a/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus
new file mode 100644
index 0000000..527b373
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus
@@ -0,0 +1,37 @@
+C C-W+RWC+o-r+a-o+o-mb-o
+
+{
+int x = 0;
+int y = 0;
+int z = 0;
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ WRITE_ONCE(*x, 1);
+ smp_store_release(y, 1);
+}
+
+P1(int *y, int *z)
+{
+ int r1;
+ int r2;
+
+ r1 = smp_load_acquire(y);
+ r2 = READ_ONCE(*z);
+}
+
+P2(int *z, int *x)
+{
+ int r3;
+
+ WRITE_ONCE(*z, 1);
+ smp_mb();
+ r3 = READ_ONCE(*x);
+}
+
+exists(1:r1=1 /\ 1:r2=0 /\ 2:r3=0)
diff --git a/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus
new file mode 100644
index 0000000..602e800
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus
@@ -0,0 +1,33 @@
+C C-WRC+o+o-data-o+o-rmb-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x)
+{
+ WRITE_ONCE(*x, 1);
+}
+
+P1(int *x, int* y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ WRITE_ONCE(*y, r1);
+}
+
+P2(int *x, int* y)
+{
+ int r2;
+ int r3;
+
+ r2 = READ_ONCE(*y);
+ smp_rmb();
+ r3 = READ_ONCE(*x);
+}
+
+exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
diff --git a/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus b/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus
new file mode 100644
index 0000000..6d55ead
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus
@@ -0,0 +1,32 @@
+C C-WRC+o+o-r+a-o
+
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x)
+{
+ WRITE_ONCE(*x, 1);
+}
+
+P1(int *x, int* y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ smp_store_release(y, r1);
+}
+
+P2(int *x, int* y)
+{
+ int r2;
+ int r3;
+
+ r2 = smp_load_acquire(y);
+ r3 = READ_ONCE(*x);
+}
+
+exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
diff --git a/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
new file mode 100644
index 0000000..c0cbee8
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
@@ -0,0 +1,36 @@
+C C-WWC+o+o-data-o+o-addr-o
+
+{
+int a = 0;
+int b = 0;
+int *c = &b;
+int *x = &a;
+int *y = &b;
+}
+
+{
+#include "api.h"
+}
+
+P0(int **x)
+{
+ WRITE_ONCE(*x, x);
+}
+
+P1(int **x, int **y)
+{
+ int *r1;
+
+ r1 = READ_ONCE(*x);
+ WRITE_ONCE(*y, r1);
+}
+
+P2(int **y, int **c)
+{
+ int *r2;
+
+ r2 = READ_ONCE(*y);
+ WRITE_ONCE(*r2, c);
+}
+
+exists(1:r1=x /\ 2:r2=x /\ x=x)
diff --git a/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus b/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
new file mode 100644
index 0000000..6f0a810
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
@@ -0,0 +1,36 @@
+C C-WWC+o+o-r+o-addr-o
+
+{
+int a = 0;
+int b = 0;
+int *c = &b;
+int *x = &a;
+int *y = &b;
+}
+
+{
+#include "api.h"
+}
+
+P0(int **x)
+{
+ WRITE_ONCE(*x, x);
+}
+
+P1(int **x, int **y)
+{
+ int *r1;
+
+ r1 = READ_ONCE(*x);
+ smp_store_release(y, r1);
+}
+
+P2(int **y, int **c)
+{
+ int *r2;
+
+ r2 = READ_ONCE(*y);
+ WRITE_ONCE(*r2, c);
+}
+
+exists(1:r1=x /\ 2:r2=x /\ x=x)
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
new file mode 100644
index 0000000..015bcd0
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
@@ -0,0 +1,46 @@
+C C-WWC+o-cge-o+o-cge-o+o+dstb
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+P2(int *x)
+{
+ WRITE_ONCE(*x, 2);
+}
+
+/* P3 is to disturb compiler optimization */
+P3(int *x, int *y)
+{
+ int r3;
+ int r4;
+
+ r3 = READ_ONCE(*x);
+ r4 = READ_ONCE(*y);
+ if (r3 < 0)
+ WRITE_ONCE(*y, -1);
+ if (r4 < 0)
+ WRITE_ONCE(*x, -1);
+}
+
+exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus
new file mode 100644
index 0000000..3fcd502
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus
@@ -0,0 +1,32 @@
+C C-WWC+o-cge-o+o-cge-o+o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+P2(int *x)
+{
+ WRITE_ONCE(*x, 2);
+}
+
+exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
new file mode 100644
index 0000000..989d99f
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
@@ -0,0 +1,46 @@
+C C-WWC+o-cgt-o+o-cgt-o+o+dstb
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 > 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 > 0)
+ WRITE_ONCE(*x, 1);
+}
+
+P2(int *x)
+{
+ WRITE_ONCE(*x, 2);
+}
+
+/* P3 is to disturb compiler optimization */
+P3(int *x, int *y)
+{
+ int r3;
+ int r4;
+
+ r3 = READ_ONCE(*x);
+ r4 = READ_ONCE(*y);
+ if (r3 < 0)
+ WRITE_ONCE(*y, -1);
+ if (r4 < 0)
+ WRITE_ONCE(*x, -1);
+}
+
+exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus
new file mode 100644
index 0000000..bfe5449
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus
@@ -0,0 +1,32 @@
+C C-WWC+o-cgt-o+o-cgt-o+o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 > 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 > 0)
+ WRITE_ONCE(*x, 1);
+}
+
+P2(int *x)
+{
+ WRITE_ONCE(*x, 2);
+}
+
+exists (0:r1=2 /\ 1:r2=1 /\ x=2)
diff --git a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
new file mode 100644
index 0000000..9563e6a
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
@@ -0,0 +1,36 @@
+C C-Z6.2+o-r+a-o+o-mb-o
+
+{
+int x = 0;
+int y = 0;
+int z = 0;
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ WRITE_ONCE(*x, 1);
+ smp_store_release(y, 1);
+}
+
+P1(int *y, int *z)
+{
+ int r1;
+
+ r1 = smp_load_acquire(y);
+ WRITE_ONCE(*z, 1);
+}
+
+P2(int *z, int *x)
+{
+ int r3;
+
+ WRITE_ONCE(*z, 2);
+ smp_mb();
+ r2 = READ_ONCE(*x);
+}
+
+exists(1:r1=1 /\ 2:r2=0 /\ z=2)
diff --git a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus
new file mode 100644
index 0000000..34f7bbb
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus
@@ -0,0 +1,40 @@
+C C-Z6.2+o-r+a-r+a-r+a-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 2);
+ smp_store_release(x1, 2);
+}
+
+
+P1(int *x1, int *x2)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x1);
+ smp_store_release(x2, 2);
+}
+
+P2(int *x2, int *x3)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x2);
+ smp_store_release(x3, 2);
+}
+
+P3(int *x3, int *x0)
+{
+ int r2;
+
+ r2 = smp_load_acquire(x3);
+ WRITE_ONCE(*x0, 3);
+}
+
+exists (1:r2=2 /\ 2:r2=2 /\ 3:r2=2 /\ x0=2)
diff --git a/CodeSamples/formal/litmus/Makefile b/CodeSamples/formal/litmus/Makefile
new file mode 100644
index 0000000..96c4495
--- /dev/null
+++ b/CodeSamples/formal/litmus/Makefile
@@ -0,0 +1,34 @@
+LITMUS := $(wildcard *.litmus)
+LITMUS_OUT = $(addsuffix .out,$(LITMUS))
+CCOPTS = -fomit-frame-pointer -O2
+CCOPTS += -I$(shell pwd)
+CUSTOM_HEADER := $(wildcard *.h)
+
+.PHONY: all clean cross-x86 cross-ppc cross-arm cross
+
+all: $(LITMUS_OUT)
+
+%.litmus.out: %.litmus $(CUSTOM_HEADER)
+ litmus7 -r 1000 -carch X86 -ccopts "$(CCOPTS)" $< > $@ 2>&1
+
+cross-x86: TARGET = X86
+cross-x86: cross
+
+cross-ppc: TARGET = PPC
+cross-ppc: cross
+
+cross-arm: TARGET = ARM
+cross-arm: cross
+
+cross:
+ echo > @all
+ for l in $(LITMUS); do \
+ echo $$l >> @all; \
+ done
+ mkdir -p $(TARGET)
+ litmus7 -r 1000 -carch $(TARGET) -o $(TARGET) @all
+ cp $(CUSTOM_HEADER) $(TARGET)
+
+clean:
+ rm -f *.out
+ rm -f @all
diff --git a/CodeSamples/formal/litmus/api.h b/CodeSamples/formal/litmus/api.h
new file mode 100644
index 0000000..0f14a48
--- /dev/null
+++ b/CodeSamples/formal/litmus/api.h
@@ -0,0 +1,23 @@
+#ifndef __API_H__
+#define __API_H__
+#ifndef READ_ONCE
+#define READ_ONCE(x) __atomic_load_n((typeof(x) *)&(x), __ATOMIC_RELAXED)
+#define WRITE_ONCE(x, v) __atomic_store_n((typeof(x) *)&(x), (v), __ATOMIC_RELAXED)
+#define smp_mb() __atomic_thread_fence(__ATOMIC_SEQ_CST)
+#define smp_rmb() __atomic_thread_fence(__ATOMIC_ACQUIRE) /* outside std. */
+#define smp_wmb() __atomic_thread_fence(__ATOMIC_RELEASE) /* outside std. */
+#define smp_load_acquire(x) __atomic_load_n(x, __ATOMIC_ACQUIRE)
+#define smp_store_release(x, v) __atomic_store_n(x, v, __ATOMIC_RELEASE)
+#define smp_load_acquire(x) __atomic_load_n(x, __ATOMIC_ACQUIRE)
+#define cmpxchg(x, o, n) ({ \
+ typeof(o) __old = (o); \
+ __atomic_compare_exchange_n((x), &__old, (n), 1, __ATOMIC_SEQ_CST, __ATOMIC_RELAXED); \
+ __old; \
+})
+#ifdef __alpha__
+#define lockless_dereference(x) ({ typeof(x) ___x = READ_ONCE(x); smp_mb(); ___x; })
+#else
+#define lockless_dereference(x) READ_ONCE(x)
+#endif
+#endif
+#endif
--
2.7.4
^ permalink raw reply related [flat|nested] 10+ messages in thread
* [PATCH 2/3] CodeSamples/formal: Remove 2nd parentheses in tests under herd/
2017-11-10 23:39 [PATCH 1/3] CodeSamples/formal: Separate litmus7 compatible litmus tests Akira Yokosawa
@ 2017-11-10 23:40 ` Akira Yokosawa
2017-11-10 23:41 ` [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling Akira Yokosawa
1 sibling, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2017-11-10 23:40 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 89710e2fb5d2692ed9b3912d907c9fc4bd15ba3e Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 11 Nov 2017 01:08:35 +0900
Subject: [PATCH 2/3] CodeSamples/formal: Remove 2nd parentheses in tests under herd/
These are incompatible with "herd7" command.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 4 ----
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 4 ----
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 4 ----
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 4 ----
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 4 ----
5 files changed, 20 deletions(-)
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
index cee5912..ae64726 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
@@ -3,10 +3,6 @@ C C-SB+l-o-o-u+l-o-o-u-C
{
}
-{
-#include "api.h"
-}
-
P0(int *sl, int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus
index b331740..1e2dd5b 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus
@@ -3,10 +3,6 @@ C C-SB+l-o-o-u+l-o-o-u-CE
{
}
-{
-#include "api.h"
-}
-
P0(int *sl, int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
index e8c489d..30a7fe7 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
@@ -3,10 +3,6 @@ C C-SB+l-o-o-u+l-o-o-u-X
{
}
-{
-#include "api.h"
-}
-
P0(int *sl, int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus
index 51aa67b..28a0f83 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus
@@ -3,10 +3,6 @@ C C-SB+l-o-o-u+l-o-o-u-XE
{
}
-{
-#include "api.h"
-}
-
P0(int *sl, int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus
index c7df045..c16d8f9 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus
@@ -3,10 +3,6 @@ C C-SB+l-o-o-u+l-o-o-u
{
}
-{
-#include "api.h"
-}
-
P0(spinlock_t *sl, int *x0, int *x1)
{
int r1;
--
2.7.4
^ permalink raw reply related [flat|nested] 10+ messages in thread
* [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-10 23:39 [PATCH 1/3] CodeSamples/formal: Separate litmus7 compatible litmus tests Akira Yokosawa
2017-11-10 23:40 ` [PATCH 2/3] CodeSamples/formal: Remove 2nd parentheses in tests under herd/ Akira Yokosawa
@ 2017-11-10 23:41 ` Akira Yokosawa
2017-11-10 23:56 ` Akira Yokosawa
1 sibling, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2017-11-10 23:41 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sat, 11 Nov 2017 08:25:34 +0900
Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
Also fix corresponding code snippet.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 2 +-
memorder/memorder.tex | 2 +-
3 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus b/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
index a58e637..7f06c85 100644
--- a/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
@@ -16,8 +16,6 @@ P0(int *x0, int *x1)
P1(int *x0, int *x1)
{
- int r2;
-
WRITE_ONCE(*x1, 1);
smp_wmb();
WRITE_ONCE(*x0, 2);
diff --git a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
index 9563e6a..8d766bf 100644
--- a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
+++ b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
@@ -26,7 +26,7 @@ P1(int *y, int *z)
P2(int *z, int *x)
{
- int r3;
+ int r2;
WRITE_ONCE(*z, 2);
smp_mb();
diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index 28be8b2..7d8e497 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -2824,7 +2824,7 @@ P1(int *y, int *z)
P2(int *z, int *x)
{
- int r3;
+ int r2;
WRITE_ONCE(*z, 2);
smp_mb();
--
2.7.4
^ permalink raw reply related [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-10 23:41 ` [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling Akira Yokosawa
@ 2017-11-10 23:56 ` Akira Yokosawa
2017-11-11 16:44 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2017-11-10 23:56 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
>>From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sat, 11 Nov 2017 08:25:34 +0900
> Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
>
> Also fix corresponding code snippet.
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
somewhere in the memorder chapter?
Thanks, Akira
> CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 2 +-
> memorder/memorder.tex | 2 +-
> 3 files changed, 2 insertions(+), 4 deletions(-)
>
[...]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-10 23:56 ` Akira Yokosawa
@ 2017-11-11 16:44 ` Paul E. McKenney
2017-11-11 16:57 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Paul E. McKenney @ 2017-11-11 16:44 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
> On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
> >>From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
> > From: Akira Yokosawa <akiyks@gmail.com>
> > Date: Sat, 11 Nov 2017 08:25:34 +0900
> > Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
> >
> > Also fix corresponding code snippet.
> >
> > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > ---
> > CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
>
> By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
> somewhere in the memorder chapter?
Good point, it is an odd corner case that is worth at least a quick quiz.
How about the following?
Thanx, Paul
------------------------------------------------------------------------
commit 9b44286879769a0973982807c80b6e0a7821a1de
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date: Sat Nov 11 08:41:47 2017 -0800
memorder: Add a quick quiz for the 2+2W litmus tests
Reported-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index 7d8e4978fa6d..327b1ad254bf 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
This should not come as a surprise to anyone who carefully examined
Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.
-But sometimes time is on our side, as shown in the next section.
+\begin{listing}[tbp]
+{ \scriptsize
+\begin{verbbox}[\LstLineNo]
+C C-2+2W+o-wmb-o+o-wmb-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ smp_wmb();
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ WRITE_ONCE(*x1, 1);
+ smp_wmb();
+ WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
+\end{verbbox}
+}
+\centering
+\theverbbox
+\caption{2+2W Litmus Test With Write Barriers}
+\label{lst:memorder:2+2W Litmus Test With Write Barriers}
+\end{listing}
+
+\QuickQuiz{}
+ But for litmus tests having only ordered stores, as shown in
+ Figure~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
+ (\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
+ research shows that the cycle is prohibited, even in weakly
+ ordered systems such as ARM and Power~\cite{test6-pdf}.
+ Given that, are store-to-store really \emph{always}
+ counter-temporal???
+\QuickQuizAnswer{
+ This litmus test is indeed a very interesting curiosity.
+ Its ordering apparently occurs naturally given typical
+ weakly ordered hardware design, which would normally be
+ considered a great gift from the relevant laws of physics
+ and cache-coherency-protocol mathematics.
+
+ Unfortunately, no one has been able to come up with a software use
+ case for this gift that does not have a much better alternative
+ implementation.
+ Therefore, neither the C11 nor the Linux kernel memory models
+ provide any guarantee corresponding to
+ Figure~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
+
+\begin{listing}[tbp]
+{ \scriptsize
+\begin{verbbox}[\LstLineNo]
+C C-2+2W+o-o+o-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ WRITE_ONCE(*x1, 1);
+ WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
+\end{verbbox}
+}
+\centering
+\theverbbox
+\caption{2+2W Litmus Test Without Write Barriers}
+\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
+\end{listing}%
+%
+ Of course, without the barrier, there are no ordering
+ guarantees, even on real weakly ordered hardware, as shown in
+ Figure~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
+ (\path{C-2+2W+o-o+o-o.litmus}).
+} \QuickQuizEnd
+
+But sometimes time really is on our side. Read on!
\subsubsection{Happens-Before}
\label{sec:memorder:Happens-Before}
^ permalink raw reply related [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-11 16:44 ` Paul E. McKenney
@ 2017-11-11 16:57 ` Paul E. McKenney
2017-11-11 23:26 ` Akira Yokosawa
0 siblings, 1 reply; 10+ messages in thread
From: Paul E. McKenney @ 2017-11-11 16:57 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Nov 11, 2017 at 08:44:38AM -0800, Paul E. McKenney wrote:
> On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
> > On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
> > >>From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
> > > From: Akira Yokosawa <akiyks@gmail.com>
> > > Date: Sat, 11 Nov 2017 08:25:34 +0900
> > > Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
> > >
> > > Also fix corresponding code snippet.
> > >
> > > Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> > > ---
> > > CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
> >
> > By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
> > somewhere in the memorder chapter?
>
> Good point, it is an odd corner case that is worth at least a quick quiz.
> How about the following?
My fingers just keep automatically typing "Figure", so please see a
corrected patch below. Presumably my fingers will get with the program
in a few months. ;-)
Thanx, Paul
------------------------------------------------------------------------
commit ac730edc868b6c8a9a71637fd205553e7ba88df2
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date: Sat Nov 11 08:41:47 2017 -0800
memorder: Add a quick quiz for the 2+2W litmus tests
Reported-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index 7d8e4978fa6d..2ef8363fba6a 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
This should not come as a surprise to anyone who carefully examined
Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.
-But sometimes time is on our side, as shown in the next section.
+\begin{listing}[tbp]
+{ \scriptsize
+\begin{verbbox}[\LstLineNo]
+C C-2+2W+o-wmb-o+o-wmb-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ smp_wmb();
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ WRITE_ONCE(*x1, 1);
+ smp_wmb();
+ WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
+\end{verbbox}
+}
+\centering
+\theverbbox
+\caption{2+2W Litmus Test With Write Barriers}
+\label{lst:memorder:2+2W Litmus Test With Write Barriers}
+\end{listing}
+
+\QuickQuiz{}
+ But for litmus tests having only ordered stores, as shown in
+ Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
+ (\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
+ research shows that the cycle is prohibited, even in weakly
+ ordered systems such as ARM and Power~\cite{test6-pdf}.
+ Given that, are store-to-store really \emph{always}
+ counter-temporal???
+\QuickQuizAnswer{
+ This litmus test is indeed a very interesting curiosity.
+ Its ordering apparently occurs naturally given typical
+ weakly ordered hardware design, which would normally be
+ considered a great gift from the relevant laws of physics
+ and cache-coherency-protocol mathematics.
+
+ Unfortunately, no one has been able to come up with a software use
+ case for this gift that does not have a much better alternative
+ implementation.
+ Therefore, neither the C11 nor the Linux kernel memory models
+ provide any guarantee corresponding to
+ Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
+
+\begin{listing}[tbp]
+{ \scriptsize
+\begin{verbbox}[\LstLineNo]
+C C-2+2W+o-o+o-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x0, int *x1)
+{
+ WRITE_ONCE(*x0, 1);
+ WRITE_ONCE(*x1, 2);
+}
+
+
+P1(int *x0, int *x1)
+{
+ WRITE_ONCE(*x1, 1);
+ WRITE_ONCE(*x0, 2);
+}
+
+exists (x0=1 /\ x1=1)
+\end{verbbox}
+}
+\centering
+\theverbbox
+\caption{2+2W Litmus Test Without Write Barriers}
+\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
+\end{listing}%
+%
+ Of course, without the barrier, there are no ordering
+ guarantees, even on real weakly ordered hardware, as shown in
+ Listing~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
+ (\path{C-2+2W+o-o+o-o.litmus}).
+} \QuickQuizEnd
+
+But sometimes time really is on our side. Read on!
\subsubsection{Happens-Before}
\label{sec:memorder:Happens-Before}
^ permalink raw reply related [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-11 16:57 ` Paul E. McKenney
@ 2017-11-11 23:26 ` Akira Yokosawa
2017-11-12 1:29 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2017-11-11 23:26 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
On 2017/11/11 08:57:23 -0800, Paul E. McKenney wrote:
> On Sat, Nov 11, 2017 at 08:44:38AM -0800, Paul E. McKenney wrote:
>> On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
>>> On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
>>>> >From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
>>>> From: Akira Yokosawa <akiyks@gmail.com>
>>>> Date: Sat, 11 Nov 2017 08:25:34 +0900
>>>> Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
>>>>
>>>> Also fix corresponding code snippet.
>>>>
>>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>>>> ---
>>>> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
>>>
>>> By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
>>> somewhere in the memorder chapter?
>>
>> Good point, it is an odd corner case that is worth at least a quick quiz.
>> How about the following?
>
> My fingers just keep automatically typing "Figure", so please see a
> corrected patch below. Presumably my fingers will get with the program
> in a few months. ;-)
;-) ;-)
Please see inline (nitpicking) comments below.
Thanks, Akira
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit ac730edc868b6c8a9a71637fd205553e7ba88df2
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date: Sat Nov 11 08:41:47 2017 -0800
>
> memorder: Add a quick quiz for the 2+2W litmus tests
>
> Reported-by: Akira Yokosawa <akiyks@gmail.com>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>
> diff --git a/memorder/memorder.tex b/memorder/memorder.tex
> index 7d8e4978fa6d..2ef8363fba6a 100644
> --- a/memorder/memorder.tex
> +++ b/memorder/memorder.tex
> @@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
> This should not come as a surprise to anyone who carefully examined
> Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.
>
> -But sometimes time is on our side, as shown in the next section.
> +\begin{listing}[tbp]
> +{ \scriptsize
> +\begin{verbbox}[\LstLineNo]
> +C C-2+2W+o-wmb-o+o-wmb-o
> +{
> +}
> +
> +{
> +#include "api.h"
> +}
2nd parentheses should be removed in code snippets.
> +
> +P0(int *x0, int *x1)
> +{
> + WRITE_ONCE(*x0, 1);
> + smp_wmb();
> + WRITE_ONCE(*x1, 2);
> +}
Need to convert "tab" -> " ".
> +
> +
> +P1(int *x0, int *x1)
> +{
> + WRITE_ONCE(*x1, 1);
> + smp_wmb();
> + WRITE_ONCE(*x0, 2);
> +}
> +
> +exists (x0=1 /\ x1=1)
> +\end{verbbox}
> +}
> +\centering
> +\theverbbox
> +\caption{2+2W Litmus Test With Write Barriers}
> +\label{lst:memorder:2+2W Litmus Test With Write Barriers}
> +\end{listing}
> +
> +\QuickQuiz{}
> + But for litmus tests having only ordered stores, as shown in
> + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
> + (\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
> + research shows that the cycle is prohibited, even in weakly
> + ordered systems such as ARM and Power~\cite{test6-pdf}.
> + Given that, are store-to-store really \emph{always}
> + counter-temporal???
> +\QuickQuizAnswer{
> + This litmus test is indeed a very interesting curiosity.
> + Its ordering apparently occurs naturally given typical
> + weakly ordered hardware design, which would normally be
> + considered a great gift from the relevant laws of physics
> + and cache-coherency-protocol mathematics.
> +
> + Unfortunately, no one has been able to come up with a software use
> + case for this gift that does not have a much better alternative
> + implementation.
> + Therefore, neither the C11 nor the Linux kernel memory models
> + provide any guarantee corresponding to
> + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
And the exists clause triggers by herd7 verification. (Redundant???)
> +
> +\begin{listing}[tbp]
> +{ \scriptsize
> +\begin{verbbox}[\LstLineNo]
> +C C-2+2W+o-o+o-o
> +{
> +}
> +
> +{
> +#include "api.h"
> +}
Ditto.
> +
> +P0(int *x0, int *x1)
> +{
> + WRITE_ONCE(*x0, 1);
> + WRITE_ONCE(*x1, 2);
Ditto.
> +}
> +
> +
> +P1(int *x0, int *x1)
> +{
> + WRITE_ONCE(*x1, 1);
> + WRITE_ONCE(*x0, 2);
> +}
> +
> +exists (x0=1 /\ x1=1)
> +\end{verbbox}
> +}
> +\centering
> +\theverbbox
> +\caption{2+2W Litmus Test Without Write Barriers}
> +\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
> +\end{listing}%
> +%
These "%"s have no effect because of the blank line above the
"listing" environment. You can remove them if you are OK with
the following sentence starting a new paragraph.
> + Of course, without the barrier, there are no ordering
> + guarantees, even on real weakly ordered hardware, as shown in
> + Listing~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
> + (\path{C-2+2W+o-o+o-o.litmus}).
> +} \QuickQuizEnd
> +
> +But sometimes time really is on our side. Read on!
>
> \subsubsection{Happens-Before}
> \label{sec:memorder:Happens-Before}
>
>
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-11 23:26 ` Akira Yokosawa
@ 2017-11-12 1:29 ` Paul E. McKenney
2017-11-12 2:27 ` Akira Yokosawa
0 siblings, 1 reply; 10+ messages in thread
From: Paul E. McKenney @ 2017-11-12 1:29 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sun, Nov 12, 2017 at 08:26:21AM +0900, Akira Yokosawa wrote:
> On 2017/11/11 08:57:23 -0800, Paul E. McKenney wrote:
> > On Sat, Nov 11, 2017 at 08:44:38AM -0800, Paul E. McKenney wrote:
> >> On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
> >>> On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
> >>>> >From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
> >>>> From: Akira Yokosawa <akiyks@gmail.com>
> >>>> Date: Sat, 11 Nov 2017 08:25:34 +0900
> >>>> Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
> >>>>
> >>>> Also fix corresponding code snippet.
> >>>>
> >>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >>>> ---
> >>>> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
> >>>
> >>> By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
> >>> somewhere in the memorder chapter?
> >>
> >> Good point, it is an odd corner case that is worth at least a quick quiz.
> >> How about the following?
> >
> > My fingers just keep automatically typing "Figure", so please see a
> > corrected patch below. Presumably my fingers will get with the program
> > in a few months. ;-)
>
> ;-) ;-)
>
> Please see inline (nitpicking) comments below.
>
> Thanks, Akira
>
> >
> > Thanx, Paul
> >
> > ------------------------------------------------------------------------
> >
> > commit ac730edc868b6c8a9a71637fd205553e7ba88df2
> > Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > Date: Sat Nov 11 08:41:47 2017 -0800
> >
> > memorder: Add a quick quiz for the 2+2W litmus tests
> >
> > Reported-by: Akira Yokosawa <akiyks@gmail.com>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> >
> > diff --git a/memorder/memorder.tex b/memorder/memorder.tex
> > index 7d8e4978fa6d..2ef8363fba6a 100644
> > --- a/memorder/memorder.tex
> > +++ b/memorder/memorder.tex
> > @@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
> > This should not come as a surprise to anyone who carefully examined
> > Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.
> >
> > -But sometimes time is on our side, as shown in the next section.
> > +\begin{listing}[tbp]
> > +{ \scriptsize
> > +\begin{verbbox}[\LstLineNo]
> > +C C-2+2W+o-wmb-o+o-wmb-o
> > +{
> > +}
> > +
> > +{
> > +#include "api.h"
> > +}
>
> 2nd parentheses should be removed in code snippets.
>
> > +
> > +P0(int *x0, int *x1)
> > +{
> > + WRITE_ONCE(*x0, 1);
> > + smp_wmb();
> > + WRITE_ONCE(*x1, 2);
> > +}
>
> Need to convert "tab" -> " ".
Good catches, fixed.
> > +
> > +
> > +P1(int *x0, int *x1)
> > +{
> > + WRITE_ONCE(*x1, 1);
> > + smp_wmb();
> > + WRITE_ONCE(*x0, 2);
> > +}
> > +
> > +exists (x0=1 /\ x1=1)
> > +\end{verbbox}
> > +}
> > +\centering
> > +\theverbbox
> > +\caption{2+2W Litmus Test With Write Barriers}
> > +\label{lst:memorder:2+2W Litmus Test With Write Barriers}
> > +\end{listing}
> > +
> > +\QuickQuiz{}
> > + But for litmus tests having only ordered stores, as shown in
> > + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
> > + (\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
> > + research shows that the cycle is prohibited, even in weakly
> > + ordered systems such as ARM and Power~\cite{test6-pdf}.
> > + Given that, are store-to-store really \emph{always}
> > + counter-temporal???
> > +\QuickQuizAnswer{
> > + This litmus test is indeed a very interesting curiosity.
> > + Its ordering apparently occurs naturally given typical
> > + weakly ordered hardware design, which would normally be
> > + considered a great gift from the relevant laws of physics
> > + and cache-coherency-protocol mathematics.
> > +
> > + Unfortunately, no one has been able to come up with a software use
> > + case for this gift that does not have a much better alternative
> > + implementation.
> > + Therefore, neither the C11 nor the Linux kernel memory models
> > + provide any guarantee corresponding to
> > + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
>
> And the exists clause triggers by herd7 verification. (Redundant???)
Good point, added.
> > +
> > +\begin{listing}[tbp]
> > +{ \scriptsize
> > +\begin{verbbox}[\LstLineNo]
> > +C C-2+2W+o-o+o-o
> > +{
> > +}
> > +
> > +{
> > +#include "api.h"
> > +}
>
> Ditto.
>
> > +
> > +P0(int *x0, int *x1)
> > +{
> > + WRITE_ONCE(*x0, 1);
> > + WRITE_ONCE(*x1, 2);
>
> Ditto.
And these.
> > +}
> > +
> > +
> > +P1(int *x0, int *x1)
> > +{
> > + WRITE_ONCE(*x1, 1);
> > + WRITE_ONCE(*x0, 2);
> > +}
> > +
> > +exists (x0=1 /\ x1=1)
> > +\end{verbbox}
> > +}
> > +\centering
> > +\theverbbox
> > +\caption{2+2W Litmus Test Without Write Barriers}
> > +\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
> > +\end{listing}%
> > +%
>
> These "%"s have no effect because of the blank line above the
> "listing" environment. You can remove them if you are OK with
> the following sentence starting a new paragraph.
OK, I removed them. So we only need the "%"s if we want the figure
in the middle of a paragraph?
Thanx, Paul
> > + Of course, without the barrier, there are no ordering
> > + guarantees, even on real weakly ordered hardware, as shown in
> > + Listing~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
> > + (\path{C-2+2W+o-o+o-o.litmus}).
> > +} \QuickQuizEnd
> > +
> > +But sometimes time really is on our side. Read on!
> >
> > \subsubsection{Happens-Before}
> > \label{sec:memorder:Happens-Before}
> >
> >
>
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-12 1:29 ` Paul E. McKenney
@ 2017-11-12 2:27 ` Akira Yokosawa
2017-11-12 17:15 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2017-11-12 2:27 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
On 2017/11/12 10:29, Paul E. McKenney wrote:
> On Sun, Nov 12, 2017 at 08:26:21AM +0900, Akira Yokosawa wrote:
>> On 2017/11/11 08:57:23 -0800, Paul E. McKenney wrote:
>>> On Sat, Nov 11, 2017 at 08:44:38AM -0800, Paul E. McKenney wrote:
>>>> On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
>>>>> On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
>>>>>> >From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
>>>>>> From: Akira Yokosawa <akiyks@gmail.com>
>>>>>> Date: Sat, 11 Nov 2017 08:25:34 +0900
>>>>>> Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
>>>>>>
>>>>>> Also fix corresponding code snippet.
>>>>>>
>>>>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>>>>>> ---
>>>>>> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
>>>>>
>>>>> By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
>>>>> somewhere in the memorder chapter?
>>>>
>>>> Good point, it is an odd corner case that is worth at least a quick quiz.
>>>> How about the following?
>>>
>>> My fingers just keep automatically typing "Figure", so please see a
>>> corrected patch below. Presumably my fingers will get with the program
>>> in a few months. ;-)
>>
>> ;-) ;-)
>>
>> Please see inline (nitpicking) comments below.
>>
>> Thanks, Akira
>>
>>>
>>> Thanx, Paul
>>>
>>> ------------------------------------------------------------------------
>>>
>>> commit ac730edc868b6c8a9a71637fd205553e7ba88df2
>>> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>>> Date: Sat Nov 11 08:41:47 2017 -0800
>>>
>>> memorder: Add a quick quiz for the 2+2W litmus tests
>>>
>>> Reported-by: Akira Yokosawa <akiyks@gmail.com>
>>> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
>>>
>>> diff --git a/memorder/memorder.tex b/memorder/memorder.tex
>>> index 7d8e4978fa6d..2ef8363fba6a 100644
>>> --- a/memorder/memorder.tex
>>> +++ b/memorder/memorder.tex
>>> @@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
>>> This should not come as a surprise to anyone who carefully examined
>>> Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.
>>>
>>> -But sometimes time is on our side, as shown in the next section.
>>> +\begin{listing}[tbp]
>>> +{ \scriptsize
>>> +\begin{verbbox}[\LstLineNo]
>>> +C C-2+2W+o-wmb-o+o-wmb-o
>>> +{
>>> +}
>>> +
>>> +{
>>> +#include "api.h"
>>> +}
>>
>> 2nd parentheses should be removed in code snippets.
>>
>>> +
>>> +P0(int *x0, int *x1)
>>> +{
>>> + WRITE_ONCE(*x0, 1);
>>> + smp_wmb();
>>> + WRITE_ONCE(*x1, 2);
>>> +}
>>
>> Need to convert "tab" -> " ".
>
> Good catches, fixed.
>
>>> +
>>> +
>>> +P1(int *x0, int *x1)
>>> +{
>>> + WRITE_ONCE(*x1, 1);
>>> + smp_wmb();
>>> + WRITE_ONCE(*x0, 2);
>>> +}
>>> +
>>> +exists (x0=1 /\ x1=1)
>>> +\end{verbbox}
>>> +}
>>> +\centering
>>> +\theverbbox
>>> +\caption{2+2W Litmus Test With Write Barriers}
>>> +\label{lst:memorder:2+2W Litmus Test With Write Barriers}
>>> +\end{listing}
>>> +
>>> +\QuickQuiz{}
>>> + But for litmus tests having only ordered stores, as shown in
>>> + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
>>> + (\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
>>> + research shows that the cycle is prohibited, even in weakly
>>> + ordered systems such as ARM and Power~\cite{test6-pdf}.
>>> + Given that, are store-to-store really \emph{always}
>>> + counter-temporal???
>>> +\QuickQuizAnswer{
>>> + This litmus test is indeed a very interesting curiosity.
>>> + Its ordering apparently occurs naturally given typical
>>> + weakly ordered hardware design, which would normally be
>>> + considered a great gift from the relevant laws of physics
>>> + and cache-coherency-protocol mathematics.
>>> +
>>> + Unfortunately, no one has been able to come up with a software use
>>> + case for this gift that does not have a much better alternative
>>> + implementation.
>>> + Therefore, neither the C11 nor the Linux kernel memory models
>>> + provide any guarantee corresponding to
>>> + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
>>
>> And the exists clause triggers by herd7 verification. (Redundant???)
>
> Good point, added.
>
>>> +
>>> +\begin{listing}[tbp]
>>> +{ \scriptsize
>>> +\begin{verbbox}[\LstLineNo]
>>> +C C-2+2W+o-o+o-o
>>> +{
>>> +}
>>> +
>>> +{
>>> +#include "api.h"
>>> +}
>>
>> Ditto.
>>
>>> +
>>> +P0(int *x0, int *x1)
>>> +{
>>> + WRITE_ONCE(*x0, 1);
>>> + WRITE_ONCE(*x1, 2);
>>
>> Ditto.
>
> And these.
>
>>> +}
>>> +
>>> +
>>> +P1(int *x0, int *x1)
>>> +{
>>> + WRITE_ONCE(*x1, 1);
>>> + WRITE_ONCE(*x0, 2);
>>> +}
>>> +
>>> +exists (x0=1 /\ x1=1)
>>> +\end{verbbox}
>>> +}
>>> +\centering
>>> +\theverbbox
>>> +\caption{2+2W Litmus Test Without Write Barriers}
>>> +\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
>>> +\end{listing}%
>>> +%
>>
>> These "%"s have no effect because of the blank line above the
>> "listing" environment. You can remove them if you are OK with
>> the following sentence starting a new paragraph.
>
> OK, I removed them. So we only need the "%"s if we want the figure
> in the middle of a paragraph?
In order to prevent paragraph break, all you need is to avoid blank lines
in LaTeX source.
"%"s are useful when you don't want any "white space" to be recognized
by LaTeX engine, as line breaks in LaTeX source imply white spaces.
A line ending with a "%" (or any comment thereafter) doesn't imply
a white space.
The fixes in commit 90197e37d310 ("Fix layout hiccups in answers to
quick quizzes") used "%"s around "listing" environments at the head or
the tail of Answers to Quick Quizzes. In those cases, any white space
would cause extra indent or horizontal skips around cross-reference
markers.
In contrast, commit 4978c9b76f47 ("appendix/whymb: Fix layout in answers
to quick quizzes") tweaked just blank lines.
So "%" is not necessary in most cases. A line of just "%" can be used
instead of a blank line in LaTeX source when you want a blank line
around some environment without causing paragraph break, though.
Such use cases are present in some of the Answers to Quick Quizzes.
Can you see the difference?
Thanks, Akira
>
> Thanx, Paul
>
>>> + Of course, without the barrier, there are no ordering
>>> + guarantees, even on real weakly ordered hardware, as shown in
>>> + Listing~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
>>> + (\path{C-2+2W+o-o+o-o.litmus}).
>>> +} \QuickQuizEnd
>>> +
>>> +But sometimes time really is on our side. Read on!
>>>
>>> \subsubsection{Happens-Before}
>>> \label{sec:memorder:Happens-Before}
>>>
>>>
>>
>
>
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
2017-11-12 2:27 ` Akira Yokosawa
@ 2017-11-12 17:15 ` Paul E. McKenney
0 siblings, 0 replies; 10+ messages in thread
From: Paul E. McKenney @ 2017-11-12 17:15 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sun, Nov 12, 2017 at 11:27:37AM +0900, Akira Yokosawa wrote:
> On 2017/11/12 10:29, Paul E. McKenney wrote:
> > On Sun, Nov 12, 2017 at 08:26:21AM +0900, Akira Yokosawa wrote:
> >> On 2017/11/11 08:57:23 -0800, Paul E. McKenney wrote:
> >>> On Sat, Nov 11, 2017 at 08:44:38AM -0800, Paul E. McKenney wrote:
> >>>> On Sat, Nov 11, 2017 at 08:56:01AM +0900, Akira Yokosawa wrote:
> >>>>> On 2017/11/11 08:41:54 +0900, Akira Yokosawa wrote:
> >>>>>> >From 6ecff66f2b5f95e914d90e29b6d0a2eb4d8901cc Mon Sep 17 00:00:00 2001
> >>>>>> From: Akira Yokosawa <akiyks@gmail.com>
> >>>>>> Date: Sat, 11 Nov 2017 08:25:34 +0900
> >>>>>> Subject: [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling
> >>>>>>
> >>>>>> Also fix corresponding code snippet.
> >>>>>>
> >>>>>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> >>>>>> ---
> >>>>>> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 2 --
> >>>>>
> >>>>> By the way Paul, didn't you have a plan to mention these "C-2+2W" litmus tests
> >>>>> somewhere in the memorder chapter?
> >>>>
> >>>> Good point, it is an odd corner case that is worth at least a quick quiz.
> >>>> How about the following?
> >>>
> >>> My fingers just keep automatically typing "Figure", so please see a
> >>> corrected patch below. Presumably my fingers will get with the program
> >>> in a few months. ;-)
> >>
> >> ;-) ;-)
> >>
> >> Please see inline (nitpicking) comments below.
> >>
> >> Thanks, Akira
> >>
> >>>
> >>> Thanx, Paul
> >>>
> >>> ------------------------------------------------------------------------
> >>>
> >>> commit ac730edc868b6c8a9a71637fd205553e7ba88df2
> >>> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> >>> Date: Sat Nov 11 08:41:47 2017 -0800
> >>>
> >>> memorder: Add a quick quiz for the 2+2W litmus tests
> >>>
> >>> Reported-by: Akira Yokosawa <akiyks@gmail.com>
> >>> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> >>>
> >>> diff --git a/memorder/memorder.tex b/memorder/memorder.tex
> >>> index 7d8e4978fa6d..2ef8363fba6a 100644
> >>> --- a/memorder/memorder.tex
> >>> +++ b/memorder/memorder.tex
> >>> @@ -2455,7 +2455,103 @@ same variable is not necessarily the store that started last.
> >>> This should not come as a surprise to anyone who carefully examined
> >>> Figure~\ref{fig:memorder:A Variable With More Simultaneous Values}.
> >>>
> >>> -But sometimes time is on our side, as shown in the next section.
> >>> +\begin{listing}[tbp]
> >>> +{ \scriptsize
> >>> +\begin{verbbox}[\LstLineNo]
> >>> +C C-2+2W+o-wmb-o+o-wmb-o
> >>> +{
> >>> +}
> >>> +
> >>> +{
> >>> +#include "api.h"
> >>> +}
> >>
> >> 2nd parentheses should be removed in code snippets.
> >>
> >>> +
> >>> +P0(int *x0, int *x1)
> >>> +{
> >>> + WRITE_ONCE(*x0, 1);
> >>> + smp_wmb();
> >>> + WRITE_ONCE(*x1, 2);
> >>> +}
> >>
> >> Need to convert "tab" -> " ".
> >
> > Good catches, fixed.
> >
> >>> +
> >>> +
> >>> +P1(int *x0, int *x1)
> >>> +{
> >>> + WRITE_ONCE(*x1, 1);
> >>> + smp_wmb();
> >>> + WRITE_ONCE(*x0, 2);
> >>> +}
> >>> +
> >>> +exists (x0=1 /\ x1=1)
> >>> +\end{verbbox}
> >>> +}
> >>> +\centering
> >>> +\theverbbox
> >>> +\caption{2+2W Litmus Test With Write Barriers}
> >>> +\label{lst:memorder:2+2W Litmus Test With Write Barriers}
> >>> +\end{listing}
> >>> +
> >>> +\QuickQuiz{}
> >>> + But for litmus tests having only ordered stores, as shown in
> >>> + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}
> >>> + (\path{C-2+2W+o-wmb-o+o-wmb-o.litmus}),
> >>> + research shows that the cycle is prohibited, even in weakly
> >>> + ordered systems such as ARM and Power~\cite{test6-pdf}.
> >>> + Given that, are store-to-store really \emph{always}
> >>> + counter-temporal???
> >>> +\QuickQuizAnswer{
> >>> + This litmus test is indeed a very interesting curiosity.
> >>> + Its ordering apparently occurs naturally given typical
> >>> + weakly ordered hardware design, which would normally be
> >>> + considered a great gift from the relevant laws of physics
> >>> + and cache-coherency-protocol mathematics.
> >>> +
> >>> + Unfortunately, no one has been able to come up with a software use
> >>> + case for this gift that does not have a much better alternative
> >>> + implementation.
> >>> + Therefore, neither the C11 nor the Linux kernel memory models
> >>> + provide any guarantee corresponding to
> >>> + Listing~\ref{lst:memorder:2+2W Litmus Test With Write Barriers}.
> >>
> >> And the exists clause triggers by herd7 verification. (Redundant???)
> >
> > Good point, added.
> >
> >>> +
> >>> +\begin{listing}[tbp]
> >>> +{ \scriptsize
> >>> +\begin{verbbox}[\LstLineNo]
> >>> +C C-2+2W+o-o+o-o
> >>> +{
> >>> +}
> >>> +
> >>> +{
> >>> +#include "api.h"
> >>> +}
> >>
> >> Ditto.
> >>
> >>> +
> >>> +P0(int *x0, int *x1)
> >>> +{
> >>> + WRITE_ONCE(*x0, 1);
> >>> + WRITE_ONCE(*x1, 2);
> >>
> >> Ditto.
> >
> > And these.
> >
> >>> +}
> >>> +
> >>> +
> >>> +P1(int *x0, int *x1)
> >>> +{
> >>> + WRITE_ONCE(*x1, 1);
> >>> + WRITE_ONCE(*x0, 2);
> >>> +}
> >>> +
> >>> +exists (x0=1 /\ x1=1)
> >>> +\end{verbbox}
> >>> +}
> >>> +\centering
> >>> +\theverbbox
> >>> +\caption{2+2W Litmus Test Without Write Barriers}
> >>> +\label{lst:memorder:2+2W Litmus Test Without Write Barriers}
> >>> +\end{listing}%
> >>> +%
> >>
> >> These "%"s have no effect because of the blank line above the
> >> "listing" environment. You can remove them if you are OK with
> >> the following sentence starting a new paragraph.
> >
> > OK, I removed them. So we only need the "%"s if we want the figure
> > in the middle of a paragraph?
>
> In order to prevent paragraph break, all you need is to avoid blank lines
> in LaTeX source.
>
> "%"s are useful when you don't want any "white space" to be recognized
> by LaTeX engine, as line breaks in LaTeX source imply white spaces.
> A line ending with a "%" (or any comment thereafter) doesn't imply
> a white space.
>
> The fixes in commit 90197e37d310 ("Fix layout hiccups in answers to
> quick quizzes") used "%"s around "listing" environments at the head or
> the tail of Answers to Quick Quizzes. In those cases, any white space
> would cause extra indent or horizontal skips around cross-reference
> markers.
>
> In contrast, commit 4978c9b76f47 ("appendix/whymb: Fix layout in answers
> to quick quizzes") tweaked just blank lines.
>
> So "%" is not necessary in most cases. A line of just "%" can be used
> instead of a blank line in LaTeX source when you want a blank line
> around some environment without causing paragraph break, though.
> Such use cases are present in some of the Answers to Quick Quizzes.
>
> Can you see the difference?
Had I put the listing at the end of the QQ, it would have been good
to use % to prevent LaTeX from making a new paragraph for the
end-of-quick-quiz market, but given that it was instead in the middle
of the quick quiz, no need.
So I got it! For the moment, anyway. ;-)
Thanx, Paul
> Thanks, Akira
>
> >
> > Thanx, Paul
> >
> >>> + Of course, without the barrier, there are no ordering
> >>> + guarantees, even on real weakly ordered hardware, as shown in
> >>> + Listing~\ref{lst:memorder:2+2W Litmus Test Without Write Barriers}
> >>> + (\path{C-2+2W+o-o+o-o.litmus}).
> >>> +} \QuickQuizEnd
> >>> +
> >>> +But sometimes time really is on our side. Read on!
> >>>
> >>> \subsubsection{Happens-Before}
> >>> \label{sec:memorder:Happens-Before}
> >>>
> >>>
> >>
> >
> >
>
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2017-11-12 17:15 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-11-10 23:39 [PATCH 1/3] CodeSamples/formal: Separate litmus7 compatible litmus tests Akira Yokosawa
2017-11-10 23:40 ` [PATCH 2/3] CodeSamples/formal: Remove 2nd parentheses in tests under herd/ Akira Yokosawa
2017-11-10 23:41 ` [PATCH 3/3] CodeSamples/formal: Get rid of warnings in cross compiling Akira Yokosawa
2017-11-10 23:56 ` Akira Yokosawa
2017-11-11 16:44 ` Paul E. McKenney
2017-11-11 16:57 ` Paul E. McKenney
2017-11-11 23:26 ` Akira Yokosawa
2017-11-12 1:29 ` Paul E. McKenney
2017-11-12 2:27 ` Akira Yokosawa
2017-11-12 17:15 ` Paul E. McKenney
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.