1. Design Criteria

<aside> 💡 Data-Race-Freedom, DRF

A data race occurs when we have two concurrent conflicting operations

• Conflicting: the two operations both access the same memory location and at least one is a write
• Concurrent: Differs across memory models
  • Java: the two operations are not ordered by “happens-before”
    • SW - Synchronizes-with

DRF programs have the same behaviors as in SC model

• For DRF programs, the programmer does not need to worry that reorderings will affect her code. </aside>

• Usability: DRF guarantee

  • DRF programs have the same behaviors as in SC model

• Implementable → Not too strong

  • Allow common optimization techniques
  • Mapping to hardware → Allow standard compilation schemes to major modern architectures
  • In some sense hijacked by the mainstream compiler

• Out-of-thin-air(OOTA) behaviors → Preserve type-safety and security guarantee

  • Cannot be too weak

2. HMM

Happens-Befor Order

Declarative Semantic → 给定行为，判定是否满足约束

Program execution → a set of events, and some orders between them.

po: program order; sw: synchronizes-with

Happens-before order (hb): transitive closure of $po \cup sw$

Happens-Before Memory Model, HMM

满足约束，就可以产生；不必构造执行流

Read can see (1) the most recent write that happens-before it, or (2) a write that has no happens-before relation.

3. JMM