advsync: Fix litmus tests

Quoted 1 line

From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Sat, 26 Aug 2017 08:48:01 +0900
Subject: [PATCH] advsync: Fix litmus tests

Adjust litmus-test syntax to be accepted by litmus7.

Signed-off-by Akira Yokosawa <[email protected]>

---
Hi Paul,

This is my attempt to make litmus7 happy. herd7 says:

--

$ herd7 -conf strong.cfg C-WWC+o+o-data-o+o-addr-o.litmus 
Test C-WWC+o+o-data-o+o-addr-o Allowed
States 5
1:r1=x; 2:r2=u; x=x;
1:r1=x; 2:r2=x; x=a;
1:r1=x; 2:r2=x; x=x;
1:r1=z; 2:r2=u; x=x;
1:r1=z; 2:r2=z; x=x;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
Observation C-WWC+o+o-data-o+o-addr-o Sometimes 1 4
Hash=262fd275af47e8ed4fba69491478bb7d
--

and

--

$ herd7 -conf strong.cfg C-WWC+o+o-r+o-addr-o.litmus 
Test C-WWC+o+o-r-o+o-addr-o Allowed
States 4
1:r1=x; 2:r2=u; x=x;
1:r1=x; 2:r2=x; x=a;
1:r1=z; 2:r2=u; x=x;
1:r1=z; 2:r2=z; x=x;
No
Witnesses
Positive: 0 Negative: 4
Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
Observation C-WWC+o+o-r-o+o-addr-o Never 0 4
Hash=607040ae8eb633fee308b55be24729e1
--

Do these look reasonable?

Thanks, Akira
--

 .../advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus  | 22 ++++++++++---
 .../advsync/herd/C-WWC+o+o-r+o-addr-o.litmus       | 24 ++++++++++----
 advsync/memorybarriers.tex                         | 38 +++++++++++++++-------
 3 files changed, 62 insertions(+), 22 deletions(-)

CodeSamples/advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus +17 -5

index e49712f..3e51168 100644
@@ -1,23 +1,35 @@
 C C-WWC+o+o-data-o+o-addr-o
 
 {
-x=z;
-b=a;
+int z = 0;
+int *x = &z;
+int u = 0;
+int *y = &u;
+int b = 0;
+int *a = &b;
 }
 
-void P0(int **x)
+{
+#include "api.h"
+}
+
+P0(int **x)
 {
 	WRITE_ONCE(*x, x);
 }
 
-void P1(int **x, int **y)
+P1(int **x, int **y)
 {
+	int *r1;
+
 	r1 = READ_ONCE(*x);
 	WRITE_ONCE(*y, r1);
 }
 
-void P2(int **x, int **y)
+P2(int **y, int **a)
 {
+	int *r2;
+
 	r2 = READ_ONCE(*y);
 	WRITE_ONCE(*r2, a);
 }

CodeSamples/advsync/herd/C-WWC+o+o-r+o-addr-o.litmus +18 -6

index 5439868..7f47f7a 100644
@@ -1,23 +1,35 @@
-C C-WWC+o+o-data-o+o-addr-o
+C C-WWC+o+o-r-o+o-addr-o
 
 {
-x=z;
-b=a;
+int z = 0;
+int *x = &z;
+int u = 0;
+int *y = &u;
+int b = 0;
+int *a = &b;
 }
 
-void P0(int **x)
+{
+#include "api.h"
+}
+
+P0(int **x)
 {
 	WRITE_ONCE(*x, x);
 }
 
-void P1(int **x, int **y)
+P1(int **x, int **y)
 {
+	int *r1;
+
 	r1 = READ_ONCE(*x);
 	smp_store_release(y, r1);
 }
 
-void P2(int **x, int **y)
+P2(int **y, int **a)
 {
+	int *r2;
+
 	r2 = READ_ONCE(*y);
 	WRITE_ONCE(*r2, a);
 }

advsync/memorybarriers.tex +27 -11

index fbcd22a..51236c8 100644
@@ -1311,23 +1311,31 @@ does need to deal with them.
 C C-WWC+o+o-data-o+o-addr-o
 
 {
-x=z;
-b=a;
+int z = 0;
+int *x = &z;
+int u = 0;
+int *y = &u;
+int b = 0;
+int *a = &b;
 }
 
-void P0(int **x)
+P0(int **x)
 {
   WRITE_ONCE(*x, x);
 }
 
-void P1(int **x, int **y)
+P1(int **x, int **y)
 {
+  int *r1;
+
   r1 = READ_ONCE(*x);
   WRITE_ONCE(*y, r1);
 }
 
-void P2(int **x, int **y)
+P2(int **y, int **a)
 {
+  int *r2;
+
   r2 = READ_ONCE(*y);
   WRITE_ONCE(*r2, a);
 }

@@ -1344,26 +1352,34 @@ exists(1:r1=x /\ 2:r2=x /\ x=x)
 \begin{listing}[tbp]
 { \scriptsize
 \begin{verbbox}[\LstLineNo]
-C C-WWC+o+o-data-o+o-addr-o
+C C-WWC+o+o-r-o+o-addr-o
 
 {
-x=z;
-b=a;
+int z = 0;
+int *x = &z;
+int u = 0;
+int *y = &u;
+int b = 0;
+int *a = &b;
 }
 
-void P0(int **x)
+P0(int **x)
 {
   WRITE_ONCE(*x, x);
 }
 
-void P1(int **x, int **y)
+P1(int **x, int **y)
 {
+  int *r1;
+
   r1 = READ_ONCE(*x);
   smp_store_release(y, r1);
 }
 
-void P2(int **x, int **y)
+P2(int **y, int **a)
 {
+  int *r2;
+
   r2 = READ_ONCE(*y);
   WRITE_ONCE(*r2, a);
 }

Signature · 1 line

2.7.4

Quoted 49 lines · Akira Yokosawa

Quoted 1 line

From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Sat, 26 Aug 2017 08:48:01 +0900
Subject: [PATCH] advsync: Fix litmus tests

Adjust litmus-test syntax to be accepted by litmus7.

Signed-off-by Akira Yokosawa <[email protected]>

---
Hi Paul,

This is my attempt to make litmus7 happy. herd7 says:

--

$ herd7 -conf strong.cfg C-WWC+o+o-data-o+o-addr-o.litmus 
Test C-WWC+o+o-data-o+o-addr-o Allowed
States 5
1:r1=x; 2:r2=u; x=x;
1:r1=x; 2:r2=x; x=a;
1:r1=x; 2:r2=x; x=x;
1:r1=z; 2:r2=u; x=x;
1:r1=z; 2:r2=z; x=x;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
Observation C-WWC+o+o-data-o+o-addr-o Sometimes 1 4
Hash=262fd275af47e8ed4fba69491478bb7d
--

and

--

$ herd7 -conf strong.cfg C-WWC+o+o-r+o-addr-o.litmus 
Test C-WWC+o+o-r-o+o-addr-o Allowed
States 4
1:r1=x; 2:r2=u; x=x;
1:r1=x; 2:r2=x; x=a;
1:r1=z; 2:r2=u; x=x;
1:r1=z; 2:r2=z; x=x;
No
Witnesses
Positive: 0 Negative: 4
Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
Observation C-WWC+o+o-r-o+o-addr-o Never 0 4
Hash=607040ae8eb633fee308b55be24729e1
--

Quoted 1 line

Do these look reasonable?

They do, but I failed to push out a change, and thus had to hand-apply them with some adjustment. Could you please double-check them? For ease of repairing any errors, I split this into two commits.

Also, I made the memory-barriers section be its own chapter. At some point I should move the litmus tests as well, but am holding off until we get these corrected.

Thanx, Paul

Quoted 7 lines

Thanks, Akira
--

 .../advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus  | 22 ++++++++++---
 .../advsync/herd/C-WWC+o+o-r+o-addr-o.litmus       | 24 ++++++++++----
 advsync/memorybarriers.tex                         | 38 +++++++++++++++-------
 3 files changed, 62 insertions(+), 22 deletions(-)

Quoted 52 lines · Paul E. McKenney

Quoted 50 lines · Akira Yokosawa

Quoted 1 line

From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Sat, 26 Aug 2017 08:48:01 +0900
Subject: [PATCH] advsync: Fix litmus tests

Adjust litmus-test syntax to be accepted by litmus7.

Signed-off-by Akira Yokosawa <[email protected]>

---
Hi Paul,

This is my attempt to make litmus7 happy. herd7 says:

--

$ herd7 -conf strong.cfg C-WWC+o+o-data-o+o-addr-o.litmus 
Test C-WWC+o+o-data-o+o-addr-o Allowed
States 5
1:r1=x; 2:r2=u; x=x;
1:r1=x; 2:r2=x; x=a;
1:r1=x; 2:r2=x; x=x;
1:r1=z; 2:r2=u; x=x;
1:r1=z; 2:r2=z; x=x;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
Observation C-WWC+o+o-data-o+o-addr-o Sometimes 1 4
Hash=262fd275af47e8ed4fba69491478bb7d
--

and

--

$ herd7 -conf strong.cfg C-WWC+o+o-r+o-addr-o.litmus 
Test C-WWC+o+o-r-o+o-addr-o Allowed
States 4
1:r1=x; 2:r2=u; x=x;
1:r1=x; 2:r2=x; x=a;
1:r1=z; 2:r2=u; x=x;
1:r1=z; 2:r2=z; x=x;
No
Witnesses
Positive: 0 Negative: 4
Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
Observation C-WWC+o+o-r-o+o-addr-o Never 0 4
Hash=607040ae8eb633fee308b55be24729e1
--

Do these look reasonable?

Quoted 3 lines

They do, but I failed to push out a change, and thus had to hand-apply them with some adjustment. Could you please double-check them? For ease of repairing any errors, I split this into two commits.

Litmus tests as listings in memorder.tex have indentations of tabs. For consistency, they should be 2 white spaces.

Other than that, the change looks OK to me.

Thanks, Akira

Quoted 14 lines

Also, I made the memory-barriers section be its own chapter. At some point I should move the litmus tests as well, but am holding off until we get these corrected.

Thanx, Paul

Quoted 7 lines

Thanks, Akira
--

 .../advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus  | 22 ++++++++++---
 .../advsync/herd/C-WWC+o+o-r+o-addr-o.litmus       | 24 ++++++++++----
 advsync/memorybarriers.tex                         | 38 +++++++++++++++-------
 3 files changed, 62 insertions(+), 22 deletions(-)

[...]