Commit f77ae9f0 authored by Hai Dang's avatar Hai Dang
Browse files

fix end_call_sat

parent 59e4404f
......@@ -106,14 +106,9 @@ Definition vrel_res (r: resUR) (e1 e2: result) :=
(** Condition for resource before EndCall *)
(* Any private location w.r.t to the current call id ownership must be related *)
Definition end_call_sat (r: resUR) (σs σt: state) : Prop :=
c, hd_error σt.(scs) = Some c is_Some (r.(rcm) !! c)
( r_f, (r_f r)
T, (r_f r).(rcm) !! c Some (Cinl (Excl T)) (t: ptr_id), t T
h, (r_f r).(rtm) !! t Some (to_tagKindR tkUnique, h)
l st, l dom (gset loc) h σt.(shp) !! l = Some st
ss, σs.(shp) !! l = Some ss arel (r_f r) ss st).
(* The call id [c] to be end must not have any privately protected locations. *)
Definition end_call_sat (r: resUR) (c: call_id) : Prop :=
r.(rcm) !! c Some (to_callStateR csPub).
Definition init_res : resUR := ((ε, {[O := to_callStateR csPub]}), ε).
Lemma wsat_init_state : wsat init_res init_state init_state.
......
......@@ -116,13 +116,12 @@ Qed.
- We start after the substitution.
- We assume the arguments are values related by [r]
- The returned result must also be values and related by [vrel]. *)
Definition fun_post (esat: A state state Prop) initial_call_id_stack
(r: A) (n: nat) rs σs rt σt :=
( c, σt.(scs) = c :: initial_call_id_stack)
esat r σs σt
Definition fun_post (esat: A call_id Prop) initial_call_id_stack
(r: A) (n: nat) rs (σs: state) rt σt :=
( c, σt.(scs) = c :: initial_call_id_stack esat r c)
( vs vt, rs = ValR vs rt = ValR vt vrel r vs vt).
Definition sim_local_fun
(esat: A state state Prop) (fn_src fn_tgt : function) : Prop :=
(esat: A call_id Prop) (fn_src fn_tgt : function) : Prop :=
r es et (vl_src vl_tgt: list value) σs σt
(VALEQ: Forall2 (vrel r) vl_src vl_tgt)
(EQS: subst_l fn_src.(fun_b) (Val <$> vl_src) fn_src.(fun_e) = Some es)
......@@ -131,7 +130,7 @@ Definition sim_local_fun
(InitCall es) σs (InitCall et) σt
(fun_post esat σt.(scs)).
Definition sim_local_funs (esat: A state state Prop) : Prop :=
Definition sim_local_funs (esat: A call_id Prop) : Prop :=
name fn_src, fns !! name = Some fn_src fn_tgt,
fnt !! name = Some fn_tgt
length fn_src.(fun_b) = length fn_tgt.(fun_b)
......
......@@ -53,8 +53,7 @@ Inductive sim_local_frames:
(fill frame.(K_src) (Val v_src)) σ_src'
(fill frame.(K_tgt) (Val v_tgt)) σ_tgt'
(λ r _ vs σs vt σt,
( c, σt.(scs) = c :: cids)
end_call_sat r σs σt
( c, σt.(scs) = c :: cids end_call_sat r c)
vrel_res r vs vt))
: sim_local_frames
(r_f frame.(rc))
......@@ -73,8 +72,7 @@ Inductive sim_local_conf:
(FRAMES: sim_local_frames r_f cids K_src K_tgt frames)
(LOCAL: sim_local_body wsat vrel fns fnt rc idx e_src σ_src e_tgt σ_tgt
(λ r _ vs σs vt σt,
( c, σt.(scs) = c :: cids)
end_call_sat r σs σt
( c, σt.(scs) = c :: cids end_call_sat r c)
vrel_res r vs vt))
(KE_SRC: Ke_src = fill K_src e_src)
(KE_TGT: Ke_tgt = fill K_tgt e_tgt)
......@@ -96,7 +94,7 @@ Proof.
destruct sim_local_body_stuck as [vt Eqvt].
rewrite -(of_to_result _ _ Eqvt).
destruct (sim_local_body_terminal _ Eqvt)
as (vs' & σs' & r' & idx' & SS' & WSAT' & CALLIDS & ESAT' & VREL).
as (vs' & σs' & r' & idx' & SS' & WSAT' & (c & CALLIDS & ESAT') & VREL).
have STEPK: (fill (Λ:=bor_ectxi_lang fns) K_src0 e_src0, σ_src)
~{fns}~>* (fill (Λ:=bor_ectxi_lang fns) K_src0 vs', σs').
{ apply fill_tstep_rtc. destruct SS' as [|[? Eq]].
......@@ -133,7 +131,7 @@ Proof.
(* Simulatin EndCall *)
rename σ_tgt into σt. rename σs' into σs.
destruct x4 as (vs1 & vt1 & Eqvs1 & Eqv1 & VR).
destruct x3 as (vs1 & vt1 & Eqvs1 & Eqv1 & VR).
simplify_eq.
set Φ : resUR nat result state result state Prop :=
......@@ -142,16 +140,11 @@ Proof.
σt.(scs) = c2 :: cids2
σs2 = mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc)
σt2 = mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc)
r2 = ((r'.(rtm),
match (r'.(rcm) !! c2) with
| Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r'.(rcm)
| _ => r'.(rcm)
end), r'.(rlm)).
r2 = r'.
have SIMEND : r' {idx',fns,fnt} (EndCall vs1, σs) (EndCall vt1, σt) : Φ.
{ apply sim_body_end_call; auto.
clear. intros. rewrite /Φ. split; last naive_solver.
eexists _, _. done.
}
{ apply sim_body_end_call; auto; [naive_solver|].
clear -VR. intros. rewrite /Φ. simpl. split; last naive_solver.
by eexists _, _. }
have NONE : to_result (EndCall e_tgt0) = None. by done.
destruct (fill_tstep_inv _ _ _ _ _ _ NONE H) as [et2 [? STEPT2]].
......
......@@ -36,16 +36,9 @@ Proof.
have ?: vrel_res (init_res r') (#vs) (#vt).
{ do 2 eexists. do 2 (split; [done|]).
eapply vrel_mono; [done|apply cmra_included_r|done]. }
split; last split; [..|done].
{ exists O. by rewrite -STACKT. }
rewrite /end_call_sat -STACKT.
intros c Eq. simpl in Eq. simplify_eq.
have HL: (init_res r').(rcm) !! 0%nat Some (to_callStateR csPub).
{ apply cmap_lookup_op_l_equiv_pub; [apply VALID|].
by rewrite /= lookup_singleton. }
split.
{ destruct ((init_res r').(rcm) !! 0%nat). by eexists. by inversion HL. }
intros r_f VALIDf T HL2. exfalso.
move : HL2. rewrite lookup_op HL. apply callStateR_exclusive_2.
split; [|done].
exists O. split; [by rewrite -STACKT|].
apply cmap_lookup_op_l_equiv_pub; [apply VALID|].
by rewrite /= lookup_singleton.
- instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.
Qed.
......@@ -997,17 +997,13 @@ Qed.
Lemma sim_body_end_call fs ft r n vs vt σs σt Φ :
(* return values are related *)
vrel r vs vt
(* and any private location w.r.t to the current call id ownership must be related *)
end_call_sat r σs σt
(* The top of the call stack has no privately protected locations left *)
( c cids, σt.(scs) = c :: cids end_call_sat r c)
( c1 c2 cids1 cids2, σs.(scs) = c1 :: cids1 σt.(scs) = c2 :: cids2
let σs' := mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc) in
let σt' := mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc) in
let r2' := match (r.(rcm) !! c2) with
| Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r.(rcm)
| _ => r.(rcm)
end in
Wf σt vrel ((r.(rtm), r2'), r.(rlm)) vs vt
Φ ((r.(rtm), r2'), r.(rlm)) n (ValR vs) σs' (ValR vt) σt' : Prop)
Wf σt
Φ r n (ValR vs) σs' (ValR vt) σt' : Prop)
r {n,fs,ft} (EndCall (Val vs), σs) (EndCall (Val vt), σt) : Φ.
Proof.
intros VREL ESAT POST. pfold. intros NT r_f WSAT.
......@@ -1020,78 +1016,36 @@ Proof.
as (vt' & Eqvt & ? & c & cids & Eqc & Eqs).
subst. simpl in Eqvt. symmetry in Eqvt. simplify_eq.
rewrite /end_call_sat Eqc in ESAT.
destruct (ESAT _ eq_refl) as [[cs Eqcs] ESAT']. clear ESAT.
destruct ESAT as [c' [cs [Eqcs ESAT]]]. symmetry in Eqcs. simplify_eq.
set σs' := (mkState σs.(shp) σs.(sst) cids σs.(snp) σs.(snc)).
have STEPS: (EndCall #vs, σs) ~{fs}~> ((#vs)%E, σs').
{ destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (? & ? & Eqcs' & ?).
eapply (head_step_fill_tstep _ []).
econstructor. by econstructor. econstructor. by rewrite Eqcs'. }
exists (Val vs), σs'.
set r2' := match (r.(rcm) !! c) with
| Some (Cinl (Excl T)) => <[c := to_callStateR csPub]> r.(rcm)
| _ => r.(rcm)
end.
exists ((r.(rtm), r2'), r.(rlm)), (S n).
exists (Val vs), σs', r, (S n).
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
split; last split.
{ left. by constructor 1. }
{ have VALID': (r_f ((r.(rtm), r2'), r.(rlm))).
{ apply (local_update_discrete_valid_frame _ _ _ VALID).
destruct (r.(rcm) !! c) as [[[T|]| |]|] eqn:Eqr2; rewrite /r2';
[|by destruct r_f as [[]], r as [[]]..].
destruct r_f as [[r_f1 r_f2] r_f3], r as [[r1 r2] r3]. rewrite 2!pair_op /=.
apply prod_local_update_1, prod_local_update_2.
rewrite (cmap_insert_op_r r_f2 r2 c T); [|apply VALID|exact Eqr2].
apply (insert_local_update _ _ _
(to_callStateR (csOwned T)) (to_callStateR (csOwned T)));
[|done|by apply exclusive_local_update].
apply cmap_lookup_op_r; [apply VALID|exact Eqr2]. }
destruct r_f as [[r_f1 r_f2] r_f3].
split; last split; last split; last split; last split; last split.
{ split; last split; last split; last split; last split; last split.
- by apply (tstep_wf _ _ _ STEPS WFS).
- by apply (tstep_wf _ _ _ STEPT WFT).
- done.
- rewrite pair_op. apply PINV.
- rewrite pair_op. intros c1 cs1. simpl.
case (decide (c1 = c)) => [->|NEqc]; last first.
+ rewrite (_: (r_f2 r2') !! c1 = (r_f2 r.(rcm)) !! c1); last first.
{ rewrite /r2'. destruct (r.(rcm) !! c) as [[[T|]| |]|]; [|done..].
by rewrite 2!lookup_op lookup_insert_ne. }
intros Eqcs1. move : (CINV _ _ Eqcs1). clear -NEqc Eqc.
destruct cs1 as [[T|]| |]; [|done..]. rewrite Eqc.
move => [/elem_of_cons IN ?]. split; [|done].
destruct IN; [by subst|done].
+ intros Eqcs1.
have VALID1: cs1. { rewrite -Some_valid -Eqcs1. apply VALID'. }
- done.
- intros c1 cs1 Eqcs1. simpl.
case (decide (c1 = c)) => [?|NEqc].
+ subst c1.
have VALID1: cs1. { rewrite -Some_valid -Eqcs1. apply VALID. }
destruct cs1 as [[T|]| |]; [|done| |done]; last first.
{ apply (state_wf_cid_agree _ WFT). rewrite Eqc. by left. }
(* TODO: move out *)
exfalso. move : Eqcs1. rewrite /r2' lookup_op.
destruct (r.(rcm) !! c) as [[[T'|]| |]|] eqn:Eqc2;
[rewrite lookup_insert|rewrite Eqc2..|done]; clear;
(destruct (r_f2 !! c) as [cs|] eqn:Eqrf2; rewrite Eqrf2 ;
[rewrite -Some_op /=; intros Eq%Some_equiv_inj
|rewrite left_id /=; intros Eq%Some_equiv_inj;
by inversion Eq; simplify_eq]);
destruct cs as [[]| |]; by inversion Eq; simplify_eq.
exfalso. move : Eqcs1. rewrite lookup_op ESAT. apply callStateR_exclusive_2.
+ move : (CINV _ _ Eqcs1). clear -NEqc Eqc.
destruct cs1 as [[T|]| |]; [|done..]. rewrite Eqc.
move => [/elem_of_cons IN ?]. split; [|done].
destruct IN; [by subst|done].
- destruct SREL as (Eqst & Eqnp & Eqcs' & Eqnc & Eqhp).
do 4 (split; [done|]). rewrite /= /r2'.
destruct (r.(rcm) !! c) as [[[T|]| |]|] eqn:Eqc2; [|apply Eqhp..].
intros l InD SHR.
specialize (Eqhp _ InD SHR) as [PUB|[t PV]]; [by left|].
destruct PV as (c' & T' & h & Eqc' & InT' & Eqt & Inh). simpl in *.
case (decide (c' = c)) => ?; last first.
{ right. exists t, c', T', h. repeat split; [|done..].
by rewrite /= lookup_op lookup_insert_ne // -lookup_op. }
subst c'.
have Eq2 := cmap_lookup_op_r r_f2 r.(rcm) _ _ (proj2 (proj1 VALID)) Eqc2.
rewrite Eq2 in Eqc'.
apply Some_equiv_inj, Cinl_inj, Excl_inj, leibniz_equiv_iff in Eqc'.
subst T'. specialize (ESAT' ((r_f1, r_f2), r_f3) VALID T).
rewrite /= Eq2 in ESAT'.
left. intros st Eqs.
destruct (ESAT' (ltac:(done)) _ InT' _ Eqt _ _ Inh Eqs) as [ss [Eqss AR]].
by exists ss.
do 4 (split; [done|]). simpl.
intros l InD SHR. by specialize (Eqhp _ InD SHR).
- intros ??. rewrite /=. by apply LINV. }
(* result *)
left. apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
......
......@@ -9,9 +9,9 @@ want to clean some stuff from your context.
From stbor.sim Require Import body instance refl_step.
Definition fun_post_simple initial_call_id_stack (r: resUR) (n: nat) vs css vt cst :=
( c, cst = c::initial_call_id_stack)
end_call_sat r (mkState css 0 0) (mkState cst 0 0)
Definition fun_post_simple
initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
( c, cst = c::initial_call_id_stack end_call_sat r c)
vrel_res r vs vt.
Definition sim_simple fs ft r n es css et cst
......@@ -59,12 +59,8 @@ Proof.
destruct vls as [|vs []]; [done| |done].
destruct vlt as [|vt []]; [done| |done].
inversion FREL. intros _ _. simplify_eq.
eapply sim_simplify; last by eapply HH.
intros ?????? (Hhead & Hend & Hrel). split; first done.
split; last done.
(* Currently [end_call_sat] still looks at the state, but we should be able to fix that. *)
admit.
Admitted.
eapply sim_simplify; last by eapply HH. done.
Qed.
Lemma sim_simple_bind fs ft
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
......
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