Refinement-based game semantics with concurrency (fork)

This fork of CertiKOS/rbgs adds a concurrency signature/monad scaffold (models/Conc*, examples/Conc*) and a white paper explaining the direction. The base repo builds against modern Coq while keeping CompCert optional.

Quick start

Toolchain

Use the CompCert-compatible toolchain (no Rosetta on macOS):

opam switch create rbgs-ocaml-4.12 4.12.1
opam install coq.8.15.2 menhir.20200211
eval "$(opam env --switch=rbgs-ocaml-4.12)"

Configure and build

Clone your fork and build:

git clone https://github.com/<your-username>/rbgs.git
cd rbgs
./configure -nocompcert   # macOS-friendly; use ./configure on Linux to include CompCert
make -j4

Notes:

• CompCert’s runtime currently expects GNU binutils; on macOS use -nocompcert or build on Linux.
• The _CoqProject already lists the new concurrency files.

What’s in this fork

• Concurrency scaffolding: models/ConcSignature.v, ConcMonad.v, ConcStrategy.v, ConcRefinement.v with handler/scheduler-parametric interpretation and reachability-based refinement.
• Examples: examples/ConcSpawn.v, examples/ConcChan.v now include concrete handlers/scheduler choices and lemmas (spawn_step_adds_child, chan_step_progress) that exercise ConcStrategy.step.
• White paper: White_paper/whitepaper.tex summarizes goals, current status, and next steps.
• Bibliography: White_paper/references.bib cites foundational work (CompCertOC, CompCertOE, CTLinear).
• DSL polish: smart constructors (ConcMonad.spawn/yield/send/recv/join) and lightweight do-notation (_ <- t ;; u) keep scripts readable.
• Hygiene: compiled Coq/LaTeX artifacts are removed and ignored to keep the tree lean.

Refinement notes:

• ConcRefinement.v expresses refinement as reachability over the scheduler/handler step relation; strengthening to trace/fairness simulations is next.
• Example lemmas are intentionally small; flesh them out into full refinement case studies as the semantics matures.

Running without CompCert

If you only need the Rocq developments, configure with ./configure -nocompcert and run make -j4. CompCert can be re-enabled later by re-running ./configure (on Linux) and make clean && make -jN.