From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: Akira Yokosawa <akiyks@gmail.com>
Cc: perfbook@vger.kernel.org
Subject: Re: [PATCH v2] advsync: Add litmus tests of control dependency
Date: Tue, 25 Jul 2017 12:44:17 -0700 [thread overview]
Message-ID: <20170725194417.GY3730@linux.vnet.ibm.com> (raw)
In-Reply-To: <89bbe5d8-39e1-1019-bfc8-175a71d1005c@gmail.com>
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
>
>
prev parent reply other threads:[~2017-07-25 19:44 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
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 message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20170725194417.GY3730@linux.vnet.ibm.com \
--to=paulmck@linux.vnet.ibm.com \
--cc=akiyks@gmail.com \
--cc=perfbook@vger.kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox