Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017).
Please visit the project website for more information.
Requirement: Coq 8.9.1, opam, Make, Rsync.
Installing dependencies with opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam remote add coq-promising -k git https://github.com/snu-sf/promising-opam-coq-archive
opam install coq-paco.2.0.3
opam install coq-sflib
opam install coq-promising-lib
Initialization
git clone https://github.com/snu-sf/promising-coq.git
make
: quickly build without checking the proofs.
./build.sh
: build with checking all the proofs. It will incrementally copy the development in the .build
directory, and then build there.
Interactive Theorem Proving: use ProofGeneral or CoqIDE.
Note that make
creates _CoqProject
, which is then used by ProofGeneral and CoqIDE. To use it:
_CoqProject
: Edit
> Preferences
> Project
: change ignored
to appended to arguments
.lib
and src/lib
contains libraries not necessarily related to the relaxed-memory concurrency.
src/lang
: Model (Section 2-4)
Language.v
: abstract interface of the programming languagesMemory.v
: memory model (MEMORY: *
rules in Figure 3)Commit.v
: the rule for thread views (*-HELPER
rules in Figure 3)Thread.v
: thread and its execution (READ
, WRITE
, UPDATE
, FENCE
, SYSTEM CALL
, SILENT
, PROMISE
rules in Figure 3)Configuration.v
: configuration (machine state) and its execution (MACHINE STEP
rule in Figure 3)Behavior.v
: the behaviors of a configurationsrc/prop
: General properties on the memory model
consistent_pf_consistent
(PFConsistent.v
)
In certification, promise is useless.src/while
Toy "while" language
This language provides the basis for the optimization & compilation results.
src/opt
: Compiler Transformations (Section 5.1)
Trace-Preserving Transformations: sim_trace_sim_stmts
(SimTrace.v
)
Strengthening: sim_stmts_instr
(SimTrace.v
)
Reorderings: reorder_sim_stmts
(Reorder.v
) and reorder_release_fenceF_sim_stmts
(ReorderRelFence.v
)
The latter proves the reordering of F_rel; *
is proved, while the former proves everything else.
Merges: Merge.v
Unused Plain Read Elimination: elim_load_sim_stmts
(ElimLoad.v
)
Read Introduction: intro_load_sim_stmts
(IntroLoad.v
)
Spliting acquire loads/updates and release writes/updates:
split_acquire_sim_stmts
(SplitAcq.v
), split_release_sim_stmts
(SplitRel.v
), split_acqrel_sim_stmts
(SplitAcqRel.v
)
These are used for the soundness proof of compilation to Power.
Proof Technique:
sim
(Simulation.v
) for the configuration simulationsim_thread
(SimThread.v
)sim_adequacy
(Adequacy.v
). From the configuration simulation to the behaviors.sim_thread_sim
(AdequacyThread.v
). From the thread simulation to the configuration simulation.sim_compose
(Composition.v
). "horizontally" composing configuration simulations for disjoint configurations.sim_stmts_*
(Compatibility.v
).src/drf
: DRF Theorems (Section 5.3)
drf_pf
(DRF_PF.v
)src/invariant
: An Invariant-Based Program Logic (Section 5.4)
sound
(Invariant.v
)