Library mcertikos.objects.ObjContainer
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 CalTicketLock.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Require Import Constant.
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, ikern adt, ihost adt, init adt, in_intr adt) with
| (false, true, true, false, 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}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)})
else
None
else
None
| _ ⇒ None
end.
Function container_set_usage_spec (i: Z) (usage_val: Z) (adt: RData): option RData :=
if zle_lt 0 i num_proc then
if zle_le 0 usage_val (cquota (ZMap.get i (AC adt))) then
let c := ZMap.get i (AC adt) in
match (init adt, ikern adt, ihost adt, cused c) with
| (true, true, true, true) ⇒
let new_c := mkContainer (cquota c) usage_val (cparent c) (cchildren c) (cused c) in
Some (adt {AC : ZMap.set i new_c (AC adt)})
| _ ⇒ None
end
else None
else None.
Function container_set_nchildren_spec (i: Z) (next_child: Z) (adt: RData): option RData :=
if zle_lt 0 i num_proc then
let c := ZMap.get i (AC adt) in
if zlt (Z_of_nat (length (cchildren c))) max_children then
match (init adt, ikern adt, ihost adt, cused c) with
| (true, true, true, true) ⇒
let new_c := mkContainer (cquota c) (cusage c) (cparent c) (next_child::(cchildren c)) (cused c) in
Some (adt {AC : ZMap.set i new_c (AC adt)})
| _ ⇒ None
end
else None
else None.
Function container_node_init_spec (i: Z) (q_val: Z) (p_val : Z) (adt: RData): option RData :=
if zle_lt 0 i num_proc then
if zle_le 0 q_val Int.max_unsigned then
if zle_lt 0 p_val num_proc then
match (init adt, ikern adt, ihost adt) with
| (true, true, true) ⇒
let new_c := mkContainer q_val 0 p_val nil true in
Some (adt {AC : ZMap.set i new_c (AC adt)})
| _ ⇒ None
end
else None
else None
else None.
Function container_get_parent_intro_spec (i: Z) (adt: RData): option Z :=
if zle_lt 0 i num_proc then
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (cparent c)
| _ ⇒ None
end
else None.
Function container_get_nchildren_intro_spec (i: Z) (adt: RData) : option Z :=
if zle_lt 0 i num_proc then
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (Z_of_nat (length (cchildren c)))
| _ ⇒ None
end
else None.
Function container_get_quota_intro_spec (i: Z) (adt: RData) : option Z :=
if zle_lt 0 i num_proc then
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (cquota c)
| _ ⇒ None
end
else None.
Function container_get_usage_intro_spec (i: Z) (adt: RData): option Z :=
if zle_lt 0 i num_proc then
let c := ZMap.get i (AC adt) in
match (ikern adt, ihost adt, cused c) with
| (true, true, true) ⇒ Some (cusage c)
| _ ⇒ None
end
else None.
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_nchildren_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 (Z_of_nat (length (cchildren 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 (id: Z) (q: Z) (adt: RData) : option (RData×Z) :=
let c := ZMap.get id (AC adt) in
let i := id × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (ikern adt, ihost adt, cused c, cused (ZMap.get i (AC adt)), zle_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, false, left _, left _, left _) ⇒
let child := mkContainer q 0 id nil true in
let cur := mkContainer (cquota c) (cusage c + q) (cparent c)
(i :: cchildren c) (cused c) in
Some (adt {AC: ZMap.set i child (ZMap.set id cur (AC adt))}, i)
| _ ⇒ 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.
Function container_can_consume_intro_spec (i: Z) (n: Z) (adt: RData) : option Z :=
if zle_lt 0 i num_proc then
if zle (cquota (ZMap.get i (AC adt))) Int.max_unsigned then
if zle_le 0 (cusage (ZMap.get i (AC adt))) (cquota (ZMap.get i (AC adt))) then
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
else None
else None
else None.
Function container_alloc_intro_spec (i: Z) (adt: RData) : option (RData×Z) :=
if zle_lt 0 i num_proc then
if zle (cquota (ZMap.get i (AC adt))) Int.max_unsigned then
if zle_le 0 (cusage (ZMap.get i (AC adt))) (cquota (ZMap.get i (AC adt))) then
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
else None
else None
else None.
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 {re20: relate_impl_multi_log}.
Context {mt10: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {mt50: match_impl_multi_log}.
Context {re7: relate_impl_ioapic}.
Context {re8: relate_impl_lapic}.
Context {re9: relate_impl_in_intr}.
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; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_multi_log_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_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_lock_update.
eapply match_impl_multi_log_update.
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 z f,
container_split_spec i n habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, container_split_spec i n 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 z f,
container_split_spec i n 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.
Section CONTAINER_GET_NCHILDREN_SIM.
Lemma container_get_nchildren_exist:
∀ s habd labd i p f,
container_get_nchildren_spec i habd = Some p
→ relate_AbData s f habd labd
→ container_get_nchildren_spec i labd = Some p.
Proof.
unfold container_get_nchildren_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
revert H. subrewrite.
Qed.
Lemma container_get_nchildren_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem container_get_nchildren_spec)
(id ↦ gensem container_get_nchildren_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite container_get_nchildren_exist; eauto 1.
reflexivity.
Qed.
End CONTAINER_GET_NCHILDREN_SIM.
End OBJ_SIM.