Relaxed Memory Model Zoo

Intel Itanium (IA-64) Memory Ordering
← Back to the map

Intel Itanium (IA-64) Memory Ordering

2002 · Intel, HP · hardware, formal · axiomatic formalism

The memory-ordering model of the Intel Itanium (IA-64) architecture. Ordinary loads and stores are 'unordered' and may be reordered in all four directions; ordering is imposed explicitly by acquire loads (ld.acq), release stores (st.rel) and the memory fence (mf) — a ld.acq is ordered before every following memory operation and a st.rel after every preceding one. This ISA-level acquire/release design is closer in spirit to ARMv8's LDAR/STLR than to a bare relaxed-plus-barrier model like POWER/ARMv7. Cache coherence (a per-location total order on writes) is guaranteed. Two independent academic formalizations exist: Yang et al. (CHARME 2003), a logic-programming/SAT axiomatization of the ordering rules, and Higham, Jackson & Kawash (2007), a programmer-centric 'views' characterization which finds the vendor specification not fully tight (the model lies between two closely related definitions). Neither formalization nor the vendor manual states a machine-checked containment or incomparability against another model in this dataset, so no strength edge is drawn.

Properties

Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.

Reordering sound
  • yes Store→Load
  • yes Store→Store
  • yes Load→Load
  • yes Load→Store
Reasoning guarantees
  • yes Coherence
  • yes No undefined behaviour
  • no In-order execution
  • yes No out-of-thin-air

Ordering relationships

Strictly stronger than
  • Cache Coherence — Itanium guarantees cache coherence (a per-location total order on writes; Intel Itanium SDM, memory-ordering rules) and adds cross-location ordering via ld.acq/st.rel/mf; bare coherence has neither. Separating outcome: MP with acquire/release or mf on both sides, forbidden by Itanium, allowed by Coherence. Cited (no herd7 cat model for IA-64), not machine-run.

References