Re: [RFC] tools/memory-model: Rule out OOTA

[Jonas Oberhauser]

Am 1/6/2025 um 10:40 PM schrieb Jonas Oberhauser:>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx>
> ---
>   tools/memory-model/linux-kernel.cat | 6 +++++-
>   1 file changed, 5 insertions(+), 1 deletion(-)
>
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index d7e7bf13c831..180cab56729e 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -71,6 +71,10 @@ let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
>   		Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
>   	(po ; [Release]) | ([Acquire] ; po)
>   
> +let w_barrier = po? ; [F | Marked] ; po?
> +let rmb-plain = [R4rmb] ; po ; [Rmb] ; (po \ (po ; [W] ; (po-loc \ w_barrier))) ; [R4rmb & Plain]
> +let plain-wmb = [W & Plain] ; (po \ ((po-loc \ w_barrier) ; po ; [W] ; po)) ; [Wmb] ; po ; [W]
> +
>   (**********************************)
>   (* Fundamental coherence ordering *)
>   (**********************************)
> @@ -90,7 +94,7 @@ empty rmw & (fre ; coe) as atomic
>   let dep = addr | data
>   let rwdep = (dep | ctrl) ; [W]
>   let overwrite = co | fr
> -let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
> +let to-w = ((addr | rmb-plain)? ; rwdep ; plain-wmb?) | (overwrite & int) | addr ; [Plain] ; wmb
>   let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi)
>   let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int)
>   

I will also try to give an intuitive :) :( :) reasoning for why this 
patch rules out OOTA.

If we look at an dep ; rfe cycle

  dep ; rfe ; dep ; rfe ; ...


then because of the absence of data races, each rfe is more or less an

  w-post-bounded ; rfe ; r-pre-bounded

edge.

If we rotate the circle around we turn

  dep ; w-post-bounded ; rfe ; r-pre-bounded ; dep ; w-post-bounded ; 
rfe ; r-pre-bounded ; ...

into

   rfe ; (r-pre-bounded ; dep ; w-post-bounded) ; rfe ; (r-pre-bounded 
; dep ; w-post-bounded) ; rfe ; (r-pre-bounded ; ...


and ideally, each of these (w-pre-bounded ; dep ; r-post-bounded) would 
imply happens-before, since then the cycle would be.
   rfe ; hb+; rfe; hb+ ; ...
which is acyclic.

However, we do not get hb+ in general, in particular if the bounding is 
due to rmb/wmb. For all other cases, it is relatively easy to see that 
we get hb+, e.g., if the bound is due to an smp_mb().

Luckily, in our specific case, we can get hb+ evenfor cases where 
rmb/wmb bound these accesses, because these accesses related by the dep 
edges are known to be reading/read-from externally.
Such an external interaction would be impossible if there were another 
store to the same location between such an access and the next 
w_barrier: because of the absence of data races and the lack of 
w_barriers that would allow synchronization with the outside world, the 
external event could not "occur between" the access and such a store.

As a result, all pre-bounds caused by a rmb must have the form

[R4rmb] ; po ; [Rmb] ; (po \ (po ; [W] ; (po-loc \ w_barrier))) ; [R4rmb 
& Plain]

and similar for post-bounds caused by wmb, which means the corresponding

   r-pre-bounded ; dep ; w-post-bounded

edges must be

   rmb-plain ; dep ; plain-wmb

which is in ppo and thus also hb.

Hope that helps clarify the idea...

  jonas