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 ?
