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

Andrea Parri
2023-01-29T17:11:24Z

> 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().

Andrea