ArchSemArm: add the acq-rel AMO full-barrier bob clause (UMArm + VMSA22Arm)

[sebpop]

UMArm and VMSA22Arm track the ESOP'22 Arm model and are missing one clause the current Arm application-level model has: the forward edge out of an acquire-release AMO write,

herd/libdir/aarch64hwreqs.cat:135

    [range([Exp & R & A]; amo; [Exp & W & L])]; po; [Exp & M | ...]

i.e. the property that an atomic with both acquire and release semantics acts as a full barrier. This property has been in the Arm model since 2018 -- herd herd/herdtools7@a6c1561 (Luc Maranget, "herd: Implement atomic operations ADD and EOR"), originally po; ([A];amo;[L]); po -- and was strengthened to this range(...) forward-edge form in 2022, herd/herdtools7@636b716 (PR #322, "Atomics with both acquire and release semantics currently act as a full barrier", Jade Alglave). It was most recently reworded in 2025-12 by herd/herdtools7@003ec32 (Fault-Effects relaxation).

The clause is added identically to UMArm.bob and VMSA22Arm.bob (user-mode projection: target [M]; the full model's [Imp & Tag & R] / [MMU & FAULT] targets do not occur in these models). Keeping the two bob definitions in sync preserves VMUMEquivThm.UM_to_VMSA_bob (VMSA.bob = UM.bob), so the whole of ArchSemArm still builds.

[febyeji]

Thank you for the PR! The Coq translation of the explicit-memory part looks right to me. However, could you clarify the statement that the full model’s Imp & Tag & R / MMU & FAULT targets “do not occur in these models”? VMSA22Arm.v does define Fault, Fault_T, and Fault_P events and uses them in obfault.

[sebpop]

Thanks! You're right, and I've fixed it. VMSA22Arm does model Fault effects (Fault_T/Fault_P) and Tag reads — the "do not occur" wording was inaccurate.

The actual reason for the [M] (explicit-memory) target is that it matches the sibling acquire/release bob clauses in the same definition — [A ∪ Q]; po; [M] and [M]; po; [L] — which likewise target only [M], rather than the full herd target [Exp & M | Imp & Tag & R | MMU & FAULT]. Fault/tag ordering in this model comes from the other ob1 components (obfault, tob, obtlbi, …), not from bob. So the new clause is consistent with how bob already treats acquire/release ordering here, and keeping UMArm.bob and VMSA22Arm.bob identical preserves VMUMEquivThm.UM_to_VMSA_bob.

I've corrected the commit message and added a code comment to both bobs spelling this out (and noting explicitly that VMSA22Arm does model faults, just ordered elsewhere). Happy to instead use the full [Exp & M | Imp & Tag & R | MMU & FAULT] target if you'd prefer faithfulness to the herd clause over consistency with the neighbouring clauses — it doesn't affect the fence-redundancy result, which only needs the [M] case.

[febyeji]

Thank you for the clarification! A simpler comment would be suffice, but I think the code looks right.

[tperami]

Thank you for this fix! I would be happy to talk by email or over a video call about the status of this model, and what use case you have in mind for it. The gist is that our only use case for this model so far was to support the proof relating it to the ESOP22 VMSA model. Therefore, I suspect it is slightly out of sync with the official herd model and probably some other small fixes are needed. We or you could do them depending on what you need this model for

[sebpop]

@tperami thanks, and yes — happy to talk by email or a call.

The use case is the proof in #212: an optimization in the OCaml runtime (runtime/memory.c) that drops the two DMB fences the runtime currently places around Armv8.1 acquire‑release LSE atomics (swpal/casal/ldaddal/…). Those fences are already redundant in the current herd model, where an acq‑rel AMO is a full ordering point (aarch64hwreqs.cat:135; the clause has been in herd since 2018, strengthened in 2022 by herd/herdtools7#322). UMArm/VMSA22Arm were just missing that clause — they track the ESOP'22 snapshot — so #211 brought them up to current herd. #212 then proves, over the ob relation, that the leading/trailing fences add no ordered‑before edge the AMO doesn't already provide (and, conversely, that for LL/SC ldaxr/stlxr the trailing fence is load‑bearing).

I only depend on this one clause for the proof, so I don't need the whole model brought fully in sync with herd. I did keep UMArm.bob and VMSA22Arm.bob identical so VMUMEquivThm.UM_to_VMSA_bob still holds.