Re: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po

Alan Stern
2023-01-29T22:10:55Z

On Sun, Jan 29, 2023 at 06:11:12PM +0100, Andrea Parri wrote:
> > The reason why Wx=1 ->ww-vis Wx=2:
> >
> > 0:Wx=1 ->po-rel 0:Wy=1 and po-rel < fence < ww-post-bounded.
> >
> > 0:Wy=1 ->rfe 1:Ry=1 ->(hb* & int) 1:Rdy=1 and
> > (rfe ; hb* & int) <= (rfe ; xbstar & int) <= vis.
> >
> > 1:Rdy=1 ->po 1:unlock ->rfe 3:lock ->po 3:Wx=2
> > so 1:Rdy=1 ->po-unlock-lock-po 3:Wx=2
> > and po-unlock-lock-po <= mb <= fence <= w-pre-bounded.
> >
> > Finally, w-post-bounded ; vis ; w-pre-bounded <= ww-vis.
>
> To clarify, po-unlock-lock-po is not a subrelation of mb; see what
> happens without the smp_mb__after_unlock_lock().

Ah, thank you again. That was what I got wrong, and it explains why the
data race appears with Jonas's patch.

This also points out an important unstated fact: All of the inter-CPU
extended fences in the memory model are A-cumulative. In this case the
fence links Rdy=1 on P1 to Wx=3 on P3. We know that 0:Wx=1 is visible
to P1 before the Rdy executes, but what we need is that it is visible to
P3 before Wx=3 executes. The fact that the extended fence is strong
(and therefore A-cumulative) provides this extra guarantee.

Alan