Commit c69ae521 authored by Hai Dang's avatar Hai Dang

WIP: retag public

parent 383206b7
...@@ -322,6 +322,8 @@ Definition retag_ref α cids (nxtp: ptr_id) l (old_tag: tag) T ...@@ -322,6 +322,8 @@ Definition retag_ref α cids (nxtp: ptr_id) l (old_tag: tag) T
end in end in
(* reborrow old_tag with new_tag *) (* reborrow old_tag with new_tag *)
α' reborrow α cids l old_tag T kind new_tag protector; α' reborrow α cids l old_tag T kind new_tag protector;
(* TODO: this always increments the [nxtp] field, even though that is not
necessary when new_tag = Untagged *)
Some (new_tag, α', S nxtp) Some (new_tag, α', S nxtp)
end. end.
......
...@@ -868,84 +868,6 @@ Proof. ...@@ -868,84 +868,6 @@ Proof.
eapply retag_head_step'; eauto. eapply retag_head_step'; eauto.
Qed. Qed.
Lemma retag_mut_ref_change α cids c nxtp l otag ntag rk mut T α' nxtp':
retag α nxtp cids c l otag rk (RefPtr mut) T = Some (ntag, α', nxtp')
let rk' := if mut then UniqueRef (is_two_phase rk) else SharedRef in
retag_ref α cids nxtp l otag T rk' (adding_protector rk c) =
Some (ntag, α', nxtp').
Proof.
rewrite /retag; destruct mut, rk; simpl;
(case retag_ref as [[[t1 α1] n1]|] eqn:Eq => [/= //|//]).
Qed.
(* Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp'
(TS: (O < tsize T)%nat) :
retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp')
l otag, h !! x = Some (ScPtr l otag)
rk' new,
h' = <[x := ScPtr l new]>h
retag_ref h α cids nxtp l otag T rk' (adding_protector rk c) =
Some (new, α', nxtp')
rk' = if mut then UniqueRef (is_two_phase rk) else SharedRef.
Proof.
rewrite retag_equation_2 /=.
destruct (h !! x) as [[| |l t|]|]; simpl; [done..| |done|done].
destruct mut; (case retag_ref as [[[t1 α1] n1]|] eqn:Eq => [/=|//]);
intros; simplify_eq; exists l, t; (split; [done|]);
eexists; exists t1; done.
Qed.
Lemma retag_ref_change_2
h α cids c nxtp l otag rk b (mut: mutability) T new α' nxtp'
(TS: (O < tsize T)%nat)
(FRZ: if mut is Immutable then is_freeze T else True) :
let rk' := if mut is Immutable then SharedRef else UniqueRef b in
let opro := (adding_protector rk c) in
retag_ref h α cids nxtp l otag T rk' opro = Some (new, α', nxtp')
nxtp' = S nxtp new = Tagged nxtp
reborrowN α cids l (tsize T) otag (Tagged nxtp)
(if mut then Unique else SharedReadOnly) opro = Some α'.
Proof.
intros rk' opro. rewrite /retag_ref. destruct (tsize T) as [|n] eqn:EqT; [lia|].
destruct mut; simpl; [destruct b|rewrite visit_freeze_sensitive_is_freeze //];
case reborrowN as [α1|] eqn:Eq1 => [/=|//]; intros; simplify_eq. by rewrite -EqT.
Qed.
Lemma retag_ref_change h α cids c nxtp x rk mut T h' α' nxtp'
(TS: (O < tsize T)%nat)
(FRZ: if mut is Immutable then is_freeze T else True) :
retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp')
l otag, h !! x = Some (ScPtr l otag)
h' = <[x := ScPtr l (Tagged nxtp)]>h
nxtp' = S nxtp
reborrowN α cids l (tsize T) otag (Tagged nxtp)
(if mut then Unique else SharedReadOnly) (adding_protector rk c) = Some α'.
Proof.
intros RT.
apply retag_ref_change_1 in RT
as (l & otag & EqL & rk' & new & Eqh & RT &?); [|done..].
subst. exists l, otag. split; [done|].
destruct rk; simpl in RT.
apply retag_ref_change_2 in RT as (?&?&?); [|done..]. by subst new.
Qed.
Lemma retag_ref_reborrowN
(h: mem) α t cids c x l otg T rk (mut: mutability) α'
(N2: rk TwoPhase) (TS: (O < tsize T)%nat)
(FRZ: if mut is Immutable then is_freeze T else True) :
h !! x = Some (ScPtr l otg)
reborrowN α cids l (tsize T) otg (Tagged t)
(if mut then Unique else SharedReadOnly) (adding_protector rk c) =
Some α'
retag h α t cids c x rk (Reference (RefPtr mut) T) =
Some (<[x:=ScPtr l (Tagged t)]> h, α', S t).
Proof.
intros Eqx RB. rewrite retag_equation_2 Eqx /= /retag_ref.
destruct (tsize T) eqn:EqT; [lia|].
rewrite (_: is_two_phase rk = false); [|by destruct rk].
destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //]; rewrite EqT RB /= //.
Qed. *)
(* Lemma syscall_head_step σ id : (* Lemma syscall_head_step σ id :
head_step (SysCall id) σ [SysCallEvt id] # σ []. head_step (SysCall id) σ [SysCallEvt id] # σ [].
Proof. Proof.
......
...@@ -705,3 +705,55 @@ Proof. ...@@ -705,3 +705,55 @@ Proof.
apply tag_on_top_grant_unique in GR as [stk1 Eq1]; [|done]. apply tag_on_top_grant_unique in GR as [stk1 Eq1]; [|done].
rewrite /tag_on_top Eq' Eq1 /=. by eexists. rewrite /tag_on_top Eq' Eq1 /=. by eexists.
Qed. Qed.
Lemma retag_nxtp_change α cids c nxtp l otag ntag rk pk T α' nxtp'
(TS: (O < tsize T)%nat)
(RK: match pk with | RawPtr _ => rk = RawRt | _ => True end) :
retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp')
nxtp' = S nxtp
match ntag with
| Untagged => True
| Tagged t => nxtp = t
end.
Proof.
assert ( n, tsize T = S n) as [n EqT].
{ destruct (tsize T); [lia|by eexists]. }
destruct pk as [[]| |]; [| |subst rk|]; rewrite /retag /= /retag_ref EqT;
(case reborrow as [α1|]; [|done]); simpl; intros; by simplify_eq.
Qed.
Lemma retag_change_case α cids c nxtp l otag ntag rk pk T α' nxtp' :
retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp')
tsize T = O α' = α nxtp' = nxtp ntag = otag
(O < tsize T)%nat
match pk, rk with
| RawPtr _, RawRt => True
| RawPtr _, _ => α' = α nxtp' = nxtp ntag = otag
| _, _ => True
end.
Proof.
destruct (tsize T) as [|n] eqn:EqT.
- rewrite /retag /retag_ref EqT /=.
destruct pk as [[]| |]; [| |destruct rk|]; simpl; intros; simplify_eq;
by left.
- rewrite /retag /retag_ref EqT /=.
destruct pk as [[]| |]; [| |destruct rk|]; simpl; intros; simplify_eq;
right; (split; [lia|done]).
Qed.
Lemma retag_change_nxtp α cids c nxtp l otag ntag rk pk T α' nxtp' :
retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp')
(nxtp nxtp')%nat.
Proof.
intros RT.
destruct (retag_change_case _ _ _ _ _ _ _ _ _ _ _ _ RT) as [[?[?[??]]]|[? Eq]].
- by simplify_eq.
- destruct pk.
+ apply retag_nxtp_change in RT as []; [lia|done..].
+ destruct rk.
* by destruct Eq as [_ [? _]]; subst.
* by destruct Eq as [_ [? _]]; subst.
* apply retag_nxtp_change in RT as []; [lia|done..].
* by destruct Eq as [_ [? _]]; subst.
+ apply retag_nxtp_change in RT as []; [lia|done..].
Qed.
...@@ -709,6 +709,29 @@ Proof. ...@@ -709,6 +709,29 @@ Proof.
+ intros ??. apply NC. lia. + intros ??. apply NC. lia.
Qed. Qed.
Lemma visit_freeze_sensitive_stacks_unchanged l (f: stacks _ _ _ _)
α α' T :
( α1 α2 l n b, f α1 l n b = Some α2
l', ( (i : nat), (i < n)%nat l' l + i) α2 !! l' = α1 !! l')
visit_freeze_sensitive l T f α = Some α'
l', ( (i : nat), (i < tsize T)%nat l' l + i) α' !! l' = α !! l'.
Proof.
intros HF.
rewrite /visit_freeze_sensitive.
case visit_freeze_sensitive' as [[α1 [l1 c1]]|] eqn:Eq; [|done].
intros Eqf.
have Eq' := Eq.
apply visit_freeze_sensitive'_offsets in Eq' as [_ Eq'].
rewrite 2!Nat.add_0_l in Eq'.
apply visit_freeze_sensitive'_stacks_unchanged in Eq as [_ EQ]; [|done].
specialize (HF _ _ _ _ _ Eqf).
intros l' NEq. rewrite HF; last first.
{ intros i Lt. rewrite shift_loc_assoc -Nat2Z.inj_add.
apply NEq. rewrite -Eq'. lia. }
rewrite EQ //.
intros i [_ Lti]. apply NEq. rewrite -Eq'. lia.
Qed.
Lemma visit_freeze_sensitive'_wf_stack l (f: stacks _ _ _ _) Lemma visit_freeze_sensitive'_wf_stack l (f: stacks _ _ _ _)
α α' last cur T l' c' nxtp nxtc (P: stacks loc nat Prop) : α α' last cur T l' c' nxtp nxtc (P: stacks loc nat Prop) :
let Hα α1 α2 l n := let Hα α1 α2 l n :=
......
...@@ -1260,23 +1260,44 @@ Proof. ...@@ -1260,23 +1260,44 @@ Proof.
(* inversion retag of tgt *) (* inversion retag of tgt *)
destruct (tstep_retag_inv _ _ _ _ _ _ _ _ STEPT) destruct (tstep_retag_inv _ _ _ _ _ _ _ _ STEPT)
as (l & otg & c & cids & ntg & α' & nxtp' & ? & Eqs & EqT & ? & ?). as (l & otg & c & cids & ntg & α' & nxtp' & ? & Eqs & EqRT & ? & ?).
subst ptr et'. subst ptr et'.
exists (#[ScPtr l ntg])%V, set σs' := (mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc)).
(mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc)), have STEPS: (Retag #[ScPtr l otg] pk T kind, σs) ~{fs}~> ((#[ScPtr l ntg])%E, σs').
r, n. subst σt'. { destruct SREL as (Eqsst & Eqnp & Eqcs & Eqnc & PUBP).
split; last split.
{ left. constructor.
destruct SREL as (Eqsst & Eqnp & Eqcs & Eqnc & PUBP).
eapply (head_step_fill_tstep _ []), retag_head_step'. eapply (head_step_fill_tstep _ []), retag_head_step'.
- rewrite Eqcs; eauto. - rewrite Eqcs; eauto.
- by rewrite Eqsst Eqnp Eqcs. } - by rewrite Eqsst Eqnp Eqcs. }
exists (#[ScPtr l ntg])%V, σs', r, n. subst σt'.
split; last split.
{ left. by constructor. }
{ (* unfolding rrel for place *) { (* unfolding rrel for place *)
simpl in RREL. simpl in RREL.
inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL. inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL.
destruct AREL as (_ & _ & AREL).
admit. } have Lenp: (σt.(snp) nxtp')%nat. by apply retag_change_nxtp in EqRT.
split; last split; last split; last split; last split.
- by apply (tstep_wf _ _ _ STEPS WFS).
- by apply (tstep_wf _ _ _ STEPT WFT).
- done. (* TODO *)
- intros t' k' h' Eqt'.
specialize (PINV _ _ _ Eqt') as [Ltp PINV].
split; [by simpl; lia|].
intros l1 ss st Eql1 PRE. specialize (PINV _ _ _ Eql1).
destruct k'.
+ specialize (PINV I) as (Eqst & Eqss & Eqstk).
do 2 (split; [done|]). move : Eqstk. simpl.
admit.
+ simpl. admit.
+ simpl. admit.
- intros c1 Tc Eqc. specialize (CINV _ _ Eqc) as [Ltc CINV].
split; [done|].
intros tc L InL. specify
admit.
- admit. }
left. left.
apply: sim_body_result. intros. eapply POST; eauto. apply: sim_body_result. intros. eapply POST; eauto.
......
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