Re: [RFC PATCH] advsync: Add litmus tests of control dependency

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

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
>