Merge branch 'daniel/readme' into 'master'

Update README.md

See merge request !17

README.md

@@ -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 Protocols as the solution of
+  construction of the model of dependent separation protocols 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 the
-Coq mechanization:
+The following table gives a mapping between the official notation in literature
+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
@@ -116,71 +107,46 @@ Concretely, the normalization performs the following actions:
 [ProofMode]: https://gitlab.mpi-sws.org/iris/iris/blob/master/ProofMode.md
 [ActrisProofMode]: theories/channel/proofmode.v
 
-## 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 Higher-Order 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/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` 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 higher-order 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`.
-
+## Semantic Session Type System
+The logical relation for type safety of a semantic session type system is contained
+in the directory [theories/logrel](theories/logrel). The logical relation is
+defined across the following files:
+
+- [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
+  of the following semantic term types: basic types (integers, booleans,
+  unit), sums, products, copyable/affine functions, universally and
+  existentially quantified types, unique/shared references, and
+  session-typed channels.
+- [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
+  defined here. As mentioned, recursive session types can be defined using
+  the mechanism defined in [theories/logrel/model.v](theories/logrel/model.v).
+- [theories/logrel/environments.v](theories/logrel/environments.v):
+  Definition of semantic type environments, which are used in the semantic
+  typing relation. This also contains the rules for splitting and copying of
+  environments, which is used for distributing affine resources across the
+  various parts of the program inside the typing rules.
+- [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.
+- [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.
+- [theories/logrel/term_typing_rules.v](theories/logrel/term_typing_rules.v):
+  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.
+
+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
+and allow one to gain exclusive ownership of resource shared between multiple
+threads.