linux-kernel - Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe link

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives
Hash Suite: Windows password security audit tool. GUI, reports in PDF.
[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Date:   Mon, 29 Jul 2019 08:17:45 -0400
From:   Joel Fernandes <joel@...lfernandes.org>
To:     Boqun Feng <boqun.feng@...il.com>
Cc:     Alan Stern <stern@...land.harvard.edu>,
        linux-kernel@...r.kernel.org, kernel-team@...roid.com,
        Akira Yokosawa <akiyks@...il.com>,
        Andrea Parri <andrea.parri@...rulasolutions.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Ingo Molnar <mingo@...nel.org>,
        Jade Alglave <j.alglave@....ac.uk>, linux-arch@...r.kernel.org,
        Luc Maranget <luc.maranget@...ia.fr>,
        Nicholas Piggin <npiggin@...il.com>,
        "Paul E. McKenney" <paulmck@...ux.ibm.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will@...nel.org>
Subject: Re: [PATCH v2] lkmm/docs: Correct ->prop example with additional rfe
 link

On Mon, Jul 29, 2019 at 01:50:44PM +0800, Boqun Feng wrote:
> On Sun, Jul 28, 2019 at 11:35:44AM -0400, Joel Fernandes wrote:
> [...]
> > > > > > +load of y (rfe link), P2's smp_store_release() ensures that P2's load
> > > > > > +of y executes before P2's store to z (second fence), which implies that
> > > > > > +that stores to x and y propagate to P2 before the smp_store_release(), which
> > > > > > +means that P2's smp_store_release() will propagate stores to x and y to all
> > > > > > +CPUs before the store to z propagates (A-cumulative property of this fence).
> > > > > > +Finally P0's load of z executes after P2's store to z has propagated to
> > > > > > +P0 (rfe link).
> > > > > 
> > > > > Again, a better change would be simply to replace the two instances of
> > > > > "fence" in the original text with "cumul-fence".
> > > > 
> > > > Ok that's fine. But I still feel the rfe is not a part of the cumul-fence.
> > > > The fences have nothing to do with the rfe. Or, I am missing something quite
> > > > badly.
> > > > 
> > > > Boqun, did you understand what Alan is saying?
> > > > 
> > > 
> > > I think 'cumul-fence' that Alan mentioned is not a fence, but a
> > > relation, which could be the result of combining a rfe relation and a
> > > A-cumulative fence relation. Please see the section "PROPAGATION ORDER
> > > RELATION: cumul-fence" or the definition of cumul-fence in
> > > linux-kernel.cat.
> > > 
> > > Did I get you right, Alan? If so, your suggestion is indeed a better
> > > change.
> > 
> > To be frank, I don't think it is better if that's what Alan meant. It is
> > better to be explicit about the ->rfe so that the reader walking through the
> > example can clearly see the ordering and make sense of it.
> > 
> > Just saying 'cumul-fence' and then hoping the reader sees the light is quite
> > a big assumption and makes the document less readable.
> > 
> 
> After a bit more rereading of the document, I still think Alan's way is
> better ;-)

I think I finally understood. What I was missing was this definition of
cumul-fence involves an rf relation (with writes being possibly on different
CPUs).

E ->cumul-fence F
	F is a release fence and some X comes before F in program order,
	where either X = E or else E ->rf X; or

So I think what Alan meant is there is a cumul-fence between y=1 and z=1
because fo the ->rfe of y. Thus making it not necessary to mention the rfe.

Labeling E and F in the example...

	P1()
	{
		WRITE_ONCE(x, 2);
		smp_wmb();
		WRITE_ONCE(y, 1);		// This is E
	}

	P2()
	{
		int r2;

		r2 = READ_ONCE(y);		// This is X
		smp_store_release(&z, 1);	// This is F
	}

Here, E ->rf X ->release-fence -> F
implies,
      E ->cumul-fence F

Considering that, I agree with Alan's suggestion.

> 
> 	The formal definition of the prop relation involves a coe or
> 	fre link, followed by an arbitrary number of cumul-fence links,
> 	ending with an rfe link.
> 
> , so using "cumul-fence" actually matches the definition of ->prop.
> 
> For the ease of readers, I can think of two ways:
> 
> 1.	Add a backwards reference to cumul-fence section here, right
> 	before using its name.

Instead of that, a reference to the fact that the rfe causes a cumul-fence
between y=1 and z=1 may be helpful. No need backward reference IMO.

> 2.	Use "->cumul-fence" notation rather than "cumul-fence" here,
> 	i.e. add an arrow "->" before the name to call it out that name
> 	"cumul-fence" here stands for links/relations rather than a
> 	fence/barrier. Maybe it's better to convert all references to 
> 	links/relations to the "->" notations in the whole doc.

No, it is a fence that causes the relation in this example.

I don't think there is a distinction between ->cumul-fence and cumul-fence at
least for this example. The smp_store_release() is a FENCE which in this
example is really a cumul-fence between y=1 and z=1 because the release fence
affects propogation order of y and z on all CPUs. For any given CPU, y
propagates to that CPU before z does, even though y and z executed on
different CPUs.

I think what you're talking about is some other definition of cumul-fence
that is not mentioned in the formal definitions. May be you can update the
document with such definition then? AFAIU, cumul-fence is always a fence.

thanks,

 - Joel