MIME-Version: 1.0
References: <20230204014941.GS2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y95yhJgNq8lMXPdF@rowland.harvard.edu> <20230204222411.GC2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y9+41ctA54pjm/KG@google.com> <Y+FJSzUoGTgReLPB@rowland.harvard.edu>
 <Y+fN2fvUjGDWBYrv@google.com> <Y+f4TYZ9BPlt8y8B@rowland.harvard.edu>
 <CAEXW_YRuTfjc=5OAskTV0Qt_zSJTPP3-01=Y=SypMdPsF_weAQ@mail.gmail.com>
 <Y+hWAksfk4C0M2gB@rowland.harvard.edu> <CAEXW_YQUOgYxYUNkQ9W6PS-JPwPSOFU5B=COV7Vf+qNF1jFC7g@mail.gmail.com>
 <Y+ob0xFUp+d7LROE@andrea>
In-Reply-To: <Y+ob0xFUp+d7LROE@andrea>
From:   Joel Fernandes <joel@joelfernandes.org>
Date:   Mon, 13 Feb 2023 19:52:27 -0500
Message-ID: <CAEXW_YRZ097Qedp+ffxvVnJGWpehAn3-3efNcrDS5YW5u5QxDA@mail.gmail.com>
Subject: Re: Current LKMM patch disposition
To:     Andrea Parri <parri.andrea@gmail.com>
Cc:     Alan Stern <stern@rowland.harvard.edu>,
        "Paul E. McKenney" <paulmck@kernel.org>,
        linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        kernel-team@meta.com, mingo@kernel.org, will@kernel.org,
        peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
        dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
        akiyks@gmail.com
Content-Type: text/plain; charset="UTF-8"
Precedence: bulk

On Mon, Feb 13, 2023 at 6:15 AM Andrea Parri <parri.andrea@gmail.com> wrote:
>
> > > Would you like to post a few examples showing some of the most difficult
> > > points you encountered?  Maybe explanation.txt can be improved.
> >
> > Just to list 2 of the pain points:
> >
> > 1. I think it is hard to reason this section
> > "PROPAGATION ORDER RELATION: cumul-fence"
> >
> > All store-related fences should affect propagation order, even the
> > smp_wmb() which is not A-cumulative should do so (po-earlier stores
> > appearing before po-later). I think expanding this section with some
> > examples would make sense to understand what makes "cumul-fence"
> > different from any other store-related fence.
>
> FWIW, litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus illustrates
> the concept of A-cumulativity.

Right, this I knew. The smp_store_release() in that test A-cumulative.
However, the "cumul-fence" naming in the document we are discussing
sounds redundant. (but I could be missing something).

> (The terminology is not LKMM-specific, it was borrowed from other MCM literature, e.g. "Understanding POWER Multiprocessors"
> in Documentation/references.txt.)

Thank you!

> > 2. This part is confusing and has always confused me " The
> > happens-before relation (hb) links memory accesses that have to
> > execute in a certain order"
> >
> > It is not memory accesses that execute, it is instructions that
> > execute. Can we separate out "memory access" from "instruction
> > execution" in this description?
> >
> > I think ->hb tries to say that A ->hb B means, memory access A
> > happened before memory access B exactly in its associated
> > instruction's execution order (time order), but to be specific --
> > should that be instruction issue order, or instruction retiring order?
> >
> > AFAICS ->hb maps instruction execution order to memory access order.
> > Not all ->po does  fall into that category because of out-of-order
> > hardware execution. As does not ->co because the memory subsystem may
> > have writes to the same variable to be resolved out of order. It would
> > be nice to call out that ->po is instruction issue order, which is
> > different from execution/retiring and that's why it cannot be ->hb.
> >
> > ->rf does because of data flow causality, ->ppo does because of
> > program structure, so that makes sense to be ->hb.
> >
> > IMHO, ->rfi should as well, because it is embodying a flow of data, so
> > that is a bit confusing. It would be great to clarify more perhaps
> > with an example about why ->rfi cannot be ->hb, in the
> > "happens-before" section.
> >
> > That's really how far I typically get (line 1368) before life takes
> > over, and I have to go do other survival-related things. Then I
> > restart the activity. Now that I started reading the CAT file as well,
> > I feel I can make it past that line :D. But I never wanted to get past
> > it, till I built a solid understanding of the contents before it.
> >
> > As I read the file more, I can give more feedback, but the above are
> > different 2 that persist.
>
> AFAICT, sections "The happens-before relation: hb" and "An operational model"
> in Documentation/explanation.txt elaborate (should help) clarify such issues.
> About the ->rfi example cf. e.g. Test PPOCA in the above mentioned paper; the
> test remains allowed in arm64 and riscv.

Thank you, this clarifies a lot and appears there is already a similar
relation mentioned in the explanation.txt as Alan pointed. This paper
is great to clarify the concept -- appreciate!.  I wonder what other
ordering 'havocs' do processor branch speculation cause.  This should
imply load-load control dependency is also subject to reordering on
these architectures.

thanks,

  - Joel