Fenced separation logic formalization
- C11 concurrency model definition
- Program expressions and their semantics
- Assertions
- The meaning of triples
- Auxiliary lemmas for the soundness proof
- Various helper lemmas
- Depth metric
- Some lemmas about validly annotated nodes
- Independent heap compatibility
- Helper lemmas for path.v
- Helper lemmas for memory safety
- Helper lemmas for initialized reads
- Lemmas about paths trough validly annotated execution
- Data race freedom.
- Memory safety
- There are no reads from uninitialized locations
- Lemmas for tracking release and acquire permissions
- Lemmas about non-atomic accesses
- Helper lemmas for triples
- Further lemmas about acquire reads and RMWs
- Adequacy
- Soundness of the proof rules
- Frame
- Consequence
- Disjunction
- Existential quantification
- Values
- Sequential composition (let)
- Parallel composition
- Loops
- Non-atomic allocations
- Non-atomic stores
- Non-atomic loads
- Atomic allocations
- Fences
- Soundness of atomic store rules
- Release stores
- Relaxed stores
- Soundness of atomic load rules
- A helper lemma
- Acquire load
- Relaxed load
This page has been generated by coqdoc