Litmus test for question from Al Viro

Litmus test for question from Al Viro

[Paul E. McKenney]

Hello!

Al Viro posted the following query:

------------------------------------------------------------------------

<viro> fun question regarding barriers, if you have time for that
<viro>         V->A = V->B = 1;
<viro>
<viro> CPU1:
<viro>         to_free = NULL
<viro>         spin_lock(&LOCK)
<viro>         if (!smp_load_acquire(&V->B))
<viro>                 to_free = V
<viro>         V->A = 0
<viro>         spin_unlock(&LOCK)
<viro>         kfree(to_free)
<viro>
<viro> CPU2:
<viro>         to_free = V;
<viro>         if (READ_ONCE(V->A)) {
<viro>                 spin_lock(&LOCK)
<viro>                 if (V->A)
<viro>                         to_free = NULL
<viro>                 smp_store_release(&V->B, 0);
<viro>                 spin_unlock(&LOCK)
<viro>         }
<viro>         kfree(to_free);
<viro> 1) is it guaranteed that V will be freed exactly once and that
	  no accesses to *V will happen after freeing it?
<viro> 2) do we need smp_store_release() there?  I.e. will anything
	  break if it's replaced with plain V->B = 0?

------------------------------------------------------------------------

Of course herd7 supports neither structures nor arrays, but I was
crazy enough to try individual variables with made-up address and data
dependencies.  This litmus test must also detect use-after-free bugs,
but a simple variable should be able to do that.  So here is a
prototype:

------------------------------------------------------------------------

C C-viro-2020.09.29a

{
	int a = 1;
	int b = 1;
	int v = 1;
}


P0(int *a, int *b, int *v, spinlock_t *l)
{
	int r0;
	int r1;
	int r2 = 2;
	int r8;
	int r9a = 2;
	int r9b = 2;

	r0 = 0;
	spin_lock(l);
	r9a = READ_ONCE(*v); // Use after free?
	r8 = r9a - r9a; // Restore address dependency
	r8 = b + r8;
	r1 = smp_load_acquire(r8);
	if (r1 == 0)
		r0 = 1;
	r9b = READ_ONCE(*v); // Use after free?
	WRITE_ONCE(*a, r9b - r9b); // Use data dependency
	spin_unlock(l);
	if (r0) {
		r2 = READ_ONCE(*v);
		WRITE_ONCE(*v, 0); /* kfree(). */
	}
}

P1(int *a, int *b, int *v, spinlock_t *l)
{
	int r0;
	int r1;
	int r1a;
	int r2 = 2;
	int r8;
	int r9a = 2;
	int r9b = 2;
	int r9c = 2;

	r0 = READ_ONCE(*v);
	r9a = r0; // Use after free?
	r8 = r9a - r9a; // Restore address dependency
	r8 = a + r8;
	r1 = READ_ONCE(*r8);
	if (r1) {
		spin_lock(l);
		r9b = READ_ONCE(*v); // Use after free?
		r8 = r9b - r9b; // Restore address dependency
		r8 = a + r8;
		r1a = READ_ONCE(*r8);
		if (r1a)
			r0 = 0;
		r9c = READ_ONCE(*v); // Use after free?
		smp_store_release(b, r9c - rc9); // Use data dependency
		spin_unlock(l);
	}
	if (r0) {
		r2 = READ_ONCE(*v);
		WRITE_ONCE(*v, 0); /* kfree(). */
	}
}

locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
	v=1 \/ (* Neither did kfree, redundant check. *)
	0:r2=0 \/ 1:r2=0 \/  (* Both did kfree, redundant check. *)
	0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
	1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)

------------------------------------------------------------------------

This "exists" clause is satisfied:

------------------------------------------------------------------------

$ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
Test C-viro-2020.09.29a Allowed
States 5
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
Ok
Witnesses
Positive: 3 Negative: 2
Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
Observation C-viro-2020.09.29a Sometimes 3 2
Time C-viro-2020.09.29a 14.33
Hash=89f74abff4de682ee0bea8ee6dd53134

------------------------------------------------------------------------

So did we end up with herd7 not respecting "fake" dependencies like
those shown above, or have I just messed up the translation from Al's
example to the litmus test?  (Given one thing and another over the past
couple of days, my guess would be that I just messed up the translation,
especially given that I don't see a reference to fake dependencies in
the documentation, but I figured that I should ask.)

							Thanx, Paul

Re: Litmus test for question from Al Viro

[Alan Stern]

On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> Hello!
> 
> Al Viro posted the following query:
> 
> ------------------------------------------------------------------------
> 
> <viro> fun question regarding barriers, if you have time for that
> <viro>         V->A = V->B = 1;
> <viro>
> <viro> CPU1:
> <viro>         to_free = NULL
> <viro>         spin_lock(&LOCK)
> <viro>         if (!smp_load_acquire(&V->B))
> <viro>                 to_free = V
> <viro>         V->A = 0
> <viro>         spin_unlock(&LOCK)
> <viro>         kfree(to_free)
> <viro>
> <viro> CPU2:
> <viro>         to_free = V;
> <viro>         if (READ_ONCE(V->A)) {
> <viro>                 spin_lock(&LOCK)
> <viro>                 if (V->A)
> <viro>                         to_free = NULL
> <viro>                 smp_store_release(&V->B, 0);
> <viro>                 spin_unlock(&LOCK)
> <viro>         }
> <viro>         kfree(to_free);
> <viro> 1) is it guaranteed that V will be freed exactly once and that
> 	  no accesses to *V will happen after freeing it?
> <viro> 2) do we need smp_store_release() there?  I.e. will anything
> 	  break if it's replaced with plain V->B = 0?

Here are my answers to Al's questions:

1) It is guaranteed that V will be freed exactly once.  It is not 
guaranteed that no accesses to *V will occur after it is freed, because 
the test contains a data race.  CPU1's plain "V->A = 0" write races with 
CPU2's READ_ONCE; if the plain write were replaced with 
"WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well, 
CPU1's smp_load_acquire could be replaced with a plain read while the 
plain write is replaced with smp_store_release.

2) The smp_store_release in CPU2 is not needed.  Replacing it with a 
plain V->B = 0 will not break anything.

Analysis: Apart from the kfree calls themselves, the only access to a 
shared variable outside of a critical section is CPU2's READ_ONCE of 
V->A.  So let's consider two possibilities:

1: The READ_ONCE returns 0.  Then CPU2 doesn't execute its critical 
section and does kfree(V).  However, the fact that the READ_ONCE got 0 
means that CPU1 has already entered its critical section, has already 
written to V->A (but with a plain write!) and therefore has already seen 
V->B = 1 (because of the smp_load_acquire), and therefore will not free 
V.  This case shows that the ordering we require is for CPU1 to read 
V->B before it writes V->A.  The ordering can be enforced by using 
either a load-acquire (as in the litmus test) or a store-release.

2: The READ_ONCE returns 1.  Then CPU2 does execute its critical 
section, and we can simply treat this case the same as if the critical 
section was executed unconditionally.  Whichever CPU runs its critical 
section second will free V, and the other CPU won't try to access V 
after leaving its own critical section (and thus won't access V after it 
has been freed).

> ------------------------------------------------------------------------
> 
> Of course herd7 supports neither structures nor arrays, but I was
> crazy enough to try individual variables with made-up address and data
> dependencies.  This litmus test must also detect use-after-free bugs,
> but a simple variable should be able to do that.  So here is a
> prototype:
> 
> ------------------------------------------------------------------------
> 
> C C-viro-2020.09.29a
> 
> {
> 	int a = 1;
> 	int b = 1;
> 	int v = 1;
> }

Not the way I would have done it, but okay.  I would have modeled the 
kfree by setting a and b both to some sentinel value.

> P0(int *a, int *b, int *v, spinlock_t *l)
> {
> 	int r0;
> 	int r1;
> 	int r2 = 2;
> 	int r8;
> 	int r9a = 2;
> 	int r9b = 2;
> 
> 	r0 = 0;
> 	spin_lock(l);
> 	r9a = READ_ONCE(*v); // Use after free?
> 	r8 = r9a - r9a; // Restore address dependency
> 	r8 = b + r8;
> 	r1 = smp_load_acquire(r8);
> 	if (r1 == 0)
> 		r0 = 1;
> 	r9b = READ_ONCE(*v); // Use after free?
> 	WRITE_ONCE(*a, r9b - r9b); // Use data dependency
> 	spin_unlock(l);
> 	if (r0) {
> 		r2 = READ_ONCE(*v);
> 		WRITE_ONCE(*v, 0); /* kfree(). */
> 	}
> }
> 
> P1(int *a, int *b, int *v, spinlock_t *l)
> {
> 	int r0;
> 	int r1;
> 	int r1a;
> 	int r2 = 2;
> 	int r8;
> 	int r9a = 2;
> 	int r9b = 2;
> 	int r9c = 2;
> 
> 	r0 = READ_ONCE(*v);
> 	r9a = r0; // Use after free?

Wrong.  This should be:

	r0 = 1;
	r9a = READ_ONCE(*v);

> 	r8 = r9a - r9a; // Restore address dependency
> 	r8 = a + r8;
> 	r1 = READ_ONCE(*r8);
> 	if (r1) {
> 		spin_lock(l);
> 		r9b = READ_ONCE(*v); // Use after free?
> 		r8 = r9b - r9b; // Restore address dependency
> 		r8 = a + r8;
> 		r1a = READ_ONCE(*r8);
> 		if (r1a)
> 			r0 = 0;
> 		r9c = READ_ONCE(*v); // Use after free?
> 		smp_store_release(b, r9c - rc9); // Use data dependency
> 		spin_unlock(l);
> 	}
> 	if (r0) {
> 		r2 = READ_ONCE(*v);
> 		WRITE_ONCE(*v, 0); /* kfree(). */
> 	}
> }
> 
> locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
> exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
> 	v=1 \/ (* Neither did kfree, redundant check. *)
> 	0:r2=0 \/ 1:r2=0 \/  (* Both did kfree, redundant check. *)
> 	0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
> 	1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)
> 
> ------------------------------------------------------------------------
> 
> This "exists" clause is satisfied:
> 
> ------------------------------------------------------------------------
> 
> $ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
> Test C-viro-2020.09.29a Allowed
> States 5
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;

The values for this case don't make sense.  I haven't checked the other 
four cases.  Printing a graph of the relations for this case (the only 
state with v=1 at the end) might help.

> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
> Ok
> Witnesses
> Positive: 3 Negative: 2
> Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
> Observation C-viro-2020.09.29a Sometimes 3 2
> Time C-viro-2020.09.29a 14.33
> Hash=89f74abff4de682ee0bea8ee6dd53134

Why didn't this flag the data race?

> ------------------------------------------------------------------------
> 
> So did we end up with herd7 not respecting "fake" dependencies like
> those shown above, or have I just messed up the translation from Al's
> example to the litmus test?  (Given one thing and another over the past
> couple of days, my guess would be that I just messed up the translation,
> especially given that I don't see a reference to fake dependencies in
> the documentation, but I figured that I should ask.)

What do you get if you fix up the litmus test?

Alan

Re: Litmus test for question from Al Viro

[Al Viro]

On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> > <viro> CPU1:
> > <viro>         to_free = NULL
> > <viro>         spin_lock(&LOCK)
> > <viro>         if (!smp_load_acquire(&V->B))
> > <viro>                 to_free = V
> > <viro>         V->A = 0
> > <viro>         spin_unlock(&LOCK)
> > <viro>         kfree(to_free)
> > <viro>
> > <viro> CPU2:
> > <viro>         to_free = V;
> > <viro>         if (READ_ONCE(V->A)) {
> > <viro>                 spin_lock(&LOCK)
> > <viro>                 if (V->A)
> > <viro>                         to_free = NULL
> > <viro>                 smp_store_release(&V->B, 0);
> > <viro>                 spin_unlock(&LOCK)
> > <viro>         }
> > <viro>         kfree(to_free);
> > <viro> 1) is it guaranteed that V will be freed exactly once and that
> > 	  no accesses to *V will happen after freeing it?
> > <viro> 2) do we need smp_store_release() there?  I.e. will anything
> > 	  break if it's replaced with plain V->B = 0?
> 
> Here are my answers to Al's questions:
> 
> 1) It is guaranteed that V will be freed exactly once.  It is not 
> guaranteed that no accesses to *V will occur after it is freed, because 
> the test contains a data race.  CPU1's plain "V->A = 0" write races with 
> CPU2's READ_ONCE;

What will that READ_ONCE() yield in that case?  If it's non-zero, we should
be fine - we won't get to kfree() until after we are done with the spinlock.
And if it's zero...  What will CPU1 do with *V accesses _after_ it has issued
the store to V->A?

Confused...

> if the plain write were replaced with 
> "WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well, 
> CPU1's smp_load_acquire could be replaced with a plain read while the 
> plain write is replaced with smp_store_release.

Er...  Do you mean the write to ->A on CPU1?

Re: Litmus test for question from Al Viro

[Alan Stern]

On Thu, Oct 01, 2020 at 05:36:46PM +0100, Al Viro wrote:
> On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> > > <viro> CPU1:
> > > <viro>         to_free = NULL
> > > <viro>         spin_lock(&LOCK)
> > > <viro>         if (!smp_load_acquire(&V->B))
> > > <viro>                 to_free = V
> > > <viro>         V->A = 0
> > > <viro>         spin_unlock(&LOCK)
> > > <viro>         kfree(to_free)
> > > <viro>
> > > <viro> CPU2:
> > > <viro>         to_free = V;
> > > <viro>         if (READ_ONCE(V->A)) {
> > > <viro>                 spin_lock(&LOCK)
> > > <viro>                 if (V->A)
> > > <viro>                         to_free = NULL
> > > <viro>                 smp_store_release(&V->B, 0);
> > > <viro>                 spin_unlock(&LOCK)
> > > <viro>         }
> > > <viro>         kfree(to_free);
> > > <viro> 1) is it guaranteed that V will be freed exactly once and that
> > > 	  no accesses to *V will happen after freeing it?
> > > <viro> 2) do we need smp_store_release() there?  I.e. will anything
> > > 	  break if it's replaced with plain V->B = 0?
> > 
> > Here are my answers to Al's questions:
> > 
> > 1) It is guaranteed that V will be freed exactly once.  It is not 
> > guaranteed that no accesses to *V will occur after it is freed, because 
> > the test contains a data race.  CPU1's plain "V->A = 0" write races with 
> > CPU2's READ_ONCE;
> 
> What will that READ_ONCE() yield in that case?  If it's non-zero, we should
> be fine - we won't get to kfree() until after we are done with the spinlock.
> And if it's zero...  What will CPU1 do with *V accesses _after_ it has issued
> the store to V->A?
> 
> Confused...

Presumably CPU2's READ_ONCE will yield either 0 or 1.  For the sake of 
argument, suppose it yields 0.  But that's not the problem.

The problem with a plain write is that it isn't guaranteed to be atomic 
in any sense.  In principle, the compiler could generate code for CPU1 
which would write 0 to V->A more than once.

Although I strongly doubt that any real compiler would actually do this, 
the memory model does allow for it, out of an overabundance of caution.  
So what could happen is:

	CPU1				CPU2
	Writes 0 to V->A a first time
					READ_ONCE(V->A) returns 0
					Skips the critical section
					Does kfree(V)
	Tries to write 0 to V->A a
	 second time

> > if the plain write were replaced with 
> > "WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well, 
> > CPU1's smp_load_acquire could be replaced with a plain read while the 
> > plain write is replaced with smp_store_release.
> 
> Er...  Do you mean the write to ->A on CPU1?

Yes; that's the only plain write in the litmus test.

Alan

Re: Litmus test for question from Al Viro

[Al Viro]

On Thu, Oct 01, 2020 at 02:39:25PM -0400, Alan Stern wrote:

> The problem with a plain write is that it isn't guaranteed to be atomic 
> in any sense.  In principle, the compiler could generate code for CPU1 
> which would write 0 to V->A more than once.
> 
> Although I strongly doubt that any real compiler would actually do this, 
> the memory model does allow for it, out of an overabundance of caution.  

Point...  OK, not a problem - actually there will be WRITE_ONCE() for other
reasons; the real-life (pseudo-)code is
        spin_lock(&file->f_lock);
        to_free = NULL;
        head = file->f_ep;
        if (head->first == &epitem->fllink && epitem->fllink.next == NULL) {
		/* the set will go empty */
                file->f_ep = NULL;
                if (!is_file_epoll(file)) {
			/*
			 * not embedded into struct eventpoll; we want it
			 * freed unless it's on the check list, in which
			 * case we leave it for reverse path check to free.
			 */
                        v = container_of(head, struct ep_head, epitems);
                        if (!smp_load_acquire(&v->next))
                                to_free = v;
                }
        }
        hlist_del_rcu(&epitem->fllink);
        spin_unlock(file->f_lock);
        kfree(to_free);
and hlist_del_rcu() will use WRITE_ONCE() to store the updated forward links.

That goes into ep_remove() and CPU1 side of that thing is the final (set-emptying)
call.  CPU2 side is the list traversal step in reverse_path_check() and
in clear_tfile_check_list():
	// under rcu_read_lock()
        to_free = head;
        epitem = rcu_dereference(hlist_first_rcu(&head->epitems));
        if (epitem) {
                spin_lock(&epitem->file->f_lock);
                if (!hlist_empty(&head->epitems))
                        to_free = NULL;
                head->next = NULL;
                spin_unlock(&epitem->file->f_lock);
        }
        kfree(to_free);

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> > Hello!
> > 
> > Al Viro posted the following query:
> > 
> > ------------------------------------------------------------------------
> > 
> > <viro> fun question regarding barriers, if you have time for that
> > <viro>         V->A = V->B = 1;
> > <viro>
> > <viro> CPU1:
> > <viro>         to_free = NULL
> > <viro>         spin_lock(&LOCK)
> > <viro>         if (!smp_load_acquire(&V->B))
> > <viro>                 to_free = V
> > <viro>         V->A = 0
> > <viro>         spin_unlock(&LOCK)
> > <viro>         kfree(to_free)
> > <viro>
> > <viro> CPU2:
> > <viro>         to_free = V;
> > <viro>         if (READ_ONCE(V->A)) {
> > <viro>                 spin_lock(&LOCK)
> > <viro>                 if (V->A)
> > <viro>                         to_free = NULL
> > <viro>                 smp_store_release(&V->B, 0);
> > <viro>                 spin_unlock(&LOCK)
> > <viro>         }
> > <viro>         kfree(to_free);
> > <viro> 1) is it guaranteed that V will be freed exactly once and that
> > 	  no accesses to *V will happen after freeing it?
> > <viro> 2) do we need smp_store_release() there?  I.e. will anything
> > 	  break if it's replaced with plain V->B = 0?
> 
> Here are my answers to Al's questions:
> 
> 1) It is guaranteed that V will be freed exactly once.  It is not 
> guaranteed that no accesses to *V will occur after it is freed, because 
> the test contains a data race.  CPU1's plain "V->A = 0" write races with 
> CPU2's READ_ONCE; if the plain write were replaced with 
> "WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well, 
> CPU1's smp_load_acquire could be replaced with a plain read while the 
> plain write is replaced with smp_store_release.
> 
> 2) The smp_store_release in CPU2 is not needed.  Replacing it with a 
> plain V->B = 0 will not break anything.
> 
> Analysis: Apart from the kfree calls themselves, the only access to a 
> shared variable outside of a critical section is CPU2's READ_ONCE of 
> V->A.  So let's consider two possibilities:
> 
> 1: The READ_ONCE returns 0.  Then CPU2 doesn't execute its critical 
> section and does kfree(V).  However, the fact that the READ_ONCE got 0 
> means that CPU1 has already entered its critical section, has already 
> written to V->A (but with a plain write!) and therefore has already seen 
> V->B = 1 (because of the smp_load_acquire), and therefore will not free 
> V.  This case shows that the ordering we require is for CPU1 to read 
> V->B before it writes V->A.  The ordering can be enforced by using 
> either a load-acquire (as in the litmus test) or a store-release.
> 
> 2: The READ_ONCE returns 1.  Then CPU2 does execute its critical 
> section, and we can simply treat this case the same as if the critical 
> section was executed unconditionally.  Whichever CPU runs its critical 
> section second will free V, and the other CPU won't try to access V 
> after leaving its own critical section (and thus won't access V after it 
> has been freed).
> 
> > ------------------------------------------------------------------------
> > 
> > Of course herd7 supports neither structures nor arrays, but I was
> > crazy enough to try individual variables with made-up address and data
> > dependencies.  This litmus test must also detect use-after-free bugs,
> > but a simple variable should be able to do that.  So here is a
> > prototype:
> > 
> > ------------------------------------------------------------------------
> > 
> > C C-viro-2020.09.29a
> > 
> > {
> > 	int a = 1;
> > 	int b = 1;
> > 	int v = 1;
> > }
> 
> Not the way I would have done it, but okay.  I would have modeled the 
> kfree by setting a and b both to some sentinel value.

Might be well worth pursuing!  But how would you model the address
dependencies in that approach?

> > P0(int *a, int *b, int *v, spinlock_t *l)
> > {
> > 	int r0;
> > 	int r1;
> > 	int r2 = 2;
> > 	int r8;
> > 	int r9a = 2;
> > 	int r9b = 2;
> > 
> > 	r0 = 0;
> > 	spin_lock(l);
> > 	r9a = READ_ONCE(*v); // Use after free?
> > 	r8 = r9a - r9a; // Restore address dependency
> > 	r8 = b + r8;
> > 	r1 = smp_load_acquire(r8);
> > 	if (r1 == 0)
> > 		r0 = 1;
> > 	r9b = READ_ONCE(*v); // Use after free?
> > 	WRITE_ONCE(*a, r9b - r9b); // Use data dependency
> > 	spin_unlock(l);
> > 	if (r0) {
> > 		r2 = READ_ONCE(*v);
> > 		WRITE_ONCE(*v, 0); /* kfree(). */
> > 	}
> > }
> > 
> > P1(int *a, int *b, int *v, spinlock_t *l)
> > {
> > 	int r0;
> > 	int r1;
> > 	int r1a;
> > 	int r2 = 2;
> > 	int r8;
> > 	int r9a = 2;
> > 	int r9b = 2;
> > 	int r9c = 2;
> > 
> > 	r0 = READ_ONCE(*v);
> > 	r9a = r0; // Use after free?
> 
> Wrong.  This should be:
> 
> 	r0 = 1;
> 	r9a = READ_ONCE(*v);

Thank you!  I was definitely suffering from a severe case of Programmer's
Blindness.  Fixed!

> > 	r8 = r9a - r9a; // Restore address dependency
> > 	r8 = a + r8;
> > 	r1 = READ_ONCE(*r8);
> > 	if (r1) {
> > 		spin_lock(l);
> > 		r9b = READ_ONCE(*v); // Use after free?
> > 		r8 = r9b - r9b; // Restore address dependency
> > 		r8 = a + r8;
> > 		r1a = READ_ONCE(*r8);
> > 		if (r1a)
> > 			r0 = 0;
> > 		r9c = READ_ONCE(*v); // Use after free?
> > 		smp_store_release(b, r9c - rc9); // Use data dependency
> > 		spin_unlock(l);
> > 	}
> > 	if (r0) {
> > 		r2 = READ_ONCE(*v);
> > 		WRITE_ONCE(*v, 0); /* kfree(). */
> > 	}
> > }
> > 
> > locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
> > exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
> > 	v=1 \/ (* Neither did kfree, redundant check. *)
> > 	0:r2=0 \/ 1:r2=0 \/  (* Both did kfree, redundant check. *)
> > 	0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
> > 	1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)
> > 
> > ------------------------------------------------------------------------
> > 
> > This "exists" clause is satisfied:
> > 
> > ------------------------------------------------------------------------
> > 
> > $ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
> > Test C-viro-2020.09.29a Allowed
> > States 5
> > 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> > 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> > 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;
> 
> The values for this case don't make sense.  I haven't checked the other 
> four cases.  Printing a graph of the relations for this case (the only 
> state with v=1 at the end) might help.
> 
> > 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> > 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
> > Ok
> > Witnesses
> > Positive: 3 Negative: 2
> > Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
> > Observation C-viro-2020.09.29a Sometimes 3 2
> > Time C-viro-2020.09.29a 14.33
> > Hash=89f74abff4de682ee0bea8ee6dd53134
> 
> Why didn't this flag the data race?

Because I turned Al's simple assignments into *_ONCE() or better.
In doing this, I was following the default KCSAN settings which
(for better or worse) forgive the stores from data races.

> > ------------------------------------------------------------------------
> > 
> > So did we end up with herd7 not respecting "fake" dependencies like
> > those shown above, or have I just messed up the translation from Al's
> > example to the litmus test?  (Given one thing and another over the past
> > couple of days, my guess would be that I just messed up the translation,
> > especially given that I don't see a reference to fake dependencies in
> > the documentation, but I figured that I should ask.)
> 
> What do you get if you fix up the litmus test?

With your suggested change and using simple assignments where Al
indicated them:

------------------------------------------------------------------------

$ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
Test C-viro-2020.09.29a Allowed
States 5
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
Ok
Witnesses
Positive: 3 Negative: 2
Flag data-race
Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
Observation C-viro-2020.09.29a Sometimes 3 2
Time C-viro-2020.09.29a 17.95
Hash=14ded51102b668bc38b790e8c3692227

------------------------------------------------------------------------

So still "Sometimes", but the "Flag data-race" you expected is there.

I posted the updated litmus test below.  Additional or other thoughts?

							Thanx, Paul

------------------------------------------------------------------------

C C-viro-2020.09.29a

{
	int a = 1;
	int b = 1;
	int v = 1;
}


P0(int *a, int *b, int *v, spinlock_t *l)
{
	int r0;
	int r1;
	int r2 = 2;
	int r8;
	int r9a = 2;
	int r9b = 2;

	r0 = 0;
	spin_lock(l);
	r9a = READ_ONCE(*v); // Use after free?
	r8 = r9a - r9a; // Restore address dependency
	r8 = b + r8;
	r1 = smp_load_acquire(r8);
	if (r1 == 0)
		r0 = 1;
	r9b = READ_ONCE(*v); // Use after free?
	// WRITE_ONCE(*a, r9b - r9b); // Use data dependency
	*a = r9b - r9b; // Use data dependency
	spin_unlock(l);
	if (r0) {
		r2 = READ_ONCE(*v);
		WRITE_ONCE(*v, 0); /* kfree(). */
	}
}

P1(int *a, int *b, int *v, spinlock_t *l)
{
	int r0;
	int r1;
	int r1a;
	int r2 = 2;
	int r8;
	int r9a = 2;
	int r9b = 2;
	int r9c = 2;

	r0 = 1;
	r9a = READ_ONCE(*v); // Use after free?
	r8 = r9a - r9a; // Restore address dependency
	r8 = a + r8;
	r1 = READ_ONCE(*r8);
	if (r1) {
		spin_lock(l);
		r9b = READ_ONCE(*v); // Use after free?
		r8 = r9b - r9b; // Restore address dependency
		r8 = a + r8;
		// r1a = READ_ONCE(*r8);
		r1a = *r8;
		if (r1a)
			r0 = 0;
		r9c = READ_ONCE(*v); // Use after free?
		smp_store_release(b, r9c - rc9); // Use data dependency
		spin_unlock(l);
	}
	if (r0) {
		r2 = READ_ONCE(*v);
		WRITE_ONCE(*v, 0); /* kfree(). */
	}
}

locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
	v=1 \/ (* Neither did kfree, redundant check. *)
	0:r2=0 \/ 1:r2=0 \/  (* Both did kfree, redundant check. *)
	0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
	1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)

Re: Litmus test for question from Al Viro

[Alan Stern]

On Thu, Oct 01, 2020 at 02:30:48PM -0700, Paul E. McKenney wrote:
> > Not the way I would have done it, but okay.  I would have modeled the 
> > kfree by setting a and b both to some sentinel value.
> 
> Might be well worth pursuing!  But how would you model the address
> dependencies in that approach?

Al's original test never writes to V.  So the address dependencies don't 
matter.

> > Why didn't this flag the data race?
> 
> Because I turned Al's simple assignments into *_ONCE() or better.
> In doing this, I was following the default KCSAN settings which
> (for better or worse) forgive the stores from data races.

Ah, yes.  I had realized that when reading the litmus test for the first 
time, and then forgot it.

> With your suggested change and using simple assignments where Al
> indicated them:
> 
> ------------------------------------------------------------------------
> 
> $ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/C-viro-2020.09.29a.litmus
> Test C-viro-2020.09.29a Allowed
> States 5
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=0; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=0; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=0; 1:r1=1; 1:r2=2; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=1;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=0; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=2; 1:r9c=2; a=0; b=1; v=0;
> 0:r0=0; 0:r1=1; 0:r2=2; 0:r8=b; 0:r9a=1; 0:r9b=1; 1:r0=1; 1:r1=1; 1:r2=1; 1:r8=a; 1:r9a=1; 1:r9b=1; 1:r9c=1; a=0; b=1; v=0;
> Ok
> Witnesses
> Positive: 3 Negative: 2
> Flag data-race
> Condition exists (0:r0=1:r0 \/ v=1 \/ 0:r2=0 \/ 1:r2=0 \/ 0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ 1:r9b=0 \/ 1:r9c=0)
> Observation C-viro-2020.09.29a Sometimes 3 2
> Time C-viro-2020.09.29a 17.95
> Hash=14ded51102b668bc38b790e8c3692227
> 
> ------------------------------------------------------------------------
> 
> So still "Sometimes", but the "Flag data-race" you expected is there.
> 
> I posted the updated litmus test below.  Additional or other thoughts?

Two problems remaining.  One in the litmus test and one in the memory 
model itself...

> ------------------------------------------------------------------------
> 
> C C-viro-2020.09.29a
> 
> {
> 	int a = 1;
> 	int b = 1;
> 	int v = 1;
> }
> 
> 
> P0(int *a, int *b, int *v, spinlock_t *l)
> {
> 	int r0;
> 	int r1;
> 	int r2 = 2;
> 	int r8;
> 	int r9a = 2;
> 	int r9b = 2;
> 
> 	r0 = 0;
> 	spin_lock(l);
> 	r9a = READ_ONCE(*v); // Use after free?
> 	r8 = r9a - r9a; // Restore address dependency
> 	r8 = b + r8;
> 	r1 = smp_load_acquire(r8);
> 	if (r1 == 0)
> 		r0 = 1;
> 	r9b = READ_ONCE(*v); // Use after free?
> 	// WRITE_ONCE(*a, r9b - r9b); // Use data dependency
> 	*a = r9b - r9b; // Use data dependency
> 	spin_unlock(l);
> 	if (r0) {
> 		r2 = READ_ONCE(*v);
> 		WRITE_ONCE(*v, 0); /* kfree(). */
> 	}
> }
> 
> P1(int *a, int *b, int *v, spinlock_t *l)
> {
> 	int r0;
> 	int r1;
> 	int r1a;
> 	int r2 = 2;
> 	int r8;
> 	int r9a = 2;
> 	int r9b = 2;
> 	int r9c = 2;
> 
> 	r0 = 1;
> 	r9a = READ_ONCE(*v); // Use after free?
> 	r8 = r9a - r9a; // Restore address dependency
> 	r8 = a + r8;
> 	r1 = READ_ONCE(*r8);
> 	if (r1) {
> 		spin_lock(l);
> 		r9b = READ_ONCE(*v); // Use after free?
> 		r8 = r9b - r9b; // Restore address dependency
> 		r8 = a + r8;
> 		// r1a = READ_ONCE(*r8);
> 		r1a = *r8;
> 		if (r1a)
> 			r0 = 0;
> 		r9c = READ_ONCE(*v); // Use after free?
> 		smp_store_release(b, r9c - rc9); // Use data dependency
-------------------------------------------^^^
Typo: this should be r9c.  Too bad herd7 doesn't warn about undeclared 
local variables.

> 		spin_unlock(l);
> 	}
> 	if (r0) {
> 		r2 = READ_ONCE(*v);
> 		WRITE_ONCE(*v, 0); /* kfree(). */
> 	}
> }
> 
> locations [a;b;v;0:r1;0:r8;1:r1;1:r8]
> exists (0:r0=1:r0 \/ (* Both or neither did kfree(). *)
> 	v=1 \/ (* Neither did kfree, redundant check. *)
> 	0:r2=0 \/ 1:r2=0 \/  (* Both did kfree, redundant check. *)
> 	0:r9a=0 \/ 0:r9b=0 \/ 1:r9a=0 \/ (* CPU1 use after free. *)
> 	1:r9b=0 \/ 1:r9c=0) (* CPU2 use after free. *)

When you fix the typo, the test still fails.  But now it all makes 
sense.  The reason for the failure is because of the way we don't model 
control dependencies.

In short, suppose P1 reads 0 for V->A.  Then it does:

	if (READ_ONCE(V->A)) {
		... skipped ...
	}
	WRITE_ONCE(V, 0); /* actually kfree(to_free); */

Because the WRITE_ONCE is beyond the end of the "if" statement, there is 
no control dependency.  Nevertheless, the compiler is not allowed to 
reorder those statements because the conditional code modifies to_free.

Since the memory model thinks there isn't any control dependency, herd7 
generates a potential execution (actually two of them) in which the 
WRITE_ONCE executes before the READ_ONCE.  And of course that messes 
everything up; in one of the executions 0:r9b is 0, and in the other 
both 0:r9a and 0:r9b are 0.

This failure to detect control dependencies properly is perhaps the 
weakest aspect of the memory model.

Alan

Re: Litmus test for question from Al Viro

[Jon Masters]

On 10/1/20 12:15 PM, Alan Stern wrote:
> On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
>> Hello!
>>
>> Al Viro posted the following query:
>>
>> ------------------------------------------------------------------------
>>
>> <viro> fun question regarding barriers, if you have time for that
>> <viro>         V->A = V->B = 1;
>> <viro>
>> <viro> CPU1:
>> <viro>         to_free = NULL
>> <viro>         spin_lock(&LOCK)
>> <viro>         if (!smp_load_acquire(&V->B))
>> <viro>                 to_free = V
>> <viro>         V->A = 0
>> <viro>         spin_unlock(&LOCK)
>> <viro>         kfree(to_free)
>> <viro>
>> <viro> CPU2:
>> <viro>         to_free = V;
>> <viro>         if (READ_ONCE(V->A)) {
>> <viro>                 spin_lock(&LOCK)
>> <viro>                 if (V->A)
>> <viro>                         to_free = NULL
>> <viro>                 smp_store_release(&V->B, 0);
>> <viro>                 spin_unlock(&LOCK)
>> <viro>         }
>> <viro>         kfree(to_free);
>> <viro> 1) is it guaranteed that V will be freed exactly once and that
>> 	  no accesses to *V will happen after freeing it?
>> <viro> 2) do we need smp_store_release() there?  I.e. will anything
>> 	  break if it's replaced with plain V->B = 0?
> 
> Here are my answers to Al's questions:
> 
> 1) It is guaranteed that V will be freed exactly once.  It is not
> guaranteed that no accesses to *V will occur after it is freed, because
> the test contains a data race.  CPU1's plain "V->A = 0" write races with
> CPU2's READ_ONCE; if the plain write were replaced with
> "WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well,
> CPU1's smp_load_acquire could be replaced with a plain read while the
> plain write is replaced with smp_store_release.
> 
> 2) The smp_store_release in CPU2 is not needed.  Replacing it with a
> plain V->B = 0 will not break anything.

This was my interpretation also. I made the mistake of reading this 
right before trying to go to bed the other night and ended up tweeting 
at Paul that I'd regret it if he gave me scary dreams. Thought about it 
and read your write up and it is still exactly how I see it.

Jon.

-- 
Computer Architect

Re: Litmus test for question from Al Viro

[Alan Stern]

To expand on my statement about the LKMM's weakness regarding control 
constructs, here is a litmus test to illustrate the issue.  You might 
want to add this to one of the archives.

Alan

C crypto-control-data
(*
 * LB plus crypto-control-data plus data
 *
 * Expected result: allowed
 *
 * This is an example of OOTA and we would like it to be forbidden.
 * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
 * control-dependent on the preceding READ_ONCE.  But the dependencies are
 * hidden by the form of the conditional control construct, hence the 
 * name "crypto-control-data".  The memory model doesn't recognize them.
 *)

{}

P0(int *x, int *y)
{
	int r1;

	r1 = 1;
	if (READ_ONCE(*x) == 0)
		r1 = 0;
	WRITE_ONCE(*y, r1);
}

P1(int *x, int *y)
{
	WRITE_ONCE(*x, READ_ONCE(*y));
}

exists (0:r1=1)

Re: Litmus test for question from Al Viro

[Akira Yokosawa]

Hi Alan,

Just a minor nit in the litmus test.

On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> To expand on my statement about the LKMM's weakness regarding control 
> constructs, here is a litmus test to illustrate the issue.  You might 
> want to add this to one of the archives.
> 
> Alan
> 
> C crypto-control-data
> (*
>  * LB plus crypto-control-data plus data
>  *
>  * Expected result: allowed
>  *
>  * This is an example of OOTA and we would like it to be forbidden.
>  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
>  * control-dependent on the preceding READ_ONCE.  But the dependencies are
>  * hidden by the form of the conditional control construct, hence the 
>  * name "crypto-control-data".  The memory model doesn't recognize them.
>  *)
> 
> {}
> 
> P0(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = 1;
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	WRITE_ONCE(*y, r1);
> }
> 
> P1(int *x, int *y)
> {
> 	WRITE_ONCE(*x, READ_ONCE(*y));

Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.

When I changed P1 to

P1(int *x, int *y)
{
	int r1;

	r1 = READ_ONCE(*y);
	WRITE_ONCE(*x, r1);
}

and replaced the WRITE_ONCE() in P0 with smp_store_release(),
I got the result of:

-----
Test crypto-control-data Allowed
States 1
0:r1=0;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r1=1)
Observation crypto-control-data Never 0 3
Time crypto-control-data 0.01
Hash=9b9aebbaf945dad8183d2be0ccb88e11
-----

Restoring the WRITE_ONCE() in P0, I got the result of:

-----
Test crypto-control-data Allowed
States 2
0:r1=0;
0:r1=1;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (0:r1=1)
Observation crypto-control-data Sometimes 1 4
Time crypto-control-data 0.01
Hash=843eaa4974cec0efae79ce3cb73a1278
-----

As this is the same as the expected result, I suppose you have missed another
limitation of herd7 + LKMM.

By the way, I think this weakness on control dependency + data dependency
deserves an entry in tools/memory-model/Documentation/litmus-tests.txt.

In the LIMITATIONS section, item #1 mentions some situation where
LKMM may not recognize possible losses of control-dependencies by
compiler optimizations.

What this litmus test demonstrates is a different class of mismatch.

Alan, can you come up with an update in this regard?

        Thanks, Akira

> }
> 
> exists (0:r1=1)
> 

Re: Litmus test for question from Al Viro

[joel]

On Thu, Oct 01, 2020 at 02:30:48PM -0700, Paul E. McKenney wrote:
> On Thu, Oct 01, 2020 at 12:15:29PM -0400, Alan Stern wrote:
> > On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> > > Hello!
> > > 
> > > Al Viro posted the following query:
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > <viro> fun question regarding barriers, if you have time for that
> > > <viro>         V->A = V->B = 1;
> > > <viro>
> > > <viro> CPU1:
> > > <viro>         to_free = NULL
> > > <viro>         spin_lock(&LOCK)
> > > <viro>         if (!smp_load_acquire(&V->B))
> > > <viro>                 to_free = V
> > > <viro>         V->A = 0
> > > <viro>         spin_unlock(&LOCK)
> > > <viro>         kfree(to_free)
> > > <viro>
> > > <viro> CPU2:
> > > <viro>         to_free = V;
> > > <viro>         if (READ_ONCE(V->A)) {
> > > <viro>                 spin_lock(&LOCK)
> > > <viro>                 if (V->A)
> > > <viro>                         to_free = NULL
> > > <viro>                 smp_store_release(&V->B, 0);
> > > <viro>                 spin_unlock(&LOCK)
> > > <viro>         }
> > > <viro>         kfree(to_free);
> > > <viro> 1) is it guaranteed that V will be freed exactly once and that
> > > 	  no accesses to *V will happen after freeing it?
> > > <viro> 2) do we need smp_store_release() there?  I.e. will anything
> > > 	  break if it's replaced with plain V->B = 0?
> > 
> > Here are my answers to Al's questions:
> > 
> > 1) It is guaranteed that V will be freed exactly once.  It is not 
> > guaranteed that no accesses to *V will occur after it is freed, because 
> > the test contains a data race.  CPU1's plain "V->A = 0" write races with 
> > CPU2's READ_ONCE; if the plain write were replaced with 
> > "WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well, 
> > CPU1's smp_load_acquire could be replaced with a plain read while the 
> > plain write is replaced with smp_store_release.
> > 
> > 2) The smp_store_release in CPU2 is not needed.  Replacing it with a 
> > plain V->B = 0 will not break anything.
> > 
> > Analysis: Apart from the kfree calls themselves, the only access to a 
> > shared variable outside of a critical section is CPU2's READ_ONCE of 
> > V->A.  So let's consider two possibilities:
> > 
> > 1: The READ_ONCE returns 0.  Then CPU2 doesn't execute its critical 
> > section and does kfree(V).  However, the fact that the READ_ONCE got 0 
> > means that CPU1 has already entered its critical section, has already 
> > written to V->A (but with a plain write!) and therefore has already seen 
> > V->B = 1 (because of the smp_load_acquire), and therefore will not free 
> > V.  This case shows that the ordering we require is for CPU1 to read 
> > V->B before it writes V->A.  The ordering can be enforced by using 
> > either a load-acquire (as in the litmus test) or a store-release.
> > 
> > 2: The READ_ONCE returns 1.  Then CPU2 does execute its critical 
> > section, and we can simply treat this case the same as if the critical 
> > section was executed unconditionally.  Whichever CPU runs its critical 
> > section second will free V, and the other CPU won't try to access V 
> > after leaving its own critical section (and thus won't access V after it 
> > has been freed).
> > 
> > > ------------------------------------------------------------------------
> > > 
> > > Of course herd7 supports neither structures nor arrays

FWIW, I turned Al's example into a klitmus test which gave me the freedom to
modify it offline and use structures.

The code of the 2 threads look like this (full module enclosed later in the
email). I don't see any issues with the example above on either x86 or arm64
which I luckily have these days. Al or others could also modify the module
with any variations and test as well:

static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {

        struct v_struct *r1; /* to_free */

        r1 = NULL;
        spin_lock(l);
        if (!smp_load_acquire(&v->b))
                r1 = v;
        v->a = 0;
        spin_unlock(l);

  *out_0_r1 = !!r1;
}

static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {

        struct v_struct *r1; /* to_free */

        r1 = v;
        if (READ_ONCE(v->a)) {
                spin_lock(l);
                if (v->a)
                        r1 = NULL;
                smp_store_release(&v->b, 0);
                spin_unlock(l);
        }

  *out_1_r1 = !!r1;
}

Results on both arm64 and x86:

    Histogram (2 states)
    19080852:>0:r1=1; 1:r1=0;
    20919148:>0:r1=0; 1:r1=1;
    No
    
    Witnesses
    Positive: 0, Negative: 40000000
    Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
    Hash=4a8c15603ffb5ab464195ea39ccd6382
    Observation AL+test Never 0 40000000
    Time AL+test 6.24

I guess I could do an alloc and free of v_struct. However, I just checked for
whether the to_free in Al's example could ever be NULL for both threads.

Here is the full test. To run it:
modprobe litmus nruns=200
cat /proc/litmus
rmmod

(The file_operations may need to be replaced trivially with proc_operations
for >5.4 kernels)

---8<-----------------------

diff --git a/Makefile b/Makefile
index 57ef8d1d5c24..493b7583f111 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,7 @@
 VERSION = 5
 PATCHLEVEL = 4
 SUBLEVEL = 68
-EXTRAVERSION =
+EXTRAVERSION = litmus
 NAME = Kleptomaniac Octopus
 
 # *DOCUMENTATION*
diff --git a/drivers/misc/Makefile b/drivers/misc/Makefile
index 9a3dda3a9d06..5af1bc2ab9a1 100644
--- a/drivers/misc/Makefile
+++ b/drivers/misc/Makefile
@@ -3,6 +3,7 @@
 # Makefile for misc devices that really don't fit anywhere else.
 #
 
+obj-m                           += mymodules/
 obj-$(CONFIG_IBM_ASM)		+= ibmasm/
 obj-$(CONFIG_IBMVMC)		+= ibmvmc.o
 obj-$(CONFIG_AD525X_DPOT)	+= ad525x_dpot.o
diff --git a/drivers/misc/mymodules/Makefile b/drivers/misc/mymodules/Makefile
new file mode 100644
index 000000000000..1ebb67fbc9ba
--- /dev/null
+++ b/drivers/misc/mymodules/Makefile
@@ -0,0 +1,8 @@
+ccflags-y += -std=gnu99 -Wno-declaration-after-statement
+obj-m += litmus000.o
+
+all:
+	make -C /lib/modules/$(shell uname -r)/build/ M=$(PWD) modules
+
+clean:
+	make -C /lib/modules/$(shell uname -r)/build/ M=$(PWD) clean
diff --git a/drivers/misc/mymodules/README.txt b/drivers/misc/mymodules/README.txt
new file mode 100644
index 000000000000..2af0ca89349f
--- /dev/null
+++ b/drivers/misc/mymodules/README.txt
@@ -0,0 +1,25 @@
+Kernel modules produced by klitmus7
+
+REQUIREMEMTS
+  - kernel headers for compiling modules.
+  - commands insmod and rmmod for installing and removing kernel modules.
+
+COMPILING
+  Once kernel headers are installed, just type 'make'
+
+RUNNING
+  Run script 'run.sh' as root, e.g. as 'sudo sh run.sh'
+  Some parameters can be passed to the script by adding
+  key=value command line arguments.
+  Main arguments are as follows:
+    * size=<n>   Tests operate on arrays of size <n>.
+    * nruns=<n>  And are repeated <n> times.
+    * stride=<n> Arrays are scanned with stride <n>.
+    * avail=<n>  Number of cores are devoted to tests.
+
+  If <avail> is the special value zero or exceeds <a>, the number of actually online cores,
+  then tests will occupy <a> cores.
+
+  By default the script runs as if called as:
+    sudo sh run.sh size=100000 nruns=10 stride=1 avail=0
+
diff --git a/drivers/misc/mymodules/litmus000.c b/drivers/misc/mymodules/litmus000.c
new file mode 100644
index 000000000000..7702e22c7126
--- /dev/null
+++ b/drivers/misc/mymodules/litmus000.c
@@ -0,0 +1,576 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* This C source is a product of litmus7 and includes source that is        */
+/* governed by the CeCILL-B license.                                        */
+/****************************************************************************/
+
+#include <linux/module.h>
+#include <linux/kernel.h>
+#include <linux/init.h>
+#include <linux/fs.h>
+#include <linux/proc_fs.h>
+#include <linux/seq_file.h>
+#include <linux/kthread.h>
+#include <linux/ktime.h>
+#include <linux/atomic.h>
+#include <linux/sysfs.h>
+#include <linux/sched.h>
+#include <linux/wait.h>
+#include <linux/slab.h>
+#include <linux/random.h>
+
+typedef u64 count_t;
+#define PCTR "llu"
+
+#ifndef WRITE_ONCE
+#define WRITE_ONCE(x,v) ({ ACCESS_ONCE((x)) = (v); })
+#endif
+#ifndef READ_ONCE
+#define READ_ONCE(x) ACCESS_ONCE((x))
+#endif
+
+#ifndef smp_store_release
+#define smp_store_release(p, v)                                         \
+do {                                                                    \
+        smp_mb();                                                       \
+        WRITE_ONCE(*p, v);                                              \
+} while (0)
+#endif
+
+#ifndef smp_load_acquire
+#define smp_load_acquire(p)                                             \
+({                                                                      \
+        typeof(*p) ___p1 = READ_ONCE(*p);                               \
+        smp_mb();                                                       \
+        ___p1;                                                          \
+})
+#endif
+
+#ifndef xchg_acquire
+#define xchg_acquire(x,v) xchg(x,v)
+#endif
+
+#ifndef xchg_release
+#define xchg_release(x,v) xchg(x,v)
+#endif
+
+#ifndef lockless_dereference 
+#define lockless_dereference(p)                                         \
+({                                                                      \
+        typeof(p) ____p1 = READ_ONCE(p);                                \
+        smp_read_barrier_depends();                                     \
+        ____p1;                                                         \
+})
+#endif
+
+#ifndef cond_resched_rcu_qs
+#define cond_resched_rcu_qs cpu_relax
+#endif
+
+/* Some constant divide (not available on ARMv7) */
+
+inline static u64 divBy10(u64 n) {
+ u64 q, r;
+ q = (n >> 1) + (n >> 2);
+ q = q + (q >> 4);
+ q = q + (q >> 8);
+ q = q + (q >> 16);
+ q = q >> 3;
+ r = n - q*10;
+ return q + ((r + 6) >> 4);
+}
+
+inline static u64 divBy1000(u64 n) {
+  u64 q, r, t;
+  t = (n >> 7) + (n >> 8) + (n >> 12);
+  q = (n >> 1) + t + (n >> 15) + (t >> 11) + (t >> 14);
+  q = q >> 9;
+  r = n - q*1000;
+  return q + ((r + 24) >> 10);
+}
+
+static int randmod(unsigned int m) {
+  unsigned int x ;
+  get_random_bytes(&x,sizeof(x));
+  return x % m ;
+}
+
+static void shuffle_array(int *t,int sz) {
+  for  (int k = 0 ; k < sz-1; k++) {
+    int j = k + randmod(sz-k);
+    int tmp = t[k] ;
+    t[k] = t[j];
+    t[j] = tmp;
+  }
+}
+/**************/
+/* Parameters */
+/**************/
+
+static const int nthreads = 2;
+static unsigned int nruns = 10;
+static unsigned int size = 100000;
+static unsigned int stride = 1;
+static unsigned int avail = 0;
+static unsigned int ninst = 0;
+static int affincr = 0;
+
+module_param(nruns,uint,0644);
+module_param(size,uint,0644);
+module_param(stride,uint,0644);
+module_param(avail,uint,0644);
+module_param(ninst,uint,0644);
+module_param(affincr,int,0644);
+
+static char *name = "AL+test";
+module_param(name,charp,0444);
+
+static wait_queue_head_t *wq;
+static atomic_t done = ATOMIC_INIT(0);
+
+/************/
+/* Outcomes */
+/************/
+
+#define NOUTS 2
+typedef u64 outcome_t[NOUTS];
+
+static const int out_0_r1_f = 0 ;
+static const int out_1_r1_f = 1 ;
+
+typedef struct outs_t {
+  struct outs_t *next,*down ;
+  count_t c ;
+  u64 k ;
+  int show ;
+} outs_t ;
+
+
+static outs_t *alloc_outs(u64 k) {
+  outs_t *r = kmalloc(sizeof(*r),GFP_KERNEL) ;
+  if (r == NULL) return NULL ;
+  r->k = k ;
+  r->c = 0 ;
+  r->show = 0 ;
+  r->next = r->down = NULL ;
+  return r ;
+}
+
+static void free_outs(outs_t *p) {
+  if (p == NULL) return ;
+  free_outs(p->next) ;
+  free_outs(p->down) ;
+  kfree(p) ;
+}
+
+static outs_t *
+loop_add_outcome_outs(outs_t *p, u64 *k, int i, count_t c, int show) {
+  outs_t *r = p ;
+  if (p == NULL || k[i] < p->k) {
+    r = alloc_outs(k[i]) ;
+    if (r == NULL) return p ; /* simply ignore insert */
+    r->next = p ;
+    p = r ;
+  }
+  for ( ; ; ) {
+    outs_t **q ;
+    if (k[i] > p->k) {
+      q = &(p->next) ;
+      p = p->next ;
+    } else if (i <= 0) {
+      p->c += c ;
+      p->show = show || p->show ;
+      return r ;
+    } else {
+      i-- ;
+      q = &(p->down) ;
+      p = p->down ;
+    }
+    if (p == NULL || k[i] < p->k) {
+      outs_t *a = alloc_outs(k[i]) ;
+      if (a == NULL) return r ;
+      a->next = p ;
+      p = a ;
+      *q = a ;
+    }
+  }
+}
+
+typedef count_t cfun(outs_t *) ;
+
+static count_t count_scan(cfun *f,outs_t *p) {
+  count_t r = 0 ;
+  for ( ; p ; p = p->next) {
+    r += f(p) ;
+    if (p->down) {
+      r += count_scan(f,p->down) ;
+    }
+  }
+  return r ;
+} 
+
+static count_t cshow(outs_t *p) {
+  if (p->show) return p->c ;
+  return 0 ;
+}
+
+static count_t count_show(outs_t *p) { return count_scan(cshow,p) ; }
+
+static count_t cnoshow(outs_t *p) {
+  if (!p->show) return p->c ;
+  return 0 ;
+}
+
+static count_t count_noshow(outs_t *p) { return count_scan(cnoshow,p); }
+
+static count_t cnstates(outs_t *p) {
+  if (p->c > 0) return 1 ;
+  return 0 ;
+}
+
+static count_t count_nstates(outs_t *p) { return count_scan(cnstates,p); }
+
+
+static outs_t *add_outcome_outs(outs_t *p,u64 *k,int show) {
+  return loop_add_outcome_outs(p,k,NOUTS-1,1,show);
+}
+
+static void do_dump_outs (struct seq_file *m,outs_t *p,u64 *o,int sz) {
+  for ( ; p ; p = p->next) {
+    o[sz-1] = p->k;
+    if (p->c > 0) {
+      seq_printf(m,"%-8"PCTR"%c>0:r1=%i; 1:r1=%i;\n",p->c,p->show ? '*' : ':',(int)o[out_0_r1_f],(int)o[out_1_r1_f]);
+    } else {
+      do_dump_outs(m,p->down,o,sz-1);
+    }
+  }
+}
+
+static void dump_outs(struct seq_file *m,outs_t *p) {
+  outcome_t buff;
+  do_dump_outs(m,p,buff,NOUTS);
+}
+
+static inline void barrier_wait(int id,int i,int *b) {
+  if ((i % nthreads) == id) {
+    WRITE_ONCE(*b,1);
+    smp_mb();
+  } else {
+    int _spin = 256;
+    for  ( ; ; ) {
+      if (READ_ONCE(*b) != 0) return;
+      if (--_spin <= 0) return;
+      cpu_relax();
+    }
+  }
+}
+
+
+/****************/
+/* Affinity     */
+/****************/
+
+static int *online;
+static int nonline;
+
+/****************/
+/* Test Context */
+/****************/
+
+struct v_struct {
+  int a;
+  int b;
+};
+
+typedef struct {
+/* Shared locations */
+  struct v_struct *v;
+  spinlock_t *l;
+/* Final contents of observed registers */
+  int *out_0_r1;
+  int *out_1_r1;
+/* For synchronisation */
+  int *barrier;
+} ctx_t ;
+
+static ctx_t **ctx;
+
+static void free_ctx(ctx_t *p) { 
+  if (p == NULL) return;
+  if (p->v) kfree(p->v);
+  if (p->l) kfree(p->l);
+  if (p->out_0_r1) kfree(p->out_0_r1);
+  if (p->out_1_r1) kfree(p->out_1_r1);
+  if (p->barrier) kfree(p->barrier);
+  kfree(p);
+}
+
+static ctx_t *alloc_ctx(size_t sz) { 
+  ctx_t *r = kzalloc(sizeof(*r),GFP_KERNEL);
+  if (!r) { return NULL; }
+  r->v = kmalloc(sizeof(r->v[0])*sz,GFP_KERNEL);
+  if (!r->v) { return NULL; }
+  r->l = kmalloc(sizeof(r->l[0])*sz,GFP_KERNEL);
+  if (!r->l) { return NULL; }
+  for (int _i=0 ; _i < sz ; _i++) spin_lock_init(&r->l[_i]);
+  r->out_0_r1 = kmalloc(sizeof(r->out_0_r1[0])*sz,GFP_KERNEL);
+  if (!r->out_0_r1) { return NULL; }
+  r->out_1_r1 = kmalloc(sizeof(r->out_1_r1[0])*sz,GFP_KERNEL);
+  if (!r->out_1_r1) { return NULL; }
+  r->barrier = kmalloc(sizeof(r->barrier[0])*sz,GFP_KERNEL);
+  if (!r->barrier) { return NULL; }
+  return r;
+}
+
+static void init_ctx(ctx_t *_a,size_t sz) {
+  for (int _i = 0 ; _i < sz ; _i++) {
+    _a->v[_i].a = 1;
+    _a->v[_i].b = 1;
+    _a->out_0_r1[_i] = -239487;
+    _a->out_1_r1[_i] = -239487;
+    _a->barrier[_i] = 0;
+  }
+}
+
+/***************/
+/* Litmus code */
+/***************/
+
+static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {
+
+	struct v_struct *r1; /* to_free */
+
+	r1 = NULL;
+	spin_lock(l);
+	if (!smp_load_acquire(&v->b))
+		r1 = v;
+	v->a = 0;
+	spin_unlock(l);
+
+  *out_0_r1 = !!r1;
+}
+
+static int thread0(void *_p) {
+  ctx_t *_a = (ctx_t *)_p;
+
+  smp_mb();
+  for (int _j = 0 ; _j < stride ; _j++) {
+    for (int _i = _j ; _i < size ; _i += stride) {
+      barrier_wait(0,_i,&_a->barrier[_i]);
+      code0(&_a->v[_i],&_a->l[_i],&_a->out_0_r1[_i]);
+    }
+  }
+  atomic_inc(&done);
+  smp_mb();
+  wake_up(wq);
+  smp_mb();
+  do_exit(0);
+}
+
+static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {
+
+	struct v_struct *r1; /* to_free */
+
+	r1 = v;
+	if (READ_ONCE(v->a)) {
+		spin_lock(l);
+		if (v->a)
+			r1 = NULL;
+                smp_store_release(&v->b, 0);
+		spin_unlock(l);
+	}
+
+  *out_1_r1 = !!r1;
+}
+
+static int thread1(void *_p) {
+  ctx_t *_a = (ctx_t *)_p;
+
+  smp_mb();
+  for (int _j = 0 ; _j < stride ; _j++) {
+    for (int _i = _j ; _i < size ; _i += stride) {
+      barrier_wait(1,_i,&_a->barrier[_i]);
+      code1(&_a->v[_i],&_a->l[_i],&_a->out_1_r1[_i]);
+    }
+  }
+  atomic_inc(&done);
+  smp_mb();
+  wake_up(wq);
+  smp_mb();
+  do_exit(0);
+}
+
+inline static int final_cond(int _out_0_r1,int _out_1_r1) {
+  switch (_out_0_r1) {
+  case 1:
+    switch (_out_1_r1) {
+    case 1:
+      return 1;
+    default:
+      return 0;
+    }
+  default:
+    return 0;
+  }
+}
+
+/********/
+/* Zyva */
+/********/
+
+static outs_t *zyva(void) {
+  ctx_t **c = ctx;
+  outs_t *outs = NULL;
+  const int nth = ninst * nthreads;
+  struct task_struct **th;
+
+  th = kzalloc(sizeof(struct task_struct *) * nth, GFP_KERNEL);
+  if (!th) return NULL;
+  for (int _k = 0 ; _k < nruns ; _k++) {
+    int _nth = 0;
+
+    for (int _ni = 0 ; _ni < ninst ; _ni++) init_ctx(c[_ni],size);
+    atomic_set(&done,0);
+    smp_mb();
+    for (int _ni = 0 ; _ni < ninst ; _ni++) {
+      th[_nth] = kthread_create(thread0,c[_ni],"thread0");
+      if (IS_ERR(th[_nth])) {kfree(th); return outs;}
+      _nth++;
+      th[_nth] = kthread_create(thread1,c[_ni],"thread1");
+      if (IS_ERR(th[_nth])) {kfree(th); return outs;}
+      _nth++;
+    }
+    if (affincr != 0) {
+      int _idx=0, _idx0=0, _incr=affincr > 0 ? affincr : 1;
+      if (affincr < 0) shuffle_array(online,nonline);
+      for (int _t = 0 ; _t < nth ; _t++) {
+        kthread_bind(th[_t],online[_idx]);
+        _idx += _incr; 
+        if (_idx >= nonline) _idx = ++_idx0;
+        if (_idx >= nonline) _idx = _idx0 = 0;
+      }
+    }
+    for (int _t = 0 ; _t < nth ; _t++) wake_up_process(th[_t]);
+    wait_event_interruptible(*wq, atomic_read(&done) == nth);
+    smp_mb();
+    for (int _ni = 0 ; _ni < ninst ; _ni++) {
+      ctx_t *_a = c[_ni];
+      for (int _i = 0 ; _i < size ; _i++) {
+        outcome_t _o;
+        int _cond;
+        _cond = final_cond(_a->out_0_r1[_i],_a->out_1_r1[_i]);
+        _o[out_0_r1_f] = _a->out_0_r1[_i];
+        _o[out_1_r1_f] = _a->out_1_r1[_i];
+        outs = add_outcome_outs(outs,_o,_cond);
+      }
+    }
+    cond_resched();
+  }
+  kfree(th);
+  return outs;
+}
+
+static int do_it(struct seq_file *m) {
+  ktime_t time_start = ktime_get();
+  outs_t *outs = zyva();
+  ktime_t time_end = ktime_get();
+  seq_printf(m,"Test AL+test Allowed\n");
+  seq_printf(m,"Histogram (%"PCTR" states)\n",count_nstates(outs));
+  dump_outs(m,outs);
+  {
+    count_t pos=count_show(outs),neg=count_noshow(outs);
+    char *msg = "Sometimes";
+    u64 delta =  ktime_to_ms(ktime_sub(time_end, time_start));
+    u64 sec = divBy1000(delta);
+    u64 cent = divBy10(delta-1000*sec + 5);
+    seq_printf(m,"%s\n\n",pos > 0 ? "Ok" : "No");
+    seq_printf(m,"Witnesses\nPositive: %"PCTR", Negative: %"PCTR"\n",pos,neg);
+    seq_printf(m,"Condition exists (0:r1=1 /\\ 1:r1=1) is %svalidated\n",pos > 0?"":"NOT ");
+    seq_printf(m,"%s\n","Hash=4a8c15603ffb5ab464195ea39ccd6382");
+    if (pos == 0) msg = "Never";
+    else if (neg == 0) msg = "Always";
+    seq_printf(m,"Observation AL+test %s %"PCTR" %"PCTR"\n",msg,pos,neg);
+    seq_printf(m,"Time AL+test %llu.%02llu\n\n",sec,cent);
+  }
+  free_outs(outs);
+  return 0;
+}
+
+static int
+litmus_proc_show(struct seq_file *m,void *v) {
+  if (ninst == 0 || ninst * nthreads > nonline) {
+    seq_printf(m,"%s: skipped\n","AL+test");
+    return 0;
+  } else {
+  return do_it(m);
+  }
+}
+
+static int
+litmus_proc_open(struct inode *inode,struct file *fp) {
+  return single_open(fp,litmus_proc_show,NULL);
+}
+
+static const struct file_operations litmus_proc_fops = {
+  .owner   = THIS_MODULE,
+  .open    = litmus_proc_open,
+  .read    = seq_read,
+  .llseek   = seq_lseek,
+  .release = single_release,
+};
+
+static int __init
+litmus_init(void) {
+  int err=0;
+  struct proc_dir_entry *litmus_pde = proc_create("litmus",0,NULL,&litmus_proc_fops);
+  if (litmus_pde == NULL) { return -ENOMEM; }
+  stride = stride == 0 ? 1 : stride;
+  nonline = num_online_cpus ();
+  online = kzalloc(sizeof(*online)*nonline,GFP_KERNEL);
+  if (online == NULL) goto clean_pde;
+  {
+    int cpu,_k;
+    _k=0; for_each_cpu(cpu,cpu_online_mask) online[_k++] = cpu;
+  }
+  if (avail == 0 || avail > nonline) avail = nonline;
+  if (ninst == 0) ninst = avail / nthreads ;
+
+  ctx = kzalloc(sizeof(ctx[0])*ninst,GFP_KERNEL);
+  if (ctx == NULL) { err = -ENOMEM ; goto clean_online; }
+  for (int _k=0 ; _k < ninst ; _k++) {
+    ctx[_k] = alloc_ctx(size);
+    if (ctx[_k] == NULL) { err = -ENOMEM; goto clean_ctx; }
+  }
+
+  wq =  kzalloc(sizeof(*wq), GFP_KERNEL);
+  if (wq == NULL) { err = -ENOMEM; goto clean_ctx; }
+  init_waitqueue_head(wq);
+  return 0; 
+clean_ctx:
+  for (int k=0 ; k < ninst ; k++) free_ctx(ctx[k]);
+  kfree(ctx);
+clean_online:
+  kfree(online);
+clean_pde:
+  remove_proc_entry("litmus",NULL);
+  return err;
+}
+
+static void __exit
+litmus_exit(void) {
+  for (int k=0 ; k < ninst ; k++) free_ctx(ctx[k]);
+  kfree(ctx);
+  kfree(online);
+  remove_proc_entry("litmus",NULL);
+}
+
+module_init(litmus_init);
+module_exit(litmus_exit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Luc");
+MODULE_DESCRIPTION("Litmus module");
diff --git a/drivers/misc/mymodules/run.sh b/drivers/misc/mymodules/run.sh
new file mode 100644
index 000000000000..c373bfc285db
--- /dev/null
+++ b/drivers/misc/mymodules/run.sh
@@ -0,0 +1,20 @@
+OPT="$*"
+date
+echo Compilation command: "/usr/local/google/home/joelaf/.local/bin/klitmus7 -o mymodules/ viro.litmus"
+echo "OPT=$OPT"
+echo "uname -r=$(uname -r)"
+echo
+
+zyva () {
+  name=$1
+  ko=$2
+  if test -f  $ko
+  then
+    insmod $ko $OPT
+    cat /proc/litmus
+    rmmod $ko
+  fi
+}
+
+zyva "AL+test" litmus000.ko
+date
-- 
2.28.0.806.g8561365e88-goog

Re: Litmus test for question from Al Viro

[joel]

On Sat, Oct 03, 2020 at 12:08:46PM -0400, joel@joelfernandes.org wrote:
[...] 
> static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {
> 
>         struct v_struct *r1; /* to_free */
> 
>         r1 = NULL;
>         spin_lock(l);
>         if (!smp_load_acquire(&v->b))
>                 r1 = v;
>         v->a = 0;
>         spin_unlock(l);
> 
>   *out_0_r1 = !!r1;
> }
> 
> static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {
> 
>         struct v_struct *r1; /* to_free */
> 
>         r1 = v;
>         if (READ_ONCE(v->a)) {
>                 spin_lock(l);
>                 if (v->a)
>                         r1 = NULL;
>                 smp_store_release(&v->b, 0);
>                 spin_unlock(l);
>         }
> 
>   *out_1_r1 = !!r1;
> }
> 
> Results on both arm64 and x86:
> 
>     Histogram (2 states)
>     19080852:>0:r1=1; 1:r1=0;
>     20919148:>0:r1=0; 1:r1=1;
>     No
>     
>     Witnesses
>     Positive: 0, Negative: 40000000
>     Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
>     Hash=4a8c15603ffb5ab464195ea39ccd6382
>     Observation AL+test Never 0 40000000
>     Time AL+test 6.24
> 
> I guess I could do an alloc and free of v_struct. However, I just checked for
> whether the to_free in Al's example could ever be NULL for both threads.

Sorry, here I meant "ever be non-NULL".

So basically I was trying to experimentally confirm that to_free could never
be non-NULL in both code0 and code1 threads.

Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> Hi Alan,
> 
> Just a minor nit in the litmus test.
> 
> On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> > To expand on my statement about the LKMM's weakness regarding control 
> > constructs, here is a litmus test to illustrate the issue.  You might 
> > want to add this to one of the archives.
> > 
> > Alan
> > 
> > C crypto-control-data
> > (*
> >  * LB plus crypto-control-data plus data
> >  *
> >  * Expected result: allowed
> >  *
> >  * This is an example of OOTA and we would like it to be forbidden.
> >  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> >  * control-dependent on the preceding READ_ONCE.  But the dependencies are
> >  * hidden by the form of the conditional control construct, hence the 
> >  * name "crypto-control-data".  The memory model doesn't recognize them.
> >  *)
> > 
> > {}
> > 
> > P0(int *x, int *y)
> > {
> > 	int r1;
> > 
> > 	r1 = 1;
> > 	if (READ_ONCE(*x) == 0)
> > 		r1 = 0;
> > 	WRITE_ONCE(*y, r1);
> > }
> > 
> > P1(int *x, int *y)
> > {
> > 	WRITE_ONCE(*x, READ_ONCE(*y));
> 
> Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.

You're right.  This is definitely a bug in herd7.

Luc, were you aware of this?

> When I changed P1 to
> 
> P1(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = READ_ONCE(*y);
> 	WRITE_ONCE(*x, r1);
> }
> 
> and replaced the WRITE_ONCE() in P0 with smp_store_release(),
> I got the result of:
> 
> -----
> Test crypto-control-data Allowed
> States 1
> 0:r1=0;
> No
> Witnesses
> Positive: 0 Negative: 3
> Condition exists (0:r1=1)
> Observation crypto-control-data Never 0 3
> Time crypto-control-data 0.01
> Hash=9b9aebbaf945dad8183d2be0ccb88e11
> -----
> 
> Restoring the WRITE_ONCE() in P0, I got the result of:
> 
> -----
> Test crypto-control-data Allowed
> States 2
> 0:r1=0;
> 0:r1=1;
> Ok
> Witnesses
> Positive: 1 Negative: 4
> Condition exists (0:r1=1)
> Observation crypto-control-data Sometimes 1 4
> Time crypto-control-data 0.01
> Hash=843eaa4974cec0efae79ce3cb73a1278
> -----

What you should have done was put smp_store_release in P0 and left P1 in 
its original form.  That test should not be allowed, but herd7 says that 
it is.

> As this is the same as the expected result, I suppose you have missed another
> limitation of herd7 + LKMM.

It would be more accurate to say that we all missed it.  :-)  (And it's 
a bug in herd7, not a limitation of either herd7 or LKMM.)  How did you 
notice it?

> By the way, I think this weakness on control dependency + data dependency
> deserves an entry in tools/memory-model/Documentation/litmus-tests.txt.
> 
> In the LIMITATIONS section, item #1 mentions some situation where
> LKMM may not recognize possible losses of control-dependencies by
> compiler optimizations.
> 
> What this litmus test demonstrates is a different class of mismatch.

Yes, one in which LKMM does not recognize a genuine dependency because 
it can't tell that some optimizations are not valid.

This flaw is fundamental to the way herd7 works.  It examines only one 
execution at a time, and it doesn't consider the code in a conditional 
branch while it's examining an execution where that branch wasn't taken.  
Therefore it has no way to know that the code in the unexecuted branch 
would prevent a certain optimization.  But the compiler does consider 
all the code in all branches when deciding what optimizations to apply.

Here's another trivial example:

	r1 = READ_ONCE(*x);
	if (r1 == 0)
		smp_mb();
	WRITE_ONCE(*y, 1);

The compiler can't move the WRITE_ONCE before the READ_ONCE or the "if" 
statement, because it's not allowed to move shared memory accesses past 
a memory barrier -- even if that memory barrier isn't always executed.  
Therefore the WRITE_ONCE actually is ordered after the READ_ONCE, but 
the memory model doesn't realize it.

> Alan, can you come up with an update in this regard?

I'll write something.

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Akira Yokosawa]

On Sat, 3 Oct 2020 13:13:38 -0400, Alan Stern wrote:
> On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
>> Hi Alan,
>>
>> Just a minor nit in the litmus test.
>>
>> On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
>>> To expand on my statement about the LKMM's weakness regarding control 
>>> constructs, here is a litmus test to illustrate the issue.  You might 
>>> want to add this to one of the archives.
>>>
>>> Alan
>>>
>>> C crypto-control-data
>>> (*
>>>  * LB plus crypto-control-data plus data
>>>  *
>>>  * Expected result: allowed
>>>  *
>>>  * This is an example of OOTA and we would like it to be forbidden.
>>>  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
>>>  * control-dependent on the preceding READ_ONCE.  But the dependencies are
>>>  * hidden by the form of the conditional control construct, hence the 
>>>  * name "crypto-control-data".  The memory model doesn't recognize them.
>>>  *)
>>>
>>> {}
>>>
>>> P0(int *x, int *y)
>>> {
>>> 	int r1;
>>>
>>> 	r1 = 1;
>>> 	if (READ_ONCE(*x) == 0)
>>> 		r1 = 0;
>>> 	WRITE_ONCE(*y, r1);
>>> }
>>>
>>> P1(int *x, int *y)
>>> {
>>> 	WRITE_ONCE(*x, READ_ONCE(*y));
>>
>> Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
> 
> You're right.  This is definitely a bug in herd7.
> 
> Luc, were you aware of this?
> 
>> When I changed P1 to
>>
>> P1(int *x, int *y)
>> {
>> 	int r1;
>>
>> 	r1 = READ_ONCE(*y);
>> 	WRITE_ONCE(*x, r1);
>> }
>>
>> and replaced the WRITE_ONCE() in P0 with smp_store_release(),
>> I got the result of:
>>
>> -----
>> Test crypto-control-data Allowed
>> States 1
>> 0:r1=0;
>> No
>> Witnesses
>> Positive: 0 Negative: 3
>> Condition exists (0:r1=1)
>> Observation crypto-control-data Never 0 3
>> Time crypto-control-data 0.01
>> Hash=9b9aebbaf945dad8183d2be0ccb88e11
>> -----
>>
>> Restoring the WRITE_ONCE() in P0, I got the result of:
>>
>> -----
>> Test crypto-control-data Allowed
>> States 2
>> 0:r1=0;
>> 0:r1=1;
>> Ok
>> Witnesses
>> Positive: 1 Negative: 4
>> Condition exists (0:r1=1)
>> Observation crypto-control-data Sometimes 1 4
>> Time crypto-control-data 0.01
>> Hash=843eaa4974cec0efae79ce3cb73a1278
>> -----
> 
> What you should have done was put smp_store_release in P0 and left P1 in 
> its original form.  That test should not be allowed, but herd7 says that 
> it is.

Yea, that was what I tried first, expecting the result of "Never".

> 
>> As this is the same as the expected result, I suppose you have missed another
>> limitation of herd7 + LKMM.
> 
> It would be more accurate to say that we all missed it.  :-)  (And it's 
> a bug in herd7, not a limitation of either herd7 or LKMM.)  How did you 
> notice it?

:-) :-) :-)

Well, I thought I had never seen a litmus test with such one-liner.
So I split the READ_ONCE() and WRITE_ONCE() into two lines and
got the expected result.

I don't expect much from herd7's C mode in the first place.
(No offense intended!)

 
>> By the way, I think this weakness on control dependency + data dependency
>> deserves an entry in tools/memory-model/Documentation/litmus-tests.txt.
>>
>> In the LIMITATIONS section, item #1 mentions some situation where
>> LKMM may not recognize possible losses of control-dependencies by
>> compiler optimizations.
>>
>> What this litmus test demonstrates is a different class of mismatch.
> 
> Yes, one in which LKMM does not recognize a genuine dependency because 
> it can't tell that some optimizations are not valid.
> 
> This flaw is fundamental to the way herd7 works.  It examines only one 
> execution at a time, and it doesn't consider the code in a conditional 
> branch while it's examining an execution where that branch wasn't taken.  
> Therefore it has no way to know that the code in the unexecuted branch 
> would prevent a certain optimization.  But the compiler does consider 
> all the code in all branches when deciding what optimizations to apply.

I see.

> 
> Here's another trivial example:
> 
> 	r1 = READ_ONCE(*x);
> 	if (r1 == 0)
> 		smp_mb();
> 	WRITE_ONCE(*y, 1);
> 
> The compiler can't move the WRITE_ONCE before the READ_ONCE or the "if" 
> statement, because it's not allowed to move shared memory accesses past 
> a memory barrier -- even if that memory barrier isn't always executed.  
> Therefore the WRITE_ONCE actually is ordered after the READ_ONCE, but 
> the memory model doesn't realize it.> 
>> Alan, can you come up with an update in this regard?
> 
> I'll write something.

Thanks!

        Akira

> 
> Alan
> 

[PATCH] tools: memory-model: Document that the LKMM can easily miss control dependencies

[Alan Stern]

Add a small section to the litmus-tests.txt documentation file for
the Linux Kernel Memory Model explaining that the memory model often
fails to recognize certain control dependencies.

Suggested-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

---

 tools/memory-model/Documentation/litmus-tests.txt |   17 +++++++++++++++++
 1 file changed, 17 insertions(+)

Index: usb-devel/tools/memory-model/Documentation/litmus-tests.txt
===================================================================
--- usb-devel.orig/tools/memory-model/Documentation/litmus-tests.txt
+++ usb-devel/tools/memory-model/Documentation/litmus-tests.txt
@@ -946,6 +946,23 @@ Limitations of the Linux-kernel memory m
 	carrying a dependency, then the compiler can break that dependency
 	by substituting a constant of that value.
 
+	Conversely, LKMM sometimes doesn't recognize that a particular
+	optimization is not allowed, and as a result, thinks that a
+	dependency is not present (because the optimization would break it).
+	The memory model misses some pretty obvious control dependencies
+	because of this limitation.  A simple example is:
+
+		r1 = READ_ONCE(x);
+		if (r1 == 0)
+			smp_mb();
+		WRITE_ONCE(y, 1);
+
+	There is a control dependency from the READ_ONCE to the WRITE_ONCE,
+	even when r1 is nonzero, but LKMM doesn't realize this and thinks
+	that the write may execute before the read if r1 != 0.  (Yes, that
+	doesn't make sense if you think about it, but the memory model's
+	intelligence is limited.)
+
 2.	Multiple access sizes for a single variable are not supported,
 	and neither are misaligned or partially overlapping accesses.
 

Re: [PATCH] tools: memory-model: Document that the LKMM can easily miss control dependencies

[joel]

On Sat, Oct 03, 2020 at 09:40:22PM -0400, Alan Stern wrote:
> Add a small section to the litmus-tests.txt documentation file for
> the Linux Kernel Memory Model explaining that the memory model often
> fails to recognize certain control dependencies.
> 
> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>

Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

thanks,

 - Joel

> 
> ---
> 
>  tools/memory-model/Documentation/litmus-tests.txt |   17 +++++++++++++++++
>  1 file changed, 17 insertions(+)
> 
> Index: usb-devel/tools/memory-model/Documentation/litmus-tests.txt
> ===================================================================
> --- usb-devel.orig/tools/memory-model/Documentation/litmus-tests.txt
> +++ usb-devel/tools/memory-model/Documentation/litmus-tests.txt
> @@ -946,6 +946,23 @@ Limitations of the Linux-kernel memory m
>  	carrying a dependency, then the compiler can break that dependency
>  	by substituting a constant of that value.
>  
> +	Conversely, LKMM sometimes doesn't recognize that a particular
> +	optimization is not allowed, and as a result, thinks that a
> +	dependency is not present (because the optimization would break it).
> +	The memory model misses some pretty obvious control dependencies
> +	because of this limitation.  A simple example is:
> +
> +		r1 = READ_ONCE(x);
> +		if (r1 == 0)
> +			smp_mb();
> +		WRITE_ONCE(y, 1);
> +
> +	There is a control dependency from the READ_ONCE to the WRITE_ONCE,
> +	even when r1 is nonzero, but LKMM doesn't realize this and thinks
> +	that the write may execute before the read if r1 != 0.  (Yes, that
> +	doesn't make sense if you think about it, but the memory model's
> +	intelligence is limited.)
> +
>  2.	Multiple access sizes for a single variable are not supported,
>  	and neither are misaligned or partially overlapping accesses.
>  

Re: [PATCH] tools: memory-model: Document that the LKMM can easily miss control dependencies

[Paul E. McKenney]

On Sun, Oct 04, 2020 at 05:07:47PM -0400, joel@joelfernandes.org wrote:
> On Sat, Oct 03, 2020 at 09:40:22PM -0400, Alan Stern wrote:
> > Add a small section to the litmus-tests.txt documentation file for
> > the Linux Kernel Memory Model explaining that the memory model often
> > fails to recognize certain control dependencies.
> > 
> > Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> 
> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

Good addition!  Applied, and thank you all!!!

							Thanx, Paul

> thanks,
> 
>  - Joel
> 
> > 
> > ---
> > 
> >  tools/memory-model/Documentation/litmus-tests.txt |   17 +++++++++++++++++
> >  1 file changed, 17 insertions(+)
> > 
> > Index: usb-devel/tools/memory-model/Documentation/litmus-tests.txt
> > ===================================================================
> > --- usb-devel.orig/tools/memory-model/Documentation/litmus-tests.txt
> > +++ usb-devel/tools/memory-model/Documentation/litmus-tests.txt
> > @@ -946,6 +946,23 @@ Limitations of the Linux-kernel memory m
> >  	carrying a dependency, then the compiler can break that dependency
> >  	by substituting a constant of that value.
> >  
> > +	Conversely, LKMM sometimes doesn't recognize that a particular
> > +	optimization is not allowed, and as a result, thinks that a
> > +	dependency is not present (because the optimization would break it).
> > +	The memory model misses some pretty obvious control dependencies
> > +	because of this limitation.  A simple example is:
> > +
> > +		r1 = READ_ONCE(x);
> > +		if (r1 == 0)
> > +			smp_mb();
> > +		WRITE_ONCE(y, 1);
> > +
> > +	There is a control dependency from the READ_ONCE to the WRITE_ONCE,
> > +	even when r1 is nonzero, but LKMM doesn't realize this and thinks
> > +	that the write may execute before the read if r1 != 0.  (Yes, that
> > +	doesn't make sense if you think about it, but the memory model's
> > +	intelligence is limited.)
> > +
> >  2.	Multiple access sizes for a single variable are not supported,
> >  	and neither are misaligned or partially overlapping accesses.
> >  

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Sat, Oct 03, 2020 at 12:11:59PM -0400, joel@joelfernandes.org wrote:
> On Sat, Oct 03, 2020 at 12:08:46PM -0400, joel@joelfernandes.org wrote:
> [...] 
> > static void code0(struct v_struct* v,spinlock_t* l,int* out_0_r1) {
> > 
> >         struct v_struct *r1; /* to_free */
> > 
> >         r1 = NULL;
> >         spin_lock(l);
> >         if (!smp_load_acquire(&v->b))
> >                 r1 = v;
> >         v->a = 0;
> >         spin_unlock(l);
> > 
> >   *out_0_r1 = !!r1;
> > }
> > 
> > static void code1(struct v_struct* v,spinlock_t* l,int* out_1_r1) {
> > 
> >         struct v_struct *r1; /* to_free */
> > 
> >         r1 = v;
> >         if (READ_ONCE(v->a)) {
> >                 spin_lock(l);
> >                 if (v->a)
> >                         r1 = NULL;
> >                 smp_store_release(&v->b, 0);
> >                 spin_unlock(l);
> >         }
> > 
> >   *out_1_r1 = !!r1;
> > }
> > 
> > Results on both arm64 and x86:
> > 
> >     Histogram (2 states)
> >     19080852:>0:r1=1; 1:r1=0;
> >     20919148:>0:r1=0; 1:r1=1;
> >     No
> >     
> >     Witnesses
> >     Positive: 0, Negative: 40000000
> >     Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
> >     Hash=4a8c15603ffb5ab464195ea39ccd6382
> >     Observation AL+test Never 0 40000000
> >     Time AL+test 6.24
> > 
> > I guess I could do an alloc and free of v_struct. However, I just checked for
> > whether the to_free in Al's example could ever be NULL for both threads.
> 
> Sorry, here I meant "ever be non-NULL".
> 
> So basically I was trying to experimentally confirm that to_free could never
> be non-NULL in both code0 and code1 threads.

Thank you for running these!  In conjunction with Alan's analysis,
this seems quite convincing.  ;-)

							Thanx, Paul

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Sat, Oct 03, 2020 at 09:22:12AM -0400, Alan Stern wrote:
> To expand on my statement about the LKMM's weakness regarding control 
> constructs, here is a litmus test to illustrate the issue.  You might 
> want to add this to one of the archives.
> 
> Alan
> 
> C crypto-control-data
> (*
>  * LB plus crypto-control-data plus data
>  *
>  * Expected result: allowed
>  *
>  * This is an example of OOTA and we would like it to be forbidden.
>  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
>  * control-dependent on the preceding READ_ONCE.  But the dependencies are
>  * hidden by the form of the conditional control construct, hence the 
>  * name "crypto-control-data".  The memory model doesn't recognize them.
>  *)
> 
> {}
> 
> P0(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = 1;
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	WRITE_ONCE(*y, r1);
> }
> 
> P1(int *x, int *y)
> {
> 	WRITE_ONCE(*x, READ_ONCE(*y));
> }
> 
> exists (0:r1=1)

Nice simple example!  How about like this?

							Thanx, Paul

------------------------------------------------------------------------

commit c964f404eabe4d8ce294e59dda713d8c19d340cf
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Sun Oct 4 16:27:03 2020 -0700

    manual/kernel: Add a litmus test with a hidden dependency
    
    This commit adds a litmus test that has a data dependency that can be
    hidden by control flow.  In this test, both the taken and the not-taken
    branches of an "if" statement must be accounted for in order to properly
    analyze the litmus test.  But herd7 looks only at individual executions
    in isolation, so fails to see the dependency.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
new file mode 100644
index 0000000..6baecf9
--- /dev/null
+++ b/manual/kernel/crypto-control-data.litmus
@@ -0,0 +1,31 @@
+C crypto-control-data
+(*
+ * LB plus crypto-control-data plus data
+ *
+ * Result: Sometimes
+ *
+ * This is an example of OOTA and we would like it to be forbidden.
+ * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
+ * control-dependent on the preceding READ_ONCE.  But the dependencies are
+ * hidden by the form of the conditional control construct, hence the 
+ * name "crypto-control-data".  The memory model doesn't recognize them.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = 1;
+	if (READ_ONCE(*x) == 0)
+		r1 = 0;
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Fri, Oct 02, 2020 at 10:35:45PM -0400, Jon Masters wrote:
> On 10/1/20 12:15 PM, Alan Stern wrote:
> > On Wed, Sep 30, 2020 at 09:51:16PM -0700, Paul E. McKenney wrote:
> > > Hello!
> > > 
> > > Al Viro posted the following query:
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > <viro> fun question regarding barriers, if you have time for that
> > > <viro>         V->A = V->B = 1;
> > > <viro>
> > > <viro> CPU1:
> > > <viro>         to_free = NULL
> > > <viro>         spin_lock(&LOCK)
> > > <viro>         if (!smp_load_acquire(&V->B))
> > > <viro>                 to_free = V
> > > <viro>         V->A = 0
> > > <viro>         spin_unlock(&LOCK)
> > > <viro>         kfree(to_free)
> > > <viro>
> > > <viro> CPU2:
> > > <viro>         to_free = V;
> > > <viro>         if (READ_ONCE(V->A)) {
> > > <viro>                 spin_lock(&LOCK)
> > > <viro>                 if (V->A)
> > > <viro>                         to_free = NULL
> > > <viro>                 smp_store_release(&V->B, 0);
> > > <viro>                 spin_unlock(&LOCK)
> > > <viro>         }
> > > <viro>         kfree(to_free);
> > > <viro> 1) is it guaranteed that V will be freed exactly once and that
> > > 	  no accesses to *V will happen after freeing it?
> > > <viro> 2) do we need smp_store_release() there?  I.e. will anything
> > > 	  break if it's replaced with plain V->B = 0?
> > 
> > Here are my answers to Al's questions:
> > 
> > 1) It is guaranteed that V will be freed exactly once.  It is not
> > guaranteed that no accesses to *V will occur after it is freed, because
> > the test contains a data race.  CPU1's plain "V->A = 0" write races with
> > CPU2's READ_ONCE; if the plain write were replaced with
> > "WRITE_ONCE(V->A, 0)" then the guarantee would hold.  Equally well,
> > CPU1's smp_load_acquire could be replaced with a plain read while the
> > plain write is replaced with smp_store_release.
> > 
> > 2) The smp_store_release in CPU2 is not needed.  Replacing it with a
> > plain V->B = 0 will not break anything.
> 
> This was my interpretation also. I made the mistake of reading this right
> before trying to go to bed the other night and ended up tweeting at Paul
> that I'd regret it if he gave me scary dreams. Thought about it and read
> your write up and it is still exactly how I see it.

Should I have added a "read at your own risk" disclaimer?  ;-)

							Thanx, Paul

Re: Litmus test for question from Al Viro

[Alan Stern]

On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> Nice simple example!  How about like this?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Sun Oct 4 16:27:03 2020 -0700
> 
>     manual/kernel: Add a litmus test with a hidden dependency
>     
>     This commit adds a litmus test that has a data dependency that can be
>     hidden by control flow.  In this test, both the taken and the not-taken
>     branches of an "if" statement must be accounted for in order to properly
>     analyze the litmus test.  But herd7 looks only at individual executions
>     in isolation, so fails to see the dependency.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 0000000..6baecf9
> --- /dev/null
> +++ b/manual/kernel/crypto-control-data.litmus
> @@ -0,0 +1,31 @@
> +C crypto-control-data
> +(*
> + * LB plus crypto-control-data plus data
> + *
> + * Result: Sometimes
> + *
> + * This is an example of OOTA and we would like it to be forbidden.
> + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> + * hidden by the form of the conditional control construct, hence the 
> + * name "crypto-control-data".  The memory model doesn't recognize them.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = 1;
> +	if (READ_ONCE(*x) == 0)
> +		r1 = 0;
> +	WRITE_ONCE(*y, r1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	WRITE_ONCE(*x, READ_ONCE(*y));
> +}
> +
> +exists (0:r1=1)

Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:

P1(int *x, int *y)
{
	int r2;

	r = READ_ONCE(*y);
	WRITE_ONCE(*x, r2);
}

Other than that, this is fine.

Alan

Re: Litmus test for question from Al Viro

[Will Deacon]

On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > Nice simple example!  How about like this?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Sun Oct 4 16:27:03 2020 -0700
> > 
> >     manual/kernel: Add a litmus test with a hidden dependency
> >     
> >     This commit adds a litmus test that has a data dependency that can be
> >     hidden by control flow.  In this test, both the taken and the not-taken
> >     branches of an "if" statement must be accounted for in order to properly
> >     analyze the litmus test.  But herd7 looks only at individual executions
> >     in isolation, so fails to see the dependency.
> >     
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 0000000..6baecf9
> > --- /dev/null
> > +++ b/manual/kernel/crypto-control-data.litmus
> > @@ -0,0 +1,31 @@
> > +C crypto-control-data
> > +(*
> > + * LB plus crypto-control-data plus data
> > + *
> > + * Result: Sometimes
> > + *
> > + * This is an example of OOTA and we would like it to be forbidden.
> > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > + * hidden by the form of the conditional control construct, hence the 
> > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = 1;
> > +	if (READ_ONCE(*x) == 0)
> > +		r1 = 0;
> > +	WRITE_ONCE(*y, r1);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > +}
> > +
> > +exists (0:r1=1)
> 
> Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> 
> P1(int *x, int *y)
> {
> 	int r2;
> 
> 	r = READ_ONCE(*y);

(r2?)

> 	WRITE_ONCE(*x, r2);
> }
> 
> Other than that, this is fine.

But yes, module the typo, I agree that this rewrite is much better than the
proposal above. The definition of control dependencies on arm64 (per the Arm
ARM [1]) isn't entirely clear that it provides order if the WRITE is
executed on both paths of the branch, and I believe there are ongoing
efforts to try to tighten that up. I'd rather keep _that_ topic separate
from the "bug in herd" topic to avoid extra confusion.

Will

[1] https://developer.arm.com/documentation/ddi0487/fc/

RE: Litmus test for question from Al Viro

[David Laight]

From: Paul E. McKenney
> Sent: 05 October 2020 00:32
...
>     manual/kernel: Add a litmus test with a hidden dependency
> 
>     This commit adds a litmus test that has a data dependency that can be
>     hidden by control flow.  In this test, both the taken and the not-taken
>     branches of an "if" statement must be accounted for in order to properly
>     analyze the litmus test.  But herd7 looks only at individual executions
>     in isolation, so fails to see the dependency.
> 
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 0000000..6baecf9
> --- /dev/null
> +++ b/manual/kernel/crypto-control-data.litmus
> @@ -0,0 +1,31 @@
> +C crypto-control-data
> +(*
> + * LB plus crypto-control-data plus data
> + *
> + * Result: Sometimes
> + *
> + * This is an example of OOTA and we would like it to be forbidden.
> + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> + * hidden by the form of the conditional control construct, hence the
> + * name "crypto-control-data".  The memory model doesn't recognize them.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = 1;
> +	if (READ_ONCE(*x) == 0)
> +		r1 = 0;
> +	WRITE_ONCE(*y, r1);
> +}

Hmmm.... the compiler will semi-randomly transform that to/from:
	if (READ_ONCE(*x) == 0)
		r1 = 0;
	else
		r1 = 1;
and
	r1 = READ_ONCE(*x) != 0;

Both of which (probably) get correctly detected as a write to *y
that is dependant on *x - so is 'problematic' with P1() which
does the opposite assignment.

Which does rather imply that hurd is a bit broken.

	David

-
Registered Address Lakeside, Bramley Road, Mount Farm, Milton Keynes, MK1 1PT, UK
Registration No: 1397386 (Wales)

Re: Litmus test for question from Al Viro

[Will Deacon]

On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > > Nice simple example!  How about like this?
> > > 
> > > 							Thanx, Paul
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > > Author: Alan Stern <stern@rowland.harvard.edu>
> > > Date:   Sun Oct 4 16:27:03 2020 -0700
> > > 
> > >     manual/kernel: Add a litmus test with a hidden dependency
> > >     
> > >     This commit adds a litmus test that has a data dependency that can be
> > >     hidden by control flow.  In this test, both the taken and the not-taken
> > >     branches of an "if" statement must be accounted for in order to properly
> > >     analyze the litmus test.  But herd7 looks only at individual executions
> > >     in isolation, so fails to see the dependency.
> > >     
> > >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > > 
> > > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > > new file mode 100644
> > > index 0000000..6baecf9
> > > --- /dev/null
> > > +++ b/manual/kernel/crypto-control-data.litmus
> > > @@ -0,0 +1,31 @@
> > > +C crypto-control-data
> > > +(*
> > > + * LB plus crypto-control-data plus data
> > > + *
> > > + * Result: Sometimes
> > > + *
> > > + * This is an example of OOTA and we would like it to be forbidden.
> > > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > > + * hidden by the form of the conditional control construct, hence the 
> > > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > > + *)
> > > +
> > > +{}
> > > +
> > > +P0(int *x, int *y)
> > > +{
> > > +	int r1;
> > > +
> > > +	r1 = 1;
> > > +	if (READ_ONCE(*x) == 0)
> > > +		r1 = 0;
> > > +	WRITE_ONCE(*y, r1);
> > > +}
> > > +
> > > +P1(int *x, int *y)
> > > +{
> > > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > > +}
> > > +
> > > +exists (0:r1=1)
> > 
> > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > 
> > P1(int *x, int *y)
> > {
> > 	int r2;
> > 
> > 	r = READ_ONCE(*y);
> 
> (r2?)
> 
> > 	WRITE_ONCE(*x, r2);
> > }
> > 
> > Other than that, this is fine.
> 
> But yes, module the typo, I agree that this rewrite is much better than the
> proposal above. The definition of control dependencies on arm64 (per the Arm
> ARM [1]) isn't entirely clear that it provides order if the WRITE is
> executed on both paths of the branch, and I believe there are ongoing
> efforts to try to tighten that up. I'd rather keep _that_ topic separate
> from the "bug in herd" topic to avoid extra confusion.

Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
about claiming that this is a bug in herd without input from Jade or Luc,
as it does unfortunately tie into the definition of control dependencies
and it could be a deliberate choice.

Jade, Luc: apparently herd doesn't emit a control dependency edge from
the READ_ONCE() to the WRITE_ONCE() in the following:


  P0(int *x, int *y)
  {
	int r1;

	r1 = 1;
	if (READ_ONCE(*x) == 0)
		r1 = 0;
	WRITE_ONCE(*y, r1);
  }


Is that deliberate?

Setting the arm64 architecture aside for one moment, I think the Linux
memory model would very much like the control dependency to exist in this
case. Documenting the unexpected outcome is one thing, but I think it would
be much better to do it in a way where users can reason about whether or not
they're falling into this trap rather than warning them that the results may
be unreliable, which is not likely to build confidence in the tool.

Will

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 08:36:51AM +0000, David Laight wrote:
> From: Paul E. McKenney
> > Sent: 05 October 2020 00:32
> ...
> >     manual/kernel: Add a litmus test with a hidden dependency
> > 
> >     This commit adds a litmus test that has a data dependency that can be
> >     hidden by control flow.  In this test, both the taken and the not-taken
> >     branches of an "if" statement must be accounted for in order to properly
> >     analyze the litmus test.  But herd7 looks only at individual executions
> >     in isolation, so fails to see the dependency.
> > 
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 0000000..6baecf9
> > --- /dev/null
> > +++ b/manual/kernel/crypto-control-data.litmus
> > @@ -0,0 +1,31 @@
> > +C crypto-control-data
> > +(*
> > + * LB plus crypto-control-data plus data
> > + *
> > + * Result: Sometimes
> > + *
> > + * This is an example of OOTA and we would like it to be forbidden.
> > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > + * hidden by the form of the conditional control construct, hence the
> > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = 1;
> > +	if (READ_ONCE(*x) == 0)
> > +		r1 = 0;
> > +	WRITE_ONCE(*y, r1);
> > +}
> 
> Hmmm.... the compiler will semi-randomly transform that to/from:
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	else
> 		r1 = 1;
> and
> 	r1 = READ_ONCE(*x) != 0;
> 
> Both of which (probably) get correctly detected as a write to *y
> that is dependant on *x - so is 'problematic' with P1() which
> does the opposite assignment.
> 
> Which does rather imply that hurd is a bit broken.

I agree that herd7 does not match all compilers, but the intent was
always to approximate them.  There has been some research work towards
the goal of accurately modeling all possible compiler optimizations,
and it gets extremely complex, and thus computationally infeasible,
very quickly.  And we do need herd7 to stay strictly in the realm of
the computationally feasible.

Hence, any use of control dependencies should follow up with something
like klitmus7 (as Joel Fernandes did earlier in this thread) or KCSAN.
These tools have their own limitations, for example, using a specific
compiler rather than saying something about all possible compilers, but
they do reflect what a specific real toolchain actually does.  They are
also execution based, so have only some probability of finding problems.
In contrast, herd7 does the moral equivalent of a full state-space search.

It would be nice to be able to say that we have one tools that does
everything, but that might be a long way down the road.

							Thanx, Paul

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > > > Nice simple example!  How about like this?
> > > > 
> > > > 							Thanx, Paul
> > > > 
> > > > ------------------------------------------------------------------------
> > > > 
> > > > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > > > Author: Alan Stern <stern@rowland.harvard.edu>
> > > > Date:   Sun Oct 4 16:27:03 2020 -0700
> > > > 
> > > >     manual/kernel: Add a litmus test with a hidden dependency
> > > >     
> > > >     This commit adds a litmus test that has a data dependency that can be
> > > >     hidden by control flow.  In this test, both the taken and the not-taken
> > > >     branches of an "if" statement must be accounted for in order to properly
> > > >     analyze the litmus test.  But herd7 looks only at individual executions
> > > >     in isolation, so fails to see the dependency.
> > > >     
> > > >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > > > 
> > > > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > > > new file mode 100644
> > > > index 0000000..6baecf9
> > > > --- /dev/null
> > > > +++ b/manual/kernel/crypto-control-data.litmus
> > > > @@ -0,0 +1,31 @@
> > > > +C crypto-control-data
> > > > +(*
> > > > + * LB plus crypto-control-data plus data
> > > > + *
> > > > + * Result: Sometimes
> > > > + *
> > > > + * This is an example of OOTA and we would like it to be forbidden.
> > > > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > > > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > > > + * hidden by the form of the conditional control construct, hence the 
> > > > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > > > + *)
> > > > +
> > > > +{}
> > > > +
> > > > +P0(int *x, int *y)
> > > > +{
> > > > +	int r1;
> > > > +
> > > > +	r1 = 1;
> > > > +	if (READ_ONCE(*x) == 0)
> > > > +		r1 = 0;
> > > > +	WRITE_ONCE(*y, r1);
> > > > +}
> > > > +
> > > > +P1(int *x, int *y)
> > > > +{
> > > > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > > > +}
> > > > +
> > > > +exists (0:r1=1)
> > > 
> > > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	int r2;
> > > 
> > > 	r = READ_ONCE(*y);
> > 
> > (r2?)
> > 
> > > 	WRITE_ONCE(*x, r2);
> > > }
> > > 
> > > Other than that, this is fine.
> > 
> > But yes, module the typo, I agree that this rewrite is much better than the
> > proposal above. The definition of control dependencies on arm64 (per the Arm
> > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > executed on both paths of the branch, and I believe there are ongoing
> > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > from the "bug in herd" topic to avoid extra confusion.
> 
> Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> about claiming that this is a bug in herd without input from Jade or Luc,
> as it does unfortunately tie into the definition of control dependencies
> and it could be a deliberate choice.
> 
> Jade, Luc: apparently herd doesn't emit a control dependency edge from
> the READ_ONCE() to the WRITE_ONCE() in the following:
> 
> 
>   P0(int *x, int *y)
>   {
> 	int r1;
> 
> 	r1 = 1;
> 	if (READ_ONCE(*x) == 0)
> 		r1 = 0;
> 	WRITE_ONCE(*y, r1);
>   }
> 
> 
> Is that deliberate?
> 
> Setting the arm64 architecture aside for one moment, I think the Linux
> memory model would very much like the control dependency to exist in this
> case. Documenting the unexpected outcome is one thing, but I think it would
> be much better to do it in a way where users can reason about whether or not
> they're falling into this trap rather than warning them that the results may
> be unreliable, which is not likely to build confidence in the tool.

It was in fact a deliberate choice.  Exact modeling of what compilers can
and cannot do gets extremely computationally intensive very quickly given
the current state of the art.

							Thanx, Paul

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > Nice simple example!  How about like this?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Sun Oct 4 16:27:03 2020 -0700
> > 
> >     manual/kernel: Add a litmus test with a hidden dependency
> >     
> >     This commit adds a litmus test that has a data dependency that can be
> >     hidden by control flow.  In this test, both the taken and the not-taken
> >     branches of an "if" statement must be accounted for in order to properly
> >     analyze the litmus test.  But herd7 looks only at individual executions
> >     in isolation, so fails to see the dependency.
> >     
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 0000000..6baecf9
> > --- /dev/null
> > +++ b/manual/kernel/crypto-control-data.litmus
> > @@ -0,0 +1,31 @@
> > +C crypto-control-data
> > +(*
> > + * LB plus crypto-control-data plus data
> > + *
> > + * Result: Sometimes
> > + *
> > + * This is an example of OOTA and we would like it to be forbidden.
> > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > + * hidden by the form of the conditional control construct, hence the 
> > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = 1;
> > +	if (READ_ONCE(*x) == 0)
> > +		r1 = 0;
> > +	WRITE_ONCE(*y, r1);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > +}
> > +
> > +exists (0:r1=1)
> 
> Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> 
> P1(int *x, int *y)
> {
> 	int r2;
> 
> 	r = READ_ONCE(*y);
> 	WRITE_ONCE(*x, r2);
> }
> 
> Other than that, this is fine.

Updated as suggested by Will, like this?

							Thanx, Paul

------------------------------------------------------------------------

commit adf43667b702582331d68acdf3732a6a017a182c
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Sun Oct 4 16:27:03 2020 -0700

    manual/kernel: Add a litmus test with a hidden dependency
    
    This commit adds a litmus test that has a data dependency that can be
    hidden by control flow.  In this test, both the taken and the not-taken
    branches of an "if" statement must be accounted for in order to properly
    analyze the litmus test.  But herd7 looks only at individual executions
    in isolation, so fails to see the dependency.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
new file mode 100644
index 0000000..cdcdec9
--- /dev/null
+++ b/manual/kernel/crypto-control-data.litmus
@@ -0,0 +1,34 @@
+C crypto-control-data
+(*
+ * LB plus crypto-control-data plus data
+ *
+ * Result: Sometimes
+ *
+ * This is an example of OOTA and we would like it to be forbidden.
+ * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
+ * control-dependent on the preceding READ_ONCE.  But the dependencies are
+ * hidden by the form of the conditional control construct, hence the 
+ * name "crypto-control-data".  The memory model doesn't recognize them.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = 1;
+	if (READ_ONCE(*x) == 0)
+		r1 = 0;
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	int r2;
+
+	r2 = READ_ONCE(*y);
+	WRITE_ONCE(*x, r2);
+}
+
+exists (0:r1=1)

Re: Litmus test for question from Al Viro

[Alan Stern]

On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > 
> > P1(int *x, int *y)
> > {
> > 	int r2;
> > 
> > 	r = READ_ONCE(*y);
> 
> (r2?)

Oops, yes, thank you.

> > 	WRITE_ONCE(*x, r2);
> > }
> > 
> > Other than that, this is fine.
> 
> But yes, module the typo, I agree that this rewrite is much better than the
> proposal above. The definition of control dependencies on arm64 (per the Arm
> ARM [1]) isn't entirely clear that it provides order if the WRITE is
> executed on both paths of the branch, and I believe there are ongoing
> efforts to try to tighten that up.

Do you mean that people aren't yet in agreement about what the answer 
should be?

How can the CPU tell whether a write is executed on both branches?  
Speculatively execute both and see if they both reach the same write 
instruction?  What if the same instruction is reached on both branches 
but the values written or the addresses written to are different?

>  I'd rather keep _that_ topic separate
> from the "bug in herd" topic to avoid extra confusion.

Indeed.

Alan

Re: Litmus test for question from Al Viro

[Alan Stern]

On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	int r2;
> > > 
> > > 	r = READ_ONCE(*y);
> > 
> > (r2?)
> > 
> > > 	WRITE_ONCE(*x, r2);
> > > }
> > > 
> > > Other than that, this is fine.
> > 
> > But yes, module the typo, I agree that this rewrite is much better than the
> > proposal above. The definition of control dependencies on arm64 (per the Arm
> > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > executed on both paths of the branch, and I believe there are ongoing
> > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > from the "bug in herd" topic to avoid extra confusion.
> 
> Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> about claiming that this is a bug in herd without input from Jade or Luc,
> as it does unfortunately tie into the definition of control dependencies
> and it could be a deliberate choice.

I think you misunderstood.  The bug in herd7 affects the way it handles 
P1, not P0.  With

	r2 = READ_ONCE(*y);
	WRITE_ONCE(*x, r2);

herd7 generates a data dependency from the read to the write.  With

	WRITE_ONCE(*x, READ_ONCE(*y));

it doesn't generate any dependency, even though the code does exactly 
the same thing as far as the memory model is concerned.  That's the bug 
I was referring to.

The failure to recognize the dependency in P0 should be considered a 
combined limitation of the memory model and herd7.  It's not a simple 
mistake that can be fixed by a small rewrite of herd7; rather it's a 
deliberate choice we made based on herd7's inherent design.  We 
explicitly said that control dependencies extend only to the code in the 
branches of an "if" statement; anything beyond the end of the statement 
is not considered to be dependent.

Alan

Re: Litmus test for question from Al Viro

[Alan Stern]

On Mon, Oct 05, 2020 at 07:03:53AM -0700, Paul E. McKenney wrote:
> Updated as suggested by Will, like this?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit adf43667b702582331d68acdf3732a6a017a182c
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Sun Oct 4 16:27:03 2020 -0700
> 
>     manual/kernel: Add a litmus test with a hidden dependency
>     
>     This commit adds a litmus test that has a data dependency that can be
>     hidden by control flow.  In this test, both the taken and the not-taken
>     branches of an "if" statement must be accounted for in order to properly
>     analyze the litmus test.  But herd7 looks only at individual executions
>     in isolation, so fails to see the dependency.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 0000000..cdcdec9
> --- /dev/null
> +++ b/manual/kernel/crypto-control-data.litmus
> @@ -0,0 +1,34 @@
> +C crypto-control-data
> +(*
> + * LB plus crypto-control-data plus data
> + *
> + * Result: Sometimes
> + *
> + * This is an example of OOTA and we would like it to be forbidden.
> + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> + * hidden by the form of the conditional control construct, hence the 
> + * name "crypto-control-data".  The memory model doesn't recognize them.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = 1;
> +	if (READ_ONCE(*x) == 0)
> +		r1 = 0;
> +	WRITE_ONCE(*y, r1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r2;
> +
> +	r2 = READ_ONCE(*y);
> +	WRITE_ONCE(*x, r2);
> +}
> +
> +exists (0:r1=1)

Perfect!

Alan

Re: Litmus test for question from Al Viro

[joel]

On Mon, Oct 05, 2020 at 07:03:53AM -0700, Paul E. McKenney wrote:
> On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > > Nice simple example!  How about like this?
> > > 
> > > 							Thanx, Paul
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > > Author: Alan Stern <stern@rowland.harvard.edu>
> > > Date:   Sun Oct 4 16:27:03 2020 -0700
> > > 
> > >     manual/kernel: Add a litmus test with a hidden dependency
> > >     
> > >     This commit adds a litmus test that has a data dependency that can be
> > >     hidden by control flow.  In this test, both the taken and the not-taken
> > >     branches of an "if" statement must be accounted for in order to properly
> > >     analyze the litmus test.  But herd7 looks only at individual executions
> > >     in isolation, so fails to see the dependency.
> > >     
> > >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > > 
> > > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > > new file mode 100644
> > > index 0000000..6baecf9
> > > --- /dev/null
> > > +++ b/manual/kernel/crypto-control-data.litmus
> > > @@ -0,0 +1,31 @@
> > > +C crypto-control-data
> > > +(*
> > > + * LB plus crypto-control-data plus data
> > > + *
> > > + * Result: Sometimes
> > > + *
> > > + * This is an example of OOTA and we would like it to be forbidden.
> > > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > > + * hidden by the form of the conditional control construct, hence the 
> > > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > > + *)
> > > +
> > > +{}
> > > +
> > > +P0(int *x, int *y)
> > > +{
> > > +	int r1;
> > > +
> > > +	r1 = 1;
> > > +	if (READ_ONCE(*x) == 0)
> > > +		r1 = 0;
> > > +	WRITE_ONCE(*y, r1);
> > > +}
> > > +
> > > +P1(int *x, int *y)
> > > +{
> > > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > > +}
> > > +
> > > +exists (0:r1=1)
> > 
> > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > 
> > P1(int *x, int *y)
> > {
> > 	int r2;
> > 
> > 	r = READ_ONCE(*y);
> > 	WRITE_ONCE(*x, r2);
> > }
> > 
> > Other than that, this is fine.
> 
> Updated as suggested by Will, like this?

LGTM as well,

FWIW:
Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

thanks,

 - Joel

> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit adf43667b702582331d68acdf3732a6a017a182c
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Sun Oct 4 16:27:03 2020 -0700
> 
>     manual/kernel: Add a litmus test with a hidden dependency
>     
>     This commit adds a litmus test that has a data dependency that can be
>     hidden by control flow.  In this test, both the taken and the not-taken
>     branches of an "if" statement must be accounted for in order to properly
>     analyze the litmus test.  But herd7 looks only at individual executions
>     in isolation, so fails to see the dependency.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> new file mode 100644
> index 0000000..cdcdec9
> --- /dev/null
> +++ b/manual/kernel/crypto-control-data.litmus
> @@ -0,0 +1,34 @@
> +C crypto-control-data
> +(*
> + * LB plus crypto-control-data plus data
> + *
> + * Result: Sometimes
> + *
> + * This is an example of OOTA and we would like it to be forbidden.
> + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> + * hidden by the form of the conditional control construct, hence the 
> + * name "crypto-control-data".  The memory model doesn't recognize them.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = 1;
> +	if (READ_ONCE(*x) == 0)
> +		r1 = 0;
> +	WRITE_ONCE(*y, r1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r2;
> +
> +	r2 = READ_ONCE(*y);
> +	WRITE_ONCE(*x, r2);
> +}
> +
> +exists (0:r1=1)

Re: Litmus test for question from Al Viro

[Will Deacon]

On Mon, Oct 05, 2020 at 10:23:51AM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 10:12:48AM +0100, Will Deacon wrote:
> > On Mon, Oct 05, 2020 at 09:20:03AM +0100, Will Deacon wrote:
> > > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > > > 
> > > > P1(int *x, int *y)
> > > > {
> > > > 	int r2;
> > > > 
> > > > 	r = READ_ONCE(*y);
> > > 
> > > (r2?)
> > > 
> > > > 	WRITE_ONCE(*x, r2);
> > > > }
> > > > 
> > > > Other than that, this is fine.
> > > 
> > > But yes, module the typo, I agree that this rewrite is much better than the
> > > proposal above. The definition of control dependencies on arm64 (per the Arm
> > > ARM [1]) isn't entirely clear that it provides order if the WRITE is
> > > executed on both paths of the branch, and I believe there are ongoing
> > > efforts to try to tighten that up. I'd rather keep _that_ topic separate
> > > from the "bug in herd" topic to avoid extra confusion.
> > 
> > Ah, now I see that you're changing P1 here, not P0. So I'm now nervous
> > about claiming that this is a bug in herd without input from Jade or Luc,
> > as it does unfortunately tie into the definition of control dependencies
> > and it could be a deliberate choice.
> 
> I think you misunderstood.  The bug in herd7 affects the way it handles 
> P1, not P0.  With
> 
> 	r2 = READ_ONCE(*y);
> 	WRITE_ONCE(*x, r2);
> 
> herd7 generates a data dependency from the read to the write.  With
> 
> 	WRITE_ONCE(*x, READ_ONCE(*y));
> 
> it doesn't generate any dependency, even though the code does exactly 
> the same thing as far as the memory model is concerned.  That's the bug 
> I was referring to.

Thanks, that clears things up. There were lots of mentions of "control
dependency" in the mail thread that threw me, because this bug is clearly
about data dependencies!

> The failure to recognize the dependency in P0 should be considered a 
> combined limitation of the memory model and herd7.  It's not a simple 
> mistake that can be fixed by a small rewrite of herd7; rather it's a 
> deliberate choice we made based on herd7's inherent design.  We 
> explicitly said that control dependencies extend only to the code in the 
> branches of an "if" statement; anything beyond the end of the statement 
> is not considered to be dependent.

Interesting. How does this interact with loops that are conditionally broken
out of, e.g.  a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call
prior to a WRITE_ONCE()?

Will

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Luc Maranget]

> On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > Hi Alan,
> > 
> > Just a minor nit in the litmus test.
> > 
> > On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> > > To expand on my statement about the LKMM's weakness regarding control 
> > > constructs, here is a litmus test to illustrate the issue.  You might 
> > > want to add this to one of the archives.
> > > 
> > > Alan
> > > 
> > > C crypto-control-data
> > > (*
> > >  * LB plus crypto-control-data plus data
> > >  *
> > >  * Expected result: allowed
> > >  *
> > >  * This is an example of OOTA and we would like it to be forbidden.
> > >  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > >  * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > >  * hidden by the form of the conditional control construct, hence the 
> > >  * name "crypto-control-data".  The memory model doesn't recognize them.
> > >  *)
> > > 
> > > {}
> > > 
> > > P0(int *x, int *y)
> > > {
> > > 	int r1;
> > > 
> > > 	r1 = 1;
> > > 	if (READ_ONCE(*x) == 0)
> > > 		r1 = 0;
> > > 	WRITE_ONCE(*y, r1);
> > > }
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(*x, READ_ONCE(*y));
> > 
> > Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
> 
> You're right.  This is definitely a bug in herd7.
> 
> Luc, were you aware of this?

Hi Alan,

No I was not aware of it. Now I am, the bug is normally fixed in the master branch of herd git deposit.
<https://github.com/herd/herdtools7/commit/0f3f8188a326d5816a82fb9970fcd209a2678859>

Thanks for the report.

--Luc

Re: Litmus test for question from Al Viro

[Alan Stern]

On Mon, Oct 05, 2020 at 04:13:13PM +0100, Will Deacon wrote:
> > The failure to recognize the dependency in P0 should be considered a 
> > combined limitation of the memory model and herd7.  It's not a simple 
> > mistake that can be fixed by a small rewrite of herd7; rather it's a 
> > deliberate choice we made based on herd7's inherent design.  We 
> > explicitly said that control dependencies extend only to the code in the 
> > branches of an "if" statement; anything beyond the end of the statement 
> > is not considered to be dependent.
> 
> Interesting. How does this interact with loops that are conditionally broken
> out of, e.g.  a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call
> prior to a WRITE_ONCE()?

Heh --  We finesse this issue by not supporting loops at all!  :-)

Alan

Re: Litmus test for question from Al Viro

[Peter Zijlstra]

On Mon, Oct 05, 2020 at 11:16:39AM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 04:13:13PM +0100, Will Deacon wrote:
> > > The failure to recognize the dependency in P0 should be considered a 
> > > combined limitation of the memory model and herd7.  It's not a simple 
> > > mistake that can be fixed by a small rewrite of herd7; rather it's a 
> > > deliberate choice we made based on herd7's inherent design.  We 
> > > explicitly said that control dependencies extend only to the code in the 
> > > branches of an "if" statement; anything beyond the end of the statement 
> > > is not considered to be dependent.
> > 
> > Interesting. How does this interact with loops that are conditionally broken
> > out of, e.g.  a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call
> > prior to a WRITE_ONCE()?
> 
> Heh --  We finesse this issue by not supporting loops at all!  :-)

Right, so something like:

	smp_cond_load_relaxed(x, !VAL);
	WRITE_ONCE(*y, 1);

Would be modeled like:

	r1 = READ_ONCE(*x);
	if (!r1)
		WRITE_ONCE(*y, 1);

with an r1==0 constraint in the condition I suppose ?

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 05:35:19PM +0200, Peter Zijlstra wrote:
> On Mon, Oct 05, 2020 at 11:16:39AM -0400, Alan Stern wrote:
> > On Mon, Oct 05, 2020 at 04:13:13PM +0100, Will Deacon wrote:
> > > > The failure to recognize the dependency in P0 should be considered a 
> > > > combined limitation of the memory model and herd7.  It's not a simple 
> > > > mistake that can be fixed by a small rewrite of herd7; rather it's a 
> > > > deliberate choice we made based on herd7's inherent design.  We 
> > > > explicitly said that control dependencies extend only to the code in the 
> > > > branches of an "if" statement; anything beyond the end of the statement 
> > > > is not considered to be dependent.
> > > 
> > > Interesting. How does this interact with loops that are conditionally broken
> > > out of, e.g.  a relaxed cmpxchg() loop or an smp_cond_load_relaxed() call
> > > prior to a WRITE_ONCE()?
> > 
> > Heh --  We finesse this issue by not supporting loops at all!  :-)
> 
> Right, so something like:
> 
> 	smp_cond_load_relaxed(x, !VAL);
> 	WRITE_ONCE(*y, 1);
> 
> Would be modeled like:
> 
> 	r1 = READ_ONCE(*x);
> 	if (!r1)
> 		WRITE_ONCE(*y, 1);
> 
> with an r1==0 constraint in the condition I suppose ?

Yes, you got it!

However, it is more efficient to use the "filter" clause to tell herd7
about executions that are to be discarded.

							Thanx, Paul

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Mon, Oct 05, 2020 at 05:15:57PM +0200, Luc Maranget wrote:
> > On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > > > P1(int *x, int *y)
> > > > {
> > > > 	WRITE_ONCE(*x, READ_ONCE(*y));
> > > 
> > > Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
> > 
> > You're right.  This is definitely a bug in herd7.
> > 
> > Luc, were you aware of this?
> 
> Hi Alan,
> 
> No I was not aware of it. Now I am, the bug is normally fixed in the master branch of herd git deposit.
> <https://github.com/herd/herdtools7/commit/0f3f8188a326d5816a82fb9970fcd209a2678859>
> 
> Thanks for the report.

I tested the new commit -- it does indeed fix the problem.

Thanks.

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 05:15:57PM +0200, Luc Maranget wrote:
> > On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > > Hi Alan,
> > > 
> > > Just a minor nit in the litmus test.
> > > 
> > > On Sat, 3 Oct 2020 09:22:12 -0400, Alan Stern wrote:
> > > > To expand on my statement about the LKMM's weakness regarding control 
> > > > constructs, here is a litmus test to illustrate the issue.  You might 
> > > > want to add this to one of the archives.
> > > > 
> > > > Alan
> > > > 
> > > > C crypto-control-data
> > > > (*
> > > >  * LB plus crypto-control-data plus data
> > > >  *
> > > >  * Expected result: allowed
> > > >  *
> > > >  * This is an example of OOTA and we would like it to be forbidden.
> > > >  * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > > >  * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > > >  * hidden by the form of the conditional control construct, hence the 
> > > >  * name "crypto-control-data".  The memory model doesn't recognize them.
> > > >  *)
> > > > 
> > > > {}
> > > > 
> > > > P0(int *x, int *y)
> > > > {
> > > > 	int r1;
> > > > 
> > > > 	r1 = 1;
> > > > 	if (READ_ONCE(*x) == 0)
> > > > 		r1 = 0;
> > > > 	WRITE_ONCE(*y, r1);
> > > > }
> > > > 
> > > > P1(int *x, int *y)
> > > > {
> > > > 	WRITE_ONCE(*x, READ_ONCE(*y));
> > > 
> > > Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
> > 
> > You're right.  This is definitely a bug in herd7.
> > 
> > Luc, were you aware of this?
> 
> Hi Alan,
> 
> No I was not aware of it. Now I am, the bug is normally fixed in the master branch of herd git deposit.
> <https://github.com/herd/herdtools7/commit/0f3f8188a326d5816a82fb9970fcd209a2678859>
> 
> Thanks for the report.

Thank you very much, Luc!  I will rebuild and give it a try.

							Thanx, Paul

Re: Litmus test for question from Al Viro

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 10:44:22AM -0400, joel@joelfernandes.org wrote:
> On Mon, Oct 05, 2020 at 07:03:53AM -0700, Paul E. McKenney wrote:
> > On Sun, Oct 04, 2020 at 10:38:46PM -0400, Alan Stern wrote:
> > > On Sun, Oct 04, 2020 at 04:31:46PM -0700, Paul E. McKenney wrote:
> > > > Nice simple example!  How about like this?
> > > > 
> > > > 							Thanx, Paul
> > > > 
> > > > ------------------------------------------------------------------------
> > > > 
> > > > commit c964f404eabe4d8ce294e59dda713d8c19d340cf
> > > > Author: Alan Stern <stern@rowland.harvard.edu>
> > > > Date:   Sun Oct 4 16:27:03 2020 -0700
> > > > 
> > > >     manual/kernel: Add a litmus test with a hidden dependency
> > > >     
> > > >     This commit adds a litmus test that has a data dependency that can be
> > > >     hidden by control flow.  In this test, both the taken and the not-taken
> > > >     branches of an "if" statement must be accounted for in order to properly
> > > >     analyze the litmus test.  But herd7 looks only at individual executions
> > > >     in isolation, so fails to see the dependency.
> > > >     
> > > >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > > > 
> > > > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > > > new file mode 100644
> > > > index 0000000..6baecf9
> > > > --- /dev/null
> > > > +++ b/manual/kernel/crypto-control-data.litmus
> > > > @@ -0,0 +1,31 @@
> > > > +C crypto-control-data
> > > > +(*
> > > > + * LB plus crypto-control-data plus data
> > > > + *
> > > > + * Result: Sometimes
> > > > + *
> > > > + * This is an example of OOTA and we would like it to be forbidden.
> > > > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > > > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > > > + * hidden by the form of the conditional control construct, hence the 
> > > > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > > > + *)
> > > > +
> > > > +{}
> > > > +
> > > > +P0(int *x, int *y)
> > > > +{
> > > > +	int r1;
> > > > +
> > > > +	r1 = 1;
> > > > +	if (READ_ONCE(*x) == 0)
> > > > +		r1 = 0;
> > > > +	WRITE_ONCE(*y, r1);
> > > > +}
> > > > +
> > > > +P1(int *x, int *y)
> > > > +{
> > > > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > > > +}
> > > > +
> > > > +exists (0:r1=1)
> > > 
> > > Considering the bug in herd7 pointed out by Akira, we should rewrite P1 as:
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	int r2;
> > > 
> > > 	r = READ_ONCE(*y);
> > > 	WRITE_ONCE(*x, r2);
> > > }
> > > 
> > > Other than that, this is fine.
> > 
> > Updated as suggested by Will, like this?
> 
> LGTM as well,
> 
> FWIW:
> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org>

Applied, thank you all!

This has been pushed to my github litmus archive.

							Thanx, Paul

> thanks,
> 
>  - Joel
> 
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit adf43667b702582331d68acdf3732a6a017a182c
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Sun Oct 4 16:27:03 2020 -0700
> > 
> >     manual/kernel: Add a litmus test with a hidden dependency
> >     
> >     This commit adds a litmus test that has a data dependency that can be
> >     hidden by control flow.  In this test, both the taken and the not-taken
> >     branches of an "if" statement must be accounted for in order to properly
> >     analyze the litmus test.  But herd7 looks only at individual executions
> >     in isolation, so fails to see the dependency.
> >     
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/crypto-control-data.litmus b/manual/kernel/crypto-control-data.litmus
> > new file mode 100644
> > index 0000000..cdcdec9
> > --- /dev/null
> > +++ b/manual/kernel/crypto-control-data.litmus
> > @@ -0,0 +1,34 @@
> > +C crypto-control-data
> > +(*
> > + * LB plus crypto-control-data plus data
> > + *
> > + * Result: Sometimes
> > + *
> > + * This is an example of OOTA and we would like it to be forbidden.
> > + * The WRITE_ONCE in P0 is both data-dependent and (at the hardware level)
> > + * control-dependent on the preceding READ_ONCE.  But the dependencies are
> > + * hidden by the form of the conditional control construct, hence the 
> > + * name "crypto-control-data".  The memory model doesn't recognize them.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = 1;
> > +	if (READ_ONCE(*x) == 0)
> > +		r1 = 0;
> > +	WRITE_ONCE(*y, r1);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	int r2;
> > +
> > +	r2 = READ_ONCE(*y);
> > +	WRITE_ONCE(*x, r2);
> > +}
> > +
> > +exists (0:r1=1)

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 11:53:10AM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 05:15:57PM +0200, Luc Maranget wrote:
> > > On Sun, Oct 04, 2020 at 12:16:31AM +0900, Akira Yokosawa wrote:
> > > > > P1(int *x, int *y)
> > > > > {
> > > > > 	WRITE_ONCE(*x, READ_ONCE(*y));
> > > > 
> > > > Looks like this one-liner doesn't provide data-dependency of y -> x on herd7.
> > > 
> > > You're right.  This is definitely a bug in herd7.
> > > 
> > > Luc, were you aware of this?
> > 
> > Hi Alan,
> > 
> > No I was not aware of it. Now I am, the bug is normally fixed in the master branch of herd git deposit.
> > <https://github.com/herd/herdtools7/commit/0f3f8188a326d5816a82fb9970fcd209a2678859>
> > 
> > Thanks for the report.
> 
> I tested the new commit -- it does indeed fix the problem.

Beat me to it, very good!  ;-)

But were you using the crypto-control-data litmus test?  That one still
gets me Sometimes:

$ herd7 -version
7.56+02~dev, Rev: 0f3f8188a326d5816a82fb9970fcd209a2678859
$ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/crypto-control-data.litmus
Test crypto-control-data Allowed
States 2
0:r1=0;
0:r1=1;
Ok
Witnesses
Positive: 1 Negative: 4
Condition exists (0:r1=1)
Observation crypto-control-data Sometimes 1 4
Time crypto-control-data 0.00
Hash=10898119bac87e11f31dc22bbb7efe17

Or did I mess something up?

							Thanx, Paul

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Mon, Oct 05, 2020 at 09:52:23AM -0700, Paul E. McKenney wrote:
> On Mon, Oct 05, 2020 at 11:53:10AM -0400, Alan Stern wrote:
> > I tested the new commit -- it does indeed fix the problem.
> 
> Beat me to it, very good!  ;-)
> 
> But were you using the crypto-control-data litmus test?

I was not.  The test I used was what you get by starting from the 
version of crypto-control-data that had the one-liner in P1, and then 
replacing P0 with:

P0(int *x, int *y)
{
	int r1;

	r1 = READ_ONCE(*x);
	smp_mb();
	WRITE_ONCE(*y, 1);
}

Without the new commit this test is allowed; with the new commit it 
isn't (as we would expect).  Also, the graphical output from herd7 shows 
the data dependency in P1 with the commit, and doesn't show it without 
the commit.

>  That one still
> gets me Sometimes:
> 
> $ herd7 -version
> 7.56+02~dev, Rev: 0f3f8188a326d5816a82fb9970fcd209a2678859
> $ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/crypto-control-data.litmus
> Test crypto-control-data Allowed
> States 2
> 0:r1=0;
> 0:r1=1;
> Ok
> Witnesses
> Positive: 1 Negative: 4
> Condition exists (0:r1=1)
> Observation crypto-control-data Sometimes 1 4
> Time crypto-control-data 0.00
> Hash=10898119bac87e11f31dc22bbb7efe17
> 
> Or did I mess something up?

You didn't mess up anything.  That's the whole point of this litmus 
test: It should be forbidden because it is an example of OOTA, but LKMM 
allows it.  Even with Luc's new commit.

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 02:19:49PM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 09:52:23AM -0700, Paul E. McKenney wrote:
> > On Mon, Oct 05, 2020 at 11:53:10AM -0400, Alan Stern wrote:
> > > I tested the new commit -- it does indeed fix the problem.
> > 
> > Beat me to it, very good!  ;-)
> > 
> > But were you using the crypto-control-data litmus test?
> 
> I was not.  The test I used was what you get by starting from the 
> version of crypto-control-data that had the one-liner in P1, and then 
> replacing P0 with:
> 
> P0(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = READ_ONCE(*x);
> 	smp_mb();
> 	WRITE_ONCE(*y, 1);
> }
> 
> Without the new commit this test is allowed; with the new commit it 
> isn't (as we would expect).  Also, the graphical output from herd7 shows 
> the data dependency in P1 with the commit, and doesn't show it without 
> the commit.
> 
> >  That one still
> > gets me Sometimes:
> > 
> > $ herd7 -version
> > 7.56+02~dev, Rev: 0f3f8188a326d5816a82fb9970fcd209a2678859
> > $ herd7 -conf linux-kernel.cfg ~/paper/scalability/LWNLinuxMM/litmus/manual/kernel/crypto-control-data.litmus
> > Test crypto-control-data Allowed
> > States 2
> > 0:r1=0;
> > 0:r1=1;
> > Ok
> > Witnesses
> > Positive: 1 Negative: 4
> > Condition exists (0:r1=1)
> > Observation crypto-control-data Sometimes 1 4
> > Time crypto-control-data 0.00
> > Hash=10898119bac87e11f31dc22bbb7efe17
> > 
> > Or did I mess something up?
> 
> You didn't mess up anything.  That's the whole point of this litmus 
> test: It should be forbidden because it is an example of OOTA, but LKMM 
> allows it.  Even with Luc's new commit.

OK, got it.

Aside from naming and comment, how about my adding the following?

							Thanx, Paul

------------------------------------------------------------------------

C crypto-control-data-1
(*
 * LB plus crypto-mb-data plus data.
 *
 * Result: Never
 *
 * This is an example of OOTA and we would like it to be forbidden.
 * If you want herd7 to get the right answer, you must use herdtools
 * 0f3f8188a326 (" [herd] Fix dependency definition") or later.
 *)

{}

P0(int *x, int *y)
{
	int r1;

	r1 = READ_ONCE(*x);
	smp_mb();
	WRITE_ONCE(*y, r1);
}

P1(int *x, int *y)
{
	int r2;

	WRITE_ONCE(*x, READ_ONCE(*y));
}

exists (0:r1=1)

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Mon, Oct 05, 2020 at 12:18:01PM -0700, Paul E. McKenney wrote:
> Aside from naming and comment, how about my adding the following?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> C crypto-control-data-1

Let's call it something more along the lines of 
dependencies-in-nested-expressions.  Maybe you can think of something a 
little more succinct, but that's the general idea of the test.

> (*
>  * LB plus crypto-mb-data plus data.

The actual pattern is LB+mb+data.

>  *
>  * Result: Never
>  *
>  * This is an example of OOTA and we would like it to be forbidden.
>  * If you want herd7 to get the right answer, you must use herdtools
>  * 0f3f8188a326 (" [herd] Fix dependency definition") or later.

Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency 
definition") recognize data dependencies only when they flow through an 
intermediate local variable.  Since the dependency in P1 doesn't, those
versions get the wrong answer for this test.

>  *)
> 
> {}
> 
> P0(int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = READ_ONCE(*x);
> 	smp_mb();
> 	WRITE_ONCE(*y, r1);
> }
> 
> P1(int *x, int *y)
> {
> 	int r2;

No need for r2.

> 
> 	WRITE_ONCE(*x, READ_ONCE(*y));
> }
> 
> exists (0:r1=1)

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Mon, Oct 05, 2020 at 03:48:34PM -0400, Alan Stern wrote:
> On Mon, Oct 05, 2020 at 12:18:01PM -0700, Paul E. McKenney wrote:
> > Aside from naming and comment, how about my adding the following?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > C crypto-control-data-1
> 
> Let's call it something more along the lines of 
> dependencies-in-nested-expressions.  Maybe you can think of something a 
> little more succinct, but that's the general idea of the test.
> 
> > (*
> >  * LB plus crypto-mb-data plus data.
> 
> The actual pattern is LB+mb+data.
> 
> >  *
> >  * Result: Never
> >  *
> >  * This is an example of OOTA and we would like it to be forbidden.
> >  * If you want herd7 to get the right answer, you must use herdtools
> >  * 0f3f8188a326 (" [herd] Fix dependency definition") or later.
> 
> Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency 
> definition") recognize data dependencies only when they flow through an 
> intermediate local variable.  Since the dependency in P1 doesn't, those
> versions get the wrong answer for this test.
> 
> >  *)
> > 
> > {}
> > 
> > P0(int *x, int *y)
> > {
> > 	int r1;
> > 
> > 	r1 = READ_ONCE(*x);
> > 	smp_mb();
> > 	WRITE_ONCE(*y, r1);
> > }
> > 
> > P1(int *x, int *y)
> > {
> > 	int r2;
> 
> No need for r2.

Thank you for looking this over!

Like this, then?

							Thanx, Paul

------------------------------------------------------------------------

commit 51898676302d8ebc93856209f7c587f1ac0fdd11
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Tue Oct 6 09:38:37 2020 -0700

    manual/kernel: Add LB+mb+data litmus test
    
    Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
    definition") recognize data dependencies only when they flow through an
    intermediate local variable.  Since the dependency in P1 doesn't, those
    versions get the wrong answer for this test.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 0000000..673eec9
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus
@@ -0,0 +1,29 @@
+C LB+mb+data.litmus
+(*
+ * LB plus crypto-mb-data plus data.
+ *
+ * Result: Never
+ *
+ * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
+ * definition") recognize data dependencies only when they flow through
+ * an intermediate local variable.  Since the dependency in P1 doesn't,
+ * those versions get the wrong answer for this test.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_mb();
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Tue, Oct 06, 2020 at 09:39:54AM -0700, Paul E. McKenney wrote:
> On Mon, Oct 05, 2020 at 03:48:34PM -0400, Alan Stern wrote:
> > On Mon, Oct 05, 2020 at 12:18:01PM -0700, Paul E. McKenney wrote:
> > > Aside from naming and comment, how about my adding the following?
> > > 
> > > 							Thanx, Paul
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > C crypto-control-data-1
> > 
> > Let's call it something more along the lines of 
> > dependencies-in-nested-expressions.  Maybe you can think of something a 
> > little more succinct, but that's the general idea of the test.
> > 
> > > (*
> > >  * LB plus crypto-mb-data plus data.
> > 
> > The actual pattern is LB+mb+data.
> > 
> > >  *
> > >  * Result: Never
> > >  *
> > >  * This is an example of OOTA and we would like it to be forbidden.
> > >  * If you want herd7 to get the right answer, you must use herdtools
> > >  * 0f3f8188a326 (" [herd] Fix dependency definition") or later.
> > 
> > Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency 
> > definition") recognize data dependencies only when they flow through an 
> > intermediate local variable.  Since the dependency in P1 doesn't, those
> > versions get the wrong answer for this test.
> > 
> > >  *)
> > > 
> > > {}
> > > 
> > > P0(int *x, int *y)
> > > {
> > > 	int r1;
> > > 
> > > 	r1 = READ_ONCE(*x);
> > > 	smp_mb();
> > > 	WRITE_ONCE(*y, r1);
> > > }
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	int r2;
> > 
> > No need for r2.
> 
> Thank you for looking this over!
> 
> Like this, then?
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit 51898676302d8ebc93856209f7c587f1ac0fdd11
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Tue Oct 6 09:38:37 2020 -0700
> 
>     manual/kernel: Add LB+mb+data litmus test
>     
>     Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
>     definition") recognize data dependencies only when they flow through an
>     intermediate local variable.  Since the dependency in P1 doesn't, those
>     versions get the wrong answer for this test.

Shouldn't the commit message be different from the actual contents of 
the update?  It's supposed to explain why the update was made, not just 
say what it does.  How about this:

Test whether herd7 can detect a data dependency when there is no 
intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).  
Commit 0f3f8188a326 fixed an oversight which caused such dependencies 
to be missed.

>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
> new file mode 100644
> index 0000000..673eec9
> --- /dev/null
> +++ b/manual/kernel/C-LB+mb+data.litmus
> @@ -0,0 +1,29 @@
> +C LB+mb+data.litmus

Do you normally put ".litmus" at the end of test names?  I leave it out, 
including it only in the filename.

> +(*
> + * LB plus crypto-mb-data plus data.

As I said earlier, the actual pattern is LB+mb+data.  There's nothing 
"crypto" about this litmus test (for example, no control dependencies).

Besides, it hardly seems worthwhile making the first comment line a 
repeat of the test name immediately above it.  Just leave it out.

> + *
> + * Result: Never
> + *
> + * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
> + * definition") recognize data dependencies only when they flow through
> + * an intermediate local variable.  Since the dependency in P1 doesn't,
> + * those versions get the wrong answer for this test.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = READ_ONCE(*x);
> +	smp_mb();
> +	WRITE_ONCE(*y, r1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	WRITE_ONCE(*x, READ_ONCE(*y));
> +}
> +
> +exists (0:r1=1)

Otherwise okay.

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Tue, Oct 06, 2020 at 01:05:25PM -0400, Alan Stern wrote:
> On Tue, Oct 06, 2020 at 09:39:54AM -0700, Paul E. McKenney wrote:
> > On Mon, Oct 05, 2020 at 03:48:34PM -0400, Alan Stern wrote:
> > > On Mon, Oct 05, 2020 at 12:18:01PM -0700, Paul E. McKenney wrote:
> > > > Aside from naming and comment, how about my adding the following?
> > > > 
> > > > 							Thanx, Paul
> > > > 
> > > > ------------------------------------------------------------------------
> > > > 
> > > > C crypto-control-data-1
> > > 
> > > Let's call it something more along the lines of 
> > > dependencies-in-nested-expressions.  Maybe you can think of something a 
> > > little more succinct, but that's the general idea of the test.
> > > 
> > > > (*
> > > >  * LB plus crypto-mb-data plus data.
> > > 
> > > The actual pattern is LB+mb+data.
> > > 
> > > >  *
> > > >  * Result: Never
> > > >  *
> > > >  * This is an example of OOTA and we would like it to be forbidden.
> > > >  * If you want herd7 to get the right answer, you must use herdtools
> > > >  * 0f3f8188a326 (" [herd] Fix dependency definition") or later.
> > > 
> > > Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency 
> > > definition") recognize data dependencies only when they flow through an 
> > > intermediate local variable.  Since the dependency in P1 doesn't, those
> > > versions get the wrong answer for this test.
> > > 
> > > >  *)
> > > > 
> > > > {}
> > > > 
> > > > P0(int *x, int *y)
> > > > {
> > > > 	int r1;
> > > > 
> > > > 	r1 = READ_ONCE(*x);
> > > > 	smp_mb();
> > > > 	WRITE_ONCE(*y, r1);
> > > > }
> > > > 
> > > > P1(int *x, int *y)
> > > > {
> > > > 	int r2;
> > > 
> > > No need for r2.
> > 
> > Thank you for looking this over!
> > 
> > Like this, then?
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit 51898676302d8ebc93856209f7c587f1ac0fdd11
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Tue Oct 6 09:38:37 2020 -0700
> > 
> >     manual/kernel: Add LB+mb+data litmus test
> >     
> >     Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
> >     definition") recognize data dependencies only when they flow through an
> >     intermediate local variable.  Since the dependency in P1 doesn't, those
> >     versions get the wrong answer for this test.
> 
> Shouldn't the commit message be different from the actual contents of 
> the update?  It's supposed to explain why the update was made, not just 
> say what it does.  How about this:
> 
> Test whether herd7 can detect a data dependency when there is no 
> intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).  
> Commit 0f3f8188a326 fixed an oversight which caused such dependencies 
> to be missed.

Much better, thank you!  I added "in herdtools" just in case someone was
confused enough to look for this commit in the Linux kernel or some such.
Which I should have done more explicitly in the original, to be sure.

> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
> > new file mode 100644
> > index 0000000..673eec9
> > --- /dev/null
> > +++ b/manual/kernel/C-LB+mb+data.litmus
> > @@ -0,0 +1,29 @@
> > +C LB+mb+data.litmus
> 
> Do you normally put ".litmus" at the end of test names?  I leave it out, 
> including it only in the filename.

No, I don't, and thank you for catching this.

> > +(*
> > + * LB plus crypto-mb-data plus data.
> 
> As I said earlier, the actual pattern is LB+mb+data.  There's nothing 
> "crypto" about this litmus test (for example, no control dependencies).
> 
> Besides, it hardly seems worthwhile making the first comment line a 
> repeat of the test name immediately above it.  Just leave it out.

Done!  ;-)

> > + *
> > + * Result: Never
> > + *
> > + * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
> > + * definition") recognize data dependencies only when they flow through
> > + * an intermediate local variable.  Since the dependency in P1 doesn't,
> > + * those versions get the wrong answer for this test.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = READ_ONCE(*x);
> > +	smp_mb();
> > +	WRITE_ONCE(*y, r1);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > +}
> > +
> > +exists (0:r1=1)
> 
> Otherwise okay.

And here is the updated version.

							Thanx, Paul

------------------------------------------------------------------------

commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Tue Oct 6 09:38:37 2020 -0700

    manual/kernel: Add LB+mb+data litmus test
    
    Test whether herd7 can detect a data dependency when there is no
    intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
    Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
    dependencies to be missed.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 0000000..0cf9a7a
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus
@@ -0,0 +1,27 @@
+C LB+mb+data
+(*
+ * Result: Never
+ *
+ * Test whether herd7 can detect a data dependency when there is no
+ * intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
+ * Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
+ * dependencies to be missed.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_mb();
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> And here is the updated version.
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Tue Oct 6 09:38:37 2020 -0700
> 
>     manual/kernel: Add LB+mb+data litmus test

Let's change this to:

      manual/kernel: Add LB data dependency test with no intermediate variable

Without that extra qualification, people reading just the title would
wonder why we need a simple LB litmus test in the archive.

>     
>     Test whether herd7 can detect a data dependency when there is no
>     intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
>     Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
>     dependencies to be missed.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
> new file mode 100644
> index 0000000..0cf9a7a
> --- /dev/null
> +++ b/manual/kernel/C-LB+mb+data.litmus
> @@ -0,0 +1,27 @@
> +C LB+mb+data
> +(*
> + * Result: Never
> + *
> + * Test whether herd7 can detect a data dependency when there is no
> + * intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
> + * Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
> + * dependencies to be missed.

You changed this comment!  It should have remained the way it was:

+ * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
+ * definition") recognize data dependencies only when they flow through
+ * an intermediate local variable.  Since the dependency in P1 doesn't,
+ * those versions get the wrong answer for this test.

> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = READ_ONCE(*x);
> +	smp_mb();
> +	WRITE_ONCE(*y, r1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	WRITE_ONCE(*x, READ_ONCE(*y));
> +}
> +
> +exists (0:r1=1)

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Wed, Oct 07, 2020 at 03:40:50PM -0400, Alan Stern wrote:
> On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> > And here is the updated version.
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Tue Oct 6 09:38:37 2020 -0700
> > 
> >     manual/kernel: Add LB+mb+data litmus test
> 
> Let's change this to:
> 
>       manual/kernel: Add LB data dependency test with no intermediate variable
> 
> Without that extra qualification, people reading just the title would
> wonder why we need a simple LB litmus test in the archive.
> 
> >     
> >     Test whether herd7 can detect a data dependency when there is no
> >     intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
> >     Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
> >     dependencies to be missed.
> >     
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
> > new file mode 100644
> > index 0000000..0cf9a7a
> > --- /dev/null
> > +++ b/manual/kernel/C-LB+mb+data.litmus
> > @@ -0,0 +1,27 @@
> > +C LB+mb+data
> > +(*
> > + * Result: Never
> > + *
> > + * Test whether herd7 can detect a data dependency when there is no
> > + * intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
> > + * Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
> > + * dependencies to be missed.
> 
> You changed this comment!  It should have remained the way it was:

I might get this right sooner or later.  You never know.

Like this?

							Thanx, Paul

------------------------------------------------------------------------

commit 5b6a4ff2c8ad25fc77f4151e71e6cbd8f3268d7b
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Tue Oct 6 09:38:37 2020 -0700

    manual/kernel: Add LB+mb+data litmus test
    
    Test whether herd7 can detect a data dependency when there is no
    intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
    Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
    dependencies to be missed.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 0000000..e9e24e0
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus
@@ -0,0 +1,27 @@
+C LB+mb+data
+(*
+ * Result: Never
+ *
+ * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
+ * definition") recognize data dependencies only when they flow through
+ * an intermediate local variable.  Since the dependency in P1 doesn't,
+ * those versions get the wrong answer for this test.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_mb();
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Wed, Oct 07, 2020 at 03:38:51PM -0700, Paul E. McKenney wrote:
> On Wed, Oct 07, 2020 at 03:40:50PM -0400, Alan Stern wrote:
> > On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> > > And here is the updated version.
> > > 
> > > 							Thanx, Paul
> > > 
> > > ------------------------------------------------------------------------
> > > 
> > > commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> > > Author: Alan Stern <stern@rowland.harvard.edu>
> > > Date:   Tue Oct 6 09:38:37 2020 -0700
> > > 
> > >     manual/kernel: Add LB+mb+data litmus test
> > 
> > Let's change this to:
> > 
> >       manual/kernel: Add LB data dependency test with no intermediate variable
> > 
> > Without that extra qualification, people reading just the title would
> > wonder why we need a simple LB litmus test in the archive.

> I might get this right sooner or later.  You never know.
> 
> Like this?
> 
> 							Thanx, Paul

Paul, I think you must need new reading glasses.  You completely missed 
the text above.

Alan

> ------------------------------------------------------------------------
> 
> commit 5b6a4ff2c8ad25fc77f4151e71e6cbd8f3268d7b
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Tue Oct 6 09:38:37 2020 -0700
> 
>     manual/kernel: Add LB+mb+data litmus test
>     
>     Test whether herd7 can detect a data dependency when there is no
>     intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
>     Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
>     dependencies to be missed.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Wed, Oct 07, 2020 at 10:25:37PM -0400, Alan Stern wrote:
> On Wed, Oct 07, 2020 at 03:38:51PM -0700, Paul E. McKenney wrote:
> > On Wed, Oct 07, 2020 at 03:40:50PM -0400, Alan Stern wrote:
> > > On Wed, Oct 07, 2020 at 10:50:40AM -0700, Paul E. McKenney wrote:
> > > > And here is the updated version.
> > > > 
> > > > 							Thanx, Paul
> > > > 
> > > > ------------------------------------------------------------------------
> > > > 
> > > > commit b7cd60d4b41ad56b32b36b978488f509c4f7e228
> > > > Author: Alan Stern <stern@rowland.harvard.edu>
> > > > Date:   Tue Oct 6 09:38:37 2020 -0700
> > > > 
> > > >     manual/kernel: Add LB+mb+data litmus test
> > > 
> > > Let's change this to:
> > > 
> > >       manual/kernel: Add LB data dependency test with no intermediate variable
> > > 
> > > Without that extra qualification, people reading just the title would
> > > wonder why we need a simple LB litmus test in the archive.
> 
> > I might get this right sooner or later.  You never know.
> > 
> > Like this?
> > 
> > 							Thanx, Paul
> 
> Paul, I think you must need new reading glasses.  You completely missed 
> the text above.

There are some distractions at the moment.

Please see below.  If this is not exactly correct, I will use "git rm"
and let you submit the patch as you wish.

						Thanx, Paul

------------------------------------------------------------------------

commit dc0119c24b64f9d541b94ba5d17eec0cbc265bfa
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Tue Oct 6 09:38:37 2020 -0700

    manual/kernel: Add LB data dependency test with no intermediate variable
    
    Test whether herd7 can detect a data dependency when there is no
    intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
    Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
    dependencies to be missed.
    
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
new file mode 100644
index 0000000..e9e24e0
--- /dev/null
+++ b/manual/kernel/C-LB+mb+data.litmus
@@ -0,0 +1,27 @@
+C LB+mb+data
+(*
+ * Result: Never
+ *
+ * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
+ * definition") recognize data dependencies only when they flow through
+ * an intermediate local variable.  Since the dependency in P1 doesn't,
+ * those versions get the wrong answer for this test.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+
+	r1 = READ_ONCE(*x);
+	smp_mb();
+	WRITE_ONCE(*y, r1);
+}
+
+P1(int *x, int *y)
+{
+	WRITE_ONCE(*x, READ_ONCE(*y));
+}
+
+exists (0:r1=1)

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Alan Stern]

On Wed, Oct 07, 2020 at 07:50:25PM -0700, Paul E. McKenney wrote:
> There are some distractions at the moment.
> 
> Please see below.  If this is not exactly correct, I will use "git rm"
> and let you submit the patch as you wish.
> 
> 						Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit dc0119c24b64f9d541b94ba5d17eec0cbc265bfa
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Tue Oct 6 09:38:37 2020 -0700
> 
>     manual/kernel: Add LB data dependency test with no intermediate variable
>     
>     Test whether herd7 can detect a data dependency when there is no
>     intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
>     Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
>     dependencies to be missed.
>     
>     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> 
> diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
> new file mode 100644
> index 0000000..e9e24e0
> --- /dev/null
> +++ b/manual/kernel/C-LB+mb+data.litmus
> @@ -0,0 +1,27 @@
> +C LB+mb+data
> +(*
> + * Result: Never
> + *
> + * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
> + * definition") recognize data dependencies only when they flow through
> + * an intermediate local variable.  Since the dependency in P1 doesn't,
> + * those versions get the wrong answer for this test.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +
> +	r1 = READ_ONCE(*x);
> +	smp_mb();
> +	WRITE_ONCE(*y, r1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	WRITE_ONCE(*x, READ_ONCE(*y));
> +}
> +
> +exists (0:r1=1)

Okay, that's exactly what it should be.  :-)

Alan

Re: Bug in herd7 [Was: Re: Litmus test for question from Al Viro]

[Paul E. McKenney]

On Thu, Oct 08, 2020 at 10:01:48AM -0400, Alan Stern wrote:
> On Wed, Oct 07, 2020 at 07:50:25PM -0700, Paul E. McKenney wrote:
> > There are some distractions at the moment.
> > 
> > Please see below.  If this is not exactly correct, I will use "git rm"
> > and let you submit the patch as you wish.
> > 
> > 						Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit dc0119c24b64f9d541b94ba5d17eec0cbc265bfa
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Tue Oct 6 09:38:37 2020 -0700
> > 
> >     manual/kernel: Add LB data dependency test with no intermediate variable
> >     
> >     Test whether herd7 can detect a data dependency when there is no
> >     intermediate local variable, as in WRITE_ONCE(*x, READ_ONCE(*y)).
> >     Commit 0f3f8188a326 in herdtools fixed an oversight which caused such
> >     dependencies to be missed.
> >     
> >     Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> >     Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> > 
> > diff --git a/manual/kernel/C-LB+mb+data.litmus b/manual/kernel/C-LB+mb+data.litmus
> > new file mode 100644
> > index 0000000..e9e24e0
> > --- /dev/null
> > +++ b/manual/kernel/C-LB+mb+data.litmus
> > @@ -0,0 +1,27 @@
> > +C LB+mb+data
> > +(*
> > + * Result: Never
> > + *
> > + * Versions of herd7 prior to commit 0f3f8188a326 ("[herd] Fix dependency
> > + * definition") recognize data dependencies only when they flow through
> > + * an intermediate local variable.  Since the dependency in P1 doesn't,
> > + * those versions get the wrong answer for this test.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +
> > +	r1 = READ_ONCE(*x);
> > +	smp_mb();
> > +	WRITE_ONCE(*y, r1);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	WRITE_ONCE(*x, READ_ONCE(*y));
> > +}
> > +
> > +exists (0:r1=1)
> 
> Okay, that's exactly what it should be.  :-)

Whew!!!  ;-)

							Thanx, Paul