linux-kernel - Re: Documentation for plain accesses and data races

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 for Android: free password hash cracker in your pocket

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <20190916164246.GA7098@tardis>
Date:   Tue, 17 Sep 2019 00:42:46 +0800
From:   Boqun Feng <boqun.feng@...il.com>
To:     Alan Stern <stern@...land.harvard.edu>
Cc:     LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>,
        Andrea Parri <parri.andrea@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        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>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: Documentation for plain accesses and data races

On Mon, Sep 16, 2019 at 11:22:18AM -0400, Alan Stern wrote:
> On Mon, 16 Sep 2019, Boqun Feng wrote:
> 
> > > executes if Y is a store.)  This is expressed by the visibility
> > > relation (vis), where X ->vis Y is defined to hold if there is an
> > > intermediate event Z such that:
> > > 
> > > 	X is connected to Z by a possibly empty sequence of
> > > 	cumul-fence links followed by an optional rfe link (if none of
> > > 	these links are present, X and Z are the same event),
> > > 
> > 
> > I wonder whehter we could add an optional ->coe or ->fre between X and
> > the possibly empty sequence of cumul-fence, smiliar to the definition
> > of ->prop. This makes sense because if we have
> > 
> > 	X ->coe X' (and X' in on CPU C)
> > 
> > , X must be already propagated to C before X' executed, according to our
> > operation model:
> > 
> > "... In particular, it must arrange for the store to be co-later than
> > (i.e., to overwrite) any other store to the same location which has
> > already propagated to CPU C."
> 
> You have misinterpreted the text.  The operational model says that if X 
> propagates to CPU C before X' executes then X ->coe X'.  It does _not_ 
> say that if X ->coe X' then X propagates to CPU C before X' executes.
> 

Alright, I got confused. If X ->coe X', we only have "X must execute
before X' propagated to the CPU of X" (otherwise, we will have X' ->coe
X), so we will only know the execution time of X (not the propagation
time) is before the propagation of X' to the CPU of X, and that won't
help build the visiblity, because we know zero about the propagation
time of X to any CPU.

> > In other words, we can define ->vis as:
> > 
> > 	let vis = prop ; ((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
> > 
> > , and for this document, reference the "prop" section in
> > explanation.txt. This could make the model simple (both for description
> > and explanation), and one better thing is that we won't need commit in
> > Paul's dev branch:
> > 	
> > 	c683f2c807d2 "tools/memory-model: Fix data race detection for unordered store and load"
> > 
> > , and data race rules will look more symmetrical ;-)
> > 
> > Thoughts? Or am I missing something subtle here?
> 
> See above.
> 

Thanks!

Regards,
Boqun

> Alan
> 

Download attachment "signature.asc" of type "application/pgp-signature" (489 bytes)