From d839cccbad0541da01435c956057d2201a77e09e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 May 2018 18:57:53 -0400 Subject: [PATCH] SessionTypes: starting with a more basic version --- SessionTypes.v | 200 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 166 insertions(+), 34 deletions(-) diff --git a/SessionTypes.v b/SessionTypes.v index d0afb99..8355273 100644 --- a/SessionTypes.v +++ b/SessionTypes.v @@ -9,6 +9,167 @@ Set Implicit Arguments. Set Asymmetric Patterns. +(** * Basic Two-Party Session Types *) + +Module BasicTwoParty. + +(** ** Defining the type system *) + +Inductive type := +| TSend (ch : channel) (A : Set) (t : type) +| TRecv (ch : channel) (A : Set) (t : type) +| TDone. + +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. + +Inductive hasty : proc -> type -> Prop := +| HtSend : forall ch (A : Set) (v : A) k t, + hasty k t + -> hasty (Send ch v k) (TSend ch A t) +| HtRecv : forall ch (A : Set) (k : A -> _) t, + (forall v, hasty (k v) t) + -> hasty (Recv ch k) (TRecv ch A t) +| HtDone : + hasty Done TDone. + + +(** * Examples of typed processes *) + +(* Recall our first example from last chapter. *) +Definition addN (k : nat) (input output : channel) : proc := + ??input(n : nat); + !!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). + +Theorem addN_typed : forall k input output, + hasty (addN k input output) (???input(nat); !!!output(nat); TDone). +Proof. + hasty. +Qed. + + +(** * Complementing types *) + +Fixpoint complement (t : type) : type := + match t with + | TSend ch A t1 => TRecv ch A (complement t1) + | TRecv ch A t1 => TSend ch A (complement t1) + | TDone => TDone + end. + +Definition add2_client (input output : channel) : proc := + !!input(42); + ??output(_ : nat); + Done. + +Theorem add2_client_typed : forall input output, + hasty (add2_client input output) (complement (???input(nat); !!!output(nat); TDone)). +Proof. + hasty. +Qed. + +(** * Parallel execution preserves the existence of complementary session types. *) + +Definition trsys_of pr := {| + Initial := {pr}; + Step := lstepSilent +|}. +(* Note: here we force silent steps, so that all channel communication is + * internal. *) + +Hint Constructors hasty. + +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. +Qed. + +Lemma output_typed : forall pr ch A v pr', + lstep pr (Output {| Channel := ch; TypeOf := A; Value := v |}) pr' + -> forall t, hasty pr t + -> exists k, pr = Send ch v k /\ pr' = k. +Proof. + induct 1; invert 1; eauto. +Qed. + +Lemma complementarity_forever : forall pr1 pr2 t, + hasty pr1 t + -> hasty pr2 (complement t) + -> invariantFor (trsys_of (pr1 || pr2)) + (fun pr => exists pr1' pr2' t', + pr = pr1' || pr2' + /\ hasty pr1' t' + /\ hasty pr2' (complement t')). +Proof. + simplify. + apply invariant_induction; simplify. + + propositional; subst. + eauto 6. + + clear pr1 pr2 t H H0. + first_order; subst. + invert H2. + + invert H6; invert H0. + invert H6; invert H1. + eapply input_typed in H4; eauto. + eapply output_typed in H5; eauto. + first_order; subst. + invert H0. + invert H1. + eauto 7. + eapply input_typed in H5; eauto. + eapply output_typed in H4; eauto. + first_order; subst. + invert H0. + invert H1. + eauto 10. +Qed. + +Theorem no_deadlock : forall pr1 pr2 t, + hasty pr1 t + -> hasty pr2 (complement t) + -> invariantFor (trsys_of (pr1 || pr2)) + (fun pr => pr = (Done || Done) + \/ exists pr', lstep pr Silent pr'). +Proof. + simplify. + eapply invariant_weaken. + eapply complementarity_forever; eauto. + + clear pr1 pr2 t H H0. + simplify; first_order; subst. + invert H0; invert H1; simplify; eauto. +Qed. + +Example adding_no_deadlock : forall k input output, + input <> output + -> invariantFor (trsys_of (addN k input output + || add2_client input output)) + (fun pr => pr = (Done || Done) + \/ exists pr', lstep pr Silent pr'). +Proof. + simplify. + eapply no_deadlock with (t := (???input(nat); !!!output(nat); TDone)%st); + hasty. +Qed. + +End BasicTwoParty. + + (** * Two-Party Session Types *) Module TwoParty. @@ -35,28 +196,12 @@ Inductive hasty : proc -> type -> Prop := | HtDone : hasty Done TDone. - -(** * Examples of typed processes *) - -(* Recall our first example from last chapter. *) -Definition addN (k : nat) (input output : channel) : proc := - ??input(n : nat); - !!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). -Theorem addN_typed : forall k input output, - hasty (addN k input output) (???input(_ : nat); !!!output(_ : nat); TDone). -Proof. - hasty. -Qed. - - (** * Complementing types *) Fixpoint complement (t : type) : type := @@ -66,17 +211,6 @@ Fixpoint complement (t : type) : type := | TDone => TDone end. -Definition add2_client (input output : channel) : proc := - !!input(42); - ??output(_ : nat); - Done. - -Theorem add2_client_typed : forall input output, - hasty (add2_client input output) (complement (???input(_ : nat); !!!output(_ : nat); TDone)). -Proof. - hasty. -Qed. - (** ** Example *) Section online_store. @@ -207,7 +341,7 @@ Theorem no_deadlock : forall pr1 pr2 t, -> hasty pr2 (complement t) -> invariantFor (trsys_of (pr1 || pr2)) (fun pr => pr = (Done || Done) - \/ exists l' pr', lstep pr l' pr'). + \/ exists pr', lstep pr Silent pr'). Proof. simplify. eapply invariant_weaken. @@ -216,8 +350,6 @@ Proof. clear pr1 pr2 t H H0. simplify; first_order; subst. invert H0; invert H1; simplify; eauto. - Unshelve. - assumption. Qed. Example online_store_no_deadlock : forall request_product in_stock_or_not @@ -230,7 +362,7 @@ Example online_store_no_deadlock : forall request_product in_stock_or_not send_payment_info payment_success add_review in_stock payment_checker)) (fun pr => pr = (Done || Done) - \/ exists l' pr', lstep pr l' pr'). + \/ exists pr', lstep pr Silent pr'). Proof. simplify. eapply no_deadlock with (t := customer_type request_product in_stock_or_not @@ -1145,12 +1277,12 @@ Section online_store_with_warehouse. {| Sender := Merchant'; Receiver := Customer' |}. - Example online_store_no_deadlock' : forall product payment_info in_stock good_infos, + Example online_store_no_deadlock' : forall product payment_info payment_checker in_stock, NoDup [request_product; in_stock_or_not; send_payment_info; payment_success; add_review; merchant_to_warehouse; warehouse_to_merchant] -> invariantFor (trsys_of (customer' product payment_info - || (merchant' in_stock - || (warehouse good_infos || Done)))) + || (merchant' payment_checker + || (warehouse in_stock || Done)))) (fun pr => inert pr \/ exists pr', lstep pr Silent pr'). Proof.