tools/memory-model: Distinguish between syntactic and semantic tags
authorJonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Tue, 5 Nov 2024 16:48:58 +0000 (17:48 +0100)
committerPaul E. McKenney <paulmck@kernel.org>
Tue, 25 Feb 2025 18:17:39 +0000 (10:17 -0800)
commitdcc5197839f22655951056f399061872adfdb0b9
tree5d80596a076d2ae57667a43e6b95c349f97758da
parentfafa180683591f5f917bfa68e95aae463afc852a
tools/memory-model: Distinguish between syntactic and semantic tags

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
tools/memory-model/Documentation/herd-representation.txt
tools/memory-model/linux-kernel.bell
tools/memory-model/linux-kernel.def