* [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 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.