Library mcertikos.objects.ObjSyncIPC
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 ASTExtra.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import LAsmModuleSemAux.
Require Export ObjTMVMM.
Require Export ObjTMSCHED.
Require Export ObjTMINTELVIRT.
Require Export ObjTMIPCDEVPRIM.
Require Import BigLogThreadConfigFunction.
Require Import SingleOracle.
Section OBJ_SyncIPC.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops: BigOracleOps}.
Context `{thread_conf_ops: ThreadsConfigurationOps}.
Function thread_syncsendto_chan_pre_spec (cv : Z) (adt : RData) : option RData :=
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
let chid := slp_q_id cv 0 in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 cv num_cv then
match big2_acquire_lock_SC_spec chid adt with
| Some adt0 ⇒
match ZMap.get chid (syncchpool adt0) with
| SyncChanValid t1 t2 t3 c ⇒
if Int.eq_dec c Int.zero then
Some (adt0 {syncchpool: ZMap.set chid (SyncChanValid t1 t2 t3 Int.one) (syncchpool adt0)})
else
match big2_thread_sleep_spec cv adt0 with
| Some adt1 ⇒
big2_acquire_lock_SC_spec chid adt1
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function thread_tryreceive_chan_spec (chanid vaddr rcount : Z) (adt : RData) : option (RData × Z) :=
let cpu := (CPU_ID adt) in
let chid := slp_q_id chanid 0 in
let sc_id := chid + lock_TCB_range in
match (init adt, pg adt, ikern adt, ihost adt, ipt adt,
B_inLock cpu (big_log adt)) with
| (true, true, true, true, true, true) ⇒
if zle_lt 0 chanid num_cv then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid _ _ _ c ⇒
if Int.eq_dec c Int.zero then
Some (adt, 0)
else
match thread_ipc_receive_body_spec chid vaddr rcount adt with
| Some (adt0, res0) ⇒
match big2_thread_wakeup_spec chanid adt0 with
| Some (adt1, res1) ⇒
if zeq res1 0 then
match ZMap.get chid (syncchpool adt1) with
| SyncChanValid t1 t2 t3 c´ ⇒
Some (adt1 {syncchpool: ZMap.set chid (SyncChanValid t1 t2 t3 Int.zero) (syncchpool adt1)}, res0)
| _ ⇒ None
end
else
if zle_le 0 res1 Int.max_unsigned then
Some (adt1, res0)
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function thread_syncreceive_chan_spec (chanid vaddr rcount : Z) (adt : RData) : option (RData × Z) :=
let cpu := (CPU_ID adt) in
let chid := slp_q_id chanid 0 in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
match big2_acquire_lock_SC_spec chid adt with
| Some adt0 ⇒
match thread_tryreceive_chan_spec chanid vaddr rcount adt0 with
| Some (adt1, res) ⇒
match big2_release_lock_SC_spec chid adt1 with
| Some adt2 ⇒
Some (adt2, res)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function thread_syncsendto_chan_spec (cv vaddr scount : Z) (adt : RData) : option (RData × Z) :=
let chid := slp_q_id cv 0 in
match thread_syncsendto_chan_pre_spec cv adt with
| Some adt0 ⇒
match thread_ipc_send_body_spec chid vaddr scount adt0 with
| Some (adt1, res) ⇒
match big2_release_lock_SC_spec chid adt1 with
| Some adt2 ⇒ Some (adt2, res)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End OBJ_SyncIPC.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops: BigOracleOps}.
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 `{thread_conf_ops: ThreadsConfigurationOps}.
Section THREAD_TRYRECEIVE_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_big_log}.
Context {re11: relate_impl_lock}.
Context {re13: relate_impl_big_oracle}.
Context {re15: relate_impl_HP}.
Context {re16: relate_impl_pperm}.
Context {re166: relate_impl_AC}.
Context {re603: relate_impl_init}.
Lemma thread_tryreceive_chan_exist:
∀ s f habd habd´ labd chanid vadr scount a,
thread_tryreceive_chan_spec chanid vadr scount habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_tryreceive_chan_spec chanid vadr scount labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_tryreceive_chan_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_AC_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_syncchpool_eq; eauto; intros.
exploit relate_impl_big_log_eq; eauto; intros.
exploit relate_impl_init_eq; eauto; intros.
revert H. subrewrite. subdestruct.
- ∃ labd. inv HQ. split; eauto.
- exploit thread_ipc_receive_body_exist; eauto. intros [ld0 [Hld0 rel0]]. rewrite Hld0.
exploit big2_thread_wakeup_exist; eauto. intros [ld1 [Hld1 rel1]]. rewrite Hld1.
subst.
rewrite zeq_true.
exploit relate_impl_syncchpool_eq; eauto; intros Hcvpool.
rewrite Hcvpool in Hdestruct13. rewrite Hdestruct13.
inv HQ. refine_split. reflexivity.
rewrite Hcvpool. eapply relate_impl_syncchpool_update; eauto.
- exploit thread_ipc_receive_body_exist; eauto. intros [ld0 [Hld0 rel0]]. rewrite Hld0.
exploit big2_thread_wakeup_exist; eauto. intros [ld1 [Hld1 rel1]]. rewrite Hld1; subst.
rewrite Hdestruct12. rewrite Hdestruct13.
inv HQ. ∃ ld1. split; eauto.
Qed.
Context {mt2: match_impl_syncchpool}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Lemma thread_tryreceive_chan_match:
∀ s d d´ m f chanid vadr scount a,
thread_tryreceive_chan_spec chanid vadr scount d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_tryreceive_chan_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_syncchpool_update; eauto.
eapply big2_thread_wakeup_match. eapply Hdestruct10.
eapply thread_ipc_receive_body_match. eapply Hdestruct8. eauto.
- eapply big2_thread_wakeup_match. eapply Hdestruct10.
eapply thread_ipc_receive_body_match. eapply Hdestruct8. eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_tryreceive_chan_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_tryreceive_chan_spec}.
Lemma thread_tryreceive_chan_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_tryreceive_chan_spec)
(id ↦ gensem thread_tryreceive_chan_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit thread_tryreceive_chan_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_tryreceive_chan_match; eauto.
Qed.
End THREAD_TRYRECEIVE_CHAN.
Section THREAD_SYNCRECEIVE_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_big_log}.
Context {re11: relate_impl_lock}.
Context {re13: relate_impl_big_oracle}.
Context {re15: relate_impl_HP}.
Context {re16: relate_impl_pperm}.
Context {re166: relate_impl_AC}.
Lemma thread_syncreceive_chan_exist:
∀ s f habd habd´ labd chanid vadr scount a,
thread_syncreceive_chan_spec chanid vadr scount habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_syncreceive_chan_spec chanid vadr scount labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_syncreceive_chan_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_AC_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite. subdestruct.
- exploit big2_acquire_lock_SC_exist; eauto. intros [ld0 [Hld0 rel0]]. rewrite Hld0.
exploit thread_tryreceive_chan_exist; eauto. intros [ld1 [Hld1 rel1]]. rewrite Hld1.
exploit big2_release_lock_SC_exist; eauto. intros [ld2 [Hld2 rel2]]. rewrite Hld2.
inv HQ. ∃ ld2. split; eauto.
Qed.
Context {mt1: match_impl_abq}.
Context {mt2: match_impl_syncchpool}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt6: match_impl_lock}.
Lemma thread_syncreceive_chan_match:
∀ s d d´ m f chanid vadr scount a,
thread_syncreceive_chan_spec chanid vadr scount d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_syncreceive_chan_spec; intros.
subdestruct; inv H; trivial.
- eapply big2_release_lock_SC_match. eapply Hdestruct6.
eapply thread_tryreceive_chan_match. eapply Hdestruct4.
eapply big2_acquire_lock_SC_match. eapply Hdestruct3. eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_syncreceive_chan_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_syncreceive_chan_spec}.
Lemma thread_syncreceive_chan_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_syncreceive_chan_spec)
(id ↦ gensem thread_syncreceive_chan_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit thread_syncreceive_chan_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_syncreceive_chan_match; eauto.
Qed.
End THREAD_SYNCRECEIVE_CHAN.
Section THREAD_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_big_log}.
Context {re11: relate_impl_lock}.
Context {re13: relate_impl_big_oracle}.
Context {re500: relate_impl_intr_flag}.
Context {re501: relate_impl_in_intr}.
Context {re600: relate_impl_lock}.
Context {re601: relate_impl_init}.
Context {re602: relate_impl_AC}.
Context {re603: relate_impl_init}.
Context {re604: relate_impl_trapinfo}.
Context {re605: relate_impl_pperm}.
Context {re606: relate_impl_HP}.
Lemma thread_syncsendto_chan_pre_exist:
∀ s f habd habd´ labd chid,
thread_syncsendto_chan_pre_spec chid habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_syncsendto_chan_pre_spec chid labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_syncsendto_chan_pre_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.
- exploit big2_acquire_lock_SC_exist; eauto. intros [ld0 [Hld0 Hrel0]]. rewrite Hld0.
exploit relate_impl_syncchpool_eq; eauto; intros Hcvpool. rewrite Hcvpool in Hdestruct5.
rewrite Hdestruct5.
rewrite Hdestruct6.
refine_split. reflexivity.
inv HQ.
rewrite Hcvpool. eapply relate_impl_syncchpool_update. assumption.
- exploit big2_acquire_lock_SC_exist. eapply Hdestruct4. eassumption. intros [ld0 [Hld0 Hrel0]]. rewrite Hld0.
exploit relate_impl_syncchpool_eq; eauto; intros Hcvpool. rewrite Hcvpool in Hdestruct5.
rewrite Hdestruct5.
rewrite Hdestruct6.
exploit big2_thread_sleep_exist; eauto.
intros [ld1 [Hld1 Hrel1]]. rewrite Hld1.
exploit big2_acquire_lock_SC_exist. eapply HQ. eassumption. intros [ld2 [Hld2 Hrel2]]. rewrite Hld2.
∃ ld2. split; auto.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt3: match_impl_lock}.
Context {mt4: match_impl_big_log}.
Lemma thread_syncsendto_chan_pre_match:
∀ s d d´ m chid f,
thread_syncsendto_chan_pre_spec chid d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_syncsendto_chan_pre_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_syncchpool_update.
exploit big2_acquire_lock_SC_match. eapply Hdestruct4. eassumption. eauto.
- exploit big2_acquire_lock_SC_match. eapply Hdestruct4. eassumption. intros.
exploit big2_thread_sleep_match. eapply Hdestruct7. eassumption. intros.
exploit big2_acquire_lock_SC_match. eapply H2. eassumption. eauto.
Qed.
Section THREAD_PRE.
Context {inv: PreservesInvariants (HD:= data) thread_syncsendto_chan_pre_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_syncsendto_chan_pre_spec}.
Lemma thread_syncsendto_chan_pre_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_syncsendto_chan_pre_spec)
(id ↦ gensem thread_syncsendto_chan_pre_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_syncsendto_chan_pre_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_syncsendto_chan_pre_match; eauto.
Qed.
End THREAD_PRE.
Lemma thread_syncsendto_chan_exist:
∀ s f habd habd´ labd chid vadr scount a,
thread_syncsendto_chan_spec chid vadr scount habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, thread_syncsendto_chan_spec chid vadr scount labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold thread_syncsendto_chan_spec. intros.
subdestruct; inv H; trivial.
exploit thread_syncsendto_chan_pre_exist; eauto. intros [ld0 [Hld0 rel0]]. rewrite Hld0.
exploit thread_ipc_send_body_exist; eauto. intros [ld1 [Hld1 rel1]]. rewrite Hld1.
exploit big2_release_lock_SC_exist; eauto. intros [ld2 [Hld2 rel2]]. rewrite Hld2.
∃ ld2. split; auto.
Qed.
Lemma thread_syncsendto_chan_match:
∀ s d d´ m f chid vadr scount a,
thread_syncsendto_chan_spec chid vadr scount d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_syncsendto_chan_spec; intros.
subdestruct; inv H; trivial.
- eapply big2_release_lock_SC_match; eauto.
eapply thread_ipc_send_body_match; eauto.
eapply thread_syncsendto_chan_pre_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) thread_syncsendto_chan_spec}.
Context {inv2: PreservesInvariants (HD:= data0) thread_syncsendto_chan_spec}.
Lemma thread_syncsendto_chan_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_syncsendto_chan_spec)
(id ↦ gensem thread_syncsendto_chan_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit thread_syncsendto_chan_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_syncsendto_chan_match; eauto.
Qed.
End THREAD_SYNCSENDTO_CHAN.
End OBJ_SIM.