A Coq library with formalization of the Truly Stateless Concurrency Model Checker (TruSt) in Coq.
Checkout the paper about TruSt and my blogpost (in Russian).
-
src/lib
- common definitions, lemmas -
src/basic
- definitions and lemmas about some common notions on semantics of concurrent programs -
src/models
- definitions of some weak memory models (RA, SCOH, TSO) -
src/trust
- TruSt formalization, includes:Util.v
- miscellaneousPath.v
- adaptation of mathcomp's pathTerminateGen.v
- lemmas for general relation terminationExecutions_Aux.v
- auxiliary lemmas about execution graphsSem.v
- general program semantics for TruStAlg.v
- TruSt definition, its simple properties and correctnessTermination.v
- TruSt terminationPrev.v
- definition of reversed TruSt algorithmComplete.v
- TruSt completenessOplimal.v
- TruSt optionalityModels.v
- Instances of concrete memory models for TruSt (SC, RA, SCOH, TSO, RC11)