README.md 10.2 KB
Newer Older
jihgfee's avatar
Readme  
jihgfee committed
1
2
# ACTRIS COQ DEVELOPMENT

Jonas Kastberg's avatar
Jonas Kastberg committed
3
4
This repository contains:
- The Coq mechanization of the Actris framework, first presented in the paper
Robbert Krebbers's avatar
Robbert Krebbers committed
5
[Actris: Session Type Based Reasoning in Separation Logic](https://iris-project.org/pdfs/2020-popl-actris-final.pdf)
6
at POPL'20
Jonas Kastberg's avatar
Jonas Kastberg committed
7
- The logical relations model for a semantic session type system, first presented in
Jonas Kastberg's avatar
Jonas Kastberg committed
8
9
the paper
[Machine-Checked Semantic Session Typing](https://iris-project.org/pdfs/2021-cpp-sessions-final.pdf)
jihgfee's avatar
Readme  
jihgfee committed
10
11
12

It has been built and tested with the following dependencies

Ralf Jung's avatar
Ralf Jung committed
13
 - Coq 8.15.1
Robbert Krebbers's avatar
Robbert Krebbers committed
14
 - The version of Iris in the [opam file](opam)
jihgfee's avatar
Readme  
jihgfee committed
15
16
17
18

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
19
20
## Theory of Actris

Robbert Krebbers's avatar
Robbert Krebbers committed
21
The theory of Actris (semantics of channels, the model, and the proof rules)
22
23
can be found in the directory [theories/channel](theories/channel).
The individual types contain the following:
Robbert Krebbers's avatar
Robbert Krebbers committed
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
- [theories/channel/proto_model.v](theories/channel/proto_model.v): The
26
  construction of the model of dependent separation protocols as the solution of
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  a recursive domain equation.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
- [theories/channel/proto.v](theories/channel/proto.v): The instantiation of
  protocols with the Iris logic, definition of `iProto_own` for channel endpoint
  ownership, and lemmas corresponding to the Actris proof rules.
31
32
33
34
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  + `iProto_le`: The subprotocol relation for protocols (notation `⊑`).
36
37
38
39
- [theories/channel/channel.v](theories/channel/channel.v): The encoding of
  bidirectional channels in terms of Iris's HeapLang language, with specifications
  defined in terms of the dependent separation protocols.
  The relevant definitions and proof rules are as follows:
40
  + `iProto_mapsto`: endpoint ownership (notation `↣`).
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  + `new_chan_spec`, `send_spec` and `recv_spec`: proof rule for `new_chan`,
Jonas Kastberg's avatar
Jonas Kastberg committed
42
	`send`, and `recv`.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  + `select_spec` and `branch_spec`: proof rule for the derived (binary)
Jonas Kastberg's avatar
Jonas Kastberg committed
44
	`select` and `branch` operations.
Robbert Krebbers's avatar
Robbert Krebbers committed
45

46
47
## Notation

Jonas Kastberg's avatar
Jonas Kastberg committed
48
The following table gives a mapping between the notation in literature
49
and the Coq mechanization:
50

Jonas Kastberg's avatar
Jonas Kastberg committed
51
52
Dependent Separation Protocols:

53
|        | POPL20 paper                  | Coq mechanization                     |
Robbert Krebbers's avatar
Robbert Krebbers committed
54
|--------|-------------------------------|---------------------------------------|
55
56
| 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`  |
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
| 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                           |
62

63
64
This notation is additionally used for the LMCS submission.

Jonas Kastberg's avatar
Jonas Kastberg committed
65
66
Semantic Session Types:

67
68
69
70
71
72
73
74
75
|          | CPP21 submission              | Coq mechanization                     |
|----------|-------------------------------|---------------------------------------|
| Send     | `!_{X_1 .. X_n} A . S`        | `<!! X_1 .. X_n> TY A ; S`            |
| Recv     | `?_{X_1 .. X_n} A . S`        | `<?? X_1 .. X_n> TY A ; S`            |
| End      | `end`                         | `END`                                 |
| Select   | `(+){ Ss }`                   | `lty_choice SEND Ss`                  |
| Branch   | `&{ Ss }`                     | `lty_choice RECV Ss`                  |
| Dual     | An overlined type             | No notation                           |
| N-append | `S^n`                         | lty_napp S n                          |
Jonas Kastberg's avatar
Jonas Kastberg committed
76

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

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.

107
108
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
109
channel with the protocol `iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot)`.
110
111
112
113
114
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
115
- It distributes duals (`iProto_dual`) over append (`<++>`).
116
117
118
119
120
121
- 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
122
123
124
125
[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
126
## Semantic Session Type System
Jonas Kastberg's avatar
Jonas Kastberg committed
127

Jonas Kastberg's avatar
Jonas Kastberg committed
128
The logical relation for type safety of a semantic session type system is contained
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
in the directory [theories/logrel](theories/logrel).
The logical relation is defined across the following files:
Jonas Kastberg's avatar
Jonas Kastberg committed
131
132
133
134
135
136
137

- [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
138
  of the following semantic term types: basic types (integers, booleans, unit),
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
  sums, products, copyable/affine functions, universally and existentially
  quantified types, unique/shared references, and session-typed channels.
Jonas Kastberg's avatar
Jonas Kastberg committed
141
142
143
- [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
144
145
146
147
  defined here. Recursive session types can be defined using the mechanism
  defined in [theories/logrel/model.v](theories/logrel/model.v).
- [theories/logrel/operators.v](theories/logrel/operators.v):
  Type definitions of unary and binary operators.
148
149
150
- [theories/logrel/contexts.v](theories/logrel/contexts.v):
  Definition of the semantic type contexts, which is used in the semantic
  typing relation. This also contains the rules for updating the context,
151
152
  which is used for distributing affine resources across the
  various parts of the proofs inside the typing rules.
Jonas Kastberg's avatar
Jonas Kastberg committed
153
154
155
- [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.
156
157
158
- [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.
159
160
- [theories/logrel/subtyping_rules.v](theories/logrel/subtyping_rules.v):
  Subtyping rules for term types and session types.
Jonas Kastberg's avatar
Jonas Kastberg committed
161
162
- [theories/logrel/term_typing_rules.v](theories/logrel/term_typing_rules.v):
  Semantic typing lemmas (typing rules) for the semantic term types.
163
- [theories/logrel/session_typing_rules.v](theories/logrel/session_typing_rules.v):
Jonas Kastberg's avatar
Jonas Kastberg committed
164
  Semantic typing lemmas (typing rules) for the semantic session types.
165
166
167
168
- [theories/logrel/napp.v](theories/logrel/napp.v):
  Definition of session types iteratively being appended to themselves a finite
  number of times, with support for swapping e.g. a send over an arbitrary number
  of receives.
Jonas Kastberg's avatar
Jonas Kastberg committed
169
170
171
172

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
173
and allow one to gain exclusive ownership of resources shared between multiple
174
175
176
threads. An encoding of a list type is found in
[theories/logrel/lib/mutex.v](theories/logrel/lib/mutex.v), along with axillary
lemmas, and a weakest precondition for `llength`,
177
178
that converts ownership of a list type into a list reference predicate, with
the values of the list made explicit.
179
180
181

## Paper-specific remarks

Jonas Kastberg's avatar
Jonas Kastberg committed
182
183
For remarks about the paper-specific submissions, see

184
185
186
- [papers/POPL20.md](papers/POPL20.md)
- [papers/CPP21.md](papers/CPP21.md)
- [papers/LMCS.md](papers/LMCS.md)