Library mcertikos.proc.ThreadSchedGenAsmData
This file provide the contextual refinement proof between MPTInit layer and MPTBit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import PCVOp.
Require Import ThreadSchedGenAsmSource.
Require Import AbstractDataType.
Section ASM_DATA.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := pcvintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Section GENERATE.
Lemma threadsched_generate:
∀ r´ (m0: mem) labd labd´ r´0,
thread_sched_spec labd ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
→ low_level_invariant (Mem.nextblock m0) labd
→ high_level_invariant labd
→ ∃ labd0 labd1 labd2 la,
dequeue0_spec (Int.unsigned (Int.repr ((rdy_q_id (CPU_ID labd))))) labd = Some (labd0, Int.unsigned la)
∧ set_state0_spec (Int.unsigned la) (Int.unsigned Int.one) labd0 = Some labd1
∧ get_curid_spec labd1 = Some (ZMap.get (CPU_ID labd1) (cid labd1))
∧ set_curid_spec (Int.unsigned la) labd1 = Some labd2
∧ kctxt_switch_spec
labd2 (ZMap.get (CPU_ID labd1) (cid labd1)) (Int.unsigned la)
((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
∧ (∀ v r, ZtoPreg v = Some r → Val.has_type (r´0 r) Tint)
∧ (∀ v r, ZtoPreg v = Some r → val_inject (Mem.flat_inj (Mem.nextblock m0))
(r´0 r) (r´0 r))
∧ ikern labd = true
∧ ihost labd = true
∧ ikern labd0 = true
∧ ihost labd0 = true
∧ ikern labd1 = true
∧ ihost labd1 = true
∧ ikern labd2 = true
∧ ihost labd2 = true
∧ 0≤ ZMap.get (CPU_ID labd1) (cid labd1) < num_proc.
Proof.
intros. inv H0.
rename H1 into Hhigh.
specialize (valid_TDQ _ Hhigh); intros HIP.
inv Hhigh.
assert (HOS: 0 ≤ rdy_q_id (CPU_ID labd) < num_chan).
{
unfold rdy_q_id. omega.
}
assert (HOS´: 0 ≤ rdy_q_id (CPU_ID labd) ≤ Int.max_unsigned).
{
rewrite_omega.
}
assert (HIK: ikern labd = true∧
ihost labd = true ∧
ipt labd = true∧
pg labd = true).
{
functional inversion H. auto.
}
destruct HIK as [HIK1 [HIH1 [HIPT1 HPE1]]].
unfold thread_sched_spec in ×.
unfold dequeue0_spec.
rewrite HIH1, HIPT1, HPE1, HIK1 in ×.
rewrite Int.unsigned_repr; try assumption.
unfold AbQCorrect_range in ×.
change (Int.unsigned (Int.repr 16337)) with 16337. simpl.
specialize (HIP refl_equal _ HOS).
unfold AbQCorrect in HIP.
subdestruct. inv H.
rewrite zle_lt_true; trivial.
destruct HIP as (l´ & Heq & Hrange). inv Heq.
specialize (Hrange z). exploit Hrange. left; trivial.
intros Hrange´.
assert (Heqz: Int.unsigned(Int.repr z) = z).
{
rewrite Int.unsigned_repr; trivial; rewrite_omega.
}
rewrite <- Heqz.
esplit; esplit; esplit; esplit.
split; trivial.
rewrite Heqz.
unfold set_state0_spec; simpl.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite ZMap.gss.
change (Int.unsigned Int.one) with 1. simpl.
split; trivial; simpl.
unfold get_curid_spec, set_curid_spec; simpl.
subrewrite´. split; trivial.
rewrite zle_lt_true; trivial.
split; trivial.
unfold kctxt_switch_spec; simpl.
subrewrite´.
rewrite zle_lt_true; [|omega].
rewrite zle_lt_true; trivial.
rewrite ZMap.set2.
refine_split´; trivial; try eapply kctxt_INJECT; eauto.
Qed.
End GENERATE.
Lemma Hdequeue:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_dequeue, Genv.find_symbol ge dequeue = Some b_dequeue
∧ Genv.find_funct_ptr ge b_dequeue =
Some (External (EF_external dequeue dequeue_sig)))
∧ get_layer_primitive dequeue pcvop = OK (Some (gensem dequeue0_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive dequeue pcvop = OK (Some (gensem dequeue0_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hget_curid:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_get_curid, Genv.find_symbol ge get_curid = Some b_get_curid
∧ Genv.find_funct_ptr ge b_get_curid =
Some (External (EF_external get_curid get_curid_sig)))
∧get_layer_primitive get_curid pcvop = OK (Some (gensem get_curid_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_curid pcvop = OK (Some (gensem get_curid_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hget_CPU_ID:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_get_CPU_ID, Genv.find_symbol ge get_CPU_ID = Some b_get_CPU_ID
∧ Genv.find_funct_ptr ge b_get_CPU_ID =
Some (External (EF_external get_CPU_ID get_CPU_ID_sig)))
∧get_layer_primitive get_CPU_ID pcvop = OK (Some (gensem get_CPU_ID_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_CPU_ID pcvop = OK (Some (gensem get_CPU_ID_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hset_curid:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_set_curid, Genv.find_symbol ge set_curid = Some b_set_curid
∧ Genv.find_funct_ptr ge b_set_curid =
Some (External (EF_external set_curid set_curid_sig)))
∧get_layer_primitive set_curid pcvop = OK (Some (gensem set_curid_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive set_curid pcvop = OK (Some (gensem set_curid_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hset_state:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_set_state, Genv.find_symbol ge set_state = Some b_set_state
∧ Genv.find_funct_ptr ge b_set_state =
Some (External (EF_external set_state set_state_sig)))
∧get_layer_primitive set_state pcvop = OK (Some (gensem set_state0_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive set_state pcvop = OK (Some (gensem set_state0_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hkctxt_switch:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_kctxt_switch, Genv.find_symbol ge kctxt_switch = Some b_kctxt_switch
∧ Genv.find_funct_ptr ge b_kctxt_switch =
Some (External (EF_external kctxt_switch null_signature)))
∧get_layer_primitive kctxt_switch pcvop = OK (Some (primcall_kctxt_switch_compatsem kctxt_switch_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive kctxt_switch pcvop = OK (Some (primcall_kctxt_switch_compatsem kctxt_switch_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hthread_sched:
∀ ge s b,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
find_symbol s thread_sched = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal threadsched_function).
Proof.
intros.
assert (Hmodule: get_module_function thread_sched (thread_sched ↦ threadsched_function) = OK (Some threadsched_function))
by apply get_module_function_mapsto.
assert (HInternal: make_internal threadsched_function = OK (AST.Internal threadsched_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
End WITHMEM.
End ASM_DATA.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import PCVOp.
Require Import ThreadSchedGenAsmSource.
Require Import AbstractDataType.
Section ASM_DATA.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := pcvintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Section GENERATE.
Lemma threadsched_generate:
∀ r´ (m0: mem) labd labd´ r´0,
thread_sched_spec labd ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
→ low_level_invariant (Mem.nextblock m0) labd
→ high_level_invariant labd
→ ∃ labd0 labd1 labd2 la,
dequeue0_spec (Int.unsigned (Int.repr ((rdy_q_id (CPU_ID labd))))) labd = Some (labd0, Int.unsigned la)
∧ set_state0_spec (Int.unsigned la) (Int.unsigned Int.one) labd0 = Some labd1
∧ get_curid_spec labd1 = Some (ZMap.get (CPU_ID labd1) (cid labd1))
∧ set_curid_spec (Int.unsigned la) labd1 = Some labd2
∧ kctxt_switch_spec
labd2 (ZMap.get (CPU_ID labd1) (cid labd1)) (Int.unsigned la)
((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
∧ (∀ v r, ZtoPreg v = Some r → Val.has_type (r´0 r) Tint)
∧ (∀ v r, ZtoPreg v = Some r → val_inject (Mem.flat_inj (Mem.nextblock m0))
(r´0 r) (r´0 r))
∧ ikern labd = true
∧ ihost labd = true
∧ ikern labd0 = true
∧ ihost labd0 = true
∧ ikern labd1 = true
∧ ihost labd1 = true
∧ ikern labd2 = true
∧ ihost labd2 = true
∧ 0≤ ZMap.get (CPU_ID labd1) (cid labd1) < num_proc.
Proof.
intros. inv H0.
rename H1 into Hhigh.
specialize (valid_TDQ _ Hhigh); intros HIP.
inv Hhigh.
assert (HOS: 0 ≤ rdy_q_id (CPU_ID labd) < num_chan).
{
unfold rdy_q_id. omega.
}
assert (HOS´: 0 ≤ rdy_q_id (CPU_ID labd) ≤ Int.max_unsigned).
{
rewrite_omega.
}
assert (HIK: ikern labd = true∧
ihost labd = true ∧
ipt labd = true∧
pg labd = true).
{
functional inversion H. auto.
}
destruct HIK as [HIK1 [HIH1 [HIPT1 HPE1]]].
unfold thread_sched_spec in ×.
unfold dequeue0_spec.
rewrite HIH1, HIPT1, HPE1, HIK1 in ×.
rewrite Int.unsigned_repr; try assumption.
unfold AbQCorrect_range in ×.
change (Int.unsigned (Int.repr 16337)) with 16337. simpl.
specialize (HIP refl_equal _ HOS).
unfold AbQCorrect in HIP.
subdestruct. inv H.
rewrite zle_lt_true; trivial.
destruct HIP as (l´ & Heq & Hrange). inv Heq.
specialize (Hrange z). exploit Hrange. left; trivial.
intros Hrange´.
assert (Heqz: Int.unsigned(Int.repr z) = z).
{
rewrite Int.unsigned_repr; trivial; rewrite_omega.
}
rewrite <- Heqz.
esplit; esplit; esplit; esplit.
split; trivial.
rewrite Heqz.
unfold set_state0_spec; simpl.
subrewrite´.
rewrite zle_lt_true; trivial.
rewrite ZMap.gss.
change (Int.unsigned Int.one) with 1. simpl.
split; trivial; simpl.
unfold get_curid_spec, set_curid_spec; simpl.
subrewrite´. split; trivial.
rewrite zle_lt_true; trivial.
split; trivial.
unfold kctxt_switch_spec; simpl.
subrewrite´.
rewrite zle_lt_true; [|omega].
rewrite zle_lt_true; trivial.
rewrite ZMap.set2.
refine_split´; trivial; try eapply kctxt_INJECT; eauto.
Qed.
End GENERATE.
Lemma Hdequeue:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_dequeue, Genv.find_symbol ge dequeue = Some b_dequeue
∧ Genv.find_funct_ptr ge b_dequeue =
Some (External (EF_external dequeue dequeue_sig)))
∧ get_layer_primitive dequeue pcvop = OK (Some (gensem dequeue0_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive dequeue pcvop = OK (Some (gensem dequeue0_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hget_curid:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_get_curid, Genv.find_symbol ge get_curid = Some b_get_curid
∧ Genv.find_funct_ptr ge b_get_curid =
Some (External (EF_external get_curid get_curid_sig)))
∧get_layer_primitive get_curid pcvop = OK (Some (gensem get_curid_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_curid pcvop = OK (Some (gensem get_curid_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hget_CPU_ID:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_get_CPU_ID, Genv.find_symbol ge get_CPU_ID = Some b_get_CPU_ID
∧ Genv.find_funct_ptr ge b_get_CPU_ID =
Some (External (EF_external get_CPU_ID get_CPU_ID_sig)))
∧get_layer_primitive get_CPU_ID pcvop = OK (Some (gensem get_CPU_ID_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_CPU_ID pcvop = OK (Some (gensem get_CPU_ID_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hset_curid:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_set_curid, Genv.find_symbol ge set_curid = Some b_set_curid
∧ Genv.find_funct_ptr ge b_set_curid =
Some (External (EF_external set_curid set_curid_sig)))
∧get_layer_primitive set_curid pcvop = OK (Some (gensem set_curid_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive set_curid pcvop = OK (Some (gensem set_curid_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hset_state:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_set_state, Genv.find_symbol ge set_state = Some b_set_state
∧ Genv.find_funct_ptr ge b_set_state =
Some (External (EF_external set_state set_state_sig)))
∧get_layer_primitive set_state pcvop = OK (Some (gensem set_state0_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive set_state pcvop = OK (Some (gensem set_state0_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hkctxt_switch:
∀ s ge,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
(∃ b_kctxt_switch, Genv.find_symbol ge kctxt_switch = Some b_kctxt_switch
∧ Genv.find_funct_ptr ge b_kctxt_switch =
Some (External (EF_external kctxt_switch null_signature)))
∧get_layer_primitive kctxt_switch pcvop = OK (Some (primcall_kctxt_switch_compatsem kctxt_switch_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive kctxt_switch pcvop = OK (Some (primcall_kctxt_switch_compatsem kctxt_switch_spec)))
by (unfold pcvop; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hthread_sched:
∀ ge s b,
make_globalenv s (thread_sched ↦ threadsched_function) pcvop = ret ge →
find_symbol s thread_sched = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal threadsched_function).
Proof.
intros.
assert (Hmodule: get_module_function thread_sched (thread_sched ↦ threadsched_function) = OK (Some threadsched_function))
by apply get_module_function_mapsto.
assert (HInternal: make_internal threadsched_function = OK (AST.Internal threadsched_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
End WITHMEM.
End ASM_DATA.