snu-sf / promising-coq

The Coq development of A Promising Semantics for Relaxed-Memory Concurrency

A Promising Semantics for Relaxed-Memory Concurrency

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.

Build

• 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:

  • ProofGeneral: use a recent version.
  • CoqIDE: configure it to use _CoqProject: Edit > Preferences > Project: change ignored to appended to arguments.

References

Model

• 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 languages
  • Memory.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 configuration

• src/prop: General properties on the memory model

  • Promise-free certification: 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.

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:

    • Simulation (Configuration): sim (Simulation.v) for the configuration simulation
    • Simulation (Thread): sim_thread (SimThread.v)
    • Adequacy (Configuration): sim_adequacy (Adequacy.v). From the configuration simulation to the behaviors.
    • Adequacy (Thread): sim_thread_sim (AdequacyThread.v). From the thread simulation to the configuration simulation.
    • Composition: sim_compose (Composition.v). "horizontally" composing configuration simulations for disjoint configurations.
    • Compatibility: sim_stmts_* (Compatibility.v).

• src/drf: DRF Theorems (Section 5.3)

  • Promise-Free DRF (Theorem 1): drf_pf (DRF_PF.v)
  • We did not formalize DRF-RA (Theorem 2) and DRF-SC (Theorem 3) yet.

• src/invariant: An Invariant-Based Program Logic (Section 5.4)

  • Soundness: sound (Invariant.v)

promising-coq's Issues

Add Documentation

• What is the motivation of separating wf and consistent in the Module Configuration?
  It seems both has the same type and same init/preservation property

Proposal: re-certification for each instruction step

It is a "call for discussion" for the matter of re-certification.

Currently we allow a thread to take instruction steps as many as it wants, and its promises are re-certified only after all the instruction steps are executed. It basically allows more behaviors, effectively validating more compiler optimizations (e.g. merging a write and a update).

Some people complained that it looks bad, and now we have quite a concrete reason why we don't want it. Consider the following code snippet:

lock(); // implemented w/ acquire CAS to location "l"
x = 1;
unlock(); // implemented as release write to "l"

Here, we want to do some modular reasoning and conclude that x = 1 cannot be promised before the lock is acquired. However, actually it can be, provided that unlock() is called right before lock(), as in the certification you can lock() "l" that is just released by unlock(). This is basically due to the fact that we re-certify the promises only at the end of a tread step, but not every instruction step, e.g. especially right before lock():

// [x = 1] can be promised
unlock();
// not required to re-certify promises here
lock();
x = 1;
unlock();

I believe the benefit of allowing these kind of reasoning is much bigger than the cost of losing some compiler optimizations, which are anyway not performed in the mainstream compilers.

So I propose to revise the promising semantics in such a way that a thread step is really a single instruction step, and the promises are re-certified for each instruction step.

We may need to adjust simulation relations for compiler optimizations, but it should not be a big deal AFAICT. We will see.

Migrate to Coq 8.6

@orilahav and I are working on it.

Port to Coq 8.8

https://coq.inria.fr/news/145.html

Add Documentation

• Add documentation for "imm"
• Add documentation for "cmem"

Porting to Coq 8.9?

Coq 8.9 is out: https://coq.inria.fr/download

build.sh spawns too many jobs

Currently, make is called with -j, which will spawn as many jobs as there are parallel targets at any given time. On systems with (only) 4 CPUs, this leads to unnecessary contention from the ~8 jobs running simultaneously. Additionally, the memory usage far exceeds my modest 8GB of RAM.

I don't quite know how to make an optional -jN parameter work well with your build.sh setup. In any case, I think it would be safer to not use -j by default.