[herd] Load-reserve Store-Conditional may pair on different addresses by maranget · Pull Request #1896 · herd/herdtools7

maranget · 2026-07-03T10:03:59Z

The following test may succeed:

AArch64 L020
(* Observed on many systems with `-mode presi` or `-s 4` *)
{
 0:X0=x; 0:X2=y;
}
 P0              ;
 LDXR W1,[X0]    ;
 MOV W3,#1       ;
 STXR W4,W3,[X2] ;
exists([y]=1)

maranget · 2026-07-03T10:04:50Z

Draft, for comments and -variant vmsa,asl still following the old semantics.

relokin

Overall looks good to me but I have a couple of comments about the tests.

maranget · 2026-07-06T12:44:04Z

Hi @relokin. What this PR basically does is changing the test that controls performing the store conditional.

First observe that the reservation (a.k.a exclusive monitor) is implemented by using a unique register RES (for AArch64, VMSA and ASL. VMSA+ASL uses an additional flag). Schematic behaviour is a follows

Initially this register holds the null pointer (i.e. 0).
LDXR sets RES to its effective address.
STRX perform a check on RES : (a) old check compare STXR effective address with RES; or (b) new check , checks that the contents of RES is different from null. Perform store when the check passes. Always reset RES to null.

See also the tests L020 (LDXR and STXR to different addresses, store was always failing now it may succeed) and L021 (LDXR followed by two STXR, all to the same address, the second STXR never succeeds).

Finally an new test L106 consists in a simple STXR, without LDXR, the store normally always fails but may succeed when -variant ConstrainedUnredictable is specified.

maranget · 2026-07-06T13:16:15Z

I have also added L107 (L021 with -variant CU). The current implementation of this PR can perform the second STXR. I am not sure at all that the result is correct, as the description of the local monitor does suggest that this variant have no impact on the local monitor being cleared (here).

AArch64 L107
(* Can the second STXR succeed? *)
Variant=CU
{
int x=1;
0:X0=x;
}
 P0               ;
 MOV W3,#2        ;
 MOV W5,#3        ;
 LDXR W1,[X0]     ;
 STXR W4,W3,[X0]  ;
 STXR W6,W5,[X0]  ;
exists 0:X4=1 /\ 0:X6=0 /\ x=3

relokin · 2026-07-07T10:28:28Z

Looks good to me. Perhaps one concern I have is that for AArch64 -variant CU is not modelling any architecturally valid behaviours. In other words, it shouldn't be used by most users.

maranget · 2026-07-07T12:20:07Z

Looks good to me. Perhaps one concern I have is that for AArch64 -variant CU is not modelling any architecturally valid behaviours. In other words, it shouldn't be used by most users.

Thanks @relokin. I'll delay considering merging until PR #1889 is merged.

Given x and y that are different addresses `LDXR x; ...; STXR y`, STXR to y can succeed. Hence, the only situation when STXR always fail is when there is no reservation, which we implement by the reservation address being null. Detailed changes: + The new semantics is also implemented for AArch64 ASL and ASL+VMSA modes + With `-variant ConstrainedUnpredictable`, STXR can succeed even in the absence of a reservation (non-ASL only, no access to variant in ASL). + Same semantics of LR/SC pairs for RISCV Notice that this semantics (SC can succeed event with a reservation to a different address) was activated by the variant `LrScDiffOk`. This behaviour now being the default, we suppress the variant.

+ Add constrained unpredictable tests Note that these tests are disabled in ASL mode. (No access to the ConstrainedUnpredicable variant) + Add "LDXR x; LDXR y, STXR x" tests.

maranget · 2026-07-10T08:26:04Z

Hi @relokin and @HadrienRenaud. Rebased on master since prerequisite PR #1889 is merged, all commits squashed into two commits, ready for review.

HadrienRenaud

This looks ok to me but I think the handling of reserved addresses in ASL could be cleaner.

HadrienRenaud · 2026-07-10T10:52:29Z

+        | _ ->
+           if setzero then
+             state_add loc ASLS.V.zero st
+           else st


I don't really understand why this is needed. In both physmem-*.asl, the address is initialised to Zeros{_}

Also the initial environment would not be correctly typed checked: this is an integer and we expect a 56 or 64 bits bitvector (depending on whether VMSA is activated, i.e. whether RESADDR stores a physical or virtual address)

HadrienRenaud · 2026-07-10T10:54:37Z


  if SuccessVA then
-    CheckEq(address, reserved);
+    CheckProp(reserved != 0);


reserved has type bits(64) here

Suggested change

CheckProp(reserved != 0);

CheckProp(!IsZeros(reserved));

or

Suggested change

CheckProp(reserved != 0);

CheckProp(reserved != Zeros{64});

HadrienRenaud · 2026-07-10T10:55:42Z


  if SuccessPA then
-    CheckEq(paddress.address, reserved);
+    CheckProp(reserved != 0);


reserved has type bits(56) here

Suggested change

CheckProp(reserved != 0);

CheckProp(!IsZeros(reserved));

Or

Suggested change

CheckProp(reserved != 0);

CheckProp(reserved != Zeros{56});

Consider two STXR in a row. The first STXR sets the RES register to zero (integer zero) and this value is seen as zero (integer) by the next STXR. In the case we have no LDXR nor STXR before an exclusive instruction, RES is not initialised, hence the setzero flag above...

Hi @maranget, I think there was a misunderstanding for what I was suggesting, so I implemented it in #1914. Please consider merging it in this branch before merging this PR.

I no longer have time to do this in a safe manner, I leave it to you.

relokin · 2026-07-10T11:15:12Z

Not really the point of this PR so you can go ahead and merge as soon as @HadrienRenaud is happy but I don't understand why we support -variant cu in AArch64. -variant cu models behaviours which are architecturally forbidden. If the point of -variant cu is to enable forbidden behaviours then I think we need to change the name of this variant. CONSTRAINED UNPREDICTABLE has a specific meaning for the AArch64 architecture and the behavious of -variant cu are not CONSTRAINED UNPREDICTABLE. Perhaps these should have been behaviours one would expect from -through all?

maranget · 2026-07-11T06:50:49Z

I do not understand the intent of -variant CU. I'd gladly keep it out of LR/SC if you think this is the thing to do. As far as I remember, some usage of this variant in mixed-size mode was less problematic.

maranget · 2026-07-11T06:55:22Z

some usage of this variant in mixed-size mode was less problematic.

My bad, this usage is for generators... Hence we can suppress -variant CU in herd7, having STXR to succeed whatever the context is being the only occurrence of this variant.

maranget force-pushed the lxsx-diff branch 3 times, most recently from 3fee515 to 4e75239 Compare July 3, 2026 10:34

relokin reviewed Jul 3, 2026

View reviewed changes

Comment thread herd/tests/instructions/AArch64/L106.litmus

Comment thread herd/tests/instructions/AArch64/L020.litmus Outdated

maranget force-pushed the lxsx-diff branch from 4e75239 to e68af4f Compare July 6, 2026 09:53

maranget force-pushed the lxsx-diff branch 2 times, most recently from 832dc8d to eaecbf6 Compare July 6, 2026 12:58

maranget force-pushed the lxsx-diff branch from eaecbf6 to 0a0046c Compare July 9, 2026 15:12

maranget mentioned this pull request Jul 9, 2026

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

Merged

maranget force-pushed the lxsx-diff branch from 0a0046c to 926e0d9 Compare July 10, 2026 08:03

maranget added 2 commits July 10, 2026 10:13

[herd] Add tests

4291cc0

+ Add constrained unpredictable tests Note that these tests are disabled in ASL mode. (No access to the ConstrainedUnpredicable variant) + Add "LDXR x; LDXR y, STXR x" tests.

maranget force-pushed the lxsx-diff branch from 926e0d9 to 4291cc0 Compare July 10, 2026 08:20

maranget marked this pull request as ready for review July 10, 2026 08:24

maranget requested review from HadrienRenaud and relokin July 10, 2026 08:26

HadrienRenaud approved these changes Jul 10, 2026

View reviewed changes

HadrienRenaud mentioned this pull request Jul 12, 2026

[herd,asl] Represent RESADDR as a bitvector #1914

Open

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

relokin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

relokin commented Jul 7, 2026

Uh oh!

maranget commented Jul 7, 2026

Uh oh!

maranget commented Jul 10, 2026

Uh oh!

HadrienRenaud left a comment

Choose a reason for hiding this comment

Uh oh!

HadrienRenaud Jul 10, 2026

Choose a reason for hiding this comment

Uh oh!

HadrienRenaud Jul 10, 2026

Choose a reason for hiding this comment

Uh oh!

HadrienRenaud Jul 10, 2026

Choose a reason for hiding this comment

Uh oh!

maranget Jul 11, 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!

HadrienRenaud Jul 12, 2026

Choose a reason for hiding this comment

Uh oh!

maranget Jul 12, 2026

Choose a reason for hiding this comment

Uh oh!

relokin commented Jul 10, 2026

Uh oh!

maranget commented Jul 11, 2026

Uh oh!

maranget commented Jul 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

maranget commented Jul 3, 2026 •

edited

Loading

maranget commented Jul 3, 2026 •

edited

Loading

maranget commented Jul 6, 2026 •

edited

Loading

maranget commented Jul 6, 2026 •

edited

Loading

maranget Jul 11, 2026 •

edited

Loading