Library mcertikos.objects.ObjBigThread
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalTicketLock.
Require Import DeviceStateDataType.
Require Export ObjInterruptDriver.
Require Import BigStepLogReplay.
Require Import CommonTactic.
Require Import GlobalOracle.
Require Import LogReplay.
Require Import ObjLMM0.
Section OBJ_Thread.
Context `{real_params: RealParams}.
Context `{oracle_ops: MultiOracleOps}.
Function big_palloc_spec (n: Z) (adt: RData): option (RData × Z) :=
let abid := 0 in
let cpu := CPU_ID adt in
let c := ZMap.get n (AC adt) in
match (ikern adt, ihost adt, pg adt, ipt adt, cused c) with
| (true, true, true, true, true) ⇒
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
if (cusage c) <? (cquota c) then
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
match B_CalAT_log_real l1 with
| Some a ⇒
match first_free a (nps adt) with
| inleft (exist i _) ⇒
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE (ZMap.get (CPU_ID adt) (cid adt)) i))) :: l1 in
Some (adt {big_log: BigDef l´}
{LAT: ZMap.set i (LATCValid nil) (LAT adt)}
{pperm: ZMap.set i PGAlloc (pperm adt)}
{AC: ZMap.set n cur (AC adt)},i)
| _ ⇒
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE (ZMap.get (CPU_ID adt) (cid adt)) 0))) :: l1 in
Some (adt{big_log: BigDef l´}, 0)
end
| _ ⇒ None
end
else
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE (ZMap.get (CPU_ID adt) (cid adt)) 0))) :: l1 in
Some (adt{big_log: BigDef l´}, 0)
| _,_ ⇒ None
end
| _ ⇒ None
end.
Lemma big_palloc_inv_prop:
∀ n d d´ v,
big_palloc_spec n d = Some (d´, v) →
ptpool d´ = ptpool d
∧ (v ≠ 0 →
ZMap.get v (pperm d´) = PGAlloc
∧ ZMap.get v (LAT d´) = LATCValid nil
∧ 0 < v < nps d´)
∧ pg d´ = true.
Proof.
unfold big_palloc_spec. intros.
subdestruct; inv H; simpl; subst.
- repeat rewrite ZMap.gss. refine_split´; trivial.
destruct a0 as (? & ? & ?). intros.
refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
Definition real_multi_log´ := real_multi_log_pb (Z.to_nat (lock_range+1)).
Function biglow_sched_init_spec (mbi_adr:Z) (adt: RData) : option RData :=
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, true, true, true, false) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
{lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
} {ioapic / s / CurrentIrq: None}
{vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{multi_log: real_multi_log´ (multi_log adt)}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde adt)}
{smspool: real_smspool (smspool adt)}
{syncchpool: real_syncchpool (syncchpool adt)}
{cid: real_cidpool (cid adt)}
else None
else None
| _ ⇒ None
end.
Function big_sched_init_spec (mbi_adr:Z) (adt: RData) : option RData :=
match (init adt, pg adt, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, true, true, true, false) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
{lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
} {ioapic / s / CurrentIrq: None}
{vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{big_log: BigDef nil}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde adt)}
{smspool: real_smspool (smspool adt)}
{syncchpool: real_syncchpool (syncchpool adt)}
{cid: real_cidpool (cid adt)}
else None
else None
| _ ⇒ None
end.
Definition IsCused (t: option Z) (ac: ContainerPool) :=
match t with
| None ⇒ true
| Some i ⇒ cused (ZMap.get i ac)
end.
Function biglow_thread_yield_spec (adt: RData) (rs: KContext) : option (RData × KContext) :=
let cpu := CPU_ID adt in
let curid := (ZMap.get (CPU_ID adt) (cid adt)) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
match ZMap.get lock_range (multi_log adt), ZMap.get (msg_q_id cpu + ID_AT_range) (lock adt),
cused (ZMap.get curid (AC adt)) with
| MultiDef l, LockFalse, true ⇒
let to := ZMap.get lock_range (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let e := TSHARED (OTDYIELD curid) in
let l´ := (TEVENT cpu e) :: l1 in
match CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if IsCused t (AC adt) then
Some (adt {multi_log: ZMap.set lock_range (MultiDef l´) (multi_log adt)}
{kctxt: ZMap.set curid rs (kctxt adt)}
{cid: (ZMap.set (CPU_ID adt) la (cid adt))}
, ZMap.get la (kctxt adt))
else None
else None
| _ ⇒ None
end
| _, _, _ ⇒ None
end
| _ ⇒ None
end.
Function big_thread_yield_spec (adt: RData) (rs: KContext) : option (RData × KContext) :=
let cpu := CPU_ID adt in
let curid := (ZMap.get (CPU_ID adt) (cid adt)) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
match big_log adt, ZMap.get (msg_q_id cpu + ID_AT_range) (lock adt), cused (ZMap.get curid (AC adt)) with
| BigDef l, LockFalse, true ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDYIELD curid) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if IsCused t (AC adt) then
Some (adt {big_log: BigDef l´}
{kctxt: ZMap.set curid rs (kctxt adt)}
{cid: (ZMap.set (CPU_ID adt) la (cid adt))}
, ZMap.get la (kctxt adt))
else None
else None
| _ ⇒ None
end
| _, _, _ ⇒ None
end
| _ ⇒ None
end.
Function biglow_thread_sleep_spec (adt: RData) (rs: KContext) (cv: Z): option (RData × KContext) :=
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match ZMap.get lock_range (multi_log adt), ZMap.get abid (lock adt),
ZMap.get sc_id (multi_log adt), ZMap.get sc_id (lock adt),
cused (ZMap.get curid (AC adt)) with
| MultiDef l, LockFalse, MultiDef sc_l, LockOwn true, true ⇒
let to := ZMap.get lock_range (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let e1 := TSHARED (OTDSLEEP curid cv (syncchpool adt)) in
let l´ := (TEVENT cpu e1) :: l1 in
let sc_e := TSHARED (OSCE (syncchpool adt)) in
let sc_l´ := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu sc_e :: sc_l in
match CalTCB_log_real l´, H_CalLock sc_l´ with
| Some (TCB_RID la), Some _ ⇒
if zle_lt 0 la num_proc then
Some (adt {multi_log: ZMap.set sc_id (MultiDef sc_l´)
(ZMap.set lock_range (MultiDef l´) (multi_log adt))}
{kctxt: ZMap.set curid rs (kctxt adt)}
{cid: (ZMap.set (CPU_ID adt) la (cid adt))}
{lock: ZMap.set sc_id LockFalse (ZMap.set abid LockFalse (lock adt))}
, ZMap.get la (kctxt adt))
else None
| _, _ ⇒ None
end
| _,_,_,_,_ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function big_thread_sleep_spec (adt: RData) (rs: KContext) (cv: Z): option (RData × KContext) :=
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get abid (lock adt), ZMap.get sc_id (lock adt),
cused (ZMap.get curid (AC adt)) with
| BigDef l, LockFalse, LockOwn true, true ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSLEEP curid cv (syncchpool adt)) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´, B_CalLock sc_id l, B_CalLock sc_id l1 with
| Some (TCB_RID la), Some (S (S _), LHOLD, Some cpu´), Some _ ⇒
if zle_lt 0 la num_proc then
if zeq cpu cpu´ then
Some (adt {big_log: BigDef l´}
{kctxt: ZMap.set curid rs (kctxt adt)}
{cid: (ZMap.set (CPU_ID adt) la (cid adt))}
{lock: ZMap.set sc_id LockFalse (ZMap.set abid LockFalse (lock adt))}
, ZMap.get la (kctxt adt))
else None
else None
| _,_,_ ⇒ None
end
| _,_,_,_ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function biglow_thread_wakeup_spec (cv: Z) (adt: RData) :=
let me := CPU_ID adt in
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
let n := slp_q_id cv 0 in
if zle_lt 0 cv num_cv then
match ZMap.get lock_range (multi_log adt), ZMap.get (n + ID_AT_range) (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get lock_range (multi_oracle adt) in
let l1 := (to me l) ++ l in
let e := TSHARED (OTDWAKE cv) in
let l´ := (TEVENT me e) :: l1 in
match CalTCB_log_real l´ with
| Some (TCBWAKE_F) ⇒
Some (adt {multi_log: ZMap.set lock_range (MultiDef l´) (multi_log adt)}, 0)
| Some (TCBWAKE_T tid) ⇒
match cused (ZMap.get tid (AC adt)) with
| true ⇒
Some (adt {multi_log: ZMap.set lock_range (MultiDef l´) (multi_log adt)}, 1)
| _ ⇒ None
end
| Some (TCBWAKE tid cpu´) ⇒
let e´ := TSHARED (OTDWAKE_DIFF tid cpu´) in
let l´´ := (TEVENT me e´) :: l´ in
match CalTCB_log_real l´´,
ZMap.get (msg_q_id cpu´ + ID_AT_range) (lock adt),
cused (ZMap.get tid (AC adt)) with
| Some _, LockFalse, true ⇒
Some (adt {multi_log: ZMap.set lock_range (MultiDef l´´) (multi_log adt)}, 1)
| _, _,_ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
| _ ⇒ None
end.
Function big_thread_wakeup_spec (cv: Z) (adt: RData) :=
let me := CPU_ID adt in
match (ikern adt, pg adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
let n := slp_q_id cv 0 in
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get (n + ID_AT_range) (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to me l) ++ l in
let e := TBSHARED (BTDWAKE (ZMap.get (CPU_ID adt) (cid adt)) cv) in
let l´ := (TBEVENT me e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCBWAKE_F) ⇒
Some (adt {big_log: BigDef l´}, 0)
| Some (TCBWAKE_T tid) ⇒
match cused (ZMap.get tid (AC adt)) with
| true ⇒
Some (adt {big_log: BigDef l´}, 1)
| _ ⇒ None
end
| Some (TCBWAKE tid cpu´) ⇒
let e´ := TBSHARED (BTDWAKE_DIFF (ZMap.get (CPU_ID adt) (cid adt)) cv tid cpu´) in
let l´´ := (TBEVENT me e´) :: l´ in
match B_CalTCB_log_real l´´,
ZMap.get (msg_q_id cpu´ + ID_AT_range) (lock adt),
cused (ZMap.get tid (AC adt)) with
| Some _, LockFalse, true ⇒
Some (adt {big_log: BigDef l´´}, 1)
| _,_,_ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
| _ ⇒ None
end.
Definition biglow_thread_spawn_spec (adt: RData) (b: block) (b´:block) (ofs´: int) id q : option (RData× Z) :=
let cpu := CPU_ID adt in
let c := ZMap.get id (AC adt) in
let i := id × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (pg adt, ikern adt, ihost adt, ipt adt,cused c, cused (ZMap.get i (AC adt)), zlt_lt 0 i num_proc,
zlt (Z_of_nat (length (cchildren c))) max_children,
zle_le 0 q (cquota c - cusage c)) with
| (true, true, true, true, true, false, left _, left _, left _) ⇒
let child := mkContainer q 0 id nil true in
let parent := (mkContainer (cquota c) (cusage c + q)
(cparent c) (i :: cchildren c) (cused c)) in
match ZMap.get lock_range (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get lock_range (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let e := TSHARED (OTDSPAWN i) in
let l´ := (TEVENT cpu e) :: l1 in
match CalTCB_log_real l´ with
| Some _ ⇒
let ofs := Int.repr ((i + 1) × PgSize -4) in
let rs := ((ZMap.get i (kctxt adt))#SP <- (Vptr b ofs))#RA <- (Vptr b´ ofs´) in
Some (adt {multi_log: ZMap.set lock_range (MultiDef l´) (multi_log adt)}
{AC: ZMap.set i child (ZMap.set id parent (AC adt))}
{kctxt: ZMap.set i rs (kctxt adt)}, i)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function big_release_lock_SC_spec (index:Z) (adt: RData) :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
match (pg adt, ikern adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockOwn true ⇒
let e := TBLOCK abid (BREL_LOCK (ZMap.get (CPU_ID adt) (cid adt)) (syncchpool adt)) in
let l´ := (TBEVENT cpu e) :: l in
match B_CalLock abid l´ with
| Some _ ⇒
Some (adt {big_log: BigDef l´}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Definition big_acquire_lock_SC_spec (index: Z) (adt: RData) :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 index num_chan then
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let l´ := (TBEVENT cpu (TBLOCK abid (BWAIT_LOCK (ZMap.get (CPU_ID adt) (cid adt)) local_lock_bound))) :: l1 in
match B_CalLock abid l´ with
| Some _ ⇒
match B_GetSharedSC abid l´ with
| Some e ⇒
Some (adt {big_log: BigDef l´}
{lock: ZMap.set abid (LockOwn true) (lock adt)} {syncchpool: e})
| _ ⇒
Some (adt {big_log: BigDef l´}
{lock: ZMap.set abid (LockOwn true) (lock adt)})
end
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Lemma big_acquire_lock_SC_lock_status:
∀ n d d´,
big_acquire_lock_SC_spec n d = Some d´ →
ZMap.get (n + lock_TCB_range) (lock d´) = LockOwn true.
Proof.
unfold big_acquire_lock_SC_spec. intros.
subdestruct; inv H; simpl.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gss. trivial.
Qed.
Require Import ObjFlatMem.
Function big_page_copy_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, ipt adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get (PageI from) (pperm adt) with
| PGAlloc ⇒
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TBEVENT cpu (TBSHARED (BBUFFERE (ZMap.get cpu (cid adt)) cv b)) :: l in
match B_CalLock abid l´ with
| Some _ ⇒ Some adt {big_log: BigDef l´}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function big_page_copy_back_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, ipt adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get (PageI to) (pperm adt) with
| PGAlloc ⇒
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockOwn true ⇒
match B_GetSharedBuffer abid l, B_CalLock abid l with
| Some b, Some (_, LHOLD, Some cpu_id) ⇒
if zeq cpu_id (CPU_ID adt) then
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
else None
| _, _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Require Import ObjCV.
Function big_ipc_receive_body_spec (chid vaddr rcount : Z) (adt : RData) : option (RData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid sender spaddr scount busy ⇒
let arecvcount := Z.min (Int.unsigned scount) rcount in
match big_page_copy_back_spec chid arecvcount vaddr adt with
| Some adt1 ⇒
Some (adt1 {syncchpool: ZMap.set chid
(SyncChanValid sender spaddr Int.zero busy)
(syncchpool adt1)}, arecvcount)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function big_ipc_send_body_spec (chid vaddr scount : Z) (adt : RData) : option (RData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
match (pg adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool adt) with
| SyncChanValid sender spaddr _ busy ⇒
let asendval := Z.min (scount) (1024) in
match big_page_copy_spec chid asendval vaddr adt with
| Some adt´ ⇒
Some (adt´ {syncchpool :
ZMap.set chid
(SyncChanValid sender spaddr (Int.repr asendval) busy)
(syncchpool adt´)}, asendval)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Section INSERT.
Function big_ptAllocPDE_spec (nn vadr: Z) (adt: RData): option (RData × Z) :=
let pdi := PDX vadr in
let c := ZMap.get nn (AC adt) in
match (ikern adt, ihost adt, pg adt, ipt adt, cused c, pt_Arg´ nn vadr) with
| (true, true, true, true, true, true) ⇒
match ZMap.get pdi (ZMap.get nn (ptpool adt)) with
| PDEUnPresent ⇒
match big_palloc_spec nn adt with
| Some (adt´, pi) ⇒
if zeq pi 0 then
Some (adt´, pi)
else
Some (adt´ {HP: FlatMem.free_page pi (HP adt´)}
{pperm: ZMap.set pi (PGHide (PGPMap nn pdi)) (pperm adt´)}
{ptpool: (ZMap.set nn (ZMap.set pdi (PDEValid pi real_init_PTE)
(ZMap.get nn (ptpool adt´))) (ptpool adt´))}
, pi)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
primitve: set the n-th page table with virtual address vadr to (padr + perm) The pt insert at this layer, is slightly different from the one at MPTComm.
0th page map has been reserved for the kernel thread, which couldn't be modified after the initialization
Function big_ptInsert_spec (nn vadr padr perm: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt, ipt adt, pg adt, pt_Arg nn vadr padr (nps adt)) with
| (true, true, true, true, true) ⇒
match ZtoPerm perm with
| Some p ⇒
let pt := ZMap.get nn (ptpool adt) in
let pdi := PDX vadr in
let pti := PTX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
match ptInsertPTE0_spec nn vadr padr p adt with
| Some adt´ ⇒ Some (adt´, 0)
| _ ⇒ None
end
| PDEUnPresent ⇒
match big_ptAllocPDE_spec nn vadr adt with
| Some (adt´, v) ⇒
if zeq v 0 then Some (adt´, MagicNumber)
else
match ptInsertPTE0_spec nn vadr padr p adt´ with
| Some adt´´ ⇒ Some (adt´´, v)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End INSERT.
Function big_ptResv_spec (n vadr perm: Z) (adt: RData): option (RData × Z) :=
match big_palloc_spec n adt with
| Some (abd´, b) ⇒
if zeq b 0 then Some (abd´, MagicNumber)
else big_ptInsert_spec n vadr b perm abd´
| _ ⇒ None
end.
Function big_ptResv2_spec (n vadr perm n´ vadr´ perm´: Z) (adt: RData): option (RData × Z) :=
match big_palloc_spec n adt with
| Some (abd´, b) ⇒
if zeq b 0 then Some (abd´, MagicNumber)
else
match big_ptInsert_spec n vadr b perm abd´ with
| Some (abd´´, v) ⇒
if zeq v MagicNumber then Some (abd´´, MagicNumber)
else big_ptInsert_spec n´ vadr´ b perm´ abd´´
| _ ⇒ None
end
| _ ⇒ None
end.
Require Import ObjShareMem.
Function big_offer_shared_mem_spec (pid1 pid2 vadr: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt, pg adt, ipt adt, shared_mem_arg pid1 pid2) with
| (true, true, true, true, true) ⇒
match ZMap.get pid2 (ZMap.get pid1 (smspool adt)) with
| SHRDValid st _ _ ⇒
if SharedMemInfo_dec st SHRDPEND then Some (adt, SHARED_MEM_PEND)
else
match ZMap.get pid1 (ZMap.get pid2 (smspool adt)) with
| SHRDValid st´ _ vadr´ ⇒
if zle_lt 0 vadr´ adr_max then
if SharedMemInfo_dec st´ SHRDPEND then
match big_ptResv2_spec pid1 vadr PT_PERM_PTU pid2 vadr´ PT_PERM_PTU adt with
| Some (adt´, re) ⇒
if zeq re MagicNumber
then
let smsp := (ZMap.set pid1 (ZMap.set pid2 (SHRDValid SHRDDEAD true 0) (ZMap.get pid1 (smspool adt)))
(smspool adt´)) in
let smsp´ := (ZMap.set pid2 (ZMap.set pid1 (SHRDValid SHRDDEAD false 0) (ZMap.get pid2 smsp))
smsp) in
Some (adt´ {smspool: smsp´}, SHARED_MEM_DEAD)
else
let smsp := (ZMap.set pid1 (ZMap.set pid2 (SHRDValid SHRDREADY true 0) (ZMap.get pid1 (smspool adt´)))
(smspool adt´)) in
let smsp´ := (ZMap.set pid2 (ZMap.set pid1 (SHRDValid SHRDREADY false 0) (ZMap.get pid2 smsp))
smsp) in
Some (adt´ {smspool: smsp´}, SHARED_MEM_READY)
| _ ⇒ None
end
else
Some (adt {smspool: ZMap.set pid1 (ZMap.set pid2 (SHRDValid SHRDPEND true vadr)
(ZMap.get pid1 (smspool adt)))
(smspool adt)}, SHARED_MEM_PEND)
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End OBJ_Thread.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.
Require Import INVLemmaThread.
Local Open Scope Z_scope.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Local Open Scope Z_scope.
Section BIG_ACQUIRE_LOCk_SC.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_syncchpool}.
Context {re14: relate_impl_cid}.
Lemma big_acquire_lock_SC_exist:
∀ s f habd habd´ labd i,
big_acquire_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big_acquire_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_acquire_lock_SC_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- refine_split´.
rewrite H4 in ×. rewrite Hdestruct4. rewrite Hdestruct5.
reflexivity.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
rewrite H4. eapply relate_impl_big_log_update.
assumption.
- refine_split´.
rewrite H4 in ×. rewrite Hdestruct4. rewrite Hdestruct5.
reflexivity.
eapply relate_impl_lock_update.
rewrite H4. eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt3: match_impl_lock}.
Context {mt4: match_impl_big_log}.
Lemma big_acquire_lock_SC_match:
∀ s d d´ m f i,
big_acquire_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_acquire_lock_SC_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_syncchpool_update; eauto.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
- eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_acquire_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_acquire_lock_SC_spec}.
Lemma big_acquire_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_acquire_lock_SC_spec)
(id ↦ gensem big_acquire_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_acquire_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_acquire_lock_SC_match; eauto.
Qed.
End BIG_ACQUIRE_LOCk_SC.
Section BIG_RELEASE_LOCk_SC.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re13: relate_impl_syncchpool}.
Context {re14: relate_impl_cid}.
Lemma big_release_lock_SC_exist:
∀ s f habd habd´ labd i,
big_release_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big_release_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_release_lock_SC_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´.
reflexivity.
eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt3: match_impl_lock}.
Context {mt4: match_impl_big_log}.
Lemma big_release_lock_SC_match:
∀ s d d´ m f i,
big_release_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_release_lock_SC_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_release_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_release_lock_SC_spec}.
Lemma big_release_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_release_lock_SC_spec)
(id ↦ gensem big_release_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_release_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_release_lock_SC_match; eauto.
Qed.
End BIG_RELEASE_LOCk_SC.
Context`{oracle_ops: MultiOracleOps}.
Section BIGLOW_THREAD_SPAWN.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_kctxt}.
Context {re7: relate_impl_AC}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_multi_log}.
Context {re10: relate_impl_multi_oracle}.
Lemma biglow_thread_spawn_exist:
∀ s habd habd´ labd b b´ ofs´ id q n 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´, biglow_thread_spawn_spec labd b b´ ofs´ id q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_thread_spawn_spec. intros until f; intros HP HR Hsys Hsys´ Hincr.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_multi_log_eq; eauto.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto. intros.
revert HP. rewrite H4. subrewrite. subdestruct; inv HQ.
generalize (relate_impl_kctxt_eq _ _ _ _ HR); eauto. intros.
refine_split´; trivial.
apply relate_impl_kctxt_update.
apply relate_impl_AC_update.
apply relate_impl_multi_log_update.
eassumption.
- 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 H5; eauto. omega.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt3: match_impl_multi_log}.
Context {mt5: match_impl_AC}.
Lemma biglow_thread_spawn_match:
∀ s d d´ m b b´ ofs id q n f,
biglow_thread_spawn_spec d b b´ ofs id q = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_spawn_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_kctxt_update.
eapply match_impl_AC_update.
eapply match_impl_multi_log_update. eassumption.
Qed.
Context {inv: DNewInvariants (data_ops:= data_ops) biglow_thread_spawn_spec}.
Context {inv0: DNewInvariants (data_ops:= data_ops0) biglow_thread_spawn_spec}.
Lemma biglow_thread_spawn_sim :
∀ id,
sim (crel RData RData) (id ↦ dnew_compatsem biglow_thread_spawn_spec)
(id ↦ dnew_compatsem biglow_thread_spawn_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit biglow_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.
eapply biglow_thread_spawn_match; eauto.
Qed.
End BIGLOW_THREAD_SPAWN.
Section BIGLOW_THREAD_WAKEUP.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_multi_log}.
Context {re6: relate_impl_multi_oracle}.
Context {re7: relate_impl_lock}.
Context {re8: relate_impl_AC}.
Lemma biglow_thread_wakeup_exist:
∀ s f habd habd´ labd cv a,
biglow_thread_wakeup_spec cv habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, biglow_thread_wakeup_spec cv labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_thread_wakeup_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_multi_oracle_eq; eauto. intros.
revert H. rewrite H7. subrewrite. subdestruct; inv HQ; subst.
- refine_split´. reflexivity.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt1: match_impl_multi_log}.
Lemma biglow_thread_wakeup_match:
∀ s d d´ m f cv a,
biglow_thread_wakeup_spec cv d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_wakeup_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_multi_log_update.
eassumption.
- eapply match_impl_multi_log_update.
eassumption.
- eapply match_impl_multi_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) biglow_thread_wakeup_spec}.
Context {inv2: PreservesInvariants (HD:= data0) biglow_thread_wakeup_spec}.
Lemma biglow_thread_wakeup_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem biglow_thread_wakeup_spec)
(id ↦ gensem biglow_thread_wakeup_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit biglow_thread_wakeup_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply biglow_thread_wakeup_match; eauto.
Qed.
End BIGLOW_THREAD_WAKEUP.
Section BIG_THREAD_WAKEUP.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_big_log}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_lock}.
Context {re8: relate_impl_AC}.
Context {re9: relate_impl_cid}.
Lemma big_thread_wakeup_exist:
∀ s f habd habd´ labd cv a,
big_thread_wakeup_spec cv habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_thread_wakeup_spec cv labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_thread_wakeup_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. rewrite H7. subrewrite. subdestruct; inv HQ; subst.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_big_log}.
Lemma big_thread_wakeup_match:
∀ s d d´ m f cv a,
big_thread_wakeup_spec cv d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_thread_wakeup_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_thread_wakeup_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_thread_wakeup_spec}.
Lemma big_thread_wakeup_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_thread_wakeup_spec)
(id ↦ gensem big_thread_wakeup_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_thread_wakeup_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_thread_wakeup_match; eauto.
Qed.
End BIG_THREAD_WAKEUP.
Section BIGLOW_THREAD_SLEEP.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_kctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_AC}.
Context {re6: relate_impl_multi_oracle}.
Context {re7: relate_impl_multi_log}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_lock}.
Context {re10: relate_impl_syncchpool}.
Lemma biglow_thread_sleep_exists:
∀ s habd habd´ labd rs rs´ rs0 n 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´, rs´)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t, val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
→ ∃ labd´ rs0´ ofs,
biglow_thread_sleep_spec
labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
#EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) n = Some (labd´, rs0´)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r, ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = rs0´.
Proof.
unfold biglow_thread_sleep_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H. subrewrite. intros.
subdestruct; inv HQ.
generalize (relate_impl_kctxt_eq _ _ _ _ H0); eauto. intros.
refine_split´. reflexivity.
- eapply relate_impl_lock_update.
apply relate_impl_cid_update.
apply relate_impl_kctxt_update; trivial.
apply relate_impl_multi_log_update; trivial.
kctxt_inj_simpl.
- intros; eapply H; eauto.
- instantiate (1:= run_id); omega.
- reflexivity.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt2: match_impl_cid}.
Context {mt3: match_impl_multi_log}.
Context {mt5: match_impl_lock}.
Lemma biglow_thread_sleep_match:
∀ s d d´ m rs rs´ n f,
biglow_thread_sleep_spec d rs n = Some (d´, rs´)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_sleep_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_lock_update.
eapply match_impl_cid_update.
eapply match_impl_kctxt_update.
eapply match_impl_multi_log_update.
eassumption.
Qed.
Context {inv: ThreadTransferInvariants (data_ops:= data_ops) biglow_thread_sleep_spec}.
Context {inv0: ThreadTransferInvariants (data_ops:= data_ops0) biglow_thread_sleep_spec}.
Context {low1: low_level_invariant_impl}.
Lemma biglow_thread_sleep_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_thread_transfer_compatsem biglow_thread_sleep_spec)
(id ↦ primcall_thread_transfer_compatsem biglow_thread_sleep_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit biglow_thread_sleep_exists; 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.
- eapply biglow_thread_sleep_match; eauto.
Qed.
End BIGLOW_THREAD_SLEEP.
Section BIGLOW_THREAD_YIELD.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_kctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_AC}.
Context {re6: relate_impl_multi_oracle}.
Context {re7: relate_impl_multi_log}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_lock}.
Lemma biglow_thread_yield_exists:
∀ s habd habd´ labd rs rs´ rs0 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´, rs´)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t, val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
→ ∃ labd´ rs0´ ofs,
biglow_thread_yield_spec
labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
#EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) = Some (labd´, rs0´)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r, ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = rs0´.
Proof.
unfold biglow_thread_yield_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
revert H. subrewrite. intros.
subdestruct; inv HQ.
generalize (relate_impl_kctxt_eq _ _ _ _ H0); eauto. intros.
refine_split´. reflexivity.
- apply relate_impl_cid_update.
apply relate_impl_kctxt_update; trivial.
apply relate_impl_multi_log_update; trivial.
kctxt_inj_simpl.
- intros; eapply H; eauto.
- instantiate (1:= run_id); omega.
- reflexivity.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt2: match_impl_cid}.
Context {mt3: match_impl_multi_log}.
Lemma biglow_thread_yield_match:
∀ s d d´ m rs rs´ f,
biglow_thread_yield_spec d rs = Some (d´, rs´)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_yield_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_kctxt_update.
eapply match_impl_multi_log_update.
eassumption.
Qed.
Context {inv: ThreadScheduleInvariants (data_ops:= data_ops) biglow_thread_yield_spec}.
Context {inv0: ThreadScheduleInvariants (data_ops:= data_ops0) biglow_thread_yield_spec}.
Context {low1: low_level_invariant_impl}.
Lemma biglow_thread_yield_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_thread_schedule_compatsem biglow_thread_yield_spec (prim_ident:= id))
(id ↦ primcall_thread_schedule_compatsem biglow_thread_yield_spec (prim_ident:= id)).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit biglow_thread_yield_exists; 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.
- eapply biglow_thread_yield_match; eauto.
Qed.
End BIGLOW_THREAD_YIELD.
Section BIGLOW_SCHED_INIT.
Context {re1: relate_impl_init}.
Context {re2: relate_impl_iflags}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_LAT}.
Context {re5: relate_impl_ptpool}.
Context {re6: relate_impl_lock}.
Context {re7: relate_impl_idpde}.
Context {re8: relate_impl_smspool}.
Context {re9: relate_impl_syncchpool}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_vmxinfo}.
Context {re14: relate_impl_nps}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_PT}.
Context {re17: relate_impl_multi_log}.
Context {re116: relate_impl_ioapic}.
Context {re117: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
Lemma biglow_sched_init_exist:
∀ s f habd habd´ labd z,
biglow_sched_init_spec z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, biglow_sched_init_spec z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_sched_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_LAT_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_idpde_eq; eauto. intros.
exploit relate_impl_smspool_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto. intros.
exploit relate_impl_lapic_eq; eauto. intros.
exploit relate_impl_in_intr_eq; eauto; intros.
exploit relate_impl_multi_log_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´. reflexivity.
eapply relate_impl_cid_update.
eapply relate_impl_syncchpool_update.
apply relate_impl_smspool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_log_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_init}.
Context {mt2: match_impl_iflags}.
Context {mt3: match_impl_ipt}.
Context {mt4: match_impl_LAT}.
Context {mt5: match_impl_ptpool}.
Context {mt6: match_impl_lock}.
Context {mt7: match_impl_idpde}.
Context {mt8: match_impl_smspool}.
Context {mt9: match_impl_syncchpool}.
Context {mt10: match_impl_CPU_ID}.
Context {mt11: match_impl_cid}.
Context {mt12: match_impl_vmxinfo}.
Context {mt13: match_impl_nps}.
Context {mt14: match_impl_AC}.
Context {mt15: match_impl_PT}.
Context {mt16: match_impl_multi_log}.
Context {mt17: match_impl_ioapic}.
Context {mt18: match_impl_lapic}.
Lemma biglow_sched_init_match:
∀ s d d´ m z f,
biglow_sched_init_spec z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_sched_init_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_syncchpool_update.
eapply match_impl_smspool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) biglow_sched_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) biglow_sched_init_spec}.
Lemma biglow_sched_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem biglow_sched_init_spec)
(id ↦ gensem biglow_sched_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit biglow_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply biglow_sched_init_match; eauto.
Qed.
End BIGLOW_SCHED_INIT.
Section BIG_PALLOC.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_cid}.
Lemma big_palloc_exist:
∀ s f habd habd´ labd n a,
big_palloc_spec n habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_palloc_spec n labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_palloc_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_pperm_eq; eauto.
exploit relate_impl_big_oracle_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ.
- refine_split´. rewrite H3 in Hdestruct7. rewrite Hdestruct7.
rewrite Hdestruct8. reflexivity.
eapply relate_impl_AC_update.
eapply relate_impl_pperm_update.
eapply relate_impl_LAT_update.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
- refine_split´. rewrite H3 in Hdestruct7. rewrite Hdestruct7.
rewrite Hdestruct8. reflexivity.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_AC}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_LAT}.
Context {mt4: match_impl_big_log}.
Lemma big_palloc_match:
∀ s d d´ m f n a,
big_palloc_spec n d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_palloc_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_LAT_update.
eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_palloc_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_palloc_spec}.
Lemma big_palloc_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_palloc_spec)
(id ↦ gensem big_palloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_palloc_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_palloc_match; eauto.
Qed.
End BIG_PALLOC.
Section BIG_PTALLOCPDE.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_cid}.
Lemma big_ptAllocPDE_exist:
∀ s f habd habd´ labd n v p,
big_ptAllocPDE_spec n v habd = Some (habd´, p)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptAllocPDE_spec n v labd = Some (labd´, p)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptAllocPDE_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_HP_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_LAT_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- specialize (big_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. simpl. subst.
∃ ld1. split; eauto.
- specialize (big_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. rewrite Hdestruct8.
esplit. split. reflexivity.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
eapply relate_impl_ptpool_update.
eapply relate_impl_pperm_update.
eapply relate_impl_HP_update; eauto.
eapply FlatMem.free_page_inj´. unfold FlatMem.flatmem_inj. intros. eapply relate_impl_HP_eq; eauto.
Grab Existential Variables.
eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Lemma big_ptAllocPDE_match:
∀ s d d´ m f n v p,
big_ptAllocPDE_spec n v d = Some (d´, p)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptAllocPDE_spec; intros.
subdestruct; inv H; trivial.
- subst. eapply big_palloc_match; eauto.
- eapply match_impl_ptpool_update.
eapply match_impl_pperm_update.
eapply match_impl_HP_update.
eapply big_palloc_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_ptAllocPDE_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_ptAllocPDE_spec}.
Lemma big_ptAllocPDE_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_ptAllocPDE_spec)
(id ↦ gensem big_ptAllocPDE_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_ptAllocPDE_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_ptAllocPDE_match; eauto.
Qed.
End BIG_PTALLOCPDE.
Section BIG_PTRESV.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_cid}.
Lemma big_ptInsert_exist:
∀ s f habd habd´ labd n vadr perm z a,
big_ptInsert_spec n vadr perm z habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptInsert_spec n vadr perm z labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptInsert_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_nps_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
revert H. subrewrite. subdestruct; inv HQ.
- exploit ptInsertPTE0_exist; eauto.
intros (labd´ & → & Hr).
refine_split´; eauto.
- exploit big_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_true.
refine_split´; eauto.
- exploit big_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_false; auto.
exploit ptInsertPTE0_exist; eauto.
intros (labd´´ & → & Hr´).
refine_split´; eauto.
Qed.
Lemma big_ptResv_exist:
∀ s f habd habd´ labd n vadr perm a,
big_ptResv_spec n vadr perm habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptResv_spec n vadr perm labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptResv_spec. intros.
subdestruct_one. destruct p.
exploit big_palloc_exist; eauto.
intros (labd´ & → & Hr).
subdestruct; inv H.
- refine_split´; eauto.
- exploit big_ptInsert_exist; eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Lemma big_ptInsert_match:
∀ s d d´ m f n vadr perm z a,
big_ptInsert_spec n vadr perm z d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptInsert_spec; intros.
subdestruct; inv H; trivial.
- eapply ptInsertPTE0_match; eauto.
- eapply big_ptAllocPDE_match; eauto.
- eapply ptInsertPTE0_match; eauto.
eapply big_ptAllocPDE_match; eauto.
Qed.
Lemma big_ptResv_match:
∀ s d d´ m f n vadr perm a,
big_ptResv_spec n vadr perm d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptResv_spec; intros.
subdestruct; inv H; trivial.
- eapply big_palloc_match; eauto.
- eapply big_palloc_match in Hdestruct; eauto.
eapply big_ptInsert_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_ptResv_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_ptResv_spec}.
Lemma big_ptResv_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_ptResv_spec)
(id ↦ gensem big_ptResv_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_ptResv_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_ptResv_match; eauto.
Qed.
End BIG_PTRESV.
Section BIG_PTRESV2.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_cid}.
Lemma big_ptResv2_exist:
∀ s f habd habd´ labd n vadr perm n´ vadr´ perm´ a,
big_ptResv2_spec n vadr perm n´ vadr´ perm´ habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptResv2_spec n vadr perm n´ vadr´ perm´ labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptResv2_spec. intros.
subdestruct_one. destruct p.
exploit big_palloc_exist; eauto.
intros (labd´ & → & Hr).
subdestruct; inv H.
- refine_split´; eauto.
- exploit big_ptInsert_exist; eauto.
intros [ld0 [Hspecd0 Hreld0]]. rewrite Hspecd0. simpl.
∃ ld0. eauto.
- generalize (big_ptInsert_exist). intros Hbig.
generalize (Hbig s f r r0 labd´ n vadr z perm z0 Hdestruct1 Hr).
intros [ld0 [Hspecd0 Hreld0]]. rewrite Hspecd0. rewrite Hdestruct3.
generalize (Hbig s f r0 habd´ ld0 _ _ _ _ _ H2 Hreld0).
intros [ld1 [Hspecd1 Hreld1]]. rewrite Hspecd1.
∃ ld1. eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Lemma big_ptResv2_match:
∀ s d d´ m f n vadr perm n´ vadr´ perm´ a,
big_ptResv2_spec n vadr perm n´ vadr´ perm´ d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptResv2_spec; intros.
subdestruct; inv H; trivial.
- eapply big_palloc_match; eauto.
- eapply big_palloc_match in Hdestruct; eauto.
eapply big_ptInsert_match; eauto.
- eapply big_palloc_match in Hdestruct; eauto.
eapply big_ptInsert_match; eauto.
eapply big_ptInsert_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_ptResv2_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_ptResv2_spec}.
Lemma big_ptResv2_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_ptResv2_spec)
(id ↦ gensem big_ptResv2_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_ptResv2_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_ptResv2_match; eauto.
Qed.
End BIG_PTRESV2.
Section BIG_OFFER_SHARED_MEM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_smspool}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_AC}.
Context {re14: relate_impl_cid}.
Lemma big_offer_shared_mem_exist:
∀ s f habd habd´ labd pid1 pid2 vadr a,
big_offer_shared_mem_spec pid1 pid2 vadr habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_offer_shared_mem_spec pid1 pid2 vadr labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_offer_shared_mem_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_smspool_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- eauto.
- exploit big_ptResv2_exist; eauto. intros [ld0 [Hlspec0 Hrel0]].
rewrite Hlspec0. simpl. refine_split´. reflexivity.
exploit relate_impl_smspool_eq; eauto. intros smspool_re. rewrite smspool_re.
eapply relate_impl_smspool_update.
assumption.
- exploit big_ptResv2_exist; eauto. intros [ld0 [Hlspec0 Hrel0]].
rewrite Hlspec0. rewrite Hdestruct11. refine_split´. reflexivity.
exploit relate_impl_smspool_eq; eauto. intros smspool_re. rewrite smspool_re.
eapply relate_impl_smspool_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_smspool_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Context {mt7: match_impl_smspool}.
Lemma big_offer_shared_mem_match:
∀ s d d´ m f pid1 pid2 vadr a,
big_offer_shared_mem_spec pid1 pid2 vadr d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_offer_shared_mem_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_smspool_update.
eapply big_ptResv2_match in Hdestruct9; eauto.
- eapply match_impl_smspool_update.
eapply big_ptResv2_match in Hdestruct9; eauto.
- eapply match_impl_smspool_update. eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_offer_shared_mem_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_offer_shared_mem_spec}.
Lemma big_offer_shared_mem_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_offer_shared_mem_spec)
(id ↦ gensem big_offer_shared_mem_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_offer_shared_mem_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_offer_shared_mem_match; eauto.
Qed.
End BIG_OFFER_SHARED_MEM.
Section BIG_SCHED_INIT.
Context {re1: relate_impl_init}.
Context {re2: relate_impl_iflags}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_LAT}.
Context {re5: relate_impl_ptpool}.
Context {re6: relate_impl_lock}.
Context {re7: relate_impl_idpde}.
Context {re8: relate_impl_smspool}.
Context {re9: relate_impl_syncchpool}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_vmxinfo}.
Context {re14: relate_impl_nps}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_PT}.
Context {re17: relate_impl_big_log}.
Context {re116: relate_impl_ioapic}.
Context {re117: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
Lemma big_sched_init_exist:
∀ s f habd habd´ labd z,
big_sched_init_spec z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big_sched_init_spec z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_sched_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_LAT_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_idpde_eq; eauto. intros.
exploit relate_impl_smspool_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto. intros.
exploit relate_impl_lapic_eq; eauto. intros.
exploit relate_impl_in_intr_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´. reflexivity.
eapply relate_impl_cid_update.
eapply relate_impl_syncchpool_update.
apply relate_impl_smspool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_big_log_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_init}.
Context {mt2: match_impl_iflags}.
Context {mt3: match_impl_ipt}.
Context {mt4: match_impl_LAT}.
Context {mt5: match_impl_ptpool}.
Context {mt6: match_impl_lock}.
Context {mt7: match_impl_idpde}.
Context {mt8: match_impl_smspool}.
Context {mt9: match_impl_syncchpool}.
Context {mt11: match_impl_CPU_ID}.
Context {mt12: match_impl_cid}.
Context {mt13: match_impl_vmxinfo}.
Context {mt14: match_impl_nps}.
Context {mt15: match_impl_AC}.
Context {mt16: match_impl_PT}.
Context {mt17: match_impl_big_log}.
Context {mt116: match_impl_ioapic}.
Context {mt117: match_impl_lapic}.
Lemma big_sched_init_match:
∀ s d d´ m z f,
big_sched_init_spec z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_sched_init_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_syncchpool_update.
eapply match_impl_smspool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_big_log_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_sched_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_sched_init_spec}.
Lemma big_sched_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_sched_init_spec)
(id ↦ gensem big_sched_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_sched_init_match; eauto.
Qed.
End BIG_SCHED_INIT.
End OBJ_SIM.
match (ikern adt, ihost adt, ipt adt, pg adt, pt_Arg nn vadr padr (nps adt)) with
| (true, true, true, true, true) ⇒
match ZtoPerm perm with
| Some p ⇒
let pt := ZMap.get nn (ptpool adt) in
let pdi := PDX vadr in
let pti := PTX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
match ptInsertPTE0_spec nn vadr padr p adt with
| Some adt´ ⇒ Some (adt´, 0)
| _ ⇒ None
end
| PDEUnPresent ⇒
match big_ptAllocPDE_spec nn vadr adt with
| Some (adt´, v) ⇒
if zeq v 0 then Some (adt´, MagicNumber)
else
match ptInsertPTE0_spec nn vadr padr p adt´ with
| Some adt´´ ⇒ Some (adt´´, v)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End INSERT.
Function big_ptResv_spec (n vadr perm: Z) (adt: RData): option (RData × Z) :=
match big_palloc_spec n adt with
| Some (abd´, b) ⇒
if zeq b 0 then Some (abd´, MagicNumber)
else big_ptInsert_spec n vadr b perm abd´
| _ ⇒ None
end.
Function big_ptResv2_spec (n vadr perm n´ vadr´ perm´: Z) (adt: RData): option (RData × Z) :=
match big_palloc_spec n adt with
| Some (abd´, b) ⇒
if zeq b 0 then Some (abd´, MagicNumber)
else
match big_ptInsert_spec n vadr b perm abd´ with
| Some (abd´´, v) ⇒
if zeq v MagicNumber then Some (abd´´, MagicNumber)
else big_ptInsert_spec n´ vadr´ b perm´ abd´´
| _ ⇒ None
end
| _ ⇒ None
end.
Require Import ObjShareMem.
Function big_offer_shared_mem_spec (pid1 pid2 vadr: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt, pg adt, ipt adt, shared_mem_arg pid1 pid2) with
| (true, true, true, true, true) ⇒
match ZMap.get pid2 (ZMap.get pid1 (smspool adt)) with
| SHRDValid st _ _ ⇒
if SharedMemInfo_dec st SHRDPEND then Some (adt, SHARED_MEM_PEND)
else
match ZMap.get pid1 (ZMap.get pid2 (smspool adt)) with
| SHRDValid st´ _ vadr´ ⇒
if zle_lt 0 vadr´ adr_max then
if SharedMemInfo_dec st´ SHRDPEND then
match big_ptResv2_spec pid1 vadr PT_PERM_PTU pid2 vadr´ PT_PERM_PTU adt with
| Some (adt´, re) ⇒
if zeq re MagicNumber
then
let smsp := (ZMap.set pid1 (ZMap.set pid2 (SHRDValid SHRDDEAD true 0) (ZMap.get pid1 (smspool adt)))
(smspool adt´)) in
let smsp´ := (ZMap.set pid2 (ZMap.set pid1 (SHRDValid SHRDDEAD false 0) (ZMap.get pid2 smsp))
smsp) in
Some (adt´ {smspool: smsp´}, SHARED_MEM_DEAD)
else
let smsp := (ZMap.set pid1 (ZMap.set pid2 (SHRDValid SHRDREADY true 0) (ZMap.get pid1 (smspool adt´)))
(smspool adt´)) in
let smsp´ := (ZMap.set pid2 (ZMap.set pid1 (SHRDValid SHRDREADY false 0) (ZMap.get pid2 smsp))
smsp) in
Some (adt´ {smspool: smsp´}, SHARED_MEM_READY)
| _ ⇒ None
end
else
Some (adt {smspool: ZMap.set pid1 (ZMap.set pid2 (SHRDValid SHRDPEND true vadr)
(ZMap.get pid1 (smspool adt)))
(smspool adt)}, SHARED_MEM_PEND)
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End OBJ_Thread.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.
Require Import INVLemmaThread.
Local Open Scope Z_scope.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Local Open Scope Z_scope.
Section BIG_ACQUIRE_LOCk_SC.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_syncchpool}.
Context {re14: relate_impl_cid}.
Lemma big_acquire_lock_SC_exist:
∀ s f habd habd´ labd i,
big_acquire_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big_acquire_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_acquire_lock_SC_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- refine_split´.
rewrite H4 in ×. rewrite Hdestruct4. rewrite Hdestruct5.
reflexivity.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
rewrite H4. eapply relate_impl_big_log_update.
assumption.
- refine_split´.
rewrite H4 in ×. rewrite Hdestruct4. rewrite Hdestruct5.
reflexivity.
eapply relate_impl_lock_update.
rewrite H4. eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_syncchpool}.
Context {mt3: match_impl_lock}.
Context {mt4: match_impl_big_log}.
Lemma big_acquire_lock_SC_match:
∀ s d d´ m f i,
big_acquire_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_acquire_lock_SC_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_syncchpool_update; eauto.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
- eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_acquire_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_acquire_lock_SC_spec}.
Lemma big_acquire_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_acquire_lock_SC_spec)
(id ↦ gensem big_acquire_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_acquire_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_acquire_lock_SC_match; eauto.
Qed.
End BIG_ACQUIRE_LOCk_SC.
Section BIG_RELEASE_LOCk_SC.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re13: relate_impl_syncchpool}.
Context {re14: relate_impl_cid}.
Lemma big_release_lock_SC_exist:
∀ s f habd habd´ labd i,
big_release_lock_SC_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big_release_lock_SC_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_release_lock_SC_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´.
reflexivity.
eapply relate_impl_lock_update.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt3: match_impl_lock}.
Context {mt4: match_impl_big_log}.
Lemma big_release_lock_SC_match:
∀ s d d´ m f i,
big_release_lock_SC_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_release_lock_SC_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_lock_update; eauto.
eapply match_impl_big_log_update; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_release_lock_SC_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_release_lock_SC_spec}.
Lemma big_release_lock_SC_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_release_lock_SC_spec)
(id ↦ gensem big_release_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_release_lock_SC_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_release_lock_SC_match; eauto.
Qed.
End BIG_RELEASE_LOCk_SC.
Context`{oracle_ops: MultiOracleOps}.
Section BIGLOW_THREAD_SPAWN.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re4: relate_impl_kctxt}.
Context {re7: relate_impl_AC}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_multi_log}.
Context {re10: relate_impl_multi_oracle}.
Lemma biglow_thread_spawn_exist:
∀ s habd habd´ labd b b´ ofs´ id q n 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´, biglow_thread_spawn_spec labd b b´ ofs´ id q = Some (labd´, n)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_thread_spawn_spec. intros until f; intros HP HR Hsys Hsys´ Hincr.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_multi_log_eq; eauto.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto. intros.
revert HP. rewrite H4. subrewrite. subdestruct; inv HQ.
generalize (relate_impl_kctxt_eq _ _ _ _ HR); eauto. intros.
refine_split´; trivial.
apply relate_impl_kctxt_update.
apply relate_impl_AC_update.
apply relate_impl_multi_log_update.
eassumption.
- 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 H5; eauto. omega.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt3: match_impl_multi_log}.
Context {mt5: match_impl_AC}.
Lemma biglow_thread_spawn_match:
∀ s d d´ m b b´ ofs id q n f,
biglow_thread_spawn_spec d b b´ ofs id q = Some (d´, n)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_spawn_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_kctxt_update.
eapply match_impl_AC_update.
eapply match_impl_multi_log_update. eassumption.
Qed.
Context {inv: DNewInvariants (data_ops:= data_ops) biglow_thread_spawn_spec}.
Context {inv0: DNewInvariants (data_ops:= data_ops0) biglow_thread_spawn_spec}.
Lemma biglow_thread_spawn_sim :
∀ id,
sim (crel RData RData) (id ↦ dnew_compatsem biglow_thread_spawn_spec)
(id ↦ dnew_compatsem biglow_thread_spawn_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
exploit biglow_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.
eapply biglow_thread_spawn_match; eauto.
Qed.
End BIGLOW_THREAD_SPAWN.
Section BIGLOW_THREAD_WAKEUP.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_multi_log}.
Context {re6: relate_impl_multi_oracle}.
Context {re7: relate_impl_lock}.
Context {re8: relate_impl_AC}.
Lemma biglow_thread_wakeup_exist:
∀ s f habd habd´ labd cv a,
biglow_thread_wakeup_spec cv habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, biglow_thread_wakeup_spec cv labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_thread_wakeup_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_multi_oracle_eq; eauto. intros.
revert H. rewrite H7. subrewrite. subdestruct; inv HQ; subst.
- refine_split´. reflexivity.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt1: match_impl_multi_log}.
Lemma biglow_thread_wakeup_match:
∀ s d d´ m f cv a,
biglow_thread_wakeup_spec cv d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_wakeup_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_multi_log_update.
eassumption.
- eapply match_impl_multi_log_update.
eassumption.
- eapply match_impl_multi_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) biglow_thread_wakeup_spec}.
Context {inv2: PreservesInvariants (HD:= data0) biglow_thread_wakeup_spec}.
Lemma biglow_thread_wakeup_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem biglow_thread_wakeup_spec)
(id ↦ gensem biglow_thread_wakeup_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit biglow_thread_wakeup_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply biglow_thread_wakeup_match; eauto.
Qed.
End BIGLOW_THREAD_WAKEUP.
Section BIG_THREAD_WAKEUP.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_big_log}.
Context {re6: relate_impl_big_oracle}.
Context {re7: relate_impl_lock}.
Context {re8: relate_impl_AC}.
Context {re9: relate_impl_cid}.
Lemma big_thread_wakeup_exist:
∀ s f habd habd´ labd cv a,
big_thread_wakeup_spec cv habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_thread_wakeup_spec cv labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_thread_wakeup_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
revert H. rewrite H7. subrewrite. subdestruct; inv HQ; subst.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_big_log}.
Lemma big_thread_wakeup_match:
∀ s d d´ m f cv a,
big_thread_wakeup_spec cv d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_thread_wakeup_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
- eapply match_impl_big_log_update.
eassumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_thread_wakeup_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_thread_wakeup_spec}.
Lemma big_thread_wakeup_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_thread_wakeup_spec)
(id ↦ gensem big_thread_wakeup_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_thread_wakeup_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_thread_wakeup_match; eauto.
Qed.
End BIG_THREAD_WAKEUP.
Section BIGLOW_THREAD_SLEEP.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_kctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_AC}.
Context {re6: relate_impl_multi_oracle}.
Context {re7: relate_impl_multi_log}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_lock}.
Context {re10: relate_impl_syncchpool}.
Lemma biglow_thread_sleep_exists:
∀ s habd habd´ labd rs rs´ rs0 n 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´, rs´)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t, val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
→ ∃ labd´ rs0´ ofs,
biglow_thread_sleep_spec
labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
#EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) n = Some (labd´, rs0´)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r, ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = rs0´.
Proof.
unfold biglow_thread_sleep_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_syncchpool_eq; eauto; intros.
revert H. subrewrite. intros.
subdestruct; inv HQ.
generalize (relate_impl_kctxt_eq _ _ _ _ H0); eauto. intros.
refine_split´. reflexivity.
- eapply relate_impl_lock_update.
apply relate_impl_cid_update.
apply relate_impl_kctxt_update; trivial.
apply relate_impl_multi_log_update; trivial.
kctxt_inj_simpl.
- intros; eapply H; eauto.
- instantiate (1:= run_id); omega.
- reflexivity.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt2: match_impl_cid}.
Context {mt3: match_impl_multi_log}.
Context {mt5: match_impl_lock}.
Lemma biglow_thread_sleep_match:
∀ s d d´ m rs rs´ n f,
biglow_thread_sleep_spec d rs n = Some (d´, rs´)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_sleep_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_lock_update.
eapply match_impl_cid_update.
eapply match_impl_kctxt_update.
eapply match_impl_multi_log_update.
eassumption.
Qed.
Context {inv: ThreadTransferInvariants (data_ops:= data_ops) biglow_thread_sleep_spec}.
Context {inv0: ThreadTransferInvariants (data_ops:= data_ops0) biglow_thread_sleep_spec}.
Context {low1: low_level_invariant_impl}.
Lemma biglow_thread_sleep_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_thread_transfer_compatsem biglow_thread_sleep_spec)
(id ↦ primcall_thread_transfer_compatsem biglow_thread_sleep_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit biglow_thread_sleep_exists; 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.
- eapply biglow_thread_sleep_match; eauto.
Qed.
End BIGLOW_THREAD_SLEEP.
Section BIGLOW_THREAD_YIELD.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_kctxt}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_AC}.
Context {re6: relate_impl_multi_oracle}.
Context {re7: relate_impl_multi_log}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_lock}.
Lemma biglow_thread_yield_exists:
∀ s habd habd´ labd rs rs´ rs0 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´, rs´)
→ relate_AbData s f habd labd
→ (∀ reg : PregEq.t, val_inject f (Pregmap.get reg rs) (Pregmap.get reg rs0))
→ ∃ labd´ rs0´ ofs,
biglow_thread_yield_spec
labd ((Pregmap.init Vundef)#ESP <- (rs0#ESP)#EDI <- (rs0#EDI)#ESI <- (rs0#ESI)
#EBX <- (rs0#EBX)#EBP <- (rs0#EBP)#RA <- (rs0#RA)) = Some (labd´, rs0´)
∧ relate_AbData s f habd´ labd´
∧ (∀ i r, ZtoPreg i = Some r → val_inject f (rs´#r) (rs0´#r))
∧ 0 ≤ ofs < num_proc
∧ ZMap.get ofs (kctxt labd) = rs0´.
Proof.
unfold biglow_thread_yield_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
revert H. subrewrite. intros.
subdestruct; inv HQ.
generalize (relate_impl_kctxt_eq _ _ _ _ H0); eauto. intros.
refine_split´. reflexivity.
- apply relate_impl_cid_update.
apply relate_impl_kctxt_update; trivial.
apply relate_impl_multi_log_update; trivial.
kctxt_inj_simpl.
- intros; eapply H; eauto.
- instantiate (1:= run_id); omega.
- reflexivity.
Qed.
Context {mt1: match_impl_kctxt}.
Context {mt2: match_impl_cid}.
Context {mt3: match_impl_multi_log}.
Lemma biglow_thread_yield_match:
∀ s d d´ m rs rs´ f,
biglow_thread_yield_spec d rs = Some (d´, rs´)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_thread_yield_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_kctxt_update.
eapply match_impl_multi_log_update.
eassumption.
Qed.
Context {inv: ThreadScheduleInvariants (data_ops:= data_ops) biglow_thread_yield_spec}.
Context {inv0: ThreadScheduleInvariants (data_ops:= data_ops0) biglow_thread_yield_spec}.
Context {low1: low_level_invariant_impl}.
Lemma biglow_thread_yield_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_thread_schedule_compatsem biglow_thread_yield_spec (prim_ident:= id))
(id ↦ primcall_thread_schedule_compatsem biglow_thread_yield_spec (prim_ident:= id)).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. simpl; intros.
inv H. inv H0. inv match_extcall_states.
exploit biglow_thread_yield_exists; 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.
- eapply biglow_thread_yield_match; eauto.
Qed.
End BIGLOW_THREAD_YIELD.
Section BIGLOW_SCHED_INIT.
Context {re1: relate_impl_init}.
Context {re2: relate_impl_iflags}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_LAT}.
Context {re5: relate_impl_ptpool}.
Context {re6: relate_impl_lock}.
Context {re7: relate_impl_idpde}.
Context {re8: relate_impl_smspool}.
Context {re9: relate_impl_syncchpool}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_vmxinfo}.
Context {re14: relate_impl_nps}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_PT}.
Context {re17: relate_impl_multi_log}.
Context {re116: relate_impl_ioapic}.
Context {re117: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
Lemma biglow_sched_init_exist:
∀ s f habd habd´ labd z,
biglow_sched_init_spec z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, biglow_sched_init_spec z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold biglow_sched_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_LAT_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_idpde_eq; eauto. intros.
exploit relate_impl_smspool_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto. intros.
exploit relate_impl_lapic_eq; eauto. intros.
exploit relate_impl_in_intr_eq; eauto; intros.
exploit relate_impl_multi_log_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´. reflexivity.
eapply relate_impl_cid_update.
eapply relate_impl_syncchpool_update.
apply relate_impl_smspool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_log_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_init}.
Context {mt2: match_impl_iflags}.
Context {mt3: match_impl_ipt}.
Context {mt4: match_impl_LAT}.
Context {mt5: match_impl_ptpool}.
Context {mt6: match_impl_lock}.
Context {mt7: match_impl_idpde}.
Context {mt8: match_impl_smspool}.
Context {mt9: match_impl_syncchpool}.
Context {mt10: match_impl_CPU_ID}.
Context {mt11: match_impl_cid}.
Context {mt12: match_impl_vmxinfo}.
Context {mt13: match_impl_nps}.
Context {mt14: match_impl_AC}.
Context {mt15: match_impl_PT}.
Context {mt16: match_impl_multi_log}.
Context {mt17: match_impl_ioapic}.
Context {mt18: match_impl_lapic}.
Lemma biglow_sched_init_match:
∀ s d d´ m z f,
biglow_sched_init_spec z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold biglow_sched_init_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_syncchpool_update.
eapply match_impl_smspool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) biglow_sched_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) biglow_sched_init_spec}.
Lemma biglow_sched_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem biglow_sched_init_spec)
(id ↦ gensem biglow_sched_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit biglow_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply biglow_sched_init_match; eauto.
Qed.
End BIGLOW_SCHED_INIT.
Section BIG_PALLOC.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_cid}.
Lemma big_palloc_exist:
∀ s f habd habd´ labd n a,
big_palloc_spec n habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_palloc_spec n labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_palloc_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_pperm_eq; eauto.
exploit relate_impl_big_oracle_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ.
- refine_split´. rewrite H3 in Hdestruct7. rewrite Hdestruct7.
rewrite Hdestruct8. reflexivity.
eapply relate_impl_AC_update.
eapply relate_impl_pperm_update.
eapply relate_impl_LAT_update.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
- refine_split´. rewrite H3 in Hdestruct7. rewrite Hdestruct7.
rewrite Hdestruct8. reflexivity.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_AC}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_LAT}.
Context {mt4: match_impl_big_log}.
Lemma big_palloc_match:
∀ s d d´ m f n a,
big_palloc_spec n d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_palloc_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_LAT_update.
eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_palloc_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_palloc_spec}.
Lemma big_palloc_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_palloc_spec)
(id ↦ gensem big_palloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_palloc_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_palloc_match; eauto.
Qed.
End BIG_PALLOC.
Section BIG_PTALLOCPDE.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_cid}.
Lemma big_ptAllocPDE_exist:
∀ s f habd habd´ labd n v p,
big_ptAllocPDE_spec n v habd = Some (habd´, p)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptAllocPDE_spec n v labd = Some (labd´, p)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptAllocPDE_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_HP_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_LAT_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- specialize (big_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. simpl. subst.
∃ ld1. split; eauto.
- specialize (big_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. rewrite Hdestruct8.
esplit. split. reflexivity.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
eapply relate_impl_ptpool_update.
eapply relate_impl_pperm_update.
eapply relate_impl_HP_update; eauto.
eapply FlatMem.free_page_inj´. unfold FlatMem.flatmem_inj. intros. eapply relate_impl_HP_eq; eauto.
Grab Existential Variables.
eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Lemma big_ptAllocPDE_match:
∀ s d d´ m f n v p,
big_ptAllocPDE_spec n v d = Some (d´, p)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptAllocPDE_spec; intros.
subdestruct; inv H; trivial.
- subst. eapply big_palloc_match; eauto.
- eapply match_impl_ptpool_update.
eapply match_impl_pperm_update.
eapply match_impl_HP_update.
eapply big_palloc_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_ptAllocPDE_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_ptAllocPDE_spec}.
Lemma big_ptAllocPDE_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_ptAllocPDE_spec)
(id ↦ gensem big_ptAllocPDE_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_ptAllocPDE_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_ptAllocPDE_match; eauto.
Qed.
End BIG_PTALLOCPDE.
Section BIG_PTRESV.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_cid}.
Lemma big_ptInsert_exist:
∀ s f habd habd´ labd n vadr perm z a,
big_ptInsert_spec n vadr perm z habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptInsert_spec n vadr perm z labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptInsert_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_nps_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
revert H. subrewrite. subdestruct; inv HQ.
- exploit ptInsertPTE0_exist; eauto.
intros (labd´ & → & Hr).
refine_split´; eauto.
- exploit big_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_true.
refine_split´; eauto.
- exploit big_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_false; auto.
exploit ptInsertPTE0_exist; eauto.
intros (labd´´ & → & Hr´).
refine_split´; eauto.
Qed.
Lemma big_ptResv_exist:
∀ s f habd habd´ labd n vadr perm a,
big_ptResv_spec n vadr perm habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptResv_spec n vadr perm labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptResv_spec. intros.
subdestruct_one. destruct p.
exploit big_palloc_exist; eauto.
intros (labd´ & → & Hr).
subdestruct; inv H.
- refine_split´; eauto.
- exploit big_ptInsert_exist; eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Lemma big_ptInsert_match:
∀ s d d´ m f n vadr perm z a,
big_ptInsert_spec n vadr perm z d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptInsert_spec; intros.
subdestruct; inv H; trivial.
- eapply ptInsertPTE0_match; eauto.
- eapply big_ptAllocPDE_match; eauto.
- eapply ptInsertPTE0_match; eauto.
eapply big_ptAllocPDE_match; eauto.
Qed.
Lemma big_ptResv_match:
∀ s d d´ m f n vadr perm a,
big_ptResv_spec n vadr perm d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptResv_spec; intros.
subdestruct; inv H; trivial.
- eapply big_palloc_match; eauto.
- eapply big_palloc_match in Hdestruct; eauto.
eapply big_ptInsert_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_ptResv_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_ptResv_spec}.
Lemma big_ptResv_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_ptResv_spec)
(id ↦ gensem big_ptResv_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_ptResv_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_ptResv_match; eauto.
Qed.
End BIG_PTRESV.
Section BIG_PTRESV2.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_cid}.
Lemma big_ptResv2_exist:
∀ s f habd habd´ labd n vadr perm n´ vadr´ perm´ a,
big_ptResv2_spec n vadr perm n´ vadr´ perm´ habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_ptResv2_spec n vadr perm n´ vadr´ perm´ labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_ptResv2_spec. intros.
subdestruct_one. destruct p.
exploit big_palloc_exist; eauto.
intros (labd´ & → & Hr).
subdestruct; inv H.
- refine_split´; eauto.
- exploit big_ptInsert_exist; eauto.
intros [ld0 [Hspecd0 Hreld0]]. rewrite Hspecd0. simpl.
∃ ld0. eauto.
- generalize (big_ptInsert_exist). intros Hbig.
generalize (Hbig s f r r0 labd´ n vadr z perm z0 Hdestruct1 Hr).
intros [ld0 [Hspecd0 Hreld0]]. rewrite Hspecd0. rewrite Hdestruct3.
generalize (Hbig s f r0 habd´ ld0 _ _ _ _ _ H2 Hreld0).
intros [ld1 [Hspecd1 Hreld1]]. rewrite Hspecd1.
∃ ld1. eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Lemma big_ptResv2_match:
∀ s d d´ m f n vadr perm n´ vadr´ perm´ a,
big_ptResv2_spec n vadr perm n´ vadr´ perm´ d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_ptResv2_spec; intros.
subdestruct; inv H; trivial.
- eapply big_palloc_match; eauto.
- eapply big_palloc_match in Hdestruct; eauto.
eapply big_ptInsert_match; eauto.
- eapply big_palloc_match in Hdestruct; eauto.
eapply big_ptInsert_match; eauto.
eapply big_ptInsert_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_ptResv2_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_ptResv2_spec}.
Lemma big_ptResv2_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_ptResv2_spec)
(id ↦ gensem big_ptResv2_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_ptResv2_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_ptResv2_match; eauto.
Qed.
End BIG_PTRESV2.
Section BIG_OFFER_SHARED_MEM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_smspool}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_LAT}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_AC}.
Context {re14: relate_impl_cid}.
Lemma big_offer_shared_mem_exist:
∀ s f habd habd´ labd pid1 pid2 vadr a,
big_offer_shared_mem_spec pid1 pid2 vadr habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big_offer_shared_mem_spec pid1 pid2 vadr labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_offer_shared_mem_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_smspool_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- eauto.
- exploit big_ptResv2_exist; eauto. intros [ld0 [Hlspec0 Hrel0]].
rewrite Hlspec0. simpl. refine_split´. reflexivity.
exploit relate_impl_smspool_eq; eauto. intros smspool_re. rewrite smspool_re.
eapply relate_impl_smspool_update.
assumption.
- exploit big_ptResv2_exist; eauto. intros [ld0 [Hlspec0 Hrel0]].
rewrite Hlspec0. rewrite Hdestruct11. refine_split´. reflexivity.
exploit relate_impl_smspool_eq; eauto. intros smspool_re. rewrite smspool_re.
eapply relate_impl_smspool_update.
assumption.
- refine_split´. reflexivity.
eapply relate_impl_smspool_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Context {mt6: match_impl_LAT}.
Context {mt7: match_impl_smspool}.
Lemma big_offer_shared_mem_match:
∀ s d d´ m f pid1 pid2 vadr a,
big_offer_shared_mem_spec pid1 pid2 vadr d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_offer_shared_mem_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_smspool_update.
eapply big_ptResv2_match in Hdestruct9; eauto.
- eapply match_impl_smspool_update.
eapply big_ptResv2_match in Hdestruct9; eauto.
- eapply match_impl_smspool_update. eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_offer_shared_mem_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_offer_shared_mem_spec}.
Lemma big_offer_shared_mem_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_offer_shared_mem_spec)
(id ↦ gensem big_offer_shared_mem_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_offer_shared_mem_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_offer_shared_mem_match; eauto.
Qed.
End BIG_OFFER_SHARED_MEM.
Section BIG_SCHED_INIT.
Context {re1: relate_impl_init}.
Context {re2: relate_impl_iflags}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_LAT}.
Context {re5: relate_impl_ptpool}.
Context {re6: relate_impl_lock}.
Context {re7: relate_impl_idpde}.
Context {re8: relate_impl_smspool}.
Context {re9: relate_impl_syncchpool}.
Context {re11: relate_impl_CPU_ID}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_vmxinfo}.
Context {re14: relate_impl_nps}.
Context {re15: relate_impl_AC}.
Context {re16: relate_impl_PT}.
Context {re17: relate_impl_big_log}.
Context {re116: relate_impl_ioapic}.
Context {re117: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
Lemma big_sched_init_exist:
∀ s f habd habd´ labd z,
big_sched_init_spec z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big_sched_init_spec z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big_sched_init_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_LAT_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_idpde_eq; eauto. intros.
exploit relate_impl_smspool_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto. intros.
exploit relate_impl_lapic_eq; eauto. intros.
exploit relate_impl_in_intr_eq; eauto; intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
refine_split´. reflexivity.
eapply relate_impl_cid_update.
eapply relate_impl_syncchpool_update.
apply relate_impl_smspool_update.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_big_log_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_init}.
Context {mt2: match_impl_iflags}.
Context {mt3: match_impl_ipt}.
Context {mt4: match_impl_LAT}.
Context {mt5: match_impl_ptpool}.
Context {mt6: match_impl_lock}.
Context {mt7: match_impl_idpde}.
Context {mt8: match_impl_smspool}.
Context {mt9: match_impl_syncchpool}.
Context {mt11: match_impl_CPU_ID}.
Context {mt12: match_impl_cid}.
Context {mt13: match_impl_vmxinfo}.
Context {mt14: match_impl_nps}.
Context {mt15: match_impl_AC}.
Context {mt16: match_impl_PT}.
Context {mt17: match_impl_big_log}.
Context {mt116: match_impl_ioapic}.
Context {mt117: match_impl_lapic}.
Lemma big_sched_init_match:
∀ s d d´ m z f,
big_sched_init_spec z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big_sched_init_spec; intros.
subdestruct; inv H; trivial.
eapply match_impl_cid_update.
eapply match_impl_syncchpool_update.
eapply match_impl_smspool_update.
eapply match_impl_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_big_log_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big_sched_init_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big_sched_init_spec}.
Lemma big_sched_init_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big_sched_init_spec)
(id ↦ gensem big_sched_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big_sched_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big_sched_init_match; eauto.
Qed.
End BIG_SCHED_INIT.
End OBJ_SIM.