Library mcertikos.proc.PQueueIntroCodeTDQueueInit
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 LoopProof.
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 CLemmas.
Require Import TacticsForTesting.
Require Import CommonTactic.
Require Import CalRealProcModule.
Require Import AbstractDataType.
Require Import AuxStateDataType.
Require Import PQueueIntro.
Require Import PQueueIntroCSource.
Require Import QueueInitGenSpec.
Module PQUEUEINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_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}.
Section TDQUEUEINIT.
Let L: compatlayer (cdata RData) := shared_mem_init ↦ gensem sharedmem_init_spec
⊕ tcb_init ↦ gensem tcb_init_spec
⊕ tdq_init ↦ gensem tdq_init_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TDQueueInitBody.
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 LoopProof.
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 CLemmas.
Require Import TacticsForTesting.
Require Import CommonTactic.
Require Import CalRealProcModule.
Require Import AbstractDataType.
Require Import AuxStateDataType.
Require Import PQueueIntro.
Require Import PQueueIntroCSource.
Require Import QueueInitGenSpec.
Module PQUEUEINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_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}.
Section TDQUEUEINIT.
Let L: compatlayer (cdata RData) := shared_mem_init ↦ gensem sharedmem_init_spec
⊕ tcb_init ↦ gensem tcb_init_spec
⊕ tdq_init ↦ gensem tdq_init_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TDQueueInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
shared_mem_init
Variable bshared_mem_init: block.
Hypothesis hshared_mem_init1 : Genv.find_symbol ge shared_mem_init = Some bshared_mem_init.
Hypothesis hshared_mem_init2 : Genv.find_funct_ptr ge bshared_mem_init
= Some (External (EF_external shared_mem_init
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
tcb_init
Variable btcb_init: block.
Hypothesis htcb_init1 : Genv.find_symbol ge tcb_init = Some btcb_init.
Hypothesis htcb_init2 : Genv.find_funct_ptr ge btcb_init
= Some (External (EF_external tcb_init
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
tdq_init
Variable btdq_init: block.
Hypothesis htdq_init1 : Genv.find_symbol ge tdq_init = Some btdq_init.
Hypothesis htdq_init2 : Genv.find_funct_ptr ge btdq_init
= Some (External (EF_external tdq_init
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Definition tdqueue_init_fst_mk_rdata (adt: RData) (index: Z) :=
adt {tcb: init_zmap (index + 1) (TCBValid DEAD 0 num_proc num_proc) (tcb adt)}.
Section tdqueue_init_fst_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis pg: pg adt = true.
Hypothesis ipt: ipt adt = true.
Hypothesis ihost: ihost adt = true.
Hypothesis ikern: ikern adt = true.
Definition tdqueue_init_fst_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get ti le = Some (Vint Int.zero) ∧
m = (minit, adt).
Definition tdqueue_init_fst_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, tdqueue_init_fst_mk_rdata adt (num_proc - 1)).
Lemma tdqueue_init_fst_loop_correct_aux :
LoopProofSimpleWhile.t tdqueue_init_fst_while_condition
tdqueue_init_fst_while_body ge
(PTree.empty _) (tdqueue_init_fst_loop_body_P)
(tdqueue_init_fst_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get ti le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ num_proc ∧
(Int.unsigned i = 0 ∧
m = (minit, adt) ∨
Int.unsigned i > 0 ∧
m = (minit, tdqueue_init_fst_mk_rdata adt (Int.unsigned i - 1))) ∧
w = num_proc - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold tdqueue_init_fst_loop_body_P in H.
destruct H as [tile msubst].
subst.
change (Int.zero) with (Int.repr 0) in tile.
esplit. esplit.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [icase nval].
subst.
unfold tdqueue_init_fst_while_body.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
Caseeq ihigh.
+ Case "Int.unsigned i < num_proc".
intro ihigh.
Caseeq icase.
× SCase "Int.unsigned i = 0".
intro tmpH; destruct tmpH as [ival mval].
injection mval; intros; subst.
rewrite ival in ×.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
∃ (num_proc - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
unfold tdqueue_init_fst_mk_rdata.
rewrite ival.
unfold init_zmap.
simpl.
reflexivity.
× SCase "Int.unsigned i > 0".
intro tmpH; destruct tmpH as [ival mval].
injection mval; intros; subst.
unfold tdqueue_init_fst_mk_rdata.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold tcb_init_spec.
simpl.
rewrite pg, ikern, ihost, ipt.
rewrite zle_lt_true.
repeat zdestruct.
reflexivity.
omega.
∃ (num_proc - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
replace (Int.unsigned i + 1 - 1) with (Int.unsigned i - 1 + 1) by omega.
replace (Int.unsigned i - 1 + 1) with (Int.unsigned i) by omega.
rewrite init_zmap_eq by omega.
reflexivity.
+ Case "Int.unsigned i = num_proc".
intro ival.
rewrite ival.
esplit. esplit.
repeat vcgen.
unfold tdqueue_init_fst_loop_body_Q.
Caseeq icase; intro tmpH; destruct tmpH as [iv mval].
exfalso; rewrite iv in ival; omega.
rewrite ival in mval; assumption.
Qed.
End tdqueue_init_fst_loop_proof.
Lemma tdqueue_init_fst_loop_correct: ∀ m d d´ le,
PTree.get ti le = Some (Vint Int.zero) →
pg d = true →
ipt d = true →
ihost d = true →
ikern d = true →
d´ = tdqueue_init_fst_mk_rdata d (num_proc - 1) →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile tdqueue_init_fst_while_condition
tdqueue_init_fst_while_body) E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize (tdqueue_init_fst_loop_correct_aux m d H0 H1 H2 H3).
unfold tdqueue_init_fst_loop_body_P.
unfold tdqueue_init_fst_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp m´´val].
∃ le´´.
subst.
assumption.
auto.
Qed.
Definition tdqueue_init_snd_mk_rdata (adt: RData) (index: Z) :=
adt {tdq: init_zmap index (TDQValid num_proc num_proc) (tdq adt)}.
Section tdqueue_init_snd_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis pg: pg adt = true.
Hypothesis ipt: ipt adt = true.
Hypothesis ihost: ihost adt = true.
Hypothesis ikern: ikern adt = true.
Definition tdqueue_init_snd_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get ti le = Some (Vint (Int.repr 0)) ∧
m = (minit, adt).
Definition tdqueue_init_snd_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, tdqueue_init_snd_mk_rdata adt num_chan).
Lemma tdqueue_init_snd_loop_correct_aux :
LoopProofSimpleWhile.t tdqueue_init_snd_while_condition
tdqueue_init_snd_while_body ge (PTree.empty _) (tdqueue_init_snd_loop_body_P)
(tdqueue_init_snd_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get ti le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ num_chan ∧
(Int.unsigned i = 0 ∧ m = (minit, adt) ∨ Int.unsigned i > 0 ∧
m = (minit, tdqueue_init_snd_mk_rdata adt (Int.unsigned i))) ∧
w = num_chan + 1 - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold tdqueue_init_snd_loop_body_P in H.
destruct H as [tile msubst].
subst.
esplit. esplit.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [icase nval].
subst.
unfold tdqueue_init_snd_while_body.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
Caseeq ihigh.
+ Case "Int.unsigned i < num_chan".
intro ihigh.
Caseeq icase.
× SCase "Int.unsigned i = 0".
intro tmpH; destruct tmpH as [ival mval].
rewrite ival in ×.
injection mval; intros; subst.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
∃ (num_chan + 1 - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
unfold tdqueue_init_snd_mk_rdata.
rewrite ival.
reflexivity.
× SCase "Int.unsigned i > 0".
intro tmpH; destruct tmpH as [ival mval].
injection mval; intros; subst.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold tdqueue_init_snd_mk_rdata; simpl.
unfold tdq_init_spec; simpl.
rewrite ikern, ihost, pg, ipt.
rewrite zle_lt_true.
repeat zdestruct.
reflexivity.
omega.
∃ (num_chan + 1 - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
unfold tdqueue_init_snd_mk_rdata.
replace (Int.unsigned i - 1 + 1) with (Int.unsigned i) by omega.
replace (Int.unsigned i + 1 - 1 + 1) with (Int.unsigned i + 1) by omega.
rewrite init_zmap_eq by omega.
reflexivity.
+ Case "Int.unsigned i = num_chan + 1".
intro ival.
rewrite ival.
esplit. esplit.
repeat vcgen.
unfold tdqueue_init_snd_loop_body_Q.
Caseeq icase; intro tmpH; destruct tmpH as [iv mval].
exfalso; rewrite iv in ival; omega.
rewrite ival in mval. assumption.
Qed.
End tdqueue_init_snd_loop_proof.
Lemma tdqueue_init_snd_loop_correct: ∀ m d d´ le,
PTree.get ti le = Some (Vint (Int.repr 0)) →
pg d = true →
ipt d = true →
ihost d = true →
ikern d = true →
d´ = tdqueue_init_snd_mk_rdata d num_chan →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile tdqueue_init_snd_while_condition tdqueue_init_snd_while_body)
E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize (tdqueue_init_snd_loop_correct_aux m d H0 H1 H2 H3).
unfold tdqueue_init_snd_loop_body_P.
unfold tdqueue_init_snd_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp m´´val].
∃ le´´.
subst.
assumption.
auto.
Qed.
Require Import CalRealPT.
Require Import CalTicketLock.
Require Import CalRealIDPDE.
Require Import CalRealSMSPool.
Require Import DeviceStateDataType.
Lemma tdqueue_init_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get tmbi_adr le = Some (Vint mbi_adr) →
PTree.get ti le = Some Vundef →
tdqueue_init_spec (Int.unsigned mbi_adr) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) tdqueue_init_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
subst.
unfold tdqueue_init_body.
functional inversion H2; subst.
functional inversion H3; subst.
simpl in ×.
set (df :=
((((((((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)})
{ l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{CurrentIrq : None}}}) {vmxinfo : real_vmxinfo})
{pg : true}) {LAT : real_LAT (LAT d)}) {nps : real_nps})
{AC : AC_init}) {init : true}) {PT : 0}) {ptpool : real_pt (ptpool d)})
{multi_log : real_multi_log (multi_log d)}) {lock : real_lock (lock d)})
{idpde :real_idpde (idpde d)}) {smspool : real_smspool (smspool d)})
{tcb : real_tcb (tcb d)}) {tdq : real_tdq (tdq d)}).
set (dm :=
(((((((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)})
{ l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{CurrentIrq : None}}}) {vmxinfo : real_vmxinfo})
{pg : true}) {LAT : real_LAT (LAT d)}) {nps : real_nps})
{AC : AC_init}) {init : true}) {PT : 0}) {ptpool : real_pt (ptpool d)})
{multi_log : real_multi_log (multi_log d)}) {lock : real_lock (lock d)})
{idpde :real_idpde (idpde d)}) {smspool : real_smspool (smspool d)})
{tcb : real_tcb (tcb d)}).
set (di :=
((((((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)})
{ l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat
(IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{CurrentIrq : None}}}) {vmxinfo : real_vmxinfo})
{pg : true}) {LAT : real_LAT (LAT d)}) {nps : real_nps})
{AC : AC_init}) {init : true}) {PT : 0}) {ptpool : real_pt (ptpool d)})
{multi_log : real_multi_log (multi_log d)}) {lock : real_lock (lock d)})
{idpde :real_idpde (idpde d)}) {smspool : real_smspool (smspool d)}).
fold df in H2.
fold di in H3.
exploit (tdqueue_init_fst_loop_correct m di dm (PTree.set ti (Vint (Int.repr 0)) (set_opttemp None Vundef le)));
unfold di in *; simpl in *; try assumption.
- repeat vcgen.
- reflexivity.
- unfold tdqueue_init_fst_mk_rdata; simpl.
unfold dm.
reflexivity.
- intros tempH1.
destruct tempH1 as [le´ stmt´].
fold di in stmt´.
exploit (tdqueue_init_snd_loop_correct m dm df (PTree.set ti (Vint (Int.repr 0)) (set_opttemp None Vundef le´)));
unfold dm in *; simpl in *; try assumption.
+ repeat vcgen.
+ reflexivity.
+ unfold tdqueue_init_snd_mk_rdata.
unfold df; simpl.
unfold real_tdq.
reflexivity.
+ intros tempH2.
destruct tempH2 as [le´´ stmt´´].
fold df in stmt´´.
esplit.
unfold exec_stmt.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
fold di.
fold dm in stmt´, stmt´´.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
exact stmt´.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
exact stmt´´.
Qed.
End TDQueueInitBody.
Theorem tdqueue_init_code_correct:
spec_le (tdqueue_init ↦ tdqueue_init_spec_low) (〚tdqueue_init ↦ f_tdqueue_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (tdqueue_init_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_tdqueue_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_tdqueue_init)))) H0.
Qed.
End TDQUEUEINIT.
End WithPrimitives.
End PQUEUEINTROCODE.