README.md 13 KB
Newer Older
jihgfee's avatar
Readme  
jihgfee committed
1 2 3 4 5 6 7
# ACTRIS COQ DEVELOPMENT

This directory contains the artifact for the paper "Actris: Session Type
Based Reasoning in Separation Logic".

It has been built and tested with the following dependencies

Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
 - Coq 8.11.1
 - The version of Iris in the [opam file](opam)
jihgfee's avatar
Readme  
jihgfee committed
10 11 12 13

In order to build, install the above dependencies and then run
`make -j [num CPU cores]` to compile Actris.

Robbert Krebbers's avatar
Robbert Krebbers committed
14 15
## Theory of Actris

Robbert Krebbers's avatar
Robbert Krebbers committed
16
The theory of Actris (semantics of channels, the model, and the proof rules)
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18 19 20 21
can be found in the directory [theories/channel](theories/channel). The files
correspond to the following parts of the paper:

- [theories/channel/channel.v](theories/channel/channel.v): The definitional
  semantics of bidirectional channels in terms of Iris's HeapLang language.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24
- [theories/channel/proto_model.v](theories/channel/proto_model.v): The
  construction of the model of Dependent Separation Protocols as the solution of
  a recursive domain equation.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
- [theories/channel/proto_channel.v](theories/channel/proto_channel.v): The
26 27 28 29 30 31 32
  instantiation of protocols with the Iris logic, definition of the connective `↣`
  for channel endpoint ownership, and lemmas corresponding to the Actris proof rules.
  The relevant definitions and proof rules are as follows:
  + `iProto Σ`: The type of protocols.
  + `iProto_message`: The constructor for sends and receives.
  + `iProto_end`: The constructor for terminated protocols.
  + `mapsto_proto`: endpoint ownership `↣`.
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35
  + `new_chan_proto_spec`: proof rule for `new_chan`.
  + `send_proto_spec` and `send_proto_spec_packed`: proof rules for `send`, the
    first version is more convenient to use in Coq, but otherwise the same as
Robbert Krebbers's avatar
Robbert Krebbers committed
36
    the latter, which is the rule in the paper.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38
  + `recv_proto_spec` and `recv_proto_spec_packed`: proof rules for `recv`, the
    first version is more convenient to use in Coq, but otherwise the same as
Robbert Krebbers's avatar
Robbert Krebbers committed
39
    the latter, which is the rule in the paper.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42
  + `select_spec`: proof rule for `select`.
  + `branch_spec`: proof rule for `branch`.

43 44
## Notation

Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
The following table gives a mapping between the notation in the paper and the
Coq mechanization:
47

Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51 52 53 54 55 56
|        | Paper                         | Coq mechanization                     |
|--------|-------------------------------|---------------------------------------|
| Send   | `! x_1 .. x_n <v>{ P }. prot` | `<!> x_1 .. x_n, MSG v {{ P }}; prot` |
| Recv   | `? x_1 .. x_n <v>{ P }. prot` | `<?> x_1 .. x_n, MSG v {{ P }}; prot` |
| End    | `end`                         | `END`                                 |
| Select | `prot_1 {Q_1}⊕{Q_2} prot_2`   | `prot_1 <{Q_1}+{Q_2}> prot_2`         |
| Branch | `prot_1 {Q_1}&{Q_2} prot_2`   | `prot_1 <{Q_1}&{Q_2}> prot_2`         |
| Append | `prot_1 · prot_2`             | `prot_1 <++> prot_2`                  |
| Dual   | An overlined protocol         | No notation                           |
57

Robbert Krebbers's avatar
Robbert Krebbers committed
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
## Weakest preconditions and Coq tactics

The presentation of Actris logic in the paper makes use of Hoare triples. In
Coq, we make use of weakest preconditions because these are more convenient for
interactive theorem proving using the the [proof mode tactics][ProofMode]. To
state concise program specifications, we use the notion of *Texan Triples* from
Iris, which provides a convenient "Hoare triple"-like syntax around weakest
preconditions:

```
{{{ P }}} e {{{ x .. y, RET v; Q }}} :=
  □ ∀ Φ, P -∗ ▷ (∀ x .. y, Q -∗ Φ v) -∗ WP e {{ Φ }}
```

In order to prove programs using Actris, one can make use of a combination of
[Iris's symbolic execution tactics for HeapLang programs][HeapLang] and
[Actris's symbolic execution tactics for message passing][ActrisProofMode]. The
Actris tactics are as follows:

- `wp_send (t1 .. tn) with "selpat"`: symbolically execute `send c v` by looking
  up ownership of a send protocol `H : c ↣ <!> y1 .. yn, MSG v; {{ P }}; prot`
  in the proof mode context. The tactic instantiates the variables `y1 .. yn`
  using the terms `t1 .. tn` and uses `selpat` to prove `P`. If fewer terms
  `t` are given than variables `y`, they will be instantiated using existential
  variables (evars). The tactic will put `H : c ↣ prot` back into the context.
- `wp_recv (x1 .. xn) as "ipat"`: symbolically execute `recv c` by looking up
  `H : c ↣  <?> y1 .. yn, MSG v; {{ P }}; prot` in the proof mode context. The
  variables `y1 .. yn` are introduced as `x1 .. xn`, and the predicate `P` is
  introduced using the introduction pattern `ipat`. The tactic will put
  `H : c ↣ prot` back into the context.
- `wp_select with "selpat"`: symbolically execute `select c b` by looking up
  `H : c ↣  prot1 {Q1}<+>{Q2} prot2` in the proof mode context. The selection
  pattern `selpat` is used to resolve either `Q1` or `Q2`, based on the chosen
  branch `b`. The tactic will put `H : c ↣  prot1` or `H : c ↣ prot2` back
  into the context based on the chosen branch `b`.
- `wp_branch as ipat1 | ipat2`: symbolically execute `branch c e1 e2` by looking
  up `H : c ↣ prot1 {Q1}<&>{Q2} prot2` in the proof mode context. The result of
  the tactic involves two subgoals, in which `Q1` and `Q2` are introduced using
  the introduction patterns `ipat1` and `ipat2`, respectively. The tactic will
  put `H : c ↣ prot1` and `H : c ↣ prot2` back into the contexts of the two
  respectively goals.

100 101
The above tactics implicitly perform normalization of the protocol `prot` in
the hypothesis `H : c ↣ prot`. For example, `wp_send` also works if there is a
Jonas Kastberg's avatar
Jonas Kastberg committed
102
channel with the protocol `iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot)`.
103 104 105 106 107
Concretely, the normalization performs the following actions:

- It re-associates appends (`<++>`), and removes left-identities (`END`) of it.
- It moves appends (`<++>`) into sends (`<!>`), receives (`<?>`), selections
  (`<+>`) and branches (`<&>`).
Jonas Kastberg's avatar
Jonas Kastberg committed
108
- It distributes duals (`iProto_dual`) over append (`<++>`).
109 110 111 112 113 114
- It unfolds `prot1` into `prot2` if there is an instance of the type class
  `ProtoUnfold prot1 prot2`. When defining a recursive protocol, it is
  useful to define a `ProtoUnfold` instance to obtain automatic unfolding
  of the recursive protocol. For example, see `sort_protocol_br_unfold` in
  [theories/examples/sort_br_del.v](theories/examples/sort_br_del.v).

Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117 118
[HeapLang]: https://gitlab.mpi-sws.org/iris/iris/blob/master/HeapLang.md
[ProofMode]: https://gitlab.mpi-sws.org/iris/iris/blob/master/ProofMode.md
[ActrisProofMode]: theories/channel/proofmode.v

Jonas Kastberg's avatar
Jonas Kastberg committed
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
## Semantic Session Type System
The logical relation for type safety of a semantic session type system is contained
in the directory [theories/logrel](theories/logrel). The logical relation is
defined across the following files:

- [theories/logrel/model.v](theories/logrel/model.v): Definition of the
  notions of a semantic term type and a semantic session type in terms of
  unary Iris predicates (on values) and Actris protocols, respectively. Also
  provides the required Coq definitions for creating recursive term/session
  types.
- [theories/logrel/term_types.v](theories/logrel/term_types.v): Definitions
  of the following semantic term types: basic types (integers, booleans,
  unit), sums, products, copyable/affine functions, universally and
  existentially quantified types, unique/shared references, and
  session-typed channels.
- [theories/logrel/session_types.v](theories/logrel/session_types.v):
  Definitions of the following semantic session types: sending and receiving
  with session polymorphism, n-ary choice. Session type duality is also
  defined here. As mentioned, recursive session types can be defined using
  the mechanism defined in [theories/logrel/model.v](theories/logrel/model.v).
- [theories/logrel/environments.v](theories/logrel/environments.v):
  Definition of semantic type environments, which are used in the semantic
  typing relation. This also contains the rules for splitting and copying of
  environments, which is used for distributing affine resources across the
  various parts of the program inside the typing rules.
- [theories/logrel/term_typing_judgment.v](theories/logrel/term_typing_judgment.v):
  Definition of the semantic typing relation, as well as the proof of type
  soundness, showing that semantically well-typed programs do not get stuck.
- [theories/logrel/subtyping.v](theories/logrel/subtyping.v): Definition of
  the semantic subtyping relation for both term and session types. This file
  also defines the notion of copyability of types in terms of subtyping.
- [theories/logrel/term_typing_rules.v](theories/logrel/term_typing_rules.v):
  Semantic typing lemmas (typing rules) for the semantic term types.
- [theories/logrel/session_typing_rules.v](theories/logrel/session.v):
  Semantic typing lemmas (typing rules) for the semantic session types.
- [theories/logrel/subtyping_rules.v](theories/logrel/subtyping_rules.v): Subtyping rules for term types and
  session types.

An extension to the basic type system is given in
[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), which defines
mutexes as a type-safe abstraction. Mutexes are implemented using spin locks
and allow one to gain exclusive ownership of resource shared between multiple
threads.

The logical relation is used to show that two example programs are semantically well-typed:
- [theories/logrel/examples/pair.v](theories/logrel/examples/pair.v):
  This program performs
  two sequential receives and stores the results in a pair. It is shown to be
  semantically well-typed by applying the semantic typing rules.
- [theories/logrel/examples/double.v](theories/logrel/examples/double.v): This program
  performs two ``racy'' parallel receives on the same channel from two
  different threads, using locks to allow the channel to be shared. This
  program cannot be shown to be well-typed using the semantic typing rules.
  Therefore, a manual proof of the well-typedness is given.
- [theories/examples/subprotocols.v](theories/examples/subprotocols.v):
  Contains an example of a subprotocol assertion between two protocols that sends
  references.

Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179
## Examples

The examples can be found in the direction [theories/examples](theories/examples).
jihgfee's avatar
Readme  
jihgfee committed
180 181 182 183

The following list gives a mapping between the examples in the paper and their
mechanization in Coq:

Robbert Krebbers's avatar
Robbert Krebbers committed
184 185 186 187 188 189 190 191 192 193 194 195 196 197
1. Introduction: [theories/examples/basics.v](theories/examples/basics.v)
2. Tour of Actris
   - 2.3 Basic: [theories/examples/sort.v](theories/examples/sort.v)
   - 2.4 Higher-Order Functions: [theories/examples/sort.v](theories/examples/sort.v)
   - 2.5 Branching: [theories/examples/sort_br_del.v](theories/examples/sort_br_del.v)
   - 2.6 Recursion: [theories/examples/sort_br_del.v](theories/examples/sort_br_del.v)
   - 2.7 Delegation: [theories/examples/sort_br_del.v](theories/examples/sort_br_del.v)
   - 2.8 Dependent: [theories/examples/sort_fg.v](theories/examples/sort_fg.v)
3. Manifest sharing via locks
   - 3.1 Sample program: [theories/examples/basics.v](theories/examples/basics.v)
   - 3.2 Distributed mapper: [theories/examples/map.v](theories/examples/map.v)
4. Case study: map reduce:
   - Utilities for shuffling/grouping: [theories/utils/group.v](theories/utils/group.v)
   - Implementation and verification: [theories/examples/map_reduce.v](theories/examples/map_reduce.v)
jihgfee's avatar
Readme  
jihgfee committed
198 199 200 201 202 203

## Differences between the formalization and the paper

There are a number of small differences between the paper presentation
of Actris and the formalization in Coq, that are briefly discussed here.

204 205 206 207
- **Notation**

  See the section "Notation" above.

Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210
- **Weakest preconditions versus Hoare triples**

  See the section "Weakest preconditions and Coq tactics" above.
211

Robbert's avatar
Robbert committed
212 213
- **Connectives for physical ownership of channels**

Robbert's avatar
Robbert committed
214
  In the paper, physical ownership of a channel is formalized using a single
Robbert Krebbers's avatar
Robbert Krebbers committed
215 216 217 218
  connective `(c1,c2) ↣ (vs1,vs2)`, while the mechanization has two connectives
  for the endpoints and one for connecting them, namely:
  - `chan_own γ Left vs1` and `chan_own γ Right vs1`
  - `is_chan N γ c1 c2`
Daniël Louwrink's avatar
Daniël Louwrink committed
219

Robbert's avatar
Robbert committed
220
  Here, `γ` is a ghost name and `N` an invariant name. This setup is less
Robbert Krebbers's avatar
Robbert Krebbers committed
221 222 223
  intuitive but gives rise to a more practical Jacobs/Piessens-style spec of
  `recv` that does not need a closing view shift (to handle the case that the
  buffer is empty).
Robbert Krebbers's avatar
Robbert Krebbers committed
224

Robbert's avatar
Robbert committed
225 226
- **Later modalities in primitive rules for channels**

Robbert's avatar
Robbert committed
227
  The primitive rules for `send` and `recv` (`send_spec` and `recv_spec` in
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229 230 231 232
  [theories/channel/channel.v](theories/channel/channel.v)) contain three later
  (``) modalities, which are omitted for brevity's sake in the paper. These
  later modalities expose that these operations perform at least three steps in
  the operational semantics, and are needed to deal with the three levels of
  indirection in the invariant for protocols:
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  1. the `` in the model of protocols,
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235
  2. the higher-order ghost state used for ownership of protocols, and
  3. the opening of the protocol invariant.
236

Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239 240 241 242 243
- **Protocol subtyping**

  The mechanization has introduced the notion of "protocol subtyping", which
  allows one to strengthen/weaken the predicates of sends/receives, respectively.
  This achieved using the relation `iProto_le p p'`, and the additional rule
  `c ↣ p -∗ iProto_le p p' -∗ c ↣ p'`. To support "protocol subtyping", the
  definition of `c ↣ p` in the model is changed to be closed under `iProto_le`.