Commit a999d36c authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Made appropriate steps blocking steps.

parent bbd1e08d
......@@ -1500,6 +1500,42 @@ Module Choreography (Import E : Expression) (L : Locations).
| RAppGlobal => False
end.
Lemma RDefLocalNoBlockers : forall l e B C1 C2,
ChorStep (RDefLocal l e) B C1 C2 ->
B = [].
Proof using.
intros l e B C1 C2 step; dependent induction step;
repeat match goal with
| [H: _ :: _ = [] |- _ ] => inversion H
| [IH : forall a b, RDefLocal ?l ?e = RDefLocal a b -> _ |- _ ] =>
specialize (IH l e eq_refl)
end; auto.
Qed.
Lemma RAppLocalNoBlockers : forall l e B C1 C2,
ChorStep (RAppLocal l e) B C1 C2 ->
B = [].
Proof using.
intros l e B C1 C2 step; dependent induction step;
repeat match goal with
| [H: _ :: _ = [] |- _ ] => inversion H
| [IH : forall a b, RAppLocal ?l ?e = RAppLocal a b -> _ |- _ ] =>
specialize (IH l e eq_refl)
end; auto.
Qed.
Lemma RAppGlobalNoBlockers : forall B C1 C2,
ChorStep RAppGlobal B C1 C2 ->
B = [].
Proof using.
intros B C1 C2 step; dependent induction step;
repeat match goal with
| [H: _ :: _ = [] |- _ ] => inversion H
| [IH : ?a = ?a -> _ |- _ ] =>
specialize (IH eq_refl)
end; auto.
Qed.
Lemma NoChorStepInList : forall p B R,
In p B ->
InvolvedWithRedex R p ->
......
......@@ -438,14 +438,14 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
else if L.eq_dec l q
then Some (AllowChoiceLabel p LR)
else None
| C.RDefLocal p _ => Some Tau
| C.RDefLocal p _ => Some SyncTau
| C.RAppLocalE p _ _ =>
if L.eq_dec l p
then Some Tau
else None
| C.RAppLocal _ _ =>
Some Tau
| C.RAppGlobal => Some Tau
Some SyncTau
| C.RAppGlobal => Some SyncTau
end.
Theorem ProjectRedexBlocked : forall C1 R B C2 l,
......@@ -1023,10 +1023,10 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
| C.RSendE l e1 e2 l' => SysTau
| C.RSendV l v l' => CommLabel l v l'
| C.RSync l ch l' => ChoiceLabel l ch l'
| C.RDefLocal x x0 => SysTau
| C.RDefLocal x x0 => SysSyncTau
| C.RAppLocalE x x0 x1 => SysTau
| C.RAppLocal x x0 => SysTau
| C.RAppGlobal => SysTau
| C.RAppLocal x x0 => SysSyncTau
| C.RAppGlobal => SysSyncTau
end.
......@@ -1363,7 +1363,7 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
Lemma ProjectTauSystemTau : forall R l,
ProjectRedex R l = Some Tau -> RedexToSystemLabel R = SysTau.
Proof using.
intro R; destruct R; intros l'; cbn; intro eq; try reflexivity.
intro R; destruct R; intros l'; cbn; intro eq; try reflexivity; try discriminate.
destruct (L.eq_dec l' l); destruct (L.eq_dec l' l0); inversion eq.
destruct (L.eq_dec l' l); destruct (L.eq_dec l' l1); inversion eq.
Qed.
......@@ -1451,7 +1451,7 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
pose proof (IHnms R B C1 C2 c0 c2 eq1' eq2' eq3 step1).
destruct H1 as [Π2' [step2 lns]].
inversion step2; subst; try discriminate.
2,3: rewrite eq3 in H1; inversion H1.
2-4: rewrite eq3 in H1; inversion H1.
inversion eq1; inversion eq2; clear eq1 eq2; subst.
exists (LM.add l c1 Π2'); split; auto with ConExpr.
2: apply LessNondetSystemAdd; auto with ConExpr.
......@@ -1496,133 +1496,12 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
pose proof (LMF.MapsToUnique mt (LM.add_1 Π2' l c)); subst; apply LM.add_1.
Qed.
(* Lemma ProjectCommStep : forall B C1 C2 p v q Ep1 Ep2 Eq1 Eq2, *)
(* C.ChorStep (C.RSendV p v q) B C1 C2 -> *)
(* ProjectChor C1 p = Some Ep1 -> *)
(* ProjectChor C2 p = Some Ep2 -> *)
(* ProjectChor C1 q = Some Eq1 -> *)
(* ProjectChor C2 q = Some Eq2 -> *)
(* exists E2, *)
(* Ep1 = Send q v Ep2 /\ *)
(* Eq1 = Recv p E2 /\ *)
(* Eq2 = E2 [cel|ValSubst v]. *)
(* Proof using. *)
(* intros B C1 C2 p v q Ep1 Ep2 Eq1 Eq2 step; *)
(* revert Ep1 Ep2 Eq1 Eq2; generalize (@eq_refl _ (C.RSendV p v q)). *)
(* revert step. generalize (C.RSendV p v q) at 1 2. *)
(* intros R step; induction step; intro eqR; inversion eqR; subst; *)
(* repeat match goal with *)
(* | [ H : ?a = ?a |- _ ] => clear H *)
(* | [ H :?a = ?a -> _ |- _ ] => specialize (H eq_refl) *)
(* end; *)
(* intros Ep1 Ep2 Eq1 Eq2 eq1 eq2 eq3 eq4; cbn in *; *)
(* repeat match goal with *)
(* | [ H : None = Some _ |- _ ] => inversion H *)
(* | [ H : Some _ = Some _ |- _ ] => *)
(* inversion H; clear H; subst *)
(* | [ H : context[L.eq_dec ?a ?b] |- _ ] => *)
(* tryif unify a b *)
(* then let n := fresh in *)
(* destruct (L.eq_dec a b) as [_ | n]; *)
(* [| destruct (n eq_refl)] *)
(* else lazymatch goal with *)
(* | [e : a = b |- _ ] => *)
(* let n := fresh in *)
(* destruct (L.eq_dec a b) as [_ | n]; *)
(* [| destruct (n e)] *)
(* | [e : b = a |- _ ] => *)
(* let n := fresh in *)
(* destruct (L.eq_dec a b) as [_ | n]; *)
(* [| destruct (n (eq_sym e))] *)
(* | [n : a <> b |- _ ] => *)
(* let e := fresh in *)
(* destruct (L.eq_dec a b) as [e | _]; *)
(* [destruct (n e)|] *)
(* | [n : b <> a |- _ ] => *)
(* let e := fresh in *)
(* destruct (L.eq_dec a b) as [e | _]; *)
(* [destruct (n (eq_sym e))|] *)
(* | _ => let eq := fresh "eq" in *)
(* let neq := fresh "neq" in *)
(* destruct (L.eq_dec a b) as [eq|neq]; subst *)
(* end *)
(* | [ H : context[ExprEqDec ?a ?b] |- _ ] => *)
(* tryif unify a b *)
(* then let n := fresh in *)
(* destruct (ExprEqDec a b) as [_ | n]; *)
(* [| destruct (n eq_refl)] *)
(* else lazymatch goal with *)
(* | [e : a = b |- _ ] => *)
(* let n := fresh in *)
(* destruct (ExprEqDec a b) as [_ | n]; *)
(* [| destruct (n e)] *)
(* | [e : b = a |- _ ] => *)
(* let n := fresh in *)
(* destruct (ExprEqDec a b) as [_ | n]; *)
(* [| destruct (n (eq_sym e))] *)
(* | [n : a <> b |- _ ] => *)
(* let e := fresh in *)
(* destruct (ExprEqDec a b) as [e | _]; *)
(* [destruct (n e)|] *)
(* | [n : b <> a |- _ ] => *)
(* let e := fresh in *)
(* destruct (ExprEqDec a b) as [e | _]; *)
(* [destruct (n (eq_sym e))|] *)
(* | _ => let eq := fresh "eq" in *)
(* let neq := fresh "neq" in *)
(* destruct (ExprEqDec a b) as [eq|neq]; subst *)
(* end *)
(* | [ H : context[ProjectChor ?C ?l] |- _ ] => *)
(* lazymatch type of H with *)
(* | ProjectChor C l = _ => fail *)
(* | _ => *)
(* lazymatch goal with *)
(* | [ eq : ProjectChor C l = _ |- _ ] => rewrite eq in H *)
(* | _ => let eq := fresh "eq" in destruct (ProjectChor C l) eqn:eq *)
(* end *)
(* end *)
(* | [H : C.ChorStep (C.RSendV ?a ?v ?b) (?a :: _) _ _ |- _ ] => *)
(* exfalso; eapply C.NoChorStepInList with (p := a); eauto; [left; reflexivity| cbn; left; auto] *)
(* | [H : C.ChorStep (C.RSendV ?a ?v ?b) (?b :: _) _ _ |- _ ] => *)
(* exfalso; eapply C.NoChorStepInList with (p := b); eauto; [left; reflexivity|cbn; right; auto] *)
(* | [H : C.ChorStep (C.RSendV ?a ?v ?b) (_ :: ?a :: _) _ _ |- _ ] => *)
(* exfalso; eapply C.NoChorStepInList with (p := a); eauto; [right; left; reflexivity|cbn; left; auto] *)
(* | [H : C.ChorStep (C.RSendV ?a ?v ?b) (_ :: ?b :: _) _ _ |- _ ] => *)
(* exfalso; eapply C.NoChorStepInList with (p := b); eauto; [right; left; reflexivity|cbn; right; auto] *)
(* | [ IH : forall Ep1 Ep2 Eq1 Eq2, *)
(* Some ?E1 = Some Ep1 -> *)
(* Some ?E2 = Some Ep2 -> *)
(* Some ?E3 = Some Eq1 -> *)
(* Some ?E4 = Some Eq2 -> *)
(* exists E2', _ /\ _ /\ _ |- _ ] => *)
(* let E2' := fresh "E" in *)
(* let eq1 := fresh "eq" in *)
(* let eq2 := fresh "eq" in *)
(* let eq3 := fresh "eq" in *)
(* destruct (IH E1 E2 E3 E4 eq_refl eq_refl eq_refl eq_refl) as [E2' [eq1 [eq2 eq3]]]; subst; clear IH *)
(* end; try discriminate. *)
(* - exists E; split; [|split]; auto. *)
(* - rewrite ProjectChorExprSubst with (E := c0) in eq2; auto; *)
(* inversion eq2; clear eq2; subst. *)
(* unfold C.ValueSubst. destruct (L.eq_dec q p) as [ e|_]; [destruct (H1 (eq_sym e))|]. *)
(* rewrite ConExprLocalIdSubst. *)
(* rewrite ProjectChorExprSubst with (E := c) in eq4; auto; *)
(* inversion eq4; clear eq4; subst. *)
(* unfold C.ValueSubst. destruct (L.eq_dec q q) as [_|n];[|destruct (n eq_refl)]. *)
(* fold (ValSubst v). *)
(* exists c; split; [|split]; reflexivity. *)
(* - cbn in eq1. cbn in eq3. *)
(* destruct (L.eq_dec q q) as [_|n];[|destruct (n eq_refl)]. *)
(* destruct (ExprEqDec v v) as [_|n];[|destruct (n eq_refl)]. *)
(* rewrite eq2 in eq1. inversion eq1; clear eq1; subst. *)
(* destruct (L.eq_dec p p) as [_|n]; [|destruct (n eq_refl)]. *)
(* destruct (ConExprMerge E E0) as [E'|] eqn:eqE'; [|inversion eq3]. *)
(* rewrite MergeExprSubst with (E := E') in eq4; auto. inversion eq4; clear eq4; subst. *)
(* inversion eq3; clear eq3; subst. *)
(* exists E'; split; [|split]; reflexivity. *)
(* - *)
Lemma RedexSysSyncTauSyncTau : forall R,
RedexToSystemLabel R = SysSyncTau ->
forall l, ProjectRedex R l = Some SyncTau.
Proof using.
intros R eq l; destruct R; cbn in eq; try discriminate; reflexivity.
Qed.
Theorem SystemOfNamesCompleteness : forall R B C1 C2 Π1 Π2 nms,
SystemOfNames C1 nms = Some Π1 ->
......@@ -1635,6 +1514,13 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
destruct (RedexToSystemLabel R) eqn:eqR.
- pose proof (ProjectSystemTauSteps R B C1 C2 Π1 Π2 nms eq1 eq2 eqR step).
rewrite eqR in H; auto.
- clear allinvolved.
exists Π2; split; [constructor | reflexivity].
intros l E1 E2 mt1 mt2.
pose proof (RedexSysSyncTauSyncTau R eqR l).
destruct (proj1 (SystemOfNamesLookup C1 nms Π1 eq1 l E1) mt1) as [i proj_l_1].
destruct (proj1 (SystemOfNamesLookup C2 nms Π2 eq2 l E2) mt2) as [_ proj_l_2].
apply (ProjectChorStep1 C1 R B C2 l E1 E2 SyncTau proj_l_1 proj_l_2 H step).
- rename l into p; rename l0 into q.
destruct R; cbn in eqR; inversion eqR; subst; clear eqR.
cbn in allinvolved; pose proof (allinvolved p ltac:(auto)) as p_i;
......
......@@ -1150,6 +1150,7 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
Inductive Label : Set :=
Tau : Label (* Internal steps *)
| SyncTau : Label (* Internal steps everyone needs to synchronize on *)
| SendLabel : Loc -> Expr -> Label
| RecvLabel : Loc -> Expr -> Label
| ChooseLabel : Loc -> LRChoice -> Label
......@@ -1196,7 +1197,7 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
| LetRetEStep : forall E1 L E1' E2,
ConExprStep E1 L E1' -> ConExprStep (LetRet E1 E2) L (LetRet E1' E2)
| LetRetStep : forall v E2,
ExprVal v -> ConExprStep (LetRet (Ret v) E2) Tau (E2 [cel| ValSubst v])
ExprVal v -> ConExprStep (LetRet (Ret v) E2) SyncTau (E2 [cel| ValSubst v])
| AppLocalFunStep : forall F1 L F2 e,
ConExprStep F1 L F2 ->
ConExprStep (AppLocal F1 e) L (AppLocal F2 e)
......@@ -1205,7 +1206,7 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
ConExprStep (AppLocal (RecLocal F) e1) Tau (AppLocal (RecLocal F) e2)
| AppLocalStep : forall F v,
ExprVal v ->
ConExprStep (AppLocal (RecLocal F) v) Tau
ConExprStep (AppLocal (RecLocal F) v) SyncTau
((F [cel| ValSubst v]) [ceg| RecLocalSubst F])
| AppGlobalFunStep : forall F1 L F2 A,
ConExprStep F1 L F2 ->
......@@ -1215,7 +1216,7 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
ConExprStep (AppGlobal (RecGlobal F) A1) L (AppGlobal (RecGlobal F) A2)
| AppGlobalStep : forall B V,
ConExprVal V ->
ConExprStep (AppGlobal (RecGlobal B) V) Tau (B [ceg| RecGlobalSubst B V]).
ConExprStep (AppGlobal (RecGlobal B) V) SyncTau (B [ceg| RecGlobalSubst B V]).
Global Hint Constructors ConExprStep : ConExpr.
Inductive ConExprSteps : ConExpr -> list Label -> ConExpr -> Prop :=
......@@ -1415,17 +1416,24 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
end
end; try discriminate; eauto with ConExpr.
- destruct E1; cbn in eq; inversion eq; subst. inversion step1.
destruct (ExprEqDec e v); inversion eq; subst; clear eq.
inversion step1; subst.
apply NoExprStepFromVal in H2; auto; destruct H2.
- destruct E1; cbn in merge1; try discriminate; inversion H0; subst.
destruct (ExprEqDec v e); inversion merge1; subst; clear merge1.
apply NoExprStepFromVal in H3; auto; destruct H3.
- destruct E1; cbn in merge1; try discriminate.
destruct (ExprEqDec v e); discriminate.
- destruct F1; cbn in eq0; try discriminate; inversion step1.
- destruct F1; cbn in eq; try discriminate; inversion eq; subst; clear eq;
inversion step1.
- destruct E1; cbn in eq; inversion eq; subst; try (inversion merge1; fail).
destruct (ExprEqDec v e); inversion eq; subst; clear eq.
inversion H0. inversion merge1.
- destruct E1; cbn in eq; inversion eq; subst; try (inversion merge1; fail).
destruct (ExprEqDec v e); inversion merge1.
- destruct F1; cbn in eq0; try discriminate.
destruct (ConExprEqDec F1 F); inversion eq0; clear eq0; subst.
destruct F2; cbn in eq; try discriminate.
destruct (ConExprEqDec F2 F); inversion eq; clear eq; subst.
constructor; auto.
- destruct F; cbn in merge2; try discriminate.
destruct n; cbn in merge2; discriminate.
destruct (ExprEqDec v (e [e|ValSubst v])); subst; try discriminate.
destruct (ConExprMerge F2 ((F [cel|ValSubst v]) [ceg| RecLocalSubst (AppLocal F e)])) eqn:eq1; try discriminate.
destruct F1; cbn in eq; try discriminate.
destruct (ConExprEqDec F1 (AppLocal F e)); inversion eq; clear eq; subst.
inversion merge2; clear merge2; subst.
inversion step1.
- destruct F1; try discriminate; inversion H0.
- destruct F1; try discriminate; inversion H0.
- destruct F1; try discriminate; cbn in eq1.
......@@ -1450,7 +1458,6 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
- destruct F1; try discriminate; inversion H0.
- destruct (MergeConExprVals V A1 c eq H); subst.
destruct c; inversion H; subst; inversion H0; subst.
apply NoExprStepFromVal in H3; auto; destruct H3.
- destruct (MergeConExprVals V V0 c eq H); subst.
rewrite MergeIdempotent in merge2; inversion merge2; subst; auto.
Qed.
......@@ -2117,6 +2124,7 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
Inductive SystemLabel : Set :=
SysTau : SystemLabel (* Internal steps *)
| SysSyncTau : SystemLabel
| CommLabel : Loc -> Expr -> Loc -> SystemLabel
| ChoiceLabel : Loc -> LRChoice -> Loc -> SystemLabel.
Global Hint Constructors SystemLabel : ConExpr.
......@@ -2128,6 +2136,12 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
LM.MapsTo p E2 Π2 ->
(forall q E, p <> q -> LM.MapsTo q E Π1 <-> LM.MapsTo q E Π2) ->
SystemStep Π1 SysTau Π2
| SyncTauStep : forall Π1 Π2,
(forall p E1 E2,
LM.MapsTo p E1 Π1 ->
LM.MapsTo p E2 Π2 ->
ConExprStep E1 SyncTau E2) ->
SystemStep Π1 SysSyncTau Π2
| CommStep : forall p q Π1 Π2 pE1 pE2 qE1 qE2 v,
LM.MapsTo p pE1 Π1 ->
LM.MapsTo q qE1 Π1 ->
......@@ -2160,6 +2174,12 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
/\ ConExprStep E1 Tau E2) ->
(forall p E, ~ In p nms -> LM.MapsTo p E Π1 <-> LM.MapsTo p E Π2) ->
SystemParStep Π1 SysTau Π2
| SyncTauStepPar : forall Π1 Π2,
(forall p E1 E2,
LM.MapsTo p E1 Π1 ->
LM.MapsTo p E2 Π2 ->
ConExprStep E1 SyncTau E2) ->
SystemParStep Π1 SysSyncTau Π2
| CommStepPar : forall p q Π1 Π2 pE1 pE2 qE1 qE2 v,
LM.MapsTo p pE1 Π1 ->
LM.MapsTo q qE1 Π1 ->
......@@ -2228,6 +2248,8 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
apply PlusStep with (C2 := LM.add l E2 Π1); auto.
apply H2. intros q E H4; split; intro mt.
apply LM.add_2; auto. apply LM.add_3 in mt; auto.
- exists [SysSyncTau]; apply PlusStep with (C2 := Π2); [|apply ZeroSteps; reflexivity].
econstructor; eauto.
- exists [CommLabel p v q]; apply PlusStep with (C2 := Π2); [|apply ZeroSteps; reflexivity].
econstructor; eauto.
- exists [ChoiceLabel p LR q];
......@@ -2455,6 +2477,5 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
destruct H2 as [E3 [mt lnd]].
exists E3; split; auto. apply LM.add_2; auto.
Qed.
End InternalConcurrentLambda.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment