Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
A
Actris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
5
Issues
5
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
Actris
Commits
8a1dbcee
Commit
8a1dbcee
authored
May 07, 2020
by
Jonas Kastberg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Made README less paperspecific
parent
15e9459e
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
19 additions
and
110 deletions
+19
110
README.md
README.md
+19
110
No files found.
README.md
View file @
8a1dbcee
...
...
@@ 14,60 +14,51 @@ In order to build, install the above dependencies and then run
## Theory of Actris
The theory of Actris (semantics of channels, the model, and the proof rules)
can be found in the directory
[
theories/channel
](
theories/channel
)
.
The files
correspond to the following parts of the paper
:
can be found in the directory
[
theories/channel
](
theories/channel
)
.
The individual types contain the following
:

[
theories/channel/channel.v
](
theories/channel/channel.v
)
: The definitional
semantics of bidirectional channels in terms of Iris's HeapLang language.

[
theories/channel/proto_model.v
](
theories/channel/proto_model.v
)
: The
construction of the model of
Dependent Separation P
rotocols as the solution of
construction of the model of
dependent separation p
rotocols as the solution of
a recursive domain equation.

[
theories/channel/proto
_channel.v
](
theories/channel/proto_channel
.v
)
: The

[
theories/channel/proto
.v
](
theories/channel/proto
.v
)
: The
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.
+
`iProto_le`
: The subprotocol relation for protocols.

[
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:
+
`mapsto_proto`
: endpoint ownership
`↣`
.
+
`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
the latter, which is
the rule in the paper
.
the latter, which is
a more legible rule
.
+
`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
the latter, which is
the rule in the paper
.
the latter, which is
a more legible rule
.
+
`select_spec`
: proof rule for
`select`
.
+
`branch_spec`
: proof rule for
`branch`
.
## Notation
The following table gives a mapping between the
notation in the paper and th
e
Coq mechanization:
The following table gives a mapping between the
official notation in literatur
e
and the
Coq mechanization:
 
Paper
 Coq mechanization 
 
Literature
 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`

 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 
## 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 {{ Φ }}
```
## Coq tactics
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
...
...
@@ 151,93 +142,11 @@ defined across the following files:
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.

[
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 typesafe 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 welltyped:

[
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 welltyped 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 welltyped using the semantic typing rules.
Therefore, a manual proof of the welltypedness is given.
 [theories/examples/subprotocols.v](theories/examples/subprotocols.v):
Contains an example of a subprotocol assertion between two protocols that sends
references.
## Examples
The examples can be found in the direction [theories/examples](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](theories/examples/basics.v)
2. Tour of Actris
 2.3 Basic: [theories/examples/sort.v](theories/examples/sort.v)
 2.4 HigherOrder 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)
## 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.
 **Notation**
See the section "Notation" above.
 **Weakest preconditions versus Hoare triples**
See the section "Weakest preconditions and Coq tactics" above.
 **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 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
`
Here, `
γ
` is a ghost name and `
N
` an invariant name. This setup is less
intuitive but gives rise to a more practical Jacobs/Piessensstyle 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
` in
[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:
1. the `
▶
` in the model of protocols,
2. the higherorder ghost state used for ownership of protocols, and
3. the opening of the protocol invariant.
 **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
`
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment