frap/SessionTypes.v

1556 lines
47 KiB
Coq
Raw Normal View History

2018-05-12 18:53:37 +00:00
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
* Chapter 21: Session Types
2018-05-12 18:53:37 +00:00
* Author: Adam Chlipala
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
Require Import Frap FunctionalExtensionality MessagesAndRefinement.
2018-05-12 18:53:37 +00:00
Set Implicit Arguments.
Set Asymmetric Patterns.
2018-05-13 23:35:14 +00:00
(* 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 *)
2018-05-13 23:35:14 +00:00
(* 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 *)
2018-05-12 18:53:37 +00:00
Inductive type :=
| TSend (ch : channel) (A : Type) (t : type)
2018-05-13 23:35:14 +00:00
(* 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 : Type) (t : type)
2018-05-13 23:35:14 +00:00
(* This type is the dual of the last one: the process begins by receiving a
* value of type [A] from channel [ch]. *)
2018-05-12 18:53:37 +00:00
2018-05-13 23:35:14 +00:00
| 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! *)
2018-05-12 18:53:37 +00:00
2018-05-13 23:35:14 +00:00
(* The typing rules mostly just formalize the comments from above. *)
2018-05-12 18:53:37 +00:00
Inductive hasty : proc -> type -> Prop :=
| HtSend : forall ch (A : Type) (v : A) k t,
hasty k t
-> hasty (Send ch v k) (TSend ch A t)
| HtRecv : forall ch (A : Type) (k : A -> _) t,
(forall v, hasty (k v) t)
-> hasty (Recv ch k) (TRecv ch A t)
2018-05-12 18:53:37 +00:00
| HtDone :
hasty Done TDone.
2018-05-13 23:35:14 +00:00
(* 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.
2018-05-12 18:53:37 +00:00
2018-05-13 23:35:14 +00:00
(* 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).
2018-05-12 18:53:37 +00:00
(** * Examples of typed processes *)
2018-05-12 18:53:37 +00:00
(* Recall our first example from last chapter. *)
Definition addN (k : nat) (input output : channel) : proc :=
??input(n : nat);
!!output(n + k);
Done.
2018-05-13 23:35:14 +00:00
(* 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.
2018-05-12 18:53:37 +00:00
Theorem addN_typed : forall k input output,
2018-05-13 23:35:14 +00:00
hasty (addN k input output) (addN_type input output).
2018-05-12 18:53:37 +00:00
Proof.
hasty.
Qed.
(** * Complementing types *)
2018-05-12 18:53:37 +00:00
2018-05-13 23:35:14 +00:00
(* 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. *)
2018-05-12 18:53:37 +00:00
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)
2018-05-12 18:53:37 +00:00
| TDone => TDone
end.
2018-05-13 23:35:14 +00:00
(* Here's a simple client for our adder example. *)
2018-05-12 18:53:37 +00:00
Definition add2_client (input output : channel) : proc :=
!!input(42);
??output(_ : nat);
Done.
2018-05-12 18:53:37 +00:00
2018-05-13 23:35:14 +00:00
(* It checks out against the complement of the type from before. *)
2018-05-12 18:53:37 +00:00
Theorem add2_client_typed : forall input output,
2018-05-13 23:35:14 +00:00
hasty (add2_client input output) (complement (addN_type input output)).
2018-05-12 18:53:37 +00:00
Proof.
hasty.
Qed.
2018-05-13 23:35:14 +00:00
(** * Main theorem: deadlock freedom for complementary processes *)
Definition trsys_of pr := {|
Initial := {pr};
Step := lstepSilent
|}.
(* Note: here we force silent steps, so that all channel communication is
* internal. *)
Hint Constructors hasty : core.
2018-05-13 23:35:14 +00:00
(* The next two lemmas state some inversions that connect stepping and
* typing. *)
Lemma input_typed : forall pr ch A v pr',
lstep pr (Action (Input {| Channel := ch; TypeOf := A; Value := v |})) pr'
-> forall t, hasty pr t
-> exists k, pr = Recv ch k /\ pr' = k v.
Proof.
2018-05-13 23:35:14 +00:00
invert 1; invert 1; eauto.
Qed.
Lemma output_typed : forall pr ch A v pr',
lstep pr (Action (Output {| Channel := ch; TypeOf := A; Value := v |})) pr'
-> forall t, hasty pr t
-> exists k, pr = Send ch v k /\ pr' = k.
Proof.
2018-05-13 23:35:14 +00:00
invert 1; invert 1; eauto.
Qed.
2018-05-13 23:35:14 +00:00
(* 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)
-> 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.
2018-05-13 23:35:14 +00:00
(* 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)
-> 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.
2018-05-13 23:35:14 +00:00
(* 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
|| add2_client input output))
(fun pr => pr = (Done || Done)
\/ exists pr', lstep pr Silent pr').
Proof.
simplify.
2018-05-13 23:35:14 +00:00
eapply no_deadlock with (t := addN_type input output);
hasty.
Qed.
End BasicTwoParty.
(** * Two-Party Session Types *)
2018-05-13 23:35:14 +00:00
(* 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 *)
Inductive type :=
| TSend (ch : channel) (A : Type) (t : A -> type)
| TRecv (ch : channel) (A : Type) (t : A -> type)
| TDone.
2018-05-13 23:35:14 +00:00
(* 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 : Type) (v : A) k t,
hasty k (t v)
-> hasty (Send ch v k) (TSend ch t)
| HtRecv : forall ch (A : Type) (k : A -> _) t,
(forall v, hasty (k v) (t v))
-> hasty (Recv ch k) (TRecv ch t)
| HtDone :
hasty Done TDone.
2018-05-13 23:35:14 +00:00
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
| [ |- hasty (match ?E with _ => _ end) _ ] => cases E
end).
(** * Complementing types *)
Fixpoint complement (t : type) : type :=
match t with
| TSend ch _ t1 => TRecv ch (fun v => complement (t1 v))
| TRecv ch _ t1 => TSend ch (fun v => complement (t1 v))
| TDone => TDone
end.
(** ** Example *)
2018-05-13 23:35:14 +00:00
(* 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.
Definition customer (product payment_info : string) :=
!!request_product(product);
??in_stock_or_not(worked : bool);
if worked then
!!send_payment_info(payment_info);
??payment_success(worked_again : bool);
if worked_again then
!!add_review((product, "awesome"));
Done
else
Done
else
Done.
Definition customer_type :=
(!!!request_product(_ : string);
???in_stock_or_not(worked : bool);
if worked then
!!!send_payment_info(_ : string);
???payment_success(worked_again : bool);
if worked_again then
!!!add_review(_ : (string * string)%type);
TDone
else
TDone
else
TDone)%st.
2018-05-13 23:35:14 +00:00
(* 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.
Proof.
hasty.
Qed.
Definition merchant (in_stock payment_checker : string -> bool) :=
??request_product(product : string);
if in_stock product then
!!in_stock_or_not(true);
??send_payment_info(payment_info : string);
if payment_checker payment_info then
!!payment_success(true);
??add_review(_ : (string * string)%type);
Done
else
!!payment_success(false);
Done
else
!!in_stock_or_not(false);
Done.
Theorem merchant_hasty : forall in_stock payment_checker,
hasty (merchant in_stock payment_checker) (complement customer_type).
Proof.
hasty.
Qed.
End online_store.
2018-05-13 23:35:14 +00:00
(** * 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
|}.
Hint Constructors hasty : core.
Lemma input_typed : forall pr ch A v pr',
lstep pr (Action (Input {| Channel := ch; TypeOf := A; Value := v |})) pr'
-> forall t, hasty pr t
-> exists k, pr = Recv ch k /\ pr' = k v.
Proof.
invert 1; invert 1; eauto.
Qed.
Lemma output_typed : forall pr ch A v pr',
lstep pr (Action (Output {| Channel := ch; TypeOf := A; Value := v |})) pr'
-> forall t, hasty pr t
-> exists k, pr = Send ch v k /\ pr' = k.
Proof.
invert 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.
2018-05-13 14:03:47 +00:00
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').
2018-05-13 14:03:47 +00:00
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.
2018-05-13 14:03:47 +00:00
Qed.
Example online_store_no_deadlock : forall request_product in_stock_or_not
send_payment_info payment_success add_review
product payment_info in_stock payment_checker,
invariantFor (trsys_of (customer request_product in_stock_or_not
send_payment_info payment_success add_review
product payment_info
|| merchant request_product in_stock_or_not
send_payment_info payment_success add_review
in_stock payment_checker))
(fun pr => pr = (Done || Done)
\/ exists pr', lstep pr Silent pr').
Proof.
simplify.
eapply no_deadlock with (t := customer_type request_product in_stock_or_not
send_payment_info payment_success add_review);
hasty.
Qed.
End TwoParty.
2018-05-13 20:52:49 +00:00
(** * Multiparty Session Types *)
2018-05-13 23:35:14 +00:00
(* 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. *)
2018-05-13 20:52:49 +00:00
Module Multiparty.
(** ** Defining the type system *)
Inductive type :=
| Communicate (ch : channel) (A : Type) (t : A -> type)
2018-05-13 20:52:49 +00:00
| TDone.
2018-05-13 23:35:14 +00:00
(* 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. *)
2018-05-13 20:52:49 +00:00
Delimit Scope st_scope with st.
Bind Scope st_scope with type.
Notation "!!! ch ( x : A ) ; k" := (Communicate ch (fun x : A => k)%st) (right associativity, at level 45, ch at level 0, x at level 0) : st_scope.
Section parties.
Variable party : Type.
2018-05-13 23:35:14 +00:00
(* We will formalize typing with respect to some (usually finite) set of
* parties/agents. *)
2018-05-13 20:52:49 +00:00
Record parties := {
Sender : party;
Receiver : party
}.
Variable channels : channel -> parties.
2018-05-13 23:35:14 +00:00
(* As promised, every channel is assigned a unique sender and receiver. *)
2018-05-13 20:52:49 +00:00
Inductive hasty (p : party) : bool -> proc -> type -> Prop :=
2018-05-13 23:35:14 +00:00
(* 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 : Type) (v : A) k t,
2018-05-13 20:52:49 +00:00
channels ch = {| Sender := p; Receiver := rr |}
-> rr <> p
-> hasty p false k (t v)
-> hasty p false (Send ch v k) (Communicate ch t)
| HtRecv : forall mayNotSend ch sr (A : Type) (k : A -> _) t (witness : A),
2018-05-13 20:52:49 +00:00
channels ch = {| Sender := sr; Receiver := p |}
-> sr <> p
-> (forall v, hasty p false (k v) (t v))
2018-05-13 20:52:49 +00:00
-> hasty p mayNotSend (Recv ch k) (Communicate ch t)
2018-05-13 23:35:14 +00:00
(* Not all parties participate in all communications. Uninvolved parties may
* (or, rather, must!) skip protocol steps. *)
| HtSkip : forall mayNotSend ch sr rr (A : Type) pr (t : A -> _) (witness : A),
2018-05-13 20:52:49 +00:00
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)
2018-05-13 23:35:14 +00:00
2018-05-13 20:52:49 +00:00
| HtDone : forall mayNotSend,
hasty p mayNotSend Done TDone.
2018-05-13 23:35:14 +00:00
(* 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. *)
2018-05-13 20:52:49 +00:00
End parties.
2018-05-13 23:35:14 +00:00
(** * Main theorem: deadlock freedom for complementary processes *)
2018-05-13 20:52:49 +00:00
Definition trsys_of pr := {|
Initial := {pr};
Step := lstepSilent
|}.
Hint Constructors hasty : core.
2018-05-13 20:52:49 +00:00
2018-05-13 23:35:14 +00:00
(* We prove that the type system rules out fancier constructs. *)
2018-05-13 20:52:49 +00:00
Lemma hasty_not_Block : forall party (channels: _ -> parties party) p mns ch pr t,
hasty channels p mns (BlockChannel ch pr) t
-> False.
Proof.
induct 1; auto.
Unshelve.
assumption.
Qed.
Lemma hasty_not_Dup : forall party (channels: _ -> parties party) p mns pr t,
hasty channels p mns (Dup pr) t
-> False.
Proof.
induct 1; auto.
Unshelve.
assumption.
Qed.
Lemma hasty_not_Par : forall party (channels: _ -> parties party) p mns pr1 pr2 t,
hasty channels p mns (pr1 || pr2) t
-> False.
Proof.
induct 1; auto.
Unshelve.
assumption.
Qed.
Hint Immediate hasty_not_Block hasty_not_Dup hasty_not_Par : core.
2018-05-13 20:52:49 +00:00
2018-05-13 23:35:14 +00:00
(* 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 : Type) (k : A -> _) t,
2018-05-13 20:52:49 +00:00
hasty channels p mns (Recv ch k) t
-> exists sr (witness : A), channels ch = {| Sender := sr; Receiver := p |}
/\ sr <> p.
Proof.
induct 1; eauto.
Unshelve.
assumption.
Qed.
Lemma input_typed : forall party (channels: _ -> parties party) pr ch A v pr',
lstep pr (Action (Input {| Channel := ch; TypeOf := A; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> forall p mns t, hasty channels p mns pr t
-> exists sr k, pr = Recv ch k /\ pr' = k v
/\ channels ch = {| Sender := sr; Receiver := p |}
/\ sr <> p.
Proof.
induct 1; simplify; try solve [ exfalso; eauto ].
eapply input_typed' in H.
first_order.
eauto 6.
Qed.
Lemma output_typed' : forall party (channels : _ -> parties party) p mns ch (A : Type) (v : A) k t,
2018-05-13 20:52:49 +00:00
hasty channels p mns (Send ch v k) t
-> exists rr, channels ch = {| Sender := p; Receiver := rr |}
/\ rr <> p.
Proof.
induct 1; eauto.
Unshelve.
assumption.
Qed.
Lemma output_typed : forall party (channels: _ -> parties party) pr ch A v pr',
lstep pr (Action (Output {| Channel := ch; TypeOf := A; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> forall p mns t, hasty channels p mns pr t
-> exists k, pr = Send ch v k /\ pr' = k.
Proof.
induct 1; simplify; try solve [ exfalso; eauto ].
eapply output_typed' in H.
first_order.
eauto.
Qed.
2018-05-13 23:35:14 +00:00
(* Here is a crucial additional typing judgment, applying to lists of parties.
* The parties' code is lined up with lopsided trees of parallel composition. *)
2018-05-13 20:52:49 +00:00
Inductive typed_multistate party (channels : channel -> parties party) (t : type)
: list party -> proc -> Prop :=
| TmsNil : typed_multistate channels t [] Done
| TmsCons : forall p ps pr1 pr2,
hasty channels p false pr1 t
-> typed_multistate channels t ps pr2
-> typed_multistate channels t (p :: ps) (pr1 || pr2).
Hint Constructors typed_multistate : core.
2018-05-13 20:52:49 +00:00
2018-05-13 23:35:14 +00:00
(* This fancier typing judgment gets a fancier tactic for type-checking. *)
Ltac side :=
match goal with
| [ |- ?E = {| Sender := _; Receiver := _ |} ] =>
let E' := eval hnf in E in change E with E';
repeat match goal with
| [ |- context[if ?E then _ else _] ] => cases E; try (exfalso; equality)
end;
try (exfalso; equality);
repeat match goal with
| [ H : NoDup _ |- _ ] => invert H
end; simplify; try (exfalso; equality); equality
| [ |- _ <> _ ] => equality
end.
Ltac hasty := simplify; repeat match goal with
| [ |- typed_multistate _ _ _ _ ] => econstructor; simplify
| [ |- hasty _ _ _ _ _ ] =>
apply HtDone
|| (eapply HtSend; [ side | side | ])
|| (eapply HtRecv; [ constructor | side | side | simplify ])
|| (eapply HtSkip; [ constructor | side | side | side | simplify ])
| [ |- hasty _ _ _ _ (match ?E with _ => _ end) ] => cases E
| [ |- hasty _ _ _ (match ?E with _ => _ end) _ ] => cases E
end.
2018-05-13 23:35:14 +00:00
(* Now follow quite a few fiddly lemmas. Commentary resumes at a crucial
* lemma. *)
2018-05-13 20:52:49 +00:00
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'
-> False.
Proof.
induct 1; invert 1; try solve [ exfalso; eauto ].
Unshelve.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.
Hint Immediate no_silent_steps : core.
2018-05-13 20:52:49 +00:00
Lemma complementarity_forever_done : forall party (channels : _ -> parties party) pr pr',
lstep pr Silent pr'
-> forall all_parties, typed_multistate channels TDone all_parties pr
-> False.
Proof.
induct 1; invert 1; eauto.
invert H5.
invert H.
invert H5.
invert H.
Qed.
Lemma mayNotSend_really : forall party (channels : _ -> parties party) p pr t,
hasty channels p true pr t
-> forall m pr', lstep pr (Action (Output m)) pr'
2018-05-13 20:52:49 +00:00
-> False.
Proof.
induct 1; eauto; invert 1.
Unshelve.
assumption.
Qed.
Hint Immediate mayNotSend_really : core.
2018-05-13 20:52:49 +00:00
Lemma may_not_output : forall (party : Type) pr pr' ch (A : Type) (v : A),
lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> forall (channels : _ -> parties party) p t,
hasty channels p true pr t
-> False.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
Unshelve.
assumption.
assumption.
assumption.
assumption.
Qed.
Hint Immediate may_not_output : core.
2018-05-13 20:52:49 +00:00
Lemma output_is_legit : forall (party : Type) pr pr' ch (A : Type) (v : A),
lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
-> forall (channels : _ -> parties party) all_parties ch' (A' : Type) (k : A' -> _),
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch' k) all_parties pr
-> In (Sender (channels ch')) all_parties.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H4.
rewrite H3 in *; simplify; eauto.
invert H.
exfalso; eauto.
invert H4.
rewrite H3 in *; simplify; eauto.
eauto.
eauto.
Unshelve.
assumption.
Qed.
Lemma output_is_first : forall (party : Type) pr pr' ch (A : Type) (v : A),
lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
-> forall (channels : _ -> parties party) all_parties ch' (A' : Type) (k : A' -> _),
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch' k) all_parties pr
-> ch' = ch.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H4.
invert H; auto.
invert H.
exfalso; eauto.
eauto.
Unshelve.
assumption.
Qed.
Lemma input_is_legit' : forall (party : Type) pr ch (A : Type) (v : A)
2018-05-13 20:52:49 +00:00
(channels : _ -> parties party) p mns t,
hasty channels p mns pr t
-> forall pr', lstep pr (Action (Input {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> p = Receiver (channels ch).
Proof.
induct 1; eauto; invert 1.
rewrite H; auto.
Qed.
Lemma input_is_legit : forall (party : Type) pr pr' ch (A : Type) (v : A),
lstep pr (Action (Input {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> forall (channels : _ -> parties party) all_parties t,
typed_multistate channels t all_parties pr
-> In (Receiver (channels ch)) all_parties.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H4.
invert H.
invert H.
rewrite H0 in *; simplify; eauto.
eapply input_is_legit' in H; eauto.
invert H.
eauto.
Unshelve.
assumption.
Qed.
Lemma comm_stuck : forall (party : Type) pr pr',
2018-05-13 20:52:49 +00:00
lstep pr Silent pr'
-> forall (channels : _ -> parties party) all_parties ch (A : Type) (k : A -> _),
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch k) all_parties pr
-> (In (Sender (channels ch)) all_parties
-> In (Receiver (channels ch)) all_parties
-> False)
-> False.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H5.
invert H.
invert H.
eapply output_is_legit in H0; eauto.
rewrite H9 in *; simplify; eauto.
rewrite H7 in *; simplify.
eapply output_is_first in H0; eauto.
subst.
eapply input_is_legit' in H; eauto.
subst.
rewrite H7 in *.
simplify.
eauto.
invert H5.
invert H.
rewrite H7 in *; simplify.
eapply input_is_legit in H0; eauto.
rewrite H7 in *; simplify.
eauto.
invert H.
eauto.
Unshelve.
assumption.
assumption.
Qed.
Lemma hasty_relax : forall party (channels : _ -> parties party) p mns pr t,
hasty channels p mns pr t
-> hasty channels p false pr t.
Proof.
induct 1; eauto.
Qed.
Local Hint Immediate hasty_relax : core.
2018-05-13 20:52:49 +00:00
Lemma complementarity_preserve_unused : forall party (channels : _ -> parties party)
pr ch (A : Type) (t : A -> _) all_parties,
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch t) all_parties pr
-> ~In (Sender (channels ch)) all_parties
-> ~In (Receiver (channels ch)) all_parties
-> forall v, typed_multistate channels (t v) all_parties pr.
Proof.
induct 1; simplify; eauto.
invert H.
rewrite H6 in *; simplify.
equality.
rewrite H8 in *; simplify.
propositional.
rewrite H6 in *; simplify.
propositional.
eauto.
Qed.
Lemma hasty_output : forall pr party (channels : _ -> parties party) p mns t,
hasty channels p mns pr t
-> forall ch (A : Type) (v : A) pr', lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> Sender (channels ch) = p.
Proof.
induct 1; invert 1.
rewrite H; auto.
eauto.
exfalso; eauto.
exfalso; eauto.
exfalso; eauto.
Unshelve.
assumption.
assumption.
assumption.
Qed.
Lemma complementarity_find_sender : forall party (channels : _ -> parties party) pr ch (A : Type) (v : A) pr',
lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> forall (t : A -> _) all_parties,
typed_multistate channels (Communicate ch t) all_parties pr
-> NoDup all_parties
-> In (Sender (channels ch)) all_parties
-> ~In (Receiver (channels ch)) all_parties
-> typed_multistate channels (t v) all_parties pr'.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H0.
generalize dependent H.
invert H4.
invert 1.
econstructor.
eauto.
eapply complementarity_preserve_unused; eauto.
rewrite H6; assumption.
invert 1.
rewrite H6 in *; simplify.
eapply hasty_output in H; eauto.
rewrite H6 in *; simplify.
equality.
invert H0.
invert H4.
rewrite H9 in *; simplify.
eapply output_is_legit in H5; try eassumption.
rewrite H9 in *; simplify.
propositional.
rewrite H11 in *; simplify.
propositional.
rewrite H9 in *; simplify.
eapply IHlstep in H5; try (eassumption || reflexivity).
2: rewrite H9; simplify; equality.
2: rewrite H9; simplify; equality.
eauto.
Unshelve.
assumption.
Qed.
Lemma complementarity_find_receiver : forall party (channels : _ -> parties party) pr ch (A : Type) (v : A) pr',
lstep pr (Action (Input {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> forall (t : A -> _) all_parties,
typed_multistate channels (Communicate ch t) all_parties pr
-> NoDup all_parties
-> ~In (Sender (channels ch)) all_parties
-> In (Receiver (channels ch)) all_parties
-> typed_multistate channels (t v) all_parties pr'.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H0.
generalize dependent H.
invert H4.
invert 1.
invert 1.
econstructor.
eauto.
eapply complementarity_preserve_unused; eauto.
rewrite H10; assumption.
rewrite H6 in *; simplify.
eapply input_is_legit' in H; eauto.
rewrite H6 in *; simplify; equality.
invert H0.
invert H4.
rewrite H9 in *; simplify.
eapply input_is_legit in H; try eassumption.
rewrite H9 in *; simplify.
propositional.
rewrite H11 in *; simplify.
propositional.
eapply input_is_legit in H; try eassumption.
rewrite H11 in *; simplify.
propositional.
eapply IHlstep in H5; try (eassumption || reflexivity).
2: rewrite H9 in *; simplify; equality.
2: rewrite H9 in *; simplify; equality.
eauto.
Unshelve.
assumption.
Qed.
Lemma output_is_legit' : forall party (channels : _ -> parties party) p mns pr t,
hasty channels p mns pr t
-> forall ch (A : Type) (v : A) pr', lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
2018-05-13 20:52:49 +00:00
-> p = Sender (channels ch).
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
rewrite H; auto.
Unshelve.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma complementarity_forever' : forall party (channels : _ -> parties party) pr pr',
lstep pr Silent pr'
-> forall ch (A : Type) (t : A -> _) all_parties,
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch t) all_parties pr
-> NoDup all_parties
-> In (Sender (channels ch)) all_parties
-> In (Receiver (channels ch)) all_parties
-> exists v, typed_multistate channels (t v) all_parties pr'.
Proof.
induct 1; invert 1; simplify; try solve [ exfalso; eauto ].
invert H0.
invert H4.
rewrite H9 in *; simplify.
propositional; try equality.
exfalso; eapply comm_stuck; try eassumption.
rewrite H9; simplify; eauto.
exfalso; eapply comm_stuck; try eassumption.
rewrite H11; simplify; eauto.
rewrite H9 in *; simplify.
apply IHlstep in H5; try assumption.
2: rewrite H9; simplify; equality.
2: rewrite H9; simplify; equality.
first_order; eauto.
invert H1.
generalize dependent H.
invert H5.
invert 1.
invert 1.
eexists.
econstructor.
eauto.
eapply complementarity_find_sender; try eassumption.
rewrite H11 in *; simplify; equality.
rewrite H11 in *; simplify; equality.
rewrite H7 in *; simplify.
eapply input_is_legit' in H; eauto.
eapply output_is_first in H6; try eassumption.
subst.
rewrite H7 in *; simplify; equality.
invert H1.
generalize dependent H.
invert H5.
invert 1.
eexists.
econstructor.
eauto.
eapply complementarity_find_receiver; try eassumption.
rewrite H7 in *; simplify; equality.
rewrite H7 in *; simplify; equality.
invert 1.
rewrite H7 in *; simplify.
exfalso; eauto.
Unshelve.
assumption.
assumption.
Qed.
2018-05-13 23:35:14 +00:00
(* 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]. *)
2018-05-13 20:52:49 +00:00
Lemma complementarity_forever : forall party (channels : _ -> parties party) all_parties pr t,
NoDup all_parties
-> (forall p, In p all_parties)
-> typed_multistate channels t all_parties pr
-> invariantFor (trsys_of pr)
(fun pr' => exists t',
typed_multistate channels t' all_parties pr').
Proof.
simplify.
apply invariant_induction; simplify.
propositional; subst.
eauto.
clear pr t H1.
first_order.
cases x.
eapply complementarity_forever' in H1; try eassumption.
first_order.
eauto.
eauto.
exfalso; eauto using complementarity_forever_done.
Qed.
2018-05-13 23:35:14 +00:00
(* To state deadlock-freedom, it will help to have a general characterization of
* when a set of agents are completely finished running. *)
2018-05-13 20:52:49 +00:00
Inductive inert : proc -> Prop :=
| InertDone : inert Done
| InertPar : forall pr1 pr2,
inert pr1
-> inert pr2
-> inert (pr1 || pr2).
Hint Constructors inert : core.
2018-05-13 20:52:49 +00:00
2018-05-13 23:35:14 +00:00
(* Now a few more fiddly lemmas. See you again at the [Theorem]. *)
2018-05-13 20:52:49 +00:00
Lemma typed_multistate_inert : forall party (channels : _ -> parties party) all_parties pr,
typed_multistate channels TDone all_parties pr
-> inert pr.
Proof.
induct 1; eauto.
invert H; eauto.
Qed.
Hint Immediate typed_multistate_inert : core.
2018-05-13 20:52:49 +00:00
Lemma deadlock_find_receiver : forall party (channels : _ -> parties party) all_parties
ch (A : Type) (k : A -> _) pr,
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch k) all_parties pr
-> In (Receiver (channels ch)) all_parties
-> forall v : A, exists pr', lstep pr (Action (Input {| Channel := ch; Value := v |})) pr'.
2018-05-13 20:52:49 +00:00
Proof.
induct 1; simplify; propositional; subst.
invert H.
rewrite H4 in *; simplify.
equality.
eauto.
rewrite H4 in *; simplify.
equality.
invert H.
rewrite H6 in *; simplify.
specialize (H1 v).
first_order.
eauto.
rewrite H8 in *; simplify.
eauto.
rewrite H6 in *; simplify.
specialize (H1 v).
first_order.
eauto.
Qed.
Lemma deadlock_find_sender : forall party (channels : _ -> parties party) all_parties
ch (A : Type) (k : A -> _) pr,
2018-05-13 20:52:49 +00:00
typed_multistate channels (Communicate ch k) all_parties pr
-> In (Sender (channels ch)) all_parties
-> exists (v : A) pr', lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'.
2018-05-13 20:52:49 +00:00
Proof.
induct 1; simplify; propositional; subst.
invert H.
rewrite H4 in *; simplify.
eauto.
rewrite H6 in *; simplify.
equality.
rewrite H4 in *; simplify.
equality.
first_order.
invert H.
rewrite H6 in *; simplify.
eauto.
rewrite H8 in *; simplify.
eauto.
eauto.
Qed.
Lemma no_deadlock' : forall party (channels : _ -> parties party) all_parties
ch (A : Type) (k : A -> _) pr,
2018-05-13 20:52:49 +00:00
NoDup all_parties
-> typed_multistate channels (Communicate ch k) all_parties pr
-> In (Sender (channels ch)) all_parties
-> In (Receiver (channels ch)) all_parties
-> exists pr', lstep pr Silent pr'.
Proof.
induct 2; simplify; propositional; subst.
invert H0.
rewrite H6 in *; simplify.
equality.
rewrite H8 in *; simplify.
equality.
rewrite H6 in *; simplify.
equality.
invert H0.
rewrite H6 in *; simplify.
eapply deadlock_find_receiver in H1.
first_order; eauto.
rewrite H6; assumption.
rewrite H8 in *; simplify.
equality.
rewrite H6 in *; simplify.
equality.
invert H0.
rewrite H6 in *; simplify.
equality.
rewrite H8 in *; simplify.
eapply deadlock_find_sender in H1.
first_order; eauto.
rewrite H8; assumption.
rewrite H6 in *; simplify.
equality.
invert H.
apply IHtyped_multistate in H7; auto.
first_order; eauto.
Qed.
2018-05-13 23:35:14 +00:00
(* 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. *)
2018-05-13 20:52:49 +00:00
Theorem no_deadlock : forall party (channels : _ -> parties party) all_parties pr t,
NoDup all_parties
-> (forall p, In p all_parties)
-> typed_multistate channels t all_parties pr
-> invariantFor (trsys_of pr)
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr').
Proof.
simplify.
eapply invariant_weaken.
eapply complementarity_forever; eassumption.
clear pr t H1.
simplify; first_order.
cases x.
right; eapply no_deadlock'; try eassumption; eauto.
eauto.
Qed.
2018-05-13 23:35:14 +00:00
(* Let's redo our online-store example as a degenerate case of multiparty
* protocols. *)
2018-05-13 20:52:49 +00:00
Inductive store_party := Customer | Merchant.
Section online_store.
Variables request_product in_stock_or_not send_payment_info payment_success add_review : channel.
Definition customer (product payment_info : string) :=
!!request_product(product);
??in_stock_or_not(worked : bool);
if worked then
!!send_payment_info(payment_info);
??payment_success(worked_again : bool);
if worked_again then
!!add_review((product, "awesome"));
Done
else
Done
else
Done.
Definition merchant (in_stock payment_checker : string -> bool) :=
??request_product(product : string);
if in_stock product then
!!in_stock_or_not(true);
??send_payment_info(payment_info : string);
if payment_checker payment_info then
!!payment_success(true);
??add_review(_ : (string * string)%type);
Done
else
!!payment_success(false);
Done
else
!!in_stock_or_not(false);
Done.
Definition online_store_type :=
(!!!request_product(_ : string);
!!!in_stock_or_not(worked : bool);
if worked then
!!!send_payment_info(_ : string);
!!!payment_success(worked_again : bool);
if worked_again then
!!!add_review(_ : (string * string)%type);
TDone
else
TDone
else
TDone)%st.
Definition online_store_channels (ch : channel) :=
if ch ==n request_product then
{| Sender := Customer;
Receiver := Merchant |}
else if ch ==n send_payment_info then
{| Sender := Customer;
Receiver := Merchant |}
else if ch ==n add_review then
{| Sender := Customer;
Receiver := Merchant |}
else
{| Sender := Merchant;
Receiver := Customer |}.
Example online_store_no_deadlock : forall product payment_info in_stock payment_checker,
NoDup [request_product; in_stock_or_not; send_payment_info; payment_success; add_review]
-> invariantFor (trsys_of (customer product payment_info
|| (merchant in_stock payment_checker
|| Done)))
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr').
Proof.
simplify.
eapply no_deadlock with (t := online_store_type)
(all_parties := [Customer; Merchant])
(channels := online_store_channels);
simplify.
repeat constructor; simplify; equality.
cases p; auto.
hasty; constructor.
Qed.
End online_store.
2018-05-13 23:35:14 +00:00
(* 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.
Variables request_product in_stock_or_not send_payment_info payment_success add_review
merchant_to_warehouse warehouse_to_merchant : channel.
Definition customer' (product payment_info : string) :=
!!request_product(product);
??in_stock_or_not(worked : bool);
if worked then
!!send_payment_info(payment_info);
??payment_success(worked_again : bool);
if worked_again then
!!add_review((product, "awesome"));
Done
else
Done
else
Done.
Definition merchant' (payment_checker : string -> bool) :=
??request_product(product : string);
!!merchant_to_warehouse(product);
??warehouse_to_merchant(in_stock : bool);
if in_stock then
!!in_stock_or_not(true);
??send_payment_info(payment_info : string);
if payment_checker payment_info then
!!payment_success(true);
??add_review(_ : (string * string)%type);
Done
else
!!payment_success(false);
Done
else
!!in_stock_or_not(false);
Done.
Definition warehouse (in_stock : string -> bool) :=
??merchant_to_warehouse(product : string);
if in_stock product then
!!warehouse_to_merchant(true);
Done
else
!!warehouse_to_merchant(false);
Done.
Definition online_store_type' :=
(!!!request_product(_ : string);
!!!merchant_to_warehouse(_ : string);
!!!warehouse_to_merchant(_ : bool);
!!!in_stock_or_not(worked : bool);
if worked then
!!!send_payment_info(_ : string);
!!!payment_success(worked_again : bool);
if worked_again then
!!!add_review(_ : (string * string)%type);
TDone
else
TDone
else
TDone)%st.
Definition online_store_channels' (ch : channel) :=
if ch ==n request_product then
{| Sender := Customer';
Receiver := Merchant' |}
else if ch ==n send_payment_info then
{| Sender := Customer';
Receiver := Merchant' |}
else if ch ==n add_review then
{| Sender := Customer';
Receiver := Merchant' |}
else if ch ==n merchant_to_warehouse then
{| Sender := Merchant';
Receiver := Warehouse |}
else if ch ==n warehouse_to_merchant then
{| Sender := Warehouse;
Receiver := Merchant' |}
else
{| Sender := Merchant';
Receiver := Customer' |}.
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' payment_checker
|| (warehouse in_stock || Done))))
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr').
Proof.
simplify.
eapply no_deadlock with (t := online_store_type')
(all_parties := [Customer'; Merchant'; Warehouse])
(channels := online_store_channels');
simplify.
repeat constructor; simplify; equality.
cases p; auto.
hasty; constructor.
Qed.
End online_store_with_warehouse.
2018-05-13 20:52:49 +00:00
End Multiparty.
(** * A bonus: running orthogonal protocols in parallel *)
Inductive mayTouch : proc -> channel -> Prop :=
| MtSend1 : forall ch (A : Type) (v : A) k,
mayTouch (Send ch v k) ch
| MtSend2 : forall ch (A : Type) (v : A) k ch',
mayTouch k ch'
-> mayTouch (Send ch v k) ch'
| MtRecv1 : forall ch (A : Type) (k : A -> _),
mayTouch (Recv ch k) ch
| MtRecv2 : forall ch (A : Type) (v : A) k ch',
mayTouch (k v) ch'
-> mayTouch (Recv ch k) ch'
| MtNewChannel : forall ch chs ch' k,
mayTouch (k ch') ch
-> mayTouch (NewChannel chs k) ch
| MtBlockChannel : forall ch ch' k,
mayTouch k ch
-> mayTouch (BlockChannel ch' k) ch
| MtPar1 : forall ch pr1 pr2,
mayTouch pr1 ch
-> mayTouch (Par pr1 pr2) ch
| MtPar2 : forall ch pr1 pr2,
mayTouch pr2 ch
-> mayTouch (Par pr1 pr2) ch
| MtDup : forall ch pr1,
mayTouch pr1 ch
-> mayTouch (Dup pr1) ch.
Hint Constructors mayTouch : core.
Import BasicTwoParty Multiparty.
Lemma lstep_mayTouch : forall pr l pr',
lstep pr l pr'
-> forall ch, mayTouch pr' ch -> mayTouch pr ch.
Proof.
induct 1; invert 1; eauto;
eapply MtRecv2;
match goal with
| [ H : _ = _ |- _ ] => rewrite <- H; eauto
end.
Qed.
Hint Immediate lstep_mayTouch : core.
Lemma Input_mayTouch : forall pr ch (A : Type) (v : A) pr',
lstep pr (Action (Input {| Channel := ch; Value := v |})) pr'
-> mayTouch pr ch.
Proof.
induct 1; eauto.
Qed.
Lemma Output_mayTouch : forall pr ch (A : Type) (v : A) pr',
lstep pr (Action (Output {| Channel := ch; Value := v |})) pr'
-> mayTouch pr ch.
Proof.
induct 1; eauto.
Qed.
Hint Immediate Input_mayTouch Output_mayTouch : core.
Lemma independent_execution : forall pr1 pr2 pr,
lstepSilent^* (pr1 || pr2) pr
-> (forall ch, mayTouch pr1 ch -> mayTouch pr2 ch -> False)
-> exists pr1' pr2', pr = pr1' || pr2'
/\ lstepSilent^* pr1 pr1'
/\ lstepSilent^* pr2 pr2'.
Proof.
induct 1; simplify; eauto.
invert H.
specialize (IHtrc _ _ eq_refl).
match type of IHtrc with
| ?P -> _ => assert P by eauto
end.
first_order.
eauto 10.
specialize (IHtrc _ _ eq_refl).
match type of IHtrc with
| ?P -> _ => assert P by eauto
end.
first_order.
eauto 10.
exfalso; eauto.
exfalso; eauto.
Qed.
Theorem independently_deadlock_free : forall pr1 pr2,
invariantFor (trsys_of pr1)
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr')
-> invariantFor (trsys_of pr2)
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr')
-> (forall ch, mayTouch pr1 ch -> mayTouch pr2 ch -> False)
-> invariantFor (trsys_of (pr1 || pr2))
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr').
Proof.
unfold invariantFor; simplify.
propositional; subst.
apply independent_execution in H3; auto.
first_order; subst.
apply H in H3; apply H0 in H4; auto.
first_order; eauto.
Qed.
Ltac NoDup :=
repeat match goal with
| [ H : NoDup _ |- _ ] => invert H
end; simplify.
Ltac mayTouch :=
match goal with
| [ H : mayTouch (match ?E with _ => _ end) _ |- _ ] => cases E
| [ H : mayTouch _ _ |- _ ] => invert H; try solve [ equality ]
end.
Example online_store_no_deadlock' : forall k input output
product payment_info payment_checker in_stock
add_review payment_success send_payment_info
in_stock_or_not request_product
merchant_to_warehouse warehouse_to_merchant,
NoDup [input; output;
request_product; in_stock_or_not; send_payment_info; payment_success; add_review;
merchant_to_warehouse; warehouse_to_merchant]
-> invariantFor (trsys_of ((addN k input output
|| add2_client input output)
|| ((customer' request_product in_stock_or_not
send_payment_info payment_success add_review
product payment_info
|| (merchant' request_product in_stock_or_not
send_payment_info payment_success add_review
merchant_to_warehouse
warehouse_to_merchant payment_checker
|| (warehouse merchant_to_warehouse
warehouse_to_merchant
in_stock || Done))))))
(fun pr => inert pr
\/ exists pr', lstep pr Silent pr').
Proof.
simplify.
eapply independently_deadlock_free.
eapply invariant_weaken.
apply adding_no_deadlock.
NoDup; equality.
simplify.
first_order; subst; eauto.
apply online_store_no_deadlock'.
NoDup; repeat constructor; simplify; equality.
simplify.
NoDup; propositional.
generalize dependent H1.
repeat mayTouch; intro; repeat mayTouch.
Qed.