Re: [PATCH memory-model 7/7] tools/memory-model: Distinguish between syntactic and semantic tags

[Akira Yokosawa <akiyks@gmail.com>]

On Thu, 20 Feb 2025 08:14:03 -0800, Paul E. McKenney wrote:
> From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> 
> Not all annotated accesses provide the semantics their syntactic tags
> would imply. For example, an 'acquire tag on a write does not imply that
> the write is finally in the Acquire set and provides acquire ordering.
> 
> To distinguish in those cases between the syntactic tags and actual
> sets, we capitalize the former, so 'ACQUIRE tags may be present on both
> reads and writes, but only reads will appear in the Acquire set.
> 
> For tags where the two concepts are the same we do not use specific
> capitalization to make this distinction.
> 
> Reported-by: Boqun Feng <boqun.feng@gmail.com>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
> Tested-by: Boqun Feng <boqun.feng@gmail.com>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

Tested-by: Akira Yokosawa <akiyks@gmail.com> # herdtools7.7.58

> ---
>  .../Documentation/herd-representation.txt     |  44 ++--
>  tools/memory-model/linux-kernel.bell          |  22 +-
>  tools/memory-model/linux-kernel.def           | 198 +++++++++---------
>  3 files changed, 132 insertions(+), 132 deletions(-)