1; |\[l:t1:store:1\]| Flag := True; |\[l:t1:store:2\]|

&

– Task 2: loop|\[l:spin:1\]| R1 := Flag; exit when R1; end loop; |\[l:spin:2\]| R2 := Data; |\[l:read\]|

&

Data : Integer with Volatile; Flag : Boolean with Atomic;

\
&

Non-blocking synchronization techniques are notoriously difficult to implement and the design of non-blocking data structures is an area of active research. To enable non-blocking synchronization, a programming language must provide a strict memory model. The purpose of a memory model is to define the set of values a read operation in a program is allowed to return [@Boehm:mem:survey].

To motivate the need for a strict memory model, consider the producer-consumer synchronization example in Fig. \[fig:mem:example\](a) (adopted from [@Hill:CSprimer] and [@Barnes:RationaleAda2012]). The programmer’s intention is to communicate the value of variable [Data]{} from Task 1 to Task 2. Without explicitly requesting a sequentially consistent execution, a compiler or CPU may break the programmer’s intended synchronization via the [Flag]{} variable by re-ordering memory operations that will result in reading [R2 = 0]{} in Line \[l:read\] of Task 2. (E.g., a store–store re-ordering of the assignments in lines \[l:t1:store:1\] and \[l:t1:store:2\] of Task 1 will allow this result.) In Ada 2012, such re-orderings can be ruled 