From 4f51005a319c3855074e515ac48d8851bc7889da Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Thu, 18 Jan 2018 15:11:23 +0100 Subject: [PATCH] Proved atomicity, working on lifting --- notes/example_code | 37 +++++++++++++++++++ theories/dist_lang/lang.v | 18 ++++++---- theories/dist_lang/lifting.v | 15 ++++++++ theories/dist_lang/tactics.v | 70 ++++++++++++++++-------------------- 4 files changed, 94 insertions(+), 46 deletions(-) create mode 100644 notes/example_code diff --git a/notes/example_code b/notes/example_code new file mode 100644 index 00000000..c94549cb --- /dev/null +++ b/notes/example_code @@ -0,0 +1,37 @@ + +let (c,c') := newch in +start c ((c) => send c ((recv c) + (recv c))); +send c 1; +send c 2; +recv c + +-------------------------- + +let c = start ((c) => send c ((recv c) + (recv c))); +send c 1; +send c 2; +recv c + +-------------------------- + + + +Start c f + +Start c (c => e) ===> Start c (c => e) ===> () | (c => e)c' +Start (c => e) ===> let (c,c') = newch in Start c (c => e); c + + + +Start c c' e + +start c (c' => e) ===> Start c c' e +start (c => e) ===> let (c,c') = newch in Start c' c e); c' + + +Start c e + +Start c' (c => e) ===> let (c,c') = newch in Start c e; c +Start (c => e) ===> Start c e + + diff --git a/theories/dist_lang/lang.v b/theories/dist_lang/lang.v index 935e346e..e6b4d451 100644 --- a/theories/dist_lang/lang.v +++ b/theories/dist_lang/lang.v @@ -72,7 +72,7 @@ Inductive expr := | Send (c e : expr) | Recv (c : expr). -Bind Scope expr_scope with expr. +(* Bind Scope expr_scope with expr. *) Fixpoint is_closed (X : list string) (e : expr) : bool := match e with @@ -100,7 +100,7 @@ Inductive val := | InjLV (v : val) | InjRV (v : val). -Bind Scope val_scope with val. +(* Bind Scope val_scope with val. *) Fixpoint of_val (v : val) : expr := match v with @@ -289,8 +289,9 @@ Inductive ectx_item := | CasRCtx (v0 : val) (v1 : val) | FaaLCtx (e2 : expr) | FaaRCtx (v1 : val) - | StartLCtx (e2 : expr) - | StartRCtx (v1 : val) + | StartCtx (e2 : expr) + (* | StartLCtx (e2 : expr) *) + (* | StartRCtx (v1 : val) *) | SendLCtx (e2 : expr) | SendRCtx (v1 : val) | RecvCtx. @@ -319,8 +320,9 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr := | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e | FaaLCtx e2 => FAA e e2 | FaaRCtx v1 => FAA (of_val v1) e - | StartLCtx e2 => Start e e2 - | StartRCtx v1 => Start (of_val v1) e + | StartCtx e2 => Start e e2 + (* | StartLCtx e2 => Start e e2 *) + (* | StartRCtx v1 => Start (of_val v1) e *) | SendLCtx e2 => Send e e2 | SendRCtx v1 => Send (of_val v1) e | RecvCtx => Recv e @@ -504,9 +506,13 @@ Definition state'' := prod processes channels. Definition pexpr := prod loc expr. Definition pexpr_to_expr (pe : pexpr) : expr := pe.2. +Bind Scope expr_scope with pexpr. + Definition pval := prod loc val. Definition pval_to_val (pv : pval) : val := pv.2. +Bind Scope val_scope with pval. + Definition of_val'' (v : pval) : pexpr := (v.1, of_val (pval_to_val v)). Definition to_val'' (e : pexpr) : option pval := diff --git a/theories/dist_lang/lifting.v b/theories/dist_lang/lifting.v index 51db7094..2accd1af 100644 --- a/theories/dist_lang/lifting.v +++ b/theories/dist_lang/lifting.v @@ -137,6 +137,21 @@ Implicit Types P Q : iProp Σ. Implicit Types Φ : val → iProp Σ. Implicit Types efs : list expr. Implicit Types σ : state. +(* Implicit Types Φ : pval → iProp Σ. *) +(* Implicit Types efs : list pexpr. *) +(* Implicit Types σ : state''. *) + + +(** Base axioms for core primitives of the language: Stateless reductions *) +Lemma wp_fork s E e Φ : + (* ▷ Φ (p, LitV LitUnit) ∗ ▷ WP (p,e) @ s; ⊤ {{ _, True }} ⊢ WP (p, Fork e) @ s; E {{ Φ }}. *) + ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}. +Proof. + rewrite -(wp_lift_pure_det_head_step ((p, Fork e):pexpr) (p, Lit LitUnit) [(p,e)]) //=; eauto. + - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ ((p, Lit _):pexpr)) // right_id. + - intros; inv_head_step; eauto. +Qed. + (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork s E e Φ : diff --git a/theories/dist_lang/tactics.v b/theories/dist_lang/tactics.v index 4e006eb9..3e3c44a3 100644 --- a/theories/dist_lang/tactics.v +++ b/theories/dist_lang/tactics.v @@ -108,6 +108,13 @@ Ltac of_expr e := constr:(CAS e0 e1 e2) | dist_lang.FAA ?e1 ?e2 => let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2) + | dist_lang.Start ?e1 ?e2 => + let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Start e1 e2) + | dist_lang.NewChan => constr:(NewChan) + | dist_lang.Send ?e1 ?e2 => + let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Send e1 e2) + | dist_lang.Recv ?e => + let e := of_expr e in constr:(Recv e) | to_expr ?e => e | of_val ?v => constr:(Val v (of_val v) (to_of_val v)) | _ => match goal with @@ -116,7 +123,7 @@ Ltac of_expr e := end end. -(* Ltac of_expr'' e := constr:(e.1, of_expr e.2). *) +Ltac of_expr'' e := let e2 := of_expr e.2 in constr:(e.1 * e2). Fixpoint is_closed (X : list string) (e : expr) : bool := match e with @@ -212,9 +219,10 @@ Definition is_atomic (e : expr) := (* Make "skip" atomic *) | App (Rec _ _ (Lit _)) (Lit _) => true | NewChan => true - | Start c _ => bool_decide (is_Some (to_val c)) + (* | Start e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2)) (* WRONG *) *) + | Start c _ => bool_decide (is_Some (to_val c) ∧ is_Some (to_val e)) | Send c e => bool_decide (is_Some (to_val c) ∧ is_Some (to_val e)) - | Recv c => bool_decide (is_Some (to_val c)) + (* | Recv c => bool_decide (is_Some (to_val c)) *) | _ => false end. @@ -222,45 +230,23 @@ Definition is_atomic'' (e : pexpr) := is_atomic e.2. Lemma is_atomic_correct s e : is_atomic'' e → Atomic s (to_expr'' e). Proof. - intros He. apply strongly_atomic_atomic, ectx_language_atomic. - (* - intros σ e' σ' ef Hstep. simpl in *. revert Hstep. *) - (* destruct e=> //=. *) - - (* intros He. apply strongly_atomic_atomic, ectx_language_atomic. *) - - intros σ e' σ' ef Hstep. simpl in *. unfold is_atomic'' in He. apply to_val_val''. - revert Hstep. inversion 1. - + revert H8. inversion 1; - first(revert H16; destruct e; simpl in *; + intros He. unfold is_atomic'' in He. unfold to_expr''. destruct e. simpl in *. + apply strongly_atomic_atomic, ectx_language_atomic. + - intros σ e' σ' ef Hstep. simpl in *. apply to_val_val''. + revert Hstep. inversion 1. + + revert H8. inversion 1; + first(revert H16; (* head_step case *) destruct e=> //=; repeat (simplify_eq/=; case_match=>//); inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto; - unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto). - revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - revert H8. (* Prove absurdity *) destruct e. destruct e. simpl in *. subst. destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - - - * revert H8. destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - revert H8. inversion 1. simplify_eq. - revert H10. - - - repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto; - revert H10; - destruct e=> //=; repeat (simplify_eq/=; case_match=>//); - inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. - unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto. - - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill. + unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto); + repeat(revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//); + inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto). + (* * (* destruct e. *) simpl in *. subst. unfold to_expr in H9. destruct e; try inversion H9; try inversion He. *) + + revert Hstep. + destruct e=> //=; repeat (simplify_eq/=; case_match=>//); + inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. + - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill. unfold fill_item'' in Hfill. apply to_val_val''. inversion Hfill. + destruct e'. simpl in *. (* inversion Hfill. inversion H1. *) destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//); naive_solver eauto using to_val_is_Some. Qed. @@ -354,4 +340,8 @@ Ltac reshape_expr e tac := | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0 | FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2) | FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1 + | Start ?e1 ?e2 => go (StartCtx e2 :: K) e1 + | Send ?e1 ?e2 => go (SendLCtx e2 :: K) e1 + | Send ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (SendRCtx v1 :: K) e2) + | Recv ?e => go (RecvCtx :: K) e end in go (@nil ectx_item) e. -- GitLab