Re: [RFC] tools/memory-model: Rule out OOTA

On Fri, Jan 17, 2025 at 05:45:50PM +0100, Jonas Oberhauser wrote:
> 
> 
> Am 1/17/2025 um 4:52 PM schrieb Alan Stern:
> > On Thu, Jan 16, 2025 at 06:02:18PM -0500, Alan Stern wrote:
> > > On Thu, Jan 16, 2025 at 08:08:22PM +0100, Jonas Oberhauser wrote:
> > This is a slight variation of the example on page 19 (section 4.3) of
> > the paper.  (Pretend this is actually C++ code, the shared variables are
> > all atomic, and their accesses are all relaxed.)
> > 
> > bool x, y, z;
> > 
> > void P0(bool *x, bool *y, bool *z) {
> > 	bool r1, r2;
> > 
> > 	r1 = *x;
> > 	r2 = *y;
> > 
> > 	*z = (r1 != r2);
> > }
> > 
> > The paper points out that although there is an apparent semantic
> > dependency from the load of x to the store to z, if the compiler is
> > allowed not to handle atomics as quasi volatile then the dependency
> > can be broken.  Nevertheless, I am not able to think of a program that
> > could exhibit OOTA as a result of breaking the semantic dependency.  The
> > best I can come up with is this:
> > 
> > [P0 as above]
> > 
> > void P1(bool *x, bool *y, bool *z) {
> > 	bool r3;
> > 
> > 	r3 = z;
> > 	x = r3;
> > }
> > 
> > void P2(bool *x, bool *y, bool *z) {
> > 	y = true;
> > }
> > 
> > exists (x=true /\ z=true)
> > 
> > If P2 were not present, this result could not occur in any physical
> > execution, even if the dependency in P0 is broken.  With P2 this result
> > isn't OOTA, even in executions where P0 ends up storing z before loading
> > x, because P2 could have executed first, then P0, then P1.
> > 
> > So perhaps this is an example of what you were talking about -- a
> > dependency which may or may not be semantic, but either way cannot lead
> > to OOTA.
> 
> Yes, that looks like an example of what I have in mind.
> 
> If at the model level we just say "yes there is a dependency, but no it does
> not give any ordering guarantee", then the compiler is still free to break
> the dependency like in your example.
> 
> A thread P3 { r1 = z; atomic_thread_fence(); r2 = y; }
> could still observe r2 == false, r1 == true, "showing" that the dependency
> was broken.

That wouldn't prove anything unless P0 had its own memory barrier 
somewhere before it stored z.

At any rate, I don't have any ideas on how to characterize semantic 
dependencies that can be broken without risking OOTA.  (Some people 
would say that if a dependency can be broken at all, that demonstrates 
it wasn't semantic to begin with.)

Alan