Library mcertikos.objects.tmobj.ObjTMSCHED
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalTicketLock.
Require Import DeviceStateDataType.
Require Export ObjInterruptDriver.
Require Import BigStepLogReplay.
Require Import CommonTactic.
Require Import ObjLMM0.
Require Import ObjLMM1.
Require Import ObjVMM.
Require Import ObjCPU.
Require Import ObjCV.
Require Import ObjContainer.
Require Import ObjBigThread.
Require Import ObjInterruptController.
Require Import ObjInterruptManagement.
Require Import ObjSerialDriver.
Require Import ObjConsole.
Require Import ObjVMCS.
Require Import ObjEPT.
Require Import ObjVMX.
Require Import liblayers.compat.CompatGenSem.
Require Import Z64Lemma.
Require Import SingleOracle.
Require Import BigLogThreadConfigFunction.
Opaque full_thread_list.
Section OBJ_SECOND_Thread_SCHED.
Context `{real_params: RealParams}.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops : BigOracleOps}.
Context `{thread_conf_ops: ThreadsConfigurationOps}.
Function thread_get_CPU_ID_spec (adt: RData): option Z :=
if (init adt) then get_CPU_ID_spec adt else None.
Function thread_get_curid_spec (adt: RData): option Z :=
if (init adt) then get_curid_spec adt else None.
Definition big2_proc_create_spec (adt: RData) (b b´ buc: block) (ofs_uc: int) q : option (RData × Z) :=
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let c := ZMap.get curid (AC adt) in
let i := curid × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, zlt_lt 0 i num_proc,
zlt (Z_of_nat (length (cchildren c))) max_children,
zle_le 0 q (cquota c - cusage c),
B_inLock cpu (big_log adt)) with
| (true, true, true, true, true, left _, left _, left _, false) ⇒
let parent := (mkContainer (cquota c) (cusage c + q)
(cparent c) (i :: cchildren c) (cused c)) in
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
match B_GetContainerUsed i cpu l, (In_dec zeq) i full_thread_list with
| false, left _ ⇒
let ofs := Int.repr ((i + 1) × PgSize -4) in
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSPAWN curid i q ofs
buc ofs_uc ) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some _ ⇒
Some (adt {big_log: BigDef l´}
{AC: ZMap.set curid parent (AC adt)}, i)
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end.
Function big2_thread_wakeup_spec (cv: Z) (adt: RData) :=
let me := CPU_ID adt in
match (init adt, ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true, true) ⇒
let n := slp_q_id cv 0 in
let sc_id := n + lock_TCB_range in
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get (n + ID_AT_range) (lock adt), B_inLock me (big_log adt) with
| BigDef l, LockFalse, true ⇒
let to := big_oracle adt in
let l1 := (to me l) ++ l in
let e := TBSHARED (BTDWAKE (ZMap.get (CPU_ID adt) (cid adt)) cv) in
let l´ := (TBEVENT me e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCBWAKE_F) ⇒
Some (adt {big_log: BigDef l´}, 0)
| Some (TCBWAKE_T tid) ⇒
match B_GetContainerUsed tid me l, (In_dec zeq) tid full_thread_list with
| true, left _ ⇒
Some (adt {big_log: BigDef l´}, 1)
| _, _ ⇒ None
end
| Some (TCBWAKE tid cpu´) ⇒
let e´ := TBSHARED (BTDWAKE_DIFF (ZMap.get (CPU_ID adt) (cid adt)) cv tid cpu´) in
let l´´ := (TBEVENT me e´) :: l´ in
match B_CalTCB_log_real l´´,
ZMap.get (msg_q_id cpu´ + ID_AT_range) (lock adt),
B_GetContainerUsed tid me l, (In_dec zeq) tid full_thread_list with
| Some _, LockFalse, true, left _ ⇒
Some (adt {big_log: BigDef l´´}, 1)
| _,_,_,_ ⇒ None
end
| _ ⇒ None
end
| _, _, _ ⇒ None
end
else None
| _ ⇒ None
end.
Function big2_sched_init_spec (mbi_adr:Z) (adt: RData) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq curid main_thread then
if zle_lt 0 (CPU_ID adt) TOTAL_CPU then
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, intr_flag adt, in_intr adt) with
| (false, false, true, true, true, true, false) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
{lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
} {ioapic / s / CurrentIrq: None}
{vmxinfo: real_vmxinfo} {pg: true} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{big_log: BigDef nil}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde adt)}
{syncchpool: real_syncchpool (syncchpool adt)}
{cid: real_cidpool (cid adt)}
else None
else None
| _ ⇒ None
end
else None
else None.
Definition option_z_check (tid : option Z) : bool :=
match tid with
| Some tid´ ⇒ (In_dec zeq) tid´ full_thread_list
| _ ⇒ false
end.
Definition z_check (tid : Z) : bool :=
(In_dec zeq) tid full_thread_list.
Function big2_thread_yield_spec (adt: RData) : option RData :=
let cpu := CPU_ID adt in
let curid := (ZMap.get (CPU_ID adt) (cid adt)) in
if zeq curid current_thread then
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, PT adt,
intr_flag adt, in_intr adt, snd (ti adt), B_inLock cpu (big_log adt)) with
| (true, true, true, true, true, 0, true, false, Vint ti_val, false) ⇒
if Int.eq ti_val Int.zero then
if Int.eq Int.zero (fst (ti adt)) then
match big_log adt, ZMap.get (msg_q_id cpu + ID_AT_range) (lock adt) with
| BigDef l, LockFalse ⇒
if B_GetContainerUsed curid cpu l then
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDYIELD curid) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if B_GetContainerUsed_opt t cpu l then
if option_z_check t then
if z_check la then
let l´´ := big_oracle_env_fun limit cpu curid to l´ in
match B_CalTCB_log_real l´´ with
| Some (TCB_YIELD la´ t´) ⇒
if zeq la´ curid then Some (adt {big_log: BigDef l´´}) else None
| Some (TCB_RID la´) ⇒
if zeq la´ curid then Some (adt {big_log: BigDef l´´}) else None
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end
else None
| _, _ ⇒ None
end
else None
else None
| _ ⇒ None
end
else None.
Function big2_thread_sleep_spec (cv: Z) (adt: RData): option RData :=
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
if zeq curid current_thread then
match (init adt, pg adt, ikern adt, ihost adt, ipt adt,
PT adt, intr_flag adt, in_intr adt, snd (ti adt), B_inLock cpu (big_log adt)) with
| (true, true, true, true, true, 0, true, false, Vint ti_val, true) ⇒
if Int.eq ti_val Int.zero then
if Int.eq Int.zero (fst (ti adt)) then
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get abid (lock adt), ZMap.get sc_id (lock adt)with
| BigDef l, LockFalse, LockOwn true ⇒
if B_GetContainerUsed curid cpu l then
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSLEEP curid cv (syncchpool adt)) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´, B_CalLock sc_id l, B_CalLock sc_id l1 with
| Some (TCB_RID la), Some (S (S _), LHOLD, Some cpu´), Some _ ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if zeq cpu cpu´ then
if z_check la then
let l´´ := big_oracle_env_fun limit cpu curid to l´ in
match B_CalTCB_log_real l´´ with
| Some (TCB_YIELD la´ t´) ⇒
if zeq la´ curid then Some (adt {big_log: BigDef l´´}
{lock: ZMap.set sc_id LockFalse
(ZMap.set abid LockFalse (lock adt))})
else None
| Some (TCB_RID la´) ⇒
if zeq la´ curid then Some (adt {big_log: BigDef l´´}
{lock: ZMap.set sc_id LockFalse
(ZMap.set abid LockFalse (lock adt))})
else None
| _ ⇒ None
end
else None
else None
else None
else None
| _,_,_ ⇒ None
end
else None
| _,_,_ ⇒ None
end
else None
else None
else None
else None
| _ ⇒ None
end
else None.
Function thread_proc_create_postinit_spec (elf_id: Z) (adt: RData) :=
if init adt then proc_create_postinit_spec elf_id adt else None.
End OBJ_SECOND_Thread_SCHED.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.
Require Import INVLemmaThread.
Local Open Scope Z_scope.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Local Open Scope Z_scope.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops: BigOracleOps}.
Context `{thread_conf_ops: ThreadsConfigurationOps}.
Section THREAD_GET_CPU_ID_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_CPU_ID}.
Context {re3: relate_impl_init}.
Lemma thread_get_CPU_ID_exist:
∀ s habd labd z f,
thread_get_CPU_ID_spec habd = Some z
→ relate_AbData s f habd labd
→ thread_get_CPU_ID_spec labd = Some z.
Proof.
unfold thread_get_CPU_ID_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
subdestruct.
rewrite <- H1; simpl.
eapply get_CPU_ID_exist; eauto.
Qed.
Lemma thread_get_CPU_ID_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_get_CPU_ID_spec)
(id ↦ gensem thread_get_CPU_ID_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite thread_get_CPU_ID_exist; eauto. reflexivity.
Qed.
End THREAD_GET_CPU_ID_SIM_PROOF.
Section THREAD_GET_CURID_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_init}.
Lemma thread_get_curid_exist:
∀ s habd labd z f,
thread_get_curid_spec habd = Some z
→ relate_AbData s f habd labd
→ thread_get_curid_spec labd = Some z.
Proof.
unfold thread_get_curid_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
subdestruct.
rewrite <- H1; simpl.
eapply get_curid_exist; eauto.
Qed.
Lemma thread_get_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_get_curid_spec)
(id ↦ gensem thread_get_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite thread_get_curid_exist; eauto. reflexivity.
Qed.
End THREAD_GET_CURID_SIM_PROOF.
Section BIG2_PROC_CREATE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_big_log}.
Context {re4: relate_impl_AC}.
Context {re5: relate_impl_cid}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_big_oracle}.
Lemma big2_proc_create_exist:
∀ (s : stencil) habd habd´ (labd : RData) b b´ buc ofs´ q n f,
big2_proc_create_spec habd b buc b´ ofs´ q = Some (habd´, n)
→ relate_AbData s f habd labd
→ find_symbol s STACK_LOC = Some b
→ find_symbol s START_USER_FUN_LOC = Some buc
→ (∃ id, find_symbol s id = Some b´)
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, big2_proc_create_spec labd b buc b´ ofs´ q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_proc_create_spec. intros until f; intros HP HR Hsys Hsys´ Hsys´´ Hincr.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
revert HP. subrewrite.
subdestruct; inv HQ.
refine_split´; trivial.
rewrite <- H1 in ×.
rewrite <- H6 in ×.
rewrite Hdestruct12.
reflexivity.
rewrite <- H1 in ×.
apply relate_impl_AC_update.
apply relate_impl_big_log_update.
trivial.
Qed.
Context {mt1: match_impl_big_log}.
Context {mt2: match_impl_AC}.
Lemma big2_proc_create_match:
∀ s d d´ m b buc b´ ofs q n f,
big2_proc_create_spec d b buc b´ ofs q = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_proc_create_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_AC_update.
eapply match_impl_big_log_update.
assumption.
Qed.
Context {inv: PCreateInvariants (data_ops:= data_ops) big2_proc_create_spec}.
Context {inv0: PCreateInvariants (data_ops:= data_ops0) big2_proc_create_spec}.
Lemma big2_proc_create_sim :
∀ id,
sim (crel RData RData) (id ↦ proc_create_compatsem big2_proc_create_spec)
(id ↦ proc_create_compatsem big2_proc_create_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit big2_proc_create_exist; eauto 1; intros (labd´ & HP & HM).
destruct H9 as [fun_id Hsys].
exploit stencil_find_symbol_inject´; eauto. intros HFB.
match_external_states_simpl.
eapply big2_proc_create_match; eauto.
Qed.
End BIG2_PROC_CREATE_SIM_PROOF.
Section BIG2_THREAD_WAKEUP_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_big_log}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_lock}.
Context {re8: relate_impl_AC}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_cid}.
Lemma big2_thread_wakeup_exist:
∀ s f habd habd´ labd cv a,
big2_thread_wakeup_spec cv habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_thread_wakeup_spec cv labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_thread_wakeup_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. rewrite H7. subrewrite. subdestruct; inv HQ; subst.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_big_log}.
Lemma big2_thread_wakeup_match:
∀ s d d´ m f cv a,
big2_thread_wakeup_spec cv d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_thread_wakeup_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_thread_wakeup_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_thread_wakeup_spec}.
Lemma big2_thread_wakeup_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_thread_wakeup_spec)
(id ↦ gensem big2_thread_wakeup_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_thread_wakeup_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_thread_wakeup_match; eauto.
Qed.
End BIG2_THREAD_WAKEUP_SIM_PROOF.
Section BIG2_SCHED_INIT_SIM_PROOF.
Context {re1: relate_impl_init}.
Context {re2: relate_impl_iflags}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_ptpool}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_idpde}.
Context {re7: relate_impl_syncchpool}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_cid}.
Context {re10: relate_impl_vmxinfo}.
Context {re11: relate_impl_nps}.
Context {re12: relate_impl_AC}.
Context {re13: relate_impl_PT}.
Context {re14: relate_impl_big_log}.
Context {re15: relate_impl_ioapic}.
Context {re16: relate_impl_lapic}.
Context {re17: relate_impl_in_intr}.
Context {re18: relate_impl_intr_flag}.
Lemma big2_sched_init_exist:
∀ s f habd habd´ labd z,
big2_sched_init_spec z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_sched_init_spec z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_sched_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_idpde_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto. intros.
exploit relate_impl_lapic_eq; eauto. intros.
exploit relate_impl_in_intr_eq; eauto; intros.
exploit relate_impl_intr_flag_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´.
reflexivity.
eapply relate_impl_cid_update.
eapply relate_impl_syncchpool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_big_log_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_init}.
Context {mt2: match_impl_iflags}.
Context {mt3: match_impl_ipt}.
Context {mt4: match_impl_LAT}.
Context {mt5: match_impl_ptpool}.
Context {mt6: match_impl_lock}.
Context {mt7: match_impl_idpde}.
Context {mt8: match_impl_smspool}.
Context {mt9: match_impl_syncchpool}.
Context {mt10: match_impl_CPU_ID}.
Context {mt11: match_impl_cid}.
Context {mt12: match_impl_vmxinfo}.
Context {mt13: match_impl_nps}.
Context {mt14: match_impl_AC}.
Context {mt15: match_impl_PT}.
Context {mt16: match_impl_big_log}.
Context {mt17: match_impl_ioapic}.
Context {mt19: match_impl_lapic}.
Lemma big2_sched_init_match:
∀ s d d´ m z f,
big2_sched_init_spec z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_sched_init_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_syncchpool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_big_log_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_sched_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_sched_init_spec}.
Lemma big2_sched_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_sched_init_spec)
(id ↦ gensem big2_sched_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_sched_init_match; eauto.
Qed.
End BIG2_SCHED_INIT_SIM_PROOF.
Section BIG2_THREAD_YIELD_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_cid}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_PT}.
Context {re8: relate_impl_in_intr}.
Context {re9: relate_impl_intr_flag}.
Context {re10: relate_impl_init}.
Context {re11: relate_impl_lock}.
Context {re12: relate_impl_AC}.
Context {re13: relate_impl_trapinfo}.
Lemma big2_thread_yield_exist:
∀ s f habd habd´ labd,
big2_thread_yield_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_thread_yield_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_thread_yield_spec. intros.
exploit relate_impl_iflags_eq; eauto.
inversion 1.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_oracle_eq; eauto; intros.
exploit relate_impl_PT_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto; intros.
exploit relate_impl_intr_flag_eq; eauto; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_trapinfo_eq; eauto; intros Htemp; inv Htemp.
revert H; subrewrite; subdestruct; inv HQ; subst.
- refine_split´.
+
inversion ti_snd_eq; subst.
rewrite Hdestruct12.
reflexivity.
+ eapply relate_impl_big_log_update.
assumption.
- refine_split´.
+
inversion ti_snd_eq; subst.
rewrite Hdestruct12.
reflexivity.
+ eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_big_log}.
Lemma big2_thread_yield_match:
∀ s d d´ m f,
big2_thread_yield_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_thread_yield_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_thread_yield_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_thread_yield_spec}.
Lemma big2_thread_yield_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_thread_yield_spec)
(id ↦ gensem big2_thread_yield_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_thread_yield_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_thread_yield_match; eauto.
Qed.
End BIG2_THREAD_YIELD_SIM_PROOF.
Section BIG2_THREAD_SLEEP_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_cid}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_lock}.
Context {re8: relate_impl_syncchpool}.
Context {re9: relate_impl_PT}.
Context {re10: relate_impl_in_intr}.
Context {re11: relate_impl_intr_flag}.
Context {re12: relate_impl_init}.
Context {re13: relate_impl_AC}.
Context {re14: relate_impl_trapinfo}.
Lemma big2_thread_sleep_exist:
∀ s f habd habd´ labd cv,
big2_thread_sleep_spec cv habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_thread_sleep_spec cv labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_thread_sleep_spec. intros.
exploit relate_impl_iflags_eq; eauto.
inversion 1.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_oracle_eq; eauto; intros.
exploit relate_impl_PT_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto; intros.
exploit relate_impl_intr_flag_eq; eauto; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_trapinfo_eq; eauto; intros Htemp; inv Htemp.
revert H. subrewrite; subdestruct; inv HQ; subst.
- refine_split´.
+
inv ti_snd_eq; subst.
rewrite Hdestruct14.
reflexivity.
+ eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
- refine_split´.
+
inv ti_snd_eq; subst.
rewrite Hdestruct14.
reflexivity.
+ eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_lock}.
Context {mt2: match_impl_big_log}.
Lemma big2_thread_sleep_match:
∀ s d d´ m f cv,
big2_thread_sleep_spec cv d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_thread_sleep_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_lock_update.
eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_lock_update.
eapply match_impl_big_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_thread_sleep_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_thread_sleep_spec}.
Lemma big2_thread_sleep_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_thread_sleep_spec)
(id ↦ gensem big2_thread_sleep_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
exploit big2_thread_sleep_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_thread_sleep_match; eauto.
Qed.
End BIG2_THREAD_SLEEP_SIM_PROOF.
Section THREAD_PROC_CREATE_POSTINIT_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Lemma thread_proc_create_postinit_exist:
∀ s habd habd´ labd f elf_id,
thread_proc_create_postinit_spec elf_id habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_proc_create_postinit_spec elf_id labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_proc_create_postinit_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
intros.
rewrite <- H1; subdestruct.
eapply proc_create_postinit_exist; eauto.
Qed.
Lemma thread_proc_create_postinit_match:
∀ s d d´ m f elf_id,
thread_proc_create_postinit_spec elf_id d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_proc_create_postinit_spec; intros.
subdestruct.
eapply proc_create_postinit_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_proc_create_postinit_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_proc_create_postinit_spec}.
Lemma thread_proc_create_postinit_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_proc_create_postinit_spec)
(id ↦ gensem thread_proc_create_postinit_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_proc_create_postinit_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_proc_create_postinit_match; eauto.
Qed.
End THREAD_PROC_CREATE_POSTINIT_SIM_PROOF.
End OBJ_SIM.