OCaml atomics on real hardware

What the compiler and runtime actually deliver, per machine

This page documents and summarises known behaviour of OCaml's memory model as delivered through Atomic on real hardware. It is not a definitive source, it is subject to change, and corrections are welcome. It exists mainly to record behaviour I have observed whilst undertaking native atomics work in the OCaml compiler. The code behind these tests is Témoin.

The tests run against Atomic rather than assembly, so they measure what the compiler and runtime give you, not what the architecture permits.

Not covered. Mutex, Condition, effects, and Domain beyond spawning. Absence from this page means untested, not permitted.

Shapes

Test	What it checks
MP	A value written before an atomic flag is visible to whoever reads the flag
MP publication	The same without atomics
SB	Store buffering, forbidden for atomics
SB control	Store buffering with plain accesses, which hardware may legally do
LB	Load buffering
CoRR	Having seen the new value, you cannot see the old one again
WRC	Causality across three domains
IRIW	Whether four domains agree on the order of two independent writes
CAS	Exactly one winner
FAA	Two increments, two distinct old values
XCHG	Exactly one domain sees the initial value

MP, SB and LB run again for each storage kind.

Kind	What it is
`atomic`	`int Atomic.t`
`plain`	Padded `int array` slot
`field`	Mutable record field holding an immediate
`ptrfield`	Mutable record field holding a pointer, so `caml_modify`
`floatarr`	`float array` element, unboxed and flat

Observed

	amd64	Power10	SpacemiT X60	Ampere eMAG	z15
Architecture	x86-64	POWER	RISC-V	AArch64	z/Architecture
Cores	12	192	8	32	2
SB control	fires	29,387	11	fires	does not fire
WRC, IRIW	ok	ok	ok	ok	skipped
Everything else	ok	ok	ok	ok	ok

Nothing has produced a forbidden outcome through Atomic on any machine.

A clean run only counts if SB control fires. It is racy plain accesses in a shape no fence orders, so the hardware is free to produce the forbidden outcome, and firing proves the harness can see one. The z15 is ordered strongly enough that it never fires, so that run detects nothing and reports a non-result rather than a pass.

Plain accesses on POWER are not multi-copy atomic, so two readers may disagree about the order of two independent writes. A million iterations of IRIW across four domains on a 192-core Power10 produced no disagreement. An observation, not a guarantee.

float array loses the fence

MP publication holds without atomics because OCaml emits lwsync before every plain store to mutable heap state on POWER, which orders store against store but not store against load. That covers value stores only. A float array element is an unboxed double, so POWER emits lwsync then std for a value store and a bare stfd for a float one.

MP publication	Power10	SpacemiT X60
`floatarr`	443 in 500,000	89 in 20,000,000
`plain`	silent	silent
`field`	silent	silent
`ptrfield`	silent	silent

Not a bug. The fence exists so nobody sees a pointer into a half-initialised block, and float arrays hold no pointers. The trap is that it gives int arrays an ordering that does not generalise, and code leaning on it loses the guarantee the moment the value is a float.

Reproducing

dune build && ./_build/default/bin/main.exe -n 1000000

-only NAME runs a subset. Counts are single runs at the iteration counts given, on the machines named.

Revisions

2026-08-24 — first version. Five machines, eleven shapes, five storage kinds.