Messages in this thread | | | Date | Mon, 5 Oct 2020 17:35:19 +0200 | From | Peter Zijlstra <> | Subject | Re: Litmus test for question from Al Viro |
| |
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 ?
| |