Re: [PATCH memory-model 7/7] tools/memory-model: Distinguish between syntactic and semantic tags
Akira Yokosawa <[email protected]>
| Newsgroups | dev.linux.lists.lkmm,org.kernel.vger.linux-arch,org.kernel.vger.linux-kernel |
|---|---|
| Message-ID | <[email protected]> |
On Thu, 20 Feb 2025 08:14:03 -0800, Paul E. McKenney wrote: > From: Jonas Oberhauser <[email protected]> > > 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 <[email protected]> > Signed-off-by: Jonas Oberhauser <[email protected]> > Reviewed-by: Boqun Feng <[email protected]> > Tested-by: Boqun Feng <[email protected]> > Signed-off-by: Paul E. McKenney <[email protected]> Tested-by: Akira Yokosawa <[email protected]> # 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(-)