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@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?
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
>
--
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
