Skip to content
Snippets Groups Projects
Forked from Iris / Actris
239 commits behind the upstream repository.

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

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.