README.md 7.26 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
# GPFSL (iRC11) COQ DEVELOPMENT
Hai Dang's avatar
Hai Dang committed
2

Hai Dang's avatar
Hai Dang committed
3
This is a separation logic for [ORC11] based on [iGPS] and [FSL]. It has been recently renamed as **iRC11**.
Hai Dang's avatar
Hai Dang committed
4 5 6 7 8

## Prerequisites

This version is known to compile with:

Ralf Jung's avatar
Ralf Jung committed
9
 - Coq 8.11.2 / 8.12.0
Hai Dang's avatar
Hai Dang committed
10 11 12 13
 - A development version of [ORC11] and [Iris]. See the [opam](opam) file for the exact
    version.

The easiest way to install the correct versions of the dependencies is through
Ralf Jung's avatar
Ralf Jung committed
14
opam (2.0.0 or newer).  You will need the Coq and Iris opam repositories:
Hai Dang's avatar
Hai Dang committed
15 16

    opam repo add coq-released https://coq.inria.fr/opam/released
Ralf Jung's avatar
Ralf Jung committed
17
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Hai Dang's avatar
Hai Dang committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32

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.

Hai Dang's avatar
Hai Dang committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
## STRUCTURE

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

* [lang/lang.v](theories/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](theories/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](theories/base_logic/vprop.v).
  The points-to assertions `l ↦ v` (Section 3.1) are defined in
  [na.v](theories/base_logic/na.v).
  * [adequacy.v](theories/base_logic/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](theories/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](theories/gps/middleware.v).
    The actual instantiation with raw cancellable invariants can be found in
    [surface.v](theories/gps/surface.v), for example
    `GPS_vSP_Reader`.
  * [surface.v](theories/gps/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](theories/logic) provides the models of various other
  features of the logic.
  * [view_invariants.v](theories/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](theories/logic/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](theories/logic/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](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/bi/monpred.v).

  * [lifting.v](theories/logic/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             |

Hai Dang's avatar
Hai Dang committed
141 142 143 144
* 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](theories/examples/mp_reclaim.v)

Ralf Jung's avatar
Ralf Jung committed
145 146
[ORC11]: https://gitlab.mpi-sws.org/iris/orc11
[Iris]: https://gitlab.mpi-sws.org/iris/iris
Hai Dang's avatar
Hai Dang committed
147 148
[iGPS]: http://plv.mpi-sws.org/igps/
[FSL]: http://plv.mpi-sws.org/fsl/