Library mcertikos.objects.ObjPMM
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import ObjInterruptDriver.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import ObjContainer.
Require Import GlobIdent.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import ObjQLock.
Require Import CalTicketLock.
Section OBJ_PMM.
Context `{real_params: RealParams}.
Local Open Scope Z_scope.
primitve: returns whether i-th page has type "normal"
Function is_at_norm_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, ihost adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, LockOwn true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (AT adt) with
| ATValid _ st ⇒
if ATType_dec st ATNorm then Some 1
else Some 0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, LockOwn true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (AT adt) with
| ATValid _ st ⇒
if ATType_dec st ATNorm then Some 1
else Some 0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
primitve: returns whether i-th page is allocated or not
Function get_at_u_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, ihost adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, LockOwn true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (AT adt) with
| ATValid true _ ⇒ Some 1
| ATValid _ _ ⇒ Some 0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, LockOwn true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (AT adt) with
| ATValid true _ ⇒ Some 1
| ATValid _ _ ⇒ Some 0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
primitve: returns whether i-th page is allocated or not
Function get_at_c_spec (i: Z) (adt: RData) : option Z :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (ATC adt) with
| ATCValid n ⇒ Some n
| _ ⇒ None
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (ATC adt) with
| ATCValid n ⇒ Some n
| _ ⇒ None
end
else None
| _ ⇒ None
end.
primitve: get the number of pages
Function get_nps_spec (adt: RData) : option Z :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (nps adt)
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (nps adt)
| _ ⇒ None
end.
primitve: set the allocated-bit of the i-th page
Function set_at_u_spec (i: Z) (b: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZtoBool b with
| Some b´ ⇒
match ZMap.get i (AT adt) with
| ATValid b1 ATNorm ⇒ Some adt {AT: ZMap.set i (ATValid b´ ATNorm) (AT adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZtoBool b with
| Some b´ ⇒
match ZMap.get i (AT adt) with
| ATValid b1 ATNorm ⇒ Some adt {AT: ZMap.set i (ATValid b´ ATNorm) (AT adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
primitve: set the type of the i-th page
Function set_at_norm_spec (i: Z) (n: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, LockFalse) ⇒
if zle_lt 0 i maxpage then
match ZtoATType n with
| Some t ⇒ Some adt {AT: ZMap.set i (ATValid false t) (AT adt)}
{ATC: ZMap.set i (ATCValid 0) (ATC adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_at_c_spec (i: Z) (n: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒ Some adt {ATC: ZMap.set i (ATCValid n) (ATC adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_at_c0_spec (i: Z) (n: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒
Some adt {ATC: ZMap.set i (ATCValid n) (ATC adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, LockFalse) ⇒
if zle_lt 0 i maxpage then
match ZtoATType n with
| Some t ⇒ Some adt {AT: ZMap.set i (ATValid false t) (AT adt)}
{ATC: ZMap.set i (ATCValid 0) (ATC adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_at_c_spec (i: Z) (n: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒ Some adt {ATC: ZMap.set i (ATCValid n) (ATC adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function set_at_c0_spec (i: Z) (n: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i maxpage then
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒
Some adt {ATC: ZMap.set i (ATCValid n) (ATC adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
primitve: set number of pages
Function set_nps_spec (n: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt {nps: n}
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt {nps: n}
| _ ⇒ None
end.
primitive: initialize the allocation table
Function mem_init_spec (mbi_adr: Z) (adt: RData) : option RData :=
match (init adt, pg adt, ikern adt, ihost adt, in_intr adt) with
| (false, false, 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}
{MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo}
{AT: real_AT (AT adt)}
{ATC: real_ATC (ATC adt)}
{nps: real_nps} {AC: AC_init} {init: true}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
match (init adt, pg adt, ikern adt, ihost adt, in_intr adt) with
| (false, false, 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}
{MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo}
{AT: real_AT (AT adt)}
{ATC: real_ATC (ATC adt)}
{nps: real_nps} {AC: AC_init} {init: true}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
primitive: initialize the allocation table
Function lmem_init_spec (mbi_adr: Z) (adt: RData) : option RData :=
match (init adt, pg adt, ikern adt, ihost adt, in_intr adt) with
| (false, false, 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}
{MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo}
{ATC: real_ATC (ATC adt)}
{nps: real_nps} {AC: AC_init} {init: true}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
Function mem_init0_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}
{MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo}
{ATC: real_ATC (ATC adt)}
{nps: real_nps} {AC: AC_init} {init: true}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
match (init adt, pg adt, ikern adt, ihost adt, in_intr adt) with
| (false, false, 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}
{MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo}
{ATC: real_ATC (ATC adt)}
{nps: real_nps} {AC: AC_init} {init: true}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
Function mem_init0_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}
{MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo}
{ATC: real_ATC (ATC adt)}
{nps: real_nps} {AC: AC_init} {init: true}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
primitve: free the i-th page, only used in the refienment proof
Function pfree´_spec (i: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt, init adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, true, LockOwn true) ⇒
if zle_lt 0 i maxpage then
match (ZMap.get i (AT adt), ZMap.get i (ATC adt), ZMap.get i (pperm adt)) with
| (ATValid true ATNorm, ATCValid 0, PGAlloc) ⇒
Some adt {AT: ZMap.set i (ATValid false ATNorm) (AT adt)}
{pperm: ZMap.set i PGUndef (pperm adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
match (ikern adt, ihost adt, init adt, ZMap.get lock_AT_start (lock adt)) with
| (true, true, true, LockOwn true) ⇒
if zle_lt 0 i maxpage then
match (ZMap.get i (AT adt), ZMap.get i (ATC adt), ZMap.get i (pperm adt)) with
| (ATValid true ATNorm, ATCValid 0, PGAlloc) ⇒
Some adt {AT: ZMap.set i (ATValid false ATNorm) (AT adt)}
{pperm: ZMap.set i PGUndef (pperm adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
primitve: alloc a page and returns the page index
Function palloc_aux_spec (n: Z) (adt: RData): option (RData × Z) :=
match (ikern adt, init adt, ihost adt) with
| (true, true, true) ⇒
let c := ZMap.get n (AC adt) in
match cused c with
| true ⇒
if (cusage c) <? (cquota c) then
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
match first_free (AT adt) (nps adt) with
| inleft (exist i _) ⇒
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒
Some (adt {AT: ZMap.set i (ATValid true ATNorm) (AT adt)}
{ATC: ZMap.set i (ATCValid 0) (ATC adt)}
{pperm: ZMap.set i PGAlloc (pperm adt)}
{AC: ZMap.set n cur (AC adt)},i)
| _ ⇒ None
end
| _ ⇒ Some (adt, 0)
end
else Some (adt, 0)
| _ ⇒ None
end
| _ ⇒ None
end.
Function palloc´_spec (n: Z) (adt: RData): option (RData × Z) :=
match acquire_lock_AT_spec adt with
| Some adt´ ⇒
match palloc_aux_spec n adt´ with
| Some (adt0, i) ⇒
match release_lock_AT_spec adt0 with
| Some adt´´ ⇒ Some (adt´´, i)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Lemma palloc_aux_inv_prop:
∀ n d d´ v,
palloc_aux_spec n d = Some (d´, v) →
init d´ = true
∧ PT d´ = PT d
∧ (v ≠ 0 → ZMap.get v (pperm d´) = PGAlloc).
Proof.
unfold palloc_aux_spec. intros.
subdestruct; inv H; simpl; subst.
- rewrite ZMap.gss. refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
Lemma acquire_lock_AT_inv_prop:
∀ d d´,
acquire_lock_AT_spec d = Some d´ →
init d´ = init d
∧ PT d´ = PT d
∧ pperm d´ = pperm d.
Proof.
intros. unfold acquire_lock_AT_spec in ×.
subdestruct; inv H; simpl; refine_split´; trivial.
Qed.
Lemma release_lock_AT_inv_prop:
∀ d d´,
release_lock_AT_spec d = Some d´ →
init d´ = init d
∧ PT d´ = PT d
∧ pperm d´ = pperm d.
Proof.
intros. unfold release_lock_AT_spec in ×.
subdestruct; inv H; simpl; refine_split´; trivial.
Qed.
Lemma palloc´_inv_prop:
∀ n d d´ v,
palloc´_spec n d = Some (d´, v) →
init d´ = true
∧ PT d´ = PT d
∧ (v ≠ 0 → ZMap.get v (pperm d´) = PGAlloc).
Proof.
intros. functional inversion H; simpl; subst.
eapply acquire_lock_AT_inv_prop in H2.
destruct H2 as (? & ? & ?).
eapply release_lock_AT_inv_prop in H4.
destruct H4 as (? & ? & ?).
eapply palloc_aux_inv_prop in H3.
destruct H3 as (? & ? & ?).
subrewrite´.
refine_split´; eauto.
Qed.
Function lpalloc_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, init adt, cused c) with
| (true, true, true, true) ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_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 CalAT_log_real l1 with
| Some a ⇒
match first_free a (nps adt) with
| inleft (exist i _) ⇒
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒
let l´ := (TEVENT cpu (TSHARED (OPALLOCE i))) :: l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{ATC: ZMap.set i (ATCValid 0) (ATC adt)}
{pperm: ZMap.set i PGAlloc (pperm adt)}
{AC: ZMap.set n cur (AC adt)},i)
| _ ⇒ None
end
| _ ⇒
let l´ := (TEVENT cpu (TSHARED (OPALLOCE 0))) :: l1 in
Some (adt{multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 0)
end
| _ ⇒ None
end
else
let l´ := (TEVENT cpu (TSHARED (OPALLOCE 0))) :: l1 in
Some (adt{multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 0)
| _,_ ⇒ None
end
| _ ⇒ None
end.
Lemma lpalloc_inv_prop:
∀ n d d´ v,
lpalloc_spec n d = Some (d´, v) →
init d´ = true
∧ PT d´ = PT d
∧ (v ≠ 0 → ZMap.get v (pperm d´) = PGAlloc).
Proof.
unfold lpalloc_spec. intros.
subdestruct; inv H; simpl; subst.
- rewrite ZMap.gss. refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
End WITHWAITTIME.
End OBJ_PMM.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Context {re1: relate_impl_iflags}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re300: relate_impl_cid}.
Context {re400: relate_impl_CPU_ID}.
match (ikern adt, init adt, ihost adt) with
| (true, true, true) ⇒
let c := ZMap.get n (AC adt) in
match cused c with
| true ⇒
if (cusage c) <? (cquota c) then
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
match first_free (AT adt) (nps adt) with
| inleft (exist i _) ⇒
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒
Some (adt {AT: ZMap.set i (ATValid true ATNorm) (AT adt)}
{ATC: ZMap.set i (ATCValid 0) (ATC adt)}
{pperm: ZMap.set i PGAlloc (pperm adt)}
{AC: ZMap.set n cur (AC adt)},i)
| _ ⇒ None
end
| _ ⇒ Some (adt, 0)
end
else Some (adt, 0)
| _ ⇒ None
end
| _ ⇒ None
end.
Function palloc´_spec (n: Z) (adt: RData): option (RData × Z) :=
match acquire_lock_AT_spec adt with
| Some adt´ ⇒
match palloc_aux_spec n adt´ with
| Some (adt0, i) ⇒
match release_lock_AT_spec adt0 with
| Some adt´´ ⇒ Some (adt´´, i)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Lemma palloc_aux_inv_prop:
∀ n d d´ v,
palloc_aux_spec n d = Some (d´, v) →
init d´ = true
∧ PT d´ = PT d
∧ (v ≠ 0 → ZMap.get v (pperm d´) = PGAlloc).
Proof.
unfold palloc_aux_spec. intros.
subdestruct; inv H; simpl; subst.
- rewrite ZMap.gss. refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
Lemma acquire_lock_AT_inv_prop:
∀ d d´,
acquire_lock_AT_spec d = Some d´ →
init d´ = init d
∧ PT d´ = PT d
∧ pperm d´ = pperm d.
Proof.
intros. unfold acquire_lock_AT_spec in ×.
subdestruct; inv H; simpl; refine_split´; trivial.
Qed.
Lemma release_lock_AT_inv_prop:
∀ d d´,
release_lock_AT_spec d = Some d´ →
init d´ = init d
∧ PT d´ = PT d
∧ pperm d´ = pperm d.
Proof.
intros. unfold release_lock_AT_spec in ×.
subdestruct; inv H; simpl; refine_split´; trivial.
Qed.
Lemma palloc´_inv_prop:
∀ n d d´ v,
palloc´_spec n d = Some (d´, v) →
init d´ = true
∧ PT d´ = PT d
∧ (v ≠ 0 → ZMap.get v (pperm d´) = PGAlloc).
Proof.
intros. functional inversion H; simpl; subst.
eapply acquire_lock_AT_inv_prop in H2.
destruct H2 as (? & ? & ?).
eapply release_lock_AT_inv_prop in H4.
destruct H4 as (? & ? & ?).
eapply palloc_aux_inv_prop in H3.
destruct H3 as (? & ? & ?).
subrewrite´.
refine_split´; eauto.
Qed.
Function lpalloc_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, init adt, cused c) with
| (true, true, true, true) ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_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 CalAT_log_real l1 with
| Some a ⇒
match first_free a (nps adt) with
| inleft (exist i _) ⇒
match ZMap.get i (ATC adt) with
| ATCValid _ ⇒
let l´ := (TEVENT cpu (TSHARED (OPALLOCE i))) :: l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{ATC: ZMap.set i (ATCValid 0) (ATC adt)}
{pperm: ZMap.set i PGAlloc (pperm adt)}
{AC: ZMap.set n cur (AC adt)},i)
| _ ⇒ None
end
| _ ⇒
let l´ := (TEVENT cpu (TSHARED (OPALLOCE 0))) :: l1 in
Some (adt{multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 0)
end
| _ ⇒ None
end
else
let l´ := (TEVENT cpu (TSHARED (OPALLOCE 0))) :: l1 in
Some (adt{multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 0)
| _,_ ⇒ None
end
| _ ⇒ None
end.
Lemma lpalloc_inv_prop:
∀ n d d´ v,
lpalloc_spec n d = Some (d´, v) →
init d´ = true
∧ PT d´ = PT d
∧ (v ≠ 0 → ZMap.get v (pperm d´) = PGAlloc).
Proof.
unfold lpalloc_spec. intros.
subdestruct; inv H; simpl; subst.
- rewrite ZMap.gss. refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
End WITHWAITTIME.
End OBJ_PMM.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Context {re1: relate_impl_iflags}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re300: relate_impl_cid}.
Context {re400: relate_impl_CPU_ID}.
Section MEMINIT_SIM.
Context `{real_params: RealParams}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_AT}.
Context {re30: relate_impl_ATC}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_MM}.
Context {re6: relate_impl_vmxinfo}.
Context {re7: relate_impl_AC}.
Context {re20: relate_impl_multi_log}.
Context {re8: relate_impl_ioapic}.
Context {re9: relate_impl_lapic}.
Context {re10: relate_impl_in_intr}.
Lemma mem_init_exist:
∀ s habd habd´ labd i f,
mem_init_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, mem_init_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold mem_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
apply relate_impl_lock_update.
apply relate_impl_multi_log_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_ATC_update.
apply relate_impl_AT_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_MMSize_update.
apply relate_impl_MM_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_nps}.
Context {mt3: match_impl_AT}.
Context {mt4: match_impl_MM}.
Context {mt5: match_impl_vmxinfo}.
Context {mt6: match_impl_AC}.
Context {mt50: match_impl_multi_log}.
Context {mt7: match_impl_ioapic}.
Context {mt8: match_impl_lapic}.
Context {mt0: match_impl_ATC}.
Lemma mem_init_match:
∀ s d d´ m i f,
mem_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold mem_init_spec; intros. subdestruct. inv H.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_ATC_update.
eapply match_impl_AT_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_MMSize_update.
eapply match_impl_MM_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) mem_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) mem_init_spec}.
Lemma mem_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem mem_init_spec)
(id ↦ gensem mem_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit mem_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply mem_init_match; eauto.
Qed.
End MEMINIT_SIM.
Section AT_SETTER_SIM.
Context {re2: relate_impl_AT}.
Context {mt1: match_impl_AT}.
Context {re20: relate_impl_ATC}.
Context {mt10: match_impl_ATC}.
Section SET_AT_U_SIM.
Lemma set_at_u_exist:
∀ s habd habd´ labd i z f,
set_at_u_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_at_u_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_at_u_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_AT_update. assumption.
Qed.
Lemma set_at_u_match:
∀ s d d´ m i z f,
set_at_u_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_at_u_spec; intros. subdestruct.
inv H. eapply match_impl_AT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_at_u_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_at_u_spec}.
Lemma set_at_u_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_at_u_spec)
(id ↦ gensem set_at_u_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_at_u_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_at_u_match; eauto.
Qed.
End SET_AT_U_SIM.
Section SET_AT_C_SIM.
Lemma set_at_c_exist:
∀ s habd habd´ labd i z f,
set_at_c_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_at_c_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_at_c_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ATC_update. assumption.
Qed.
Lemma set_at_c_match:
∀ s d d´ m i z f,
set_at_c_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_at_c_spec; intros. subdestruct.
inv H. eapply match_impl_ATC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_at_c_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_at_c_spec}.
Lemma set_at_c_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_at_c_spec)
(id ↦ gensem set_at_c_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_at_c_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_at_c_match; eauto.
Qed.
End SET_AT_C_SIM.
Section SET_AT_C0_SIM.
Lemma set_at_c0_exist:
∀ s habd habd´ labd i z f,
set_at_c0_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_at_c0_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_at_c0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ATC_update. assumption.
Qed.
Lemma set_at_c0_match:
∀ s d d´ m i z f,
set_at_c0_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_at_c0_spec; intros. subdestruct.
inv H. eapply match_impl_ATC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_at_c0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_at_c0_spec}.
Lemma set_at_c0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_at_c0_spec)
(id ↦ gensem set_at_c0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_at_c0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_at_c0_match; eauto.
Qed.
End SET_AT_C0_SIM.
End AT_SETTER_SIM.
Section AT_GETTER_SIM.
Context {re2: relate_impl_AT}.
Context {re20: relate_impl_ATC}.
Lemma is_at_norm_exist:
∀ s habd labd i z f,
is_at_norm_spec i habd = Some z
→ relate_AbData s f habd labd
→ is_at_norm_spec i labd = Some z.
Proof.
unfold is_at_norm_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_at_u_exist:
∀ s habd labd i z f,
get_at_u_spec i habd = Some z
→ relate_AbData s f habd labd
→ get_at_u_spec i labd = Some z.
Proof.
unfold get_at_u_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_at_c_exist:
∀ s habd labd i z f,
get_at_c_spec i habd = Some z
→ relate_AbData s f habd labd
→ get_at_c_spec i labd = Some z.
Proof.
unfold get_at_c_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_at_c_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_at_c_spec)
(id ↦ gensem get_at_c_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_at_c_exist; eauto. reflexivity.
Qed.
Lemma is_at_norm_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem is_at_norm_spec)
(id ↦ gensem is_at_norm_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite is_at_norm_exist; eauto. reflexivity.
Qed.
Lemma get_at_u_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_at_u_spec)
(id ↦ gensem get_at_u_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_at_u_exist; eauto. reflexivity.
Qed.
End AT_GETTER_SIM.
Section GET_NPS_SIM.
Context {re2: relate_impl_nps}.
Lemma get_nps_exist:
∀ s habd labd z f,
get_nps_spec habd = Some z
→ relate_AbData s f habd labd
→ get_nps_spec labd = Some z.
Proof.
unfold get_nps_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_nps_eq; eauto; intros.
revert H; subrewrite.
Qed.
Lemma get_nps_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_nps_spec)
(id ↦ gensem get_nps_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_nps_exist; eauto. reflexivity.
Qed.
End GET_NPS_SIM.
Section PALLOC´_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_AT}.
Context {re33: relate_impl_ATC}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_AC}.
Context {re20: relate_impl_multi_log}.
Context {re30: relate_impl_multi_oracle}.
Context `{waittime: WaitTime}.
Require Import TacticsForTesting.
Lemma palloc_aux_exist:
∀ s habd habd´ labd n i f,
palloc_aux_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_aux_spec n labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_aux_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_nps_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial; simpl.
- apply relate_impl_AC_update.
apply relate_impl_pperm_update.
apply relate_impl_ATC_update.
apply relate_impl_AT_update. assumption.
Qed.
Lemma palloc´_exist:
∀ s habd habd´ labd n i f,
palloc´_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc´_spec n labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
intros. functional inversion H.
unfold palloc´_spec.
exploit acquire_lock_AT_exist; eauto.
intros (labd0 & → & Hre0).
exploit palloc_aux_exist; eauto.
intros (labd1 & → & Hre1).
exploit release_lock_AT_exist; eauto.
intros (labd´´ & → & Hre´).
refine_split´; trivial.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_AT}.
Context {mt22: match_impl_ATC}.
Context {mt3: match_impl_AC}.
Context {mt4: match_impl_lock}.
Context {mt5: match_impl_multi_log}.
Lemma palloc_aux_match:
∀ s d d´ m i n f,
palloc_aux_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold palloc_aux_spec; intros.
subdestruct; inv H; subst; trivial.
eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_ATC_update.
eapply match_impl_AT_update.
trivial.
Qed.
Lemma palloc´_match:
∀ s d d´ m n i f,
palloc´_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
intros. functional inversion H; subst.
eapply release_lock_AT_match; eauto.
eapply palloc_aux_match; eauto.
eapply acquire_lock_AT_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) palloc´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) palloc´_spec}.
Lemma palloc´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem palloc´_spec)
(id ↦ gensem palloc´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit palloc´_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply palloc´_match; eauto.
Qed.
End PALLOC´_SIM.
Section LPALLOC_SIM.
Context {re2: relate_impl_init}.
Context {re33: relate_impl_ATC}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_AC}.
Context {re20: relate_impl_multi_log}.
Context {re30: relate_impl_multi_oracle}.
Context `{real_params: RealParams}.
Lemma lpalloc_exist:
∀ s habd habd´ labd n i f,
lpalloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, lpalloc_spec n labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lpalloc_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_nps_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial; simpl.
- apply relate_impl_AC_update.
apply relate_impl_pperm_update.
apply relate_impl_ATC_update.
apply relate_impl_multi_log_update.
assumption.
- apply relate_impl_multi_log_update.
assumption.
- apply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt22: match_impl_ATC}.
Context {mt3: match_impl_AC}.
Context {mt4: match_impl_lock}.
Context {mt5: match_impl_multi_log}.
Lemma lpalloc_match:
∀ s d d´ m i n f,
lpalloc_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lpalloc_spec; intros.
subdestruct; inv H; subst; trivial.
- eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_ATC_update.
eapply match_impl_multi_log_update.
trivial.
- eapply match_impl_multi_log_update.
trivial.
- eapply match_impl_multi_log_update.
trivial.
Qed.
Context {inv: PreservesInvariants (HD:= data) lpalloc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lpalloc_spec}.
Lemma lpalloc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lpalloc_spec)
(id ↦ gensem lpalloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lpalloc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lpalloc_match; eauto.
Qed.
End LPALLOC_SIM.
Section PFREE´_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_AT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re33: relate_impl_ATC}.
Lemma pfree´_exist:
∀ s habd habd´ labd i f,
pfree´_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pfree´_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pfree´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pperm_update.
apply relate_impl_AT_update. assumption.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_AT}.
Lemma pfree´_match:
∀ s d d´ m i f,
pfree´_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pfree´_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pperm_update.
eapply match_impl_AT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pfree´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pfree´_spec}.
Lemma pfree´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pfree´_spec)
(id ↦ gensem pfree´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pfree´_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pfree´_match; eauto.
Qed.
End PFREE´_SIM.
End OBJ_SIM.
Context `{real_params: RealParams}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_AT}.
Context {re30: relate_impl_ATC}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_MM}.
Context {re6: relate_impl_vmxinfo}.
Context {re7: relate_impl_AC}.
Context {re20: relate_impl_multi_log}.
Context {re8: relate_impl_ioapic}.
Context {re9: relate_impl_lapic}.
Context {re10: relate_impl_in_intr}.
Lemma mem_init_exist:
∀ s habd habd´ labd i f,
mem_init_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, mem_init_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold mem_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
apply relate_impl_lock_update.
apply relate_impl_multi_log_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_ATC_update.
apply relate_impl_AT_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_MMSize_update.
apply relate_impl_MM_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_nps}.
Context {mt3: match_impl_AT}.
Context {mt4: match_impl_MM}.
Context {mt5: match_impl_vmxinfo}.
Context {mt6: match_impl_AC}.
Context {mt50: match_impl_multi_log}.
Context {mt7: match_impl_ioapic}.
Context {mt8: match_impl_lapic}.
Context {mt0: match_impl_ATC}.
Lemma mem_init_match:
∀ s d d´ m i f,
mem_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold mem_init_spec; intros. subdestruct. inv H.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_ATC_update.
eapply match_impl_AT_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_MMSize_update.
eapply match_impl_MM_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) mem_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) mem_init_spec}.
Lemma mem_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem mem_init_spec)
(id ↦ gensem mem_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit mem_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply mem_init_match; eauto.
Qed.
End MEMINIT_SIM.
Section AT_SETTER_SIM.
Context {re2: relate_impl_AT}.
Context {mt1: match_impl_AT}.
Context {re20: relate_impl_ATC}.
Context {mt10: match_impl_ATC}.
Section SET_AT_U_SIM.
Lemma set_at_u_exist:
∀ s habd habd´ labd i z f,
set_at_u_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_at_u_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_at_u_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_AT_update. assumption.
Qed.
Lemma set_at_u_match:
∀ s d d´ m i z f,
set_at_u_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_at_u_spec; intros. subdestruct.
inv H. eapply match_impl_AT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_at_u_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_at_u_spec}.
Lemma set_at_u_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_at_u_spec)
(id ↦ gensem set_at_u_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_at_u_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_at_u_match; eauto.
Qed.
End SET_AT_U_SIM.
Section SET_AT_C_SIM.
Lemma set_at_c_exist:
∀ s habd habd´ labd i z f,
set_at_c_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_at_c_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_at_c_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ATC_update. assumption.
Qed.
Lemma set_at_c_match:
∀ s d d´ m i z f,
set_at_c_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_at_c_spec; intros. subdestruct.
inv H. eapply match_impl_ATC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_at_c_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_at_c_spec}.
Lemma set_at_c_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_at_c_spec)
(id ↦ gensem set_at_c_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_at_c_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_at_c_match; eauto.
Qed.
End SET_AT_C_SIM.
Section SET_AT_C0_SIM.
Lemma set_at_c0_exist:
∀ s habd habd´ labd i z f,
set_at_c0_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_at_c0_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold set_at_c0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ATC_update. assumption.
Qed.
Lemma set_at_c0_match:
∀ s d d´ m i z f,
set_at_c0_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_at_c0_spec; intros. subdestruct.
inv H. eapply match_impl_ATC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_at_c0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_at_c0_spec}.
Lemma set_at_c0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_at_c0_spec)
(id ↦ gensem set_at_c0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_at_c0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_at_c0_match; eauto.
Qed.
End SET_AT_C0_SIM.
End AT_SETTER_SIM.
Section AT_GETTER_SIM.
Context {re2: relate_impl_AT}.
Context {re20: relate_impl_ATC}.
Lemma is_at_norm_exist:
∀ s habd labd i z f,
is_at_norm_spec i habd = Some z
→ relate_AbData s f habd labd
→ is_at_norm_spec i labd = Some z.
Proof.
unfold is_at_norm_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_at_u_exist:
∀ s habd labd i z f,
get_at_u_spec i habd = Some z
→ relate_AbData s f habd labd
→ get_at_u_spec i labd = Some z.
Proof.
unfold get_at_u_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_at_c_exist:
∀ s habd labd i z f,
get_at_c_spec i habd = Some z
→ relate_AbData s f habd labd
→ get_at_c_spec i labd = Some z.
Proof.
unfold get_at_c_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_at_c_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_at_c_spec)
(id ↦ gensem get_at_c_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_at_c_exist; eauto. reflexivity.
Qed.
Lemma is_at_norm_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem is_at_norm_spec)
(id ↦ gensem is_at_norm_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite is_at_norm_exist; eauto. reflexivity.
Qed.
Lemma get_at_u_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_at_u_spec)
(id ↦ gensem get_at_u_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_at_u_exist; eauto. reflexivity.
Qed.
End AT_GETTER_SIM.
Section GET_NPS_SIM.
Context {re2: relate_impl_nps}.
Lemma get_nps_exist:
∀ s habd labd z f,
get_nps_spec habd = Some z
→ relate_AbData s f habd labd
→ get_nps_spec labd = Some z.
Proof.
unfold get_nps_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_nps_eq; eauto; intros.
revert H; subrewrite.
Qed.
Lemma get_nps_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_nps_spec)
(id ↦ gensem get_nps_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_nps_exist; eauto. reflexivity.
Qed.
End GET_NPS_SIM.
Section PALLOC´_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_AT}.
Context {re33: relate_impl_ATC}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_AC}.
Context {re20: relate_impl_multi_log}.
Context {re30: relate_impl_multi_oracle}.
Context `{waittime: WaitTime}.
Require Import TacticsForTesting.
Lemma palloc_aux_exist:
∀ s habd habd´ labd n i f,
palloc_aux_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_aux_spec n labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_aux_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_nps_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial; simpl.
- apply relate_impl_AC_update.
apply relate_impl_pperm_update.
apply relate_impl_ATC_update.
apply relate_impl_AT_update. assumption.
Qed.
Lemma palloc´_exist:
∀ s habd habd´ labd n i f,
palloc´_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc´_spec n labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
intros. functional inversion H.
unfold palloc´_spec.
exploit acquire_lock_AT_exist; eauto.
intros (labd0 & → & Hre0).
exploit palloc_aux_exist; eauto.
intros (labd1 & → & Hre1).
exploit release_lock_AT_exist; eauto.
intros (labd´´ & → & Hre´).
refine_split´; trivial.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_AT}.
Context {mt22: match_impl_ATC}.
Context {mt3: match_impl_AC}.
Context {mt4: match_impl_lock}.
Context {mt5: match_impl_multi_log}.
Lemma palloc_aux_match:
∀ s d d´ m i n f,
palloc_aux_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold palloc_aux_spec; intros.
subdestruct; inv H; subst; trivial.
eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_ATC_update.
eapply match_impl_AT_update.
trivial.
Qed.
Lemma palloc´_match:
∀ s d d´ m n i f,
palloc´_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
intros. functional inversion H; subst.
eapply release_lock_AT_match; eauto.
eapply palloc_aux_match; eauto.
eapply acquire_lock_AT_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) palloc´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) palloc´_spec}.
Lemma palloc´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem palloc´_spec)
(id ↦ gensem palloc´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit palloc´_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply palloc´_match; eauto.
Qed.
End PALLOC´_SIM.
Section LPALLOC_SIM.
Context {re2: relate_impl_init}.
Context {re33: relate_impl_ATC}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_AC}.
Context {re20: relate_impl_multi_log}.
Context {re30: relate_impl_multi_oracle}.
Context `{real_params: RealParams}.
Lemma lpalloc_exist:
∀ s habd habd´ labd n i f,
lpalloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, lpalloc_spec n labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold lpalloc_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_nps_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_multi_log_eq; eauto; intros.
exploit relate_impl_multi_oracle_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial; simpl.
- apply relate_impl_AC_update.
apply relate_impl_pperm_update.
apply relate_impl_ATC_update.
apply relate_impl_multi_log_update.
assumption.
- apply relate_impl_multi_log_update.
assumption.
- apply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt22: match_impl_ATC}.
Context {mt3: match_impl_AC}.
Context {mt4: match_impl_lock}.
Context {mt5: match_impl_multi_log}.
Lemma lpalloc_match:
∀ s d d´ m i n f,
lpalloc_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold lpalloc_spec; intros.
subdestruct; inv H; subst; trivial.
- eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_ATC_update.
eapply match_impl_multi_log_update.
trivial.
- eapply match_impl_multi_log_update.
trivial.
- eapply match_impl_multi_log_update.
trivial.
Qed.
Context {inv: PreservesInvariants (HD:= data) lpalloc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) lpalloc_spec}.
Lemma lpalloc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem lpalloc_spec)
(id ↦ gensem lpalloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit lpalloc_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply lpalloc_match; eauto.
Qed.
End LPALLOC_SIM.
Section PFREE´_SIM.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_AT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re33: relate_impl_ATC}.
Lemma pfree´_exist:
∀ s habd habd´ labd i f,
pfree´_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pfree´_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pfree´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_AT_eq; eauto; intros.
exploit relate_impl_ATC_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pperm_update.
apply relate_impl_AT_update. assumption.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_AT}.
Lemma pfree´_match:
∀ s d d´ m i f,
pfree´_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pfree´_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pperm_update.
eapply match_impl_AT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pfree´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pfree´_spec}.
Lemma pfree´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pfree´_spec)
(id ↦ gensem pfree´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pfree´_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pfree´_match; eauto.
Qed.
End PFREE´_SIM.
End OBJ_SIM.