Library mcertikos.mm.MALOpCode
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import TacticsForTesting.
Require Import CLemmas.
Require Import CommonTactic.
Require Import LoopProof.
Require Import MALOp.
Require Import MALOpCSource.
Require Import ALGenSpec.
Require Export ObjCPU.
Require Export ObjMM.
Require Export ObjFlatMem.
Require Export ObjContainer.
Require Export ObjMultiprocessor.
Require Export ObjQLock.
Require Import FutureTactic.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Module MALOPCODE.
Section With_primitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section PFree.
Let L: compatlayer (cdata RData) := at_set ↦ gensem set_at_u_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PFreeBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import TacticsForTesting.
Require Import CLemmas.
Require Import CommonTactic.
Require Import LoopProof.
Require Import MALOp.
Require Import MALOpCSource.
Require Import ALGenSpec.
Require Export ObjCPU.
Require Export ObjMM.
Require Export ObjFlatMem.
Require Export ObjContainer.
Require Export ObjMultiprocessor.
Require Export ObjQLock.
Require Import FutureTactic.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Module MALOPCODE.
Section With_primitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section PFree.
Let L: compatlayer (cdata RData) := at_set ↦ gensem set_at_u_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PFreeBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
at_set
Variable batset: block.
Hypothesis hat_set1 : Genv.find_symbol ge at_set = Some batset.
Hypothesis hat_set2 : Genv.find_funct_ptr ge batset =
Some (External (EF_external at_set
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma pfree_body_correct: ∀ m d d´ env le index,
env = PTree.empty _ →
PTree.get tpfree_index le = Some (Vint index)->
MALOp.pfree_spec (Int.unsigned index) d = Some d´ →
∃ le´,
(exec_stmt ge env le ((m, d): mem) pfree_body E0 le´ (m, d´) Out_normal).
Proof.
generalize max_unsigned_val; intro.
intros.
subst.
unfold pfree_body in ×.
functional inversion H2; subst.
esplit.
repeat vcgen.
Qed.
End PFreeBody.
Theorem pfree_code_correct:
spec_le (pfree ↦ pfree_spec_low) (〚pfree ↦ f_pfree 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pfree_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_pfree)
(Vint n::nil)
(create_undef_temps (fn_temps f_pfree)))) H0.
Qed.
End PFree.
Section PAlloc.
Let L: compatlayer (cdata RData) :=
get_nps ↦ gensem get_nps_spec
⊕ is_norm ↦ gensem is_at_norm_spec
⊕ at_get ↦ gensem get_at_u_spec
⊕ at_set ↦ gensem set_at_u_spec
⊕ at_set_c ↦ gensem set_at_c_spec
⊕ acquire_lock_AT ↦ gensem acquire_lock_AT_spec
⊕ release_lock_AT ↦ gensem release_lock_AT_spec
⊕ container_alloc ↦ gensem container_alloc_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PallocBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
External functions from lower layers
get_nps
Variable bgetnps: block.
Hypothesis hget_nps1 : Genv.find_symbol ge get_nps = Some bgetnps.
Hypothesis hget_nps2 : Genv.find_funct_ptr ge bgetnps =
Some (External (EF_external get_nps
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
is_norm
Variable bisnorm: block.
Hypothesis hat_isnorm1 : Genv.find_symbol ge is_norm = Some bisnorm.
Hypothesis hat_isnorm2 : Genv.find_funct_ptr ge bisnorm =
Some (External (EF_external is_norm
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
at_get
Variable batget: block.
Hypothesis hat_get1 : Genv.find_symbol ge at_get = Some batget.
Hypothesis hat_get2 : Genv.find_funct_ptr ge batget =
Some (External (EF_external at_get
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
at_set
Variable batset: block.
Hypothesis hat_set1 : Genv.find_symbol ge at_set = Some batset.
Hypothesis hat_set2 : Genv.find_funct_ptr ge batset =
Some (External (EF_external at_set
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
at_set_c
Variable batset_c: block.
Hypothesis hat_set_c1 : Genv.find_symbol ge at_set_c = Some batset_c.
Hypothesis hat_set_c2 : Genv.find_funct_ptr ge batset_c =
Some (External (EF_external at_set_c
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
rel_lock
Variable brel: block.
Hypothesis hrel : Genv.find_symbol ge release_lock_AT = Some brel.
Hypothesis hrel2 : Genv.find_funct_ptr ge brel =
Some (External
(EF_external
release_lock_AT
(signature_of_type Tnil tvoid cc_default))
Tnil tvoid cc_default).
Hypothesis hrel : Genv.find_symbol ge release_lock_AT = Some brel.
Hypothesis hrel2 : Genv.find_funct_ptr ge brel =
Some (External
(EF_external
release_lock_AT
(signature_of_type Tnil tvoid cc_default))
Tnil tvoid cc_default).
acq_lock
Variable bacq: block.
Hypothesis hacq : Genv.find_symbol ge acquire_lock_AT = Some bacq.
Hypothesis hacq2 : Genv.find_funct_ptr ge bacq =
Some (External
(EF_external
acquire_lock_AT
(signature_of_type Tnil tvoid cc_default))
Tnil tvoid cc_default).
Hypothesis hacq : Genv.find_symbol ge acquire_lock_AT = Some bacq.
Hypothesis hacq2 : Genv.find_funct_ptr ge bacq =
Some (External
(EF_external
acquire_lock_AT
(signature_of_type Tnil tvoid cc_default))
Tnil tvoid cc_default).
container_alloc
Variable bcontainer_alloc: block.
Hypothesis hcontainer_alloc1 : Genv.find_symbol ge container_alloc = Some bcontainer_alloc.
Hypothesis hcontainer_alloc2 : Genv.find_funct_ptr ge bcontainer_alloc =
Some (External (EF_external container_alloc
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hcontainer_alloc1 : Genv.find_symbol ge container_alloc = Some bcontainer_alloc.
Hypothesis hcontainer_alloc2 : Genv.find_funct_ptr ge bcontainer_alloc =
Some (External (EF_external container_alloc
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Lemmas for local variables
Variable conid : int.
Lemma nps_range : ∀ d, high_level_invariant d → init d = true → kern_low ≤ nps d ≤ maxpage.
Proof.
intros.
inv H.
generalize (valid_nps H0); intro.
repeat autounfold; simpl.
repeat autounfold in ×.
omega.
Qed.
Lemma nps_representable : ∀ d, high_level_invariant d → init d = true → Int.unsigned (Int.repr (nps d)) = nps d.
Proof.
intros.
apply Int.unsigned_repr.
generalize (nps_range d H H0).
repeat autounfold; simpl.
omega.
Qed.
palloc loop proof section
Section Palloc_loop_proof.
Variable minit: memb.
Variable adt : RData.
Notation nps := (AbstractDataType.nps adt).
Variable n: int.
Hypothesis inv: high_level_invariant adt.
Hypothesis n_property: 0 < Int.unsigned n < nps ∧ ZMap.get (Int.unsigned n) (AT adt) =
ATValid false ATNorm ∨ Int.unsigned n = nps.
Hypothesis lt_n_not_free: (∀ x: Z, ((0 < x < Int.unsigned n)%Z →
ZMap.get x (AT adt) ≠ ATValid false ATNorm)).
Hypothesis initialized : init adt = true.
Hypothesis ikern: ikern adt = true.
Hypothesis ihost: ihost adt = true.
Hypothesis lockonwer: ZMap.get lock_AT_start (lock adt) = LockOwn true.
Lemma permission_valid : ∀ index,
0 < Int.unsigned index < nps →
∃ t1 t2, ZMap.get (Int.unsigned index) (AT adt) = ATValid t1 t2.
Proof.
intros.
generalize nps_range; intro nps_range.
inv inv.
simpl.
unfold AT_kern in valid_AT_kern.
unfold AT_usr in valid_AT_usr.
simpl in ×.
assert(0 ≤ Int.unsigned index < kern_low ∨
kern_high ≤ Int.unsigned index < AbstractDataType.nps adt ∨
kern_low ≤ Int.unsigned index < Z.min kern_high (AbstractDataType.nps adt)).
{
destruct (Zmin.Zmin_spec kern_high (AbstractDataType.nps adt)).
destruct H0.
rewrite H1.
omega.
destruct H0.
rewrite H1.
omega.
}
destruct H0.
- ∃ false.
∃ ATKern.
apply valid_AT_kern.
assumption.
trivial.
left.
assumption.
- destruct H0.
∃ false.
∃ ATKern.
apply valid_AT_kern.
trivial.
right.
trivial.
apply valid_AT_usr in H0.
destruct H0 as [b].
∃ b.
destruct H0.
eauto.
eauto.
trivial.
Qed.
Local Open Scope Z_scope.
Lemma permission_norm : ∀ index, (0 < Int.unsigned index < nps) →
is_at_norm_spec (Int.unsigned index) adt = Some 0 ∨
is_at_norm_spec (Int.unsigned index) adt = Some 1.
Proof.
intros.
generalize (nps_range adt inv initialized); intro.
unfold is_at_norm_spec.
generalize(permission_valid index H); intro.
destruct H1 as [t1].
destruct H1 as [t2].
rewrite ikern, ihost.
unfold AuxFunctions.zle_lt.
autounfold in ×.
destruct (ZMap.get lock_AT_start (lock adt));
inv lockonwer.
repeat zdestruct.
destruct n_property.
- rewrite H1; eauto.
destruct (ATType_dec t2 ATNorm); tauto.
- rewrite H1; eauto.
destruct (ATType_dec t2 ATNorm); tauto.
Qed.
Lemma get_at_u_valid : ∀ index, is_at_norm_spec (Int.unsigned index) adt = Some 1 →
(get_at_u_spec (Int.unsigned index) adt = Some 0 ∨
get_at_u_spec (Int.unsigned index) adt = Some 1).
Proof.
intros.
unfold is_at_norm_spec in H.
unfold get_at_u_spec.
unfold AuxFunctions.zle_lt in ×.
autounfold in ×.
rewrite ikern, ihost in ×.
destruct (ZMap.get lock_AT_start (lock adt)). inv H.
inv lockonwer.
destruct (ZMap.get (Int.unsigned index) (AT adt)).
destruct b; auto.
repeat zdestruct.
repeat zdestruct.
repeat zdestruct.
Qed.
Definition palloc_index_valid (index: int): Prop :=
(ZMap.get (Int.unsigned index) (AT adt) = ATValid false ATNorm) ∧
∀ x, 0 < x < (Int.unsigned index) → ZMap.get x (AT adt) ≠ ATValid false ATNorm.
Lemma get_and_norm : ∀ index, 0 < Int.unsigned index < nps →
(∀ x: Z, 0 < x < Int.unsigned index →
ZMap.get x (AT adt) ≠
ATValid false ATNorm) →
is_at_norm_spec (Int.unsigned index) adt = Some 1 →
get_at_u_spec (Int.unsigned index) adt = Some 0 →
palloc_index_valid index.
Proof.
intros index indexrange indvalid isnorm atget.
generalize (nps_range adt inv initialized); intro.
unfold is_at_norm_spec in isnorm.
unfold get_at_u_spec in atget.
unfold palloc_index_valid.
unfold AuxFunctions.zle_lt in ×.
autounfold in ×.
rewrite ikern, ihost in ×.
destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
inv lockonwer.
repeat zdestruct.
destruct (ZMap.get (Int.unsigned index) (AT adt)).
- destruct b.
+ inversion atget.
+ destruct (ATType_dec t ATNorm); eauto.
× destruct t.
{ discriminate e. }
{ discriminate e. }
{ split.
esplit.
trivial. }
× inversion isnorm.
- discriminate isnorm.
Qed.
Lemma palloc_index_unique : ∀ index1 index2,
palloc_index_valid index1 →
palloc_index_valid index2 → Int.unsigned index1 > 0 →
Int.unsigned index2 > 0 → index1 = index2.
Proof.
intros index1 index2 valid1 valid2.
unfold palloc_index_valid in ×.
destruct valid1 as [valid1a valid1b].
destruct valid2 as [valid2a valid2b].
case_eq (Int.unsigned index1).
-
intros.
omega.
-
intro.
case_eq (Int.unsigned index2).
+
intros.
omega.
+
intros.
rewrite H in ×.
rewrite H0 in ×.
generalize (Zgt_pos_0 p); intro ppos.
generalize (Zgt_pos_0 p0); intro p0pos.
assert(Z.pos p0 < Z.pos p → False).
{ intro.
assert(ZMap.get (Z.pos p0) (AT adt) ≠ ATValid false ATNorm).
{
apply valid1b.
split.
omega.
assumption.
}
contradiction.
}
assert(Z.pos p < Z.pos p0 → False).
{
intro.
assert(ZMap.get (Z.pos p) (AT adt) ≠ ATValid false ATNorm).
{
apply valid2b.
split.
omega.
assumption.
}
contradiction.
}
assert(Z.pos p = Z.pos p0) by omega.
assert(Int.unsigned index1 = Int.unsigned index2).
{
rewrite H.
rewrite H0.
rewrite H5.
trivial.
}
apply unsigned_inj.
assumption.
+
intros.
generalize (Zlt_neg_0 p0).
omega.
-
intros.
generalize (Zlt_neg_0 p).
omega.
Qed.
Lemma palloc_index_invalid_norm : ∀ index,
is_at_norm_spec (Int.unsigned index) adt = Some 0 →
ZMap.get (Int.unsigned index) (AT adt) ≠ ATValid false ATNorm.
Proof.
intros.
intro.
unfold is_at_norm_spec in H.
unfold AuxFunctions.zle_lt in ×.
rewrite ikern, ihost in ×.
destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
inv lockonwer.
repeat zdestruct.
autounfold in ×.
rewrite H0 in H.
inversion H.
destruct (ATType_dec ATNorm ATNorm); eauto.
inv H2.
Qed.
Lemma palloc_index_invalid_atget : ∀ index,
get_at_u_spec (Int.unsigned index) adt = Some 1 →
ZMap.get (Int.unsigned index) (AT adt) ≠ ATValid false ATNorm.
Proof.
intros.
intro.
autounfold in ×.
unfold get_at_u_spec in H.
unfold AuxFunctions.zle_lt in ×.
rewrite ikern, ihost in ×.
destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
inv lockonwer.
repeat zdestruct.
rewrite H0 in H.
inversion H.
Qed.
Definition palloc_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get tnps le = Some (Vint (Int.repr nps)) ∧
PTree.get tpalloc_index le = Some (Vint (Int.repr 1)) ∧
PTree.get tpalloc_free_index le = Some (Vint (Int.repr nps)) ∧
PTree.get tid le = Some (Vint conid) ∧
ZMap.get lock_AT_start (lock adt) = LockOwn true ∧
m = (minit, adt).
Definition palloc_loop_body_Q (le : temp_env) (m: mem): Prop :=
PTree.get tpalloc_free_index le = Some (Vint n) ∧
PTree.get tnps le = Some (Vint (Int.repr nps)) ∧
PTree.get tid le = Some (Vint conid) ∧
ZMap.get lock_AT_start (lock adt) = LockOwn true ∧
m = (minit, adt).
Lemma palloc_loop_correct_aux : LoopProof.LoopProofSimpleWhile.t
palloc_while_condition palloc_while_body ge (PTree.empty _)
(palloc_loop_body_P) (palloc_loop_body_Q).
Proof.
generalize nps_range; intro nps_range.
generalize max_unsigned_val; intro max_unsignedval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ index,
PTree.get tpalloc_index le = Some (Vint index) ∧
PTree.get tnps le = Some (Vint (Int.repr nps)) ∧
PTree.get tid le = Some (Vint conid) ∧
ZMap.get lock_AT_start (lock adt) = LockOwn true ∧
(0 < Int.unsigned index ≤ nps) ∧
m = (minit, adt) ∧
w = nps - Int.unsigned index ∧
(PTree.get tpalloc_free_index le = Some (Vint n) ∨
PTree.get tpalloc_free_index le = Some (Vint (Int.repr nps)) ∧
(Int.unsigned index ≤ Int.unsigned n) ∧
(∀ x: Z, (0 < x < Int.unsigned index) →
ZMap.get x (AT adt) ≠ ATValid false ATNorm))
).
- apply Zwf_well_founded.
- intros.
unfold palloc_loop_body_P in H.
destruct H as [tnps_v H].
destruct H as [index_v H].
destruct H as [tpalloc_free_index_v H].
destruct H as [tid_v H].
destruct H as [lock_st H].
subst.
generalize (nps_range adt inv initialized); intro npsrange.
Caseeq n_property.
+ intro tmpn.
destruct tmpn as [tmpn1 tmpn2].
esplit. esplit.
repeat vcgen.
right.
split; auto.
split; auto.
omega.
intros.
apply lt_n_not_free; eauto.
omega.
+ intro tmpn.
subst.
esplit. esplit.
repeat vcgen.
left.
rewrite <- tmpn in tnps_v.
rewrite <- tmpn in tpalloc_free_index_v.
rewrite Int.repr_unsigned in tnps_v.
rewrite Int.repr_unsigned in tpalloc_free_index_v.
assumption.
- intros.
unfold palloc_while_condition.
unfold palloc_while_body.
unfold palloc_loop_body_Q.
destruct H as [index].
destruct H.
destruct H0.
destruct H1 as [ tid_eq_curid H1 ].
destruct H1 as [ lock_st H2].
destruct H2.
destruct H2.
destruct H3 as [n0val casefreeindex].
destruct H1 as [indexge0 caseindexnps].
apply Zle_lt_or_eq in caseindexnps.
subst.
generalize (nps_range adt inv initialized); intro npsrange.
Caseeq caseindexnps.
+
intros.
Caseeq casefreeindex.
×
intros.
Caseeq n_property.
{
intros.
destruct H3.
esplit. esplit.
repeat vcgen. }
{
intros.
assert(normcase: is_at_norm_spec (Int.unsigned index) adt = Some 0 ∨
is_at_norm_spec (Int.unsigned index) adt = Some 1).
apply permission_norm.
omega.
esplit. esplit.
repeat vcgen.
Caseeq normcase.
{
intro.
esplit. esplit.
change 0 with (Int.unsigned Int.zero) in H5.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
left.
rewrite PTree.gso.
rewrite PTree.gso.
assumption.
vcgen.
vcgen. }
{
intro.
generalize (get_at_u_valid index H5).
intro get_at_u_case.
Caseeq get_at_u_case.
{
intro.
unfold is_at_norm_spec in H5.
rewrite ikern, ihost in H5.
unfold get_at_u_spec in H6.
rewrite ikern, ihost in H6.
unfold AuxFunctions.zle_lt in ×.
repeat zdestruct.
case_eq (ZMap.get (Int.unsigned index) (AT adt)); intros.
{ rewrite H7 in H5, H6.
destruct b.
rewrite lock_st in ×.
destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
rewrite lock_st in ×.
inv lock_st.
destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
destruct (ATType_dec t ATNorm).
{ subst.
assert(0 < Int.unsigned index < Int.unsigned n) by omega.
generalize (lt_n_not_free (Int.unsigned index) H8); intro.
contradiction. }
{ discriminate H5. } }
{
rewrite lock_st in ×.
destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
rewrite H7 in H5; discriminate H5. } }
{
intros.
esplit. esplit.
replace 1 with (Int.unsigned Int.one) in H5, H6; try reflexivity.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
left.
rewrite PTree.gso; repeat vcgen. } } }
×
intro tcond.
destruct tcond as [freeind tcond].
destruct tcond as [indleqn leind].
Caseeq n_property.
{
intro tmpn.
destruct tmpn as [tmpn1 tmpn2].
esplit. esplit.
repeat vcgen.
assert(normcase: is_at_norm_spec (Int.unsigned index) adt = Some 0 ∨
is_at_norm_spec (Int.unsigned index) adt = Some 1).
apply permission_norm.
omega.
Caseeq normcase.
{
intro.
esplit. esplit.
change 0 with (Int.unsigned Int.zero) in H3.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
repeat vcgen.
{ assert(Int.unsigned index ≠ Int.unsigned n).
{ intro.
apply (palloc_index_invalid_norm _) in H3.
rewrite H4 in ×.
contradiction. }
omega. }
assert(LessOrEqual: 0≤ x< Int.unsigned index ∨ x = Int.unsigned index) by omega.
Caseeq LessOrEqual.
{
intros.
apply lt_n_not_free.
omega. }
{
intros.
subst x.
apply (palloc_index_invalid_norm _) in H3.
assumption. } }
{
intro.
generalize (get_at_u_valid index H3).
intro get_at_u_case.
Caseeq get_at_u_case.
{
intro.
assert(n = index).
{ apply palloc_index_unique.
unfold palloc_index_valid.
split.
eauto.
eauto.
apply get_and_norm; eauto.
intros.
omega.
omega. }
subst.
esplit. esplit.
change 0 with (Int.unsigned Int.zero) in H4.
change 1 with (Int.unsigned Int.one) in H3.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
left.
rewrite PTree.gso; repeat vcgen. }
{
intro.
esplit. esplit.
change 1 with (Int.unsigned Int.one) in H3, H4.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
repeat vcgen.
{ assert(Int.unsigned index ≠ Int.unsigned n).
{ intro equal.
rewrite <- equal in tmpn2.
apply (palloc_index_invalid_atget _) in H4.
contradiction. }
omega. }
{ assert(LessOrEqual: 0< x< Int.unsigned index ∨ x = Int.unsigned index) by omega.
Caseeq LessOrEqual.
{
intros.
apply leind.
assumption. }
{
intros.
subst x.
apply (palloc_index_invalid_atget _) in H4.
assumption. } } } } }
{
intros.
esplit. esplit.
repeat vcgen.
assert(normcase: is_at_norm_spec (Int.unsigned index) adt = Some 0 ∨
is_at_norm_spec (Int.unsigned index) adt = Some 1).
apply permission_norm.
omega.
Caseeq normcase.
{
intro.
esplit. esplit.
change 0 with (Int.unsigned Int.zero) in H4.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
left.
rewrite PTree.gso; repeat vcgen.
rewrite <- H2 in freeind.
rewrite Int.repr_unsigned in freeind.
assumption. }
{
intro.
generalize (get_at_u_valid index H4).
intro get_at_u_case.
Caseeq get_at_u_case.
{
intro.
unfold is_at_norm_spec in H4.
rewrite ikern, ihost in H4.
unfold get_at_u_spec in H5.
rewrite ikern, ihost in H5.
unfold AuxFunctions.zle_lt in ×.
rewrite lock_st in ×.
repeat zdestruct.
case_eq (ZMap.get (Int.unsigned index) (AT adt)); intros.
{ rewrite H6 in H4, H5.
destruct b.
{ destruct (ZMap.get lock_AT_start (lock adt)); contra_inv. }
{ destruct (ATType_dec t ATNorm).
{ subst.
assert(0 < Int.unsigned index < Int.unsigned n) by omega.
generalize (lt_n_not_free (Int.unsigned index) H7); intro.
contradiction. }
{ destruct (ZMap.get lock_AT_start (lock adt)); contra_inv. } } }
{ destruct (ZMap.get lock_AT_start (lock adt)); contra_inv.
rewrite H6 in H4; discriminate H4. } }
{
intros.
esplit. esplit.
replace 1 with (Int.unsigned Int.one) in H4, H5; try reflexivity.
repeat vcgen.
∃ (nps - Int.unsigned index - 1).
repeat vcgen.
esplit.
repeat vcgen.
left.
rewrite PTree.gso; repeat vcgen.
rewrite <- H2 in freeind.
rewrite Int.repr_unsigned in freeind.
assumption. } } }
+
intros.
Caseeq n_property.
×
intro tmpH.
destruct tmpH as [nrange zget].
esplit. esplit.
repeat vcgen.
destruct casefreeindex.
eassumption.
destruct H2.
destruct H3.
omega.
discharge_cmp.
discharge_cmp.
discharge_cmp.
destruct casefreeindex.
assumption.
destruct H3.
destruct H4.
rewrite H3.
f_equal.
f_equal.
omega.
discriminate H2.
×
intro nval.
esplit. esplit.
repeat vcgen.
destruct casefreeindex.
eassumption.
destruct H2.
destruct H3.
rewrite <- nval in H2.
rewrite Int.repr_unsigned in H2.
assumption.
discharge_cmp.
discharge_cmp.
discharge_cmp.
destruct casefreeindex.
assumption.
destruct H3.
destruct H4.
rewrite H3.
f_equal.
f_equal.
rewrite <- nval.
rewrite Int.repr_unsigned.
reflexivity.
discriminate H2.
Qed.
End Palloc_loop_proof.
Lemma palloc_loop_correct: ∀ m d le n,
high_level_invariant d →
init d = true →
ikern d = true →
ihost d = true →
(0 < Int.unsigned n < nps d ∧ ZMap.get (Int.unsigned n) (AT d) =
ATValid false ATNorm ∨
Int.unsigned n = nps d) →
(∀ x: Z, ((0 < x < Int.unsigned n)%Z →
ZMap.get x (AT d) ≠ ATValid false ATNorm)) →
PTree.get tnps le = Some (Vint (Int.repr(nps d))) →
PTree.get tpalloc_index le = Some (Vint (Int.repr 1)) →
PTree.get tpalloc_free_index le = Some (Vint (Int.repr(nps d))) →
PTree.get tid le = Some (Vint conid) →
ZMap.get lock_AT_start (lock d) = LockOwn true →
∃ le´, exec_stmt ge (PTree.empty _) le ((m, d) : mem)
(Swhile palloc_while_condition palloc_while_body)
E0 le´ (m, d) Out_normal ∧
PTree.get tpalloc_free_index le´= Some (Vint n) ∧
PTree.get tnps le´ = Some (Vint (Int.repr (nps d))) ∧
PTree.get tid le´ = Some (Vint conid).
Proof.
intros m d le n inv init kern host nrange indvalid letnps leindex lefreeindex ltid lock_st.
generalize (palloc_loop_correct_aux m d n inv nrange indvalid init kern host lock_st).
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´ pre].
destruct pre as [m´ pre].
destruct pre as [pre1 pre2].
∃ le´.
unfold palloc_loop_body_Q in pre2.
destruct pre2 as (tpalloc_free_index_v & tnps_val & tid_val & lock_cond & m´_val).
subst.
auto.
unfold palloc_loop_body_P.
tauto.
Qed.
Lemma acquire_lock_AT_prop:
∀ d d´,
acquire_lock_AT_spec (d: RData) = Some (d´: RData) →
nps d´ = nps d ∧ init d´ = init d ∧ ikern d´ = ikern d ∧ ihost d´ = ihost d ∧ AC d´ = AC d ∧
ATC d´ = ATC d.
Proof.
intros. unfold acquire_lock_AT_spec in H.
subdestruct; inv H; simpl; refine_split´; eauto.
Qed.
Lemma acquire_lock_AT_ownership:
∀ d d´,
acquire_lock_AT_spec (d: RData) = Some (d´: RData) →
(ZMap.get 0 (lock d)) ≠ LockOwn true ∧
(ZMap.get 0 (lock d´)) = LockOwn true.
Proof.
intros.
unfold acquire_lock_AT_spec in H.
subdestruct; inv H; simpl; rewrite ZMap.gss; split; eauto; intro HF; inv HF.
Qed.
Lemma get_nps_valid: ∀ (m:mem) (d:RData),
high_level_invariant d →
init d = true →
ikern d = true →
ihost d = true →
get_nps_spec d = Some (Int.unsigned (Int.repr (nps d))).
Proof.
intros.
inv H.
simpl in ×.
generalize (valid_nps H0); intro nps_range.
unfold get_nps_spec.
simpl.
rewrite H1, H2.
f_equal.
rewrite Int.unsigned_repr.
trivial.
generalize max_unsigned_val.
omega.
Qed.
Lemma palloc_body_correct: ∀ m d d´ env le index,
env = PTree.empty _ →
PTree.get tid le = Some (Vint conid) →
palloc_spec (Int.unsigned conid) d = Some (d´, Int.unsigned index) →
high_level_invariant d →
kernel_mode d →
init d = true →
∃ le´,
(exec_stmt ge env le ((m, d): mem) palloc_body E0 le´ (m, d´)
(Out_return (Some (Vint index, tint)))).
Proof.
generalize max_unsigned_val; intro muval.
generalize get_nps_valid; intro npsvalid.
intros m d d´ env le index emp_env argu pspec hinv km iinit.
functional inversion pspec; subst.
destruct km as (iikern & iihost).
subst.
unfold palloc_body.
simpl in H2.
remember H2 as pspec_aux; clear Heqpspec_aux.
unfold palloc_aux_spec in pspec_aux.
set (ZMap.get (Int.unsigned conid) (AC adt´)) as c.
fold c in pspec_aux.
set ({| cquota := cquota c;
cusage := cusage c + 1;
cparent := cparent c;
cchildren := cchildren c;
cused := cused c |}) as cur.
fold cur in pspec_aux.
case_eq (ikern adt´); intros iikern_adt´; rewrite iikern_adt´ in pspec_aux; try (inv pspec_aux; fail).
case_eq (init adt´); intros iinit_adt´; rewrite iinit_adt´ in pspec_aux; try (inv pspec_aux; fail).
case_eq (ihost adt´); intros iihost_adt´; rewrite iihost_adt´ in pspec_aux; try (inv pspec_aux; fail).
case_eq (cused c); intros cused_get; rewrite cused_get in pspec_aux;
try (inv pspec_aux; fail).
case_eq (cusage c <? cquota c); intros cusage_cquota; rewrite cusage_cquota in pspec_aux.
{ remember (first_free (AT adt´) (nps adt´)) as H.
subdestruct; subst.
inv pspec_aux.
-
destruct a.
destruct a0.
assert (Heq: nps adt´ = nps d ∧ init adt´ = init d ∧ ikern adt´ = ikern d ∧
ihost adt´ = ihost d ∧ AC adt´ = AC d ∧ ATC adt´ = ATC d).
{ eapply acquire_lock_AT_prop; eauto. }
destruct Heq as (Hnps & Hinit & Hik & Hih & HAC & HATC).
remember H1 as H15.
clear HeqH15.
apply acquire_lock_AT_ownership in H15.
destruct H15 as (lock_bf & lock_af).
edestruct palloc_loop_correct with (m := m)
(le :=
PTree.set tpalloc_free_index (Vint (Int.repr (nps adt´)))
(PTree.set tpalloc_index (Vint (Int.repr 1))
(PTree.set tnps (Vint (Int.repr (nps adt´)))
le))).
{ eapply acquire_lock_AT_high_level_inv; eauto. }
{ congruence. }
{ congruence. }
{ congruence. }
{ left.
split.
eassumption.
assumption. }
{ intros.
unfold not in ×.
intro.
eapply n0.
eassumption.
eassumption. }
{ d3 vcgen. }
{ d3 vcgen. }
{ d3 vcgen. }
{ d5 vcgen. }
{ assumption. }
{ destruct H.
destruct H0.
generalize (nps_range _ hinv iinit); intro.
destruct H4.
esplit.
rewrite Hnps in H.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
{
unfold get_nps_spec.
subrewrite´.
rewrite Int.unsigned_repr; try omega.
reflexivity. omega. }
symmetry in HeqH.
d3 vcgen.
repeat vcgen.
d3 vcgen.
vcgen.
repeat vcgen.
{
unfold container_alloc_spec.
unfold c in cused_get, cusage_cquota.
subrewrite´.
instantiate (1 := Int.one).
reflexivity. }
{ reflexivity. }
change (Int.eq Int.zero Int.zero) with true; simpl.
repeat vcgen.
{
unfold set_at_u_spec; simpl.
subrewrite´.
unfold zle_lt.
repeat zdestruct. }
{
unfold set_at_c_spec; simpl.
subrewrite´.
rewrite zle_lt_true; try omega.
unfold lock_AT_start.
subrewrite´. }
{ repeat vcgen.
remember H1 as ac_lock_spec.
clear Heqac_lock_spec.
unfold acquire_lock_AT_spec in ac_lock_spec.
subdestruct.
- inversion ac_lock_spec.
unfold release_lock_AT_spec; simpl.
unfold cur in H3.
unfold c in H3.
subrewrite´.
rewrite ZMap.gss.
rewrite ZMap.gss.
functional inversion H3.
unfold l´ in H13.
simpl in ×.
inversion ac_lock_spec; substx; simpl in ×.
rewrite ZMap.gss in H11.
inversion H11; substx; simpl in ×.
rewrite H13.
simpl.
repeat rewrite ZMap.set2.
rewrite cused_get.
reflexivity.
- inversion ac_lock_spec.
unfold release_lock_AT_spec; simpl.
unfold cur in H3.
unfold c in H3.
subrewrite´.
rewrite ZMap.gss.
rewrite ZMap.gss.
functional inversion H3.
unfold l´ in H13.
simpl in ×.
inversion ac_lock_spec; substx; simpl in ×.
rewrite ZMap.gss in H11.
inversion H11; substx; simpl in ×.
rewrite H13.
simpl.
repeat rewrite ZMap.set2.
rewrite cused_get.
reflexivity. } }
-
inversion pspec_aux. substx.
destruct (first_free (AT adt0) (nps adt0)).
+ inv HeqH.
+ generalize (nps_range d hinv iinit); intro.
assert (Heq: nps adt0 = nps d ∧ init adt0 = init d ∧ ikern adt0 = ikern d ∧
ihost adt0 = ihost d ∧ AC adt0 = AC d ∧ ATC adt0 = ATC d).
{ eapply acquire_lock_AT_prop; eauto. }
destruct Heq as (Hnps & Hinit & Hik & Hih & HAC & HATC).
edestruct palloc_loop_correct.
{ eapply acquire_lock_AT_high_level_inv; eauto. }
{ congruence. }
{ congruence. }
{ congruence. }
{ right.
rewrite Hnps.
erewrite <- nps_representable; eauto. }
{ intros.
unfold not in ×.
intro.
erewrite nps_representable in ×.
eapply n; eauto. rewrite Hnps.
assumption.
assumption.
congruence. }
{ instantiate
(1 :=
PTree.set tpalloc_free_index (Vint (Int.repr (nps adt0)))
(PTree.set tpalloc_index (Vint (Int.repr 1))
(PTree.set tnps (Vint (Int.repr (nps adt0)))
le))).
repeat vcgen. }
{ repeat vcgen. }
{ repeat vcgen. }
{ repeat vcgen. }
{ destruct acquire_lock_AT_ownership with (1:= H1); unfold lock_AT_start; auto. }
{ destruct H0.
destruct H5.
destruct H6.
esplit.
rewrite <-(Int.repr_unsigned index).
rewrite <- H4.
repeat vcgen.
{
unfold get_nps_spec; simpl.
subrewrite´.
erewrite <- nps_representable; eauto.
rewrite Int.unsigned_repr; try (rewrite Int.unsigned_repr); try (rewrite muval); try (omega; fail).
reflexivity. }
}
}
{
remember (first_free (AT adt´) (nps adt´)) as H.
subdestruct; subst.
inversion pspec_aux; substx.
assert (Heq: nps adt0 = nps d ∧ init adt0 = init d ∧ ikern adt0 = ikern d
∧ ihost adt0 = ihost d ∧ AC adt0 = AC d ∧ ATC adt0 = ATC d).
{ eapply acquire_lock_AT_prop; eauto. }
destruct Heq as (Hnps & Hinit & Hik & Hih & HAC).
destruct (first_free (AT adt0) (nps adt0)).
+
destruct s as (n & n_range & ATn & n_first_free).
assert (n_unsigned : Int.unsigned (Int.repr n) = n).
{ apply Int.unsigned_repr.
pose proof (nps_range _ hinv iinit).
omega. }
edestruct palloc_loop_correct.
{ eapply acquire_lock_AT_high_level_inv; eauto. }
{ congruence. }
{ congruence. }
{ congruence. }
{ left.
split.
rewrite <- n_unsigned in n_range; eassumption.
rewrite n_unsigned; assumption. }
{ intros.
unfold not in ×.
intro.
eapply n_first_free.
rewrite <- n_unsigned; eassumption.
eassumption. }
{ instantiate
(1:=
PTree.set tpalloc_free_index (Vint (Int.repr (nps adt0)))
(PTree.set tpalloc_index (Vint (Int.repr 1))
(PTree.set tnps (Vint (Int.repr (nps adt0)))
le))).
repeat vcgen. }
{ repeat vcgen. }
{ repeat vcgen. }
{ repeat vcgen. }
{ destruct acquire_lock_AT_ownership with (1:= H1); assumption. }
{ destruct H.
destruct H0.
destruct H5.
generalize (nps_range _ hinv iinit); intro.
esplit.
rewrite H4.
repeat vcgen.
{
unfold get_nps_spec.
subrewrite´.
rewrite Int.unsigned_repr; try omega.
reflexivity. } }
+
generalize (nps_range d hinv iinit); intro.
edestruct palloc_loop_correct.
{ eapply acquire_lock_AT_high_level_inv; eauto. }
{ congruence. }
{ congruence. }
{ congruence. }
{ right.
erewrite <- nps_representable; eauto.
eapply acquire_lock_AT_high_level_inv; eauto. }
{ intros.
unfold not in ×.
intro.
erewrite nps_representable in ×.
eapply n; eauto.
eapply acquire_lock_AT_high_level_inv; eauto.
congruence. }
{ instantiate
(1 :=
PTree.set tpalloc_free_index (Vint (Int.repr (nps adt0)))
(PTree.set tpalloc_index (Vint (Int.repr 1))
(PTree.set tnps (Vint (Int.repr (nps adt0)))
le))).
repeat vcgen. }
{ repeat vcgen. }
{ repeat vcgen. }
{ repeat vcgen. }
{ destruct acquire_lock_AT_ownership with (1:= H1); assumption. }
{ destruct H0.
destruct H5.
destruct H6.
esplit.
d3 vcgen.
repeat vcgen.
rewrite <- (Int.repr_unsigned index).
rewrite <- H4.
repeat vcgen.
{
unfold get_nps_spec.
subrewrite´.
rewrite Int.unsigned_repr; try omega.
reflexivity. } } }
Qed.
End PallocBody.
Theorem palloc_code_correct:
spec_le (palloc ↦ palloc_spec_low) (〚palloc ↦ f_palloc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´. idtac.
fbigsteptest
(palloc_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp
b6 Hb6fs Hb6fp
b5 Hb5fs Hb5fp
b7 Hb7fs Hb7fp
i m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_palloc)
(Vint i::nil)
(create_undef_temps (fn_temps f_palloc)))) H0.
- functional inversion H. subst.
assert (Heq: nps adt´ = nps labd ∧ init adt´ = init labd ∧ ikern adt´ = ikern labd ∧
ihost adt´ = ihost labd ∧ AC adt´ = AC labd ∧ ATC adt´ = ATC labd).
{ eapply acquire_lock_AT_prop; eauto. }
destruct Heq as (_ & Heq & _ & _).
rewrite <- Heq.
unfold palloc_aux_spec in H6.
case_eq (ikern adt´); intros iikern_adt´; rewrite iikern_adt´ in H6; try (inv H6; fail).
case_eq (init adt´); intros iinit_adt´; rewrite iinit_adt´ in H6; try (inv H6; fail).
reflexivity.
- functional inversion H; auto.
intros ev; destruct ev; repeat fbigstep_post.
Qed.
End PAlloc.
End With_primitives.
End MALOPCODE.