Repository navigation
Conversation
With the acq-rel AMO full-barrier clause present, prove against UMArm.ob:
- LSE (e.g. SWPAL): the leading and trailing DMB fences OCaml emits around an
atomic RMW add no ob edge the AMO does not already add (redundant);
- LL/SC (ldaxr/stlxr): the store-exclusive release is lxsx, not amo, so the
clause does not fire and the trailing fence is load-bearing.
Print Assumptions reports only stdpp functional_extensionality (no Admitted, no
added axiom). Motivation: the OCaml runtime (ocaml/ocaml#14936) drops these
redundant fences around LSE atomics on AArch64.
Collaborator
|
I think this will require rebasing onto main because of the GitHub CI fixes. |
Collaborator
|
@sebpop, Sorry for the delay I was on leave. This proof is really nice, although there are some things that should be cleaned-up before merging, I think. In particular, using “clause 135” to designate a line in a herd file is really confusing and really not robust if herd model is updated (even by adding irrelevant stuff). Before looking at it further, I'd really like to talk be email or if possible over a call. I couldn't find your email. Can you email me at |
sebpop
added a commit
to sebpop/ocaml
that referenced
this pull request
Sep 16, 2026
caml_atomic_exchange_field / caml_atomic_cas_field / caml_atomic_fetch_add_field wrap a seq_cst atomic read-modify-write in an acquire and a release fence (Note [MM]), emitting `dmb ishld`/`dmb ish` on AArch64. An acquire-release LSE atomic (SWPAL/CASAL/LDADDAL) is itself a full ordering point, so both fences are redundant when the RMW runs as one. The ARMv8.0 LL/SC expansion (LDAXR...STLXR) is not, so the trailing fence stays load-bearing there (ocaml#10972). We drop the fences only where an LSE atomic is known to run: - __ARM_FEATURE_ATOMICS: the compiler emits the LSE atomic inline. - HAS_OUTLINE_ATOMICS: the compiler uses libgcc's outline-atomics trampolines, which run an LSE atomic exactly when HWCAP_ATOMICS is set; we read that bit at run time. configure detects this lowering from the generated assembly, so -mno-outline-atomics keeps the fences. Every other configuration keeps the fenced C11 sequence, unchanged. Checked against the Arm AArch64 memory model with herd7 and a Rocq proof (rems-project/archsem#212): https://github.com/sebpop/ocaml-arm64-barrier-proofs Verified on macOS arm64 and on Vera linux-arm64.
sebpop
added a commit
to sebpop/ocaml
that referenced
this pull request
Sep 16, 2026
caml_atomic_exchange_field / caml_atomic_cas_field / caml_atomic_fetch_add_field wrap a seq_cst atomic read-modify-write in an acquire and a release fence (Note [MM]), emitting `dmb ishld`/`dmb ish` on AArch64. An acquire-release LSE atomic (SWPAL/CASAL/LDADDAL) is itself a full ordering point, so both fences are redundant when the RMW runs as one. The ARMv8.0 LL/SC expansion (LDAXR...STLXR) is not, so the trailing fence stays load-bearing there (ocaml#10972). We drop the fences only where an LSE atomic is known to run: - __ARM_FEATURE_ATOMICS: the compiler emits the LSE atomic inline. - HAS_OUTLINE_ATOMICS: the compiler uses libgcc's outline-atomics trampolines, which run an LSE atomic exactly when HWCAP_ATOMICS is set; we read that bit at run time. configure detects this lowering from the generated assembly, so -mno-outline-atomics keeps the fences. Every other configuration keeps the fenced C11 sequence, unchanged. Checked against the Arm AArch64 memory model with herd7 and a Rocq proof (rems-project/archsem#212): https://github.com/sebpop/ocaml-arm64-barrier-proofs Verified on macOS arm64 and on Vera linux-arm64.
sebpop
added a commit
to sebpop/ocaml
that referenced
this pull request
Sep 16, 2026
caml_atomic_exchange_field / caml_atomic_cas_field / caml_atomic_fetch_add_field wrap a seq_cst atomic read-modify-write in an acquire and a release fence (Note [MM]), emitting `dmb ishld`/`dmb ish` on AArch64. An acquire-release LSE atomic (SWPAL/CASAL/LDADDAL) is itself a full ordering point, so both fences are redundant when the RMW runs as one. The ARMv8.0 LL/SC expansion (LDAXR...STLXR) is not, so the trailing fence stays load-bearing there (ocaml#10972). We drop the fences only where an LSE atomic is known to run: - __ARM_FEATURE_ATOMICS: the compiler emits the LSE atomic inline. - HAS_OUTLINE_ATOMICS: the compiler uses libgcc's outline-atomics trampolines, which run an LSE atomic exactly when HWCAP_ATOMICS is set; we read that bit at run time. configure detects this lowering from the generated assembly, so -mno-outline-atomics keeps the fences. Every other configuration keeps the fenced C11 sequence, unchanged. Checked against the Arm AArch64 memory model with herd7 and a Rocq proof (rems-project/archsem#212): https://github.com/sebpop/ocaml-arm64-barrier-proofs Verified on macOS arm64 and on Vera linux-arm64.
sebpop
added a commit
to sebpop/ocaml
that referenced
this pull request
Sep 16, 2026
caml_atomic_exchange_field / caml_atomic_cas_field / caml_atomic_fetch_add_field wrap a seq_cst atomic read-modify-write in an acquire and a release fence (Note [MM]), emitting `dmb ishld`/`dmb ish` on AArch64. An acquire-release LSE atomic (SWPAL/CASAL/LDADDAL) is itself a full ordering point, so both fences are redundant when the RMW runs as one. The ARMv8.0 LL/SC expansion (LDAXR...STLXR) is not, so the trailing fence stays load-bearing there (ocaml#10972). We drop the fences only where an LSE atomic is known to run: - __ARM_FEATURE_ATOMICS: the compiler emits the LSE atomic inline. - HAS_OUTLINE_ATOMICS: the compiler uses libgcc's outline-atomics trampolines, which run an LSE atomic exactly when HWCAP_ATOMICS is set; we read that bit at run time. configure detects this lowering from the generated assembly, so -mno-outline-atomics keeps the fences. Every other configuration keeps the fenced C11 sequence, unchanged. Checked against the Arm AArch64 memory model with herd7 and a Rocq proof (rems-project/archsem#212): https://github.com/sebpop/ocaml-arm64-barrier-proofs Verified on macOS arm64 and on Vera linux-arm64.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
With the acq-rel AMO full-barrier clause present, prove against UMArm.ob:
Print Assumptions reports only stdpp functional_extensionality (no Admitted, no added axiom). Motivation: the OCaml runtime (ocaml/ocaml#14936) drops these redundant fences around LSE atomics on AArch64.