Library mcertikos.objects.ObjCV
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 ObjVMM.
Require Import ObjFlatMem.
Require Import DeviceStateDataType.
Require Export ObjInterruptDriver.
Section MULTIPROCESSOR.
primitive: get the i-th sync_channel's count
Function get_sync_chan_count_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ _ c _ ⇒ Some (Int.unsigned c)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function get_sync_chan_to_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid to _ _ _ ⇒ Some (Int.unsigned to)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function get_sync_chan_paddr_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ vaddr _ _ ⇒ Some (Int.unsigned vaddr)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function get_sync_chan_busy_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ _ _ busy ⇒ Some (Int.unsigned busy)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_count_spec (i count: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid t v _ b
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid t v (Int.repr count) b)
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_to_spec (i to: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ v c b
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid (Int.repr to) v c b)
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_paddr_spec (i vaddr: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid t _ c b
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid t (Int.repr vaddr) c b)
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_busy_spec (i busy: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid t v c _
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid t v c (Int.repr busy))
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function init_sync_chan_spec (i : Z) (adt : RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
Some adt {syncchpool:
ZMap.set i (SyncChanValid (Int.repr num_chan) (Int.repr 0) (Int.repr 0) (Int.repr 0))
(syncchpool adt)}
else None
| _ ⇒ None
end.
Context `{real_params: RealParams}.
Context `{waittime: WaitTime}.
Function fifobbq_pool_init_spec (mbi_adr: Z) (adt: RData): option RData :=
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, 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} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde adt)}
{smspool: real_smspool (smspool adt)}
{abtcb: real_abtcb (abtcb adt)}
{abq: real_abq (abq adt)}
{syncchpool: real_syncchpool (syncchpool adt)}
else None
else None
| _ ⇒ None
end.
Function get_kernel_pa_spec (pid vaddr : Z) (adt : RData) : option Z :=
match pg adt with
| true ⇒ match ptRead_spec pid vaddr adt with
| Some paddr ⇒
if zeq paddr 0 then None else Some (paddr / PgSize × PgSize + (vaddr mod PgSize))
| _ ⇒ None
end
| _ ⇒ None
end.
Function ipc_receive_body_spec (chid vaddr rcount : Z) (adt : RData) : option (RData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid sender spaddr scount busy ⇒
let arecvcount := Z.min (Int.unsigned scount) rcount in
match page_copy_back_spec chid arecvcount vaddr adt with
| Some adt1 ⇒
Some (adt1 {syncchpool: ZMap.set chid
(SyncChanValid sender spaddr Int.zero busy)
(syncchpool adt1)}, arecvcount)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function ipc_send_body_spec (chid vaddr scount : Z) (adt : RData) : option (RData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid sender spaddr _ busy ⇒
let asendval := Z.min (scount) (1024) in
match page_copy_spec chid asendval vaddr adt with
| Some adt´ ⇒
Some (adt´ {syncchpool :
ZMap.set chid
(SyncChanValid sender spaddr (Int.repr asendval) busy)
(syncchpool adt´)}, asendval)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
End MULTIPROCESSOR.
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.
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}.
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.
Section GET_KERNEL_PA.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_PT}.
Context {re4: relate_impl_ptpool}.
Context {re5: relate_impl_init}.
Lemma get_kernel_pa_exist:
∀ s f habd labd va chid pa,
get_kernel_pa_spec chid va habd = Some pa
→ relate_AbData s f habd labd
→ get_kernel_pa_spec chid va labd = Some pa.
Proof.
unfold get_kernel_pa_spec in *; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_PT_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ.
erewrite ptRead_exist; eauto.
rewrite Hdestruct1; auto.
Qed.
End GET_KERNEL_PA.
Section FIFOBBQ_POOl_INIT.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re10: relate_impl_smspool}.
Context {re11: relate_impl_abtcb}.
Context {re12: relate_impl_abq}.
Context {re13: relate_impl_cid}.
Context {re14: relate_impl_vmxinfo}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_ioapic}.
Context {re17: relate_impl_lapic}.
Context {re18: relate_impl_in_intr}.
Context {re30: relate_impl_syncchpool}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re20: relate_impl_multi_log}.
Lemma fifobbq_pool_init_exist:
∀ s f habd habd´ labd i,
fifobbq_pool_init_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fifobbq_pool_init_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold fifobbq_pool_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_idpde_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_abq_eq; eauto.
exploit relate_impl_abtcb_eq; eauto.
exploit relate_impl_vmxinfo_eq; eauto.
exploit relate_impl_smspool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_syncchpool_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.
revert H. subrewrite.
subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_syncchpool_update.
apply relate_impl_abq_update.
apply relate_impl_abtcb_update.
apply relate_impl_smspool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_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_LAT_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_iflags}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_LAT}.
Context {mt4: match_impl_nps}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_PT}.
Context {mt7: match_impl_ptpool}.
Context {mt8: match_impl_idpde}.
Context {mt10: match_impl_smspool}.
Context {mt11: match_impl_abtcb}.
Context {mt12: match_impl_abq}.
Context {mt13: match_impl_cid}.
Context {mt14: match_impl_vmxinfo}.
Context {mt15: match_impl_AC}.
Context {mt50: match_impl_multi_log}.
Context {mt30: match_impl_syncchpool}.
Context {mt16: match_impl_ioapic}.
Context {mt17: match_impl_lapic}.
Lemma fifobbq_pool_init_match:
∀ s d d´ m i f,
fifobbq_pool_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold fifobbq_pool_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update.
eapply match_impl_abq_update.
eapply match_impl_abtcb_update.
eapply match_impl_smspool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_multi_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_LAT_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) fifobbq_pool_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) fifobbq_pool_init_spec}.
Lemma fifobbq_pool_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem fifobbq_pool_init_spec)
(id ↦ gensem fifobbq_pool_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit fifobbq_pool_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply fifobbq_pool_init_match; eauto.
Qed.
End FIFOBBQ_POOl_INIT.
Section SYNCRECEIVE_CHAN.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_syncchpool}.
Context {re8: relate_impl_abq}.
Context {re10: relate_impl_PT}.
Context {re11: relate_impl_ptpool}.
Context {re12: relate_impl_init}.
Context {re14: relate_impl_HP}.
Context {re15: relate_impl_pperm}.
Context {re300: relate_impl_CPU_ID}.
Context {re301: relate_impl_lock}.
Context {re302: relate_impl_multi_log}.
Lemma ipc_receive_body_exist:
∀ s f habd habd´ labd fromid vaddr count i,
ipc_receive_body_spec fromid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ipc_receive_body_spec fromid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ipc_receive_body_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H. subrewrite;
subdestruct; inv HQ;
try (refine_split´; trivial; fail).
exploit page_copy_back_exist; eauto.
intros (labd´ & Hmemcpy2 & Hmemcpy3).
rewrite Hmemcpy2.
exploit relate_impl_syncchpool_eq; eauto; intros.
refine_split´; trivial.
rewrite H.
eapply relate_impl_syncchpool_update.
assumption.
Qed.
Context {mt15: match_impl_abq}.
Context {mt16: match_impl_syncchpool}.
Context {mt1: match_impl_HP}.
Lemma ipc_receive_body_match:
∀ s d d´ m i f fromid rvaddr count,
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 ipc_receive_body_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update;
eapply page_copy_back_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) ipc_receive_body_spec}.
Context {inv2: PreservesInvariants (HD:= data0) ipc_receive_body_spec}.
Lemma ipc_receive_body_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ipc_receive_body_spec)
(id ↦ gensem ipc_receive_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit ipc_receive_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ipc_receive_body_match; eauto.
Qed.
End SYNCRECEIVE_CHAN.
Section SYNCSENDTO_CHAN.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_syncchpool}.
Context {re12: relate_impl_init}.
Context {re7: relate_impl_PT}.
Context {re9: relate_impl_ptpool}.
Context {re300: relate_impl_CPU_ID}.
Context {re10: relate_impl_HP}.
Context {re40: relate_impl_pperm}.
Context {re60: relate_impl_lock}.
Context {re30: relate_impl_multi_log}.
Lemma ipc_send_body_exist:
∀ s f habd habd´ labd chid vaddr count i,
ipc_send_body_spec chid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ipc_send_body_spec chid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ipc_send_body_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ.
eapply page_copy_exist in Hdestruct5; eauto.
destruct Hdestruct5 as (labd´ & Hpage & Hrel).
rewrite Hpage.
refine_split´; trivial.
exploit relate_impl_syncchpool_eq; eauto; intros. rewrite H.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {re13: match_impl_syncchpool}.
Context {mt1: match_impl_multi_log}.
Lemma ipc_send_body_match:
∀ s d d´ m chid vaddr count i f,
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 ipc_send_body_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update.
eapply page_copy_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) ipc_send_body_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ipc_send_body_spec}.
Lemma ipc_send_body_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ipc_send_body_spec)
(id ↦ gensem ipc_send_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ipc_send_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ipc_send_body_match; eauto.
Qed.
End SYNCSENDTO_CHAN.
Section GET_SYNC_CHAN_TO.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma get_sync_chan_to_exist:
∀ s f habd labd chid to,
get_sync_chan_to_spec chid habd = Some to
→ relate_AbData s f habd labd
→ get_sync_chan_to_spec chid labd = Some to.
Proof.
unfold get_sync_chan_to_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
Qed.
End GET_SYNC_CHAN_TO.
Section GET_SYNC_CHAN_COUNT.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma get_sync_chan_count_exist:
∀ s f habd labd chid count,
get_sync_chan_count_spec chid habd = Some count
→ relate_AbData s f habd labd
→ get_sync_chan_count_spec chid labd = Some count.
Proof.
unfold get_sync_chan_count_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
Qed.
End GET_SYNC_CHAN_COUNT.
Section GET_SYNC_CHAN_BUSY.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma get_sync_chan_busy_exist:
∀ s f habd labd chid busy,
get_sync_chan_busy_spec chid habd = Some busy
→ relate_AbData s f habd labd
→ get_sync_chan_busy_spec chid labd = Some busy.
Proof.
unfold get_sync_chan_busy_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
Qed.
Context {inv1: PreservesInvariants (HD:= data) get_sync_chan_busy_spec}.
Context {inv2: PreservesInvariants (HD:= data0) get_sync_chan_busy_spec}.
Lemma get_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem get_sync_chan_busy_spec)
(id ↦ gensem get_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_sync_chan_busy_exist; eauto. reflexivity.
Qed.
End GET_SYNC_CHAN_BUSY.
Section SET_SYNC_CHAN_TO.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_to_exist:
∀ s f habd habd´ labd chid to,
set_sync_chan_to_spec chid to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_to_spec chid to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_to_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_to_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_to_spec}.
End SET_SYNC_CHAN_TO.
Section SET_SYNC_CHAN_PADDR.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_paddr_exist:
∀ s f habd habd´ labd chid vaddr,
set_sync_chan_paddr_spec chid vaddr habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_paddr_spec chid vaddr labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_paddr_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_paddr_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_paddr_spec}.
End SET_SYNC_CHAN_PADDR.
Section SET_SYNC_CHAN_COUNT.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_count_exist:
∀ s f habd habd´ labd chid count,
set_sync_chan_count_spec chid count habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_count_spec chid count labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_count_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_count_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_count_spec}.
End SET_SYNC_CHAN_COUNT.
Section SET_SYNC_CHAN_BUSY.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_busy_exist:
∀ s f habd habd´ labd chid busy,
set_sync_chan_busy_spec chid busy habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_busy_spec chid busy labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_busy_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_busy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_busy_spec}.
Context {mt1: match_impl_syncchpool}.
Lemma set_sync_chan_busy_match:
∀ s d d´ m i n f,
set_sync_chan_busy_spec i n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_sync_chan_busy_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update. assumption.
Qed.
Lemma set_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem set_sync_chan_busy_spec)
(id ↦ gensem set_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_sync_chan_busy_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply set_sync_chan_busy_match; eauto.
Qed.
End SET_SYNC_CHAN_BUSY.
End OBJ_SIM.
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ _ c _ ⇒ Some (Int.unsigned c)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function get_sync_chan_to_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid to _ _ _ ⇒ Some (Int.unsigned to)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function get_sync_chan_paddr_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ vaddr _ _ ⇒ Some (Int.unsigned vaddr)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function get_sync_chan_busy_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ _ _ busy ⇒ Some (Int.unsigned busy)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_count_spec (i count: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid t v _ b
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid t v (Int.repr count) b)
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_to_spec (i to: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid _ v c b
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid (Int.repr to) v c b)
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_paddr_spec (i vaddr: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid t _ c b
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid t (Int.repr vaddr) c b)
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_sync_chan_busy_spec (i busy: Z) (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool adt) with
| SyncChanValid t v c _
⇒ Some (adt {syncchpool: ZMap.set i (SyncChanValid t v c (Int.repr busy))
(syncchpool adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function init_sync_chan_spec (i : Z) (adt : RData) : option RData :=
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i num_chan then
Some adt {syncchpool:
ZMap.set i (SyncChanValid (Int.repr num_chan) (Int.repr 0) (Int.repr 0) (Int.repr 0))
(syncchpool adt)}
else None
| _ ⇒ None
end.
Context `{real_params: RealParams}.
Context `{waittime: WaitTime}.
Function fifobbq_pool_init_spec (mbi_adr: Z) (adt: RData): option RData :=
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, 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} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde adt)}
{smspool: real_smspool (smspool adt)}
{abtcb: real_abtcb (abtcb adt)}
{abq: real_abq (abq adt)}
{syncchpool: real_syncchpool (syncchpool adt)}
else None
else None
| _ ⇒ None
end.
Function get_kernel_pa_spec (pid vaddr : Z) (adt : RData) : option Z :=
match pg adt with
| true ⇒ match ptRead_spec pid vaddr adt with
| Some paddr ⇒
if zeq paddr 0 then None else Some (paddr / PgSize × PgSize + (vaddr mod PgSize))
| _ ⇒ None
end
| _ ⇒ None
end.
Function ipc_receive_body_spec (chid vaddr rcount : Z) (adt : RData) : option (RData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid sender spaddr scount busy ⇒
let arecvcount := Z.min (Int.unsigned scount) rcount in
match page_copy_back_spec chid arecvcount vaddr adt with
| Some adt1 ⇒
Some (adt1 {syncchpool: ZMap.set chid
(SyncChanValid sender spaddr Int.zero busy)
(syncchpool adt1)}, arecvcount)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function ipc_send_body_spec (chid vaddr scount : Z) (adt : RData) : option (RData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid sender spaddr _ busy ⇒
let asendval := Z.min (scount) (1024) in
match page_copy_spec chid asendval vaddr adt with
| Some adt´ ⇒
Some (adt´ {syncchpool :
ZMap.set chid
(SyncChanValid sender spaddr (Int.repr asendval) busy)
(syncchpool adt´)}, asendval)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
End MULTIPROCESSOR.
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.
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}.
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.
Section GET_KERNEL_PA.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_PT}.
Context {re4: relate_impl_ptpool}.
Context {re5: relate_impl_init}.
Lemma get_kernel_pa_exist:
∀ s f habd labd va chid pa,
get_kernel_pa_spec chid va habd = Some pa
→ relate_AbData s f habd labd
→ get_kernel_pa_spec chid va labd = Some pa.
Proof.
unfold get_kernel_pa_spec in *; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_PT_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_init_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ.
erewrite ptRead_exist; eauto.
rewrite Hdestruct1; auto.
Qed.
End GET_KERNEL_PA.
Section FIFOBBQ_POOl_INIT.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_PT}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re10: relate_impl_smspool}.
Context {re11: relate_impl_abtcb}.
Context {re12: relate_impl_abq}.
Context {re13: relate_impl_cid}.
Context {re14: relate_impl_vmxinfo}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_ioapic}.
Context {re17: relate_impl_lapic}.
Context {re18: relate_impl_in_intr}.
Context {re30: relate_impl_syncchpool}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re20: relate_impl_multi_log}.
Lemma fifobbq_pool_init_exist:
∀ s f habd habd´ labd i,
fifobbq_pool_init_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fifobbq_pool_init_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold fifobbq_pool_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_idpde_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_abq_eq; eauto.
exploit relate_impl_abtcb_eq; eauto.
exploit relate_impl_vmxinfo_eq; eauto.
exploit relate_impl_smspool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_syncchpool_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.
revert H. subrewrite.
subdestruct.
inv HQ; refine_split´; trivial.
apply relate_impl_syncchpool_update.
apply relate_impl_abq_update.
apply relate_impl_abtcb_update.
apply relate_impl_smspool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_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_LAT_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_iflags}.
Context {mt2: match_impl_ipt}.
Context {mt3: match_impl_LAT}.
Context {mt4: match_impl_nps}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_PT}.
Context {mt7: match_impl_ptpool}.
Context {mt8: match_impl_idpde}.
Context {mt10: match_impl_smspool}.
Context {mt11: match_impl_abtcb}.
Context {mt12: match_impl_abq}.
Context {mt13: match_impl_cid}.
Context {mt14: match_impl_vmxinfo}.
Context {mt15: match_impl_AC}.
Context {mt50: match_impl_multi_log}.
Context {mt30: match_impl_syncchpool}.
Context {mt16: match_impl_ioapic}.
Context {mt17: match_impl_lapic}.
Lemma fifobbq_pool_init_match:
∀ s d d´ m i f,
fifobbq_pool_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold fifobbq_pool_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update.
eapply match_impl_abq_update.
eapply match_impl_abtcb_update.
eapply match_impl_smspool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_multi_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_LAT_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) fifobbq_pool_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) fifobbq_pool_init_spec}.
Lemma fifobbq_pool_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem fifobbq_pool_init_spec)
(id ↦ gensem fifobbq_pool_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit fifobbq_pool_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply fifobbq_pool_init_match; eauto.
Qed.
End FIFOBBQ_POOl_INIT.
Section SYNCRECEIVE_CHAN.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_syncchpool}.
Context {re8: relate_impl_abq}.
Context {re10: relate_impl_PT}.
Context {re11: relate_impl_ptpool}.
Context {re12: relate_impl_init}.
Context {re14: relate_impl_HP}.
Context {re15: relate_impl_pperm}.
Context {re300: relate_impl_CPU_ID}.
Context {re301: relate_impl_lock}.
Context {re302: relate_impl_multi_log}.
Lemma ipc_receive_body_exist:
∀ s f habd habd´ labd fromid vaddr count i,
ipc_receive_body_spec fromid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ipc_receive_body_spec fromid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ipc_receive_body_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H. subrewrite;
subdestruct; inv HQ;
try (refine_split´; trivial; fail).
exploit page_copy_back_exist; eauto.
intros (labd´ & Hmemcpy2 & Hmemcpy3).
rewrite Hmemcpy2.
exploit relate_impl_syncchpool_eq; eauto; intros.
refine_split´; trivial.
rewrite H.
eapply relate_impl_syncchpool_update.
assumption.
Qed.
Context {mt15: match_impl_abq}.
Context {mt16: match_impl_syncchpool}.
Context {mt1: match_impl_HP}.
Lemma ipc_receive_body_match:
∀ s d d´ m i f fromid rvaddr count,
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 ipc_receive_body_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update;
eapply page_copy_back_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) ipc_receive_body_spec}.
Context {inv2: PreservesInvariants (HD:= data0) ipc_receive_body_spec}.
Lemma ipc_receive_body_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem ipc_receive_body_spec)
(id ↦ gensem ipc_receive_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit ipc_receive_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ipc_receive_body_match; eauto.
Qed.
End SYNCRECEIVE_CHAN.
Section SYNCSENDTO_CHAN.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_syncchpool}.
Context {re12: relate_impl_init}.
Context {re7: relate_impl_PT}.
Context {re9: relate_impl_ptpool}.
Context {re300: relate_impl_CPU_ID}.
Context {re10: relate_impl_HP}.
Context {re40: relate_impl_pperm}.
Context {re60: relate_impl_lock}.
Context {re30: relate_impl_multi_log}.
Lemma ipc_send_body_exist:
∀ s f habd habd´ labd chid vaddr count i,
ipc_send_body_spec chid vaddr count habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ipc_send_body_spec chid vaddr count labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ipc_send_body_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ.
eapply page_copy_exist in Hdestruct5; eauto.
destruct Hdestruct5 as (labd´ & Hpage & Hrel).
rewrite Hpage.
refine_split´; trivial.
exploit relate_impl_syncchpool_eq; eauto; intros. rewrite H.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {re13: match_impl_syncchpool}.
Context {mt1: match_impl_multi_log}.
Lemma ipc_send_body_match:
∀ s d d´ m chid vaddr count i f,
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 ipc_send_body_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update.
eapply page_copy_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) ipc_send_body_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ipc_send_body_spec}.
Lemma ipc_send_body_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ipc_send_body_spec)
(id ↦ gensem ipc_send_body_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ipc_send_body_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ipc_send_body_match; eauto.
Qed.
End SYNCSENDTO_CHAN.
Section GET_SYNC_CHAN_TO.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma get_sync_chan_to_exist:
∀ s f habd labd chid to,
get_sync_chan_to_spec chid habd = Some to
→ relate_AbData s f habd labd
→ get_sync_chan_to_spec chid labd = Some to.
Proof.
unfold get_sync_chan_to_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
Qed.
End GET_SYNC_CHAN_TO.
Section GET_SYNC_CHAN_COUNT.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma get_sync_chan_count_exist:
∀ s f habd labd chid count,
get_sync_chan_count_spec chid habd = Some count
→ relate_AbData s f habd labd
→ get_sync_chan_count_spec chid labd = Some count.
Proof.
unfold get_sync_chan_count_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
Qed.
End GET_SYNC_CHAN_COUNT.
Section GET_SYNC_CHAN_BUSY.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma get_sync_chan_busy_exist:
∀ s f habd labd chid busy,
get_sync_chan_busy_spec chid habd = Some busy
→ relate_AbData s f habd labd
→ get_sync_chan_busy_spec chid labd = Some busy.
Proof.
unfold get_sync_chan_busy_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
Qed.
Context {inv1: PreservesInvariants (HD:= data) get_sync_chan_busy_spec}.
Context {inv2: PreservesInvariants (HD:= data0) get_sync_chan_busy_spec}.
Lemma get_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem get_sync_chan_busy_spec)
(id ↦ gensem get_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_sync_chan_busy_exist; eauto. reflexivity.
Qed.
End GET_SYNC_CHAN_BUSY.
Section SET_SYNC_CHAN_TO.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_to_exist:
∀ s f habd habd´ labd chid to,
set_sync_chan_to_spec chid to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_to_spec chid to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_to_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_to_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_to_spec}.
End SET_SYNC_CHAN_TO.
Section SET_SYNC_CHAN_PADDR.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_paddr_exist:
∀ s f habd habd´ labd chid vaddr,
set_sync_chan_paddr_spec chid vaddr habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_paddr_spec chid vaddr labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_paddr_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_paddr_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_paddr_spec}.
End SET_SYNC_CHAN_PADDR.
Section SET_SYNC_CHAN_COUNT.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_count_exist:
∀ s f habd habd´ labd chid count,
set_sync_chan_count_spec chid count habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_count_spec chid count labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_count_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_count_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_count_spec}.
End SET_SYNC_CHAN_COUNT.
Section SET_SYNC_CHAN_BUSY.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re5: relate_impl_syncchpool}.
Lemma set_sync_chan_busy_exist:
∀ s f habd habd´ labd chid busy,
set_sync_chan_busy_spec chid busy habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_sync_chan_busy_spec chid busy labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_sync_chan_busy_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; try (refine_split´; trivial; fail).
exploit relate_impl_syncchpool_eq; eauto; intros.
subrewrite´. refine_split´; trivial.
eapply relate_impl_syncchpool_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_sync_chan_busy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_sync_chan_busy_spec}.
Context {mt1: match_impl_syncchpool}.
Lemma set_sync_chan_busy_match:
∀ s d d´ m i n f,
set_sync_chan_busy_spec i n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_sync_chan_busy_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_syncchpool_update. assumption.
Qed.
Lemma set_sync_chan_busy_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem set_sync_chan_busy_spec)
(id ↦ gensem set_sync_chan_busy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_sync_chan_busy_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply set_sync_chan_busy_match; eauto.
Qed.
End SET_SYNC_CHAN_BUSY.
End OBJ_SIM.