RC11

This repository contains a coq development of the Repaired C11 Memory Model presented in Repairing Sequential Consistency in C/C++11 by Lahav, Vafeiadis, Kang et al.

Compilation

The relation-algebra library is needed to compile the proofs.

You can compile the proofs by running make.

You can generate documentation in HTML format using two different tools:

• With coq2html, you can generate the documentation by running ./generate_doc.sh.

• With coqdoc, you can generate the documentation by running make html.

Files

• util.v : definition of relations, sequencing of relations, acyclicity and useful lemmas about them

• exec.v : definition of a valid and complete program execution. This files contains the definitions of essential notions : events, consistency levels, sequenced-before, reads-from, modification order and read-modify write relations)

• rc11.v : definition of the validity of an execution on the RC11 memory model and on the classical SC model. This files contains the definitions of the derived relations : eco, rs, sw, hb.

• prefix.v : definition of the prefix of an execution and associated lemmas.

• conflict.v : definition of conflicting events and associated lemmas.

• numbering.v : definition of a valid ordering of the events of an execution, and its connection with validity, prefixes and conflicts.

• drf.v : the proof of the DRF-SC property for the RC11 memory model. This file is currently a work in progress