>From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
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 <akiyks@xxxxxxxxx>
---
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(-)
diff --git a/CodeSamples/advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus b/CodeSamples/advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus
index e49712f..3e51168 100644
--- a/CodeSamples/advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus
+++ b/CodeSamples/advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus
@@ -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);
}
diff --git a/CodeSamples/advsync/herd/C-WWC+o+o-r+o-addr-o.litmus b/CodeSamples/advsync/herd/C-WWC+o+o-r+o-addr-o.litmus
index 5439868..7f47f7a 100644
--- a/CodeSamples/advsync/herd/C-WWC+o+o-r+o-addr-o.litmus
+++ b/CodeSamples/advsync/herd/C-WWC+o+o-r+o-addr-o.litmus
@@ -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);
}
diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index fbcd22a..51236c8 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -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);
}
--
2.7.4
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
