Library mcertikos.multithread.lowrefins.E2PBThreadGenLemmaHASEVENT
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem3.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import I64Layer.
Require Import AlgebraicMem.
Require Import Decision.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import PHBThread.
Require Import AsmE2L.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import E2PBThreadComposeData.
Require Import LoadStoreSemPHB.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadINTELVIRT.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadReplayFunction.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadVMM.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjInterruptController.
Require Import ObjSerialDevice.
Require Import OracleInstances.
Require Import ObjVMMFun.
Require Import ObjVMMGetSet.
Require Import ObjVMMDef.
Require Import ObjCV.
Require Import ObjCPU.
Require Import ObjVMX.
Require Import ObjVMCS.
Require Import ObjProc.
Require Import ObjBigThread.
Require Import ObjContainer.
Require Import ObjMultiprocessor.
Require Import ObjThread.
Require Import BigLogThreadConfigFunction.
Require Import BigLogThreadConfigFunctionProp.
Require Import StencilImpl.
Require Import E2PBThreadGenDef.
Section E2PBTHREADGENLEMMAHASEVENT.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := SingleOracleImpl.s_oracle_prf.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_prop_prf : SingleOracleProp := SingleOracleImpl.s_oracle_prop_prf.
Context `{Hstencil : Stencil (stencil := stencil)}.
Local Instance s_config : SingleConfiguration mem := s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_link_prop_prf : SingleOracleLinkProp := SingleOracleImpl.s_oracle_link_prop_prf.
Local Instance s_link_config : SingleLinkConfiguration mem := s_link_config.
Context `{acc_def: !AccessorsDefined (mem := mem) (stencil := stencil) (stencil_ops := stencil_ops)
(memory_model_ops := memory_model_ops)
(phbthread (s_config := s_config) ⊕ L64)}.
Context `{e2pbthread_gen_prop: !E2PBThreadGenProp s_oracle_prf}.
Opaque PDX Zdivide_dec zle Z.mul Z.add Z.sub Z.div.
Opaque CalRealPT.real_pt CalRealProcModule.real_syncchpool.
Opaque compatlayer_ops.
Opaque update.
Opaque uRData.
Opaque proc_id.
Opaque full_thread_list.
Lemma big_ipc_send_body_related:
∀ kctxt_pool l dp a chid vaddr scount d d´ ds´ choice l´ res,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
single_big_ipc_send_body_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scount) ((uRData l), d)
= Some (ds´, d´, res) →
choice_check ipc_send_body (Lint chid :: Lint vaddr :: Lint scount :: nil) (uRData l) d = choice →
l´ = LEvent (proc_id (uRData l)) (LogPrim ipc_send_body (Lint chid :: Lint vaddr :: Lint scount :: nil)
choice (snap_func d)) :: l →
val2Lval_list (Vint chid :: Vint vaddr :: Vint scount :: nil) (Lint chid :: Lint vaddr :: Lint scount :: nil) →
∃ (a´ : RData) res´,
big_ipc_send_body_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scount) a = Some (a´, res´) ∧
relate_RData kctxt_pool (uRData l´) (ZMap.set (proc_id (uRData l)) (Some d´) dp) a´ ∧
kctxt a = kctxt a´ ∧ ds´ = uRData l´ ∧ res = res´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
assert (in_event: has_event ipc_send_body = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num ipc_send_body = 8) by (unfold prim_id_num; simpl; auto).
Opaque Z.add Z.sub Z.div Z.mul.
Opaque OracleInstances.SerialEnv.
Opaque cons_buf list_eq_dec Zlength serial_exists.
intros.
Transparent uRData proc_id update.
generalize H; intros Hrelated.
inv H; simpl in ×.
rewrite prim_num.
functional inversion H1. subst; simpl in ×.
unfold sh_adt, pv_adt, curid in *; simpl in ×.
unfold sh_adt.
unfold sh_adt in H12, H1.
clear sh_adt pv_adt curid.
unfold big_ipc_send_body_spec, single_big_ipc_send_body_spec.
generalize (per_data_re (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))).
intros.
rewrite H0 in H.
inv H.
simpl in ×.
rewrite zeq_true in ×.
rewrite H10 in ×.
rewrite <- pg_re, <- ikern_re, <- ihost_re, <- ipt_re.
rewrite H6, H7, H8, H9, H11.
rewrite <- cid_re.
unfold relate_SyncChanPool_per_pd in syncchpool_re.
rewrite H10, H5 in syncchpool_re; simpl in syncchpool_re; rewrite zeq_true in syncchpool_re.
rewrite <- syncchpool_re.
rewrite H12.
rewrite H5.
rewrite snap_rev_func_snap_func_eq_pd.
functional inversion H13; subst.
unfold sh_adt, pv_adt in ×.
unfold index, sh_adt, cpu in *; simpl in ×.
unfold sh_adt in l´.
clear sh_adt pv_adt index cpu.
simpl in *; subst.
unfold big_page_copy_spec.
rewrite <- ikern_re, <- ihost_re, <- ipt_re.
rewrite H6, H7, H8, H2, H16, H17, H18.
assert (Hpperm: ZMap.get (PageI (Int.unsigned vaddr)) (AbstractDataType.pperm a) = PGAlloc).
{ unfold pperm_inject in pperm_re.
generalize (pperm_re (PageI (Int.unsigned vaddr))).
rewrite H19.
intros.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; inv H.
reflexivity. }
rewrite Hpperm.
rewrite <- big_log_re, <- lock_re.
rewrite H20, H21.
assert (Hcopy: ∃ b´,
page_copy_aux (Z.to_nat (Z.min (Int.unsigned scount) 1024))
(Int.unsigned vaddr) (AbstractDataType.HP a) = Some b´ ∧ b = b´).
{ eauto using page_copy_aux_related. }
destruct Hcopy as (b´ & Hcopy & Hb).
substx.
rewrite Hcopy.
rewrite <- cid_re, <- CPU_ID_re.
rewrite H13.
rewrite H23.
refine_split´; eauto.
constructor; simpl; eauto.
- rewrite H10; auto.
- intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))).
+ intros; subst.
rewrite ZMap.gss.
simpl.
per_data_auto.
× rewrite <- sh_init_re; auto.
× rewrite H10; auto.
× rewrite zeq_true; auto.
× rewrite zeq_true; auto.
× unfold relate_AC_per_pd in ×.
simpl in ×.
rewrite H10 in ×.
unfold B_GetContainerUsed in *; simpl in ×.
unfold B_GetContainerUsed´ in AC_re; unfold B_GetContainerUsed in AC_re.
simpl in AC_re.
rewrite H20 in AC_re.
auto.
× rewrite zeq_true; auto.
× auto.
× rewrite H10.
rewrite zeq_true; auto.
× rewrite H10.
auto.
× rewrite zeq_true; auto.
× rewrite zeq_true; auto.
× rewrite zeq_true; auto.
× unfold relate_SyncChanPool_per_pd.
simpl in ×.
rewrite H10.
rewrite zeq_true.
auto.
rewrite zeq_true.
rewrite <- syncchpool_re.
reflexivity.
× unfold relate_uctxt_per_pd in ×.
simpl in ×.
rewrite H10 in ×.
unfold B_GetContainerUsed in *; simpl in ×.
unfold B_GetContainerUsed´ in uctxt_re; unfold B_GetContainerUsed in uctxt_re.
simpl in uctxt_re.
rewrite H20 in uctxt_re.
auto.
× auto.
× inv inv_re; constructor; simpl; auto.
+ intros.
rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
generalize (per_data_re i).
intros.
subdestruct; [ | constructor; simpl; auto].
inv H24; simpl in ×.
per_data_auto.
× unfold relate_AC_per_pd in ×.
simpl in ×.
rewrite H10 in ×.
unfold B_GetContainerUsed in *; simpl in ×.
unfold B_GetContainerUsed´ in AC_re0; unfold B_GetContainerUsed in AC_re0.
simpl in AC_re0.
rewrite H20 in AC_re0.
auto.
× auto.
× rewrite H10 in PT_re0; rewrite H10; auto.
× unfold relate_SyncChanPool_per_pd.
simpl in ×.
rewrite H10.
rewrite zeq_true.
auto.
rewrite zeq_false; try omega.
auto.
× unfold relate_uctxt_per_pd in ×.
simpl in ×.
rewrite H10 in ×.
unfold B_GetContainerUsed in *; simpl in ×.
unfold B_GetContainerUsed´ in uctxt_re0; unfold B_GetContainerUsed in uctxt_re0.
simpl in uctxt_re0.
rewrite H20 in uctxt_re0.
auto.
× auto.
× inv inv_re0; constructor; simpl; auto.
- inv sh_shared_inv_re; constructor; simpl; auto.
+ intros.
rewrite H10 in H; inv H.
+ intros.
rewrite zeq_true in H.
inv H.
+ intros.
generalize (container_used_inv _ H).
intros.
unfold B_GetContainerUsed´ in H24.
rewrite H20 in H24.
unfold B_GetContainerUsed in H24.
unfold B_GetContainerUsed.
simpl.
case_eq (zeq tid (CPU_ID (update init_shared_adt l) + 1)).
× intros.
subst.
rewrite zeq_true in H24.
rewrite <- H24.
reflexivity.
× intros.
rewrite zeq_false in H24; try omega.
case_eq (zle_le 0 tid 8).
{ intros; subst.
rewrite H26 in H24.
rewrite <- H24; reflexivity. }
{ intros.
rewrite H26 in H24.
auto. }
+ intros.
apply uctxt_used_inv.
unfold B_GetContainerUsed´.
rewrite H20.
unfold B_GetContainerUsed in H.
unfold B_GetContainerUsed.
simpl in H.
auto.
+ unfold valid_AT_log_type_B.
intros.
inv Hdef; subst.
unfold valid_AT_log_B.
unfold valid_AT_log_type_B in valid_AT_log_inv.
exploit valid_AT_log_inv; eauto.
intros.
unfold valid_AT_log_B in H.
destruct H.
∃ x.
simpl.
unfold B_CalAT_log_real in ×.
simpl.
rewrite H.
auto.
+ unfold valid_TCB_log_type_B.
intros.
inv Hdef; subst.
unfold valid_TCB_log_B.
unfold valid_TCB_log_type_B in valid_TCB_log_inv.
exploit valid_TCB_log_inv; eauto.
intros.
unfold valid_TCB_log_B in H.
destruct H.
∃ x.
simpl.
unfold B_CalTCB_log_real in ×.
unfold B_CalTCB_log in *; simpl in ×.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; inv H.
reflexivity.
+ intros.
inv H24.
unfold B_CalAT_log_real in H25.
simpl in H25.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct.
inv H25.
unfold B_CalAT_log_real in valid_B_Cal_AT_log_inv.
exploit valid_B_Cal_AT_log_inv; eauto.
rewrite <- big_log_re.
auto.
- generalize sh_mem_inv_re.
generalize H0.
clear.
intros.
inv sh_mem_inv_re.
constructor; simpl; auto.
intros.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))).
+ generalize (pperm_disjoint i j d pd´ H).
intros; subst.
rewrite ZMap.gss in H1.
rewrite ZMap.gso in H2; try auto.
inv H1.
simpl in ×.
eapply H4; eauto.
+ intros; subst.
rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))).
× generalize (pperm_disjoint i j pd d H).
intros; subst; simpl.
rewrite ZMap.gss in H2.
inv H2; simpl in ×.
eapply H5; eauto.
× intros.
generalize (pperm_disjoint i j pd pd´ H).
rewrite ZMap.gso in H2; eauto.
Qed.
Lemma big_palloc_related:
∀ kctxt_pool l dp a n d d´ ds´ choice optSync l´ res,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
single_big_palloc_spec (Int.unsigned n) (uRData l, d) = Some (ds´, d´, res) →
choice_check palloc (Lint n :: nil) (uRData l) d = choice →
sync_chpool_check palloc (Lint n :: nil) (uRData l) d = optSync →
l´ = LEvent (proc_id (uRData l)) (LogPrim palloc (Lint n :: nil) choice (snap_func d)) :: l →
val2Lval_list (Vint n :: nil) (Lint n :: nil) →
∃ (a´ : RData) res´,
big_palloc_spec (Int.unsigned n) a = Some (a´, res´) ∧
relate_RData kctxt_pool (uRData l´) (ZMap.set (proc_id (uRData l)) (Some d´) dp) a´ ∧
kctxt a = kctxt a´ ∧ ds´ = uRData l´ ∧ res = res´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
assert (in_event: has_event palloc = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num palloc = 1) by (unfold prim_id_num; simpl; auto).
intros.
assert (valid_procid: proc_id (uRData l) = main_thread ∨ TOTAL_CPU < proc_id (uRData l) < num_proc).
{ generalize (all_cid_in_full_thread_list l); intros.
generalize (valid_thread_list (proc_id (uRData l))); intros.
eapply H7 in H6.
tauto. }
generalize (per_data_re _ _ _ _ H (proc_id (uRData l))); intros Hper_data_rel.
Transparent uRData proc_id update.
simpl in Hper_data_rel, H0.
rewrite H0 in Hper_data_rel.
inv Hper_data_rel; simpl in *; rewrite zeq_true in ×.
assert (init (update init_shared_adt l) = true).
{ unfold single_big_palloc_spec in H1.
unfold single_big_palloc_spec_share in H1.
subdestruct; simpl in *; auto. }
rewrite H2 in ptp_re.
rewrite H2 in PT_re.
assert (HgetUsed´: B_GetContainerUsed´ (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))
(CPU_ID (update init_shared_adt l)) (big_log (update init_shared_adt l)) = true).
{ unfold B_GetContainerUsed´; unfold single_big_palloc_spec in H1; subdestruct; simpl; auto. }
assert (Hinit: init (update init_shared_adt l) = true).
{ unfold single_big_palloc_spec in H1; subdestruct; simpl; auto. }
assert (AC_cused: cused (ZMap.get (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l))) (AbstractDataType.AC a)) = true).
{ inv H.
inv sh_shared_inv_re.
generalize (container_used_inv (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros.
assert (In (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l))) full_thread_list).
{ generalize (all_cid_in_full_thread_list l).
intros.
simpl in H3; auto. }
apply H in H3.
rewrite HgetUsed´ in H3.
symmetry in H3; auto. }
assert (AC_re´ : AC d = ZMap.get (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l))) (AbstractDataType.AC a)).
{
unfold relate_AC_per_pd in AC_re.
rewrite HgetUsed´ in AC_re.
rewrite Hinit in AC_re.
destruct valid_procid as [ valid_proc | valid_proc].
× rewrite <- valid_proc in AC_re.
rewrite zeq_true in AC_re.
rewrite AC_re; auto.
× destruct (zeq (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l))) main_thread); auto.
rewrite zlt_lt_true in AC_re; auto. }
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
rewrite prim_num.
clear H2.
unfold single_big_palloc_spec in H1; unfold big_palloc_spec.
unfold single_big_palloc_spec_share in H1; subdestruct; subst; inv H1; simpl in *;
unfold single_big_palloc_spec_share;
unfold choice_check; simpl in *; rewrite prim_num;
unfold single_big_palloc_spec_test; simpl in *; try rewrite prim_num;
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- ipt_re; rewrite <- big_log_re; try (rewrite <- e in AC_re´; rewrite <- AC_re´);
(rewrite Hdestruct4); try (rewrite Hdestruct5); rewrite <- lock_re, <- big_oracle_re;
try (rewrite Hdestruct6, Hdestruct7, Hdestruct8; try (rewrite <- CPU_ID_re; rewrite Hdestruct10);
try (rewrite <- nps_re; rewrite Hdestruct11); try rewrite Hdestruct9);
try (rewrite Hdestruct0, Hdestruct1, Hdestruct2); try rewrite Hdestruct10, Hdestruct11;
try (rewrite AC_re´; rewrite e; rewrite AC_cused).
- destruct a1; try omega.
- rewrite zeq_true.
∃ ((((a {big_log : BigDef (TBEVENT (AbstractDataType.CPU_ID a)
(TBSHARED (BPALLOCE (ZMap.get (AbstractDataType.CPU_ID a)
(AbstractDataType.cid a)) res))
:: big_oracle (update init_shared_adt l)
(AbstractDataType.CPU_ID a) l0 ++ l0)})
{LAT : ZMap.set res (LATCValid nil) (LAT a)})
{pperm : ZMap.set res PGAlloc (AbstractDataType.pperm a)})
{AC : ZMap.set (ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))
{| cquota := cquota (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))
(AbstractDataType.AC a));
cusage := cusage (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))
(AbstractDataType.AC a)) + 1;
cparent := cparent (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))
(AbstractDataType.AC a));
cchildren := cchildren (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))
(AbstractDataType.AC a));
cused := true |} (AbstractDataType.AC a)}).
esplit; refine_split; eauto; try (simpl; rewrite CPU_ID_re; auto; fail).
inv H; constructor; simpl; auto.
+ rewrite Hdestruct5 in sh_cid_re.
rewrite <- sh_CPU_ID_re.
rewrite sh_cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
+ intros.
generalize (per_data_re i); intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss.
rewrite H0 in H.
inv H; simpl; rewrite zeq_true in ×.
{ per_data_auto.
- rewrite Hdestruct5 in sh_cid_re.
rewrite <- sh_CPU_ID_re.
rewrite sh_cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
- assert (ZMap.get res (AbstractDataType.pperm a) = PGUndef).
{ inv sh_shared_inv_re.
assert (Htemp: ZMap.get res (AbstractDataType.pperm a) = PGUndef ∨
ZMap.get res (AbstractDataType.pperm a) ≠ PGUndef).
{ destruct (ZMap.get res (AbstractDataType.pperm a)); eauto.
right.
intro contra.
inv contra.
right.
intro contra.
inv contra. }
destruct Htemp; eauto.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct (valid_AT_log_inv l0 Hdestruct8) as (at´ & H8).
eapply valid_B_Cal_AT_log_inv in H; eauto.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ H8 Hdestruct10 res) in H; auto.
destruct a1 as (? & a1´ & ?).
rewrite a1´ in H.
inv H. }
assert (ZMap.get res (pperm d) = PGUndef).
{ generalize (pperm_re res).
rewrite H.
intros.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; try inv H2.
reflexivity. }
inv inv_re0.
assert (∀ id, ZMap.get id (HP d) = ZMap.get id (FlatMem.free_page res (HP d))).
{ intros; eapply dirty_page_per_thread_inv; eauto. }
assert (∀ id, ZMap.get id (AbstractDataType.HP a)
= ZMap.get id (FlatMem.free_page res (AbstractDataType.HP a))).
{ inv sh_shared_inv_re.
intros.
eapply dirty_page_shared_inv; eauto. }
revert H4; revert H3.
intros Hd_init Ha_init v ofs TY Htemp1 Htemp2 Htemp3.
case_eq (zeq ((v × 4096 + ofs mod 4096) / 4096) res).
+ intros.
rewrite e0 in Htemp1.
rewrite <- e0 in Hd_init, Ha_init.
revert Hd_init Ha_init.
clear H3 e0 Htemp1.
revert Htemp2 Htemp3.
eapply abs_rel_palloc_mem_related_prop; eauto.
+ intros; subst.
rewrite ZMap.gso in Htemp1; eauto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in AC_re.
rewrite CPU_ID_re.
rewrite ZMap.gss; auto.
exploit (single_big_palloc_preserves_cused
(ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
((update init_shared_adt l), d)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
rewrite zeq_false; auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
rewrite Hdestruct9.
rewrite cid_re, CPU_ID_re in AC_re.
rewrite Hdestruct8 in AC_re.
unfold B_GetContainerUsed´ in AC_re; simpl in AC_re.
rewrite Hdestruct9 in AC_re.
destruct valid_procid as [ valid_proc | valid_proc].
+ rewrite <- valid_proc.
rewrite cid_re.
rewrite zeq_true; auto.
+ rewrite <- cid_re.
destruct (zeq (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l))) main_thread);
auto.
rewrite zlt_lt_true; auto.
- rewrite zeq_true; auto.
- unfold pperm_inject.
intros.
generalize (pperm_re0 i); intros.
case_eq (zeq i res); intros; subst;
[ rewrite ZMap.gss; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto; rewrite ZMap.gso; auto].
- rewrite Hdestruct5.
rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd in ×.
simpl; rewrite Hdestruct5.
rewrite zeq_true.
auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in uctxt_re.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
(ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
((update init_shared_adt l), d)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
rewrite zeq_false; auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
rewrite Hdestruct9.
rewrite cid_re, CPU_ID_re in uctxt_re.
rewrite Hdestruct8 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re; simpl in uctxt_re.
rewrite Hdestruct9 in uctxt_re.
auto.
- auto.
- constructor.
simpl.
inv inv_re0.
intros.
assert (∀ i : ZIndexed.t,
ZMap.get i (pperm d) = PGUndef →
∀ res,
ZMap.get res (HP d) =
ZMap.get res (FlatMem.free_page i (HP d))).
{ intros; auto. }
eapply single_dirty_ppage´_gso_alloc in H2.
instantiate (1:= res) in H2.
apply H2 in H.
apply H. }
× rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv H.
{ per_data_auto.
- rewrite <- sh_CPU_ID_re.
rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in AC_re0.
rewrite CPU_ID_re.
rewrite ZMap.gso; [ | rewrite <- CPU_ID_re; auto].
exploit (single_big_palloc_preserves_cused
i ((update init_shared_adt l), d)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
rewrite zeq_false; auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
auto.
unfold B_GetContainerUsed´ in AC_re0; simpl in AC_re0.
rewrite Hdestruct8 in AC_re0.
rewrite <- CPU_ID_re; auto.
- unfold pperm_inject.
intros.
generalize (pperm_re0 i0); intros.
case_eq (zeq i0 res); intros; subst.
{ assert (ZMap.get res (AbstractDataType.pperm a) = PGUndef).
{ inv sh_shared_inv_re.
assert (Htemp: ZMap.get res (AbstractDataType.pperm a) = PGUndef ∨
ZMap.get res (AbstractDataType.pperm a) ≠ PGUndef).
{ destruct (ZMap.get res (AbstractDataType.pperm a)); eauto.
right.
intro contra.
inv contra.
right.
intro contra.
inv contra. }
destruct Htemp; eauto.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct (valid_AT_log_inv l0 Hdestruct8) as (at´ & H8).
eapply valid_B_Cal_AT_log_inv in H3; eauto.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ H8 Hdestruct10 res) in H3; auto.
destruct a1 as (? & a1´ & ?).
rewrite a1´ in H3.
inv H3. }
rewrite ZMap.gss.
symmetry in big_log_re.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
intros.
subdestruct; eauto. }
{ rewrite ZMap.gso; auto. }
- auto.
- unfold relate_SyncChanPool_per_pd.
simpl.
rewrite Hdestruct5.
rewrite zeq_true; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in uctxt_re0.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
i ((update init_shared_adt l), d)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
rewrite zeq_false; auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
auto.
unfold B_GetContainerUsed´ in uctxt_re0; simpl in uctxt_re0.
rewrite Hdestruct8 in uctxt_re0.
rewrite <- CPU_ID_re; auto.
- auto.
- inv inv_re0; constructor; auto. }
{ constructor. }
+ inv sh_shared_inv_re.
constructor; simpl; auto.
× intros.
assert (∀ i : ZIndexed.t,
ZMap.get i (AbstractDataType.pperm a) = PGUndef →
∀ res,
ZMap.get res (AbstractDataType.HP a) =
ZMap.get res (FlatMem.free_page i (AbstractDataType.HP a))).
{ intros; auto. }
eapply single_dirty_ppage´_gso_alloc in H1.
instantiate (1:= res) in H1.
apply H1 in H.
apply H.
× intros.
rewrite Hdestruct5 in H; inv H.
× intros.
rewrite Hdestruct5 in H; inv H.
× rewrite zeq_true.
intros.
unfold B_inLock in syncchpool_inv.
rewrite Hdestruct8, Hdestruct3 in syncchpool_inv.
apply syncchpool_inv in H.
erewrite <- single_big_oracle_query_preserves_B_GetlastPush_aux; auto.
× intros.
apply container_used_inv in H.
exploit (single_big_palloc_preserves_cused
tid ((update init_shared_adt l), d)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
rewrite zeq_false; auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros.
rewrite <- H1.
clear H1.
case_eq (zeq tid (ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss; simpl.
rewrite <- CPU_ID_re.
rewrite Hdestruct9.
auto. }
{ rewrite ZMap.gso; auto.
unfold B_GetContainerUsed´ in H.
rewrite Hdestruct8 in H; auto. }
× intros.
apply uctxt_used_inv.
unfold B_GetContainerUsed´.
rewrite Hdestruct8.
exploit (single_big_palloc_preserves_cused
tid ((update init_shared_adt l), d)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
rewrite zeq_false; auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros.
rewrite H1.
auto.
× unfold valid_AT_log_type_B.
intros.
inv Hdef.
unfold valid_AT_log_B.
unfold B_CalAT_log_real.
simpl.
unfold B_CalAT_log_real in Hdestruct10; revert Hdestruct10.
intros.
rewrite Hdestruct10.
rewrite zeq_false; auto.
destruct a1 as (a1 & a1´ & a1´´).
rewrite a1´.
esplit; auto.
× unfold valid_TCB_log_type_B.
intros ? Hdef.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_TCB_oracle_B in Htemp2.
generalize (valid_TCB_log_inv _ Hdestruct8); intros Hvalid_log.
generalize (Htemp2 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros Hvalid_oracle_log.
unfold valid_TCB_log_B in ×.
revert Hvalid_oracle_log.
unfold B_CalTCB_log_real.
unfold B_CalTCB_log.
simpl.
clear.
intros Hvalid_oracle_log; destruct Hvalid_oracle_log.
subdestruct.
inv H.
esplit; auto.
× intros.
case_eq (zeq i res).
{ inv H1.
unfold B_CalAT_log_real in H2.
simpl in H2.
unfold B_CalAT_log_real in Hdestruct10.
rewrite <- CPU_ID_re in H2.
rewrite Hdestruct10 in H2.
rewrite zeq_false in H2; auto.
intros; subst.
rewrite ZMap.gss in H.
clear Hdestruct11.
case_eq (ZMap.get res a0).
{ intros.
rewrite H3 in H2.
destruct b; inv H2.
destruct t; inv H6.
rewrite ZMap.gss.
auto. }
{ intros.
rewrite H3 in H2; inv H2. } }
{ intros.
rewrite ZMap.gso in H; eauto.
inv H1.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 Hdestruct8); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H2.
unfold B_CalAT_log_real in Hvalid_AT_log, H4.
simpl in H4.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(AbstractDataType.CPU_ID a) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H1 in H4.
rewrite zeq_false in H4; auto.
subdestruct.
inv H4.
rewrite ZMap.gso; auto.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H1 i H); eauto.
rewrite H1 in H4.
inv H4. }
+ inv sh_mem_inv_re.
constructor; simpl; auto.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))).
{ intros; subst.
rewrite ZMap.gss in H1.
inv H1; subst; simpl.
simpl in H3.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))).
{ intros; subst; simpl.
rewrite ZMap.gss in H2.
inv H2; simpl.
elim H; reflexivity. }
{ intros; rewrite ZMap.gso in H2; auto.
case_eq (zeq j0 res); intros.
- subst.
rewrite ZMap.gss in H3.
assert (ZMap.get res (AbstractDataType.pperm a) = PGUndef).
{ inv sh_shared_inv_re.
assert (Htemp: ZMap.get res (AbstractDataType.pperm a) = PGUndef ∨
ZMap.get res (AbstractDataType.pperm a) ≠ PGUndef).
{ destruct (ZMap.get res (AbstractDataType.pperm a)); eauto.
right.
intro contra.
inv contra. }
destruct Htemp; eauto.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct (valid_AT_log_inv l0 Hdestruct8) as (at´ & H8).
eapply valid_B_Cal_AT_log_inv in H7; eauto.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ H8 Hdestruct10 res) in H7; eauto.
destruct a1 as (? & a1´ & ?).
rewrite a1´ in H7.
inv H7. }
intros.
generalize (per_data_re j).
rewrite H2.
intros.
inv H8.
generalize (pperm_re0 res).
intros.
rewrite H7 in H8.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; try (inv H8; fail).
reflexivity.
- rewrite ZMap.gso in H3; auto.
eapply pperm_disjoint in H2; eauto. } }
{ intros; subst; rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
- rewrite ZMap.gss in H2.
inv H2; simpl.
case_eq (zeq j0 res); intros; subst.
+ rewrite ZMap.gss.
assert (ZMap.get res (AbstractDataType.pperm a) = PGUndef).
{ inv sh_shared_inv_re.
assert (Htemp: ZMap.get res (AbstractDataType.pperm a) = PGUndef ∨
ZMap.get res (AbstractDataType.pperm a) ≠ PGUndef).
{ destruct (ZMap.get res (AbstractDataType.pperm a)); eauto.
right.
intro contra.
inv contra.
right.
intro contra.
inv contra. }
destruct Htemp; eauto.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct (valid_AT_log_inv l0 Hdestruct8) as (at´ & H8).
eapply valid_B_Cal_AT_log_inv in H7; eauto.
Check B_CalAT_log_keeps_allocated_pages.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ H8 Hdestruct10 res) in H7; eauto.
destruct a1 as (? & a1´ & ?).
rewrite a1´ in H7.
inv H7. }
intros.
generalize (per_data_re i).
rewrite H1.
intros.
inv H8.
generalize (pperm_re0 res).
intros.
rewrite H7 in H8.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; try (inv H8; fail).
elim H3; reflexivity.
+ rewrite ZMap.gso; auto.
eapply (pperm_disjoint i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l))))
in H3; eauto.
- rewrite ZMap.gso in H2; auto.
eapply (pperm_disjoint i j); eauto. }
- rewrite zeq_true.
esplit; esplit; refine_split; eauto; try (simpl; rewrite CPU_ID_re; auto; fail).
inv H; simpl; constructor; simpl; auto.
+ rewrite Hdestruct5 in sh_cid_re.
rewrite sh_cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
+ intros.
generalize (per_data_re i); intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss.
rewrite H0 in H.
inv H; simpl; rewrite zeq_true in ×.
{ per_data_auto.
- rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in AC_re.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
(ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite <- CPU_ID_re.
rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
rewrite Hdestruct9.
rewrite cid_re, CPU_ID_re in AC_re.
rewrite Hdestruct8 in AC_re.
unfold B_GetContainerUsed´ in AC_re; simpl in AC_re.
rewrite Hdestruct9 in AC_re.
auto.
- rewrite zeq_true; auto.
- auto.
- rewrite Hdestruct5.
rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd in ×.
simpl; rewrite Hdestruct5.
rewrite zeq_true.
auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in uctxt_re.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
(ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite <- CPU_ID_re.
rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
rewrite Hdestruct9.
rewrite cid_re, CPU_ID_re in uctxt_re.
rewrite Hdestruct8 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re; simpl in uctxt_re.
rewrite Hdestruct9 in uctxt_re.
auto.
- auto.
- inv inv_re0; constructor; auto. }
× rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv H.
{ per_data_auto.
- rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in AC_re0.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
i ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
auto.
unfold B_GetContainerUsed´ in AC_re0; simpl in AC_re0.
rewrite Hdestruct8 in AC_re0.
rewrite <- CPU_ID_re; auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd.
simpl.
rewrite Hdestruct5.
rewrite zeq_true; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in uctxt_re0.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
i ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
auto.
unfold B_GetContainerUsed´ in uctxt_re0; simpl in uctxt_re0.
rewrite Hdestruct8 in uctxt_re0.
rewrite <- CPU_ID_re; auto.
- auto.
- inv inv_re0; constructor; auto. }
{ constructor. }
+ inv sh_shared_inv_re.
constructor; simpl; auto.
intros.
× rewrite Hdestruct5 in H; inv H.
× rewrite zeq_true.
intros.
unfold B_inLock in syncchpool_inv.
rewrite Hdestruct8, Hdestruct3 in syncchpool_inv.
apply syncchpool_inv in H.
erewrite <- single_big_oracle_query_preserves_B_GetlastPush_aux; auto.
× intros.
apply container_used_inv in H.
exploit (single_big_palloc_preserves_cused
tid ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros.
rewrite <- H1.
clear H1.
auto.
unfold B_GetContainerUsed´ in H.
rewrite Hdestruct8 in H.
auto.
× intros.
apply uctxt_used_inv.
unfold B_GetContainerUsed´.
rewrite Hdestruct8.
exploit (single_big_palloc_preserves_cused
tid ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9, Hdestruct10, Hdestruct11.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
auto. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros.
rewrite H1.
auto.
× unfold valid_AT_log_type_B.
intros.
inv Hdef.
unfold valid_AT_log_B.
unfold B_CalAT_log_real.
simpl.
unfold B_CalAT_log_real in Hdestruct10; revert Hdestruct10.
intros.
rewrite Hdestruct10.
esplit; auto.
× unfold valid_TCB_log_type_B.
intros ? Hdef.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_TCB_oracle_B in Htemp2.
generalize (valid_TCB_log_inv _ Hdestruct8); intros Hvalid_log.
generalize (Htemp2 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros Hvalid_oracle_log.
unfold valid_TCB_log_B in ×.
revert Hvalid_oracle_log.
unfold B_CalTCB_log_real.
unfold B_CalTCB_log.
simpl.
clear.
intros Hvalid_oracle_log; destruct Hvalid_oracle_log.
subdestruct.
inv H.
esplit; auto.
× intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 Hdestruct8); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H1.
unfold B_CalAT_log_real in Hvalid_AT_log, H2.
simpl in H2.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H1 in H2.
inv H2.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H1 i H); eauto.
rewrite H1 in H2; inv H2.
+ inv sh_mem_inv_re.
constructor; simpl.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). } }
- rewrite zeq_false; [ | intro contra; inv contra].
esplit; esplit; refine_split; eauto.
rewrite <- CPU_ID_re; auto.
inv H; simpl; constructor; simpl; auto.
+ rewrite Hdestruct5 in sh_cid_re.
rewrite sh_cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
+ intros.
generalize (per_data_re i); intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss.
rewrite H0 in H.
inv H; simpl; rewrite zeq_true in ×.
{ per_data_auto.
- rewrite Hdestruct5 in sh_cid_re.
rewrite sh_cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in AC_re.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
(ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
rewrite Hdestruct9.
rewrite cid_re, CPU_ID_re in AC_re.
rewrite Hdestruct8 in AC_re.
unfold B_GetContainerUsed´ in AC_re; simpl in AC_re.
rewrite Hdestruct9 in AC_re.
auto.
- rewrite zeq_true; auto.
- auto.
- rewrite Hdestruct5.
rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd in ×.
simpl; rewrite Hdestruct5.
rewrite zeq_true.
auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in uctxt_re.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
(ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite <- CPU_ID_re.
rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
rewrite Hdestruct9.
rewrite cid_re, CPU_ID_re in uctxt_re.
rewrite Hdestruct8 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re; simpl in uctxt_re.
rewrite Hdestruct9 in uctxt_re.
auto.
- auto.
- inv inv_re0; constructor; auto. }
× rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv H.
{ per_data_auto.
- rewrite Hdestruct5 in cid_re.
rewrite cid_re.
rewrite big_oracle_re.
rewrite CPU_ID_re.
auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in AC_re0.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
i ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
auto.
unfold B_GetContainerUsed´ in AC_re0; simpl in AC_re0.
rewrite Hdestruct8 in AC_re0.
rewrite <- CPU_ID_re; auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd.
simpl.
rewrite Hdestruct5.
rewrite zeq_true; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct5.
rewrite Hdestruct5 in uctxt_re0.
rewrite CPU_ID_re.
exploit (single_big_palloc_preserves_cused
i ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros; simpl in H.
rewrite Hdestruct5 in cid_re.
rewrite <- CPU_ID_re.
rewrite cid_re.
rewrite CPU_ID_re.
rewrite cid_re in H.
rewrite CPU_ID_re in H.
rewrite <- H.
rewrite cid_re, CPU_ID_re in Hdestruct9.
auto.
unfold B_GetContainerUsed´ in uctxt_re0; simpl in uctxt_re0.
rewrite Hdestruct8 in uctxt_re0.
rewrite <- CPU_ID_re; auto.
- auto.
- inv inv_re0; constructor; auto. }
{ constructor. }
+ inv sh_shared_inv_re.
constructor; simpl; auto.
intros.
× rewrite Hdestruct5 in H; inv H.
× rewrite zeq_true.
intros.
unfold B_inLock in syncchpool_inv.
rewrite Hdestruct8, Hdestruct3 in syncchpool_inv.
apply syncchpool_inv in H.
erewrite <- single_big_oracle_query_preserves_B_GetlastPush_aux; auto.
× intros.
apply container_used_inv in H.
exploit (single_big_palloc_preserves_cused
tid ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros.
rewrite <- H1.
clear H1.
auto.
unfold B_GetContainerUsed´ in H.
rewrite Hdestruct8 in H.
auto.
× intros.
apply uctxt_used_inv; auto.
unfold B_GetContainerUsed´.
rewrite Hdestruct8.
exploit (single_big_palloc_preserves_cused
tid ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_palloc_spec; unfold single_big_palloc_spec_share; simpl.
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7,
Hdestruct8, Hdestruct9.
instantiate (3:= Int.unsigned n).
rewrite Hdestruct.
simpl.
rewrite Hdestruct3.
reflexivity. }
{ rewrite Hdestruct8.
auto. }
{ simpl; reflexivity. }
intros.
rewrite H1; auto.
× unfold valid_AT_log_type_B.
intros.
inv Hdef.
unfold valid_AT_log_B.
unfold B_CalAT_log_real.
simpl.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
generalize (valid_AT_log_inv _ Hdestruct8); intros Hvalid_log.
generalize (Htemp3 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros Hvalid_oracle_log.
unfold valid_AT_log_B in ×.
destruct Hvalid_oracle_log as (? & Hvalid_oracle_log).
unfold B_CalAT_log_real in Hvalid_oracle_log; simpl.
rewrite Hvalid_oracle_log; auto.
esplit; auto.
× unfold valid_TCB_log_type_B.
intros ? Hdef.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_TCB_oracle_B in Htemp2.
generalize (valid_TCB_log_inv _ Hdestruct8); intros Hvalid_log.
generalize (Htemp2 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros Hvalid_oracle_log.
unfold valid_TCB_log_B in ×.
revert Hvalid_oracle_log.
unfold B_CalTCB_log_real.
unfold B_CalTCB_log.
simpl.
clear.
intros Hvalid_oracle_log; destruct Hvalid_oracle_log.
subdestruct.
inv H.
esplit; auto.
× intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 Hdestruct8); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H1.
unfold B_CalAT_log_real in Hvalid_AT_log, H2.
simpl in H2.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H1 in H2.
inv H2.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H1 i H); eauto.
rewrite H1 in H2; inv H2.
+ inv sh_mem_inv_re.
constructor; simpl.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). } }
Opaque uRData proc_id update.
Qed.
Lemma acquire_lock_CHAN_related:
∀ kctxt_pool l dp a index d d´ ds´ choice optSync l´,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
single_big_acquire_lock_SC_spec (Int.unsigned index) (uRData l, d) = Some (ds´, d´) →
choice_check acquire_lock_CHAN (Lint index :: nil) (uRData l) d = choice →
sync_chpool_check acquire_lock_CHAN (Lint index :: nil) (uRData l) d = optSync →
l´ = LEvent (proc_id (uRData l)) (LogPrim acquire_lock_CHAN (Lint index :: nil) choice (snap_func d)) :: l →
val2Lval_list (Vint index :: nil) (Lint index :: nil) →
∃ a´ : RData,
big_acquire_lock_SC_spec (Int.unsigned index) a = Some a´ ∧
relate_RData kctxt_pool (uRData l´) (ZMap.set (proc_id (uRData l)) (Some d´) dp) a´ ∧
kctxt a = kctxt a´ ∧ ds´ = uRData l´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
assert (in_event: has_event acquire_lock_CHAN = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num acquire_lock_CHAN = 6) by (unfold prim_id_num; simpl; auto).
intros.
unfold single_big_acquire_lock_SC_spec in H1.
unfold single_big_acquire_lock_SC_spec_share in H1; subdestruct; subst.
- inv H1.
Transparent uRData proc_id update.
unfold choice_check.
unfold sync_chpool_check.
rewrite prim_num; subst.
unfold big_acquire_lock_SC_spec.
simpl in *; rewrite prim_num.
generalize (per_data_re _ _ _ _ H (proc_id (uRData l))); intros Hper_data_rel.
simpl in Hper_data_rel; rewrite H0 in Hper_data_rel.
unfold single_big_acquire_lock_SC_spec_share.
inv Hper_data_rel; rewrite zeq_true in *; rewritesb.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
simpl; rewrite zle_lt_true, Hdestruct2, Hdestruct3, Hdestruct7; auto.
rewrite CPU_ID_re.
rewrite Hdestruct2 in cid_re.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite Hdestruct6.
esplit; eauto.
refine_split; simpl; eauto.
+ constructor; simpl; auto.
× inv H; simpl; auto.
× inv H; simpl; auto.
× intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l))));
intros; subst.
{ rewrite ZMap.gss.
per_data_auto.
- rewrite Hdestruct2.
auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- auto.
unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in AC_re.
unfold B_GetContainerUsed´ in AC_re.
rewrite Hdestruct5 in AC_re.
exploit (single_big_acquire_lock_SC_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- rewrite zeq_true; auto.
- auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
rewrite Hdestruct2.
rewrite zeq_true.
rewrite zeq_true.
auto.
- auto.
unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re.
rewrite Hdestruct5 in uctxt_re.
exploit (single_big_acquire_lock_SC_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- auto.
- constructor; simpl; inv inv_re; auto. }
{ rewrite ZMap.gso; auto.
generalize (per_data_re _ _ _ _ H i); intros Hper_data_rel.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv Hper_data_rel.
per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in AC_re0.
unfold B_GetContainerUsed´ in AC_re0.
rewrite Hdestruct5 in AC_re0.
exploit (single_big_acquire_lock_SC_preserves_cused
i (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- auto.
- rewrite Hdestruct2.
rewrite Hdestruct2 in PT_re; auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
rewrite Hdestruct2.
rewrite zeq_true.
rewrite zeq_false; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in uctxt_re0.
unfold B_GetContainerUsed´ in uctxt_re0.
rewrite Hdestruct5 in uctxt_re0.
exploit (single_big_acquire_lock_SC_preserves_cused
i (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- auto.
- inv inv_re0; constructor; simpl; auto.
- constructor. }
× inv H.
inv sh_shared_inv_re.
constructor; simpl; auto.
{ intros.
rewrite Hdestruct2 in H; inv H. }
{ erewrite single_big_oracle_query_preserves_B_inLock_aux; eauto.
intros.
rewrite zeq_true in H.
inv H. }
{ intros.
apply container_used_inv in H.
unfold B_GetContainerUsed´ in H.
rewrite Hdestruct5 in H.
exploit (single_big_acquire_lock_SC_preserves_cused
tid (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros; rewrite H1 in H; auto. }
{ intros thread_id HUsed_Info.
apply uctxt_used_inv.
unfold B_GetContainerUsed´.
rewrite Hdestruct5.
exploit (single_big_acquire_lock_SC_preserves_cused
thread_id (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite H.
auto. }
{ unfold valid_AT_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
generalize (valid_AT_log_inv _ Hdestruct5); intros.
generalize (Htemp3 l0 (CPU_ID (update init_shared_adt l)) H); intros.
unfold valid_AT_log_B in ×.
destruct H1.
unfold B_CalAT_log_real in *; simpl.
rewrite H1; esplit; auto. }
{ unfold valid_TCB_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_TCB_oracle_B in Htemp2.
generalize (valid_TCB_log_inv _ Hdestruct5); intros.
generalize (Htemp2 l0 (CPU_ID (update init_shared_adt l)) H); intros.
unfold valid_TCB_log_B in ×.
revert H1.
unfold B_CalTCB_log_real.
unfold B_CalTCB_log.
simpl.
clear.
intros; destruct H1.
subdestruct.
esplit; auto. }
{ intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 Hdestruct5); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H1.
unfold B_CalAT_log_real in Hvalid_AT_log, H2.
simpl in H2.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H1 in H2.
inv H2.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H1 i H); eauto.
rewrite H1 in H2; inv H2.
rewrite <- sh_big_log_re; eauto. }
× inv H.
inv sh_mem_inv_re.
constructor.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
simpl in H3.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). } }
- inv H1.
unfold choice_check.
unfold sync_chpool_check.
rewrite prim_num; subst.
unfold big_acquire_lock_SC_spec.
simpl in *; rewrite prim_num.
generalize (per_data_re _ _ _ _ H (proc_id (uRData l))); intros Hper_data_rel.
simpl in Hper_data_rel; rewrite H0 in Hper_data_rel.
unfold single_big_acquire_lock_SC_spec_share.
inv Hper_data_rel; rewrite zeq_true in *; rewritesb.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
simpl; rewrite zle_lt_true, Hdestruct2, Hdestruct3, Hdestruct7; auto.
rewrite CPU_ID_re.
rewrite Hdestruct2 in ×.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite Hdestruct6.
esplit; eauto.
refine_split; simpl; eauto.
+ constructor; simpl; auto.
× inv H; simpl; auto.
× inv H; simpl; auto.
× inv H; simpl; auto.
× intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l))));
intros; subst.
{ rewrite ZMap.gss.
per_data_auto_simpl.
- rewrite Hdestruct2.
auto.
- rewrite Hdestruct2; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in AC_re.
unfold B_GetContainerUsed´ in AC_re.
rewrite Hdestruct5 in AC_re.
exploit (single_big_acquire_lock_SC_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- rewrite zeq_true; auto.
- auto.
- rewrite Hdestruct2; rewrite zeq_true; auto.
- rewrite Hdestruct2; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
rewrite Hdestruct2.
rewrite zeq_true.
rewrite zeq_true.
rewrite CPU_ID_re.
rewrite big_log_re in Hdestruct5.
rewrite CPU_ID_re in Hdestruct3.
inv H.
inv sh_shared_inv_re.
unfold B_inLock in syncchpool_inv.
rewrite big_log_re in syncchpool_inv.
rewrite Hdestruct5 in syncchpool_inv.
rewrite CPU_ID_re in syncchpool_inv.
rewrite Hdestruct3 in syncchpool_inv.
unfold B_GetlastPush in syncchpool_inv.
rewrite syncchpool_inv; reflexivity.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re.
rewrite Hdestruct5 in uctxt_re.
exploit (single_big_acquire_lock_SC_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- auto.
- auto.
- auto.
- inv inv_re; constructor; simpl; auto. }
{ rewrite ZMap.gso; auto.
generalize (per_data_re _ _ _ _ H i); intros Hper_data_rel.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv Hper_data_rel.
per_data_auto_simpl.
- unfold relate_AC_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in AC_re0.
unfold B_GetContainerUsed´ in AC_re0.
rewrite Hdestruct5 in AC_re0.
exploit (single_big_acquire_lock_SC_preserves_cused
i (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- auto.
- auto.
- rewrite Hdestruct2.
rewrite Hdestruct2 in PT_re0; auto.
- rewrite Hdestruct2.
rewrite Hdestruct2 in ptp_re0; auto.
- auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
rewrite Hdestruct2.
rewrite zeq_true.
rewrite zeq_false; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite Hdestruct2.
rewrite Hdestruct2 in uctxt_re0.
unfold B_GetContainerUsed´ in uctxt_re0.
rewrite Hdestruct5 in uctxt_re0.
exploit (single_big_acquire_lock_SC_preserves_cused
i (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros.
rewrite <- H2.
auto.
- auto.
- auto.
- auto.
- inv inv_re0; constructor; simpl; auto.
- constructor; auto. }
× inv H.
inv sh_shared_inv_re.
constructor; simpl; auto.
{ intros.
rewrite Hdestruct2 in H; inv H. }
{ erewrite single_big_oracle_query_preserves_B_inLock_aux; eauto.
intros.
rewrite zeq_true in H.
inv H. }
{ intros.
apply container_used_inv in H.
unfold B_GetContainerUsed´ in H.
rewrite Hdestruct5 in H.
exploit (single_big_acquire_lock_SC_preserves_cused
tid (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros; rewrite H1 in H; auto. }
{ intros.
apply uctxt_used_inv.
unfold B_GetContainerUsed´.
rewrite Hdestruct5.
exploit (single_big_acquire_lock_SC_preserves_cused
tid (Int.unsigned index) ((update init_shared_adt l), d)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_acquire_lock_SC_spec; unfold single_big_acquire_lock_SC_spec_share; simpl.
rewrite Hdestruct, Hdestruct0, zle_lt_true, Hdestruct5, Hdestruct4, Hdestruct6, Hdestruct7; auto.
rewrite Hdestruct2; simpl.
rewrite Hdestruct3.
reflexivity. }
{ exact Hdestruct5. }
{ simpl.
reflexivity. }
intros; rewrite H1; auto. }
{ unfold valid_AT_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
generalize (valid_AT_log_inv _ Hdestruct5); intros.
generalize (Htemp3 l0 (CPU_ID (update init_shared_adt l)) H); intros.
unfold valid_AT_log_B in ×.
destruct H1.
unfold B_CalAT_log_real in *; simpl.
rewrite H1; esplit; auto. }
{ unfold valid_TCB_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_TCB_oracle_B in Htemp2.
generalize (valid_TCB_log_inv _ Hdestruct5); intros.
generalize (Htemp2 l0 (CPU_ID (update init_shared_adt l)) H); intros.
unfold valid_TCB_log_B in ×.
revert H1.
unfold B_CalTCB_log_real.
unfold B_CalTCB_log.
simpl.
clear.
intros; destruct H1.
subdestruct.
esplit; auto. }
{ intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 Hdestruct5); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H1.
unfold B_CalAT_log_real in Hvalid_AT_log, H2.
simpl in H2.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H1 in H2.
inv H2.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H1 i H); eauto.
rewrite H1 in H2; inv H2.
rewrite <- sh_big_log_re; eauto. }
× inv H.
inv sh_mem_inv_re.
constructor.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
simpl in H3.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). } }
Opaque uRData proc_id update.
Qed.
Lemma release_lock_CHAN_related:
∀ kctxt_pool l dp a index d d´ ds´ choice optSync l´,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
single_big_release_lock_SC_spec (Int.unsigned index) (uRData l, d) = Some (ds´, d´) →
choice_check release_lock_CHAN (Lint index :: nil) (uRData l) d = choice →
sync_chpool_check release_lock_CHAN (Lint index :: nil) (uRData l) d = optSync →
l´ = LEvent (proc_id (uRData l)) (LogPrim release_lock_CHAN (Lint index :: nil) choice (snap_func d)) :: l →
val2Lval_list (Vint index :: nil) (Lint index :: nil) →
∃ a´ : RData,
big_release_lock_SC_spec (Int.unsigned index) a = Some a´ ∧
relate_RData kctxt_pool (uRData l´) (ZMap.set (proc_id (uRData l)) (Some d´) dp) a´ ∧
kctxt a = kctxt a´ ∧ d = d´ ∧ ds´ = uRData l´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
assert (in_event: has_event release_lock_CHAN = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num release_lock_CHAN = 7) by (unfold prim_id_num; simpl; auto).
intros.
functional inversion H1.
functional inversion H10.
Transparent uRData proc_id update.
unfold choice_check in H2.
unfold sync_chpool_check in H3; simpl in ×.
rewrite prim_num in H2; subst.
unfold big_release_lock_SC_spec.
simpl in *; rewrite prim_num.
generalize (per_data_re _ _ _ _ H (proc_id (uRData l))); intros Hper_data_rel.
simpl in Hper_data_rel; rewrite H0 in Hper_data_rel.
unfold single_big_release_lock_SC_chan_pool.
unfold single_big_release_lock_SC_spec_share.
inv Hper_data_rel; rewrite zeq_true in *; rewritesb.
simpl in ×.
rewrite H13, H9, H8, zle_lt_true; eauto.
rewrite H16.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
unfold relate_SyncChanPool_per_pd in syncchpool_re.
unfold cpu in H12.
rewrite H14, H12, zeq_true in syncchpool_re.
rewrite <- syncchpool_re.
rewrite CPU_ID_re.
rewrite H14 in cid_re.
rewrite <- cid_re.
rewrite <- CPU_ID_re.
rewrite H18; auto.
rewrite H14, <- H16, H12, zle_lt_true ; auto.
esplit; eauto.
refine_split; simpl; eauto.
- constructor; simpl; auto.
+ inv H; simpl; auto.
+ inv H; simpl; auto.
+ intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss; rewrite H0.
{ per_data_auto.
- rewrite H14.
auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H14.
rewrite H14 in AC_re.
unfold B_GetContainerUsed´ in AC_re.
rewrite H16 in AC_re.
exploit (single_big_release_lock_SC_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned index) ((update init_shared_adt l), d´)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_release_lock_SC_spec; unfold single_big_release_lock_SC_spec_share; simpl.
rewrite H13, H9, H8, H16, H14, zle_lt_true; eauto.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
rewrite <- H16; rewrite H12.
rewrite H18.
reflexivity. }
intros; simpl in H3.
rewrite <- H3.
auto.
rewrite H16.
auto.
- rewrite zeq_true; auto.
- auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
rewrite H14; auto.
rewrite zeq_true.
auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H14.
rewrite H14 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re.
rewrite H16 in uctxt_re.
exploit (single_big_release_lock_SC_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned index) ((update init_shared_adt l), d´)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_release_lock_SC_spec; unfold single_big_release_lock_SC_spec_share; simpl.
rewrite H13, H9, H8, H16, H14, zle_lt_true; eauto.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
rewrite <- H16; rewrite H12.
rewrite H18.
reflexivity. }
intros; simpl in H3.
rewrite <- H3.
auto.
rewrite H16.
auto.
- auto.
- inv inv_re; constructor; auto. }
× rewrite ZMap.gso; auto.
generalize (per_data_re _ _ _ _ H i); intros Hper_data_rel.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv Hper_data_rel.
{ per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H14.
rewrite H14 in AC_re0.
unfold B_GetContainerUsed´ in AC_re0.
rewrite H16 in AC_re0.
exploit (single_big_release_lock_SC_preserves_cused
i (Int.unsigned index) ((update init_shared_adt l), d´)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_release_lock_SC_spec; unfold single_big_release_lock_SC_spec_share; simpl.
rewrite H13, H9, H8, H16, H14, zle_lt_true; eauto.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
rewrite <- H16; rewrite H12.
rewrite H18.
reflexivity. }
intros; simpl in H3.
rewrite <- H3.
auto.
rewrite H16.
auto.
- auto.
- rewrite H14.
rewrite H14 in PT_re; auto.
- unfold relate_SyncChanPool_per_pd.
simpl in *; rewrite H14; auto.
rewrite zeq_true; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H14.
rewrite H14 in uctxt_re0.
unfold B_GetContainerUsed´ in uctxt_re0.
rewrite H16 in uctxt_re0.
exploit (single_big_release_lock_SC_preserves_cused
i (Int.unsigned index) ((update init_shared_adt l), d´)); simpl in ×.
{ inv H; inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_release_lock_SC_spec; unfold single_big_release_lock_SC_spec_share; simpl.
rewrite H13, H9, H8, H16, H14, zle_lt_true; eauto.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
rewrite <- H16; rewrite H12.
rewrite H18.
reflexivity. }
intros; simpl in H3.
rewrite <- H3.
auto.
rewrite H16.
auto.
- auto.
- inv inv_re0; constructor; simpl; auto. }
{ constructor. }
+ inv H.
inv sh_shared_inv_re.
constructor; simpl; auto.
× rewrite H14; intro contra; inv contra.
× rewrite zeq_true.
rewrite zeq_true.
intros.
auto.
× intros.
exploit (single_big_release_lock_SC_preserves_cused
tid (Int.unsigned index) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_release_lock_SC_spec; unfold single_big_release_lock_SC_spec_share; simpl.
rewrite H13, H9, H8, H16, H14, zle_lt_true; eauto.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
rewrite <- H16; rewrite H12.
rewrite H18.
reflexivity. }
intros; simpl in H2.
rewrite <- H2.
auto.
× intros.
apply uctxt_used_inv.
exploit (single_big_release_lock_SC_preserves_cused
tid (Int.unsigned index) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_release_lock_SC_spec; unfold single_big_release_lock_SC_spec_share; simpl.
rewrite H13, H9, H8, H16, H14, zle_lt_true; eauto.
fold abid; rewrite H17.
unfold l´0 in H18.
unfold cpu, e in H18.
rewrite <- H16; rewrite H12.
rewrite H18.
reflexivity. }
simpl.
intros.
rewrite H2.
auto.
× unfold valid_AT_log_type_B.
intros.
inv Hdef.
generalize (valid_AT_log_inv _ H16); intros.
unfold valid_AT_log_B in ×.
unfold B_CalAT_log_real in *; simpl.
destruct H; rewrite H; esplit; auto.
× unfold valid_TCB_log_type_B.
intros.
inv Hdef.
generalize (valid_TCB_log_inv _ H16); intros.
unfold valid_TCB_log_B in ×.
destruct H.
unfold B_CalTCB_log_real in *; simpl.
unfold B_CalTCB_log in *; simpl.
revert H; clear; intros.
subdestruct.
inv H; esplit; auto.
× intros.
generalize (valid_AT_log_inv l0 H16); intros Hvalid_AT_log.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H2.
unfold B_CalAT_log_real in Hvalid_AT_log, H3.
simpl in H3.
rewrite Hvalid_AT_log in H3.
inv H3.
auto.
rewrite <- sh_big_log_re; auto.
+ inv H.
inv sh_mem_inv_re.
constructor.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss in H2; rewrite ZMap.gso in H3; auto; simpl in ×.
inv H2.
eapply pperm_disjoint; eauto.
× rewrite ZMap.gso in H2; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H3.
inv H3.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H3; auto.
apply (pperm_disjoint i j pd pd´ H H2 H3 j0 H4). }
Opaque uRData proc_id update.
Qed.
Lemma thread_wakeup_related:
∀ kctxt_pool l dp a n d d´ ds´ choice optSync l´ res,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
single_big_thread_wakeup_spec (Int.unsigned n) (uRData l, d) = Some (ds´, d´, res) →
choice_check thread_wakeup (Lint n :: nil) (uRData l) d = choice →
sync_chpool_check thread_wakeup (Lint n :: nil) (uRData l) d = optSync →
l´ = LEvent (proc_id (uRData l)) (LogPrim thread_wakeup (Lint n :: nil) choice (snap_func d)) :: l →
val2Lval_list (Vint n :: nil) (Lint n :: nil) →
∃ (a´ : RData) res´,
big_thread_wakeup_spec (Int.unsigned n) a = Some (a´, res´) ∧
relate_RData kctxt_pool (uRData l´) (ZMap.set (proc_id (uRData l)) (Some d´) dp) a´ ∧
kctxt a = kctxt a´ ∧ ds´ = uRData l´ ∧ res = res´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
assert (in_event: has_event thread_wakeup = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num thread_wakeup = 4) by (unfold prim_id_num; simpl; auto).
intros.
unfold choice_check in H2.
unfold sync_chpool_check in H3; simpl in ×.
Transparent uRData proc_id update.
functional inversion H1.
rewrite prim_num in H2; subst.
generalize (per_data_re _ _ _ _ H (proc_id (uRData l))); intros Hper_data_rel.
simpl in Hper_data_rel; simpl in H0; rewrite H0 in Hper_data_rel.
simpl in ×.
rewrite prim_num.
unfold single_big_thread_wakeup_spec_share.
unfold big_thread_wakeup_spec.
functional inversion H12; inv Hper_data_rel; simpl in *; try (rewrite zeq_true in *; auto);
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- ipt_re, <- big_log_re, <- lock_re;
rewrite H9, H10, H11, H7, H4, H8, H6;
unfold n0 in H13; rewrite H13;
rewrite <- big_oracle_re; rewrite <- CPU_ID_re;
unfold me, e, l1 in l´; unfold to in l´; unfold me in l´; unfold l´ in H15; rewrite H15;
unfold me in H14; rewrite H8 in H14; rewrite H14;
rewrite H6 in cid_re;
rewrite CPU_ID_re;
rewrite <- cid_re;
rewrite <- CPU_ID_re;
rewrite H15.
- esplit; esplit; eauto.
refine_split; simpl; eauto.
+ inv H; simpl in *; constructor; simpl in *; auto.
intros.
generalize (per_data_re i); intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss.
rewrite H0 in H; inv H.
{
per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H6.
rewrite H6 in AC_re.
unfold B_GetContainerUsed´ in AC_re.
rewrite H8 in AC_re.
exploit (single_big_thread_wakeup_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
unfold relate_SyncChanPool_per_pd in syncchpool_re0; simpl in ×.
rewrite H8 in syncchpool_re0; simpl in ×.
rewrite H6.
rewrite zeq_true in syncchpool_re0; rewrite zeq_true; auto.
rewrite zeq_true.
rewrite H14 in syncchpool_re0.
simpl in syncchpool_re0; rewrite H6 in syncchpool_re0; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H6.
rewrite H6 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re.
rewrite H8 in uctxt_re.
exploit (single_big_thread_wakeup_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- inv inv_re0; constructor; auto. }
× rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv H.
{
per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H6.
rewrite H6 in AC_re0.
unfold B_GetContainerUsed´ in AC_re0.
rewrite H8 in AC_re0.
exploit (single_big_thread_wakeup_preserves_cused
i (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd.
simpl.
rewrite H6.
rewrite zeq_true; rewrite zeq_false; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H6.
rewrite H6 in uctxt_re0.
unfold B_GetContainerUsed´ in uctxt_re0.
rewrite H8 in uctxt_re0.
exploit (single_big_thread_wakeup_preserves_cused
i (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- inv inv_re0; constructor; auto. }
{ constructor. }
× inv sh_shared_inv_re.
constructor; simpl; auto.
{ rewrite H6; intro contra; inv contra. }
{ rewrite zeq_true; intro contra; inv contra. }
{ intros.
exploit (single_big_thread_wakeup_preserves_cused
tid (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
reflexivity. }
intros; simpl in H2.
rewrite <- H2.
apply container_used_inv in H; auto. }
{ intros.
apply uctxt_used_inv; eauto.
exploit (single_big_thread_wakeup_preserves_cused
tid (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
reflexivity. }
unfold B_GetContainerUsed´; simpl.
rewrite H8.
intros; simpl in H2.
rewrite H2.
auto. }
{ unfold valid_AT_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
generalize (valid_AT_log_inv _ H8); intros Hvalid_log.
generalize (Htemp3 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros HValid_oracle_log.
unfold valid_AT_log_B in ×.
destruct HValid_oracle_log as (? & HValid_oracle_log).
unfold B_CalAT_log_real in *; simpl.
rewrite HValid_oracle_log; esplit; auto. }
{ unfold valid_TCB_log_type_B.
intros; inv Hdef.
unfold valid_TCB_log_B.
revert H15.
clear.
intros.
simpl.
∃ TCBWAKE_F.
auto. }
{ intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 H8); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H2.
unfold B_CalAT_log_real in Hvalid_AT_log, H3.
simpl in H3.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H2 in H3.
inv H3.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H2 i H); eauto.
rewrite H2 in H3; inv H3.
rewrite <- sh_big_log_re; eauto. }
× inv sh_mem_inv_re.
constructor.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H2; rewrite ZMap.gso in H3; auto; simpl in ×.
inv H2.
simpl in H4.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H3.
inv H3.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H3; auto.
apply (pperm_disjoint i j pd pd´ H H2 H3 j0 H16). } }
- assert (AbstractDataType.big_log a = BigDef l0).
{ rewrite <- big_log_re; auto. }
assert (cused (ZMap.get tid (AbstractDataType.AC a)) =
B_GetContainerUsed tid (CPU_ID (update init_shared_adt l)) l0).
{ inv H; inv sh_shared_inv_re.
symmetry.
unfold B_GetContainerUsed´ in container_used_inv.
rewrite H8 in container_used_inv.
apply container_used_inv.
auto. }
rewrite H3; clear H3.
unfold me in H16; rewrite H16.
esplit; esplit; eauto.
refine_split; simpl; eauto.
+ case_eq (in_dec zeq tid full_thread_list); intros; subst; [ | elim n1; auto].
rename i into in_dec.
rename H3 into Htemp.
inv H; constructor; simpl in *; auto.
intros.
generalize (per_data_re i); intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss.
rewrite H0 in H.
inv H.
{ per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H6.
rewrite H6 in AC_re.
unfold B_GetContainerUsed´ in AC_re.
rewrite H8 in AC_re.
exploit (single_big_thread_wakeup_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
rewrite H16.
rewrite Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
unfold relate_SyncChanPool_per_pd in syncchpool_re0; simpl in ×.
rewrite H8 in syncchpool_re0; simpl in ×.
rewrite H6.
rewrite zeq_true in syncchpool_re0; rewrite zeq_true; auto.
rewrite zeq_true.
rewrite H14 in syncchpool_re0.
simpl in syncchpool_re0; rewrite H6 in syncchpool_re0; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H6.
rewrite H6 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re.
rewrite H8 in uctxt_re.
exploit (single_big_thread_wakeup_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
rewrite H16.
rewrite Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- inv inv_re; constructor; auto. }
× rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv H.
{ per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H6.
rewrite H6 in AC_re0.
unfold B_GetContainerUsed´ in AC_re0.
rewrite H8 in AC_re0.
exploit (single_big_thread_wakeup_preserves_cused
i (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
rewrite H16.
rewrite Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd.
simpl.
rewrite H6.
rewrite zeq_true; rewrite zeq_false; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H6.
rewrite H6 in uctxt_re0.
unfold B_GetContainerUsed´ in uctxt_re0.
rewrite H8 in uctxt_re0.
exploit (single_big_thread_wakeup_preserves_cused
i (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
rewrite H16.
rewrite Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- inv inv_re0; constructor; auto. }
{ constructor; auto. }
× inv sh_shared_inv_re.
constructor; simpl; auto.
{ rewrite H6; intro contra; inv contra. }
{ rewrite zeq_true; intro contra; inv contra. }
{ intros.
exploit (single_big_thread_wakeup_preserves_cused
tid0 (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
rewrite H16.
rewrite Htemp.
reflexivity. }
intros; simpl in H3.
rewrite <- H3.
apply container_used_inv in H; auto. }
{ intros.
apply uctxt_used_inv; eauto.
exploit (single_big_thread_wakeup_preserves_cused
tid0 (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl.
rewrite H14.
rewrite H16.
rewrite Htemp.
reflexivity. }
unfold B_GetContainerUsed´; simpl.
rewrite H8.
intros; simpl in H3. idtac.
rewrite H3.
auto. }
{ unfold valid_AT_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
generalize (valid_AT_log_inv _ H8); intros Hvalid_log.
generalize (Htemp3 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros HValid_oracle_log.
unfold valid_AT_log_B in ×.
destruct HValid_oracle_log as (? & HValid_oracle_log).
unfold B_CalAT_log_real in *; simpl.
rewrite HValid_oracle_log; esplit; auto. }
{ unfold valid_TCB_log_type_B.
intros; inv Hdef.
unfold valid_TCB_log_B.
revert H15.
clear.
intros.
simpl.
∃ (TCBWAKE_T tid).
auto. }
{ intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 H8); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H3.
unfold B_CalAT_log_real in Hvalid_AT_log, H18.
simpl in H18.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H3 in H18.
inv H18.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H3 i H); eauto.
rewrite H3 in H18; inv H18. }
× inv sh_mem_inv_re.
constructor.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H3; rewrite ZMap.gso in H18; auto; simpl in ×.
inv H3.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H3; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H18.
inv H18.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H18; auto.
apply (pperm_disjoint i j pd pd´ H H3 H18 j0 H19). } }
+ case_eq (in_dec zeq tid full_thread_list); intros; subst; [ | elim n1; auto].
simpl.
unfold l´; auto.
- unfold l´´ in H16; unfold me, e´, l´ in H16; rewrite H16, H17.
assert (AbstractDataType.big_log a = BigDef l0).
{ rewrite <- big_log_re; auto. }
assert (cused (ZMap.get tid (AbstractDataType.AC a)) =
B_GetContainerUsed tid (CPU_ID (update init_shared_adt l)) l0).
{ inv H; inv sh_shared_inv_re.
symmetry.
unfold B_GetContainerUsed´ in container_used_inv.
rewrite H8 in container_used_inv.
apply container_used_inv.
auto. }
rewrite H3; clear H3.
unfold me in H18; rewrite H18.
esplit; esplit; eauto.
refine_split; simpl; eauto.
+ case_eq (in_dec zeq tid full_thread_list); intros; subst; [ | elim n1; auto].
rename i into in_dec.
rename H3 into Htemp.
inv H; constructor; simpl in *; auto.
intros.
generalize (per_data_re i); intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))); intros; subst.
× rewrite ZMap.gss.
rewrite H0 in H.
inv H.
{ per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H6.
rewrite H6 in AC_re.
unfold B_GetContainerUsed´ in AC_re.
rewrite H8 in AC_re.
exploit (single_big_thread_wakeup_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl; rewrite H14, H16, H17, H18, Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd; simpl in ×.
unfold relate_SyncChanPool_per_pd in syncchpool_re0; simpl in ×.
rewrite H8 in syncchpool_re0; simpl in ×.
rewrite H6.
rewrite zeq_true in syncchpool_re0; rewrite zeq_true; auto.
rewrite zeq_true.
rewrite H14 in syncchpool_re0.
simpl in syncchpool_re0; rewrite H6 in syncchpool_re0; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H6.
rewrite H6 in uctxt_re.
unfold B_GetContainerUsed´ in uctxt_re.
rewrite H8 in uctxt_re.
exploit (single_big_thread_wakeup_preserves_cused
(ZMap.get (CPU_ID (update init_shared_adt l)) (cid (update init_shared_adt l)))
(Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl; rewrite H14, H16, H17, H18, Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- inv inv_re; constructor; auto. }
× rewrite ZMap.gso; auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
inv H.
{ per_data_auto.
- unfold relate_AC_per_pd in *; simpl.
rewrite H6.
rewrite H6 in AC_re0.
unfold B_GetContainerUsed´ in AC_re0.
rewrite H8 in AC_re0.
exploit (single_big_thread_wakeup_preserves_cused
i (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl; rewrite H14, H16, H17, H18, Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- auto.
- unfold relate_SyncChanPool_per_pd.
simpl.
rewrite H6.
rewrite zeq_true; rewrite zeq_false; auto.
- unfold relate_uctxt_per_pd in *; simpl.
rewrite H6.
rewrite H6 in uctxt_re0.
unfold B_GetContainerUsed´ in uctxt_re0.
rewrite H8 in uctxt_re0.
exploit (single_big_thread_wakeup_preserves_cused
i (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ inv sh_shared_inv_re; simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl; rewrite H14, H16, H17, H18, Htemp.
reflexivity. }
intros; simpl in H.
rewrite <- H.
rewrite H8.
auto.
- auto.
- inv inv_re0; constructor; auto. }
{ constructor; auto. }
× inv sh_shared_inv_re.
constructor; simpl; auto.
{ rewrite H6; intro contra; inv contra. }
{ rewrite zeq_true; intro contra; inv contra. }
{ intros.
exploit (single_big_thread_wakeup_preserves_cused
tid0 (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl; rewrite H14, H16, H17, H18, Htemp.
reflexivity. }
intros; simpl in H3.
rewrite <- H3.
apply container_used_inv in H; auto. }
{ intros.
apply uctxt_used_inv; eauto.
exploit (single_big_thread_wakeup_preserves_cused
tid0 (Int.unsigned n) ((update init_shared_adt l), d´)); simpl in ×.
{ simpl; auto. }
{ unfold single_big_thread_wakeup_spec; unfold single_big_thread_wakeup_spec_share; simpl.
rewrite H9, H10, H11, H7, H4, H8, H6, H13, H15.
simpl; rewrite H14, H16, H17, H18, Htemp.
reflexivity. }
unfold B_GetContainerUsed´; simpl.
rewrite H8.
intros; simpl in H3. idtac.
rewrite H3.
auto. }
{ unfold valid_AT_log_type_B.
intros.
inv Hdef.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
generalize (valid_AT_log_inv _ H8); intros Hvalid_log.
generalize (Htemp3 l0 (CPU_ID (update init_shared_adt l)) Hvalid_log); intros HValid_oracle_log.
unfold valid_AT_log_B in ×.
destruct HValid_oracle_log as (? & HValid_oracle_log).
unfold B_CalAT_log_real in *; simpl.
rewrite HValid_oracle_log; esplit; auto. }
{ unfold valid_TCB_log_type_B.
intros; inv Hdef.
unfold valid_TCB_log_B.
revert H16.
clear.
intros.
simpl.
∃ _x0.
auto. }
{ intros.
destruct big_oracle_inv as (Htemp1 & Htemp2 & Htemp3 & Htemp4).
unfold valid_AT_oracle_B in Htemp3.
unfold valid_AT_log_type_B in valid_AT_log_inv.
generalize (valid_AT_log_inv l0 H8); intros Hvalid_AT_log.
generalize (Htemp3 _ (CPU_ID (update init_shared_adt l)) Hvalid_AT_log);
intros Hvalid_AT_oracle_res.
unfold valid_AT_log_type_B in valid_AT_log_inv.
unfold valid_AT_log_B in valid_AT_log_inv.
destruct Hvalid_AT_log as (at0 & Hvalid_AT_log).
eapply (valid_B_Cal_AT_log_inv i l0 at0) in H; eauto.
inv H3.
unfold B_CalAT_log_real in Hvalid_AT_log, H20.
simpl in H20.
case_eq (B_CalAT_log (big_oracle (update init_shared_adt l)
(CPU_ID (update init_shared_adt l)) l0 ++ l0)
(real_AT (ZMap.init ATUndef))); intros.
rewrite H3 in H20.
inv H20.
eapply (B_CalAT_log_keeps_allocated_pages _ _ _ _ _ Hvalid_AT_log H3 i H); eauto.
rewrite H3 in H20; inv H20. }
× inv sh_mem_inv_re.
constructor.
intros.
case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H3; rewrite ZMap.gso in H20; auto; simpl in ×.
inv H3.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H3; auto.
case_eq (zeq j (ZMap.get (CPU_ID (update init_shared_adt l))
(cid (update init_shared_adt l)))); intros; subst.
{ rewrite ZMap.gss in H20.
inv H20.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H20; auto.
apply (pperm_disjoint i j pd pd´ H H3 H20 j0 H21). } }
+ case_eq (in_dec zeq tid full_thread_list); intros; subst; [ | elim n1; auto].
simpl.
unfold l´´.
unfold l´.
unfold me, e´.
auto.
Opaque uRData proc_id update.
Qed.
End E2PBTHREADGENLEMMAHASEVENT.