Relaxed separation logic formalization
Version 1.1, released 2016-03-22
Copyright (c) Viktor Vafeiadis
C11 concurrency model definition
Consistency axioms
Properties describing the absence of memory errors
Examples
Mutual exclusion locks
Message passing
Program expressions and their semantics
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
Release stores
Relaxed stores
Relaxed loads
Acquire loads
Atomic RMWs: Compare and swap
Assertions
Normalization
Syntactic properties of assertions
Model of heaps
Assertion semantics
Lemmas about heaps and assertions
Auxiliary lemmas for the soundness proof
Lemmas about view shifts
Various helper lemmas
Depth metric
Memory safety
Independent heap compatibitity
Race freedom
Lemmas about acquire-release accesses
Lemmas about non-atomic accesses
The meaning of triples
Heap annotations
Configuration safety
The meaning of triples
Helper lemmas for triples
Further lemmas about acquire reads and RMWs
This page has been generated by
coqdoc
Imprint
|
Data protection