README.md 11.7 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6
# Iron: Managing Obligations in Higher-Order Concurrent Separation Logic

This repository contains the Iron logic, as described in the POPL'19 paper
"Iron: Managing Obligations in Higher-Order Concurrent Separation Logic" by
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal.

Robbert Krebbers's avatar
Robbert Krebbers committed
7
## Building Iron
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11

Iron has been built and tested with the following dependencies

 - Coq 8.7.1 / 8.7.2 / 8.8.0
Robbert Krebbers's avatar
Robbert Krebbers committed
12
 - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 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 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236

## Directory Structure

- In `theories/algebra` two new cameras are defined.
  1. Improper fractions as a camera without identity with addition as
     the operation are defined in `theories/algebra/vfrac.v`.
  2. The fractional authoritative camera described in Section 5 built
     with improper fractions is defined in
     `theories/algebra/vfrac_auth.v`.

- The semantics of the connectives of the lifted logic are given in
  `theories/bi/fracpred.v`.

    This file does not contain a description of the lifted program
  logic but instead contains the definitions of ∧, ∗, ∀, and other
  the other connectives. It also contains all the rules of the
  specific to this logic that are used later.

- The machinery for connecting the generalized proofmode from
 `iris-coq` to fractional predicates is contained in
 `theories/proofmode`.

- In `theories/iron_logic` much of the core Iron logic discussed
  in Section 2 is defined.

  * Uniformity with respect to fractions is defined in
    `theories/iron_logic/iron.v` as `Uniform` and
    several closure properties of it are proved.
  * Trackable invariants as discussed in Section 2.1 are formalized
    in `theories/iron_logic/fcinv.v`.
  * The definition of weakest preconditions from Section 4 is in
   `theories/iron_logic/weakestpre.v`.

- The formalization specific to the λref,conc is in
  `theories/heap_lang`.

  * The definition of the heap in terms of ghost state from Section
    5 is in `theories/heap_lang/heap.v` as `heapG`. So too are
    the definitions of ↦ and e (in the formalization called `perm`).
  * The theorems stated in Section 5 about updates to the heap ghost
    state are proven in `theories/heap_lang/heap.v`.
  * The state interpretation from Section 5 is defined in
    `theories/heap_lang/heap.v` as `heap_ctx`.
  * Theorems 2.1, 2.2, 4.1, and 4.2 are proven in
    `theories/heap_lang/adequacy.v`.
  * The operational semantics from Figure 4 are defined in
    `theories/heap_lang/lang.v`.
  * The rules from Figures 1, 2, 3, and 5 are proven in
    `theories/heap_lang/lifting.v`.

- All of the examples of the paper are formalized and may be found in
  `theories/heap_lang/lib/`. All of the examples are formalized
  purely within the lifted logic. There is no fraction accounting in
  the proofs and no significant bookkeeping beyond what is found in
  vanilla Iris.
 
    As mentioned in the paper, a small portion of `par` cannot be
  formalized in the lifted logic but in the formalization this is
  factored out into `spawn` in `theories/heap_lang/lib/spawn.v`.

  * The example from 3.1 is in `theories/heap_lang/lib/resource_transfer_par.v`.
  * The example from 3.2 is in `theories/heap_lang/lib/resource_transfer_fork.v`.
  * The example from 3.3 is in `theories/heap_lang/lib/message_passing.v`.
  * The example from 3.4 is in `theories/heap_lang/lib/message_passing_example.v`.
  * The example from 3.5 is in `theories/heap_lang/lib/par.v`.

    Note that `spawn.v`, `resource_transfer_par.v`, and `resource_transfer_fork.v`
  use the same state transition system (from Figure 3). This is formalized in
  `theories/heap_lang/lib/transfer_resource_sts.v`.
   
## Differences Between the Formalization and The Paper

There are a number of small differences between the paper presentation
of Iron and the formalization in Coq. We briefly discuss them here.

### Weakest Preconditions and Texan Triples

In the paper we have worked with Hoare triples in
specifying theorems and rules. In the Iris formalization we have used
weakest preconditions. Weakest preconditions are used for the
definition of Hoare triples (see Section 5) but in the formalization
we also work with them throughout the proofs and in some
specifications. They are often easier more convenient to work with in
Coq because they allow us to use the Iris proofmode context and native
Coq context for manipulating preconditions.

More than this, in the paper we define Hoare triples as follows:

    {P} e {v. Q(v)} ≜ □ (P -∗ wp e {v. Q(v)})

In the Coq formalization this proves to be often unwieldy. Generally
when we has a Hoare triple `{P} e {v.Q(v)}` we use it by applying it to a
goal of the form `wp e {v. Q'(v')}`. With this definition, we must
first apply a lemma about the monotonicity of Hoare triples to obtain
`{P} e {Q'(v)}` from `∀ v. Q(v) -∗ Q'(v)` and then we may apply
this. In Coq we *bake in this cut* with so called Texan Triples,
defined as follows:

    {P} e {v. Q(v)} ≜
      □ ∀ Φ : Val → iProp. P -∗ ▷ (∀ v. Q(v) -∗ Φ(v)) -∗ wp e {v. Φ(v)}

With this formulation we can apply `{P} e {v. Q(v)}` to any goal of the
form `wp e {v. Q'(v)}`, saving a step. Additionally, the fact that we
only need to prove the implication for post-conditions under a ▷ is
a strictly more general requirement.

### Invariant Rules

In the paper all of the invariant rules are stated in terms of Hoare
triples. In Coq this is a needless entangling and a more flexible
collection of invariant rules is used instead.
Specifically, rather than proving rules such as
`LTINV-OPEN` which specify how to open an invariant with a Hoare
triple, we have rules specifying invariants in terms of the fancy
update modality.

This modality was briefly discussed in the paper. It is defined in
`iris-coq/theories/base_logic/lib/fancy_update.v` (as `fupd_def`) and
its adaption to for the the lifted logic is defined in
`theories/iron_logic/iron.v` (as `iron_fupd_def`). Briefly, it's
a frame-preserving update which also allows for the use of invariants.

Since weakest preconditions (and by extension Hoare triples) are
defined with fancy updates the invariant rules written in terms of fancy
updates lift easily to the ones described in the paper.
The paper rules are less flexible though because they only
apply when the goal is a weakest precondition or Hoare triple rather
than any goal with fancy updates.

Instead of the Hoare rule for invariant allocation, for instance, in
the formalization we have `fcinv_alloc_named` from
`theories/iron_logic/fcinv.v` which states that the following
holds:

    ▷ (∀ γ. Ψ γ) -∗
      |={E}=> ∃ γ. fcinv_own γ 1 ∗ fcinv_cancel_own γ 1 ∗ fcinv N γ (Ψ γ)

This can be used to derive `LINV-ALLOC` when used in conjunction with
`HOARE-CONS`. The latter rule is called `ht_vs` in
`iris-coq/theories/program_logic/hoare.v`.

There is a correspondence between the invariant rules presented in the
paper with Hoare triples and those in the formalization.

 - `TINV-ALLOC` and `LTINV-ALLOC` follow from `fcinv_alloc_named`.
 - `TINV-OPEN` and `LTINV-OPEN` follow from `fcinv_open`.
 - `TINV-DEALLOC` and `LTINV-DEALLOC` follow from `fcinv_cancel`.

All of these theorems are proven in `theories/iron_logic/fcinv.v`.

The rules governing normal Iris invariants, such as those for `INV-OPEN`,
are also defined using the fancy update modality. They may be found in
`iris-coq/theories/base_logic/lib/invariants.v`.

## A Correspondence of Theorems, Definitions, and Examples in the Paper to the Formalization

While the correspondence between the contents of the paper and the
formalization is discussed above, we have provided an explicit table
for convenience.

The format of the table is as follows: Name of
Theorem/Rule/Definition/Proposition, the name in the formalization,
and the file in the formalization.

 - The language definition in Section 2, `expr`, `theories/heap_lang/lang.v`
 - `e` and `↦`, `perm` and `↦`, `theories/heap_lang/heap.v`
 - Trackable invariants, `fcinv`, `theories/iron_logic/fcinv.v`
 - `OPerm(-, -)`, `fcinv_own`, `theories/iron_logic/fcinv.v`
 - `DPerm(-, -)`, `fcinv_cancel_own`, `theories/iron_logic/fcinv.v`
 - `HOARE-FRAME`, `hoare_frame_r`, `iris-coq/theories/program_logic/hoare.v`
 - `HOARE-VAL`, `ht_val`, `iris-coq/theories/program_logic/hoare.v`
 - `HOARE-λ`, `pure_rec`, `theories/heap_lang/lifting.v`
 - `HOARE-BIND`, `ht_bind`, `iris-coq/theories/program_logic/hoare.v`
 - `EMP-SPLIT`, `perm_split`, `theories/heap_lang/heap.v`
 - `PT-SPLIT`, `mapsto_uniform`, `theories/heap_lang/heap.v`
 - `PT-DISJ`, `mapsto_valid_2`, `theories/heap_lang/heap.v`
 - `HOARE-ALLOC`, `wp_alloc`, `theories/heap_lang/lifting.v`
 - `HOARE-FREE`, `wp_free`, `theories/heap_lang/lifting.v`
 - `HOARE-LOAD`, `wp_load`, `theories/heap_lang/lifting.v`
 - `HOARE-STORE`, `wp_store`, `theories/heap_lang/lifting.v`
 - `HOARE-FORK-EMP`/`HOARE-FORK-TRUE`, `wp_fork`, `theories/heap_lang/lifting.v`
 - `INV-DUP`, `inv_persistent`, `theories/heap_lang/lifting.v`
 - `INV-ALLOC`, `inv_alloc`, `iris-coq/theories/base_logic/lib/invariants.v`
 - `INV-OPEN`, `inv_open`, `iris-coq/theories/base_logic/lib/invariants.v`
 - `TINV-SPLIT`, `fcinv_own_fractional`, `theories/iron_logic/fcinv.v`
 - `TINV-DUP`, `fcinv_persistent`, `theories/iron_logic/fcinv.v`
 - `TINV-ALLOC`, `fcinv_alloc_named`, `theories/iron_logic/fcinv.v`
 - `TINV-OPEN`, `fcinv_open`, `theories/iron_logic/fcinv.v`
 - `TINV-DEALLOC`, `fcinv_cancel`, `theories/iron_logic/fcinv.v`
 - Uniform with respect to fractions, `Uniform`, `theories/iron_logic/iron.v`
 - `HOARE-CONS`, `ht_vs`, `iris-coq/theories/program_logic/hoare.v`
 - The rules from Figure 4, `head_step`, `theories/heap_lang/lang.v`
 - Theorem 2.1, `heap_adequacy`, `theories/heap_lang/adequacy.v`
 - Theorem 2.2, `heap_strong_adequacy`, `theories/heap_lang/adequacy.v`
 - `HOARE-PAR`, `par_spec`, `theories/heap_lang/lib/par.v`
 - The example from 3.1, `transfer_works1`, `theories/heap_lang/lib/resource_tranfer_par.v`
 - The example from 3.2, `transfer_works1`, `theories/heap_lang/lib/resource_tranfer_fork.v`
 - The example from 3.3, Several theorems, `theories/heap_lang/lib/message_passing.v`
 - The example from 3.4, `program_spec`, `theories/heap_lang/lib/message_passing_example.v`
 - The example from 3.5, Several theorems, `theories/heap_lang/lib/{spawn, par}.v`
 - Definitions of lifted connectives, Several definitions, `theories/bi/fracpred.v`
 - Definition of lifted `↦`, `↦`, `theories/heap_lang/heap.v`
 - `LHOARE-FRAME`, `iron_wp_frame_r`, `iris-coq/theories/program_logic/hoare.v`
 - `LHOARE-VAL`, `iron_wp_val`, `iris-coq/theories/program_logic/hoare.v`
 - `LHOARE-λ`, `pure_rec`, `theories/heap_lang/lifting.v`
 - `LHOARE-BIND`, `iron_wp_bind`, `iris-coq/theories/program_logic/hoare.v`
 - `LPT-DISJ`, `mapsto_valid_2`, `theories/heap_lang/heap.v`
 - `LHOARE-ALLOC`, `iron_wp_alloc`, `theories/heap_lang/lifting.v`
 - `LHOARE-FREE`, `iron_wp_free`, `theories/heap_lang/lifting.v`
 - `LHOARE-LOAD`, `iron_wp_load`, `theories/heap_lang/lifting.v`
 - `LHOARE-STORE`, `iron_wp_store`, `theories/heap_lang/lifting.v`
 - `LHOARE-FORK`, `iron_wp_fork`, `theories/heap_lang/lifting.v`
 - `LTINV-SPLIT`, `fcinv_own_fractional`, `theories/iron_logic/fcinv.v`
 - `LTINV-DUP`, `fcinv_persistent`, `theories/iron_logic/fcinv.v`
 - `LTINV-ALLOC`, `fcinv_alloc_named`, `theories/iron_logic/fcinv.v`
 - `LTINV-OPEN`, `fcinv_open`, `theories/iron_logic/fcinv.v`
 - `LTINV-DEALLOC`, `fcinv_cancel`, `theories/iron_logic/fcinv.v`
 - Definition of Hoare triples, `iron_wp`, `theories/iron_logic/weakestpre.v`
 - Theorem 4.1, `heap_adequacy`, `theories/heap_lang/adequacy.v`
 - Theorem 4.2, `heap_strong_adequacy`, `theories/heap_lang/adequacy.v`
 - Definition of WP in Section 5, `wp_def`, `iris-coq/theories/program_logic/weakestpre.v`
 - Definition of state interp from Section 5, `heap_ctx`, `theories/heap_lang/heap.v`
 - Theorem 5.1, `wp_strong_all_adequacy`, `iris-coq/theories/program_logic/adequacy.v`