I. Definition

1. Naive Definition

Each memory accesses has a mode:

• Reads: rlx or acq
• Writes: rlx or rel
• RMWs: rlx, acq, rel or acq-rel

“Strength” order $\sqsupset$ is given by (the transitive closure of):

• Synchronization ($\tt \color{green} sw$ → synchronize-with)

  $$ ⁍ $$

• Happens-before

  $$ \gdef\gr{\textcolor{green}} \gdef\dr{\textcolor{darkred}} \gdef\dg{\textcolor{darkgreen}} \gdef\db{\textcolor{darkblue}} \tt G.\dr{hb} = (G.po ∪ G.\gr{sw})^+ $$

• Axiom

  $$ \gdef\gr{\textcolor{green}} \gdef\dr{\textcolor{darkred}} \gdef\dg{\textcolor{darkgreen}} \gdef\db{\textcolor{darkblue}}

  \texttt{$\tt \dr{hb}|_{loc} ∪ rf ∪ mo ∪ rb$ is acyclic} $$

2. Full Definition

$$ {\tt non-atomic \sqsubset relaxed \sqsubset release / acqire\sqsubset sc} $$

The full C/C++11 is more general:

• Non-atomics for non-racy code (the default!)
• Four types of fences for fine grained control
• SC accesses to ensure sequential consistency if needed