SessionTypes: commented

SessionTypes.v

@@ -9,22 +9,43 @@ Set Implicit Arguments.
 Set Asymmetric Patterns.
 
 
+(* One natural view of process algebra is as a way of orchestrating multiple
+ * agents that communicate with each other through prearranged protocols.
+ * Session types are a way of doing static analysis, in the style of type
+ * checking as we saw in earlier chapters, to guarantee that agents play well
+ * together.  Specifically, in this chapter, we'll confine our attention to
+ * avoiding stuckness: a set of agents should either reach a state where
+ * everyone is done or should continue stepping forever.  A counterexample would
+ * be a configuration where each of two agents is blocked waiting for input from
+ * the other -- a classic deadlock. *)
+
+
 (** * Basic Two-Party Session Types *)
 
+(* We'll consider some gradations of fanciness in our session type systems.
+ * Even the final version will have some notable expressiveness weaknesses, but
+ * we'll still be able to handle a variety of nontrivial protocols.  Each
+ * variant will be confined to its own module, allowing us to reuse names. *)
+
 Module BasicTwoParty.
 
 (** ** Defining the type system *)
 
 Inductive type :=
 | TSend (ch : channel) (A : Set) (t : type)
+(* This type applies to a process that begins by sending a value of type [A]
+ * over channel [ch], then continuing according to type [t]. *)
+
 | TRecv (ch : channel) (A : Set) (t :  type)
+(* This type is the dual of the last one: the process begins by receiving a
+ * value of type [A] from channel [ch]. *)
+
 | TDone.
+(* This type describes processes that are done.  Notice that we make our lives
+ * easier by not supporting any of the other constructs (parallel composition,
+ * duplication, ...) from our process algebra! *)
 
-Delimit Scope st_scope with st.
+(* The typing rules mostly just formalize the comments from above. *)
-Bind Scope st_scope with type.
-Notation "!!! ch ( A ) ; k" := (TSend ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope.
-Notation "??? ch ( A ) ; k" := (TRecv ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope.
-
 Inductive hasty : proc -> type -> Prop :=
 | HtSend : forall ch (A : Set) (v : A) k t,
     hasty k t
@@ -34,7 +55,22 @@ Inductive hasty : proc -> type -> Prop :=
     -> hasty (Recv ch k) (TRecv ch A t)
 | HtDone :
     hasty Done TDone.
+(* Notice, though, that the premise of [HtRecv] does quantification over all
+ * possible values that might come down the channel [ch].  The follow-up type [t]
+ * must be independent of those values, though. *)
 
+(* Some notations will let us write nicer-looking types. *)
+Delimit Scope st_scope with st.
+Bind Scope st_scope with type.
+Notation "!!! ch ( A ) ; k" := (TSend ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope.
+Notation "??? ch ( A ) ; k" := (TRecv ch A k%st) (right associativity, at level 45, ch at level 0) : st_scope.
+
+(* This tactic happens to be good for automating typing derivations. *)
+Ltac hasty := simplify; repeat ((constructor; simplify)
+                                || match goal with
+                                   | [ |- hasty _ (match ?E with _ => _ end) ] => cases E
+                                   | [ |- hasty (match ?E with _ => _ end) _ ] => cases E
+                                   end).
 
 (** * Examples of typed processes *)
 
@@ -44,14 +80,12 @@ Definition addN (k : nat) (input output : channel) : proc :=
   !!output(n + k);
   Done.
 
-Ltac hasty := simplify; repeat ((constructor; simplify)
+(* Let's prove it against a type, which looks a lot like the program itself. *)
-                                || match goal with
+Definition addN_type input output :=
-                                   | [ |- hasty _ (match ?E with _ => _ end) ] => cases E
+  (???input(nat); !!!output(nat); TDone)%st.
-                                   | [ |- hasty (match ?E with _ => _ end) _ ] => cases E
-                                   end).
 
 Theorem addN_typed : forall k input output,
-    hasty (addN k input output) (???input(nat); !!!output(nat); TDone).
+    hasty (addN k input output) (addN_type input output).
 Proof.
   hasty.
 Qed.
@@ -59,6 +93,11 @@ Qed.
 
 (** * Complementing types *)
 
+(* We will focus on pairs of interacting processes, where one process follows a
+ * session type, and the other process follows the *complement* of that type,
+ * guaranteeing that they agree on the protocol. *)
+
+(* Complementation just flips all sends and receives. *)
 Fixpoint complement (t : type) : type :=
   match t with
   | TSend ch A t1 => TRecv ch A (complement t1)
@@ -66,18 +105,21 @@ Fixpoint complement (t : type) : type :=
   | TDone => TDone
   end.
 
+(* Here's a simple client for our adder example. *)
 Definition add2_client (input output : channel) : proc :=
   !!input(42);
   ??output(_ : nat);
   Done.
 
+(* It checks out against the complement of the type from before. *)
 Theorem add2_client_typed : forall input output,
-    hasty (add2_client input output) (complement (???input(nat); !!!output(nat); TDone)).
+    hasty (add2_client input output) (complement (addN_type input output)).
 Proof.
   hasty.
 Qed.
 
-(** * Parallel execution preserves the existence of complementary session types. *)
+
+(** * Main theorem: deadlock freedom for complementary processes *)
 
 Definition trsys_of pr := {|
   Initial := {pr};
@@ -88,12 +130,15 @@ Definition trsys_of pr := {|
 
 Hint Constructors hasty.
 
+(* The next two lemmas state some inversions that connect stepping and
+ * typing. *)
+
 Lemma input_typed : forall pr ch A v pr',
     lstep pr (Input {| Channel := ch; TypeOf := A; Value := v |}) pr'
     -> forall t, hasty pr t
                  -> exists k, pr = Recv ch k /\ pr' = k v.
 Proof.
-  induct 1; invert 1; eauto.
+  invert 1; invert 1; eauto.
 Qed.
 
 Lemma output_typed : forall pr ch A v pr',
@@ -101,9 +146,12 @@ Lemma output_typed : forall pr ch A v pr',
     -> forall t, hasty pr t
                  -> exists k, pr = Send ch v k /\ pr' = k.
 Proof.
-  induct 1; invert 1; eauto.
+  invert 1; invert 1; eauto.
 Qed.
 
+(* A key strengthened invariant: when two processes begin life as complementary,
+ * they remain complementary forever after, though the shared type may
+ * change. *)
 Lemma complementarity_forever : forall pr1 pr2 t,
     hasty pr1 t
     -> hasty pr2 (complement t)
@@ -139,6 +187,8 @@ Proof.
   eauto 10.
 Qed.
 
+(* The main theorem: it's an invariant that the system is done or can take a
+ * step. *)
 Theorem no_deadlock : forall pr1 pr2 t,
     hasty pr1 t
     -> hasty pr2 (complement t)
@@ -155,6 +205,7 @@ Proof.
   invert H0; invert H1; simplify; eauto.
 Qed.
 
+(* Applying the theorem to our earlier example is easy. *)
 Example adding_no_deadlock : forall k input output,
     input <> output
     -> invariantFor (trsys_of (addN k input output
@@ -163,7 +214,7 @@ Example adding_no_deadlock : forall k input output,
                           \/ exists pr', lstep pr Silent pr').
 Proof.
   simplify.
-  eapply no_deadlock with (t := (???input(nat); !!!output(nat); TDone)%st);
+  eapply no_deadlock with (t := addN_type input output);
     hasty.
 Qed.
 
@@ -172,6 +223,11 @@ End BasicTwoParty.
 
 (** * Two-Party Session Types *)
 
+(* That last type system has a serious weakness: it doesn't allow communication
+ * patterns to vary, based on what was received on channels earlier in
+ * execution.  Let's switch to a simple kind of *dependent* session types, where
+ * send and receive types bind message values for use in decision-making. *)
+
 Module TwoParty.
 
 (** ** Defining the type system *)
@@ -180,11 +236,9 @@ Inductive type :=
 | TSend (ch : channel) (A : Set) (t : A -> type)
 | TRecv (ch : channel) (A : Set) (t : A -> type)
 | TDone.
-
+(* Note the big change: each follow-up type [t] is parameterized on the value
-Delimit Scope st_scope with st.
+ * sent or received.  As with our mixed-embedding programs, within these
-Bind Scope st_scope with type.
+ * functions we may employ the full expressiveness of Gallina. *)
-Notation "!!! ch ( x : A ) ; k" := (TSend ch (fun x : A => k)%st) (right associativity, at level 45, ch at level 0, x at level 0) : st_scope.
-Notation "??? ch ( x : A ) ; k" := (TRecv ch (fun x : A => k)%st) (right associativity, at level 45, ch at level 0, x at level 0) : st_scope.
 
 Inductive hasty : proc -> type -> Prop :=
 | HtSend : forall ch (A : Set) (v : A) k t,
@@ -196,6 +250,11 @@ Inductive hasty : proc -> type -> Prop :=
 | HtDone :
     hasty Done TDone.
 
+Delimit Scope st_scope with st.
+Bind Scope st_scope with type.
+Notation "!!! ch ( x : A ) ; k" := (TSend ch (fun x : A => k)%st) (right associativity, at level 45, ch at level 0, x at level 0) : st_scope.
+Notation "??? ch ( x : A ) ; k" := (TRecv ch (fun x : A => k)%st) (right associativity, at level 45, ch at level 0, x at level 0) : st_scope.
+
 Ltac hasty := simplify; repeat ((constructor; simplify)
                                 || match goal with
                                    | [ |- hasty _ (match ?E with _ => _ end) ] => cases E
@@ -213,6 +272,8 @@ Fixpoint complement (t : type) : type :=
 
 (** ** Example *)
 
+(* Let's demonstrate the power of the strengthened type system.  We'll model an
+ * online store communicating with a customer. *)
 Section online_store.
   Variables request_product in_stock_or_not send_payment_info payment_success add_review : channel.
 
@@ -243,6 +304,8 @@ Section online_store.
          TDone
      else
        TDone)%st.
+  (* Yes, that type again looks a lot like the program!  However, we abstract
+   * away the details of all non-[bool] messages. *)
 
   Theorem customer_hasty : forall product payment_info,
       hasty (customer product payment_info) customer_type.
@@ -274,14 +337,15 @@ Section online_store.
 End online_store.
 
 
-(** * Parallel execution preserves the existence of complementary session types. *)
+(** * Main theorem: deadlock freedom for complementary processes *)
+
+(* The proof is essentially identical to before, which is kind of neat, given
+ * the fundamental new capability that we added. *)
 
 Definition trsys_of pr := {|
   Initial := {pr};
   Step := lstepSilent
 |}.
-(* Note: here we force silent steps, so that all channel communication is
- * internal. *)
 
 Hint Constructors hasty.
 
@@ -375,6 +439,10 @@ End TwoParty.
 
 (** * Multiparty Session Types *)
 
+(* Let's generalize to any number of agents participating in a protocol.  We
+ * won't support all reasonable protocols, and it's an edifying exercise for the
+ * reader to think up examples that this type system rejects. *)
+
 Module Multiparty.
 
 (** ** Defining the type system *)
@@ -382,6 +450,11 @@ Module Multiparty.
 Inductive type :=
 | Communicate (ch : channel) (A : Set) (t : A -> type)
 | TDone.
+(* Things are quite different now.  We define one protocol with a series of
+ * communications, not specifying read vs. write polarity.  Every agent will be
+ * checked against this type, referring to a mapping that tells us which agent
+ * controls the receive end and which the send end of each channel.  Exactly one
+ * agent will have each role. *)
 
 Delimit Scope st_scope with st.
 Bind Scope st_scope with type.
@@ -389,15 +462,20 @@ Notation "!!! ch ( x : A ) ; k" := (Communicate ch (fun x : A => k)%st) (right a
 
 Section parties.
   Variable party : Set.
+  (* We will formalize typing with respect to some (usually finite) set of
+   * parties/agents. *)
 
   Record parties := {
     Sender : party;
     Receiver : party
   }.
-
   Variable channels : channel -> parties.
+  (* As promised, every channel is assigned a unique sender and receiver. *)
 
   Inductive hasty (p : party) : bool -> proc -> type -> Prop :=
+
+  (* The first two rules look up the next channel and confirm that the current
+   * process is in the right role to perform a send or receive. *)
   | HtSend : forall ch rr (A : Set) (v : A) k t,
     channels ch = {| Sender := p; Receiver := rr |}
     -> rr <> p
@@ -408,18 +486,29 @@ Section parties.
       -> sr <> p
       -> (forall v, hasty p false (k v) (t v))
       -> hasty p mayNotSend (Recv ch k) (Communicate ch t)
+
+  (* Not all parties participate in all communications.  Uninvolved parties may
+   * (or, rather, must!) skip protocol steps. *)
   | HtSkip : forall mayNotSend ch sr rr (A : Set) pr (t : A -> _) (witness : A),
       channels ch = {| Sender := sr; Receiver := rr |}
       -> sr <> p
       -> rr <> p
       -> (forall v, hasty p true pr (t v))
       -> hasty p mayNotSend pr (Communicate ch t)
+
   | HtDone : forall mayNotSend,
       hasty p mayNotSend Done TDone.
+
+  (* What was that peculiar [bool] parameter?  If [true], it prohibits the
+   * process from running a [Send] as its next action.  The idea is that, when a
+   * process sits out one step of a protocol, its next action (if any) had
+   * better be a receive, so that it gets some signal to wake up and resume
+   * participating.  Otherwise, the deadlock-freedom analysis is more
+   * complicated. *)
 End parties.
 
 
-(** * Parallel execution preserves the existence of complementary session types. *)
+(** * Main theorem: deadlock freedom for complementary processes *)
 
 Definition trsys_of pr := {|
   Initial := {pr};
@@ -428,6 +517,8 @@ Definition trsys_of pr := {|
 
 Hint Constructors hasty.
 
+(* We prove that the type system rules out fancier constructs. *)
+
 Lemma hasty_not_Block : forall party (channels: _ -> parties party) p mns ch pr t,
     hasty channels p mns (BlockChannel ch pr) t
     -> False.
@@ -457,6 +548,9 @@ Qed.
 
 Hint Immediate hasty_not_Block hasty_not_Dup hasty_not_Par.
 
+(* Next, we characterize how channels must be mapped, given typing of a
+ * process. *)
+
 Lemma input_typed' : forall party (channels : _ -> parties party) p mns ch (A : Set) (k : A -> _) t,
     hasty channels p mns (Recv ch k) t
     -> exists sr (witness : A), channels ch = {| Sender := sr; Receiver := p |}
@@ -501,6 +595,8 @@ Proof.
   eauto.
 Qed.
 
+(* Here is a crucial additional typing judgment, applying to lists of parties.
+ * The parties' code is lined up with lopsided trees of parallel composition. *)
 Inductive typed_multistate party (channels : channel -> parties party) (t : type)
   : list party -> proc -> Prop :=
 | TmsNil : typed_multistate channels t [] Done
@@ -511,6 +607,7 @@ Inductive typed_multistate party (channels : channel -> parties party) (t : type
 
 Hint Constructors typed_multistate.
 
+(* This fancier typing judgment gets a fancier tactic for type-checking. *)
 
 Ltac side :=
   match goal with
@@ -537,6 +634,9 @@ Ltac hasty := simplify; repeat match goal with
                                | [ |- hasty _ _ _ (match ?E with _ => _ end) _ ] => cases E
                                end.
 
+(* Now follow quite a few fiddly lemmas.  Commentary resumes at a crucial
+ * lemma. *)
+
 Lemma no_silent_steps : forall party (channels : _ -> parties party) p mns pr t,
     hasty channels p mns pr t
     -> forall pr', lstep pr Silent pr'
@@ -948,6 +1048,10 @@ Proof.
   assumption.
 Qed.
 
+(* Note how the strengthened invariant here is a natural analogue of the one
+ * for our previous type system.  Instead of calling out two composed actors, we
+ * use predicate [typed_multistate] to constrain process [pr] to include all
+ * parties from [all_parties]. *)
 Lemma complementarity_forever : forall party (channels : _ -> parties party) all_parties pr t,
     NoDup all_parties
     -> (forall p, In p all_parties)
@@ -973,6 +1077,8 @@ Proof.
   exfalso; eauto using complementarity_forever_done.
 Qed.
 
+(* To state deadlock-freedom, it will help to have a general characterization of
+ * when a set of agents are completely finished running. *)
 Inductive inert : proc -> Prop :=
 | InertDone : inert Done
 | InertPar : forall pr1 pr2,
@@ -982,6 +1088,8 @@ Inductive inert : proc -> Prop :=
 
 Hint Constructors inert.
 
+(* Now a few more fiddly lemmas.  See you again at the [Theorem]. *)
+
 Lemma typed_multistate_inert : forall party (channels : _ -> parties party) all_parties pr,
     typed_multistate channels TDone all_parties pr
     -> inert pr.
@@ -1090,6 +1198,9 @@ Proof.
   first_order; eauto.
 Qed.
 
+(* The statement is pleasingly similar to for our prior type system.  The main
+ * new wrinkle is the list [all_parties] of all possible parties, as the first
+ * two hypotheses enforce. *)
 Theorem no_deadlock : forall party (channels : _ -> parties party) all_parties pr t,
     NoDup all_parties
     -> (forall p, In p all_parties)
@@ -1109,6 +1220,9 @@ Proof.
   eauto.
 Qed.
 
+(* Let's redo our online-store example as a degenerate case of multiparty
+ * protocols. *)
+
 Inductive store_party := Customer | Merchant.
 
 Section online_store.
@@ -1194,6 +1308,8 @@ Section online_store.
   Qed.
 End online_store.
 
+(* Next, let's add a new party, to exercise the type system more fully. *)
+
 Inductive store_party' := Customer' | Merchant' | Warehouse.
 
 Section online_store_with_warehouse.

_CoqProject

@@ -55,3 +55,4 @@ SharedMemory.v
 ConcurrentSeparationLogic_template.v
 ConcurrentSeparationLogic.v
 MessagesAndRefinement.v
+SessionTypes.v