* [PATCH] advsync: Fix litmus tests
@ 2017-08-26 0:07 Akira Yokosawa
2017-08-26 1:59 ` Paul E. McKenney
0 siblings, 1 reply; 4+ messages in thread
From: Akira Yokosawa @ 2017-08-26 0:07 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
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@gmail.com>
---
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
^ permalink raw reply related [flat|nested] 4+ messages in thread
* Re: [PATCH] advsync: Fix litmus tests
2017-08-26 0:07 [PATCH] advsync: Fix litmus tests Akira Yokosawa
@ 2017-08-26 1:59 ` Paul E. McKenney
2017-08-26 2:47 ` Akira Yokosawa
0 siblings, 1 reply; 4+ messages in thread
From: Paul E. McKenney @ 2017-08-26 1:59 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Aug 26, 2017 at 09:07:33AM +0900, Akira Yokosawa wrote:
> >From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> 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@gmail.com>
> ---
> 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?
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
> 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
>
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [PATCH] advsync: Fix litmus tests
2017-08-26 1:59 ` Paul E. McKenney
@ 2017-08-26 2:47 ` Akira Yokosawa
2017-08-26 4:35 ` Paul E. McKenney
0 siblings, 1 reply; 4+ messages in thread
From: Akira Yokosawa @ 2017-08-26 2:47 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
On 2017/08/25 18:59:44 -0700, Paul E. McKenney wrote:
> On Sat, Aug 26, 2017 at 09:07:33AM +0900, Akira Yokosawa wrote:
>> >From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> 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@gmail.com>
>> ---
>> 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?
>
> 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
>
> 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
>
>> 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(-)
>>
[...]
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [PATCH] advsync: Fix litmus tests
2017-08-26 2:47 ` Akira Yokosawa
@ 2017-08-26 4:35 ` Paul E. McKenney
0 siblings, 0 replies; 4+ messages in thread
From: Paul E. McKenney @ 2017-08-26 4:35 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Aug 26, 2017 at 11:47:29AM +0900, Akira Yokosawa wrote:
> On 2017/08/25 18:59:44 -0700, Paul E. McKenney wrote:
> > On Sat, Aug 26, 2017 at 09:07:33AM +0900, Akira Yokosawa wrote:
> >> >From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@gmail.com>
> >> 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@gmail.com>
> >> ---
> >> 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?
> >
> > 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.
Good catch, I converted the tabs to spaces.
Thanx, Paul
> Thanks, Akira
>
> >
> > 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
> >
> >> 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(-)
> >>
> [...]
>
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2017-08-26 4:35 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-08-26 0:07 [PATCH] advsync: Fix litmus tests Akira Yokosawa
2017-08-26 1:59 ` Paul E. McKenney
2017-08-26 2:47 ` Akira Yokosawa
2017-08-26 4:35 ` 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.