-
Jonas Kastberg authoredJonas Kastberg authored
Examples
The examples can be found in the directory theories/examples.
The following list gives a mapping between the examples in the paper and their mechanization in Coq:
Introduction: theories/examples/basics.v Tour of Actris
- Basics: theories/examples/sort.v
- Higher-Order Functions: theories/examples/sort.v
- Choice: theories/examples/sort_br_del.v
- Recursion: theories/examples/sort_br_del.v
- Delegation: theories/examples/sort_br_del.v
- Dependent: theories/examples/sort_fg.v Manifest sharing via locks
- Sample program: theories/examples/basics.v
- Distributed mapper: theories/examples/par_map.v 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.
Weakest preconditions versus Hoare triples
The presentation of the 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 {{ Φ }}
Connectives for physical ownership of channels
In the paper, physical ownership of a channel is formalized using a single
connective (c1,c2) ↣ (vs1,vs2)
. Since then we have made the Actris
hoare triples the primitive specification for the channels, and instead
defined channel ownership directly in terms of the buffer ownership
llist internal_eq l vs1
and llist intenral_eq r vs2
for channels
(l,r,lk)
and (r,l,lk)
.
Protocol subtyping
The mechanization has introduced the notion of "protocol subtyping", which
allows one to strengthen/weaken the predicates of sends/receives, respectively.
This is 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
.
This idea is formally presented in the LMCS submission.