* [RFC PATCH] advsync: Add litmus tests of control dependency
@ 2017-07-17 14:28 Akira Yokosawa
2017-07-19 17:44 ` Paul E. McKenney
0 siblings, 1 reply; 4+ messages in thread
From: Akira Yokosawa @ 2017-07-17 14:28 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 892d8e1014c5bca1c83fbc35bcc1951c6c497b7f Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Mon, 17 Jul 2017 20:56:19 +0900
Subject: [RFC PATCH] advsync: Add litmus tests of control dependency
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
Hi Paul,
So I converted the 2 examples of control dependency to litmus tests.
I mentioned the name "C-SB+o-c-o+o-c-o", but it should have been
"C-LB+o-c-o+o-c-o".
They correspond to the example after the partial revert to the
two-CPU example I submitted earlier.
Do they make sense?
Thanks, Akira
--
CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus | 27 ++++++++++++++++++
.../advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus | 32 ++++++++++++++++++++++
2 files changed, 59 insertions(+)
create mode 100644 CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
create mode 100644 CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
diff --git a/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus b/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
new file mode 100644
index 0000000..023af2e
--- /dev/null
+++ b/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
@@ -0,0 +1,27 @@
+C C-LB+o-c-o+o-c-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/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
new file mode 100644
index 0000000..80dc2f6
--- /dev/null
+++ b/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
@@ -0,0 +1,32 @@
+C C-WWC+o-c-o+o-c-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)
--
2.7.4
^ permalink raw reply related [flat|nested] 4+ messages in thread
* Re: [RFC PATCH] advsync: Add litmus tests of control dependency
2017-07-17 14:28 [RFC PATCH] advsync: Add litmus tests of control dependency Akira Yokosawa
@ 2017-07-19 17:44 ` Paul E. McKenney
2017-07-23 4:16 ` [PATCH v2] " Akira Yokosawa
0 siblings, 1 reply; 4+ messages in thread
From: Paul E. McKenney @ 2017-07-19 17:44 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Mon, Jul 17, 2017 at 11:28:09PM +0900, Akira Yokosawa wrote:
> >From 892d8e1014c5bca1c83fbc35bcc1951c6c497b7f Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Mon, 17 Jul 2017 20:56:19 +0900
> Subject: [RFC PATCH] advsync: Add litmus tests of control dependency
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Hello, Akira,
If you make these have the ">" condition, I would be very happy to
apply the resulting patch.
Thanx, Paul
> ---
> Hi Paul,
>
> So I converted the 2 examples of control dependency to litmus tests.
> I mentioned the name "C-SB+o-c-o+o-c-o", but it should have been
> "C-LB+o-c-o+o-c-o".
>
> They correspond to the example after the partial revert to the
> two-CPU example I submitted earlier.
>
> Do they make sense?
>
> Thanks, Akira
> --
> CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus | 27 ++++++++++++++++++
> .../advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus | 32 ++++++++++++++++++++++
> 2 files changed, 59 insertions(+)
> create mode 100644 CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
> create mode 100644 CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
>
> diff --git a/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus b/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
> new file mode 100644
> index 0000000..023af2e
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
> @@ -0,0 +1,27 @@
> +C C-LB+o-c-o+o-c-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/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
> new file mode 100644
> index 0000000..80dc2f6
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
> @@ -0,0 +1,32 @@
> +C C-WWC+o-c-o+o-c-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)
> --
> 2.7.4
>
^ permalink raw reply [flat|nested] 4+ messages in thread
* [PATCH v2] advsync: Add litmus tests of control dependency
2017-07-19 17:44 ` Paul E. McKenney
@ 2017-07-23 4:16 ` Akira Yokosawa
2017-07-25 19:44 ` Paul E. McKenney
0 siblings, 1 reply; 4+ messages in thread
From: Akira Yokosawa @ 2017-07-23 4:16 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 4b73c3ec0a875ac5f1bc58afa1a5db49014b4ad3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 23 Jul 2017 09:11:03 +0900
Subject: [PATCH v2] advsync: Add litmus tests of control dependency
C-LB+o-cgt-o+o-cgt-o and C-WWC+o-cgt-o+o-cgt-o+o correspond to
2-CPU and 3-CPU examples found in the discussion of lack of
transitivity in control dependency.
The 2-CPU example (with ">" in the "if" statements) behaves
differently from other LB (Load Buffering) litmus tests.
To get the expected behavior of an LB litmus test, we need to use
the ">=" operator (C-LB+o-cge-o+o-cge-o).
However, the "if" statements in this test are always true.
Optimizing compilers can prove it fairly easily from
the initial values and assigned-to values of "x" and "y" (0 and 1).
To prevent the "if" statements from being optimized out,
C-LB+o-cge-o+o-cge-o+dstb adds another thread which has
never-executed assignments of -1 to "x" and "y".
C-WWC+o-cge-o+o-cge-o+o is a ">=" version of 3-CPU example.
C-WWC+o-cge-o+o-cge-o+o+dstb has the extra thread mentioned above.
On PPC, C-WWC+o-cge-o+o-cge-o+o+dstb sometimes demonstrates
the lack of transitivity.
In the hope we can see the same with the ">" version,
C-WWC+o-cgt-o+o-cgt-o+o-dstb has the same extra thread.
And on PPC, it does occasionally show the lack of transitivity
while C-WWC+o-cgt-o+o-cgt-o+o does not.
Examples of litmus7 results on PPC demonstrating the lack of
transitivity:
-----------
Test C-WWC+o-cge-o+o-cge-o+o+dstb Allowed
Histogram (10 states)
848181:>0:r1=0; 1:r2=0; x=1;
15701449:>0:r1=1; 1:r2=0; x=1;
7523103:>0:r1=2; 1:r2=0; x=1;
20215797:>0:r1=0; 1:r2=1; x=1;
11079459:>0:r1=2; 1:r2=1; x=1;
4122418:>0:r1=0; 1:r2=0; x=2;
14473329:>0:r1=1; 1:r2=0; x=2;
15258139:>0:r1=2; 1:r2=0; x=2;
10778124:>0:r1=0; 1:r2=1; x=2;
1 *>0:r1=2; 1:r2=1; x=2;
Ok
Witnesses
Positive: 1, Negative: 99999999
Condition exists (0:r1=2 /\ 1:r2=1 /\ x=2) is validated
Hash=08acbed570bea87fa17496409e3b6fb4
Observation C-WWC+o-cge-o+o-cge-o+o+dstb Sometimes 1 99999999
Time C-WWC+o-cge-o+o-cge-o+o+dstb 98.11
-----------
Test C-WWC+o-cgt-o+o-cgt-o+o+dstb Allowed
Histogram (4 states)
10507061:>0:r1=2; 1:r2=1; x=1;
50351171:>0:r1=0; 1:r2=0; x=2;
39141767:>0:r1=2; 1:r2=0; x=2;
1 *>0:r1=2; 1:r2=1; x=2;
Ok
Witnesses
Positive: 1, Negative: 99999999
Condition exists (0:r1=2 /\ 1:r2=1 /\ x=2) is validated
Hash=a23a617c655d9e373993764f59634ed9
Observation C-WWC+o-cgt-o+o-cgt-o+o+dstb Sometimes 1 99999999
Time C-WWC+o-cgt-o+o-cgt-o+o+dstb 94.83
-----------
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
v1 (RFC) -> v2:
o Add ">" versions of test as C-LB+o-cgt-o+o-cgt-o.litmus and
C-WWC+o-cgt-o+o-cgt-o+o.litmus.
o Rename ">=" versions of test C-LB+o-cge-o+o-cge-o.litmus and
C-WWC+o-cge-o+o-cge-o+o.litmus.
o Add ">=" tests with an extra thread to make it hard for compilers
to optimize out "if" statements (C-LB+o-cge-o+o-cge-o+dstb and
C-WWC+o-cge-o+o-cge-o+o+dstb).
o Add ">" version of WWC test with the same extra thread
(C-WWC+o-cgt-o+o-cgt-o+o+dstb). In this case it is not necessary
to restrict optimizations, but it increases the probability
the lack of transitivity is demonstrated.
--
.../advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus | 41 +++++++++++++++++++
.../advsync/herd/C-LB+o-cge-o+o-cge-o.litmus | 27 +++++++++++++
.../advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus | 27 +++++++++++++
.../herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 46 ++++++++++++++++++++++
.../advsync/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 ++++++++++++++++++++++
.../advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 32 +++++++++++++++
7 files changed, 251 insertions(+)
create mode 100644 CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
create mode 100644 CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o.litmus
create mode 100644 CodeSamples/advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus
create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
diff --git a/CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus b/CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
new file mode 100644
index 0000000..e97b879
--- /dev/null
+++ b/CodeSamples/advsync/herd/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/advsync/herd/C-LB+o-cge-o+o-cge-o.litmus b/CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o.litmus
new file mode 100644
index 0000000..14539b9
--- /dev/null
+++ b/CodeSamples/advsync/herd/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/advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus b/CodeSamples/advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus
new file mode 100644
index 0000000..d442f76
--- /dev/null
+++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus b/CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
new file mode 100644
index 0000000..015bcd0
--- /dev/null
+++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cge-o+o-cge-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
new file mode 100644
index 0000000..3fcd502
--- /dev/null
+++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus b/CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
new file mode 100644
index 0000000..989d99f
--- /dev/null
+++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
new file mode 100644
index 0000000..bfe5449
--- /dev/null
+++ b/CodeSamples/advsync/herd/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)
--
2.7.4
^ permalink raw reply related [flat|nested] 4+ messages in thread
* Re: [PATCH v2] advsync: Add litmus tests of control dependency
2017-07-23 4:16 ` [PATCH v2] " Akira Yokosawa
@ 2017-07-25 19:44 ` Paul E. McKenney
0 siblings, 0 replies; 4+ messages in thread
From: Paul E. McKenney @ 2017-07-25 19:44 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sun, Jul 23, 2017 at 01:16:39PM +0900, Akira Yokosawa wrote:
> >From 4b73c3ec0a875ac5f1bc58afa1a5db49014b4ad3 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Sun, 23 Jul 2017 09:11:03 +0900
> Subject: [PATCH v2] advsync: Add litmus tests of control dependency
>
> C-LB+o-cgt-o+o-cgt-o and C-WWC+o-cgt-o+o-cgt-o+o correspond to
> 2-CPU and 3-CPU examples found in the discussion of lack of
> transitivity in control dependency.
>
> The 2-CPU example (with ">" in the "if" statements) behaves
> differently from other LB (Load Buffering) litmus tests.
> To get the expected behavior of an LB litmus test, we need to use
> the ">=" operator (C-LB+o-cge-o+o-cge-o).
> However, the "if" statements in this test are always true.
> Optimizing compilers can prove it fairly easily from
> the initial values and assigned-to values of "x" and "y" (0 and 1).
>
> To prevent the "if" statements from being optimized out,
> C-LB+o-cge-o+o-cge-o+dstb adds another thread which has
> never-executed assignments of -1 to "x" and "y".
>
> C-WWC+o-cge-o+o-cge-o+o is a ">=" version of 3-CPU example.
> C-WWC+o-cge-o+o-cge-o+o+dstb has the extra thread mentioned above.
>
> On PPC, C-WWC+o-cge-o+o-cge-o+o+dstb sometimes demonstrates
> the lack of transitivity.
>
> In the hope we can see the same with the ">" version,
> C-WWC+o-cgt-o+o-cgt-o+o-dstb has the same extra thread.
>
> And on PPC, it does occasionally show the lack of transitivity
> while C-WWC+o-cgt-o+o-cgt-o+o does not.
I am not sure that we want all of these long-term, but I queued and
pushed this anyway just to make it easier for people to play with them.
If some of the prove to be unnecessary later on, there is always
"git rm". ;-)
Thanx, Paul
> Examples of litmus7 results on PPC demonstrating the lack of
> transitivity:
>
> -----------
> Test C-WWC+o-cge-o+o-cge-o+o+dstb Allowed
> Histogram (10 states)
> 848181:>0:r1=0; 1:r2=0; x=1;
> 15701449:>0:r1=1; 1:r2=0; x=1;
> 7523103:>0:r1=2; 1:r2=0; x=1;
> 20215797:>0:r1=0; 1:r2=1; x=1;
> 11079459:>0:r1=2; 1:r2=1; x=1;
> 4122418:>0:r1=0; 1:r2=0; x=2;
> 14473329:>0:r1=1; 1:r2=0; x=2;
> 15258139:>0:r1=2; 1:r2=0; x=2;
> 10778124:>0:r1=0; 1:r2=1; x=2;
> 1 *>0:r1=2; 1:r2=1; x=2;
> Ok
>
> Witnesses
> Positive: 1, Negative: 99999999
> Condition exists (0:r1=2 /\ 1:r2=1 /\ x=2) is validated
> Hash=08acbed570bea87fa17496409e3b6fb4
> Observation C-WWC+o-cge-o+o-cge-o+o+dstb Sometimes 1 99999999
> Time C-WWC+o-cge-o+o-cge-o+o+dstb 98.11
> -----------
> Test C-WWC+o-cgt-o+o-cgt-o+o+dstb Allowed
> Histogram (4 states)
> 10507061:>0:r1=2; 1:r2=1; x=1;
> 50351171:>0:r1=0; 1:r2=0; x=2;
> 39141767:>0:r1=2; 1:r2=0; x=2;
> 1 *>0:r1=2; 1:r2=1; x=2;
> Ok
>
> Witnesses
> Positive: 1, Negative: 99999999
> Condition exists (0:r1=2 /\ 1:r2=1 /\ x=2) is validated
> Hash=a23a617c655d9e373993764f59634ed9
> Observation C-WWC+o-cgt-o+o-cgt-o+o+dstb Sometimes 1 99999999
> Time C-WWC+o-cgt-o+o-cgt-o+o+dstb 94.83
> -----------
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
> ---
> v1 (RFC) -> v2:
> o Add ">" versions of test as C-LB+o-cgt-o+o-cgt-o.litmus and
> C-WWC+o-cgt-o+o-cgt-o+o.litmus.
> o Rename ">=" versions of test C-LB+o-cge-o+o-cge-o.litmus and
> C-WWC+o-cge-o+o-cge-o+o.litmus.
> o Add ">=" tests with an extra thread to make it hard for compilers
> to optimize out "if" statements (C-LB+o-cge-o+o-cge-o+dstb and
> C-WWC+o-cge-o+o-cge-o+o+dstb).
> o Add ">" version of WWC test with the same extra thread
> (C-WWC+o-cgt-o+o-cgt-o+o+dstb). In this case it is not necessary
> to restrict optimizations, but it increases the probability
> the lack of transitivity is demonstrated.
> --
> .../advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus | 41 +++++++++++++++++++
> .../advsync/herd/C-LB+o-cge-o+o-cge-o.litmus | 27 +++++++++++++
> .../advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus | 27 +++++++++++++
> .../herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 46 ++++++++++++++++++++++
> .../advsync/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 ++++++++++++++++++++++
> .../advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 32 +++++++++++++++
> 7 files changed, 251 insertions(+)
> create mode 100644 CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
> create mode 100644 CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o.litmus
> create mode 100644 CodeSamples/advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus
> create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
> create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
> create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
> create mode 100644 CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
>
> diff --git a/CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus b/CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o+dstb.litmus
> new file mode 100644
> index 0000000..e97b879
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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/advsync/herd/C-LB+o-cge-o+o-cge-o.litmus b/CodeSamples/advsync/herd/C-LB+o-cge-o+o-cge-o.litmus
> new file mode 100644
> index 0000000..14539b9
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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/advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus b/CodeSamples/advsync/herd/C-LB+o-cgt-o+o-cgt-o.litmus
> new file mode 100644
> index 0000000..d442f76
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus b/CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
> new file mode 100644
> index 0000000..015bcd0
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cge-o+o-cge-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-cge-o+o-cge-o+o.litmus
> new file mode 100644
> index 0000000..3fcd502
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus b/CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
> new file mode 100644
> index 0000000..989d99f
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-cgt-o+o-cgt-o+o.litmus
> new file mode 100644
> index 0000000..bfe5449
> --- /dev/null
> +++ b/CodeSamples/advsync/herd/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)
> --
> 2.7.4
>
>
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2017-07-25 19:44 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-07-17 14:28 [RFC PATCH] advsync: Add litmus tests of control dependency Akira Yokosawa
2017-07-19 17:44 ` Paul E. McKenney
2017-07-23 4:16 ` [PATCH v2] " Akira Yokosawa
2017-07-25 19:44 ` Paul E. McKenney
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox