lkml.org 
[lkml]   [2023]   [Jan]   [29]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po
> 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

\
 
 \ /
  Last update: 2023-03-27 00:01    [W:0.134 / U:0.220 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site