From af4a09c0473387bd3a99ff50130e5edc3921f2f2 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 May 2018 10:16:42 -0400 Subject: [PATCH] SessionTypes: changed to make choices explicitly dependent on message contents --- SessionTypes.v | 189 ++++++++----------------------------------------- 1 file changed, 31 insertions(+), 158 deletions(-) diff --git a/SessionTypes.v b/SessionTypes.v index 6b0336d..acdeb8b 100644 --- a/SessionTypes.v +++ b/SessionTypes.v @@ -3,7 +3,7 @@ * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) -Require Import Frap MessagesAndRefinement. +Require Import Frap FunctionalExtensionality MessagesAndRefinement. Set Implicit Arguments. Set Asymmetric Patterns. @@ -12,40 +12,24 @@ Set Asymmetric Patterns. (** * Defining the Type System *) Inductive type := -| TSend (ch : channel) (A : Set) (t : type) -| TRecv (ch : channel) (A : Set) (t : type) -| TDone - -| InternalChoice (t1 t2 : type) -| ExternalChoice (t1 t2 : 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 ( 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. -Infix "|?|" := InternalChoice (at level 40) : st_scope. -Infix "?|?" := ExternalChoice (at level 40) : st_scope. +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, - hasty k t - -> hasty (Send ch v k) (TSend ch A t) -| HtRecv : forall ch (A : Set) (k : A -> _) t (v : A), - (forall v, hasty (k v) t) - -> hasty (Recv ch k) (TRecv ch A t) + hasty k (t v) + -> hasty (Send ch v k) (TSend ch t) +| HtRecv : forall ch (A : Set) (k : A -> _) t, + (forall v, hasty (k v) (t v)) + -> hasty (Recv ch k) (TRecv ch t) | HtDone : - hasty Done TDone - -| HtInternalChoice1 : forall pr t1 t2, - hasty pr t1 - -> hasty pr (InternalChoice t1 t2) -| HtInternalChoice2 : forall pr t1 t2, - hasty pr t2 - -> hasty pr (InternalChoice t1 t2) -| HtExternalChoice : forall pr t1 t2, - hasty pr t1 - -> hasty pr t2 - -> hasty pr (ExternalChoice t1 t2). + hasty Done TDone. (** * Examples of Typed Processes *) @@ -59,7 +43,7 @@ Definition addN (k : nat) (input output : channel) : proc := Ltac hasty := simplify; repeat (constructor; simplify). Theorem addN_typed : forall k input output, - hasty (addN k input output) (???input(nat); !!!output(nat); TDone). + hasty (addN k input output) (???input(_ : nat); !!!output(_ : nat); TDone). Proof. hasty. Qed. @@ -69,12 +53,9 @@ Qed. 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) + | TSend ch _ t1 => TRecv ch (fun v => complement (t1 v)) + | TRecv ch _ t1 => TSend ch (fun v => complement (t1 v)) | TDone => TDone - - | InternalChoice t1 t2 => ExternalChoice (complement t1) (complement t2) - | ExternalChoice t1 t2 => InternalChoice (complement t1) (complement t2) end. Definition add2_client (input output : channel) : proc := @@ -83,8 +64,7 @@ Definition add2_client (input output : channel) : proc := Done. Theorem add2_client_typed : forall input output, - input <> output - -> hasty (add2_client input output) (complement (???input(nat); !!!output(nat); TDone)). + hasty (add2_client input output) (complement (???input(_ : nat); !!!output(_ : nat); TDone)). Proof. hasty. Qed. @@ -101,43 +81,12 @@ Definition trsys_of pr := {| Hint Constructors hasty. -Lemma hasty_not_NewChannel : forall chs pr t, - hasty (NewChannel chs pr) t - -> False. -Proof. - induct 1; auto. -Qed. - -Lemma hasty_not_BlockChannel : forall ch pr t, - hasty (BlockChannel ch pr) t - -> False. -Proof. - induct 1; auto. -Qed. - -Lemma hasty_not_Dup : forall pr t, - hasty (Dup pr) t - -> False. -Proof. - induct 1; auto. -Qed. - -Lemma hasty_not_Par : forall pr1 pr2 t, - hasty (pr1 || pr2) t - -> False. -Proof. - induct 1; auto. -Qed. - -Hint Immediate hasty_not_NewChannel hasty_not_BlockChannel hasty_not_Dup hasty_not_Par. - 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; simplify; try solve [ exfalso; eauto ]. - induct H; eauto. + induct 1; invert 1; eauto. Qed. Lemma output_typed : forall pr ch A v pr', @@ -145,22 +94,7 @@ 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; simplify; try solve [ exfalso; eauto ]. - induct H; eauto. -Qed. - -Lemma complementarity_rendezvous : forall ch (A : Set) (k1 : A -> _) t, - hasty (Recv ch k1) t - -> forall (v : A) k2, hasty (Send ch v k2) (complement t) - -> exists t', hasty (k1 v) t' /\ hasty k2 (complement t'). -Proof. - induct 1; invert 1; simplify; eauto. -Qed. - -Lemma complement_inverse : forall t, - t = complement (complement t). -Proof. - induct t; simplify; equality. + induct 1; invert 1; eauto. Qed. Lemma complementarity_forever : forall pr1 pr2 t, @@ -182,73 +116,20 @@ Proof. first_order; subst. invert H2. - invert H6; try solve [ exfalso; eauto ]. - - invert H6; try solve [ exfalso; eauto ]. - + invert H6; invert H0. + invert H6; invert H1. eapply input_typed in H4; eauto. eapply output_typed in H5; eauto. first_order; subst. - eapply complementarity_rendezvous in H0; eauto. - first_order. - + invert H0. + invert H1. + eauto 7. eapply input_typed in H5; eauto. eapply output_typed in H4; eauto. first_order; subst. - rewrite complement_inverse in H0. - eapply complementarity_rendezvous in H1; eauto. - first_order. - rewrite complement_inverse in H. - first_order. -Qed. - -Lemma notstuck_send : forall pr1 t, - hasty pr1 t - -> forall pr2, hasty pr2 (complement t) - -> forall ch (A : Set) (v : A) pr1', lstep pr1 (Output {| Channel := ch; Value := v |}) pr1' - -> exists pr2', lstep pr2 (Input {| Channel := ch; Value := v |}) pr2'. -Proof. - induct 1; invert 1; simplify; eauto; - match goal with - | [ H : lstep _ _ _ |- _ ] => invert H; eauto - end. -Qed. - -Lemma notstuck_nosilent : forall pr1 t, - hasty pr1 t - -> forall pr1', lstep pr1 Silent pr1' - -> False. -Proof. - induct 1; invert 1; simplify; eauto. -Qed. - -Lemma notstuck_recv : forall pr1 t, - hasty pr1 t - -> forall pr2, hasty pr2 (complement t) - -> forall ch (A : Set) (v : A) pr1', lstep pr1 (Input {| Channel := ch; Value := v |}) pr1' - -> exists (v' : A) pr2', lstep pr2 (Output {| Channel := ch; Value := v' |}) pr2'. -Proof. - induct 1; invert 1; simplify; eauto; - match goal with - | [ H : lstep _ _ _ |- _ ] => invert H; eauto - end. -Qed. - -Lemma one_thread_progress : forall pr t, - hasty pr t - -> pr = Done \/ exists l pr', lstep pr l pr'. -Proof. - induct 1; first_order; subst; eauto. - Unshelve. - assumption. -Qed. - -Lemma hasty_Done : forall t, - hasty Done t - -> forall pr, hasty pr (complement t) - -> pr = Done. -Proof. - induct 1; invert 1; eauto. + invert H0. + invert H1. + eauto 10. Qed. Theorem no_deadlock : forall pr1 pr2 t, @@ -261,18 +142,10 @@ Proof. simplify. eapply invariant_weaken. eapply complementarity_forever; eauto. + + clear pr1 pr2 t H H0. simplify; first_order; subst. - specialize (one_thread_progress H2); first_order; subst. - - eapply hasty_Done in H2; eauto. - equality. - - cases x2. - exfalso; eauto using notstuck_nosilent. - right. - cases a; cases m. - eapply notstuck_send in H1; [ | eauto | eauto ]. - first_order; eauto. - eapply notstuck_recv in H1; [ | eauto | eauto ]. - first_order; eauto. + invert H0; invert H1; simplify; eauto. + Unshelve. + assumption. Qed.