Library mcertikos.proc.QThreadGen
This file provide the contextual refinement proof between PQueueIntro layer and PQueueInit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem2.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LAsmModuleSemAux.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import PQThread.
Require Import PThread.
Require Export QThreadGenDef.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem2.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LAsmModuleSemAux.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import PQThread.
Require Import PThread.
Require Export QThreadGenDef.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pqthread_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pthread_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Require Import CalRealProcModule.
Inductive relate_tcb: MultiLogPool → AbTCBPool → AbQueuePool→ Sleeper → ZMap.t Z → Prop :=
| RELATE_TCB_INTRO:
∀ bl t´ q´ s´ c´
(Hpre: ∀ l t q slp cache res curid
(Hlog: ZMap.get lock_range bl = MultiDef l)
(Hcal: CalTCB_log l = Some (t, q, slp, curid, cache, res)),
slp = ZMap.get current_CPU_ID s´
∧ curid = ZMap.get current_CPU_ID c´
∧ t = t´
∧ q = q´),
relate_tcb bl t´ q´ s´ c´.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pqthread_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pthread_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Require Import CalRealProcModule.
Inductive relate_tcb: MultiLogPool → AbTCBPool → AbQueuePool→ Sleeper → ZMap.t Z → Prop :=
| RELATE_TCB_INTRO:
∀ bl t´ q´ s´ c´
(Hpre: ∀ l t q slp cache res curid
(Hlog: ZMap.get lock_range bl = MultiDef l)
(Hcal: CalTCB_log l = Some (t, q, slp, curid, cache, res)),
slp = ZMap.get current_CPU_ID s´
∧ curid = ZMap.get current_CPU_ID c´
∧ t = t´
∧ q = q´),
relate_tcb bl t´ q´ s´ c´.
Relation between raw data at two layers
Record relate_RData (f: meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
AC_re: AC hadt = AC ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
LAT_re: LAT hadt = LAT ladt;
nps_re: nps hadt = nps ladt;
init_re: init hadt = init ladt;
pperm_re: pperm hadt = pperm ladt;
PT_re: PT hadt = PT ladt;
ptp_re: ptpool hadt = ptpool ladt;
idpde_re: idpde hadt = idpde ladt;
ipt_re: ipt hadt = ipt ladt;
smspool_re: smspool hadt = smspool ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
multi_oracle_re: relate_Thread_Oracle_Pool (multi_oracle hadt) (multi_oracle ladt);
multi_log_re: relate_Thread_Log_Pool (multi_log hadt) (multi_log ladt);
lock_re: ∀ i, ZMap.get i (lock hadt) = ZMap.get i (lock ladt);
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt;
kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
syncchpool_re: syncchpool hadt = syncchpool ladt;
abtcb_re: relate_tcb (multi_log hadt) (abtcb ladt)
(abq ladt) (sleeper ladt) (cid ladt)
}.
Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
| MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.
Local Hint Resolve MATCH_RDATA.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
AC_re: AC hadt = AC ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
LAT_re: LAT hadt = LAT ladt;
nps_re: nps hadt = nps ladt;
init_re: init hadt = init ladt;
pperm_re: pperm hadt = pperm ladt;
PT_re: PT hadt = PT ladt;
ptp_re: ptpool hadt = ptpool ladt;
idpde_re: idpde hadt = idpde ladt;
ipt_re: ipt hadt = ipt ladt;
smspool_re: smspool hadt = smspool ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
multi_oracle_re: relate_Thread_Oracle_Pool (multi_oracle hadt) (multi_oracle ladt);
multi_log_re: relate_Thread_Log_Pool (multi_log hadt) (multi_log ladt);
lock_re: ∀ i, ZMap.get i (lock hadt) = ZMap.get i (lock ladt);
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt;
kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
syncchpool_re: syncchpool hadt = syncchpool ladt;
abtcb_re: relate_tcb (multi_log hadt) (abtcb ladt)
(abq ladt) (sleeper ladt) (cid ladt)
}.
Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
| MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.
Local Hint Resolve MATCH_RDATA.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := nil
}.
Prove that after taking one step, the refinement relation still holds
Lemma relate_incr:
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
- eapply kctxt_inj_incr; eauto.
Qed.
End Rel_Property.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
- eapply kctxt_inj_incr; eauto.
Qed.
End Rel_Property.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
eapply relate_incr; eauto.
Qed.
Section Exists.
Require Import TacticsForTesting.
Lemma lock_max:
∀ i ofs r,
index2Z i ofs = Some r →
r < lock_range.
Proof.
unfold lock_range.
intros. functional inversion H; subst.
functional inversion H1; subst.
- unfold ID_AT_range in ×.
functional inversion H2; subst.
unfold ID_TCB_range, ID_SC_range. omega.
- functional inversion H2; subst.
unfold ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
- functional inversion H2; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
Qed.
Lemma lock_neq:
∀ i ofs r,
index2Z i ofs = Some r →
lock_range ≠ r.
Proof.
intros. exploit lock_max; eauto.
intros. omega.
Qed.
Lemma lock_re_gss:
∀ (l1 l2: Lock)
(lock_re0 : ∀ i0, ZMap.get i0 l1 = ZMap.get i0 l2) k ofs,
(∀ i0,
ZMap.get i0 (ZMap.set ofs k l1) =
ZMap.get i0 (ZMap.set ofs k l2)).
Proof.
intros. destruct (zeq i0 ofs); subst.
{
repeat rewrite ZMap.gss; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
}
Qed.
Lemma lock_re_gss´:
∀ (l1 l2: Lock)
(lock_re0 : ∀ i0, ZMap.get i0 l1 = ZMap.get i0 l2) k ofs
(lock_eq: ZMap.get ofs l2 = k),
(∀ i0, ZMap.get i0 l1 =
ZMap.get i0 (ZMap.set ofs k l2)).
Proof.
intros. destruct (zeq i0 ofs); subst.
{
repeat rewrite ZMap.gss; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
}
Qed.
Lemma TCB_range_neq:
∀ i ofs r i0,
0 ≤ i0 < num_chan →
i ≠ ID_TCB →
index2Z i ofs = Some r →
i0 + ID_AT_range ≠ r.
Proof.
intros. functional inversion H1.
functional inversion H3; subst.
- unfold ID_AT_range in ×.
functional inversion H4; subst. omega.
- omega.
- functional inversion H4; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
Qed.
Lemma relate_Thread_Log_Pool_gso:
∀ i ofs r hl ll l0,
relate_Thread_Log_Pool hl ll →
i ≠ ID_TCB →
index2Z i ofs = Some r →
relate_Thread_Log_Pool (ZMap.set r l0 hl) (ZMap.set r l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r0 r); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
repeat rewrite ZMap.gso; eauto.
+ eapply TCB_range_neq; eauto. omega.
+ eapply lock_neq; eauto.
Qed.
Local Transparent H_CalLock.
Lemma MultiLogMap2id_imply_HCal:
∀ l_high l_low id
(Hlog: MultiLogMap2id l_high id l_low),
∃ self_c, H_CalLock l_low = Some (self_c, LEMPTY, None).
Proof.
induction l_high; simpl; intros.
- inv Hlog. simpl; eauto.
- inv Hlog. eapply IHl_high in Hbig.
destruct Hbig as (x & Hcal).
inv Hrel_e; simpl; eauto; rewrite Hcal.
repeat rewrite zeq_true; simpl; repeat rewrite zeq_true; eauto.
Qed.
Lemma MultiLogMap2id_imply_HCal_wait:
∀ n cpu l_high l_low id
(Hlog: MultiLogMap2id l_high id l_low)
(Hn: n ≠ O),
∃ x, H_CalLock (TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK n)) :: l_low) = Some x.
Proof.
intros. eapply MultiLogMap2id_imply_HCal in Hlog.
destruct Hlog as (self_c & Hcal).
simpl. rewrite Hcal. rewrite zeq_true.
destruct n; eauto. elim Hn; eauto.
Qed.
Lemma H_CalLock_rel:
∀ t q l cpu x
(Hcal: H_CalLock (TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l) = Some x),
∃ y, H_CalLock (TEVENT cpu (TTICKET REL_LOCK)
:: TEVENT cpu (TSHARED (OABTCBE t q))
:: TEVENT cpu (TSHARED OPULL)
:: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l) = Some y.
Proof.
simpl; intros. subdestruct; inv Hcal.
repeat rewrite zeq_true. eauto.
Qed.
Local Opaque H_CalLock.
Ltac subdestruct_match term:=
match term with
| context[match ?con with |_ ⇒ _ end] ⇒
progress subdestruct_if con
| _ ⇒
let H := fresh "Hdestruct" in
destruct term eqn: H; contra_inv
end.
Ltac subdestruct_match_one:=
match goal with
| [ HT: context[match ?con with |_ ⇒ _ end] |- _] ⇒ subdestruct_match con; simpl in HT
end; simpl.
Lemma CalTCB_log_real_cons:
∀ l x e
(Hcal: CalTCB_log_real (e::l) = Some x),
∃ y, CalTCB_log_real l = Some y.
Proof.
unfold CalTCB_log_real. simpl; intros.
unfold CalTCB_log in ×. simpl; intros. simpl in Hcal.
destruct e. simpl in Hcal.
subdestruct_match_one.
repeat destruct p; eauto.
Qed.
Lemma RData_update_tcb:
∀ a t q,
t = abtcb a →
q = abq a →
a = a {abtcb : t} {abq : q}.
Proof.
intros. unfold update_cid. subst.
destruct a; trivial.
Qed.
Lemma append_rewrite {A: Type}:
∀ (a: A) l,
a :: l = (a::nil) ++ l.
Proof.
simpl. trivial.
Qed.
Lemma append_rewrite3 {A: Type}:
∀ (a b c: A) l,
a :: b :: c :: l = (a::b::c::nil) ++ l.
Proof.
simpl. trivial.
Qed.
Lemma msg_range_neq:
∀ i ofs r i0 n,
0 ≤ i0 < num_chan →
i ≠ ID_TCB →
index2Z i ofs = Some r →
0 ≤ n < 8 →
r ≠ msg_q_id n + ID_AT_range.
Proof.
intros. functional inversion H1.
functional inversion H4; subst.
- unfold ID_AT_range in ×.
functional inversion H5; subst.
unfold msg_q_id. omega.
- omega.
- functional inversion H5; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
unfold msg_q_id. omega.
Qed.
Lemma slpq_id_neq_lock_range:
∀ n (Hr: 0 ≤ n < num_cv),
lock_range ≠ slp_q_id n 0 + lock_TCB_range.
Proof.
unfold slp_q_id. intros.
unfold lock_range, lock_TCB_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range.
omega.
Qed.
Lemma slpq_id_neq_rdq:
∀ n (Hr: 0 ≤ n < num_cv),
rdy_q_id current_CPU_ID ≠ slp_q_id n 0.
Proof.
unfold slp_q_id, rdy_q_id. intros.
pose proof current_CPU_ID_range.
omega.
Qed.
Lemma add_aux:
∀ (a b c: Z),
a ≠ b →
a + c ≠ b + c.
Proof.
intros. omega.
Qed.
Lemma msg_neq:
∀ n,
rdy_q_id n ≠ msg_q_id n.
Proof.
intros.
unfold rdy_q_id, msg_q_id. omega.
Qed.
Lemma list_append_eq:
∀ {A: Type} (a b: A) l1 l2 l3
(Hn : a ≠ b)
(Hl1 : l1 ++ a :: l2 = b :: l3),
In b l1.
Proof.
intros. destruct l1; subst.
- inv Hl1. elim Hn; trivial.
- inv Hl1. left; trivial.
Qed.
Lemma relate_Thread_Log_Pool_gss:
∀ gl sl gl0 gl1 sl0 n (Hrel: relate_Thread_Log_Pool gl sl)
(Hrelm: relate_Thread_Log_Type (MultiDef gl0) n (MultiDef sl0))
(Hn: 0 ≤ n < num_chan)
(Hgl: ZMap.get lock_range gl = MultiDef gl1)
(Hmulti: ∀ i l, i ≠ n → relate_Thread_Log gl1 i l → relate_Thread_Log gl0 i l),
relate_Thread_Log_Pool (ZMap.set lock_range (MultiDef gl0) gl)
(ZMap.set (n + ID_AT_range) (MultiDef sl0) sl).
Proof.
intros. inv Hrel. econstructor.
- intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H0; eauto.
eapply lock_neq in H0; eauto.
- intros. rewrite ZMap.gss.
destruct (zeq i n); subst.
+ rewrite ZMap.gss. eauto.
+ rewrite ZMap.gso; eauto.
× inv Hrelm. exploit Hdiff; eauto.
erewrite Hgl. intros HF. inv HF.
constructor. eauto.
× eapply add_aux; eauto.
Qed.
Lemma MultiLogMap2id_get_shared:
∀ l1 l2 id t q slp cache res curid
(Hmulti: MultiLogMap2id l1 id l2)
(Hcal: CalTCB_log l1 = Some (t, q, slp, curid, cache, res)),
GetSharedABTCB l2 = ZMap.get id cache.
Proof.
induction l1; simpl; intros.
- inv Hmulti. inv Hcal.
rewrite ZMap.gi. trivial.
- destruct a. pose proof Hcal as Hcal_t.
unfold CalTCB_log in Hcal. simpl in Hcal.
subdestruct_match_one.
destruct p as (((((t0 & q0) & slp0) & curid0) & cache0) & res0).
inv Hmulti. inv Hrel_e.
+ simpl. subdestruct; inv Hcal; eauto.
+ simpl. inv Hsome.
destruct e; inv H0.
destruct e; inv H1.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
+ simpl. rewrite Hcal0 in Hcal_t. inv Hcal_t. inv Hsome.
destruct e; inv H0.
destruct e; inv H1.
× repeat subdestruct_match_one; inv Hcal; eauto.
× repeat subdestruct_match_one; inv Hcal; eauto.
× repeat subdestruct_match_one; inv Hcal; eauto.
× repeat subdestruct_match_one; inv Hcal; eauto.
Qed.
Lemma CalTCB_log_gso:
∀ l l´ t q s curid cached res
(Hlog: ∀ e cpu,
In (TEVENT cpu e) l → cpu ≠ current_CPU_ID)
(Hcal: CalTCB_log (l ++ l´) = Some (t, q, s, curid, cached, res)),
∃ cached´ res´, CalTCB_log l´ = Some (t, q, s, curid, cached´, res´).
Proof.
induction l; simpl; intros; eauto.
unfold CalTCB_log in Hcal. simpl in Hcal.
destruct a.
assert (Hneq: i ≠ current_CPU_ID).
{
eapply Hlog. left; trivial.
}
assert (Hcal´: ∃ cached´ res´,
CalTCB_log (l ++ l´) = Some (t, q, s, curid, cached´, res´)).
{
subdestruct_match_one.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1).
unfold CalTCB_log. rewrite Hdestruct. clear Hdestruct.
destruct e.
- inv Hcal. eauto.
- destruct e; try (inv Hcal; eauto; fail).
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
}
destruct Hcal´ as (cache´ & res´ & Hcal´).
eapply IHl; eauto.
Qed.
Lemma CalTCB_log_gso´:
∀ l t q s curid cached res habd
(Hhigh: PQThread.high_level_invariant habd)
(Hcal: CalTCB_log ((ZMap.get lock_range (multi_oracle habd) current_CPU_ID l) ++ l) =
Some (t, q, s, curid, cached, res)),
∃ cached´ res´, CalTCB_log l = Some (t, q, s, curid, cached´, res´).
Proof.
intros. eapply CalTCB_log_gso in Hcal; eauto.
eapply valid_big_oracle; eauto.
Qed.
Section INIT.
Require Import CalTicketLock.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealPTPool.
Require Import CalRealSMSPool.
Require Import DeviceStateDataType.
Lemma real_lock__pb_re:
∀ n l1 l2
(Hrel: ∀ i, ZMap.get i l1 = ZMap.get i l2),
(∀ i,
ZMap.get i (real_lock_pb n l1) = ZMap.get i (real_lock_pb n l2)).
Proof.
induction n; simpl; intros; trivial.
destruct (zeq i (Z.of_nat n)); subst; trivial.
- repeat rewrite ZMap.gss; trivial.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_multi_log_gss:
∀ i l (Hrange: 0 ≤ i < lock_range),
ZMap.get i (real_multi_log l) = MultiDef nil.
Proof.
unfold real_multi_log. intros.
replace i with (Z.of_nat (Z.to_nat i)).
- rewrite real_multi_log_pb_in. trivial. xomega.
- xomega.
Qed.
Lemma real_multi_log_gss´:
∀ i l (Hrange: 0 ≤ i ≤ lock_range),
ZMap.get i (real_multi_log´ l) = MultiDef nil.
Proof.
unfold real_multi_log´. intros.
replace i with (Z.of_nat (Z.to_nat i)).
- rewrite real_multi_log_pb_in. trivial. xomega.
- xomega.
Qed.
Lemma index2Z_range:
∀ i ofs r,
index2Z i ofs = Some r →
0 ≤ r < lock_range.
Proof.
split.
- functional inversion H; subst.
functional inversion H1; subst.
+ unfold ID_AT_range in ×.
functional inversion H2; subst. omega.
+ functional inversion H2; subst.
unfold ID_AT_range. omega.
+ functional inversion H2; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
- eapply lock_max; eauto.
Qed.
Opaque real_multi_log´ real_multi_log real_vmxinfo real_LAT real_nps
real_pt real_idpde real_smspool real_abq real_syncchpool.
Lemma real_multi_log_eq:
∀ i ofs r l1 l2,
i ≠ 1 →
index2Z i ofs = Some r →
ZMap.get r (real_multi_log´ l1) = ZMap.get r (real_multi_log l2).
Proof.
intros. eapply index2Z_range in H0.
rewrite (real_multi_log_gss _ l2 H0).
assert (Hr: 0 ≤ r ≤ lock_range) by omega.
rewrite (real_multi_log_gss´ _ l1 Hr).
trivial.
Qed.
Lemma lock_range_r:
0 ≤ lock_range ≤ lock_range.
Proof.
unfold lock_range, lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
Qed.
Lemma real_multi_log_rel:
∀ i l1 l2,
MSG_Q_START ≤ i < num_chan →
relate_Thread_Log_Type (ZMap.get lock_range (real_multi_log´ l1)) i
(ZMap.get (i + ID_AT_range) (real_multi_log l2)).
Proof.
intros.
rewrite (real_multi_log_gss´ _ l1 lock_range_r).
assert (Hr´: 0 ≤ i + ID_AT_range < lock_range).
{
unfold lock_range, lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
}
rewrite (real_multi_log_gss _ l2 Hr´).
econstructor; eauto. econstructor; eauto.
instantiate (1:= nil). constructor. simpl. trivial.
Qed.
Lemma big_sched_init_exist:
∀ s habd habd´ labd mbi_adr
(Hhigh: PQThread.high_level_invariant habd)
(Hlow: PThread.high_level_invariant labd)f,
biglow_sched_init_spec mbi_adr habd = Some habd´
→ relate_AbData s f habd labd
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, sched_init_spec mbi_adr labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_sched_init_spec, sched_init_spec.
intros until f; intros HP HR Hincr.
pose proof HR as HR´. inv HR´.
revert HP.
rewrite init_re0, pg_re0, ikern_re0, ihost_re0, ipt_re0, in_intr_re0, ioapic_re0, lapic_re0, LAT_re0,
idpde_re0, smspool_re0, syncchpool_re0.
intros.
subdestruct; inv HP; simpl.
assert(∀ i : ZIndexed.t,
ZMap.get i (real_lock (lock habd)) = ZMap.get i (real_lock (lock labd))).
{
unfold real_lock. eapply real_lock__pb_re; eauto.
}
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv Hhigh; assumption.
}
refine_split´; trivial.
Ltac simpl_tac :=
match goal with
| |- ?a = ?a ⇒ reflexivity
| H: ?X |- ?X ⇒ exact H
| H: ?a = ?b |- ?b = ?a ⇒ rewrite H; reflexivity
| _ ⇒ try congruence
end.
econstructor; simpl; simpl_tac.
{
econstructor.
- intros. eapply real_multi_log_eq; eauto.
- intros. eapply real_multi_log_rel; eauto.
}
{
econstructor. intros.
rewrite (real_multi_log_gss´ _ (multi_log habd) lock_range_r) in Hlog.
inv Hlog. unfold CalTCB_log in Hcal; simpl in Hcal. inv Hcal.
refine_split´.
{
inv Hlow; symmetry; eauto.
}
{
symmetry.
eapply real_valid_cidpool.
apply current_CPU_ID_range.
}
{
rewrite HCPU.
inv Hlow; eauto.
rewrite <- valid_init_abtcb; eauto.
}
{
inv Hlow.
rewrite (valid_init_abq Hdestruct0); reflexivity.
}
}
Qed.
End INIT.
Section SLEEP.
Lemma remove_cache_event_gso:
∀ l l´ cid
(Hgso: ∀ e cid´,
In (TEVENT cid´ e) l → cid´ ≠ cid),
remove_cache_event (l ++ l´) cid
= remove_cache_event (l´) cid.
Proof.
induction l; simpl; eauto; intros.
destruct a; eauto.
rewrite zeq_false; eauto.
Qed.
Lemma remove_cache_event_gss:
∀ bl0 i,
remove_cache_event (remove_cache_event bl0 i) i =
remove_cache_event bl0 i.
Proof.
intros.
induction bl0.
reflexivity.
simpl.
destruct a.
destruct (zeq i0 i).
simpl.
destruct (zeq i0 i); try congruence.
assumption.
Qed.
Lemma remove_cache_event_eq:
∀ i bl0 labd,
PThread.high_level_invariant labd →
MSG_Q_START ≤ i < num_chan →
remove_cache_event(ZMap.get (i + ID_AT_range) (multi_oracle labd) current_CPU_ID
(remove_cache_event bl0 current_CPU_ID) ++
remove_cache_event bl0 current_CPU_ID) current_CPU_ID = remove_cache_event bl0 current_CPU_ID.
Proof.
intros.
erewrite remove_cache_event_gso; eauto.
eapply remove_cache_event_gss.
inv H.
unfold valid_multi_oracle_pool_H1 in valid_multi_oracle_pool_inv.
unfold valid_multi_oracle_domain in valid_multi_oracle_pool_inv.
exploit (valid_multi_oracle_pool_inv ID_TCB i ((i + ID_AT_range))); eauto.
Opaque Z.add.
unfold index2Z1; simpl.
rewrite zle_lt_true.
f_equal.
omega.
unfold ID_TCB_range.
omega.
intros (valid_oracle & valid_hqueue).
intros.
exploit valid_oracle; eauto.
intro tmp; destruct tmp; assumption.
Qed.
Lemma big_thread_sleep_exist:
∀ habd habd´ labd rs r´ rs0 n s
(HINV: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd) f,
biglow_thread_sleep_spec
habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) n = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t,
val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
→ ∃ labd´ r´0 ofs, thread_sleep_spec
labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
#EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) n = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r,
ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = r´0.
Proof.
Opaque remove.
generalize max_unsigned_val; intro muval.
unfold thread_sleep_spec, biglow_thread_sleep_spec; intros until f.
intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
specialize (PQThread.CPU_ID_range _ HINV).
specialize (PQThread.valid_curid _ HINV).
subrewrite´. intros HCPU_range Hcid Hinv. subdestruct; contra_inv;
inv Hinv.
assert (HOS1: MSG_Q_START ≤ (slp_q_id n 0) < num_chan).
{
unfold slp_q_id. omega.
}
assert (HOS2: 0 ≤ (slp_q_id n 0) < num_chan) by omega.
pose proof multi_log_re0 as Hrel_log´.
inv multi_log_re0. specialize (Hdiff _ HOS1).
rewrite Hdestruct7 in Hdiff. inv Hdiff.
pose proof multi_oracle_re0 as Hrel_oracle´.
inv multi_oracle_re0. specialize (Hdiff _ HOS1).
inv Hdiff. exploit (Hpre (CPU_ID labd)); eauto.
intros Hrel_log_oracle.
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv HINV; assumption.
}
rewrite HCPU in ×.
inv abtcb_re0.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound. omega.
}
intros (x & Hcal´). rename Hdestruct12 into Hcal_tcb´.
unfold CalTCB_log_real in Hcal_tcb´.
subdestruct_one. inv Hcal_tcb´.
destruct p0 as (((((t1 & q1) & s1) & curid1) & cached1) & res1).
assert (Hslpq_r: 16 ≤ slp_q_id n 0 < num_chan).
{
unfold slp_q_id. omega.
}
rewrite zle_lt_true; trivial.
inv H1.
unfold enqueue_atomic_spec.
generalize Hdestruct11; intro tcbinv.
unfold CalTCB_log in tcbinv; simpl in tcbinv.
subdestruct_match_one.
destruct p0 as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (Hacq: ∃ t_lock q_lock,
acquire_lock_ABTCB_spec (slp_q_id n 0) labd =
Some (labd
{multi_log
: ZMap.set (slp_q_id n 0 + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID
(TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get (slp_q_id n 0 + ID_AT_range)
(multi_oracle labd) current_CPU_ID l2 ++ l2))
(multi_log labd)}
{lock : ZMap.set (slp_q_id n 0 + ID_AT_range) (LockOwn true) (lock labd)}
{abtcb : t_lock} {abq : q_lock})
∧ (t_lock, q_lock) = match ZMap.get (slp_q_id n 0) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (t2, q2)
end
∧ ZMap.get current_CPU_ID (sleeper labd) = s2
∧ ZMap.get current_CPU_ID (cid labd) = curid2).
{
assert (Hlock: ZMap.get (slp_q_id n 0 + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
unfold acquire_lock_ABTCB_spec.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite <- H.
rewrite Hcal´. simpl.
erewrite MultiLogMap2id_get_shared; eauto.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
destruct (ZMap.get (slp_q_id n 0) cached2) eqn: Hcache.
- destruct p0.
refine_split´; eauto.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock & q_lock & → & Htq_eq & Hsleep´ & Hcid´).
assert (Hneq1: slp_q_id n 0 + lock_TCB_range ≠ slp_q_id n 0 + ID_AT_range).
{
unfold lock_TCB_range. unfold ID_TCB_range. omega.
}
assert (Heq1: index2Z 2 (slp_q_id n 0) = Some (slp_q_id n 0 + lock_TCB_range)).
{
unfold index2Z. unfold index_range. unfold index_incrange.
rewrite zle_lt_true; eauto. f_equal. omega.
}
assert (Hneq3: lock_range ≠ slp_q_id n 0 + lock_TCB_range).
{
eapply slpq_id_neq_lock_range; eauto.
}
assert (Hneq2: rdy_q_id current_CPU_ID ≠ slp_q_id n 0).
{
eapply slpq_id_neq_rdq; eauto.
}
rewrite <- Htq_eq in tcbinv.
unfold enqueue0_spec; simpl.
subrewrite´.
unfold Queue_arg.
rewrite zle_lt_true by omega.
rewrite zle_lt_true by omega.
clear Htq_eq.
d7 subdestruct_match_one.
d7 subdestruct_one; try omega.
inv tcbinv; simpl. subst.
rewrite Hdestruct6; simpl.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´; simpl.
rewrite zle_lt_true by omega.
repeat rewrite ZMap.gss.
set (t´:= (ZMap.set (ZMap.get current_CPU_ID (cid labd))
(AbTCBValid RUN current_CPU_ID (slp_q_id n 0)) t_lock)) in ×.
set (q´:= (ZMap.set (slp_q_id n 0)
(AbQValid
(l1 ++ (ZMap.get current_CPU_ID (cid labd)) :: nil)) q_lock)) in ×.
exploit (H_CalLock_rel t´ q´); eauto.
intros (y´ & ->); simpl. repeat rewrite ZMap.set2.
unfold release_lock_SC_spec; simpl. subrewrite´.
rewrite zle_lt_true by omega.
rewrite ZMap.gso; eauto.
erewrite <- (Hsame ID_SC (slp_q_id n 0)); try omega; eauto.
rewrite ZMap.gso; eauto.
erewrite <- lock_re0. simpl.
subrewrite´; simpl.
subst t´ q´.
rewrite ZMap.gso; auto.
rewrite Hdestruct15. rewrite ZMap.gss.
rewrite zle_lt_true; eauto.
rewrite ZMap.gso; auto. rewrite Hdestruct19.
rewrite zeq_true, zeq_true, zlt_lt_true; eauto; simpl.
{
refine_split´; eauto.
econstructor; simpl; eauto.
- congruence.
- congruence.
- eapply (relate_Thread_Log_Pool_gso ID_SC (slp_q_id n 0)); try omega; eauto.
inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (slp_q_id n 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct7. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
- eapply lock_re_gss; eauto.
eapply lock_re_gss; eauto.
- kctxt_inj_simpl.
- econstructor; eauto.
rewrite ZMap.gso; auto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct11 in Hcal. inv Hcal.
repeat rewrite ZMap.gss. repeat rewrite ZMap.set2.
refine_split´; trivial.
rewrite HCPU. rewrite ZMap.gss. trivial.
- intros. eapply kctxt_re0; eauto.
}
Fail idtac.
Qed.
End SLEEP.
Section WAKEUP.
Lemma big_thread_wakeup_exist:
∀ s habd habd´ labd cv r
(Hhigh: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd) f,
biglow_thread_wakeup_spec cv habd = Some (habd´, r)
→ relate_AbData s f habd labd
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, thread_wakeup_spec cv labd = Some (labd´, r)
∧ relate_AbData s f habd´ labd´.
Proof.
Opaque remove.
generalize max_unsigned_val; intro muval.
unfold thread_wakeup_spec, biglow_thread_wakeup_spec; intros until f.
intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
specialize (PQThread.CPU_ID_range _ Hhigh).
specialize (PQThread.valid_curid _ Hhigh).
subrewrite´. intros HCPU_range Hcid Hinv. d7 subdestruct_one.
subdestruct_match_one.
assert (HOS1: MSG_Q_START ≤ (slp_q_id cv 0) < num_chan).
{
unfold slp_q_id. omega.
}
assert (HOS2: 0 ≤ (slp_q_id cv 0) < num_chan) by omega.
pose proof multi_log_re0 as Hrel_log´.
inv multi_log_re0. pose proof Hdiff as Hdiff´. specialize (Hdiff _ HOS1).
rewrite Hdestruct5 in Hdiff. inv Hdiff.
pose proof multi_oracle_re0 as Hrel_oracle´.
inv multi_oracle_re0. pose proof Hdiff as Hdiff´´. specialize (Hdiff _ HOS1).
inv Hdiff. exploit (Hpre (CPU_ID labd)); eauto.
intros Hrel_log_oracle.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound; omega.
}
intros (x & Hcal´). rename Hdestruct6 into Hcal_tcb´.
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv Hhigh; assumption.
}
rewrite HCPU in ×.
inv abtcb_re0.
unfold CalTCB_log_real in Hcal_tcb´. revert Hinv.
subdestruct_match_one. intros. inv Hcal_tcb´.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1). inv H1.
unfold dequeue_atomic_spec.
pose proof Hdestruct6 as tcbinv.
unfold CalTCB_log in tcbinv; simpl in tcbinv.
subdestruct_match_one.
destruct p as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (Hlock: ZMap.get ((slp_q_id cv 0) + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
assert (Hacq: ∃ t_lock q_lock,
acquire_lock_ABTCB_spec (slp_q_id cv 0) labd =
Some (labd
{multi_log
: ZMap.set ((slp_q_id cv 0) + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID (TTICKET (WAIT_LOCK local_lock_bound)) ::
ZMap.get ((slp_q_id cv 0) + ID_AT_range)
(multi_oracle labd) current_CPU_ID l2 ++ l2))
(multi_log labd)}
{lock : ZMap.set ((slp_q_id cv 0) + ID_AT_range) (LockOwn true) (lock labd)}
{abtcb : t_lock} {abq : q_lock})
∧ (t_lock, q_lock) = match ZMap.get (slp_q_id cv 0) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (t2, q2)
end
∧ ZMap.get current_CPU_ID (sleeper labd) = s2
∧ ZMap.get current_CPU_ID (cid labd) = curid2).
{
unfold acquire_lock_ABTCB_spec.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite <- H.
rewrite Hcal´. simpl.
erewrite MultiLogMap2id_get_shared; eauto.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
destruct (ZMap.get (slp_q_id cv 0) cached2) eqn: Hcache.
- destruct p.
refine_split´; eauto.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock & q_lock & → & Htq_eq & Hsleep´ & Hcid´).
assert (Hneq2: rdy_q_id current_CPU_ID ≠ slp_q_id cv 0).
{
eapply slpq_id_neq_rdq; eauto.
}
rewrite <- Htq_eq in tcbinv.
unfold dequeue0_spec; simpl.
subrewrite´.
rewrite zle_lt_true by omega.
destruct (ZMap.get (slp_q_id cv 0) q_lock); contra_inv.
destruct l0.
- rewrite zeq_true in tcbinv. inv tcbinv.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.gss. simpl.
exploit (H_CalLock_rel t1 q1); eauto.
intros (y´ & ->); simpl. inv Hinv; simpl.
repeat rewrite ZMap.set2.
refine_split´; eauto.
{
econstructor; eauto; simpl.
- congruence.
- inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (slp_q_id cv 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
- eapply lock_re_gss´; eauto.
- econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct6 in Hcal. inv Hcal.
repeat rewrite ZMap.gss.
refine_split´; trivial.
}
- subdestruct_one.
destruct (ZMap.get z t_lock); contra_inv.
subdestruct_one; subst.
+ subdestruct_match_one.
rewrite zeq_true in tcbinv. inv tcbinv; simpl. inv Hinv.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.gss. simpl.
exploit (H_CalLock_rel (ZMap.set z (AbTCBValid tds current_CPU_ID (-1)) t_lock)
(ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock)); eauto.
intros (y´ & ->); simpl.
rewrite zle_lt_true by omega. rewrite ZMap.gss.
subdestruct_match_one.
rewrite zeq_true.
rewrite ZMap.gso; eauto.
rewrite Hdestruct10.
repeat rewrite ZMap.set2. inv H1.
refine_split´; eauto.
{
econstructor; eauto; simpl.
- congruence.
- inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (slp_q_id cv 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
- eapply lock_re_gss´; eauto.
- econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct6 in Hcal. inv Hcal.
repeat rewrite ZMap.gss.
refine_split´; trivial.
}
+ rewrite zeq_true in tcbinv. inv tcbinv; simpl.
clear Htq_eq. d5 subdestruct_match_one. inv Hinv.
unfold CalTCB_log_real in Hdestruct12.
subdestruct_match_one.
destruct p as (((((t3 & q3) & s3) & curid3) & cached3) & res3).
inv Hdestruct12. inv H1.
unfold CalTCB_log in ×. pose proof Hdestruct11 as Hcal_real.
assert (Hex: ∃ l_low,
l_low = TEVENT current_CPU_ID (TSHARED (OTDWAKE cv))
:: ZMap.get lock_range (multi_oracle habd)
current_CPU_ID l ++ l) by eauto.
destruct Hex as (l_low & Hex).
rewrite <- Hex in ×.
simpl in Hdestruct11. rewrite Hdestruct6 in Hdestruct11.
assert (HOS1´: MSG_Q_START ≤ (msg_q_id cpu_id) < num_chan).
{
unfold msg_q_id. omega.
}
assert (HOS2´: 0 ≤ (msg_q_id cpu_id) < num_chan) by omega.
specialize (Hdiff´ _ HOS1´).
rewrite Hdestruct5 in Hdiff´. inv Hdiff´.
specialize (Hdiff´´ _ HOS1´).
inv Hdiff´´. exploit (Hpre1 current_CPU_ID); eauto.
intros Hrel_log_oracle´.
assert (Hneq: msg_q_id cpu_id ≠ slp_q_id cv 0).
{
unfold msg_q_id, slp_q_id. omega.
}
assert (Hneq´: msg_q_id cpu_id + ID_AT_range ≠ slp_q_id cv 0 + ID_AT_range).
{
eapply add_aux. trivial.
}
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss; simpl.
rewrite ZMap.gss; simpl.
exploit (H_CalLock_rel (ZMap.set wk_id (AbTCBValid tds cpu_id (-1)) t_lock)
(ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock)); eauto.
intros (y´ & ->); simpl.
rewrite zle_lt_true by omega. rewrite ZMap.gss.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound; omega.
}
intros (x´ & Hcal´´).
rewrite Hdestruct14.
rewrite zeq_false; auto.
rewrite zle_lt_true; try omega.
unfold enqueue_atomic_spec; simpl.
repeat rewrite ZMap.gss. repeat rewrite ZMap.set2.
repeat match goal with
| |- context[MultiDef (?a :: ?l)] ⇒
let l´ := fresh "l_temp" in
set (l´ := a :: l) in ×
end.
match goal with
| |- context[acquire_lock_ABTCB_spec _ ?a] ⇒
set (a´:= labd {abtcb: ZMap.set wk_id (AbTCBValid tds cpu_id (-1)) t_lock}
{abq: ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock}
{multi_log: ZMap.set (slp_q_id cv 0 + ID_AT_range)
(MultiDef l_temp0) (multi_log labd)}
{lock: ZMap.set (slp_q_id cv 0 + ID_AT_range) LockFalse (lock labd)});
assert (Ha_eq: a = a´)
end.
{
reflexivity.
}
rewrite Ha_eq. clear Ha_eq.
rewrite ZMap.gso in Hdestruct11; eauto.
assert (Hacq: ∃ t_lock´ q_lock´,
acquire_lock_ABTCB_spec (msg_q_id cpu_id) a´ =
Some (labd
{multi_log
: ZMap.set ((msg_q_id cpu_id) + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID
(TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get ((msg_q_id cpu_id) + ID_AT_range)
(multi_oracle labd) current_CPU_ID l3 ++ l3))
(multi_log a´)}
{lock : ZMap.set ((msg_q_id cpu_id) + ID_AT_range) (LockOwn true) (lock a´)}
{abtcb : t_lock´} {abq : q_lock´})
∧ (t_lock´, q_lock´) = match ZMap.get (msg_q_id cpu_id) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (ZMap.set wk_id (AbTCBValid tds cpu_id (-1)) t_lock,
ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock)
end).
{
unfold acquire_lock_ABTCB_spec.
subst a´; simpl.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite ZMap.gso; eauto.
rewrite <- H3.
rewrite ZMap.gso; eauto.
assert (Hlock´: ZMap.get ((msg_q_id cpu_id) + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
rewrite Hlock´. rewrite Hcal´´; simpl.
erewrite MultiLogMap2id_get_shared; eauto.
unfold AbTCBPool, AbQueuePool, ZMap.t, PMap.t in ×.
subdestruct_match_one.
- destruct p as (nt, nq).
subdestruct_match_one.
refine_split´; eauto. reflexivity.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock´ & q_lock´ & → & Htq_eq´).
unfold enqueue0_spec; simpl.
subrewrite´.
unfold Queue_arg.
rewrite zle_lt_true; eauto.
rewrite zle_lt_true; eauto.
unfold AbTCBPool, AbQueuePool, ZMap.t, PMap.t in ×.
rewrite <- Htq_eq´ in Hdestruct11. clear Htq_eq´.
destruct (ZMap.get (msg_q_id cpu_id) q_lock´); contra_inv.
destruct (ZMap.get wk_id t_lock´); contra_inv.
subdestruct_match_one.
subdestruct_match_one.
rewrite zeq_true in Hdestruct11. inv Hdestruct11.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.gss. simpl.
exploit (H_CalLock_rel (ZMap.set wk_id (AbTCBValid tds0 cpu_id (msg_q_id cpu_id)) t_lock´)
(ZMap.set (msg_q_id cpu_id) (AbQValid (l1 ++ wk_id :: nil)) q_lock´)); eauto.
intros (y´´ & ->); simpl.
repeat rewrite ZMap.set2.
repeat rewrite ZMap.gss.
refine_split´; eauto.
{
econstructor; eauto; simpl.
- congruence.
- subst l_temp1 l_temp0.
inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (msg_q_id cpu_id) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ assert(MultiLogMap2id nil (msg_q_id cpu_id) nil) by constructor.
exploit (BIGMAP_CONS (TEVENT current_CPU_ID (TSHARED (OTDWAKE_DIFF wk_id cpu_id)))
(TEVENT current_CPU_ID (TSHARED (OTDWAKE cv))
:: ZMap.get lock_range (multi_oracle habd) current_CPU_ID l ++ l)); eauto.
econstructor; eauto.
econstructor; eauto.
reflexivity.
eapply MultiE2id_EQ; eauto.
reflexivity.
rewrite ZMap.gss.
reflexivity.
+ simpl.
rewrite zeq_true by reflexivity.
reflexivity.
}
{
rewrite ZMap.gso; eauto.
destruct (zeq (slp_q_id cv 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ assert(MultiLogMap2id nil (msg_q_id cpu_id) nil) by constructor.
exploit (BIGMAP_CONS (TEVENT current_CPU_ID (TSHARED (OTDWAKE_DIFF wk_id cpu_id)))
(TEVENT current_CPU_ID (TSHARED (OTDWAKE cv))
:: ZMap.get lock_range (multi_oracle habd) current_CPU_ID l ++ l)); eauto.
econstructor; eauto.
eapply MultiE2id_EQ; eauto.
reflexivity.
rewrite ZMap.gss.
reflexivity.
econstructor; eauto.
reflexivity.
+ simpl.
rewrite zeq_true by reflexivity.
reflexivity.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre2 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log1.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
econstructor.
reflexivity.
assumption.
eapply add_aux; eauto.
}
eapply add_aux; eauto.
}
- eapply lock_re_gss´; eauto.
eapply lock_re_gss´; eauto.
rewrite ZMap.gso; eauto.
rewrite <- lock_re0.
rewrite Hdestruct13. trivial.
- econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
subst l4. unfold CalTCB_log in Hcal.
unfold AbTCBPool, AbQueuePool, ZMap.t, PMap.t in ×.
rewrite Hcal_real in Hcal. inv Hcal.
repeat rewrite ZMap.gss.
refine_split´; trivial.
}
Fail idtac.
Qed.
End WAKEUP.
Section SPAWN.
Lemma big_thread_spawn_exist:
∀ s habd habd´ labd b b´ ofs´ id q n
(Hhigh: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd) f,
biglow_thread_spawn_spec habd b b´ ofs´ id q = Some (habd´, n)
→ relate_AbData s f habd labd
→ find_symbol s STACK_LOC = Some b
→ (∃ id, find_symbol s id = Some b´)
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, thread_spawn_spec labd b b´ ofs´ id q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_thread_spawn_spec, thread_spawn_spec.
intros until f; intros HP HR Hsys Hsys´ Hincr.
pose proof HR as HR´. inv HR´.
revert HP. subrewrite. subdestruct; inv HQ; simpl.
pose proof abtcb_re0 as Htcb. inv Htcb.
unfold CalTCB_log_real in ×.
subdestruct_match_one.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1).
pose proof Hdestruct10 as Hcal_t.
unfold CalTCB_log in Hdestruct10. simpl in Hdestruct10.
subdestruct_match_one.
destruct p as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv Hhigh; assumption.
}
rewrite HCPU in ×.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l0 = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
inv abtcb_re0.
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
subdestruct; try omega; simpl.
inv Hdestruct10; simpl.
refine_split´; eauto.
econstructor; simpl; eauto.
- congruence.
- inv multi_log_re0.
econstructor.
× intros. rewrite ZMap.gso.
eauto.
eapply lock_neq in H0; eauto.
× intros. rewrite ZMap.gss.
exploit Hdiff; eauto.
erewrite Hdestruct8. intros HF. inv HF.
econstructor; eauto.
inv multi_oracle_re0.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
- kctxt_inj_simpl.
+ destruct Hsys´ as [id´ Hsys´].
eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply kctxt_re0; eauto. omega.
- econstructor. rewrite ZMap.gss.
intros. inv Hlog.
rewrite Hcal_t in Hcal. inv Hcal.
refine_split´; trivial.
Fail idtac.
Qed.
End SPAWN.
Lemma relate_tcb_gso:
∀ i l bl t q s c,
relate_tcb bl t q s c →
lock_range ≠ i →
relate_tcb (ZMap.set i l bl) t q s c.
Proof.
intros. inv H. econstructor; eauto.
rewrite ZMap.gso; eauto.
Qed.
Lemma relate_tcb_gso´:
∀ i ofs r l bl t q s c,
relate_tcb bl t q s c →
index2Z i ofs = Some r →
relate_tcb (ZMap.set r l bl) t q s c.
Proof.
intros. eapply relate_tcb_gso; eauto.
eapply lock_neq; eauto.
Qed.
Lemma palloc_exist:
∀ s habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re0. eapply (Hsame 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re0. eapply (Hsame 0 0); auto. omega.
}
rewrite Horacle.
erewrite lock_re0.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso 0 0); eauto. omega.
+ eapply (relate_tcb_gso´ 0 0); eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso 0 0); eauto. omega.
+ eapply (relate_tcb_gso´ 0 0); eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso 0 0); eauto. omega.
+ eapply (relate_tcb_gso´ 0 0); eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ s habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f, ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma index2Z_eq´:
∀ i,
0 ≤ i < num_chan →
index2Z 2 i = Some (i + lock_TCB_range).
Proof.
unfold index2Z.
unfold index_incrange, index_range.
intros.
unfold ID_SC_range. rewrite zle_lt_true; trivial.
f_equal. omega.
Qed.
Lemma acquire_lock_SC_exist:
∀ s i habd habd´ labd f,
acquire_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_SC_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_SC_spec; intros.
pose proof H0 as HR. inv H0.
revert H. rewrite lock_re0.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + lock_TCB_range) (multi_log habd)
= ZMap.get (i + lock_TCB_range) (multi_log labd)).
{
inv multi_log_re0. eapply (Hsame ID_SC i); auto.
omega. eapply index2Z_eq´; eauto.
}
assert (Horacle: ZMap.get (i + lock_TCB_range) (multi_oracle habd)
= ZMap.get (i + lock_TCB_range) (multi_oracle labd)).
{
inv multi_oracle_re0. eapply (Hsame ID_SC i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog, <- Horacle.
subdestruct; inv HQ.
- refine_split´; trivial.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso ID_SC i); eauto. omega.
eapply index2Z_eq´; eauto.
+ eapply lock_re_gss; eauto.
+ eapply (relate_tcb_gso´ ID_SC i); eauto.
eapply index2Z_eq´; eauto.
- refine_split´; trivial.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso ID_SC i); eauto. omega.
eapply index2Z_eq´; eauto.
+ eapply lock_re_gss; eauto.
+ eapply (relate_tcb_gso´ ID_SC i); eauto.
eapply index2Z_eq´; eauto.
Qed.
Lemma release_lock_SC_exist:
∀ s i habd habd´ labd f,
release_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_SC_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_SC_spec; intros.
pose proof H0 as HR. inv H0.
revert H. rewrite lock_re0.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + lock_TCB_range) (multi_log habd)
= ZMap.get (i + lock_TCB_range) (multi_log labd)).
{
inv multi_log_re0. eapply (Hsame ID_SC i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog.
subdestruct; inv HQ.
refine_split´; trivial.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso ID_SC i); eauto. omega.
eapply index2Z_eq´; eauto.
+ eapply lock_re_gss; eauto.
+ eapply (relate_tcb_gso´ ID_SC i); eauto.
eapply index2Z_eq´; eauto.
Qed.
Section YIELD.
Lemma thread_yield_exist:
∀ habd habd´ labd rs r´ rs0 s
(HINV: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd)f,
biglow_thread_yield_spec
habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t,
val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
→ ∃ labd´ r´0 ofs, thread_yield_spec
labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
#EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r,
ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = r´0.
Proof.
Opaque remove.
unfold thread_yield_spec, biglow_thread_yield_spec; intros until f.
intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
specialize (PQThread.CPU_ID_range _ HINV).
specialize (PQThread.valid_curid _ HINV).
subrewrite´. intros HCPU_range Hcid Hhigh.
subdestruct; contra_inv.
inv Hhigh.
assert (HOS1: MSG_Q_START ≤ (msg_q_id (CPU_ID labd)) < num_chan).
{
unfold msg_q_id. omega.
}
assert (HOS2: 0 ≤ (msg_q_id (CPU_ID labd)) < num_chan).
{
omega.
}
pose proof multi_log_re0 as Hrel_log´.
inv multi_log_re0. specialize (Hdiff _ HOS1).
rewrite Hdestruct5 in Hdiff. inv Hdiff.
pose proof multi_oracle_re0 as Hrel_oracle´.
inv multi_oracle_re0. specialize (Hdiff _ HOS1).
inv Hdiff. exploit (Hpre (CPU_ID labd)); eauto.
intros Hrel_log_oracle.
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv HINV; assumption.
}
rewrite HCPU in ×.
inv abtcb_re0.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound; omega.
}
intros (x & Hcal). rename Hdestruct6 into Hcal_tcb´.
unfold CalTCB_log_real in Hcal_tcb´.
subdestruct_match_one. inv Hcal_tcb´.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1). inv H1.
unfold thread_poll_pending_spec, dequeue_atomic_spec.
pose proof Hdestruct6 as tcbinv.
unfold CalTCB_log in tcbinv; simpl in tcbinv.
subdestruct_match_one.
destruct p as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (Hlock: ZMap.get (msg_q_id current_CPU_ID + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
assert (Hacq: ∃ t_lock q_lock,
acquire_lock_ABTCB_spec (msg_q_id (CPU_ID labd)) labd =
Some (labd
{multi_log
: ZMap.set ((msg_q_id (CPU_ID labd)) + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID
(TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get ((msg_q_id (CPU_ID labd)) + ID_AT_range)
(multi_oracle labd) current_CPU_ID l2 ++ l2))
(multi_log labd)}
{lock : ZMap.set ((msg_q_id (CPU_ID labd)) + ID_AT_range) (LockOwn true) (lock labd)}
{abtcb : t_lock} {abq : q_lock})
∧ (t_lock, q_lock) = match ZMap.get (msg_q_id (CPU_ID labd)) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (t2, q2)
end
∧ ZMap.get current_CPU_ID (sleeper labd) = s2
∧ ZMap.get current_CPU_ID (cid labd) = curid2).
{
unfold acquire_lock_ABTCB_spec.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite <- H.
rewrite Hcal. simpl.
erewrite MultiLogMap2id_get_shared; eauto.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
destruct (ZMap.get (msg_q_id current_CPU_ID) cached2) eqn: Hcache.
- destruct p.
refine_split´; eauto.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock & q_lock & → & Htq_eq & Hsleep´ & Hcid´).
rewrite HCPU in ×.
rewrite <- Htq_eq in tcbinv.
unfold dequeue0_spec; simpl.
subrewrite´.
rewrite zle_lt_true by omega.
clear Htq_eq.
d2 subdestruct_match_one; contra_inv.
- subdestruct; contra_inv; try omega.
inv tcbinv. subst.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´; simpl.
rewrite zle_lt_true by omega.
repeat rewrite ZMap.gss.
exploit (H_CalLock_rel t_lock q_lock); eauto.
intros (y´ & ->); simpl. repeat rewrite ZMap.set2.
subrewrite´; simpl.
refine_split´; eauto.
econstructor; simpl; eauto.
+ congruence.
+ inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (msg_q_id current_CPU_ID) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
+ eapply lock_re_gss´; eauto.
+ kctxt_inj_simpl.
+ econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct6 in Hcal0. inv Hcal0.
repeat rewrite ZMap.gss.
refine_split´; trivial.
+ intros. eapply kctxt_re0; eauto.
- subdestruct; contra_inv; try omega.
inv tcbinv; simpl. subst.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´; simpl.
rewrite zle_lt_true by omega.
repeat rewrite ZMap.gss.
exploit (H_CalLock_rel (ZMap.set z (AbTCBValid tds cpuid (-1)) t_lock)
(ZMap.set (msg_q_id current_CPU_ID)
(AbQValid l1) q_lock)); eauto.
intros (y´ & ->); simpl. repeat rewrite ZMap.set2.
rewrite zle_lt_true; trivial.
rewrite ZMap.gso; eauto.
assert (Hcused: cused (ZMap.get z (AC labd)) = true).
{
inv Hdestruct9. trivial.
}
rewrite Hdestruct16. rewrite zle_lt_true; trivial. rewrite Hcused; simpl.
rewrite ZMap.gss.
rewrite ZMap.gso; eauto.
subrewrite´; simpl.
assert (Hget: ∃ t b,
ZMap.get run_id (ZMap.set z (AbTCBValid READY current_CPU_ID (rdy_q_id current_CPU_ID)) t_lock)
= AbTCBValid t current_CPU_ID b).
{
destruct (zeq run_id z); subst.
- rewrite ZMap.gss. eauto.
- rewrite ZMap.gso; eauto.
}
destruct Hget as (t & b & ->).
rewrite zeq_true; simpl.
refine_split´; try eapply a; eauto.
econstructor; simpl; eauto.
+ congruence.
+ inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (msg_q_id current_CPU_ID) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
+ eapply lock_re_gss´; eauto.
+ kctxt_inj_simpl.
+ econstructor; eauto.
rewrite ZMap.gss. intros. repeat rewrite ZMap.set2.
inv Hlog.
rewrite Hdestruct6 in Hcal0. inv Hcal0.
repeat rewrite ZMap.gss.
refine_split´; trivial.
+ intros. eapply kctxt_re0; eauto.
+ eapply msg_neq.
Fail idtac.
Qed.
End YIELD.
End Exists.
Section PASSTHROUGH_PRIM.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
Qed.
Lemma get_curid_exist:
∀ s habd labd z f,
get_curid_spec habd = Some z
→ relate_AbData s f habd labd
→ get_curid_spec labd = Some z.
Proof.
unfold get_curid_spec; intros.
inv H0.
revert H;
subrewrite.
Qed.
Lemma get_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_curid_spec)
(id ↦ gensem get_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_curid_exist; eauto. reflexivity.
Qed.
Lemma lock_SC_range:
∀ ofs z
(Hindex: index2Z 2 ofs = Some z),
z ≠ lock_range.
Proof.
intros. unfold lock_range. functional inversion Hindex. subst.
functional inversion H0; subst. simpl in H1.
inv H1. unfold lock_TCB_range, ID_SC_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma lock_SC_range´:
∀ ofs z i
(Hindex: index2Z 2 ofs = Some z)
(Hrange: MSG_Q_START ≤ i < num_chan),
z ≠ i + ID_AT_range.
Proof.
intros. functional inversion Hindex. subst.
functional inversion H0; subst. simpl in H1.
inv H1. unfold lock_TCB_range, ID_SC_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. simpl in ×.
exploit Hsame; eauto. omega.
intros Hlog. rewrite <- Hlog. rewrite Hdestruct7.
erewrite <- lock_re0. rewrite Hdestruct8.
exploit page_copy_aux_exists; eauto.
intros Hpage. rewrite Hpage.
rewrite Hdestruct11.
refine_split´; try trivial.
econstructor; simpl; eauto.
- constructor; intros.
+ destruct (zeq r z); subst.
× repeat rewrite ZMap.gss. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq: z ≠ lock_range).
{
eapply lock_SC_range; eauto.
}
assert (Hneq´: z ≠ i0 + ID_AT_range).
{
eapply lock_SC_range´; eauto.
}
repeat rewrite ZMap.gso; eauto.
- constructor. intros.
assert (Hneq: z ≠ lock_range).
{
eapply lock_SC_range; eauto.
}
rewrite ZMap.gso in Hlog0; eauto.
inv abtcb_re0. eauto.
Qed.
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.
generalize H0; intro relateD.
inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
exploit page_copy_exist; eauto.
intros (labd´ & Hpage & Hrel).
rewrite Hpage.
refine_split´; trivial.
inv Hrel. econstructor; eauto.
rewrite syncchpool_re1. trivial.
Qed.
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.
Qed.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. simpl in ×.
exploit Hsame; eauto. omega.
intros Hlog. rewrite <- Hlog. rewrite Hdestruct7.
erewrite <- lock_re0. rewrite Hdestruct8.
rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & Hback & Hinj). rewrite Hback.
refine_split´; try trivial.
econstructor; simpl; eauto.
Qed.
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.
generalize H0; intro relateD.
inv H0.
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.
exploit relate_impl_syncchpool_update; eauto.
Qed.
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.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pqthread_passthrough pthread.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1. intros (labd´ & HP & HM).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit big_thread_spawn_exist; eauto 1; intros (labd´ & HP & HM).
destruct H8 as [fun_id Hsys].
exploit stencil_find_symbol_inject´; eauto. intros HFB.
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit big_thread_wakeup_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit thread_yield_exist; eauto 1.
intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
+ eapply kctxt_INJECT; try assumption.
+ eapply kctxt_INJECT; try assumption.
-
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit big_thread_sleep_exist; eauto 1.
intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
+ inv H9. inv H3. simpl in ×.
exploit Mem.loadv_inject; try eassumption.
val_inject_simpl. unfold Pregmap.get.
intros (v2 & HL & Hv). inv Hv. assumption.
+ eapply kctxt_INJECT; try assumption.
+ eapply kctxt_INJECT; try assumption.
-
intros. layer_sim_simpl.
simpl. constructor.
split; simpl; [|reflexivity|reflexivity|repeat constructor].
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd match_RData.
exploit big_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr _ _ ⇒ eapply inject_incr_refl
| _ ⇒ idtac
end.
repeat (econstructor). eapply HP.
constructor. econstructor; try eassumption. constructor.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit acquire_lock_SC_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit release_lock_SC_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply get_sync_chan_busy_sim.
- apply set_sync_chan_busy_sim.
- apply ipc_send_body_sim.
- apply ipc_receive_body_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply proc_create_postinit_sim.
- apply trapin_sim.
- apply trapout_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End PASSTHROUGH_PRIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.
Require Import TacticsForTesting.
Lemma lock_max:
∀ i ofs r,
index2Z i ofs = Some r →
r < lock_range.
Proof.
unfold lock_range.
intros. functional inversion H; subst.
functional inversion H1; subst.
- unfold ID_AT_range in ×.
functional inversion H2; subst.
unfold ID_TCB_range, ID_SC_range. omega.
- functional inversion H2; subst.
unfold ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
- functional inversion H2; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
Qed.
Lemma lock_neq:
∀ i ofs r,
index2Z i ofs = Some r →
lock_range ≠ r.
Proof.
intros. exploit lock_max; eauto.
intros. omega.
Qed.
Lemma lock_re_gss:
∀ (l1 l2: Lock)
(lock_re0 : ∀ i0, ZMap.get i0 l1 = ZMap.get i0 l2) k ofs,
(∀ i0,
ZMap.get i0 (ZMap.set ofs k l1) =
ZMap.get i0 (ZMap.set ofs k l2)).
Proof.
intros. destruct (zeq i0 ofs); subst.
{
repeat rewrite ZMap.gss; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
}
Qed.
Lemma lock_re_gss´:
∀ (l1 l2: Lock)
(lock_re0 : ∀ i0, ZMap.get i0 l1 = ZMap.get i0 l2) k ofs
(lock_eq: ZMap.get ofs l2 = k),
(∀ i0, ZMap.get i0 l1 =
ZMap.get i0 (ZMap.set ofs k l2)).
Proof.
intros. destruct (zeq i0 ofs); subst.
{
repeat rewrite ZMap.gss; eauto.
}
{
repeat rewrite ZMap.gso; eauto.
}
Qed.
Lemma TCB_range_neq:
∀ i ofs r i0,
0 ≤ i0 < num_chan →
i ≠ ID_TCB →
index2Z i ofs = Some r →
i0 + ID_AT_range ≠ r.
Proof.
intros. functional inversion H1.
functional inversion H3; subst.
- unfold ID_AT_range in ×.
functional inversion H4; subst. omega.
- omega.
- functional inversion H4; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
Qed.
Lemma relate_Thread_Log_Pool_gso:
∀ i ofs r hl ll l0,
relate_Thread_Log_Pool hl ll →
i ≠ ID_TCB →
index2Z i ofs = Some r →
relate_Thread_Log_Pool (ZMap.set r l0 hl) (ZMap.set r l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r0 r); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
repeat rewrite ZMap.gso; eauto.
+ eapply TCB_range_neq; eauto. omega.
+ eapply lock_neq; eauto.
Qed.
Local Transparent H_CalLock.
Lemma MultiLogMap2id_imply_HCal:
∀ l_high l_low id
(Hlog: MultiLogMap2id l_high id l_low),
∃ self_c, H_CalLock l_low = Some (self_c, LEMPTY, None).
Proof.
induction l_high; simpl; intros.
- inv Hlog. simpl; eauto.
- inv Hlog. eapply IHl_high in Hbig.
destruct Hbig as (x & Hcal).
inv Hrel_e; simpl; eauto; rewrite Hcal.
repeat rewrite zeq_true; simpl; repeat rewrite zeq_true; eauto.
Qed.
Lemma MultiLogMap2id_imply_HCal_wait:
∀ n cpu l_high l_low id
(Hlog: MultiLogMap2id l_high id l_low)
(Hn: n ≠ O),
∃ x, H_CalLock (TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK n)) :: l_low) = Some x.
Proof.
intros. eapply MultiLogMap2id_imply_HCal in Hlog.
destruct Hlog as (self_c & Hcal).
simpl. rewrite Hcal. rewrite zeq_true.
destruct n; eauto. elim Hn; eauto.
Qed.
Lemma H_CalLock_rel:
∀ t q l cpu x
(Hcal: H_CalLock (TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l) = Some x),
∃ y, H_CalLock (TEVENT cpu (TTICKET REL_LOCK)
:: TEVENT cpu (TSHARED (OABTCBE t q))
:: TEVENT cpu (TSHARED OPULL)
:: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l) = Some y.
Proof.
simpl; intros. subdestruct; inv Hcal.
repeat rewrite zeq_true. eauto.
Qed.
Local Opaque H_CalLock.
Ltac subdestruct_match term:=
match term with
| context[match ?con with |_ ⇒ _ end] ⇒
progress subdestruct_if con
| _ ⇒
let H := fresh "Hdestruct" in
destruct term eqn: H; contra_inv
end.
Ltac subdestruct_match_one:=
match goal with
| [ HT: context[match ?con with |_ ⇒ _ end] |- _] ⇒ subdestruct_match con; simpl in HT
end; simpl.
Lemma CalTCB_log_real_cons:
∀ l x e
(Hcal: CalTCB_log_real (e::l) = Some x),
∃ y, CalTCB_log_real l = Some y.
Proof.
unfold CalTCB_log_real. simpl; intros.
unfold CalTCB_log in ×. simpl; intros. simpl in Hcal.
destruct e. simpl in Hcal.
subdestruct_match_one.
repeat destruct p; eauto.
Qed.
Lemma RData_update_tcb:
∀ a t q,
t = abtcb a →
q = abq a →
a = a {abtcb : t} {abq : q}.
Proof.
intros. unfold update_cid. subst.
destruct a; trivial.
Qed.
Lemma append_rewrite {A: Type}:
∀ (a: A) l,
a :: l = (a::nil) ++ l.
Proof.
simpl. trivial.
Qed.
Lemma append_rewrite3 {A: Type}:
∀ (a b c: A) l,
a :: b :: c :: l = (a::b::c::nil) ++ l.
Proof.
simpl. trivial.
Qed.
Lemma msg_range_neq:
∀ i ofs r i0 n,
0 ≤ i0 < num_chan →
i ≠ ID_TCB →
index2Z i ofs = Some r →
0 ≤ n < 8 →
r ≠ msg_q_id n + ID_AT_range.
Proof.
intros. functional inversion H1.
functional inversion H4; subst.
- unfold ID_AT_range in ×.
functional inversion H5; subst.
unfold msg_q_id. omega.
- omega.
- functional inversion H5; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
unfold msg_q_id. omega.
Qed.
Lemma slpq_id_neq_lock_range:
∀ n (Hr: 0 ≤ n < num_cv),
lock_range ≠ slp_q_id n 0 + lock_TCB_range.
Proof.
unfold slp_q_id. intros.
unfold lock_range, lock_TCB_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range.
omega.
Qed.
Lemma slpq_id_neq_rdq:
∀ n (Hr: 0 ≤ n < num_cv),
rdy_q_id current_CPU_ID ≠ slp_q_id n 0.
Proof.
unfold slp_q_id, rdy_q_id. intros.
pose proof current_CPU_ID_range.
omega.
Qed.
Lemma add_aux:
∀ (a b c: Z),
a ≠ b →
a + c ≠ b + c.
Proof.
intros. omega.
Qed.
Lemma msg_neq:
∀ n,
rdy_q_id n ≠ msg_q_id n.
Proof.
intros.
unfold rdy_q_id, msg_q_id. omega.
Qed.
Lemma list_append_eq:
∀ {A: Type} (a b: A) l1 l2 l3
(Hn : a ≠ b)
(Hl1 : l1 ++ a :: l2 = b :: l3),
In b l1.
Proof.
intros. destruct l1; subst.
- inv Hl1. elim Hn; trivial.
- inv Hl1. left; trivial.
Qed.
Lemma relate_Thread_Log_Pool_gss:
∀ gl sl gl0 gl1 sl0 n (Hrel: relate_Thread_Log_Pool gl sl)
(Hrelm: relate_Thread_Log_Type (MultiDef gl0) n (MultiDef sl0))
(Hn: 0 ≤ n < num_chan)
(Hgl: ZMap.get lock_range gl = MultiDef gl1)
(Hmulti: ∀ i l, i ≠ n → relate_Thread_Log gl1 i l → relate_Thread_Log gl0 i l),
relate_Thread_Log_Pool (ZMap.set lock_range (MultiDef gl0) gl)
(ZMap.set (n + ID_AT_range) (MultiDef sl0) sl).
Proof.
intros. inv Hrel. econstructor.
- intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H0; eauto.
eapply lock_neq in H0; eauto.
- intros. rewrite ZMap.gss.
destruct (zeq i n); subst.
+ rewrite ZMap.gss. eauto.
+ rewrite ZMap.gso; eauto.
× inv Hrelm. exploit Hdiff; eauto.
erewrite Hgl. intros HF. inv HF.
constructor. eauto.
× eapply add_aux; eauto.
Qed.
Lemma MultiLogMap2id_get_shared:
∀ l1 l2 id t q slp cache res curid
(Hmulti: MultiLogMap2id l1 id l2)
(Hcal: CalTCB_log l1 = Some (t, q, slp, curid, cache, res)),
GetSharedABTCB l2 = ZMap.get id cache.
Proof.
induction l1; simpl; intros.
- inv Hmulti. inv Hcal.
rewrite ZMap.gi. trivial.
- destruct a. pose proof Hcal as Hcal_t.
unfold CalTCB_log in Hcal. simpl in Hcal.
subdestruct_match_one.
destruct p as (((((t0 & q0) & slp0) & curid0) & cache0) & res0).
inv Hmulti. inv Hrel_e.
+ simpl. subdestruct; inv Hcal; eauto.
+ simpl. inv Hsome.
destruct e; inv H0.
destruct e; inv H1.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
× repeat subdestruct_match_one; inv Hcal; rewrite ZMap.gso; eauto.
+ simpl. rewrite Hcal0 in Hcal_t. inv Hcal_t. inv Hsome.
destruct e; inv H0.
destruct e; inv H1.
× repeat subdestruct_match_one; inv Hcal; eauto.
× repeat subdestruct_match_one; inv Hcal; eauto.
× repeat subdestruct_match_one; inv Hcal; eauto.
× repeat subdestruct_match_one; inv Hcal; eauto.
Qed.
Lemma CalTCB_log_gso:
∀ l l´ t q s curid cached res
(Hlog: ∀ e cpu,
In (TEVENT cpu e) l → cpu ≠ current_CPU_ID)
(Hcal: CalTCB_log (l ++ l´) = Some (t, q, s, curid, cached, res)),
∃ cached´ res´, CalTCB_log l´ = Some (t, q, s, curid, cached´, res´).
Proof.
induction l; simpl; intros; eauto.
unfold CalTCB_log in Hcal. simpl in Hcal.
destruct a.
assert (Hneq: i ≠ current_CPU_ID).
{
eapply Hlog. left; trivial.
}
assert (Hcal´: ∃ cached´ res´,
CalTCB_log (l ++ l´) = Some (t, q, s, curid, cached´, res´)).
{
subdestruct_match_one.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1).
unfold CalTCB_log. rewrite Hdestruct. clear Hdestruct.
destruct e.
- inv Hcal. eauto.
- destruct e; try (inv Hcal; eauto; fail).
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
+ repeat subdestruct_match_one; try omega; inv Hcal; eauto.
}
destruct Hcal´ as (cache´ & res´ & Hcal´).
eapply IHl; eauto.
Qed.
Lemma CalTCB_log_gso´:
∀ l t q s curid cached res habd
(Hhigh: PQThread.high_level_invariant habd)
(Hcal: CalTCB_log ((ZMap.get lock_range (multi_oracle habd) current_CPU_ID l) ++ l) =
Some (t, q, s, curid, cached, res)),
∃ cached´ res´, CalTCB_log l = Some (t, q, s, curid, cached´, res´).
Proof.
intros. eapply CalTCB_log_gso in Hcal; eauto.
eapply valid_big_oracle; eauto.
Qed.
Section INIT.
Require Import CalTicketLock.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealPTPool.
Require Import CalRealSMSPool.
Require Import DeviceStateDataType.
Lemma real_lock__pb_re:
∀ n l1 l2
(Hrel: ∀ i, ZMap.get i l1 = ZMap.get i l2),
(∀ i,
ZMap.get i (real_lock_pb n l1) = ZMap.get i (real_lock_pb n l2)).
Proof.
induction n; simpl; intros; trivial.
destruct (zeq i (Z.of_nat n)); subst; trivial.
- repeat rewrite ZMap.gss; trivial.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_multi_log_gss:
∀ i l (Hrange: 0 ≤ i < lock_range),
ZMap.get i (real_multi_log l) = MultiDef nil.
Proof.
unfold real_multi_log. intros.
replace i with (Z.of_nat (Z.to_nat i)).
- rewrite real_multi_log_pb_in. trivial. xomega.
- xomega.
Qed.
Lemma real_multi_log_gss´:
∀ i l (Hrange: 0 ≤ i ≤ lock_range),
ZMap.get i (real_multi_log´ l) = MultiDef nil.
Proof.
unfold real_multi_log´. intros.
replace i with (Z.of_nat (Z.to_nat i)).
- rewrite real_multi_log_pb_in. trivial. xomega.
- xomega.
Qed.
Lemma index2Z_range:
∀ i ofs r,
index2Z i ofs = Some r →
0 ≤ r < lock_range.
Proof.
split.
- functional inversion H; subst.
functional inversion H1; subst.
+ unfold ID_AT_range in ×.
functional inversion H2; subst. omega.
+ functional inversion H2; subst.
unfold ID_AT_range. omega.
+ functional inversion H2; subst.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
- eapply lock_max; eauto.
Qed.
Opaque real_multi_log´ real_multi_log real_vmxinfo real_LAT real_nps
real_pt real_idpde real_smspool real_abq real_syncchpool.
Lemma real_multi_log_eq:
∀ i ofs r l1 l2,
i ≠ 1 →
index2Z i ofs = Some r →
ZMap.get r (real_multi_log´ l1) = ZMap.get r (real_multi_log l2).
Proof.
intros. eapply index2Z_range in H0.
rewrite (real_multi_log_gss _ l2 H0).
assert (Hr: 0 ≤ r ≤ lock_range) by omega.
rewrite (real_multi_log_gss´ _ l1 Hr).
trivial.
Qed.
Lemma lock_range_r:
0 ≤ lock_range ≤ lock_range.
Proof.
unfold lock_range, lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
Qed.
Lemma real_multi_log_rel:
∀ i l1 l2,
MSG_Q_START ≤ i < num_chan →
relate_Thread_Log_Type (ZMap.get lock_range (real_multi_log´ l1)) i
(ZMap.get (i + ID_AT_range) (real_multi_log l2)).
Proof.
intros.
rewrite (real_multi_log_gss´ _ l1 lock_range_r).
assert (Hr´: 0 ≤ i + ID_AT_range < lock_range).
{
unfold lock_range, lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
omega.
}
rewrite (real_multi_log_gss _ l2 Hr´).
econstructor; eauto. econstructor; eauto.
instantiate (1:= nil). constructor. simpl. trivial.
Qed.
Lemma big_sched_init_exist:
∀ s habd habd´ labd mbi_adr
(Hhigh: PQThread.high_level_invariant habd)
(Hlow: PThread.high_level_invariant labd)f,
biglow_sched_init_spec mbi_adr habd = Some habd´
→ relate_AbData s f habd labd
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, sched_init_spec mbi_adr labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_sched_init_spec, sched_init_spec.
intros until f; intros HP HR Hincr.
pose proof HR as HR´. inv HR´.
revert HP.
rewrite init_re0, pg_re0, ikern_re0, ihost_re0, ipt_re0, in_intr_re0, ioapic_re0, lapic_re0, LAT_re0,
idpde_re0, smspool_re0, syncchpool_re0.
intros.
subdestruct; inv HP; simpl.
assert(∀ i : ZIndexed.t,
ZMap.get i (real_lock (lock habd)) = ZMap.get i (real_lock (lock labd))).
{
unfold real_lock. eapply real_lock__pb_re; eauto.
}
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv Hhigh; assumption.
}
refine_split´; trivial.
Ltac simpl_tac :=
match goal with
| |- ?a = ?a ⇒ reflexivity
| H: ?X |- ?X ⇒ exact H
| H: ?a = ?b |- ?b = ?a ⇒ rewrite H; reflexivity
| _ ⇒ try congruence
end.
econstructor; simpl; simpl_tac.
{
econstructor.
- intros. eapply real_multi_log_eq; eauto.
- intros. eapply real_multi_log_rel; eauto.
}
{
econstructor. intros.
rewrite (real_multi_log_gss´ _ (multi_log habd) lock_range_r) in Hlog.
inv Hlog. unfold CalTCB_log in Hcal; simpl in Hcal. inv Hcal.
refine_split´.
{
inv Hlow; symmetry; eauto.
}
{
symmetry.
eapply real_valid_cidpool.
apply current_CPU_ID_range.
}
{
rewrite HCPU.
inv Hlow; eauto.
rewrite <- valid_init_abtcb; eauto.
}
{
inv Hlow.
rewrite (valid_init_abq Hdestruct0); reflexivity.
}
}
Qed.
End INIT.
Section SLEEP.
Lemma remove_cache_event_gso:
∀ l l´ cid
(Hgso: ∀ e cid´,
In (TEVENT cid´ e) l → cid´ ≠ cid),
remove_cache_event (l ++ l´) cid
= remove_cache_event (l´) cid.
Proof.
induction l; simpl; eauto; intros.
destruct a; eauto.
rewrite zeq_false; eauto.
Qed.
Lemma remove_cache_event_gss:
∀ bl0 i,
remove_cache_event (remove_cache_event bl0 i) i =
remove_cache_event bl0 i.
Proof.
intros.
induction bl0.
reflexivity.
simpl.
destruct a.
destruct (zeq i0 i).
simpl.
destruct (zeq i0 i); try congruence.
assumption.
Qed.
Lemma remove_cache_event_eq:
∀ i bl0 labd,
PThread.high_level_invariant labd →
MSG_Q_START ≤ i < num_chan →
remove_cache_event(ZMap.get (i + ID_AT_range) (multi_oracle labd) current_CPU_ID
(remove_cache_event bl0 current_CPU_ID) ++
remove_cache_event bl0 current_CPU_ID) current_CPU_ID = remove_cache_event bl0 current_CPU_ID.
Proof.
intros.
erewrite remove_cache_event_gso; eauto.
eapply remove_cache_event_gss.
inv H.
unfold valid_multi_oracle_pool_H1 in valid_multi_oracle_pool_inv.
unfold valid_multi_oracle_domain in valid_multi_oracle_pool_inv.
exploit (valid_multi_oracle_pool_inv ID_TCB i ((i + ID_AT_range))); eauto.
Opaque Z.add.
unfold index2Z1; simpl.
rewrite zle_lt_true.
f_equal.
omega.
unfold ID_TCB_range.
omega.
intros (valid_oracle & valid_hqueue).
intros.
exploit valid_oracle; eauto.
intro tmp; destruct tmp; assumption.
Qed.
Lemma big_thread_sleep_exist:
∀ habd habd´ labd rs r´ rs0 n s
(HINV: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd) f,
biglow_thread_sleep_spec
habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) n = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t,
val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
→ ∃ labd´ r´0 ofs, thread_sleep_spec
labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
#EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) n = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r,
ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = r´0.
Proof.
Opaque remove.
generalize max_unsigned_val; intro muval.
unfold thread_sleep_spec, biglow_thread_sleep_spec; intros until f.
intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
specialize (PQThread.CPU_ID_range _ HINV).
specialize (PQThread.valid_curid _ HINV).
subrewrite´. intros HCPU_range Hcid Hinv. subdestruct; contra_inv;
inv Hinv.
assert (HOS1: MSG_Q_START ≤ (slp_q_id n 0) < num_chan).
{
unfold slp_q_id. omega.
}
assert (HOS2: 0 ≤ (slp_q_id n 0) < num_chan) by omega.
pose proof multi_log_re0 as Hrel_log´.
inv multi_log_re0. specialize (Hdiff _ HOS1).
rewrite Hdestruct7 in Hdiff. inv Hdiff.
pose proof multi_oracle_re0 as Hrel_oracle´.
inv multi_oracle_re0. specialize (Hdiff _ HOS1).
inv Hdiff. exploit (Hpre (CPU_ID labd)); eauto.
intros Hrel_log_oracle.
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv HINV; assumption.
}
rewrite HCPU in ×.
inv abtcb_re0.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound. omega.
}
intros (x & Hcal´). rename Hdestruct12 into Hcal_tcb´.
unfold CalTCB_log_real in Hcal_tcb´.
subdestruct_one. inv Hcal_tcb´.
destruct p0 as (((((t1 & q1) & s1) & curid1) & cached1) & res1).
assert (Hslpq_r: 16 ≤ slp_q_id n 0 < num_chan).
{
unfold slp_q_id. omega.
}
rewrite zle_lt_true; trivial.
inv H1.
unfold enqueue_atomic_spec.
generalize Hdestruct11; intro tcbinv.
unfold CalTCB_log in tcbinv; simpl in tcbinv.
subdestruct_match_one.
destruct p0 as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (Hacq: ∃ t_lock q_lock,
acquire_lock_ABTCB_spec (slp_q_id n 0) labd =
Some (labd
{multi_log
: ZMap.set (slp_q_id n 0 + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID
(TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get (slp_q_id n 0 + ID_AT_range)
(multi_oracle labd) current_CPU_ID l2 ++ l2))
(multi_log labd)}
{lock : ZMap.set (slp_q_id n 0 + ID_AT_range) (LockOwn true) (lock labd)}
{abtcb : t_lock} {abq : q_lock})
∧ (t_lock, q_lock) = match ZMap.get (slp_q_id n 0) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (t2, q2)
end
∧ ZMap.get current_CPU_ID (sleeper labd) = s2
∧ ZMap.get current_CPU_ID (cid labd) = curid2).
{
assert (Hlock: ZMap.get (slp_q_id n 0 + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
unfold acquire_lock_ABTCB_spec.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite <- H.
rewrite Hcal´. simpl.
erewrite MultiLogMap2id_get_shared; eauto.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
destruct (ZMap.get (slp_q_id n 0) cached2) eqn: Hcache.
- destruct p0.
refine_split´; eauto.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock & q_lock & → & Htq_eq & Hsleep´ & Hcid´).
assert (Hneq1: slp_q_id n 0 + lock_TCB_range ≠ slp_q_id n 0 + ID_AT_range).
{
unfold lock_TCB_range. unfold ID_TCB_range. omega.
}
assert (Heq1: index2Z 2 (slp_q_id n 0) = Some (slp_q_id n 0 + lock_TCB_range)).
{
unfold index2Z. unfold index_range. unfold index_incrange.
rewrite zle_lt_true; eauto. f_equal. omega.
}
assert (Hneq3: lock_range ≠ slp_q_id n 0 + lock_TCB_range).
{
eapply slpq_id_neq_lock_range; eauto.
}
assert (Hneq2: rdy_q_id current_CPU_ID ≠ slp_q_id n 0).
{
eapply slpq_id_neq_rdq; eauto.
}
rewrite <- Htq_eq in tcbinv.
unfold enqueue0_spec; simpl.
subrewrite´.
unfold Queue_arg.
rewrite zle_lt_true by omega.
rewrite zle_lt_true by omega.
clear Htq_eq.
d7 subdestruct_match_one.
d7 subdestruct_one; try omega.
inv tcbinv; simpl. subst.
rewrite Hdestruct6; simpl.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´; simpl.
rewrite zle_lt_true by omega.
repeat rewrite ZMap.gss.
set (t´:= (ZMap.set (ZMap.get current_CPU_ID (cid labd))
(AbTCBValid RUN current_CPU_ID (slp_q_id n 0)) t_lock)) in ×.
set (q´:= (ZMap.set (slp_q_id n 0)
(AbQValid
(l1 ++ (ZMap.get current_CPU_ID (cid labd)) :: nil)) q_lock)) in ×.
exploit (H_CalLock_rel t´ q´); eauto.
intros (y´ & ->); simpl. repeat rewrite ZMap.set2.
unfold release_lock_SC_spec; simpl. subrewrite´.
rewrite zle_lt_true by omega.
rewrite ZMap.gso; eauto.
erewrite <- (Hsame ID_SC (slp_q_id n 0)); try omega; eauto.
rewrite ZMap.gso; eauto.
erewrite <- lock_re0. simpl.
subrewrite´; simpl.
subst t´ q´.
rewrite ZMap.gso; auto.
rewrite Hdestruct15. rewrite ZMap.gss.
rewrite zle_lt_true; eauto.
rewrite ZMap.gso; auto. rewrite Hdestruct19.
rewrite zeq_true, zeq_true, zlt_lt_true; eauto; simpl.
{
refine_split´; eauto.
econstructor; simpl; eauto.
- congruence.
- congruence.
- eapply (relate_Thread_Log_Pool_gso ID_SC (slp_q_id n 0)); try omega; eauto.
inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (slp_q_id n 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct7. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
- eapply lock_re_gss; eauto.
eapply lock_re_gss; eauto.
- kctxt_inj_simpl.
- econstructor; eauto.
rewrite ZMap.gso; auto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct11 in Hcal. inv Hcal.
repeat rewrite ZMap.gss. repeat rewrite ZMap.set2.
refine_split´; trivial.
rewrite HCPU. rewrite ZMap.gss. trivial.
- intros. eapply kctxt_re0; eauto.
}
Fail idtac.
Qed.
End SLEEP.
Section WAKEUP.
Lemma big_thread_wakeup_exist:
∀ s habd habd´ labd cv r
(Hhigh: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd) f,
biglow_thread_wakeup_spec cv habd = Some (habd´, r)
→ relate_AbData s f habd labd
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, thread_wakeup_spec cv labd = Some (labd´, r)
∧ relate_AbData s f habd´ labd´.
Proof.
Opaque remove.
generalize max_unsigned_val; intro muval.
unfold thread_wakeup_spec, biglow_thread_wakeup_spec; intros until f.
intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
specialize (PQThread.CPU_ID_range _ Hhigh).
specialize (PQThread.valid_curid _ Hhigh).
subrewrite´. intros HCPU_range Hcid Hinv. d7 subdestruct_one.
subdestruct_match_one.
assert (HOS1: MSG_Q_START ≤ (slp_q_id cv 0) < num_chan).
{
unfold slp_q_id. omega.
}
assert (HOS2: 0 ≤ (slp_q_id cv 0) < num_chan) by omega.
pose proof multi_log_re0 as Hrel_log´.
inv multi_log_re0. pose proof Hdiff as Hdiff´. specialize (Hdiff _ HOS1).
rewrite Hdestruct5 in Hdiff. inv Hdiff.
pose proof multi_oracle_re0 as Hrel_oracle´.
inv multi_oracle_re0. pose proof Hdiff as Hdiff´´. specialize (Hdiff _ HOS1).
inv Hdiff. exploit (Hpre (CPU_ID labd)); eauto.
intros Hrel_log_oracle.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound; omega.
}
intros (x & Hcal´). rename Hdestruct6 into Hcal_tcb´.
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv Hhigh; assumption.
}
rewrite HCPU in ×.
inv abtcb_re0.
unfold CalTCB_log_real in Hcal_tcb´. revert Hinv.
subdestruct_match_one. intros. inv Hcal_tcb´.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1). inv H1.
unfold dequeue_atomic_spec.
pose proof Hdestruct6 as tcbinv.
unfold CalTCB_log in tcbinv; simpl in tcbinv.
subdestruct_match_one.
destruct p as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (Hlock: ZMap.get ((slp_q_id cv 0) + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
assert (Hacq: ∃ t_lock q_lock,
acquire_lock_ABTCB_spec (slp_q_id cv 0) labd =
Some (labd
{multi_log
: ZMap.set ((slp_q_id cv 0) + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID (TTICKET (WAIT_LOCK local_lock_bound)) ::
ZMap.get ((slp_q_id cv 0) + ID_AT_range)
(multi_oracle labd) current_CPU_ID l2 ++ l2))
(multi_log labd)}
{lock : ZMap.set ((slp_q_id cv 0) + ID_AT_range) (LockOwn true) (lock labd)}
{abtcb : t_lock} {abq : q_lock})
∧ (t_lock, q_lock) = match ZMap.get (slp_q_id cv 0) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (t2, q2)
end
∧ ZMap.get current_CPU_ID (sleeper labd) = s2
∧ ZMap.get current_CPU_ID (cid labd) = curid2).
{
unfold acquire_lock_ABTCB_spec.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite <- H.
rewrite Hcal´. simpl.
erewrite MultiLogMap2id_get_shared; eauto.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
destruct (ZMap.get (slp_q_id cv 0) cached2) eqn: Hcache.
- destruct p.
refine_split´; eauto.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock & q_lock & → & Htq_eq & Hsleep´ & Hcid´).
assert (Hneq2: rdy_q_id current_CPU_ID ≠ slp_q_id cv 0).
{
eapply slpq_id_neq_rdq; eauto.
}
rewrite <- Htq_eq in tcbinv.
unfold dequeue0_spec; simpl.
subrewrite´.
rewrite zle_lt_true by omega.
destruct (ZMap.get (slp_q_id cv 0) q_lock); contra_inv.
destruct l0.
- rewrite zeq_true in tcbinv. inv tcbinv.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.gss. simpl.
exploit (H_CalLock_rel t1 q1); eauto.
intros (y´ & ->); simpl. inv Hinv; simpl.
repeat rewrite ZMap.set2.
refine_split´; eauto.
{
econstructor; eauto; simpl.
- congruence.
- inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (slp_q_id cv 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
- eapply lock_re_gss´; eauto.
- econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct6 in Hcal. inv Hcal.
repeat rewrite ZMap.gss.
refine_split´; trivial.
}
- subdestruct_one.
destruct (ZMap.get z t_lock); contra_inv.
subdestruct_one; subst.
+ subdestruct_match_one.
rewrite zeq_true in tcbinv. inv tcbinv; simpl. inv Hinv.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.gss. simpl.
exploit (H_CalLock_rel (ZMap.set z (AbTCBValid tds current_CPU_ID (-1)) t_lock)
(ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock)); eauto.
intros (y´ & ->); simpl.
rewrite zle_lt_true by omega. rewrite ZMap.gss.
subdestruct_match_one.
rewrite zeq_true.
rewrite ZMap.gso; eauto.
rewrite Hdestruct10.
repeat rewrite ZMap.set2. inv H1.
refine_split´; eauto.
{
econstructor; eauto; simpl.
- congruence.
- inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (slp_q_id cv 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
- eapply lock_re_gss´; eauto.
- econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct6 in Hcal. inv Hcal.
repeat rewrite ZMap.gss.
refine_split´; trivial.
}
+ rewrite zeq_true in tcbinv. inv tcbinv; simpl.
clear Htq_eq. d5 subdestruct_match_one. inv Hinv.
unfold CalTCB_log_real in Hdestruct12.
subdestruct_match_one.
destruct p as (((((t3 & q3) & s3) & curid3) & cached3) & res3).
inv Hdestruct12. inv H1.
unfold CalTCB_log in ×. pose proof Hdestruct11 as Hcal_real.
assert (Hex: ∃ l_low,
l_low = TEVENT current_CPU_ID (TSHARED (OTDWAKE cv))
:: ZMap.get lock_range (multi_oracle habd)
current_CPU_ID l ++ l) by eauto.
destruct Hex as (l_low & Hex).
rewrite <- Hex in ×.
simpl in Hdestruct11. rewrite Hdestruct6 in Hdestruct11.
assert (HOS1´: MSG_Q_START ≤ (msg_q_id cpu_id) < num_chan).
{
unfold msg_q_id. omega.
}
assert (HOS2´: 0 ≤ (msg_q_id cpu_id) < num_chan) by omega.
specialize (Hdiff´ _ HOS1´).
rewrite Hdestruct5 in Hdiff´. inv Hdiff´.
specialize (Hdiff´´ _ HOS1´).
inv Hdiff´´. exploit (Hpre1 current_CPU_ID); eauto.
intros Hrel_log_oracle´.
assert (Hneq: msg_q_id cpu_id ≠ slp_q_id cv 0).
{
unfold msg_q_id, slp_q_id. omega.
}
assert (Hneq´: msg_q_id cpu_id + ID_AT_range ≠ slp_q_id cv 0 + ID_AT_range).
{
eapply add_aux. trivial.
}
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss; simpl.
rewrite ZMap.gss; simpl.
exploit (H_CalLock_rel (ZMap.set wk_id (AbTCBValid tds cpu_id (-1)) t_lock)
(ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock)); eauto.
intros (y´ & ->); simpl.
rewrite zle_lt_true by omega. rewrite ZMap.gss.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound; omega.
}
intros (x´ & Hcal´´).
rewrite Hdestruct14.
rewrite zeq_false; auto.
rewrite zle_lt_true; try omega.
unfold enqueue_atomic_spec; simpl.
repeat rewrite ZMap.gss. repeat rewrite ZMap.set2.
repeat match goal with
| |- context[MultiDef (?a :: ?l)] ⇒
let l´ := fresh "l_temp" in
set (l´ := a :: l) in ×
end.
match goal with
| |- context[acquire_lock_ABTCB_spec _ ?a] ⇒
set (a´:= labd {abtcb: ZMap.set wk_id (AbTCBValid tds cpu_id (-1)) t_lock}
{abq: ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock}
{multi_log: ZMap.set (slp_q_id cv 0 + ID_AT_range)
(MultiDef l_temp0) (multi_log labd)}
{lock: ZMap.set (slp_q_id cv 0 + ID_AT_range) LockFalse (lock labd)});
assert (Ha_eq: a = a´)
end.
{
reflexivity.
}
rewrite Ha_eq. clear Ha_eq.
rewrite ZMap.gso in Hdestruct11; eauto.
assert (Hacq: ∃ t_lock´ q_lock´,
acquire_lock_ABTCB_spec (msg_q_id cpu_id) a´ =
Some (labd
{multi_log
: ZMap.set ((msg_q_id cpu_id) + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID
(TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get ((msg_q_id cpu_id) + ID_AT_range)
(multi_oracle labd) current_CPU_ID l3 ++ l3))
(multi_log a´)}
{lock : ZMap.set ((msg_q_id cpu_id) + ID_AT_range) (LockOwn true) (lock a´)}
{abtcb : t_lock´} {abq : q_lock´})
∧ (t_lock´, q_lock´) = match ZMap.get (msg_q_id cpu_id) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (ZMap.set wk_id (AbTCBValid tds cpu_id (-1)) t_lock,
ZMap.set (slp_q_id cv 0) (AbQValid l0) q_lock)
end).
{
unfold acquire_lock_ABTCB_spec.
subst a´; simpl.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite ZMap.gso; eauto.
rewrite <- H3.
rewrite ZMap.gso; eauto.
assert (Hlock´: ZMap.get ((msg_q_id cpu_id) + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
rewrite Hlock´. rewrite Hcal´´; simpl.
erewrite MultiLogMap2id_get_shared; eauto.
unfold AbTCBPool, AbQueuePool, ZMap.t, PMap.t in ×.
subdestruct_match_one.
- destruct p as (nt, nq).
subdestruct_match_one.
refine_split´; eauto. reflexivity.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock´ & q_lock´ & → & Htq_eq´).
unfold enqueue0_spec; simpl.
subrewrite´.
unfold Queue_arg.
rewrite zle_lt_true; eauto.
rewrite zle_lt_true; eauto.
unfold AbTCBPool, AbQueuePool, ZMap.t, PMap.t in ×.
rewrite <- Htq_eq´ in Hdestruct11. clear Htq_eq´.
destruct (ZMap.get (msg_q_id cpu_id) q_lock´); contra_inv.
destruct (ZMap.get wk_id t_lock´); contra_inv.
subdestruct_match_one.
subdestruct_match_one.
rewrite zeq_true in Hdestruct11. inv Hdestruct11.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´. rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.gss. simpl.
exploit (H_CalLock_rel (ZMap.set wk_id (AbTCBValid tds0 cpu_id (msg_q_id cpu_id)) t_lock´)
(ZMap.set (msg_q_id cpu_id) (AbQValid (l1 ++ wk_id :: nil)) q_lock´)); eauto.
intros (y´´ & ->); simpl.
repeat rewrite ZMap.set2.
repeat rewrite ZMap.gss.
refine_split´; eauto.
{
econstructor; eauto; simpl.
- congruence.
- subst l_temp1 l_temp0.
inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (msg_q_id cpu_id) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ assert(MultiLogMap2id nil (msg_q_id cpu_id) nil) by constructor.
exploit (BIGMAP_CONS (TEVENT current_CPU_ID (TSHARED (OTDWAKE_DIFF wk_id cpu_id)))
(TEVENT current_CPU_ID (TSHARED (OTDWAKE cv))
:: ZMap.get lock_range (multi_oracle habd) current_CPU_ID l ++ l)); eauto.
econstructor; eauto.
econstructor; eauto.
reflexivity.
eapply MultiE2id_EQ; eauto.
reflexivity.
rewrite ZMap.gss.
reflexivity.
+ simpl.
rewrite zeq_true by reflexivity.
reflexivity.
}
{
rewrite ZMap.gso; eauto.
destruct (zeq (slp_q_id cv 0) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ assert(MultiLogMap2id nil (msg_q_id cpu_id) nil) by constructor.
exploit (BIGMAP_CONS (TEVENT current_CPU_ID (TSHARED (OTDWAKE_DIFF wk_id cpu_id)))
(TEVENT current_CPU_ID (TSHARED (OTDWAKE cv))
:: ZMap.get lock_range (multi_oracle habd) current_CPU_ID l ++ l)); eauto.
econstructor; eauto.
eapply MultiE2id_EQ; eauto.
reflexivity.
rewrite ZMap.gss.
reflexivity.
econstructor; eauto.
reflexivity.
+ simpl.
rewrite zeq_true by reflexivity.
reflexivity.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre2 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log1.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
econstructor.
reflexivity.
assumption.
eapply add_aux; eauto.
}
eapply add_aux; eauto.
}
- eapply lock_re_gss´; eauto.
eapply lock_re_gss´; eauto.
rewrite ZMap.gso; eauto.
rewrite <- lock_re0.
rewrite Hdestruct13. trivial.
- econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
subst l4. unfold CalTCB_log in Hcal.
unfold AbTCBPool, AbQueuePool, ZMap.t, PMap.t in ×.
rewrite Hcal_real in Hcal. inv Hcal.
repeat rewrite ZMap.gss.
refine_split´; trivial.
}
Fail idtac.
Qed.
End WAKEUP.
Section SPAWN.
Lemma big_thread_spawn_exist:
∀ s habd habd´ labd b b´ ofs´ id q n
(Hhigh: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd) f,
biglow_thread_spawn_spec habd b b´ ofs´ id q = Some (habd´, n)
→ relate_AbData s f habd labd
→ find_symbol s STACK_LOC = Some b
→ (∃ id, find_symbol s id = Some b´)
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ ∃ labd´, thread_spawn_spec labd b b´ ofs´ id q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_thread_spawn_spec, thread_spawn_spec.
intros until f; intros HP HR Hsys Hsys´ Hincr.
pose proof HR as HR´. inv HR´.
revert HP. subrewrite. subdestruct; inv HQ; simpl.
pose proof abtcb_re0 as Htcb. inv Htcb.
unfold CalTCB_log_real in ×.
subdestruct_match_one.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1).
pose proof Hdestruct10 as Hcal_t.
unfold CalTCB_log in Hdestruct10. simpl in Hdestruct10.
subdestruct_match_one.
destruct p as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv Hhigh; assumption.
}
rewrite HCPU in ×.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l0 = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
inv abtcb_re0.
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
subdestruct; try omega; simpl.
inv Hdestruct10; simpl.
refine_split´; eauto.
econstructor; simpl; eauto.
- congruence.
- inv multi_log_re0.
econstructor.
× intros. rewrite ZMap.gso.
eauto.
eapply lock_neq in H0; eauto.
× intros. rewrite ZMap.gss.
exploit Hdiff; eauto.
erewrite Hdestruct8. intros HF. inv HF.
econstructor; eauto.
inv multi_oracle_re0.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
- kctxt_inj_simpl.
+ destruct Hsys´ as [id´ Hsys´].
eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply stencil_find_symbol_inject´; eauto.
+ rewrite Int.add_zero; trivial.
+ eapply kctxt_re0; eauto. omega.
- econstructor. rewrite ZMap.gss.
intros. inv Hlog.
rewrite Hcal_t in Hcal. inv Hcal.
refine_split´; trivial.
Fail idtac.
Qed.
End SPAWN.
Lemma relate_tcb_gso:
∀ i l bl t q s c,
relate_tcb bl t q s c →
lock_range ≠ i →
relate_tcb (ZMap.set i l bl) t q s c.
Proof.
intros. inv H. econstructor; eauto.
rewrite ZMap.gso; eauto.
Qed.
Lemma relate_tcb_gso´:
∀ i ofs r l bl t q s c,
relate_tcb bl t q s c →
index2Z i ofs = Some r →
relate_tcb (ZMap.set r l bl) t q s c.
Proof.
intros. eapply relate_tcb_gso; eauto.
eapply lock_neq; eauto.
Qed.
Lemma palloc_exist:
∀ s habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re0. eapply (Hsame 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re0. eapply (Hsame 0 0); auto. omega.
}
rewrite Horacle.
erewrite lock_re0.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso 0 0); eauto. omega.
+ eapply (relate_tcb_gso´ 0 0); eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso 0 0); eauto. omega.
+ eapply (relate_tcb_gso´ 0 0); eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso 0 0); eauto. omega.
+ eapply (relate_tcb_gso´ 0 0); eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ s habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f, ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma index2Z_eq´:
∀ i,
0 ≤ i < num_chan →
index2Z 2 i = Some (i + lock_TCB_range).
Proof.
unfold index2Z.
unfold index_incrange, index_range.
intros.
unfold ID_SC_range. rewrite zle_lt_true; trivial.
f_equal. omega.
Qed.
Lemma acquire_lock_SC_exist:
∀ s i habd habd´ labd f,
acquire_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_SC_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_SC_spec; intros.
pose proof H0 as HR. inv H0.
revert H. rewrite lock_re0.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + lock_TCB_range) (multi_log habd)
= ZMap.get (i + lock_TCB_range) (multi_log labd)).
{
inv multi_log_re0. eapply (Hsame ID_SC i); auto.
omega. eapply index2Z_eq´; eauto.
}
assert (Horacle: ZMap.get (i + lock_TCB_range) (multi_oracle habd)
= ZMap.get (i + lock_TCB_range) (multi_oracle labd)).
{
inv multi_oracle_re0. eapply (Hsame ID_SC i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog, <- Horacle.
subdestruct; inv HQ.
- refine_split´; trivial.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso ID_SC i); eauto. omega.
eapply index2Z_eq´; eauto.
+ eapply lock_re_gss; eauto.
+ eapply (relate_tcb_gso´ ID_SC i); eauto.
eapply index2Z_eq´; eauto.
- refine_split´; trivial.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso ID_SC i); eauto. omega.
eapply index2Z_eq´; eauto.
+ eapply lock_re_gss; eauto.
+ eapply (relate_tcb_gso´ ID_SC i); eauto.
eapply index2Z_eq´; eauto.
Qed.
Lemma release_lock_SC_exist:
∀ s i habd habd´ labd f,
release_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_SC_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_SC_spec; intros.
pose proof H0 as HR. inv H0.
revert H. rewrite lock_re0.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + lock_TCB_range) (multi_log habd)
= ZMap.get (i + lock_TCB_range) (multi_log labd)).
{
inv multi_log_re0. eapply (Hsame ID_SC i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog.
subdestruct; inv HQ.
refine_split´; trivial.
constructor; eauto; simpl.
+ eapply (relate_Thread_Log_Pool_gso ID_SC i); eauto. omega.
eapply index2Z_eq´; eauto.
+ eapply lock_re_gss; eauto.
+ eapply (relate_tcb_gso´ ID_SC i); eauto.
eapply index2Z_eq´; eauto.
Qed.
Section YIELD.
Lemma thread_yield_exist:
∀ habd habd´ labd rs r´ rs0 s
(HINV: PQThread.high_level_invariant habd)
(HLINV: PThread.high_level_invariant labd)f,
biglow_thread_yield_spec
habd (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) = Some (habd´, rs0)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t,
val_inject f (Pregmap.get reg rs) (Pregmap.get reg r´))
→ ∃ labd´ r´0 ofs, thread_yield_spec
labd (Pregmap.init Vundef)#ESP <- (r´#ESP)#EDI <- (r´#EDI)#ESI <- (r´#ESI)
#EBX <- (r´#EBX)#EBP <- (r´#EBP)#RA <- (r´#RA) = Some (labd´, r´0)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r,
ZtoPreg i = Some r → val_inject f (rs0#r) (r´0#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = r´0.
Proof.
Opaque remove.
unfold thread_yield_spec, biglow_thread_yield_spec; intros until f.
intros HP HR HVL; pose proof HR as HR´; inv HR; revert HP.
specialize (PQThread.CPU_ID_range _ HINV).
specialize (PQThread.valid_curid _ HINV).
subrewrite´. intros HCPU_range Hcid Hhigh.
subdestruct; contra_inv.
inv Hhigh.
assert (HOS1: MSG_Q_START ≤ (msg_q_id (CPU_ID labd)) < num_chan).
{
unfold msg_q_id. omega.
}
assert (HOS2: 0 ≤ (msg_q_id (CPU_ID labd)) < num_chan).
{
omega.
}
pose proof multi_log_re0 as Hrel_log´.
inv multi_log_re0. specialize (Hdiff _ HOS1).
rewrite Hdestruct5 in Hdiff. inv Hdiff.
pose proof multi_oracle_re0 as Hrel_oracle´.
inv multi_oracle_re0. specialize (Hdiff _ HOS1).
inv Hdiff. exploit (Hpre (CPU_ID labd)); eauto.
intros Hrel_log_oracle.
assert (HCPU: (CPU_ID labd) = current_CPU_ID).
{
rewrite <- CPU_ID_re0.
inv HINV; assumption.
}
rewrite HCPU in ×.
inv abtcb_re0.
exploit (MultiLogMap2id_imply_HCal_wait local_lock_bound current_CPU_ID); eauto.
{
unfold local_lock_bound; omega.
}
intros (x & Hcal). rename Hdestruct6 into Hcal_tcb´.
unfold CalTCB_log_real in Hcal_tcb´.
subdestruct_match_one. inv Hcal_tcb´.
destruct p as (((((t1 & q1) & s1) & curid1) & cached1) & res1). inv H1.
unfold thread_poll_pending_spec, dequeue_atomic_spec.
pose proof Hdestruct6 as tcbinv.
unfold CalTCB_log in tcbinv; simpl in tcbinv.
subdestruct_match_one.
destruct p as (((((t2 & q2) & s2) & curid2) & cached2) & res2).
assert (Hlock: ZMap.get (msg_q_id current_CPU_ID + ID_AT_range) (lock labd) = LockFalse).
{
rewrite <- lock_re0. eauto.
}
assert (Hacq: ∃ t_lock q_lock,
acquire_lock_ABTCB_spec (msg_q_id (CPU_ID labd)) labd =
Some (labd
{multi_log
: ZMap.set ((msg_q_id (CPU_ID labd)) + ID_AT_range)
(MultiDef
(TEVENT current_CPU_ID (TSHARED OPULL) ::
TEVENT current_CPU_ID
(TTICKET (WAIT_LOCK local_lock_bound))
:: ZMap.get ((msg_q_id (CPU_ID labd)) + ID_AT_range)
(multi_oracle labd) current_CPU_ID l2 ++ l2))
(multi_log labd)}
{lock : ZMap.set ((msg_q_id (CPU_ID labd)) + ID_AT_range) (LockOwn true) (lock labd)}
{abtcb : t_lock} {abq : q_lock})
∧ (t_lock, q_lock) = match ZMap.get (msg_q_id (CPU_ID labd)) cached2 with
| Some (t0, q0) ⇒ (t0, q0)
| None ⇒ (t2, q2)
end
∧ ZMap.get current_CPU_ID (sleeper labd) = s2
∧ ZMap.get current_CPU_ID (cid labd) = curid2).
{
unfold acquire_lock_ABTCB_spec.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite <- H.
rewrite Hcal. simpl.
erewrite MultiLogMap2id_get_shared; eauto.
assert (Hcal_same: ∃ cached3 res3, CalTCB_log l = Some (t2, q2, s2, curid2, cached3, res3)).
{
exploit CalTCB_log_gso´; eauto.
}
destruct Hcal_same as (cached3 & res3 & Hcal_same).
exploit Hpre0; eauto.
intros (? & ? & ? & ?); subst.
destruct (ZMap.get (msg_q_id current_CPU_ID) cached2) eqn: Hcache.
- destruct p.
refine_split´; eauto.
- refine_split´; eauto.
f_equal.
}
destruct Hacq as (t_lock & q_lock & → & Htq_eq & Hsleep´ & Hcid´).
rewrite HCPU in ×.
rewrite <- Htq_eq in tcbinv.
unfold dequeue0_spec; simpl.
subrewrite´.
rewrite zle_lt_true by omega.
clear Htq_eq.
d2 subdestruct_match_one; contra_inv.
- subdestruct; contra_inv; try omega.
inv tcbinv. subst.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´; simpl.
rewrite zle_lt_true by omega.
repeat rewrite ZMap.gss.
exploit (H_CalLock_rel t_lock q_lock); eauto.
intros (y´ & ->); simpl. repeat rewrite ZMap.set2.
subrewrite´; simpl.
refine_split´; eauto.
econstructor; simpl; eauto.
+ congruence.
+ inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (msg_q_id current_CPU_ID) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
+ eapply lock_re_gss´; eauto.
+ kctxt_inj_simpl.
+ econstructor; eauto.
rewrite ZMap.gss. intros. inv Hlog.
rewrite Hdestruct6 in Hcal0. inv Hcal0.
repeat rewrite ZMap.gss.
refine_split´; trivial.
+ intros. eapply kctxt_re0; eauto.
- subdestruct; contra_inv; try omega.
inv tcbinv; simpl. subst.
unfold release_lock_ABTCB_spec; simpl.
subrewrite´; simpl.
rewrite zle_lt_true by omega.
repeat rewrite ZMap.gss.
exploit (H_CalLock_rel (ZMap.set z (AbTCBValid tds cpuid (-1)) t_lock)
(ZMap.set (msg_q_id current_CPU_ID)
(AbQValid l1) q_lock)); eauto.
intros (y´ & ->); simpl. repeat rewrite ZMap.set2.
rewrite zle_lt_true; trivial.
rewrite ZMap.gso; eauto.
assert (Hcused: cused (ZMap.get z (AC labd)) = true).
{
inv Hdestruct9. trivial.
}
rewrite Hdestruct16. rewrite zle_lt_true; trivial. rewrite Hcused; simpl.
rewrite ZMap.gss.
rewrite ZMap.gso; eauto.
subrewrite´; simpl.
assert (Hget: ∃ t b,
ZMap.get run_id (ZMap.set z (AbTCBValid READY current_CPU_ID (rdy_q_id current_CPU_ID)) t_lock)
= AbTCBValid t current_CPU_ID b).
{
destruct (zeq run_id z); subst.
- rewrite ZMap.gss. eauto.
- rewrite ZMap.gso; eauto.
}
destruct Hget as (t & b & ->).
rewrite zeq_true; simpl.
refine_split´; try eapply a; eauto.
econstructor; simpl; eauto.
+ congruence.
+ inv Hrel_log´. econstructor.
× intros. rewrite ZMap.gso.
rewrite ZMap.gso; eauto.
eapply TCB_range_neq in H1; eauto.
eapply lock_neq in H1; eauto.
× intros. rewrite ZMap.gss.
destruct (zeq (msg_q_id current_CPU_ID) i); subst.
{
rewrite ZMap.gss.
econstructor. econstructor.
+ econstructor; eauto.
eapply MultiE2id_EQ; eauto.
{ simpl. trivial. }
{
rewrite ZMap.gss. eauto.
}
+ simpl. repeat rewrite zeq_true. trivial.
}
{
rewrite ZMap.gso; eauto.
exploit Hdiff; eauto.
erewrite Hdestruct5. intros HF. inv HF.
econstructor; eauto.
inv Hrel_oracle´.
exploit Hdiff0; eauto.
intros HF. inv HF.
exploit (Hpre1 current_CPU_ID); eauto.
intro map2id.
inv Hrel_log0.
erewrite <- remove_cache_event_eq; eauto.
econstructor; try reflexivity; eauto.
rewrite <- app_nil_l.
econstructor; try reflexivity; eauto.
econstructor; eauto.
reflexivity.
eapply add_aux; eauto.
}
+ eapply lock_re_gss´; eauto.
+ kctxt_inj_simpl.
+ econstructor; eauto.
rewrite ZMap.gss. intros. repeat rewrite ZMap.set2.
inv Hlog.
rewrite Hdestruct6 in Hcal0. inv Hcal0.
repeat rewrite ZMap.gss.
refine_split´; trivial.
+ intros. eapply kctxt_re0; eauto.
+ eapply msg_neq.
Fail idtac.
Qed.
End YIELD.
End Exists.
Section PASSTHROUGH_PRIM.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
Qed.
Lemma get_curid_exist:
∀ s habd labd z f,
get_curid_spec habd = Some z
→ relate_AbData s f habd labd
→ get_curid_spec labd = Some z.
Proof.
unfold get_curid_spec; intros.
inv H0.
revert H;
subrewrite.
Qed.
Lemma get_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_curid_spec)
(id ↦ gensem get_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_curid_exist; eauto. reflexivity.
Qed.
Lemma lock_SC_range:
∀ ofs z
(Hindex: index2Z 2 ofs = Some z),
z ≠ lock_range.
Proof.
intros. unfold lock_range. functional inversion Hindex. subst.
functional inversion H0; subst. simpl in H1.
inv H1. unfold lock_TCB_range, ID_SC_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma lock_SC_range´:
∀ ofs z i
(Hindex: index2Z 2 ofs = Some z)
(Hrange: MSG_Q_START ≤ i < num_chan),
z ≠ i + ID_AT_range.
Proof.
intros. functional inversion Hindex. subst.
functional inversion H0; subst. simpl in H1.
inv H1. unfold lock_TCB_range, ID_SC_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. simpl in ×.
exploit Hsame; eauto. omega.
intros Hlog. rewrite <- Hlog. rewrite Hdestruct7.
erewrite <- lock_re0. rewrite Hdestruct8.
exploit page_copy_aux_exists; eauto.
intros Hpage. rewrite Hpage.
rewrite Hdestruct11.
refine_split´; try trivial.
econstructor; simpl; eauto.
- constructor; intros.
+ destruct (zeq r z); subst.
× repeat rewrite ZMap.gss. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq: z ≠ lock_range).
{
eapply lock_SC_range; eauto.
}
assert (Hneq´: z ≠ i0 + ID_AT_range).
{
eapply lock_SC_range´; eauto.
}
repeat rewrite ZMap.gso; eauto.
- constructor. intros.
assert (Hneq: z ≠ lock_range).
{
eapply lock_SC_range; eauto.
}
rewrite ZMap.gso in Hlog0; eauto.
inv abtcb_re0. eauto.
Qed.
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.
generalize H0; intro relateD.
inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
exploit page_copy_exist; eauto.
intros (labd´ & Hpage & Hrel).
rewrite Hpage.
refine_split´; trivial.
inv Hrel. econstructor; eauto.
rewrite syncchpool_re1. trivial.
Qed.
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.
Qed.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re0 as multi_log_re´.
inv multi_log_re0. simpl in ×.
exploit Hsame; eauto. omega.
intros Hlog. rewrite <- Hlog. rewrite Hdestruct7.
erewrite <- lock_re0. rewrite Hdestruct8.
rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & Hback & Hinj). rewrite Hback.
refine_split´; try trivial.
econstructor; simpl; eauto.
Qed.
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.
generalize H0; intro relateD.
inv H0.
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.
exploit relate_impl_syncchpool_update; eauto.
Qed.
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.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pqthread_passthrough pthread.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1. intros (labd´ & HP & HM).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit big_thread_spawn_exist; eauto 1; intros (labd´ & HP & HM).
destruct H8 as [fun_id Hsys].
exploit stencil_find_symbol_inject´; eauto. intros HFB.
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit big_thread_wakeup_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit thread_yield_exist; eauto 1.
intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
+ eapply kctxt_INJECT; try assumption.
+ eapply kctxt_INJECT; try assumption.
-
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit big_thread_sleep_exist; eauto 1.
intros (labd´ & rs0´ & ofs & HP & HM & Hrinj´ & HOS´ & Hr). subst. subst rs3.
exploit low_level_invariant_impl_eq; eauto. inversion 1.
match_external_states_simpl; try (eapply Hrinj´; eapply PregToZ_correct; reflexivity).
+ inv H9. inv H3. simpl in ×.
exploit Mem.loadv_inject; try eassumption.
val_inject_simpl. unfold Pregmap.get.
intros (v2 & HL & Hv). inv Hv. assumption.
+ eapply kctxt_INJECT; try assumption.
+ eapply kctxt_INJECT; try assumption.
-
intros. layer_sim_simpl.
simpl. constructor.
split; simpl; [|reflexivity|reflexivity|repeat constructor].
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd match_RData.
exploit big_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr _ _ ⇒ eapply inject_incr_refl
| _ ⇒ idtac
end.
repeat (econstructor). eapply HP.
constructor. econstructor; try eassumption. constructor.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit acquire_lock_SC_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit release_lock_SC_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
- apply get_sync_chan_busy_sim.
- apply set_sync_chan_busy_sim.
- apply ipc_send_body_sim.
- apply ipc_receive_body_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply proc_create_postinit_sim.
- apply trapin_sim.
- apply trapout_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End PASSTHROUGH_PRIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.