Skip to content

Latest commit

 

History

History
24 lines (15 loc) · 830 Bytes

README.md

File metadata and controls

24 lines (15 loc) · 830 Bytes
Raw

Known-Joins formalization in Coq

Run once:

./configure

To run the proofs use make.

  • src/SafeJoins.v corresponds to Section 3, where Theorem 3.2 is called deadlock_avoidance.

  • src/CG.v defines computation graph from traces (Section 4.1).

  • src/AccessHistory.v defines shared memory, data-races, memory accesses and so on.

  • src/SJ_CG.v formalizes maps Safe-Joins in a computation graph (since the former operates on a trace); in short, this file formalizes known-sets at the node level (of a computation graph).

  • src/LocalInfo.v formalizes the local memory in a computation graph. The file also includes the connection between shared memory and local information. The main result is wf_reduces_alt.