Re: [PATCH v5 03/10] rust: sync: atomic: Add ordering annotation types

[Alan Stern <stern@rowland.harvard.edu>]

On Thu, Jun 19, 2025 at 08:00:30AM -0700, Boqun Feng wrote:
> Make sense, so something like this in the model should work:
> 
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index d7e7bf13c831..90cb6db6e335 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -27,7 +27,7 @@ include "lock.cat"
>  (* Release Acquire *)
>  let acq-po = [Acquire] ; po ; [M]
>  let po-rel = [M] ; po ; [Release]
> -let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po
> +let po-unlock-lock-po = po ; (([UL] ; (po|rf) ; [LKR]) | ([Release]; (po;rf); [Acquire & RMW])) ; po
> 
>  (* Fences *)
>  let R4rmb = R \ Noreturn       (* Reads for which rmb works *)
> 
> 
> although I'm not sure whether there will be actual users that use this
> ordering.

If we do end up making a change like this then we should also start 
keeping careful track of the parts of the LKMM that are not justified by 
the operational model (and vice versa), perhaps putting something about 
them into the documentation.  As far as I can remember, 
po-unlock-lock-po is the only current example, but my memory isn't 
always the greatest -- just one reason why it would be good to have 
these things written down in an organized manner.

Alan