Proved atomicity, working on lifting

parent 953bbe8f
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
......@@ -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 :=
......
......@@ -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 Φ :
......
......@@ -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.
Markdown is supported
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