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} \).

Happens-Before Order

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.

References

  1. An Operational Happens-Before Memory Model, Yang Zhang and Xinyu Feng