Commit 020277ad authored by Hai Dang's avatar Hai Dang
Browse files

parallelize body.v and one_step.v

parent 2ad7eef7
......@@ -21,6 +21,7 @@ theories/sim/local.v
theories/sim/local_adequacy.v
theories/sim/program.v
theories/sim/sflib.v
theories/sim/instance.v
theories/sim/body.v
theories/sim/one_step.v
theories/opt/ex1.v
......
From stbor.lang Require Import steps_inversion.
From stbor.sim Require Import local invariant.
From stbor.sim Require Export instance.
Set Default Proof Using "Type".
Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
(sim_local_body wsat vrel_expr fs ft r n%nat es%E σs et%E σt Φ)
(at level 70, format "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ").
Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
(sim_local_fun wsat vrel_expr fs ft end_call_sat f1 f2)
(at level 70, format "⊨{ fs , ft } f1 ≥ᶠ f2").
Instance dom_proper `{Countable K} {A : cmraT} :
Proper (() ==> ()) (dom (M:=gmap K A) (gset K)).
Proof.
intros m1 m2 Eq. apply elem_of_equiv. intros i.
by rewrite !elem_of_dom Eq.
Qed.
Lemma sim_body_res_proper fs ft n es σs et σt Φ r1 r2:
r1 r2
r1 {n,fs,ft} (es, σs) (et, σt) : Φ
......@@ -78,22 +63,6 @@ Lemma sim_body_frame fs ft n (rf r: resUR) es σs et σt Φ :
(λ r' n' es' σs' et' σt', r0, r' rf r0 Φ r0 n' es' σs' et' σt').
Proof. intros. eapply sim_body_frame'; eauto. Qed.
Lemma sim_body_result fs ft r n es et σs σt Φ :
( r Φ r n es σs et σt : Prop)
r {S n,fs,ft} (of_result es, σs) (of_result et, σt) : Φ.
Proof.
intros POST. pfold. split; last first.
{ constructor 1. intros vt' ? STEPT'. exfalso.
apply result_tstep_stuck in STEPT'. by rewrite to_of_result in STEPT'. }
{ move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
exists es, σs, r, n. split; last split.
- right. split; [lia|]. eauto.
- eauto.
- rewrite to_of_result in Eqvt'. simplify_eq.
apply POST. by destruct WSAT as (?&?&?%cmra_valid_op_r &?). }
{ left. rewrite to_of_result. by eexists. }
Qed.
Lemma sim_body_val_elim fs ft r n vs σs vt σt Φ :
r {n,fs,ft} ((Val vs), σs) ((Val vt), σt) : Φ
r_f (WSAT: wsat (r_f r) σs σt),
......
......@@ -232,6 +232,7 @@ Proof.
by rewrite (ptrmap_lookup_op_r _ _ _ _ VALID Eqtg).
Qed.
(** heaplet *)
Lemma to_heapletR_valid h : (to_heapletR h).
Proof.
intros l. rewrite /to_heapletR lookup_fmap.
......@@ -246,6 +247,13 @@ Proof.
intros Eq%Some_equiv_inj%to_agree_inj. by inversion Eq.
Qed.
Lemma heapletR_elem_of_dom (h: heapletR) l (VALID: valid h) :
l dom (gset loc) h s, h !! l Some (to_agree s).
Proof.
rewrite elem_of_dom. intros [sa Eqs]. move : (VALID l). rewrite Eqs.
intros [s Eq]%to_agree_uninj. exists s. by rewrite Eq.
Qed.
(** The Core *)
Lemma heaplet_core (h: heapletR) : core h = h.
......
From stbor.lang Require Import steps_inversion.
From stbor.sim Require Export local invariant.
Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
(sim_local_body wsat vrel_expr fs ft r n%nat es%E σs et%E σt Φ)
(at level 70, format "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ").
Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
(sim_local_fun wsat vrel_expr fs ft end_call_sat f1 f2)
(at level 70, format "⊨{ fs , ft } f1 ≥ᶠ f2").
Instance dom_proper `{Countable K} {A : cmraT} :
Proper (() ==> ()) (dom (M:=gmap K A) (gset K)).
Proof.
intros m1 m2 Eq. apply elem_of_equiv. intros i.
by rewrite !elem_of_dom Eq.
Qed.
Lemma sim_body_result fs ft r n es et σs σt Φ :
( r Φ r n es σs et σt : Prop)
r {S n,fs,ft} (of_result es, σs) (of_result et, σt) : Φ.
Proof.
intros POST. pfold. split; last first.
{ constructor 1. intros vt' ? STEPT'. exfalso.
apply result_tstep_stuck in STEPT'. by rewrite to_of_result in STEPT'. }
{ move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
exists es, σs, r, n. split; last split.
- right. split; [lia|]. eauto.
- eauto.
- rewrite to_of_result in Eqvt'. simplify_eq.
apply POST. by destruct WSAT as (?&?&?%cmra_valid_op_r &?). }
{ left. rewrite to_of_result. by eexists. }
Qed.
From iris.algebra Require Import local_updates.
From stbor.lang Require Import steps_progress steps_inversion.
From stbor.sim Require Export local invariant body.
From stbor.sim Require Export instance.
Set Default Proof Using "Type".
......@@ -194,7 +194,12 @@ Proof.
destruct ss as [| |l1 [t1|]|], st as [| |l2 [t2|]|]; auto; simpl; [|by intros [?[]]].
intros [? [? [h' Eqh']]]. simplify_eq. do 2 (split; [done|]).
exists h'. by apply ptrmap_lookup_core_pub. }
destruct PV as (c' & T' & h' & Eqci & InT').
destruct PV as (c' & T' & h' & Eqci & InT' & Eqh' & Inl).
specialize (CINV _ _ Eqci) as [Inc' CINV].
specialize (CINV _ InT') as [Ltt' CINV].
specialize (CINV _ _ Eqh' _ Inl) as (stk & pm & Eqstk & Instk).
specialize (PINV _ _ _ Eqh') as [_ PINV].
(* impossible: t' is protected by c' which is still active.
So t t' and protected(t',c') is on top of (l + i), so access with t is UB *)
admit.
......
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