README.md 3.22 KB
Newer Older
jihgfee's avatar
Readme    
jihgfee committed
1
2
3
4
5
6
7
8
9
# 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

 - Coq 8.9.1
 - [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) at
Jonas Kastberg's avatar
Jonas Kastberg committed
10
   commit 9041e6d8.
jihgfee's avatar
Readme    
jihgfee committed
11
 - [iris](https://gitlab.mpi-sws.org/iris/iris) at
Jonas Kastberg's avatar
Jonas Kastberg committed
12
   commit 15f1ac56.
jihgfee's avatar
Readme    
jihgfee committed
13
14
15
16
17
18
19
20
21
22
23

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

## Directory structure

### Theory

The theory can be found in `theories/channel`. Some used utilities can be found
in `theories/utils`.

Jonas Kastberg's avatar
Jonas Kastberg committed
24
The files correspond to the following content of the paper:
jihgfee's avatar
Readme    
jihgfee committed
25
26
27

- `theories/channel/channel.v`: The definitional semantics of bidirectional
  channels in HeapLang.
Jonas Kastberg's avatar
Jonas Kastberg committed
28
29
- `theories/channel/proto_model.v`: The CPS model of Dependent Separation
  Protocols.
jihgfee's avatar
Readme    
jihgfee committed
30
31
32
33
34
35
36
37
38
39
40
41
42
- `theories/channel/proto_channel.v`: The definition of the connective `↣` for
  channel ownership and the proof rules of the Actris logic.
- `theories/channel/proofmode.v`: The Coq tactics for symbolic execution.

### Examples

The examples can be found in `theories/examples`.

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

* 1. Introduction: `theories/examples/basics.v`
* 2. Tour of Actris
Jonas Kastberg's avatar
Jonas Kastberg committed
43
44
  * 2.3 Basic: `theories/examples/sort.v`
  * 2.4 Higher-Order Functions: `theories/examples/sort.v`
45
46
47
48
  * 2.5 Branching: `theories/examples/sort_br_del.v`
  * 2.6 Recursion: `theories/examples/sort_br_del.v`
  * 2.7 Delegation: `theories/examples/sort_br_del.v`
  * 2.8 Dependent: `theories/examples/sort_fg.v`
jihgfee's avatar
Readme    
jihgfee committed
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
* 3. Manifest sharing via locks
  * 3.1 Sample program: `theories/examples/basics.v`
  * 3.2 Distributed mapper: `theories/examples/map.v`
* 4. Case study: map reduce:
  * Utilities for shuffling/grouping: `theories/utils/group.v`
  * Implementation and verification: `theories/examples/map_reduce.v`

## 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.

### Connectives for physical ownership of channels

In the paper physical ownership of a channel is formalized using a single
connective `(c1,c2) ↣ (vs1,vs2)`, while the mechanisation 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`

Where `γ` is a ghost name and `N` the invariant used internally. This setup is
less 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).

### Later modalities in primitive rules for channels

The primitive rules for `send` and `recv` (`send_spec` and `recv_spec`) 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: 1.) the `▶` in the CPS encoding of
protocols, 2.) the higher-order ghost state used for ownership of protocols,
3.) the opening of the protocol invariant.