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

This repository contains the Iron logic, as described in the POPL'19 paper
Robbert Krebbers's avatar
Robbert Krebbers committed
4
"[Iron: Managing Obligations in Higher-Order Concurrent Separation Logic](https://iris-project.org/pdfs/2019-popl-iron-final.pdf)" by
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6
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

Iron has been built and tested with the following dependencies

11
 - Coq 8.9.0
Robbert's avatar
Robbert committed
12
 - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq)
Robbert Krebbers's avatar
Robbert Krebbers committed
13
 - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16

## Directory Structure

17 18 19
- In [theories/algebra/ufrac_auth.v](theories/algebra/ufrac_auth.v), the
  fractional authoritative camera described in Section 6 with improper
  fractions is defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
20

Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
- The semantics of the connectives of fractional predicates logic are given in
  [theories/bi/fracpred.v](theories/bi/fracpred.v).
Robbert Krebbers's avatar
Robbert Krebbers committed
23

Robbert's avatar
Robbert committed
24
  This file does not contain a description of the lifted program
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
29
- The machinery for connecting the generalized proofmode/MoSeL from to
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  fractional predicates is contained in [theories/proofmode](theories/proofmode).
Robbert Krebbers's avatar
Robbert Krebbers committed
31

Robbert Krebbers's avatar
Robbert Krebbers committed
32
- In [theories/iron_logic](theories/iron_logic) much of the core Iron logic
Daniel Gratzer's avatar
Daniel Gratzer committed
33
  discussed in Section 3 is defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
  * _Uniformity_ with respect to fractions is defined in
    [theories/iron_logic/iron.v](theories/iron_logic/iron.v) as `Uniform` and
Robbert Krebbers's avatar
Robbert Krebbers committed
36
    several closure properties of it are proved.
Daniel Gratzer's avatar
Daniel Gratzer committed
37
  * _Trackable invariants_ as discussed in Section 3.2 are formalized
Robbert Krebbers's avatar
Robbert Krebbers committed
38
    in [theories/iron_logic/fcinv.v](theories/iron_logic/fcinv.v).
Daniel Gratzer's avatar
Daniel Gratzer committed
39
  * The definition of weakest preconditions from Section 6 is in
Robbert Krebbers's avatar
Robbert Krebbers committed
40
   [theories/iron_logic/weakestpre.v](theories/iron_logic/weakestpre.v).
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42

- The formalization specific to the λref,conc is in
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  [theories/heap_lang](theories/heap_lang).
Daniel Gratzer's avatar
Daniel Gratzer committed
44
  * The definition of the heap in terms of ghost state from Section 6 is in
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
    [theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heapG`. So too
    are the definitions of ↦ and 𝖊 (in the formalization called `perm`).
47
  * The theorems mentioned in Section 6 about updates to the heap ghost
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    state are proven in [theories/heap_lang/heap.v](theories/heap_lang/heap.v).
Daniel Gratzer's avatar
Daniel Gratzer committed
49
  * The state interpretation from Section 6 is defined in
Robbert Krebbers's avatar
Robbert Krebbers committed
50
    [theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heap_ctx`.
Daniel Gratzer's avatar
Daniel Gratzer committed
51
  * Theorems 3.1 and 6.1 are proven in
Robbert Krebbers's avatar
Robbert Krebbers committed
52
    [theories/heap_lang/adequacy.v](theories/heap_lang/adequacy.v).
Daniel Gratzer's avatar
Daniel Gratzer committed
53
  * The operational semantics from Figure 5 are defined in
Robbert Krebbers's avatar
Robbert Krebbers committed
54
    [theories/heap_lang/lang.v](theories/heap_lang/lang.v).
Daniel Gratzer's avatar
Daniel Gratzer committed
55
  * The rules from Figures 4 and 7 are proven in
Robbert Krebbers's avatar
Robbert Krebbers committed
56
    [theories/heap_lang/lifting.v](theories/heap_lang/lifting.v).
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58

- All of the examples of the paper are formalized and may be found in
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60
  [theories/heap_lang/lib/](theories/heap_lang/lib/). All of the examples are
  formalized purely within the lifted logic. There is no fraction accounting in
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62 63
  the proofs and no significant bookkeeping beyond what is found in
  vanilla Iris.
 
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66
  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](theories/heap_lang/lib/spawn.v)
Daniel Gratzer's avatar
Daniel Gratzer committed
67 68 69 70 71
  * The example from 4.1 is in [theories/heap_lang/lib/resource_transfer_par.v](theories/heap_lang/lib/resource_transfer_par.v).
  * The example from 4.2 is in [theories/heap_lang/lib/resource_transfer_fork.v](theories/heap_lang/lib/resource_transfer_fork.v).
  * The example from 4.3 is in [theories/heap_lang/lib/message_passing.v](theories/heap_lang/lib/message_passing.v).
  * The example from 4.4 is in [theories/heap_lang/lib/message_passing_example.v](theories/heap_lang/lib/message_passing_example.v).
  * The example from 4.5 is in [theories/heap_lang/lib/par.v](theories/heap_lang/lib/resource_transfer_par.v).
Robbert Krebbers's avatar
Robbert Krebbers committed
72

Robbert's avatar
Robbert committed
73
  Note that `spawn.v`, `resource_transfer_par.v`, and `resource_transfer_fork.v`
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  use the same state transition system (from Figure 3). This is formalized in
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  [theories/heap_lang/lib/transfer_resource_sts.v](theories/heap_lang/lib/transfer_resource_sts.v).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
   
## 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153
- `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`.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158 159 160 161 162

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

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
While the correspondence between the contents of the paper and the formalization
is discussed above, we also provide an explicit table for convenience.

| Paper definition or theorem |  Coq definition or theorem | File | 
|-------|--------|---------|
| The language definition in Sec. 3 | `expr` | `iron/theories/heap_lang/lang.v` |
| `𝖊` and `↪` | `perm` and `↦` | `iron/theories/heap_lang/heap.v` |
| Trackable invariants | `fcinv` | `iron/theories/iron_logic/fcinv.v` |
| `OPerm(-, -)` | `fcinv_own` | `iron/theories/iron_logic/fcinv.v` |
| `DPerm(-, -)` | `fcinv_cancel_own` | `iron/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` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-BIND` | `ht_bind` | `iris-coq/theories/program_logic/hoare.v` |
| `EMP-SPLIT` | `perm_split` | `iron/theories/heap_lang/heap.v` |
| `PT-SPLIT` | `mapsto_uniform` | `iron/theories/heap_lang/heap.v` |
| `PT-DISJ` | `mapsto_valid_2` | `iron/theories/heap_lang/heap.v` |
| `HOARE-ALLOC` | `wp_alloc` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-FREE` | `wp_free` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-LOAD` | `wp_load` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-STORE` | `wp_store` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-FORK-EMP`/`HOARE-FORK-TRUE` | `wp_fork` | `iron/theories/heap_lang/lifting.v` |
| `INV-DUP` | `inv_persistent` | `iron/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` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-DUP` | `fcinv_persistent` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-ALLOC` | `fcinv_alloc_named` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-OPEN` | `fcinv_open` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-DEALLOC` | `fcinv_cancel` | `iron/theories/iron_logic/fcinv.v` |
| Uniform with respect to fractions | `Uniform` | `iron/theories/iron_logic/iron.v` |
| `HOARE-CONS` | `ht_vs` | `iris-coq/theories/program_logic/hoare.v` |
| The rules from Figure 5 | `head_step` | `iron/theories/heap_lang/lang.v` |
| Theorem 3.1 | `heap_basic_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| Theorem 3.2 | `heap_all_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| `HOARE-PAR` | `par_spec` | `iron/theories/heap_lang/lib/par.v` |
| The example from 4.1 | `transfer_works1` | `iron/theories/heap_lang/lib/resource_transfer_par.v` |
| The rules from Figure 6 | Several theorems | `iron/theories/heap_lang/lib/resource_transfer_sts.v` |
| The example from 4.2 | `transfer_works1` | `iron/theories/heap_lang/lib/resource_transfer_fork.v` |
| The example from 4.3 | Several theorems | `iron/theories/heap_lang/lib/message_passing.v` |
| The queue specifications from 4.3 | Several theorems in Section `queue_bag_spec` | `iron/theories/heap_lang/lib/queue.v` |
| The example from 4.4 | `program_spec` | `iron/theories/heap_lang/lib/message_passing_example.v` |
| The example from 4.5 | Several theorems | `iron/theories/heap_lang/lib/{spawn,par}.v` |
| Definitions of lifted connectives | Several definitions | `iron/theories/bi/fracpred.v` |
| Definition of lifted `↦` | `↦` | `iron/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` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-BIND` | `iron_wp_bind` | `iris-coq/theories/program_logic/hoare.v` |
| `LPT-DISJ` | `mapsto_valid_2` | `iron/theories/heap_lang/heap.v` |
| `LHOARE-ALLOC` | `iron_wp_alloc` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-FREE` | `iron_wp_free` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-LOAD` | `iron_wp_load` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-STORE` | `iron_wp_store` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-FORK` | `iron_wp_fork` | `iron/theories/heap_lang/lifting.v` |
| `LTINV-SPLIT` | `fcinv_own_fractional` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-DUP` | `fcinv_persistent` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-ALLOC` | `fcinv_alloc_named` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-OPEN` | `fcinv_open` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-DEALLOC` | `fcinv_cancel` | `iron/theories/iron_logic/fcinv.v` | 
| Definition of Hoare triples | `iron_wp` | `iron/theories/iron_logic/weakestpre.v` |
| Theorem 5.1 | `heap_basic_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| Theorem 5.2 | `heap_all_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| Definition of WP in Section 6 | `wp_def` | `iris-coq/theories/program_logic/weakestpre.v` |
| Definition of state interpretation from Section 6 | `heap_ctx` | `iron/theories/heap_lang/heap.v` |
| Theorem 6.1 | `wp_strong_all_adequacy` | `iris-coq/theories/program_logic/adequacy.v` |
| The lock specifications | Several theorems | `iron/theories/heap_lang/lib/spin_lock_track.v` |
| Adequacy for the lock | `lock_always_freed` | `iron/theories/heap_lang/lib/spin_lock_track.v` |