Title Page
Abstract
Contents
Chapter 1. Prologue 7
1.1. Introduction 7
1.2. Background: The Promising Semantics 8
1.2.1. The Promising Semantics 8
1.2.2. Additional Examples of the Promising Semantics 15
Chapter 2. Local Data-Race-Freedom Guarantees for Program Writers 17
2.1. Introduction: The Need for Local DRF 17
2.2. Local DRF in Weak Memory Models 22
2.2.1. Local DRF w.r.t. an "In-Order" Semantics 22
2.2.2. Local DRF w.r.t. RA and SC 28
2.3. Local DRF Guarantees 32
2.3.1. Local DRF-PF 32
2.3.2. Local DRF-RA 35
2.3.3. Local DRF-SC 38
2.3.4. Time-wise Local DRF Guarantees 39
2.4. Applying LDRF for Modular Reasoning 42
2.4.1. Reasoning About Client Code 43
2.4.2. Reasoning About Library Code 46
2.5. Mapping PS2.1 to Hardware 47
2.6. A Counterexample to Local DRF in PS 52
2.7. Conclusion and Related Work 53
Chapter 3. Sequential Reasoning for Compiler Writers 57
3.1. Introduction: Optimizations under Weak Memory 57
3.2. The Sequential Permission Machine 62
3.3. Advanced Behavior Refinement 74
3.4. An Overview of a Certified Optimizer 80
3.5. A Certified Optimizer in Detail 84
3.5.1. Optimizations in Detail 84
3.5.2. Simulation Relation in SEQ 87
3.6. Non-atomics in the Promising Semantics 88
3.7. Adequacy of Sequential Reasoning 93
3.8. Conclusion and Related Work 96
Bibliography 101
초록 111