Library mcertikos.objects.ObjContainer
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import Constant.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Section PRIM_Container.
Context `{real_params: RealParams}.
Definition container_first_unused (C: ContainerPool) (size: Z) :
{iii | 0 < iii < size ∧ cused (ZMap.get iii C) = false ∧
∀ x, 0 < x < iii → cused (ZMap.get x C) ≠ false} +
{∀ x, 0 < x < size → cused (ZMap.get x C) ≠ false}.
Proof.
apply min_ex; intros.
destruct (cused (ZMap.get n C)); [right; discriminate | left; auto].
Defined.
Definition container_first_used (C: ContainerPool) (size: Z) :
{iii | 0 < iii < size ∧ cused (ZMap.get iii C) = true ∧
∀ x, 0 < x < iii → cused (ZMap.get x C) ≠ true} +
{∀ x, 0 < x < size → cused (ZMap.get x C) ≠ true}.
Proof.
apply min_ex; intros.
destruct (cused (ZMap.get n C)); [left; auto | right; discriminate].
Defined.
Function container_init_spec (mbi: Z) (adt: RData) : option RData :=
match (pg adt, in_intr adt, ikern adt, ihost adt, init 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}
{AC: AC_init} {init: true})
else
None
else
None
| _ ⇒ None
end.
Function container_get_parent_spec (i: Z) (adt: RData): option Z :=
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (cparent c)
| _ ⇒ None
end.
Function container_get_quota_spec (i: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (cquota c)
| _ ⇒ None
end.
Function container_get_usage_spec (i: Z) (adt: RData): option Z :=
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (cusage c)
| _ ⇒ None
end.
Function container_can_consume_spec (i: Z) (n: Z) (adt: RData) : option Z :=
match (ikern adt, ihost adt, cused (ZMap.get i (AC adt))) with
| (true, true, true) ⇒
Some (if zle_le 0 n (cquota (ZMap.get i (AC adt)) - cusage (ZMap.get i (AC adt)))
then 1 else 0)
| _ ⇒ None
end.
Function container_split_spec (i: Z) (n: Z) (j: Z) (adt: RData) : option (RData×Z) :=
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c, cused (ZMap.get j (AC adt)),
zlt_lt 0 j num_id, zle_le 0 n (cquota c - cusage c)) with
| (true, true, true, false, left _, left _) ⇒
let child := mkContainer n 0 i nil true in
let cur := mkContainer (cquota c) (cusage c + n) (cparent c)
(j :: cchildren c) (cused c) in
Some (adt {AC: ZMap.set j child (ZMap.set i cur (AC adt))}, j)
| _ ⇒ None
end.
Function container_alloc_spec (i: Z) (adt: RData) : option (RData×Z) :=
let c := ZMap.get i (AC adt) in
match (init adt, ikern adt, ihost adt, cused c) with
| (true, true, true, true) ⇒
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
if (cusage c) <? (cquota c)
then Some (adt {AC: ZMap.set i cur (AC adt)}, 1)
else Some (adt, 0)
| _ ⇒ None
end.
End PRIM_Container.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
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 {re2: relate_impl_init}.
Context {re3: relate_impl_AC}.
Section CONTAINER_INIT_SIM.
Context `{real_params: RealParams}.
Context {re4: relate_impl_MM}.
Context {re5: relate_impl_vmxinfo}.
Context {re6: relate_impl_in_intr}.
Context {re7: relate_impl_ioapic}.
Context {re8: relate_impl_lapic}.
Lemma container_init_exist:
∀ s habd habd´ labd mbi f,
container_init_spec mbi habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, container_init_spec mbi labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold container_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_ioapic_eq; eauto.
exploit relate_impl_lapic_eq; eauto.
exploit relate_impl_AC_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
apply relate_impl_init_update.
apply relate_impl_AC_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 {mt2: match_impl_init}.
Context {mt3: match_impl_AC}.
Context {mt4: match_impl_MM}.
Context {mt5: match_impl_vmxinfo}.
Context {mt6: match_impl_ioapic}.
Context {mt7: match_impl_lapic}.
Lemma container_init_match:
∀ s d d´ m mbi f,
container_init_spec mbi d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold container_init_spec; intros. subdestruct. inv H.
eapply match_impl_init_update.
eapply match_impl_AC_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) container_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) container_init_spec}.
Lemma container_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem container_init_spec)
(id ↦ gensem container_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit container_init_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply container_init_match; eauto.
Qed.
End CONTAINER_INIT_SIM.
Section CONTAINER_GET_PARENT_SIM.
Lemma container_get_parent_exist:
∀ s habd labd i p f,
container_get_parent_spec i habd = Some p
→ relate_AbData s f habd labd
→ container_get_parent_spec i labd = Some p.
Proof.
unfold container_get_parent_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma container_get_parent_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem container_get_parent_spec)
(id ↦ gensem container_get_parent_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite container_get_parent_exist; eauto 1.
reflexivity.
Qed.
End CONTAINER_GET_PARENT_SIM.
Section CONTAINER_GET_QUOTA_SIM.
Lemma container_get_quota_exist:
∀ s habd labd i p f,
container_get_quota_spec i habd = Some p
→ relate_AbData s f habd labd
→ container_get_quota_spec i labd = Some p.
Proof.
unfold container_get_quota_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma container_get_quota_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem container_get_quota_spec)
(id ↦ gensem container_get_quota_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite container_get_quota_exist; eauto 1.
reflexivity.
Qed.
End CONTAINER_GET_QUOTA_SIM.
Section CONTAINER_GET_USAGE_SIM.
Lemma container_get_usage_exist:
∀ s habd labd i p f,
container_get_usage_spec i habd = Some p
→ relate_AbData s f habd labd
→ container_get_usage_spec i labd = Some p.
Proof.
unfold container_get_usage_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma container_get_usage_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem container_get_usage_spec)
(id ↦ gensem container_get_usage_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite container_get_usage_exist; eauto 1.
reflexivity.
Qed.
End CONTAINER_GET_USAGE_SIM.
Section CONTAINER_CAN_CONSUME_SIM.
Lemma container_can_consume_exist:
∀ s habd labd i n b f,
container_can_consume_spec i n habd = Some b
→ relate_AbData s f habd labd
→ container_can_consume_spec i n labd = Some b.
Proof.
unfold container_can_consume_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma container_can_consume_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem container_can_consume_spec)
(id ↦ gensem container_can_consume_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite container_can_consume_exist; eauto 1.
reflexivity.
Qed.
End CONTAINER_CAN_CONSUME_SIM.
Section CONTAINER_SPLIT_SIM.
Lemma container_split_exist:
∀ s habd habd´ labd i n j z f,
container_split_spec i n j habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, container_split_spec i n j labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold container_split_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_AC_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
apply relate_impl_AC_update. assumption.
Qed.
Context {mt2: match_impl_AC}.
Lemma container_split_match:
∀ s d d´ m i n j z f,
container_split_spec i n j d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold container_split_spec; intros. subdestruct. inv H.
eapply match_impl_AC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) container_split_spec}.
Context {inv0: PreservesInvariants (HD:= data0) container_split_spec}.
Lemma container_split_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem container_split_spec)
(id ↦ gensem container_split_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit container_split_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply container_split_match; eauto.
Qed.
End CONTAINER_SPLIT_SIM.
Section CONTAINER_ALLOC_SIM.
Lemma container_alloc_exist:
∀ s habd habd´ labd i f z,
container_alloc_spec i habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, container_alloc_spec i labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold container_alloc_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_AC_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_AC_update. assumption.
Qed.
Context {mt2: match_impl_AC}.
Lemma container_alloc_match:
∀ s d d´ m i f z,
container_alloc_spec i d = Some (d´,z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold container_alloc_spec; intros.
subdestruct; inv H; auto.
eapply match_impl_AC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) container_alloc_spec}.
Context {inv0: PreservesInvariants (HD:= data0) container_alloc_spec}.
Lemma container_alloc_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem container_alloc_spec)
(id ↦ gensem container_alloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit container_alloc_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply container_alloc_match; eauto.
Qed.
End CONTAINER_ALLOC_SIM.
End OBJ_SIM.