GPFSL (iRC11) COQ DEVELOPMENT

This is a separation logic for ORC11 based on iGPS and FSL. It has been recently renamed as iRC11.

Prerequisites

This version is known to compile with:

• Coq 8.13.2
• A development version of ORC11 and Iris. See the opam file for the exact version.

The easiest way to install the correct versions of the dependencies is through opam (2.0.0 or newer). You will need the Coq and Iris opam repositories:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Once you got opam set up, run make build-dep to install the right versions of the dependencies.

Updating

After doing git pull, the development may fail to compile because of outdated dependencies. To fix that, please run opam update followed by make build-dep.

Building Instructions

Run make -jN to build the full development, where N is the number of your CPU cores.

STRUCTURE

iRC11 formalizes the actual language of RBrlx, as well as the logic for general verification of programs written that language.

• lang/lang.v defines the language as a combination of ORC11 and a CPS-style expression language following that of lambda-Rust.

  • The expression language is defined with base.head_step.
  • The complete language combines base.head_step, lbl_machine_step, drf_pre, and drf_post into head_step.

• base_logic is the instantiation of the language in Iris. The view-predicate assertion type vProp (Section 3.1, 4.2 of the RBrlx paper) is defined in vprop.v. The points-to assertions l ↦ v (Section 3.1) are defined in na.v.

  • adequacy.v proves that expressions verified in the base logic are actually safe and functionally correct. Since iRC11 is built on the base logic, this in turn implies that expressions verified in iRC11 are also safe and functionally correct.

• gps provides the model of iRC11 single-location cancellable invariants (Section 3.2, 4.4). Note that iRC11 single-location invariants presented in the paper are only a very simplified version of what we actually need in Coq.

  • The ATOM definition (iRC11-CInv-Model, Section 4.4) is called GPS_INV in Coq, see GPS_INV_def in middleware.v. The actual instantiation with raw cancellable invariants can be found in surface.v, for example GPS_vSP_Reader.

  • surface.v contains a single-writer instance of iRC11 single-location cancellable invariants. The following table lists the rules that are similar but not exactly the same as the rules presented in Section 3 of the RBrlx paper, because in Coq they are more powerful and hence more complicated.

    Proof Rule (Fig. 3)	File	Similar lemma
    iRC11-CInv-New	surface.v	GPS_vSP_Init
    iRC11-CInv-FAA-Rlx	surface.v	GPS_vSP_SWWrite_rel
    iRC11-CInv-FAA-Rlx	surface.v	GPS_vSP_Read
    iRC11-CInv-Cancel	surface.v	GPS_vSP_dealloc

    The rule iRC11-CInv-Tok is exactly the rule Raw-CInv-Tok (see below), because single-location cancellable invariants are built from raw cancellable invariants.

    More details on the single-writer invariants can be found in Section 5 of the technical appendix of the RBrlx paper.

• logic provides the models of various other features of the logic.

  • view_invariants.v provides the model of raw cancellable invariants (Section 4.2, 4.3). So in Coq, raw cancellable invariants are call view invariants.

    In Coq, raw cancellable invariants have more complex rules than what were presented in the paper. Below is only the mapping of rules in the paper to Coq.

    Definition (Sect. 4.3)	File	Definition
    Raw-CInv-Model-Tok	view_invariants.v	view_tok_def
    Raw-CInv-Model	view_invariants.v	view_inv_def

    Proof Rule (Fig. 7)	File	Lemma
    Raw-CInv-New	view_invariants.v	view_inv_alloc
    Raw-CInv-Tok	view_invariants.v	view_tok_asfractional
    Raw-CInv-Acc	view_invariants.v	view_inv_acc_consume
    Raw-CInv-Cancel	view_invariants.v	view_inv_dealloc

    Note that the access rule Raw-CInv-Acc is given Coq with Iris style, where viewshifts are used instead of Hoare triples.

  • relacq.v provides the model of fence modalities (Section 5.2).

    Definition (Sect. 5.2)	File	Definition
    RelMod-Model	relacq.v	rel_mod_def
    AcqMod-Model	relacq.v	acq_mod_def

  • The Ghost-Mod rule is realized by rel_embed_elim and acq_embed_elim (in relacq.v), because ghost elements are embedded in iRC11 directly from Iris.

    If ownGhost(γ,a) is the ghost ownership assertion in Iris (dashed box in Fig. 3 of the paper), then ⎡ownGhost(γ,a)⎤ is the ghost ownership assertion in iRC11. The embedding modality ⎡·⎤ is defined with monPred_embed_def in Iris's monPred.v.

  • lifting.v provides the rules of various features around Hoare triples. In Iris's Coq, we use weakest preconditions wp instead of Hoare triples. Again, not all rules are exact matches with what were presented in the paper. For example, allocation and deallocation of locations additionally involve the freeable resource ⎡†l…n⎤.

    Proof Rule (Fig. 3)	File	Lemma
    Dealloc	lifting.v	wp_free
    NA-Read	lifting.v	wp_read_non_atomic
    NA-Write	lifting.v	wp_write_non_atomic
    Rel-Fence	lifting.v	wp_rel_fence
    Acq-Fence	lifting.v	wp_acq_fence

• An example verification of the Message-Passing example, which has stronger resource reclamation than both examples given in Figure 4 of the RBrlx paper, is given in examples/mp_reclaim.v