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

From: Alan Stern
Date: Fri Jan 17 2025 - 14:02:46 EST


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