Pomsets with preconditions: a simple model of relaxed memory

Pomsets with preconditions: a simple model of relaxed memory

---

연구 분야: Verification

---

---

학회: Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA

---

초록

Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning. Is that why they have become so complicated? We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the 80s (pomsets), at least for X64 and ARMv8. We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all expected sequential compiler optimizations, (3) satisfies the DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.

---