# Weak Memory Models

$$\require{enclose}$$

The simplest memory model: sequential consistency (SC) model, where programs access memory in turn (interleaving semantics).

• One memory operation is executed at a time.
• Operations from each thread are executed following their orders in the program (program-order).

SC model is too expensive to implement in practice, it prevents optimization in hardware and compilers. （程序优化在设计上是保持了顺序执行的行为的，但是在并发环境下可能会导致意外结果，例如下面的代码）

The store buffering program:

x = 1  | y = 1
r1 = y | r2 = x


The result might be $$r_1 = r_2 = 0$$ on x86 (compiler optimization, or write buffer) or Java.

r1 = y  # reordered by compiler since r1 is always y
y = 1
r2 = x
x = 1


Another example:

x = 0, y = 1

r1 = x       | x3 = y
r2 = x       | x = r3
if r1 == r2: |
y = 2    |


$$r_1 = r_2 = r_3 = 2$$ will never happen in SC model, but possible if compiler optimization happens.

## Memory Model Design Criteria

Models allowing optimizations are called relaxed memory models. For programming languages, MM can be complex since they have to reflect optimization of compilers and processors.

A data race occurs when we have two concurrent conflicting operations:

• Conflicting: two operations access same memory location and at least one is a write
• Concurrent: Differs across memory models, Java: two operations are not ordered by "happens before"

Memory model design criteria:

• Usability: data-race-free (DRF) guarantee
• DRF Programs have the same behaviors as in SC model
• Programmer does not need to worry that reorderings will affect her code
• Not too strong: allow common optimization techniques
• Cannot be too weak: preserve type-safety and security guarantee
• E.g. should not produce out-of-thin-air values

## Happens-Before Memory Model

In HMM, program execution is modeled as a set events, and some orders between them.

• Program order (PO):
• total order among events executed by the same thread
• Synchronization order (SO):
• total order among all synchronization events
• acquire / release of locks
• read / write of volatile variables
• SO needs to be consistent with PO
• SO events in same thread must be ordered in the same way as PO
• Synchronization-with Order (SW):
• a relation between a release of a lock and the next acquire event of the same lock
• a relation between a write of a volatile variable and the next read of the same variable
• SW is a partial order and a subset of SO
• Happens-before Order (HB):
• the transitive closure of the union of PO and SW
• E.g. $$A \rightarrow B$$, $$A \rightarrow C$$, but neither $$\enclose{horizontalstrike}{B \rightarrow C}$$ nor $$\enclose{horizontalstrike}{C \rightarrow B}$$.

In HMM, a read $$r$$ can see the:

• a write $$w$$ immediately happens before $$r$$
• $$w \rightarrow r \wedge \neg\exists w', w \rightarrow w' \rightarrow r$$
• any write $$w$$ that is not HB ordered with $$r$$
• $$\neg(w \rightarrow r \vee r \rightarrow w)$$

A program is DRF if for every execution, a read can only see the write that immediately happends before it.

HMM is a very week model. In the previous example,

x = 1  | y = 1
r1 = y | r2 = x


r1 = y can read result of y = 1 since they are not HB ordered.

### Causality Circle and Out-of-Thin-Air Read

Initially: x = y = 0

r1 = x      | r2 = y
if r1 != 0: | if r2 != 0:
y = 42    |   x = 42


In SC semantics, the left thread could not access $$y$$, and the right thread could not access $$x$$.

However, the result is possible in HMM due to a self-justifying causality circle:

• We speculate that y = 42 will be executed,
• Then r2 = y reads 42, and executes x = 42,
• Finally r1 = x reads 42 and justifies our speculation.

The next example shows HMM allows out-of-thin-air read, as result $$x = y = 42$$ is allowed for a same reason. （首先假设y = r1读出42，然后右边线程就会给x赋值42，因此假设成立了。）

Initially: x = y = 0

r1 = x | r2 = y
y = r1 | x = r2


### Java Memory Model

JMM is based on HMM, tries hard to distinguish good speculation and bad speculation.

• Introduce 9 axioms to constrain causality.
• Very complex, with surprising results and bugs.