Verifying concurrent programs under weak memory models / vorgelegt von Oleg Travkin, M.Sc. Paderborn, 2017
Inhalt
- Introduction
- Memory Models
- Programs
- Parameterized Semantics
- Sequential Consistency
- Total Store Order
- Partial Store Order
- Relaxed Memory Order
- Related Work
- Reduction from Weak Semantics to Sequential Consistency
- Symbolic Execution with Weak Memory Semantics
- Transformation to a new SC Program
- Reduction is Sound and Compositional
- Weak2SC – The Implementation
- Architecture of Weak2SC
- Case Study – Work Stealing Queue
- From LLVM IR to a Store Buffer Graph
- Template-based Generation of new Programs
- Generating Promela Programs
- Generating KIV Program Encoding
- Promela Programs for Operational Memory Models
- Discussion and Possible Future Extensions
- Correctness of Concurrent Data Structures
- Verifying Linearizability under Weak Memory Models
- Model Checking under Weak Memory Models
- Proving Linearizability under Weak Memory Models
- Overview
- Abstract Data Type
- Concrete Data Type
- Abstraction Function
- Invariant
- Proof Procedure and Comparison
- Related Work and Discussion
- Conclusion
- Proofs
- Code Examples
- Bibliography