Re: [PATCH] Linux: Implement membarrier function

[David Goldblatt <davidtgoldblatt at gmail dot com>]

One note with the suggested patch is that
`atomic_thread_fence(memory_order_acq_rel)` should probably be
`atomic_thread_fence (memory_order_seq_cst)` (otherwise the call would
be a no-op on, say, x86, which it very much isn't).

The non-transitivity thing makes the resulting description arguably
incorrect, but this is informal enough that it might not be a big deal
to add something after "For these threads, the membarrier function
call turns an existing compiler barrier (see above) executed by these
threads into full memory barriers" that clarifies it. E.g. you could
make it into "turns an existing compiler barrier [...] into full
memory barriers, with respect to the calling thread".

Since this is targeting the description of the OS call (and doesn't
have to concern itself with also being implementable by other
asymmetric techniques or degrading to architectural barriers), I think
that the description in "approach 2" in P1202 would also make sense
for a formal description of the syscall. (Of course, without the
kernel itself committing to a rigorous semantics, anything specified
on top of it will be on slightly shaky ground).

- David

On Thu, Nov 29, 2018 at 7:04 AM Paul E. McKenney <paulmck@linux.ibm.com> wrote:
>
> On Thu, Nov 29, 2018 at 09:44:22AM -0500, Mathieu Desnoyers wrote:
> > ----- On Nov 29, 2018, at 8:50 AM, Florian Weimer fweimer@redhat.com wrote:
> >
> > > * Torvald Riegel:
> > >
> > >> On Wed, 2018-11-28 at 16:05 +0100, Florian Weimer wrote:
> > >>> This is essentially a repost of last year's patch, rebased to the glibc
> > >>> 2.29 symbol version and reflecting the introduction of
> > >>> MEMBARRIER_CMD_GLOBAL.
> > >>>
> > >>> I'm not including any changes to manual/ here because the set of
> > >>> supported operations is evolving rapidly, we could not get consensus for
> > >>> the language I proposed the last time, and I do not want to contribute
> > >>> to the manual for the time being.
> > >>
> > >> Fair enough.  Nonetheless, can you summarize how far you're along with
> > >> properly defining the semantics (eg, based on the C/C++ memory model)?
> > >
> > > I wrote down what you could, but no one liked it.
> > >
> > > <https://sourceware.org/ml/libc-alpha/2017-12/msg00796.html>
> > >
> > > I expect that a formalization would interact in non-trivial ways with
> > > any potential formalization of usable relaxed memory order semantics,
> > > and I'm not sure if anyone knows how to do the latter today.
> >
> > Adding Paul E. McKenney in CC.
>
> There is some prototype C++ memory model wording from David Goldblatt (CCed)
> here (search for "Standarese"):
>
> http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1202r0.pdf
>
> David's key insight is that (in Linuxese) light fences cannot pair with
> each other.
>
>                                                         Thanx, Paul
>