Commit ee56df0d authored by Hai Dang's avatar Hai Dang

alloc public

parent d9a5618d
......@@ -235,3 +235,10 @@ Proof.
simpl. rewrite Hfg. destruct (g y); last done.
by f_equal.
Qed.
Lemma repeat_lookup_lt_length `{A: Type} (a: A) (n: nat) :
i, (i < n)%nat repeat a n !! i = Some a.
Proof.
induction n as [|n IH]; intros i Lt; [lia|]; simpl.
destruct i as [|i]; [done|]. simpl. apply IH. lia.
Qed.
......@@ -372,7 +372,7 @@ Fixpoint write_local (l:loc) (n:nat) (t: ptr_id) (ls: lmap) : lmap :=
| S n => <[l := t]>(write_local (l + 1) n t ls)
end.
Definition res_loc l n t : resUR := (ε, fmap to_tagR (write_local l n t )).
Definition res_loc l n t : resUR := (ε, to_tagR <$> (write_local l n t )).
Definition res_mapsto (l:loc) (v: value) (t: ptr_id) : resUR :=
res_loc l (length v) t res_tag t tkUnique (write_mem l v ).
......@@ -388,6 +388,66 @@ Proof.
split. by destruct k. apply to_heapR_valid.
Qed.
Lemma res_tag_unique_pub_local_update (r: resUR) t h
(NONE: r.(rtm) !! t = None) :
(r res_tag t tkUnique h, res_tag t tkUnique h) ~l~>
(r res_tag t tkPub , res_tag t tkPub ).
Proof.
destruct r as [[tm cm] lm].
apply prod_local_update_1, prod_local_update_1. rewrite /=.
do 2 rewrite (cmra_comm tm) -insert_singleton_op //.
rewrite -(insert_insert tm t (Cinr (), to_agree <$> )
(Cinl (Excl ()), to_agree <$> h)).
eapply (singleton_local_update (<[t := _]> tm : tmapUR)).
by rewrite lookup_insert.
apply exclusive_local_update. split; [done|apply to_heapR_valid].
Qed.
Lemma res_tag_insert_local_update (r: resUR) h1 h2 (t: ptr_id)
(NONE: r.(rtm) !! t = None):
(r res_tag t tkUnique h1, res_tag t tkUnique h1) ~l~>
(r res_tag t tkUnique h2, res_tag t tkUnique h2).
Proof.
destruct r as [[tm cm] lm].
apply prod_local_update_1, prod_local_update_1. rewrite /=.
do 2 rewrite (cmra_comm tm) -insert_singleton_op //.
rewrite -(insert_insert tm t (_, to_agree <$> h2)
(Cinl (Excl ()), to_agree <$> h1)).
eapply (singleton_local_update (<[t := _]> tm : tmapUR)).
by rewrite lookup_insert.
apply exclusive_local_update. split; [done|apply to_heapR_valid].
Qed.
Lemma res_tag_1_insert_local_update (r: resUR) (l: loc) s1 s2 (t: ptr_id)
(NONE: r.(rtm) !! t = None):
(r res_tag t tkUnique {[l := s1]}, res_tag t tkUnique {[l := s1]}) ~l~>
(r res_tag t tkUnique {[l := s2]}, res_tag t tkUnique {[l := s2]}).
Proof. by apply res_tag_insert_local_update. Qed.
Lemma res_tag_1_insert_local_update_r (r: resUR) r' (l: loc) s1 s2 (t: ptr_id)
(NONE: r.(rtm) !! t = None):
(r res_tag t tkUnique {[l := s1]}, (ε, r') res_tag t tkUnique {[l := s1]}) ~l~>
(r res_tag t tkUnique {[l := s2]}, (ε, r') res_tag t tkUnique {[l := s2]}).
Proof.
destruct r as [[tm cm] lm].
apply prod_local_update_1, prod_local_update_1. rewrite /= 2!left_id.
do 2 rewrite (cmra_comm tm) -insert_singleton_op //.
rewrite -(insert_insert tm t (_, to_agree <$> {[l := s2]})
(Cinl (Excl ()), to_agree <$> {[l := s1]})).
eapply (singleton_local_update (<[t := _]> tm : tmapUR)).
by rewrite lookup_insert.
apply exclusive_local_update. split; [done|apply to_heapR_valid].
Qed.
Lemma res_tag_lookup (k: tag_kind) (h: heaplet) (t: ptr_id) :
(res_tag t k h).(rtm) !! t Some (to_tagKindR k, to_agree <$> h).
Proof. by rewrite lookup_insert. Qed.
Lemma res_tag_lookup_ne (k: tag_kind) (h: heaplet) (t t': ptr_id) (NEQ: t' t) :
(res_tag t k h).(rtm) !! t' None.
Proof. by rewrite lookup_insert_ne. Qed.
(** res_mapsto *)
Lemma write_local_lookup l n t ls :
( (i: nat), (i < n)%nat
......@@ -507,7 +567,8 @@ Proof.
rewrite /= 2!dom_insert IH //.
Qed.
Lemma write_local_res_local_update lsf l n t:
(** allocating locals *)
Lemma write_local_res_alloc_local_update lsf l n t:
( i, (i < n)%nat lsf !! (l + i) = None)
(lsf, ε) ~l~>
(lsf (to_tagR <$> write_local l n t ) : lmapUR, to_tagR <$> write_local l n t : lmapUR).
......@@ -533,7 +594,6 @@ Proof.
by apply alloc_local_update.
Qed.
Lemma res_mapsto_local_alloc_local_update lsf l v t:
lsf.(rtm) !! t = None
( i, (i < length v)%nat lsf.(rlm) !! (l + i) = None)
......@@ -543,22 +603,67 @@ Proof.
rewrite /res_mapsto (cmra_comm (res_loc _ _ _)).
etrans. by apply (res_tag_alloc_local_update _ t tkUnique (write_mem l v )).
rewrite !pair_op !right_id left_id /=. apply prod_local_update_2.
by apply write_local_res_local_update.
by apply write_local_res_alloc_local_update.
Qed.
(** deallocating locals *)
Lemma write_local_res_dealloc_local_update (lsf: lmapUR) l n t:
( i, (i < n)%nat lsf !! (l + i) = None)
(lsf (to_tagR <$> write_local l n t ) : lmapUR, (to_tagR <$> write_local l n t ) : lmapUR) ~l~>
(lsf : lmapUR, ε : lmapUR).
Proof.
revert l lsf.
induction n as [|n IH]; intros l lsf HL.
- rewrite /= fmap_empty right_id_L //.
- rewrite /= write_local_res_S.
rewrite (cmra_comm ({[l := to_tagR t]} : lmapUR) (to_tagR <$> write_local _ _ _ _)).
rewrite cmra_assoc.
have NEQ1: write_local (l + 1) n t !! l = None.
{ rewrite {1}/write_local write_local_plus1 //. }
have ?: (lsf (to_tagR <$> write_local (l + 1) n t )) !! l = None.
{ rewrite lookup_op lookup_fmap NEQ1 right_id_L.
specialize (HL O). rewrite shift_loc_0_nat in HL. apply HL. lia. }
etrans.
+ rewrite 2!(cmra_comm _ {[l := _]}) -insert_singleton_op; [|done].
rewrite -insert_singleton_op; [|by rewrite lookup_fmap NEQ1].
eapply (delete_local_update_cancelable _ _ l); [|by rewrite lookup_insert..].
apply _.
+ rewrite 2!delete_insert_delete delete_notin // delete_notin;
[|by rewrite lookup_fmap NEQ1].
apply (IH (l + 1)).
intros i Lt. rewrite shift_loc_assoc -(Nat2Z.inj_add 1).
apply HL. lia.
Qed.
Lemma res_mapsto_res_tag_public (r: resUR) l v t
(NONE1: i, (i < length v)%nat r.(rlm) !! (l + i) = None)
(NONE2: r.(rtm) !! t = None):
(r res_mapsto l v t, res_mapsto l v t) ~l~>
(r res_tag t tkPub , res_tag t tkPub ).
Proof.
rewrite /res_mapsto. destruct r as [[tm cm] lm].
rewrite (cmra_comm (res_loc _ _ _)) cmra_assoc. etrans.
- apply prod_local_update_2. rewrite /= right_id left_id.
by apply write_local_res_dealloc_local_update.
- rewrite !pair_op /= !right_id.
apply prod_local_update_1, prod_local_update_1. rewrite /=.
do 2 rewrite (cmra_comm tm) -insert_singleton_op //.
rewrite -(insert_insert tm t (Cinr (), to_agree <$> )
(Cinl (Excl ()), to_agree <$> (write_mem l v ))).
eapply (singleton_local_update (<[t := _]> tm : tmapUR)).
by rewrite lookup_insert.
apply exclusive_local_update. split; [done|apply to_heapR_valid].
Qed.
(** updating locals *)
Lemma res_mapsto_1_insert_local_update (r: resUR) (l: loc) s1 s2 (t: ptr_id)
(NONE1: r.(rlm) !! l = None) (NONE2: r.(rtm) !! t = None):
(r res_mapsto l [s1] t, res_mapsto l [s1] t) ~l~>
(r res_mapsto l [s2] t, res_mapsto l [s2] t).
Proof.
intros. destruct r as [[tm cm] lm].
rewrite !pair_op !right_id /= !left_id /=.
do 2 (rewrite (cmra_comm tm) -insert_singleton_op; [|done]). etrans.
- apply prod_local_update_1, prod_local_update_1.
rewrite /= left_id.
instantiate (1:= {[t := (Cinl (Excl ()), to_agree <$> <[l:=s2]> )]}).
eapply (singleton_local_update (<[t := _]> tm : tmapUR)). by rewrite lookup_insert.
apply exclusive_local_update. split; [done|apply to_heapR_valid].
- rewrite /res_mapsto !right_id_L /= insert_insert /=.
rewrite /res_loc /res_tag /= pair_op left_id right_id //.
intros. rewrite /res_mapsto cmra_assoc. etrans.
- eapply res_tag_1_insert_local_update_r.
by rewrite lookup_op NONE2 /= lookup_empty right_id_L.
- rewrite -(cmra_assoc r) 2!(cmra_comm (res_loc _ _ _)) 2!cmra_assoc.
rewrite /= insert_empty //.
Qed.
......@@ -9,6 +9,9 @@ Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
Notation "r |==> r'" := (viewshift wsat r r') (at level 65, format "r |==> r'").
Notation "r |={ σs , σt }=> r'" := (viewshift_state wsat r r' σs σt)
(at level 65, format "r |={ σs , σt }=> r'").
Notation rrel := (rrel vrel).
(** "modular" simulation relations dont make assumptions
......
......@@ -158,17 +158,17 @@ Proof.
Qed.
(** Viewshift *)
Definition viewshift (r1 r2: A) : Prop :=
r_f σs σt, wsat (r_f r1) σs σt wsat (r_f r2) σs σt.
Definition viewshift_state (r1 r2: A) (σs σt: state) :=
r_f, wsat (r_f r1) σs σt wsat (r_f r2) σs σt.
Lemma viewshift_sim_local_body r1 r2 n es σs et σt Φ :
viewshift r1 r2
Lemma viewshift_state_sim_local_body r1 r2 n es σs et σt Φ :
viewshift_state r1 r2 σs σt
sim_local_body r2 n es σs et σt Φ sim_local_body r1 n es σs et σt Φ.
Proof.
revert r1 r2 n es σs et σt Φ. pcofix CIH.
intros r1 r2 n es σs et σt Φ VS SIM.
pfold. punfold SIM; [|apply sim_local_body_mono].
intros NT r_f WSAT1. have WSAT2 := VS _ _ _ WSAT1.
intros NT r_f WSAT1. have WSAT2 := VS _ WSAT1.
specialize (SIM NT r_f WSAT2) as [NOTS TE SIM].
constructor; [done|..].
{ intros.
......@@ -184,6 +184,14 @@ Proof.
exists idx'. pclearbot. right. eapply CIH; eauto. done.
Qed.
Definition viewshift (r1 r2: A) : Prop :=
r_f σs σt, wsat (r_f r1) σs σt wsat (r_f r2) σs σt.
Lemma viewshift_sim_local_body r1 r2 n es σs et σt Φ :
viewshift r1 r2
sim_local_body r2 n es σs et σt Φ sim_local_body r1 n es σs et σt Φ.
Proof. intros VS. apply viewshift_state_sim_local_body. intros ?. by apply VS. Qed.
End local.
Hint Resolve sim_local_body_mono : paco.
This diff is collapsed.
......@@ -325,7 +325,8 @@ Lemma sim_simple_alloc_public fs ft r n T css cst Φ :
Φ (r rt) n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst)
r ⊨ˢ{n,fs,ft} (Alloc T, css) (Alloc T, cst) : Φ.
Proof.
Admitted.
intros HH σs σt <-<-. apply sim_body_alloc_shared=>/=. exact: HH.
Qed.
Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) css cst Φ :
rrel r rs1 rt1
......
......@@ -10,6 +10,14 @@ Lemma viewshift_frame_r r r1 r2 :
r1 |==> r2 (r1 r) |==> (r2 r).
Proof. intros VS ???. rewrite (cmra_comm r1) (cmra_comm r2) 2!cmra_assoc. apply VS. Qed.
Lemma viewshift_state_frame_l r r1 r2 σs σt :
r1 |={σs,σt}=> r2 (r r1) |={σs,σt}=> (r r2).
Proof. intros VS r_f. rewrite 2!cmra_assoc. apply VS. Qed.
Lemma viewshift_state_frame_r r r1 r2 σs σt :
r1 |={σs,σt}=> r2 (r1 r) |={σs,σt}=> (r2 r).
Proof. intros VS ?. rewrite (cmra_comm r1) (cmra_comm r2) 2!cmra_assoc. apply VS. Qed.
Lemma vs_call_empty_public c :
res_callState c (csOwned ) |==> res_callState c csPub.
Proof.
......
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