tchajed/instrumented-semantics
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Proving refinement of concurrent programming language models in Coq
6 commits 1 branch 0 tags 38 KiB
  • Rocq Prover 98.7%
  • Makefile 1.3%
Find a file
Exact
Tej Chajed 70b4e64ea7
 Rename repo
2018-01-26 15:13:16 -05:00
.gitignore Define basic cooperative semantics 2017-03-07 13:19:12 -05:00
Automation.v State a consistency between envExec and texec 2017-03-07 14:29:35 -05:00
Makefile State a consistency between envExec and texec 2017-03-07 14:29:35 -05:00
PFun.v Note problem with env to texec theorem statement 2017-03-09 10:27:27 -05:00
Prog.v State a consistency between envExec and texec 2017-03-07 14:29:35 -05:00
README.md Rename repo 2018-01-26 15:13:16 -05:00
Threads.v Note problem with env to texec theorem statement 2017-03-09 10:27:27 -05:00

README.md

Intrumented concurrent semantics

Experiments in defining instrumented semantics for programming languages and proving them sound with respect to lower-level semantics.

Our particular use cases have instrumented semantics where:

  • the semantics defines execution of a single program, abstracting away other threads in terms of a protocol, and
  • ghost state that is shared among all threads but cannot influence program behavior.

The desired primitive semantics should include a scheduler that interleaves a set of threads. Programs proven using the instrumented semantics should be correct under the primitive semantics, so we need a proof that every primitive execution has an instrumented one.