From 4874184ac987b6ad78a1cf4ee46539916cc81650 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 May 2018 19:35:14 -0400 Subject: [PATCH] SessionTypes: commented --- SessionTypes.v | 168 +++++++++++++++++++++++++++++++++++++++++-------- _CoqProject | 1 + 2 files changed, 143 insertions(+), 26 deletions(-) diff --git a/SessionTypes.v b/SessionTypes.v index 8355273..970caf1 100644 --- a/SessionTypes.v +++ b/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. -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. - +(* The typing rules mostly just formalize the comments from above. *) 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) - || match goal with - | [ |- hasty _ (match ?E with _ => _ end) ] => cases E - | [ |- hasty (match ?E with _ => _ end) _ ] => cases E - end). +(* Let's prove it against a type, which looks a lot like the program itself. *) +Definition addN_type input output := + (???input(nat); !!!output(nat); TDone)%st. 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. - -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. +(* Note the big change: each follow-up type [t] is parameterized on the value + * sent or received. As with our mixed-embedding programs, within these + * functions we may employ the full expressiveness of Gallina. *) 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. diff --git a/_CoqProject b/_CoqProject index f4bd6ca..19d5cab 100644 --- a/_CoqProject +++ b/_CoqProject @@ -55,3 +55,4 @@ SharedMemory.v ConcurrentSeparationLogic_template.v ConcurrentSeparationLogic.v MessagesAndRefinement.v +SessionTypes.v