[herd] Split exclusive accesses from the X event set by relokin · Pull Request #1889 · herd/herdtools7

relokin · 2026-06-29T12:23:18Z

Summary

This PR makes exclusive accesses explicit in herd by introducing a distinct EX event set instead of treating them as
part of X.

The main goal is to let CAT models distinguish reservation-based exclusive operations from other atomic/RMW events more
precisely, while also exposing reusable helpers for reasoning about RMWs.

What changed

add dedicated exclusive annotations for AArch64 (EX, EXA, EXL) and thread them through the AArch64/ASL semantics
use EX for exclusive/LR-SC style instructions in ARM, RISC-V, MIPS, and PPC
keep X separate from EX, rather than conflating all of these events in one set
extend stdlib.cat with reusable EX, lxsx, amo, and rmw helpers
update ppc-checks.cat so scXX is defined over exclusive events
remove the AArch64 A162 test which duplicates A44

Why

Previously, exclusive accesses were folded into the generic X set. That made it harder to express model rules that
specifically target reservation-based exclusives rather than all atomic accesses.

By separating EX from X, the model becomes clearer and CAT code can talk about exclusives and RMWs directly.

relokin · 2026-06-29T12:24:25Z

One question I had is whether we want to remove some of the code that's used to compute atomic_load_store?

HadrienRenaud

One question I had is whether we want to remove some of the code that's used to compute atomic_load_store?

At the current state of the PR, I don't see why we would want to keep it.

HadrienRenaud · 2026-06-29T12:45:48Z

+let EX = try EX with emptyset
+let X = try X with emptyset
+
+let lxsx = [R & EX]; po \ (po; [M & EX]; po); [W & EX]


This is different semantics to what it was before (where it needed to be the same memory location). IIUC this is wanted for AArch64, but is this what is wanted for the other arch?

this is true but as we've discussed in the past, this test is allowed by the architecture:

AArch64 CoRW1+podxx { 0:X0=x; 0:X2=y; } P0 ; LDXR W1,[X0] ; MOV W3,#1 ; STXR W4,W3,[X2] ; exists([y]=1)

Which I took it to mean that the requirement for same location is not valid.

Sorry my comment was confusing. I understand that the change you made for all the architectures is wanted for AArch64. What I'm not sure is if this applies for other architectures?

In other words, I agree that this AArch64 test should behave like what your implementation does, but I'm wondering how a similar test should behave for risc-v or ppc.

That's a good point, and I am happy to start to split out the definitions for AArch64/AArch32/arm and all other architectures. Also the case of hardware updates is very specific to AArch64 too.

@maranget, I am not very familiar with the ordering requirements for ll/sc for other architectures. Do you think the definition of lxsx should be restricted to same location for MIPS, RISCV and PPC?

No idea! The RISCV description clearly states that the "reserved bytes" contains (and not is equal to) the bytes written, Additionally the size of these "reserved bytes" is not specified. So I guess that the new definitiobn is acceptable for RISCV.

Should we retain the old behaviour for architectures other than AArch64/AArch32/arm then?

Maybe the version in the standard library needs to have the old behaviour, and aarch64utils could redefine it with the Arm-specific definition?

But at this point, I'm wondering why not keep the old computed-in-mem.ml behaviour for non-Arm architectures. And maybe at this point #1876 should be amended for simply removing the handling of implicit atomic accesses because only Arm architectures generate them.

Happy either way. One of the problems with the old computed-in-mem.ml code is that it is also used for reasons other than computing rmw. For example, the optace optimisation relies on having rmwand then it does some checks (one of them is wrong though and started the whole discussion).

One of the problems with the old computed-in-mem.ml code is that it is also used for reasons other than computing rmw

Oh I had not realised. Maybe this is a good reason to keep the old computed-in-mem.ml code then?

I'm wondering if we could do a "best of both" and check that the two computations are equal in cat? This way it is explicitly defined in cat, and still enables the optimisations or the other uses of rmw before the start of the cat interpretation

maranget · 2026-06-29T13:43:38Z

remove the obsolete AArch64 A162 test, which relied on the previous treatment of exclusives

Perhaps we can keep this test?

relokin · 2026-06-29T14:27:34Z

remove the obsolete AArch64 A162 test, which relied on the previous treatment of exclusives

Perhaps we can keep this test?

Sorry Luc, the message is incorrect - I didn't remember correctly why I removed this test. herd/tests/instructions/AArch64/A162.litmus is a duplicate of herd/tests/instructions/AArch64/A44.litmus.

maranget · 2026-06-29T14:29:46Z

There is a difficulty with RISCV, the following test yields no outcome at all:

RISCV TST
{
 0:x5=x;
 1:x5=x;
}
 P0                   | P1          ;
 ori x7,x0,1          | ori x6,x0,2 ;
 amoswap.w x6,x7,(x5) | sw x6,0(x5) ;

exists ([x]=1 /\ 0:x6=0)

The reason may be that RISCV AMO instructions are represented by a specific "read and write" event.

relokin · 2026-06-29T14:46:48Z

There is a difficulty with RISCV, the following test yields no outcome at all:
RISCV TST
{
 0:x5=x;
 1:x5=x;
}
 P0                   | P1          ;
 ori x7,x0,1          | ori x6,x0,2 ;
 amoswap.w x6,x7,(x5) | sw x6,0(x5) ;

exists ([x]=1 /\ 0:x6=0)
The reason may be that RISCV AMO instructions are represented by a specific "read and write" event.

Thanks Luc, I wasn't really familiar with the Amo actions. I've excluded id from the definition of amo here: 491e759

relokin · 2026-06-30T11:32:01Z

One question I had is whether we want to remove some of the code that's used to compute atomic_load_store?

At the current state of the PR, I don't see why we would want to keep it.

Commits 222e509 and 5b6af15 are the first steps in this process. Very quickly, I am stepping into the territory of other architectures and rc11.ml and I am not sure what the right thing would be.

@maranget do you have a opinion about this?

maranget · 2026-07-01T07:33:17Z

I guess we can get rid of dead code, BTW, there is a shadowed definition of lxsx in stdlib.cat, let us get rid of it too!

diff --git a/herd/libdir/stdlib.cat b/herd/libdir/stdlib.cat
index e48ddda7f..74e51a8e8 100644
--- a/herd/libdir/stdlib.cat
+++ b/herd/libdir/stdlib.cat
@@ -33,9 +33,6 @@ let fencerel(B) = (po & (_ * B)) ;  po
 (* Control+cfence *)
 let ctrlcfence(ctrl,CFENCE) = (ctrl & (_ * CFENCE)) ; po
 
-(* Make the difference between load-reserve/store conditional and amo insructions *)
-let lxsx = rmw \ amo
-
 (* Backward compatibility *)
 let inv-field = try inv-domain with 0

relokin · 2026-07-01T11:57:07Z

+let X = try X with emptyset
+
+(* Define pairs of exclusives *)
+let lxsx = [R & EX]; po \ (po; [R & EX]; po); [W & EX]


BTW, I've relaxed this definition even further. AFAIU, for AArch64 at least, we need to pair a LDXR with the next in-po STXR (regardless of location) and any other following in-po STXR, unless we have a new LDXR.

Is it possible that in an instruction sequence LDXR; STXR; STXR; the second STXR may succeed? I thought that STXR was cancelling any reservation, whether it succeeds or not.

And, as far as I know, this is what our semantics does.

Sorry I think I got confused and I will revert this.

If the STXR is successful then the global monitor has to to go to open access: https://developer.arm.com/documentation/ddi0487/mb/-Part-B-The-AArch64-Application-Level-Architecture/-Chapter-B2-The-AArch64-Application-Level-Memory-Model/-B2-12-Synchronization-and-semaphores/-B2-12-1-Exclusive-access-instructions-and-Non-shareable-memory-locations . In our case the presence of an Explicit Memory Write Effect is the consequence of a successful STXR.

maranget · 2026-07-01T17:28:38Z

FYI I have made a draft PR #1894 that computes the EX and X sets in OCaml differently. The main feature is a (hopfully) fixed computation of rmw in OCaml. Namely, the computation of PR #1876 is incorrect by lack of making the difference between exclusives and AMO's. The PR also adds a predicate is_exclusive on events.

maranget · 2026-07-02T15:24:59Z


 (* Internal visibility requirement *)
-acyclic po-loc | ca | rf as internal
+acyclic po-loc | amo | ca | rf as internal


You may consider applying the same fix to x86tso.cat, which is the default model of the architecture X86. We may also add at lease the corresponding test for this (obsolete I admit) architecture:

X86 CoRW2+rmw { } P0 | P1 ; MOV EAX,$1 | MOV [x],$2 ; XCHG [x],EAX | ; exists ([x]=2 /\ 0:EAX=2)

maranget

LGTM. Some suggestions for a future PR

Add LR/SC and AMO tests for all architectures.
As long as there is is_atomic on events, we can define teh set "X" in machModelChecker.ml and avoid arch-specific defintions.

relokin · 2026-07-07T12:30:54Z

As long as there is is_atomic on events, we can define teh set "X" in machModelChecker.ml and avoid arch-specific defintions.

Wouldn't it be preferable to move towards a solution where the amo is computed when we build semantics. For example, in herd/AArch64Sem.ml when we build the semantics of a SWP we know that the Explicit Memory Read Effect and the Explicit Memory Write Effect should be in amo. Similarly for a hardware update of af and db. If we introduce a new field in event_structure then we would only need to modify the monadic operators to populate it correctly.

relokin · 2026-07-07T12:31:41Z

@maranget @HadrienRenaud are you happy with this PR? If you are, I'll rebase squash and merge.

maranget · 2026-07-07T12:38:26Z

As long as there is is_atomic on events, we can define teh set "X" in machModelChecker.ml and avoid arch-specific defintions.

Wouldn't it be preferable to move towards a solution where the amo is computed when we build semantics. For example, in herd/AArch64Sem.ml when we build the semantics of a SWP we know that the Explicit Memory Read Effect and the Explicit Memory Write Effect should be in amo. Similarly for a hardware update of af and db. If we introduce a new field in event_structure then we would only need to modify the monadic operators to populate it correctly.

Both solutions are fine (although mutually exclusive...). The first one (in MachModelChecker.ml) is compatible with the idea that such "atomic" accesses are a common to all architectures and avoids some duplication of code. The second (in semantics)n highlights the connexion with semantics.

maranget · 2026-07-07T12:38:58Z

@maranget @HadrienRenaud are you happy with this PR? If you are, I'll rebase squash and merge.

I'd like to have a last look at the last commit.

maranget · 2026-07-07T13:05:00Z

Hi @relokin. LGTM, merge at your earliest convenience.

HadrienRenaud

This looks good to me, thanks.

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

relokin · 2026-07-07T14:56:34Z

Merged, thanks @maranget and @HadrienRenaud !

This commit regroups three changes related to the new organisation of "atomic" accesses performed by PR #1889: such effects are now partitioned into the sets 'X' (emited by access-modify instructions, OCaml function `is_atomic`) and 'EX' (emited by exclusive access instructions, _i.e._ load reserve and store conditional, OCaml function `is_exclusive`). Notice that before the OCaml function `is_atomic` and the Cat set `X` were gathering all such effects. Also notice that `is_exclusive` was absent and that there existed a set `AMO` gathering the memory write effects emited by access-modify instructions. 1. Noticing that `is_atomic` no longer holds on effects generated by exclusive load and store, change `collect_atomics` (from memUtils.ml) names and code into `collect_atomics_and_exclusives`. 2. Modify the RISCV Cat models to account for the new semantics of the sets 'X' and `EX`. 3. Remove the Cat set `AMO` and the code that computed it.

[herd,cat] Fix some problems with the C architecture This PR fixes two problems: 1. Since PR #1855, the polymorphic value `V.Empty` circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting. 2. PR #1889 changed how the relation `rmw` is computed by defining it in stdlb.cat. The Cat definition of the relation `rmw` assumes that atomic effects are gathered in the set `X`, which was not the case of the C semantics. As a result the `rmw` relation was empty when the read-modify-write instructions are implemented by two (atomic) effects.

This commit regroups three changes related to the new organisation of "atomic" accesses performed by PR #1889: such effects are now partitioned into the sets 'X' (emited by access-modify instructions, OCaml function `is_atomic`) and 'EX' (emited by exclusive access instructions, _i.e._ load reserve and store conditional, OCaml function `is_exclusive`). Notice that before the OCaml function `is_atomic` and the Cat set `X` were gathering all such effects. Also notice that `is_exclusive` was absent and that there existed a set `AMO` gathering the memory write effects emited by access-modify instructions. 1. Noticing that `is_atomic` no longer holds on effects generated by exclusive load and store, change `collect_atomics` (from memUtils.ml) names and code into `collect_atomics_and_exclusives`. 2. Modify the RISCV Cat models to account for the new semantics of the sets 'X' and `EX`. 3. Remove the Cat set `AMO` and the code that computed it.

[herd] Consequences of splitting exclusive effects from the X events set (PR #1889) This PR groups three commits 1. Fixing the RISCV model (and the `collect_atomics` function from memUtils.ml) 2. Add some RISCV tests that check the problem fixed in 1. 3. Fix the computation of "atomic pairs" in OCaml, this computation was wrong before PR #1889: the cases of AMO's and exclusive accessed were not separated as they should be. As to 3., notice that, since PR #1889, there is no need to compute atomic pairs in OCaml for AArch64 and possibly for all Cat model (perhaps at the price of a small optimisation of `-optace iico`). Implementation of limiting the usage of the OCaml code for atomic pairs not being that straightforward, we leave that to a further PR.

relokin requested review from HadrienRenaud and maranget June 29, 2026 12:23

relokin requested a review from fsestini June 29, 2026 12:24

HadrienRenaud reviewed Jun 29, 2026

View reviewed changes

relokin force-pushed the rmw branch from 3f72170 to 5b6af15 Compare June 30, 2026 11:29

maranget mentioned this pull request Jul 1, 2026

[herd] Fix non explicit atomic pairs #1876

Closed

relokin commented Jul 1, 2026

View reviewed changes

maranget mentioned this pull request Jul 1, 2026

[herd] Compute EX and X sets in OCaml #1894

Closed

maranget reviewed Jul 2, 2026

View reviewed changes

maranget approved these changes Jul 2, 2026

View reviewed changes

maranget mentioned this pull request Jul 7, 2026

[herd] Load-reserve Store-Conditional may pair on different addresses #1896

Open

relokin force-pushed the rmw branch from 9ac95ae to d9802f6 Compare July 7, 2026 14:31

HadrienRenaud approved these changes Jul 7, 2026

View reviewed changes

relokin added 4 commits July 7, 2026 15:43

[herd] Add an annotation for exclusives in AArch64

b188a7e

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

[herd] Introduce EX annotation for ARM exclusive instructions

beadcfc

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

[herd] Introduce EX annotation for RISCV LR/SC instructions

79cda88

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

[herd] Introduce EX annotation for MIPS LL/SC instructions

5b5c593

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

relokin added 4 commits July 7, 2026 15:43

[herd] Introduce EX annotation for PPC LR/SC instructions

52719ec

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

[herd] Make EX a distinct eventset from X

6207e6e

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

[herd] Do not expose the rmw and amo relations

9660093

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

[herd] Do not include rmw in po-loc for all architectures

184f264

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

relokin force-pushed the rmw branch from d9802f6 to 184f264 Compare July 7, 2026 14:43

relokin merged commit f3f14bb into herd:master Jul 7, 2026
3 checks passed

relokin deleted the rmw branch July 7, 2026 14:56

maranget mentioned this pull request Jul 9, 2026

[herd] Consequences of splitting exclusive effects from the X events set (PR #1889) #1908

Merged

fsestini mentioned this pull request Jul 10, 2026

[libdir] Backport new version of stdlib.cat #1911

Merged

maranget mentioned this pull request Jul 10, 2026

[herd,cat] Fix some problems with the C architecture #1912

Merged

Uh oh!

Conversation

relokin commented Jun 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

What changed

Why

Uh oh!

relokin commented Jun 29, 2026

Uh oh!

HadrienRenaud left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

HadrienRenaud Jun 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Jun 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

HadrienRenaud Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget commented Jun 29, 2026

Uh oh!

relokin commented Jun 29, 2026

Uh oh!

maranget commented Jun 29, 2026

Uh oh!

relokin commented Jun 29, 2026

Uh oh!

relokin commented Jun 30, 2026

Uh oh!

maranget commented Jul 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget commented Jul 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget left a comment

Choose a reason for hiding this comment

Uh oh!

relokin commented Jul 7, 2026

Uh oh!

relokin commented Jul 7, 2026

Uh oh!

maranget commented Jul 7, 2026

Uh oh!

maranget commented Jul 7, 2026

Uh oh!

relokin commented Jun 29, 2026 •

edited

Loading

HadrienRenaud Jun 29, 2026 •

edited

Loading

maranget Jun 29, 2026 •

edited

Loading

HadrienRenaud Jul 1, 2026 •

edited

Loading

maranget Jul 1, 2026 •

edited

Loading