Library mcertikos.objects.tmobj.ObjTMIPCDEVPRIM
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 ObjProc.
Require Import liblayers.compat.CompatGenSem.
Require Import Z64Lemma.
Require Import SingleOracle.
Require Import BigLogThreadConfigFunction.
Section OBJ_SECOND_Thread_IPC.
Definition big2_acquire_lock_SC_spec (index: Z) (adt: RData) :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
match (init adt, ikern adt, ihost adt, B_inLock cpu (big_log adt)) with
| (true, true, true, false) ⇒
if zle_lt 0 index num_chan then
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let l´ := (TBEVENT cpu (TBLOCK abid (BWAIT_LOCK (ZMap.get (CPU_ID adt) (cid adt)) local_lock_bound))) :: l1 in
match B_CalLock abid l´ with
| Some _ ⇒
match B_GetSharedSC abid l´ with
| Some e ⇒
Some (adt {big_log: BigDef l´}
{lock: ZMap.set abid (LockOwn true) (lock adt)} {syncchpool: e})
| _ ⇒
Some (adt {big_log: BigDef l´}
{lock: ZMap.set abid (LockOwn true) (lock adt)}
{syncchpool: B_GetlastPush cpu (big_log adt)})
end
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Lemma big2_acquire_lock_SC_lock_status:
∀ n d d´,
big2_acquire_lock_SC_spec n d = Some d´ →
ZMap.get (n + lock_TCB_range) (lock d´) = LockOwn true.
Proof.
unfold big2_acquire_lock_SC_spec. intros.
destruct (init d); try discriminate.
subdestruct; inv H; simpl.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gss. trivial.
Qed.
Function big2_release_lock_SC_spec (index:Z) (adt: RData) :=
match (init adt,
B_inLock (CPU_ID adt) (big_log adt)) with
| (true, true) ⇒ big_release_lock_SC_spec index adt
| _ ⇒ None
end.
Function thread_get_sync_chan_busy_spec (i: Z) (adt: RData) : option Z :=
match (init adt,
B_inLock (CPU_ID adt) (big_log adt)) with
| (true, true) ⇒ get_sync_chan_busy_spec i adt
| _ ⇒ None
end.
Function thread_set_sync_chan_busy_spec (i busy: Z) (adt: RData) : option RData :=
match (init adt,
B_inLock (CPU_ID adt) (big_log adt)) with
| (true, true) ⇒ set_sync_chan_busy_spec i busy adt
| _ ⇒ None
end.
Function thread_ipc_send_body_spec (chid vaddr scount : Z) (adt : RData) : option (RData × Z) :=
match (init adt,
B_inLock (CPU_ID adt) (big_log adt)) with
| (true, true) ⇒ big_ipc_send_body_spec chid vaddr scount adt
| _ ⇒ None
end.
Function thread_ipc_receive_body_spec (chid vaddr rcount : Z) (adt : RData) : option (RData × Z) :=
match (init adt,
B_inLock (CPU_ID adt) (big_log adt)) with
| (true, true) ⇒ big_ipc_receive_body_spec chid vaddr rcount adt
| _ ⇒ None
end.
End OBJ_SECOND_Thread_IPC.
Section OBJ_SECOND_Thread_DEV.
Require Import SingleConfiguration.
Require Import ObjInterruptController.
Require Import ObjInterruptManagement.
Require Import ObjSerialDriver.
Require Import ObjConsole.
Context `{real_params: RealParams}.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops : BigOracleOps}.
Context `{thread_conf_ops: ThreadsConfigurationOps}.
Function thread_cli_spec (abd: RData): option RData :=
if zeq (ZMap.get (CPU_ID abd) (cid abd)) dev_handling_cid
then if (init abd) then cli_spec abd else None else None.
Function thread_sti_spec (abd: RData): option RData :=
if zeq (ZMap.get (CPU_ID abd) (cid abd)) dev_handling_cid
then if (init abd) then sti_spec abd else None else None.
Function thread_serial_intr_disable_spec (abd: RData): option RData :=
if zeq (ZMap.get (CPU_ID abd) (cid abd)) dev_handling_cid
then if (init abd) then serial_intr_disable_spec abd else None else None.
Function thread_serial_intr_enable_spec (abd: RData): option RData :=
if zeq (ZMap.get (CPU_ID abd) (cid abd)) dev_handling_cid
then if (init abd) then serial_intr_enable_spec abd else None else None.
Function thread_serial_putc_spec (c: Z) (abd: RData): option RData :=
if zeq (ZMap.get (CPU_ID abd) (cid abd)) dev_handling_cid
then if (init abd) then serial_putc_spec c abd else None else None.
Function thread_cons_buf_read_spec (abd: RData): option (RData × Z) :=
if zeq (ZMap.get (CPU_ID abd) (cid abd)) dev_handling_cid
then if (init abd) then cons_buf_read_spec abd else None else None.
End OBJ_SECOND_Thread_DEV.
Section OBJ_SECOND_Thread_PRIM.
Context `{real_params: RealParams}.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops : BigOracleOps}.
primitve: return to the host/kernel mode from guest/kernel mode
Function thread_hostin_spec (adt: RData): option RData :=
if init adt then hostin_spec adt else None.
Function thread_hostout_spec (adt: RData): option RData :=
if init adt then hostout_spec adt else None.
Definition thread_trap_info_get_spec (adt: RData): int := trap_info_get_spec adt.
Definition thread_trap_info_ret_spec (adt: RData): val := trap_info_ret_spec adt.
Function thread_uctx_get_spec (i ofs: Z) (adt: RData) : option Z :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
if zeq curid i then if (init adt) then
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
uctx_get_spec i ofs adt else None
| _ ⇒ None
end
else None
else None.
Function thread_uctx_set_spec (i ofs n: Z) (adt: RData) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
if zeq curid i then if (init adt) then
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
uctx_set_spec i ofs n adt else None
| _ ⇒ None
end
else None
else None.
Function thread_proc_start_user_spec (adt : RData) : option (RData × UContext) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
proc_start_user_spec adt else None
| _ ⇒ None
end.
Function thread_proc_exit_user_spec (adt: RData) (rs: UContext) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
proc_exit_user_spec adt rs else None
| _ ⇒ None
end.
End OBJ_SECOND_Thread_PRIM.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import PrimTMSemantics.
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 BIG2_ACQUIRE_LOCk_SC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_big_log}.
Context {re4: relate_impl_lock}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_syncchpool}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_cid}.
Lemma big2_acquire_lock_SC_exist:
∀ s f habd habd´ labd i,
big2_acquire_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_acquire_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_acquire_lock_SC_spec. intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
revert H.
subrewrite; subdestruct; inv HQ.
- rewrite <- H5.
rewrite Hdestruct6.
rewrite Hdestruct7.
refine_split´.
reflexivity.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
- rewrite <- H5.
rewrite Hdestruct6.
rewrite Hdestruct7.
refine_split´.
reflexivity.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt2: match_impl_lock}.
Context {mt3: match_impl_big_log}.
Lemma big2_acquire_lock_SC_match:
∀ s d d´ m f i,
big2_acquire_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_syncchpool_update; eauto.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
- eapply match_impl_syncchpool_update; eauto.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_acquire_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_acquire_lock_SC_spec}.
Lemma big2_acquire_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_acquire_lock_SC_spec)
(id ↦ gensem big2_acquire_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_acquire_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_acquire_lock_SC_match; eauto.
Qed.
End BIG2_ACQUIRE_LOCk_SC_SIM_PROOF.
Section BIG2_RELEASE_LOCk_SC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_big_log}.
Context {re4: relate_impl_lock}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_syncchpool}.
Context {re8: relate_impl_init}.
Context {re9: relate_impl_cid}.
Lemma big2_release_lock_SC_exist:
∀ s f habd habd´ labd i,
big2_release_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_release_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_release_lock_SC_spec. intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
revert H. subrewrite; subdestruct.
eapply big_release_lock_SC_exist in HQ; eauto.
Qed.
Context {mt1: match_impl_lock}.
Context {mt2: match_impl_big_log}.
Lemma big2_release_lock_SC_match:
∀ s d d´ m f i,
big2_release_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_release_lock_SC_spec; intros.
subdestruct.
eapply big_release_lock_SC_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_release_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_release_lock_SC_spec}.
Lemma big2_release_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_release_lock_SC_spec)
(id ↦ gensem big2_release_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_release_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_release_lock_SC_match; eauto.
Qed.
End BIG2_RELEASE_LOCk_SC_SIM_PROOF.
Section THREAD_GET_SYNC_CHAN_BUSY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_syncchpool}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_big_log}.
Lemma thread_get_sync_chan_busy_exist:
∀ s f habd labd chid busy,
thread_get_sync_chan_busy_spec chid habd = Some busy
→ relate_AbData s f habd labd
→ thread_get_sync_chan_busy_spec chid labd = Some busy.
Proof.
unfold thread_get_sync_chan_busy_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
revert H; subrewrite; subdestruct.
eapply get_sync_chan_busy_exist; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_get_sync_chan_busy_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_get_sync_chan_busy_spec}.
Lemma thread_get_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_get_sync_chan_busy_spec)
(id ↦ gensem thread_get_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite thread_get_sync_chan_busy_exist; eauto. reflexivity.
Qed.
End THREAD_GET_SYNC_CHAN_BUSY_SIM_PROOF.
Section THREAD_SET_SYNC_CHAN_BUSY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_syncchpool}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_big_log}.
Context {re6: relate_impl_CPU_ID}.
Lemma thread_set_sync_chan_busy_exist:
∀ s f habd habd´ labd chid busy,
thread_set_sync_chan_busy_spec chid busy habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_set_sync_chan_busy_spec chid busy labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_set_sync_chan_busy_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
eapply set_sync_chan_busy_exist; eauto.
Qed.
Context {mt1: match_impl_syncchpool}.
Lemma thread_set_sync_chan_busy_match:
∀ s d d´ m i n f,
thread_set_sync_chan_busy_spec i n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_set_sync_chan_busy_spec; intros.
subdestruct; inv H; trivial.
eapply set_sync_chan_busy_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_set_sync_chan_busy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_set_sync_chan_busy_spec}.
Lemma thread_set_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_set_sync_chan_busy_spec)
(id ↦ gensem thread_set_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_set_sync_chan_busy_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_set_sync_chan_busy_match; eauto.
Qed.
End THREAD_SET_SYNC_CHAN_BUSY_SIM_PROOF.
Section THREAD_IPC_SEND_BODY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_cid}.
Context {re4: relate_impl_syncchpool}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_big_log}.
Context {re10: relate_impl_HP}.
Context {re11: relate_impl_pperm}.
Context {re12: relate_impl_lock}.
Lemma thread_ipc_send_body_exist:
∀ s f habd habd´ labd chid vaddr count i,
thread_ipc_send_body_spec chid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_ipc_send_body_spec chid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_ipc_send_body_spec; unfold big_ipc_send_body_spec; intros.
exploit relate_impl_iflags_eq; eauto; intros; inv H1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
unfold big_page_copy_spec in Hdestruct7.
unfold big_page_copy_spec.
revert Hdestruct7.
subrewrite´.
intros HQ´; subdestruct.
inv HQ´; inv HQ; simpl in ×.
eapply ObjFlatMem.page_copy_aux_exists in Hdestruct15; eauto;
[ | eapply relate_impl_HP_eq; eauto].
rewrite Hdestruct15.
rewrite Hdestruct16.
refine_split´; eauto.
simpl in ×.
rewrite H6.
eapply relate_impl_syncchpool_update; eauto.
eapply relate_impl_big_log_update; eauto.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt2: match_impl_big_log}.
Lemma thread_ipc_send_body_match:
∀ s d d´ m chid vaddr count i f,
thread_ipc_send_body_spec chid vaddr count d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_ipc_send_body_spec.
unfold big_ipc_send_body_spec.
unfold big_page_copy_spec; intros.
subdestruct; inv H.
eapply match_impl_syncchpool_update.
eapply match_impl_big_log_update.
eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_ipc_send_body_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_ipc_send_body_spec}.
Lemma thread_ipc_send_body_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_ipc_send_body_spec)
(id ↦ gensem thread_ipc_send_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_ipc_send_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_ipc_send_body_match; eauto.
Qed.
End THREAD_IPC_SEND_BODY_SIM_PROOF.
Section THREAD_IPC_RECEIVE_BODY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_cid}.
Context {re4: relate_impl_syncchpool}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_init}.
Context {re9: relate_impl_HP}.
Context {re10: relate_impl_big_log}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_pperm}.
Context {re13: relate_impl_lock}.
Lemma thread_ipc_receive_body_exist:
∀ s f habd habd´ labd fromid vaddr count i,
thread_ipc_receive_body_spec fromid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_ipc_receive_body_spec fromid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_ipc_receive_body_spec;
unfold big_ipc_receive_body_spec;
unfold big_page_copy_back_spec; intros.
exploit relate_impl_iflags_eq; eauto; intros; inv H1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
inv HQ.
eapply ObjFlatMem.page_copy_back_aux_exists in Hdestruct22; eauto;
[ | eapply relate_impl_HP_eq; eauto].
destruct Hdestruct22 as (lh´ & Hdestruct22 & HP´).
rewrite Hdestruct22.
refine_split; eauto.
simpl.
rewrite H5.
eapply relate_impl_syncchpool_update; eauto.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt2: match_impl_HP}.
Lemma thread_ipc_receive_body_match:
∀ s d d´ m i f fromid rvaddr count,
thread_ipc_receive_body_spec fromid rvaddr count d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_ipc_receive_body_spec;
unfold big_ipc_receive_body_spec;
unfold big_page_copy_back_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update.
eapply match_impl_HP_update.
eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_ipc_receive_body_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_ipc_receive_body_spec}.
Lemma thread_ipc_receive_body_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_ipc_receive_body_spec)
(id ↦ gensem thread_ipc_receive_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit thread_ipc_receive_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_ipc_receive_body_match; eauto.
Qed.
End THREAD_IPC_RECEIVE_BODY_SIM_PROOF.
Section THREAD_CLI_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Lemma thread_cli_exist:
∀ s habd habd´ labd f,
thread_cli_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_cli_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_cli_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply cli_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_CPU_ID}.
Context {mt3: match_impl_cid}.
Lemma thread_cli_match:
∀ s d d´ m f,
thread_cli_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_cli_spec.
intros; subdestruct.
eapply cli_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_cli_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_cli_spec}.
Lemma thread_cli_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_cli_spec)
(id ↦ gensem thread_cli_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
edestruct thread_cli_exist as (d2´ & Ha & Hb); eauto.
match_external_states_simpl.
eapply thread_cli_match; eauto.
Qed.
End THREAD_CLI_SIM_PROOF.
Section THREAD_STI_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Lemma thread_sti_exist:
∀ s habd habd´ labd f,
thread_sti_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_sti_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_sti_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply sti_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_CPU_ID}.
Context {mt3: match_impl_cid}.
Lemma thread_sti_match:
∀ s d d´ m f,
thread_sti_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_sti_spec.
intros; subdestruct.
eapply sti_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_sti_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_sti_spec}.
Lemma thread_sti_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_sti_spec)
(id ↦ gensem thread_sti_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
edestruct thread_sti_exist as (d2´ & Ha & Hb); eauto.
match_external_states_simpl.
eapply thread_sti_match; eauto.
Qed.
End THREAD_STI_SIM_PROOF.
Section THREAD_SERIAL_INTR_DISABLE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_drv_serial}.
Context {re4: relate_impl_com1}.
Context {re5: relate_impl_console}.
Context {re6: relate_impl_ioapic}.
Context {re7: relate_impl_lapic}.
Context {re8: relate_impl_curr_intr_num}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_in_intr}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_init}.
Lemma thread_serial_intr_disable_exist:
∀ s habd habd´ labd f,
thread_serial_intr_disable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_serial_intr_disable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_serial_intr_disable_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply serial_intr_disable_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt4: match_impl_curr_intr_num}.
Context {mt5: match_impl_console}.
Context {mt6: match_impl_ioapic}.
Context {mt7: match_impl_lapic}.
Context {mt8: match_impl_in_intr}.
Lemma thread_serial_intr_disable_match:
∀ s d d´ m f,
thread_serial_intr_disable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_serial_intr_disable_spec; intros.
subdestruct.
exploit serial_intr_disable_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_serial_intr_disable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_serial_intr_disable_spec}.
Lemma thread_serial_intr_disable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_serial_intr_disable_spec)
(id ↦ gensem thread_serial_intr_disable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_serial_intr_disable_exist; eauto.
intros.
destruct H as (d2´ & Ha & Hb).
match_external_states_simpl; eauto.
eapply thread_serial_intr_disable_match; eauto.
Qed.
End THREAD_SERIAL_INTR_DISABLE_SIM_PROOF.
Section THREAD_SERIAL_INTR_ENABLE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ioapic}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_intr_flag}.
Context {re5: relate_impl_com1}.
Context {re6: relate_impl_console}.
Context {re7: relate_impl_drv_serial}.
Context {re8: relate_impl_in_intr}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_cid}.
Context {re11: relate_impl_init}.
Lemma thread_serial_intr_enable_spec_exist:
∀ s habd habd´ labd f,
thread_serial_intr_enable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_serial_intr_enable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_serial_intr_enable_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply serial_intr_enable_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt4: match_impl_console}.
Context {mt5: match_impl_ioapic}.
Context {mt6: match_impl_in_intr}.
Lemma thread_serial_intr_enable_spec_match:
∀ s d d´ m f,
thread_serial_intr_enable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_serial_intr_enable_spec; intros.
subdestruct.
exploit serial_intr_enable_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_serial_intr_enable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_serial_intr_enable_spec}.
Lemma thread_serial_intr_enable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_serial_intr_enable_spec)
(id ↦ gensem thread_serial_intr_enable_spec).
Proof.
intros. layer_sim_simpl.
compatsim_simpl (@match_AbData). intros.
exploit thread_serial_intr_enable_spec_exist; eauto. intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_serial_intr_enable_spec_match; eauto.
Qed.
End THREAD_SERIAL_INTR_ENABLE_SIM_PROOF.
Section THREAD_SERIAL_PUTC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Context {re3: relate_impl_com1}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_init}.
Lemma thread_serial_putc_exist:
∀ s habd habd´ labd i f,
thread_serial_putc_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_serial_putc_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_serial_putc_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply serial_putc_exist; eauto.
Qed.
Context {mt1: match_impl_com1}.
Lemma thread_serial_putc_match:
∀ s d d´ m i f,
thread_serial_putc_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_serial_putc_spec; intros. subdestruct; inv H; trivial.
exploit serial_putc_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_serial_putc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_serial_putc_spec}.
Lemma thread_serial_putc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_serial_putc_spec)
(id ↦ gensem thread_serial_putc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_serial_putc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_serial_putc_match; eauto.
Qed.
End THREAD_SERIAL_PUTC_SIM_PROOF.
Section THREAD_CONS_BUF_READ_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_console}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_CPU_ID}.
Context {re5: relate_impl_cid}.
Lemma thread_cons_buf_read_exist:
∀ s habd habd´ c labd f,
thread_cons_buf_read_spec habd = Some (habd´, c)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_cons_buf_read_spec labd = Some (labd´, c)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_cons_buf_read_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
exploit cons_buf_read_exist; eauto.
Qed.
Context {mt1: match_impl_console}.
Lemma thread_cons_buf_read_match:
∀ s d d´ c m f,
thread_cons_buf_read_spec d = Some (d´, c)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_cons_buf_read_spec; intros. subdestruct; inv H; trivial.
exploit cons_buf_read_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_cons_buf_read_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_cons_buf_read_spec}.
Lemma thread_cons_buf_read_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_cons_buf_read_spec)
(id ↦ gensem thread_cons_buf_read_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_cons_buf_read_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_cons_buf_read_match; eauto.
Qed.
End THREAD_CONS_BUF_READ_SIM_PROOF.
if init adt then hostin_spec adt else None.
Function thread_hostout_spec (adt: RData): option RData :=
if init adt then hostout_spec adt else None.
Definition thread_trap_info_get_spec (adt: RData): int := trap_info_get_spec adt.
Definition thread_trap_info_ret_spec (adt: RData): val := trap_info_ret_spec adt.
Function thread_uctx_get_spec (i ofs: Z) (adt: RData) : option Z :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
if zeq curid i then if (init adt) then
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
uctx_get_spec i ofs adt else None
| _ ⇒ None
end
else None
else None.
Function thread_uctx_set_spec (i ofs n: Z) (adt: RData) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
if zeq curid i then if (init adt) then
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
uctx_set_spec i ofs n adt else None
| _ ⇒ None
end
else None
else None.
Function thread_proc_start_user_spec (adt : RData) : option (RData × UContext) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
proc_start_user_spec adt else None
| _ ⇒ None
end.
Function thread_proc_exit_user_spec (adt: RData) (rs: UContext) : option RData :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
proc_exit_user_spec adt rs else None
| _ ⇒ None
end.
End OBJ_SECOND_Thread_PRIM.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import PrimTMSemantics.
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 BIG2_ACQUIRE_LOCk_SC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_big_log}.
Context {re4: relate_impl_lock}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_syncchpool}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_cid}.
Lemma big2_acquire_lock_SC_exist:
∀ s f habd habd´ labd i,
big2_acquire_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_acquire_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_acquire_lock_SC_spec. intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
revert H.
subrewrite; subdestruct; inv HQ.
- rewrite <- H5.
rewrite Hdestruct6.
rewrite Hdestruct7.
refine_split´.
reflexivity.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
- rewrite <- H5.
rewrite Hdestruct6.
rewrite Hdestruct7.
refine_split´.
reflexivity.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt2: match_impl_lock}.
Context {mt3: match_impl_big_log}.
Lemma big2_acquire_lock_SC_match:
∀ s d d´ m f i,
big2_acquire_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_syncchpool_update; eauto.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
- eapply match_impl_syncchpool_update; eauto.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_acquire_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_acquire_lock_SC_spec}.
Lemma big2_acquire_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_acquire_lock_SC_spec)
(id ↦ gensem big2_acquire_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_acquire_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_acquire_lock_SC_match; eauto.
Qed.
End BIG2_ACQUIRE_LOCk_SC_SIM_PROOF.
Section BIG2_RELEASE_LOCk_SC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_big_log}.
Context {re4: relate_impl_lock}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_syncchpool}.
Context {re8: relate_impl_init}.
Context {re9: relate_impl_cid}.
Lemma big2_release_lock_SC_exist:
∀ s f habd habd´ labd i,
big2_release_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_release_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_release_lock_SC_spec. intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
revert H. subrewrite; subdestruct.
eapply big_release_lock_SC_exist in HQ; eauto.
Qed.
Context {mt1: match_impl_lock}.
Context {mt2: match_impl_big_log}.
Lemma big2_release_lock_SC_match:
∀ s d d´ m f i,
big2_release_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_release_lock_SC_spec; intros.
subdestruct.
eapply big_release_lock_SC_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_release_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_release_lock_SC_spec}.
Lemma big2_release_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_release_lock_SC_spec)
(id ↦ gensem big2_release_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_release_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_release_lock_SC_match; eauto.
Qed.
End BIG2_RELEASE_LOCk_SC_SIM_PROOF.
Section THREAD_GET_SYNC_CHAN_BUSY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_syncchpool}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_big_log}.
Lemma thread_get_sync_chan_busy_exist:
∀ s f habd labd chid busy,
thread_get_sync_chan_busy_spec chid habd = Some busy
→ relate_AbData s f habd labd
→ thread_get_sync_chan_busy_spec chid labd = Some busy.
Proof.
unfold thread_get_sync_chan_busy_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
revert H; subrewrite; subdestruct.
eapply get_sync_chan_busy_exist; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_get_sync_chan_busy_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_get_sync_chan_busy_spec}.
Lemma thread_get_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_get_sync_chan_busy_spec)
(id ↦ gensem thread_get_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite thread_get_sync_chan_busy_exist; eauto. reflexivity.
Qed.
End THREAD_GET_SYNC_CHAN_BUSY_SIM_PROOF.
Section THREAD_SET_SYNC_CHAN_BUSY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_syncchpool}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_big_log}.
Context {re6: relate_impl_CPU_ID}.
Lemma thread_set_sync_chan_busy_exist:
∀ s f habd habd´ labd chid busy,
thread_set_sync_chan_busy_spec chid busy habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_set_sync_chan_busy_spec chid busy labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_set_sync_chan_busy_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
eapply set_sync_chan_busy_exist; eauto.
Qed.
Context {mt1: match_impl_syncchpool}.
Lemma thread_set_sync_chan_busy_match:
∀ s d d´ m i n f,
thread_set_sync_chan_busy_spec i n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_set_sync_chan_busy_spec; intros.
subdestruct; inv H; trivial.
eapply set_sync_chan_busy_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_set_sync_chan_busy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_set_sync_chan_busy_spec}.
Lemma thread_set_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_set_sync_chan_busy_spec)
(id ↦ gensem thread_set_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_set_sync_chan_busy_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_set_sync_chan_busy_match; eauto.
Qed.
End THREAD_SET_SYNC_CHAN_BUSY_SIM_PROOF.
Section THREAD_IPC_SEND_BODY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_cid}.
Context {re4: relate_impl_syncchpool}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_big_log}.
Context {re10: relate_impl_HP}.
Context {re11: relate_impl_pperm}.
Context {re12: relate_impl_lock}.
Lemma thread_ipc_send_body_exist:
∀ s f habd habd´ labd chid vaddr count i,
thread_ipc_send_body_spec chid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_ipc_send_body_spec chid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_ipc_send_body_spec; unfold big_ipc_send_body_spec; intros.
exploit relate_impl_iflags_eq; eauto; intros; inv H1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
unfold big_page_copy_spec in Hdestruct7.
unfold big_page_copy_spec.
revert Hdestruct7.
subrewrite´.
intros HQ´; subdestruct.
inv HQ´; inv HQ; simpl in ×.
eapply ObjFlatMem.page_copy_aux_exists in Hdestruct15; eauto;
[ | eapply relate_impl_HP_eq; eauto].
rewrite Hdestruct15.
rewrite Hdestruct16.
refine_split´; eauto.
simpl in ×.
rewrite H6.
eapply relate_impl_syncchpool_update; eauto.
eapply relate_impl_big_log_update; eauto.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt2: match_impl_big_log}.
Lemma thread_ipc_send_body_match:
∀ s d d´ m chid vaddr count i f,
thread_ipc_send_body_spec chid vaddr count d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_ipc_send_body_spec.
unfold big_ipc_send_body_spec.
unfold big_page_copy_spec; intros.
subdestruct; inv H.
eapply match_impl_syncchpool_update.
eapply match_impl_big_log_update.
eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_ipc_send_body_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_ipc_send_body_spec}.
Lemma thread_ipc_send_body_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_ipc_send_body_spec)
(id ↦ gensem thread_ipc_send_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_ipc_send_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_ipc_send_body_match; eauto.
Qed.
End THREAD_IPC_SEND_BODY_SIM_PROOF.
Section THREAD_IPC_RECEIVE_BODY_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_cid}.
Context {re4: relate_impl_syncchpool}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_init}.
Context {re9: relate_impl_HP}.
Context {re10: relate_impl_big_log}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_pperm}.
Context {re13: relate_impl_lock}.
Lemma thread_ipc_receive_body_exist:
∀ s f habd habd´ labd fromid vaddr count i,
thread_ipc_receive_body_spec fromid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_ipc_receive_body_spec fromid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_ipc_receive_body_spec;
unfold big_ipc_receive_body_spec;
unfold big_page_copy_back_spec; intros.
exploit relate_impl_iflags_eq; eauto; intros; inv H1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
inv HQ.
eapply ObjFlatMem.page_copy_back_aux_exists in Hdestruct22; eauto;
[ | eapply relate_impl_HP_eq; eauto].
destruct Hdestruct22 as (lh´ & Hdestruct22 & HP´).
rewrite Hdestruct22.
refine_split; eauto.
simpl.
rewrite H5.
eapply relate_impl_syncchpool_update; eauto.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt2: match_impl_HP}.
Lemma thread_ipc_receive_body_match:
∀ s d d´ m i f fromid rvaddr count,
thread_ipc_receive_body_spec fromid rvaddr count d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_ipc_receive_body_spec;
unfold big_ipc_receive_body_spec;
unfold big_page_copy_back_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update.
eapply match_impl_HP_update.
eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_ipc_receive_body_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_ipc_receive_body_spec}.
Lemma thread_ipc_receive_body_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_ipc_receive_body_spec)
(id ↦ gensem thread_ipc_receive_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit thread_ipc_receive_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_ipc_receive_body_match; eauto.
Qed.
End THREAD_IPC_RECEIVE_BODY_SIM_PROOF.
Section THREAD_CLI_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Lemma thread_cli_exist:
∀ s habd habd´ labd f,
thread_cli_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_cli_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_cli_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply cli_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_CPU_ID}.
Context {mt3: match_impl_cid}.
Lemma thread_cli_match:
∀ s d d´ m f,
thread_cli_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_cli_spec.
intros; subdestruct.
eapply cli_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_cli_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_cli_spec}.
Lemma thread_cli_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_cli_spec)
(id ↦ gensem thread_cli_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
edestruct thread_cli_exist as (d2´ & Ha & Hb); eauto.
match_external_states_simpl.
eapply thread_cli_match; eauto.
Qed.
End THREAD_CLI_SIM_PROOF.
Section THREAD_STI_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Lemma thread_sti_exist:
∀ s habd habd´ labd f,
thread_sti_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_sti_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_sti_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply sti_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_CPU_ID}.
Context {mt3: match_impl_cid}.
Lemma thread_sti_match:
∀ s d d´ m f,
thread_sti_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_sti_spec.
intros; subdestruct.
eapply sti_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_sti_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_sti_spec}.
Lemma thread_sti_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_sti_spec)
(id ↦ gensem thread_sti_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
edestruct thread_sti_exist as (d2´ & Ha & Hb); eauto.
match_external_states_simpl.
eapply thread_sti_match; eauto.
Qed.
End THREAD_STI_SIM_PROOF.
Section THREAD_SERIAL_INTR_DISABLE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_intr_flag}.
Context {re3: relate_impl_drv_serial}.
Context {re4: relate_impl_com1}.
Context {re5: relate_impl_console}.
Context {re6: relate_impl_ioapic}.
Context {re7: relate_impl_lapic}.
Context {re8: relate_impl_curr_intr_num}.
Context {re9: relate_impl_init}.
Context {re10: relate_impl_in_intr}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_init}.
Lemma thread_serial_intr_disable_exist:
∀ s habd habd´ labd f,
thread_serial_intr_disable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_serial_intr_disable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_serial_intr_disable_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply serial_intr_disable_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt4: match_impl_curr_intr_num}.
Context {mt5: match_impl_console}.
Context {mt6: match_impl_ioapic}.
Context {mt7: match_impl_lapic}.
Context {mt8: match_impl_in_intr}.
Lemma thread_serial_intr_disable_match:
∀ s d d´ m f,
thread_serial_intr_disable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_serial_intr_disable_spec; intros.
subdestruct.
exploit serial_intr_disable_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_serial_intr_disable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_serial_intr_disable_spec}.
Lemma thread_serial_intr_disable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_serial_intr_disable_spec)
(id ↦ gensem thread_serial_intr_disable_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_serial_intr_disable_exist; eauto.
intros.
destruct H as (d2´ & Ha & Hb).
match_external_states_simpl; eauto.
eapply thread_serial_intr_disable_match; eauto.
Qed.
End THREAD_SERIAL_INTR_DISABLE_SIM_PROOF.
Section THREAD_SERIAL_INTR_ENABLE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ioapic}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_intr_flag}.
Context {re5: relate_impl_com1}.
Context {re6: relate_impl_console}.
Context {re7: relate_impl_drv_serial}.
Context {re8: relate_impl_in_intr}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_cid}.
Context {re11: relate_impl_init}.
Lemma thread_serial_intr_enable_spec_exist:
∀ s habd habd´ labd f,
thread_serial_intr_enable_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_serial_intr_enable_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_serial_intr_enable_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply serial_intr_enable_exist; eauto.
Qed.
Context {mt1: match_impl_intr_flag}.
Context {mt2: match_impl_drv_serial}.
Context {mt3: match_impl_com1}.
Context {mt4: match_impl_console}.
Context {mt5: match_impl_ioapic}.
Context {mt6: match_impl_in_intr}.
Lemma thread_serial_intr_enable_spec_match:
∀ s d d´ m f,
thread_serial_intr_enable_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_serial_intr_enable_spec; intros.
subdestruct.
exploit serial_intr_enable_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_serial_intr_enable_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_serial_intr_enable_spec}.
Lemma thread_serial_intr_enable_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_serial_intr_enable_spec)
(id ↦ gensem thread_serial_intr_enable_spec).
Proof.
intros. layer_sim_simpl.
compatsim_simpl (@match_AbData). intros.
exploit thread_serial_intr_enable_spec_exist; eauto. intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_serial_intr_enable_spec_match; eauto.
Qed.
End THREAD_SERIAL_INTR_ENABLE_SIM_PROOF.
Section THREAD_SERIAL_PUTC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_drv_serial}.
Context {re3: relate_impl_com1}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_init}.
Lemma thread_serial_putc_exist:
∀ s habd habd´ labd i f,
thread_serial_putc_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_serial_putc_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_serial_putc_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
eapply serial_putc_exist; eauto.
Qed.
Context {mt1: match_impl_com1}.
Lemma thread_serial_putc_match:
∀ s d d´ m i f,
thread_serial_putc_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_serial_putc_spec; intros. subdestruct; inv H; trivial.
exploit serial_putc_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_serial_putc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_serial_putc_spec}.
Lemma thread_serial_putc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_serial_putc_spec)
(id ↦ gensem thread_serial_putc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_serial_putc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_serial_putc_match; eauto.
Qed.
End THREAD_SERIAL_PUTC_SIM_PROOF.
Section THREAD_CONS_BUF_READ_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_console}.
Context {re3: relate_impl_init}.
Context {re4: relate_impl_CPU_ID}.
Context {re5: relate_impl_cid}.
Lemma thread_cons_buf_read_exist:
∀ s habd habd´ c labd f,
thread_cons_buf_read_spec habd = Some (habd´, c)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_cons_buf_read_spec labd = Some (labd´, c)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_cons_buf_read_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
exploit cons_buf_read_exist; eauto.
Qed.
Context {mt1: match_impl_console}.
Lemma thread_cons_buf_read_match:
∀ s d d´ c m f,
thread_cons_buf_read_spec d = Some (d´, c)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_cons_buf_read_spec; intros. subdestruct; inv H; trivial.
exploit cons_buf_read_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_cons_buf_read_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_cons_buf_read_spec}.
Lemma thread_cons_buf_read_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_cons_buf_read_spec)
(id ↦ gensem thread_cons_buf_read_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_cons_buf_read_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_cons_buf_read_match; eauto.
Qed.
End THREAD_CONS_BUF_READ_SIM_PROOF.
primitve: return to the host/kernel mode from guest/kernel mode
Section THREAD_HOSTIN_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Lemma thread_hostin_exist:
∀ s habd habd´ labd f,
thread_hostin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_hostin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_hostin_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
exploit hostin_exist; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Lemma thread_hostin_match:
∀ s d d´ m f,
thread_hostin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_hostin_spec; intros.
subdestruct.
eapply hostin_match; eauto.
Qed.
Context {inv: PrimInvariants (data_ops:= data_ops) thread_hostin_spec}.
Context {inv0: PrimInvariants (data_ops:= data_ops0) thread_hostin_spec}.
Lemma thread_hostin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem thread_hostin_spec)
(id ↦ primcall_general_compatsem thread_hostin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit thread_hostin_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_hostin_match; eauto.
Qed.
End THREAD_HOSTIN_SIM_PROOF.
Section THREAD_HOSTOUT_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Lemma thread_hostout_exist:
∀ s habd habd´ labd f,
thread_hostout_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_hostout_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_hostout_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
exploit hostout_exist; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Lemma thread_hostout_match:
∀ s d d´ m f,
thread_hostout_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_hostout_spec; intros.
subdestruct.
eapply hostout_match; eauto.
Qed.
Context {inv: PrimInvariants (data_ops:= data_ops) thread_hostout_spec}.
Context {inv0: PrimInvariants (data_ops:= data_ops0) thread_hostout_spec}.
Lemma thread_hostout_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem thread_hostout_spec)
(id ↦ primcall_general_compatsem thread_hostout_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit thread_hostout_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_hostout_match; eauto.
Qed.
End THREAD_HOSTOUT_SIM_PROOF.
Section THREAD_TRAP_INFO_SIM_PROOF.
Context {re1: relate_impl_trapinfo}.
Lemma thread_trap_info_get_exist:
∀ habd labd s z f,
thread_trap_info_get_spec habd = z
→ relate_AbData s f habd labd
→ thread_trap_info_get_spec labd = z.
Proof.
unfold thread_trap_info_get_spec.
eapply trap_info_get_exist; eauto.
Qed.
Lemma thread_trap_info_ret_exist:
∀ habd labd s f,
relate_AbData s f habd labd
→ val_inject f (thread_trap_info_ret_spec habd) (thread_trap_info_ret_spec labd).
Proof.
unfold thread_trap_info_ret_spec.
eapply trap_info_ret_exist; eauto.
Qed.
Lemma thread_trap_info_get_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec)
(id ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
match_external_states_simpl.
erewrite (thread_trap_info_get_exist d1´ d2); eauto.
Qed.
Context {low1: low_level_invariant_impl}.
Lemma thread_trap_info_ret_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec)
(id ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl.
eapply thread_trap_info_ret_exist; eauto.
Qed.
End THREAD_TRAP_INFO_SIM_PROOF.
Section THREAD_UCTX_GET_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_uctxt}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_big_log}.
Lemma thread_uctx_get_exist:
∀ s habd labd i1 i2 z f,
thread_uctx_get_spec i1 i2 habd = Some z
→ relate_AbData s f habd labd
→ thread_uctx_get_spec i1 i2 labd = Some z.
Proof.
unfold thread_uctx_get_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
rewrite <- H4.
rewrite <- e.
rewrite H2, H3 in Hdestruct2.
rewrite Hdestruct2.
rewrite e.
eapply uctx_get_exist; eauto.
Qed.
Lemma thread_uctx_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_uctx_get_spec)
(id ↦ gensem thread_uctx_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite thread_uctx_get_exist; eauto. reflexivity.
Qed.
End THREAD_UCTX_GET_SIM_PROOF.
Section THREAD_UCTX_SET_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_big_log}.
Lemma thread_uctx_set_exist:
∀ s habd habd´ labd z1 z2 i f,
thread_uctx_set_spec i z1 z2 habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_uctx_set_spec i z1 z2 labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_uctx_set_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite <- e; rewrite <- H1.
rewrite H2, H3.
rewrite zeq_true.
rewrite <- e in H.
rewrite H2, H3 in H.
rewrite <- H4.
rewrite H2, H3 in Hdestruct2.
rewrite Hdestruct2.
eauto using uctx_set_exist.
Qed.
Context {mt1: match_impl_uctxt}.
Lemma thread_uctx_set_match:
∀ s d d´ m z1 z2 i f,
thread_uctx_set_spec i z1 z2 d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_uctx_set_spec; intros. subdestruct; inv H; trivial.
eauto using uctx_set_match.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_uctx_set_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_uctx_set_spec}.
Lemma thread_uctx_set_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_uctx_set_spec)
(id ↦ gensem thread_uctx_set_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_uctx_set_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_uctx_set_match; eauto.
Qed.
End THREAD_UCTX_SET_SIM_PROOF.
Section THREAD_PROC_START_USER_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma thread_proc_start_user_exist:
∀ s habd habd´ labd rs0 f,
thread_proc_start_user_spec habd = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´ r´0, thread_proc_start_user_spec labd = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i,
0≤ i < UCTXT_SIZE → val_inject f (ZMap.get i rs0) (ZMap.get i r´0))
∧ r´0 = ZMap.get (ZMap.get (CPU_ID labd) (cid labd)) (uctxt labd)
∧ 0 ≤ ZMap.get (CPU_ID labd) (cid labd) < num_proc.
Proof.
unfold thread_proc_start_user_spec; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite <- H4.
rewrite Hdestruct0.
eauto using proc_start_user_exist.
Qed.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Lemma thread_proc_start_user_match:
∀ s d d´ m rs0 f,
thread_proc_start_user_spec d = Some (d´, rs0)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_proc_start_user_spec; intros.
subdestruct.
eauto using proc_start_user_match.
Qed.
Context {inv: TMStartUserInvariants thread_proc_start_user_spec (data_ops:= data_ops)}.
Context {inv0: TMStartUserInvariants thread_proc_start_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_start_user_sim :
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec)
(id ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H0. inv H1. inv match_extcall_states.
exploit thread_proc_start_user_exist; eauto 1.
eapply H; assumption.
intros (labd´ & r´0 & HP & HM & Hrinj´ & Hr & HOS´). subst r´0.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; omega).
- intros. eapply uctxt_INJECT; try assumption.
- intros. eapply uctxt_INJECT; try assumption.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
+ rewrite <- H2 in HUEIP_val_cond1.
elim HUEIP_val_cond1.
reflexivity.
+ rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- eapply thread_proc_start_user_match; eauto.
Qed.
End THREAD_PROC_START_USER_SIM_PROOF.
Section THREAD_PROC_START_USER_SIM2_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {inv: TMStartUserInvariants2 thread_proc_start_user_spec (data_ops:= data_ops)}.
Context {inv0: TMStartUserInvariants2 thread_proc_start_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_start_user_sim2 :
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec)
(id ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H0. inv H1. inv match_extcall_states.
exploit thread_proc_start_user_exist; eauto 1.
eapply H; assumption.
intros (labd´ & r´0 & HP & HM & Hrinj´ & Hr & HOS´). subst r´0.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; omega).
- intros. eapply uctxt_INJECT; try assumption.
- intros. eapply uctxt_INJECT; try assumption.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
+ rewrite <- H2 in HUEIP_val_cond1.
elim HUEIP_val_cond1.
reflexivity.
+ rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- eapply thread_proc_start_user_match; eauto.
Qed.
End THREAD_PROC_START_USER_SIM2_PROOF.
Section THREAD_PROC_EXIT_USER_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_PT}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_big_log}.
Lemma thread_proc_exit_user_exist:
∀ s habd habd´ labd rs0 f,
thread_proc_exit_user_spec habd rs0 = Some habd´
→ relate_AbData s f habd labd
→ (∀ i,
0≤ i < UCTXT_SIZE → val_inject f (ZMap.get i rs0) (ZMap.get i rs0))
→ ∃ labd´, thread_proc_exit_user_spec labd rs0 = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_proc_exit_user_spec; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite <- H4.
rewrite Hdestruct0.
eauto using proc_exit_user_exist.
Qed.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {mt4: match_impl_uctxt}.
Lemma thread_proc_exit_user_match:
∀ s d d´ m rs0 f,
thread_proc_exit_user_spec d rs0 = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_proc_exit_user_spec; intros.
subdestruct.
eauto using proc_exit_user_match.
Qed.
Context {inv: TMExitUserInvariants thread_proc_exit_user_spec (data_ops:= data_ops)}.
Context {inv0: TMExitUserInvariants thread_proc_exit_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_exit_user_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec)
(id ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit thread_proc_exit_user_exist; eauto 1.
- subst uctx4 uctx3 uctx2 uctx1.
intros. inv_proc.
rewrite ZMap.gi. constructor.
- intros (labd´ & HP & HM).
refine_split; eauto 1.
econstructor; eauto 1.
+ reflexivity.
+ eapply reg_val_inject_defined; eauto 1.
+ intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H2) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H2 match_inject).
+ exploit (LAsmModuleSemAux.extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply LAsmModuleSemAux.extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply LAsmModuleSemAux.extcall_args_without_data in H; eauto.
+ eapply reg_symbol_inject; eassumption.
+ econstructor; eauto. econstructor; eauto.
eapply thread_proc_exit_user_match; eauto.
val_inject_simpl.
Qed.
End THREAD_PROC_EXIT_USER_SIM_PROOF.
Section THREAD_PROC_EXIT_USER_SIM2_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_PT}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_big_log}.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {mt4: match_impl_uctxt}.
Context {inv: TMExitUserInvariants2 thread_proc_exit_user_spec (data_ops:= data_ops)}.
Context {inv0: TMExitUserInvariants2 thread_proc_exit_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_exit_user_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec)
(id ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit thread_proc_exit_user_exist; eauto 1.
- subst uctx4 uctx3 uctx2 uctx1.
intros. inv_proc.
rewrite ZMap.gi. constructor.
- intros (labd´ & HP & HM).
refine_split; eauto 1.
econstructor; eauto 1.
+ reflexivity.
+ eapply reg_val_inject_defined; eauto 1.
+ intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H2) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H2 match_inject).
+ exploit (LAsmModuleSemAux.extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply LAsmModuleSemAux.extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply LAsmModuleSemAux.extcall_args_without_data in H; eauto.
+ eapply reg_symbol_inject; eassumption.
+ econstructor; eauto. econstructor; eauto.
eapply thread_proc_exit_user_match; eauto.
val_inject_simpl.
Qed.
End THREAD_PROC_EXIT_USER_SIM2_PROOF.
End OBJ_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Lemma thread_hostin_exist:
∀ s habd habd´ labd f,
thread_hostin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_hostin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_hostin_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
exploit hostin_exist; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Lemma thread_hostin_match:
∀ s d d´ m f,
thread_hostin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_hostin_spec; intros.
subdestruct.
eapply hostin_match; eauto.
Qed.
Context {inv: PrimInvariants (data_ops:= data_ops) thread_hostin_spec}.
Context {inv0: PrimInvariants (data_ops:= data_ops0) thread_hostin_spec}.
Lemma thread_hostin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem thread_hostin_spec)
(id ↦ primcall_general_compatsem thread_hostin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit thread_hostin_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_hostin_match; eauto.
Qed.
End THREAD_HOSTIN_SIM_PROOF.
Section THREAD_HOSTOUT_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Lemma thread_hostout_exist:
∀ s habd habd´ labd f,
thread_hostout_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_hostout_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_hostout_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
revert H; subrewrite.
subdestruct.
exploit hostout_exist; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Lemma thread_hostout_match:
∀ s d d´ m f,
thread_hostout_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_hostout_spec; intros.
subdestruct.
eapply hostout_match; eauto.
Qed.
Context {inv: PrimInvariants (data_ops:= data_ops) thread_hostout_spec}.
Context {inv0: PrimInvariants (data_ops:= data_ops0) thread_hostout_spec}.
Lemma thread_hostout_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem thread_hostout_spec)
(id ↦ primcall_general_compatsem thread_hostout_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit thread_hostout_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_hostout_match; eauto.
Qed.
End THREAD_HOSTOUT_SIM_PROOF.
Section THREAD_TRAP_INFO_SIM_PROOF.
Context {re1: relate_impl_trapinfo}.
Lemma thread_trap_info_get_exist:
∀ habd labd s z f,
thread_trap_info_get_spec habd = z
→ relate_AbData s f habd labd
→ thread_trap_info_get_spec labd = z.
Proof.
unfold thread_trap_info_get_spec.
eapply trap_info_get_exist; eauto.
Qed.
Lemma thread_trap_info_ret_exist:
∀ habd labd s f,
relate_AbData s f habd labd
→ val_inject f (thread_trap_info_ret_spec habd) (thread_trap_info_ret_spec labd).
Proof.
unfold thread_trap_info_ret_spec.
eapply trap_info_ret_exist; eauto.
Qed.
Lemma thread_trap_info_get_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec)
(id ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
match_external_states_simpl.
erewrite (thread_trap_info_get_exist d1´ d2); eauto.
Qed.
Context {low1: low_level_invariant_impl}.
Lemma thread_trap_info_ret_sim :
∀ id,
sim (crel RData RData)
(id ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec)
(id ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl.
eapply thread_trap_info_ret_exist; eauto.
Qed.
End THREAD_TRAP_INFO_SIM_PROOF.
Section THREAD_UCTX_GET_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_uctxt}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_big_log}.
Lemma thread_uctx_get_exist:
∀ s habd labd i1 i2 z f,
thread_uctx_get_spec i1 i2 habd = Some z
→ relate_AbData s f habd labd
→ thread_uctx_get_spec i1 i2 labd = Some z.
Proof.
unfold thread_uctx_get_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite H2, H3 in e.
rewrite <- H1; rewrite e; rewrite zeq_true; auto.
rewrite <- H4.
rewrite <- e.
rewrite H2, H3 in Hdestruct2.
rewrite Hdestruct2.
rewrite e.
eapply uctx_get_exist; eauto.
Qed.
Lemma thread_uctx_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_uctx_get_spec)
(id ↦ gensem thread_uctx_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite thread_uctx_get_exist; eauto. reflexivity.
Qed.
End THREAD_UCTX_GET_SIM_PROOF.
Section THREAD_UCTX_SET_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_big_log}.
Lemma thread_uctx_set_exist:
∀ s habd habd´ labd z1 z2 i f,
thread_uctx_set_spec i z1 z2 habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_uctx_set_spec i z1 z2 labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_uctx_set_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite <- e; rewrite <- H1.
rewrite H2, H3.
rewrite zeq_true.
rewrite <- e in H.
rewrite H2, H3 in H.
rewrite <- H4.
rewrite H2, H3 in Hdestruct2.
rewrite Hdestruct2.
eauto using uctx_set_exist.
Qed.
Context {mt1: match_impl_uctxt}.
Lemma thread_uctx_set_match:
∀ s d d´ m z1 z2 i f,
thread_uctx_set_spec i z1 z2 d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_uctx_set_spec; intros. subdestruct; inv H; trivial.
eauto using uctx_set_match.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_uctx_set_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_uctx_set_spec}.
Lemma thread_uctx_set_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_uctx_set_spec)
(id ↦ gensem thread_uctx_set_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_uctx_set_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply thread_uctx_set_match; eauto.
Qed.
End THREAD_UCTX_SET_SIM_PROOF.
Section THREAD_PROC_START_USER_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Lemma thread_proc_start_user_exist:
∀ s habd habd´ labd rs0 f,
thread_proc_start_user_spec habd = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ 0 ≤ ZMap.get (CPU_ID habd) (cid habd) < num_proc
→ ∃ labd´ r´0, thread_proc_start_user_spec labd = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i,
0≤ i < UCTXT_SIZE → val_inject f (ZMap.get i rs0) (ZMap.get i r´0))
∧ r´0 = ZMap.get (ZMap.get (CPU_ID labd) (cid labd)) (uctxt labd)
∧ 0 ≤ ZMap.get (CPU_ID labd) (cid labd) < num_proc.
Proof.
unfold thread_proc_start_user_spec; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite <- H4.
rewrite Hdestruct0.
eauto using proc_start_user_exist.
Qed.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Lemma thread_proc_start_user_match:
∀ s d d´ m rs0 f,
thread_proc_start_user_spec d = Some (d´, rs0)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_proc_start_user_spec; intros.
subdestruct.
eauto using proc_start_user_match.
Qed.
Context {inv: TMStartUserInvariants thread_proc_start_user_spec (data_ops:= data_ops)}.
Context {inv0: TMStartUserInvariants thread_proc_start_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_start_user_sim :
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec)
(id ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H0. inv H1. inv match_extcall_states.
exploit thread_proc_start_user_exist; eauto 1.
eapply H; assumption.
intros (labd´ & r´0 & HP & HM & Hrinj´ & Hr & HOS´). subst r´0.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; omega).
- intros. eapply uctxt_INJECT; try assumption.
- intros. eapply uctxt_INJECT; try assumption.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
+ rewrite <- H2 in HUEIP_val_cond1.
elim HUEIP_val_cond1.
reflexivity.
+ rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- eapply thread_proc_start_user_match; eauto.
Qed.
End THREAD_PROC_START_USER_SIM_PROOF.
Section THREAD_PROC_START_USER_SIM2_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_CPU_ID}.
Context {re8: relate_impl_big_log}.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {inv: TMStartUserInvariants2 thread_proc_start_user_spec (data_ops:= data_ops)}.
Context {inv0: TMStartUserInvariants2 thread_proc_start_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_start_user_sim2 :
∀ id,
(∀ d1, high_level_invariant (CompatDataOps:= data_ops) d1 →
0 ≤ ZMap.get (CPU_ID d1) (cid d1) < num_proc) →
sim (crel RData RData) (id ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec)
(id ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H0. inv H1. inv match_extcall_states.
exploit thread_proc_start_user_exist; eauto 1.
eapply H; assumption.
intros (labd´ & r´0 & HP & HM & Hrinj´ & Hr & HOS´). subst r´0.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; omega).
- intros. eapply uctxt_INJECT; try assumption.
- intros. eapply uctxt_INJECT; try assumption.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
+ rewrite <- H2 in HUEIP_val_cond1.
elim HUEIP_val_cond1.
reflexivity.
+ rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- intro contra.
generalize (Hrinj´ 12).
intros Htemp; exploit Htemp; try omega.
clear Htemp.
intro Htemp.
rewrite contra in Htemp.
inv Htemp.
rewrite <- H2 in HUEIP_val_cond2.
elim HUEIP_val_cond2.
reflexivity.
- eapply thread_proc_start_user_match; eauto.
Qed.
End THREAD_PROC_START_USER_SIM2_PROOF.
Section THREAD_PROC_EXIT_USER_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_PT}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_big_log}.
Lemma thread_proc_exit_user_exist:
∀ s habd habd´ labd rs0 f,
thread_proc_exit_user_spec habd rs0 = Some habd´
→ relate_AbData s f habd labd
→ (∀ i,
0≤ i < UCTXT_SIZE → val_inject f (ZMap.get i rs0) (ZMap.get i rs0))
→ ∃ labd´, thread_proc_exit_user_spec labd rs0 = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_proc_exit_user_spec; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
subdestruct.
revert Hdestruct Hdestruct0; subrewrite; intros.
rewrite <- H4.
rewrite Hdestruct0.
eauto using proc_exit_user_exist.
Qed.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {mt4: match_impl_uctxt}.
Lemma thread_proc_exit_user_match:
∀ s d d´ m rs0 f,
thread_proc_exit_user_spec d rs0 = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_proc_exit_user_spec; intros.
subdestruct.
eauto using proc_exit_user_match.
Qed.
Context {inv: TMExitUserInvariants thread_proc_exit_user_spec (data_ops:= data_ops)}.
Context {inv0: TMExitUserInvariants thread_proc_exit_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_exit_user_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec)
(id ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit thread_proc_exit_user_exist; eauto 1.
- subst uctx4 uctx3 uctx2 uctx1.
intros. inv_proc.
rewrite ZMap.gi. constructor.
- intros (labd´ & HP & HM).
refine_split; eauto 1.
econstructor; eauto 1.
+ reflexivity.
+ eapply reg_val_inject_defined; eauto 1.
+ intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H2) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H2 match_inject).
+ exploit (LAsmModuleSemAux.extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply LAsmModuleSemAux.extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply LAsmModuleSemAux.extcall_args_without_data in H; eauto.
+ eapply reg_symbol_inject; eassumption.
+ econstructor; eauto. econstructor; eauto.
eapply thread_proc_exit_user_match; eauto.
val_inject_simpl.
Qed.
End THREAD_PROC_EXIT_USER_SIM_PROOF.
Section THREAD_PROC_EXIT_USER_SIM2_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_uctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_PT}.
Context {re6: relate_impl_CPU_ID}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_big_log}.
Context {mt1: match_impl_PT}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_iflags}.
Context {mt4: match_impl_uctxt}.
Context {inv: TMExitUserInvariants2 thread_proc_exit_user_spec (data_ops:= data_ops)}.
Context {inv0: TMExitUserInvariants2 thread_proc_exit_user_spec (data_ops:= data_ops0)}.
Context {low1: low_level_invariant_impl}.
Lemma thread_proc_exit_user_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec)
(id ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit thread_proc_exit_user_exist; eauto 1.
- subst uctx4 uctx3 uctx2 uctx1.
intros. inv_proc.
rewrite ZMap.gi. constructor.
- intros (labd´ & HP & HM).
refine_split; eauto 1.
econstructor; eauto 1.
+ reflexivity.
+ eapply reg_val_inject_defined; eauto 1.
+ intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H0)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H2) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H2 match_inject).
+ exploit (LAsmModuleSemAux.extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= d1´).
apply LAsmModuleSemAux.extcall_args_with_data; eauto.
instantiate (1:= d2).
intros [?[? Hinv]]. inv_val_inject.
apply LAsmModuleSemAux.extcall_args_without_data in H; eauto.
+ eapply reg_symbol_inject; eassumption.
+ econstructor; eauto. econstructor; eauto.
eapply thread_proc_exit_user_match; eauto.
val_inject_simpl.
Qed.
End THREAD_PROC_EXIT_USER_SIM2_PROOF.
End OBJ_SIM.