Library mcertikos.multithread.lowrefins.E2PBThreadGenLemmaSCHEDINIT
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem3.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import I64Layer.
Require Import AlgebraicMem.
Require Import Decision.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import PHBThread.
Require Import AsmE2L.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import E2PBThreadComposeData.
Require Import LoadStoreSemPHB.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadINTELVIRT.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadReplayFunction.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadVMM.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjInterruptController.
Require Import ObjSerialDevice.
Require Import OracleInstances.
Require Import ObjVMMFun.
Require Import ObjVMMGetSet.
Require Import ObjVMMDef.
Require Import ObjCV.
Require Import ObjCPU.
Require Import ObjVMX.
Require Import ObjVMCS.
Require Import ObjProc.
Require Import ObjBigThread.
Require Import ObjContainer.
Require Import ObjMultiprocessor.
Require Import ObjThread.
Require Import BigLogThreadConfigFunction.
Require Import BigLogThreadConfigFunctionProp.
Require Import StencilImpl.
Require Import E2PBThreadGenDef.
Section E2PBTHREADGENLEMMASCHEDINIT.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := SingleOracleImpl.s_oracle_prf.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_prop_prf : SingleOracleProp := SingleOracleImpl.s_oracle_prop_prf.
Context `{Hstencil : Stencil (stencil := stencil)}.
Local Instance s_config : SingleConfiguration mem := s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_link_prop_prf : SingleOracleLinkProp := SingleOracleImpl.s_oracle_link_prop_prf.
Local Instance s_link_config : SingleLinkConfiguration mem := s_link_config.
Context `{acc_def: !AccessorsDefined (mem := mem) (stencil := stencil) (stencil_ops := stencil_ops)
(memory_model_ops := memory_model_ops)
(phbthread (s_config := s_config) ⊕ L64)}.
Opaque PDX Zdivide_dec zle Z.mul Z.add Z.sub Z.div.
Opaque CalRealPT.real_pt CalRealProcModule.real_syncchpool.
Opaque compatlayer_ops.
Opaque update.
Opaque uRData.
Opaque proc_id.
Opaque full_thread_list.
Lemma sched_init_related:
∀ kctxt_pool l dp a n d d´ ds´ choice optSync l´,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
ObjPHBThreadSCHED.single_big_sched_init_spec (Int.unsigned n) (uRData l, d) = Some (ds´, d´) →
choice_check sched_init (Lint n :: nil) (uRData l) d = choice →
sync_chpool_check sched_init (Lint n :: nil) (uRData l) d = optSync →
l´ = LEvent (proc_id (uRData l)) (LogPrim sched_init (Lint n :: nil) choice (snap_func d)) :: l →
val2Lval_list (Vint n :: nil) (Lint n :: nil) →
∃ (a´ : RData),
big_sched_init_spec (Int.unsigned n) a = Some a´ ∧
relate_RData kctxt_pool (uRData l´) (ZMap.set (proc_id (uRData l)) (Some d´) dp) a´ ∧
kctxt a = kctxt a´ ∧ ds´ = uRData l´.
Proof.
assert (in_event: has_event sched_init = true) by (unfold has_event; auto).
assert (prim_num: prim_id_num sched_init = 5) by (unfold prim_id_num; simpl; auto).
intros.
assert (valid_procid: proc_id (uRData l) = main_thread ∨ TOTAL_CPU < proc_id (uRData l) < num_proc).
{ generalize (all_cid_in_full_thread_list l); intros.
generalize (valid_thread_list (proc_id (uRData l))); intros.
eapply H7 in H6.
tauto. }
unfold choice_check in H2.
unfold sync_chpool_check in H3; simpl in ×.
Transparent uRData proc_id update.
functional inversion H1.
rewrite prim_num in H2; subst.
generalize (per_data_re _ _ _ _ H (proc_id (uRData l))); intros Hper_data_rel.
simpl in Hper_data_rel; simpl in H0; rewrite H0 in Hper_data_rel.
simpl in ×.
rewrite prim_num.
unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share.
functional inversion H14.
unfold big_sched_init_spec.
inv Hper_data_rel; rewrite zeq_true in ×.
rewrite <- init_re, <- pg_re, <- ikern_re, <- ihost_re, <- ipt_re, <- in_intr_re.
rewrite H6, H7, H9, H11, H12, H13; subst.
generalize dev_handling_cid_constraint; intros Hdevid; simpl.
rewrite Hdevid in ×.
rewrite _x in ×.
rewrite zeq_true in *; auto.
rewrite <- ioapic_re, <- lapic_re.
unfold pv_adt in H15, H16.
rewrite H15, H16.
rewrite H4.
esplit; split; simpl; auto.
split; simpl; auto.
- inv H.
{
constructor.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; rewrite lock_re; auto.
+ simpl; rewrite CPU_ID_re; auto.
+ simpl.
rewrite CPU_ID_re.
assert (Hinj: Z.to_nat (8 - 1) = 7%nat).
{ replace (8 - 1) with 7 by ring.
simpl.
simpl.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
ring. }
assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; auto. }
assert (Hmain_thread_range : 1 ≤ AbstractDataType.CPU_ID a + 1 < 9) by omega.
assert (Hinitcid: (ZMap.get (AbstractDataType.CPU_ID a) (CalRealProcModule.real_cidpool (AbstractDataType.cid a)))
= (AbstractDataType.CPU_ID a) + 1).
{ unfold CalRealProcModule.real_cidpool.
rewrite Hinj.
simpl.
assert (CPU_ID_val: AbstractDataType.CPU_ID a = 0 ∨ AbstractDataType.CPU_ID a = 1 ∨ AbstractDataType.CPU_ID a = 2 ∨
AbstractDataType.CPU_ID a = 3 ∨ AbstractDataType.CPU_ID a = 4 ∨ AbstractDataType.CPU_ID a = 5 ∨
AbstractDataType.CPU_ID a = 6 ∨ AbstractDataType.CPU_ID a = 7).
{ revert HCPU_ID_range; clear; intros; omega. }
destruct CPU_ID_val as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
- rewrite i00.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i01.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i02.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i03.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i04.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i05.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i06.
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i07.
rewrite ZMap.gss; auto.
}
rewrite ZMap.gss.
rewrite Hinitcid.
rewrite main_thread_val.
rewrite <- (CPU_ID_valid l).
simpl.
rewrite CPU_ID_re; auto.
+ simpl; rewrite idpde_re; reflexivity.
+ simpl; reflexivity.
+ simpl; reflexivity.
+ simpl; rewrite <- big_oracle_re; auto.
+ intros.
generalize (per_data_re i); intros; simpl.
case_eq (zeq i main_thread); intros; subst.
× rewrite ZMap.gss.
rewrite <- _x.
rewrite <- _x in H.
rewrite <- _x in H0.
rewrite H0 in H.
inv H; simpl.
{
constructor.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; rewrite lock_re; auto.
+ simpl; rewrite CPU_ID_re; auto.
+ rewrite CPU_ID_re.
assert (Hinj: Z.to_nat (8 - 1) = 7%nat).
{ replace (8 - 1) with 7 by ring.
simpl.
simpl.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
ring. }
assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; auto. }
assert (Hmain_thread_range : 1 ≤ AbstractDataType.CPU_ID a + 1 < 9) by omega.
assert (Hinitcid: (ZMap.get (AbstractDataType.CPU_ID a) (CalRealProcModule.real_cidpool (AbstractDataType.cid a)))
= (AbstractDataType.CPU_ID a) + 1).
{ unfold CalRealProcModule.real_cidpool.
rewrite Hinj.
simpl.
assert (CPU_ID_val: AbstractDataType.CPU_ID a = 0 ∨ AbstractDataType.CPU_ID a = 1 ∨
AbstractDataType.CPU_ID a = 2 ∨
AbstractDataType.CPU_ID a = 3 ∨ AbstractDataType.CPU_ID a = 4 ∨
AbstractDataType.CPU_ID a = 5 ∨
AbstractDataType.CPU_ID a = 6 ∨ AbstractDataType.CPU_ID a = 7).
{ revert HCPU_ID_range; clear; intros; omega. }
destruct CPU_ID_val as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
- rewrite i00.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i01.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i02.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i03.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i04.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i05.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i06.
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i07.
rewrite ZMap.gss; auto.
}
simpl.
rewrite <- CPU_ID_re.
rewrite ZMap.gss.
rewrite _x.
rewrite CPU_ID_re.
rewrite Hinitcid.
rewrite main_thread_val; auto.
rewrite <- (CPU_ID_valid l).
simpl.
rewrite CPU_ID_re.
auto.
+ simpl; rewrite idpde_re; reflexivity.
+ simpl; reflexivity.
+ simpl; reflexivity.
+ simpl; rewrite <- big_oracle_re; auto.
+ intros.
simpl; unfold pv_adt; auto.
+ simpl.
rewrite ZMap.gss.
rewrite zeq_true; auto.
+ simpl.
rewrite ZMap.gss.
rewrite zeq_true; auto.
+ simpl.
unfold relate_AC_per_pd in *; simpl.
unfold AC_init.
rewrite _x.
rewrite main_thread_val.
assert (main_thread_val: AbstractDataType.CPU_ID a + 1 = 1 ∨ AbstractDataType.CPU_ID a + 1 = 2 ∨
AbstractDataType.CPU_ID a + 1 = 3 ∨
AbstractDataType.CPU_ID a + 1 = 4 ∨ AbstractDataType.CPU_ID a + 1 = 5 ∨
AbstractDataType.CPU_ID a + 1 = 6 ∨
AbstractDataType.CPU_ID a + 1 = 7 ∨ AbstractDataType.CPU_ID a + 1 = 8).
{ assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; auto. }
assert (Hmain_thread_range : 1 ≤ AbstractDataType.CPU_ID a + 1 < 9) by omega.
omega. }
unfold init_real_container.
assert (Hinj: Z.to_nat (8 - 1) = 7%nat).
{ replace (8 - 1) with 7 by ring.
simpl.
simpl.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
ring. }
rewrite Hinj.
simpl.
rewrite <- (CPU_ID_valid l); simpl; rewrite CPU_ID_re.
destruct main_thread_val as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
{ rewrite i00.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i00.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i01.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i01.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i02.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i02.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i03.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i03.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i04.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i04.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i05.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i05.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i06.
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold B_GetContainerUsed.
rewrite i06.
rewrite zeq_true.
rewrite zeq_true.
unfold init_container; reflexivity. }
{ rewrite i07.
unfold B_GetContainerUsed.
rewrite i07.
rewrite zeq_true.
rewrite zeq_true.
rewrite ZMap.gss.
unfold init_container; reflexivity. }
+ simpl.
rewrite ZMap.gss.
rewrite zeq_true; auto.
+ simpl.
unfold pv_adt; auto.
+ simpl.
rewrite ZMap.gss.
rewrite zeq_true; auto.
+ simpl.
simpl in ptp_re0.
rewrite H7 in ptp_re0.
rewrite _x in ptp_re0; rewrite zeq_true in ptp_re0.
rewrite ptp_re0; auto.
+ simpl; rewrite ZMap.gss; rewrite zeq_true; auto.
+ simpl; rewrite ZMap.gss; rewrite zeq_true; auto.
+ simpl; rewrite ZMap.gss; rewrite zeq_true; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ simpl; rewrite Hdevid; rewrite _x; rewrite zeq_true; unfold pv_adt; auto.
+ unfold relate_SyncChanPool_per_pd; simpl.
unfold relate_SyncChanPool_per_pd in syncchpool_re0.
rewrite H7 in syncchpool_re0.
rewrite _x in syncchpool_re0.
rewrite zeq_true in syncchpool_re0.
rewrite syncchpool_re0.
reflexivity.
+ simpl.
unfold relate_uctxt_per_pd in *; simpl.
rewrite H7 in uctxt_re0.
rewrite _x in uctxt_re0.
rewrite zeq_true in uctxt_re0.
unfold pv_adt.
unfold AC_init.
rewrite _x.
rewrite main_thread_val; rewrite main_thread_val in uctxt_re0.
assert (main_thread_val: AbstractDataType.CPU_ID a + 1 = 1 ∨ AbstractDataType.CPU_ID a + 1 = 2 ∨
AbstractDataType.CPU_ID a + 1 = 3 ∨
AbstractDataType.CPU_ID a + 1 = 4 ∨ AbstractDataType.CPU_ID a + 1 = 5 ∨
AbstractDataType.CPU_ID a + 1 = 6 ∨
AbstractDataType.CPU_ID a + 1 = 7 ∨ AbstractDataType.CPU_ID a + 1 = 8).
{ assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; auto. }
assert (Hmain_thread_range : 1 ≤ AbstractDataType.CPU_ID a + 1 < 9) by omega.
omega. }
simpl.
rewrite <- (CPU_ID_valid l); simpl; rewrite CPU_ID_re.
rewrite <- (CPU_ID_valid l) in uctxt_re0; simpl in uctxt_re0; rewrite CPU_ID_re in uctxt_re0.
destruct main_thread_val as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
{ rewrite i00; rewrite i00 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i00.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i01; rewrite i01 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i01.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i02; rewrite i02 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i02.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i03; rewrite i03 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i03.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i04; rewrite i04 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i04.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i05; rewrite i05 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i05.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i06; rewrite i06 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i06.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
{ rewrite i07; rewrite i07 in uctxt_re0.
unfold B_GetContainerUsed.
rewrite i07.
rewrite zeq_true.
rewrite zeq_true.
unfold uctxt_bieq.
rewrite H7 in uctxt_re.
rewrite uctxt_re0.
inv sh_shared_inv_re.
rewrite H7 in init_uctxt_inv.
exploit init_uctxt_inv; auto.
intros.
rewrite H.
rewrite ZMap.gi.
rewrite ZMap.gi.
split.
intros.
rewrite ZMap.gi; auto.
∃ Vundef; auto. }
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ constructor.
simpl.
intros.
unfold pv_adt.
unfold pv_adt in H.
inv inv_re0.
auto.
}
× rewrite ZMap.gso; auto.
{
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; simpl; auto.
generalize H; intro Hrelate_reserve.
inv H; constructor.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; rewrite lock_re; auto.
+ simpl; rewrite CPU_ID_re; auto.
+ rewrite CPU_ID_re.
assert (Hinj: Z.to_nat (8 - 1) = 7%nat).
{ replace (8 - 1) with 7 by ring.
simpl.
simpl.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
ring. }
assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; auto. }
assert (Hmain_thread_range : 1 ≤ AbstractDataType.CPU_ID a + 1 < 9) by omega.
assert (Hinitcid: (ZMap.get (AbstractDataType.CPU_ID a) (CalRealProcModule.real_cidpool (AbstractDataType.cid a)))
= (AbstractDataType.CPU_ID a) + 1).
{ unfold CalRealProcModule.real_cidpool.
rewrite Hinj.
simpl.
assert (CPU_ID_val: AbstractDataType.CPU_ID a = 0 ∨ AbstractDataType.CPU_ID a = 1 ∨
AbstractDataType.CPU_ID a = 2 ∨
AbstractDataType.CPU_ID a = 3 ∨ AbstractDataType.CPU_ID a = 4 ∨
AbstractDataType.CPU_ID a = 5 ∨
AbstractDataType.CPU_ID a = 6 ∨ AbstractDataType.CPU_ID a = 7).
{ revert HCPU_ID_range; clear; intros; omega. }
destruct CPU_ID_val as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
- rewrite i00.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i01.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i02.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i03.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i04.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i05.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i06.
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss; auto.
- rewrite i07.
rewrite ZMap.gss; auto.
}
simpl.
rewrite <- CPU_ID_re.
rewrite ZMap.gss.
rewrite CPU_ID_re.
rewrite Hinitcid.
rewrite main_thread_val; auto.
rewrite <- (CPU_ID_valid l).
simpl.
rewrite CPU_ID_re.
auto.
+ simpl; rewrite idpde_re; reflexivity.
+ simpl; reflexivity.
+ simpl; reflexivity.
+ simpl; rewrite <- big_oracle_re; auto.
+ intros.
simpl; unfold pv_adt; auto.
+ simpl.
rewrite ZMap.gss; auto; rewrite <- _x.
rewrite zeq_false; auto; try (rewrite _x; auto).
simpl in ikern_re0; rewrite _x in ikern_re0; rewrite zeq_false in ikern_re0; auto; rewrite _x; auto.
+ simpl.
rewrite ZMap.gss; auto; rewrite <- _x.
rewrite zeq_false; auto; try (rewrite _x; auto).
simpl in ihost_re0; rewrite _x in ihost_re0; rewrite zeq_false in ihost_re0; auto; rewrite _x; auto.
+ simpl.
unfold relate_AC_per_pd in *; simpl.
rewrite H7 in AC_re.
rewrite zeq_false; auto.
rewrite H7 in AC_re0; auto.
rewrite zeq_false in AC_re0; auto.
unfold B_GetContainerUsed.
generalize (CPU_ID_valid l).
intros.
simpl in H.
rewrite H.
rewrite <- main_thread_val.
rewrite zeq_false; auto.
case_eq (zle_le 0 i 8); intros; auto.
+ simpl.
rewrite ZMap.gss.
rewrite zeq_false; auto.
rewrite zeq_false in ti_re0; auto.
simpl.
rewrite _x.
intros contra; elim n0; auto.
+ simpl; auto.
+ simpl.
rewrite ZMap.gss.
rewrite H7 in PT_re.
rewrite zeq_false in PT_re; auto.
rewrite zeq_false; auto.
+ simpl.
rewrite H7 in ptp_re.
rewrite zeq_false in ptp_re.
× rewrite ptp_re; auto.
× auto.
+ simpl.
rewrite ZMap.gss; auto.
simpl in ipt_re0.
rewrite _x in ipt_re0; rewrite zeq_false in ipt_re0; auto.
rewrite zeq_false; auto.
+ simpl.
rewrite ZMap.gss; auto.
simpl in intr_flag_re0.
rewrite _x in intr_flag_re0; rewrite zeq_false in intr_flag_re0; auto.
rewrite zeq_false; auto.
+ simpl.
rewrite ZMap.gss; auto.
simpl in in_intr_re0.
rewrite _x in in_intr_re0; rewrite zeq_false in in_intr_re0; auto.
rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ simpl; rewrite Hdevid; rewrite zeq_false; auto.
+ unfold relate_SyncChanPool_per_pd; simpl.
unfold relate_SyncChanPool_per_pd in syncchpool_re0.
rewrite H7 in syncchpool_re0.
rewrite zeq_false in syncchpool_re0.
rewrite syncchpool_re0.
× reflexivity.
× auto.
+ simpl.
unfold relate_uctxt_per_pd in *; simpl.
rewrite H7 in uctxt_re.
rewrite zeq_false; auto.
rewrite H7 in uctxt_re0; auto.
rewrite zeq_false in uctxt_re0; auto.
unfold B_GetContainerUsed.
generalize (CPU_ID_valid l).
intros.
simpl in H.
rewrite H.
rewrite <- main_thread_val.
rewrite zeq_false; auto.
case_eq (zle_le 0 i 8); intros; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ constructor; simpl.
inv inv_re0; auto.
+ constructor. }
+ inv sh_shared_inv_re.
constructor; simpl.
× intros.
eapply dirty_page_shared_inv in H; eauto.
× intros; inv H.
× intros; inv H.
× intros; inv H.
× intros.
apply init_big_log_inv in H7.
rewrite H7 in syncchpool_inv.
simpl in syncchpool_inv.
apply syncchpool_inv in H.
rewrite H.
reflexivity.
× intros.
apply valid_thread_list in H.
destruct H.
{ unfold B_GetContainerUsed.
assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H2; auto. }
rewrite CPU_ID_re.
rewrite zeq_false.
destruct (zle_le 0 tid 8).
{ omega. }
unfold AC_init.
unfold init_real_container.
assert (Hinj: Z.to_nat (8 - 1) = 7%nat).
{ replace (8 - 1) with 7 by ring.
simpl.
simpl.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
ring. }
rewrite Hinj.
simpl.
repeat (rewrite ZMap.gso; [ | intro contra; subst; try omega]); simpl.
rewrite ZMap.gi; auto.
intro contra.
subst.
omega. }
{ unfold B_GetContainerUsed.
subst.
unfold AC_init.
rewrite main_thread_val.
assert (main_thread_val: AbstractDataType.CPU_ID a + 1 = 1 ∨ AbstractDataType.CPU_ID a + 1 = 2 ∨
AbstractDataType.CPU_ID a + 1 = 3 ∨
AbstractDataType.CPU_ID a + 1 = 4 ∨ AbstractDataType.CPU_ID a + 1 = 5 ∨
AbstractDataType.CPU_ID a + 1 = 6 ∨
AbstractDataType.CPU_ID a + 1 = 7 ∨ AbstractDataType.CPU_ID a + 1 = 8).
{ assert (HCPU_ID_range : 0 ≤ AbstractDataType.CPU_ID a < TOTAL_CPU).
{ generalize current_CPU_ID_range.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; auto. }
assert (Hmain_thread_range : 1 ≤ AbstractDataType.CPU_ID a + 1 < 9) by omega.
omega. }
unfold init_real_container.
assert (Hinj: Z.to_nat (8 - 1) = 7%nat).
{ replace (8 - 1) with 7 by ring.
simpl.
simpl.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_xI.
rewrite Pos2Nat.inj_1.
ring. }
rewrite Hinj.
simpl.
rewrite <- (CPU_ID_valid l); simpl; rewrite CPU_ID_re.
rewrite zeq_true.
destruct main_thread_val as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
{ rewrite i00.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i01.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i02.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i03.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i04.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i05.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i06.
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
simpl; auto. }
{ rewrite i07.
unfold B_GetContainerUsed.
rewrite ZMap.gss.
simpl; auto. } }
× intros.
exploit init_uctxt_inv; eauto.
intros.
rewrite H2.
rewrite ZMap.gi; auto.
× unfold valid_AT_log_type_B.
intros; inv Hdef.
unfold valid_AT_log_B.
unfold B_CalAT_log_real.
simpl.
esplit; auto.
× unfold valid_TCB_log_type_B.
intros; inv Hdef.
unfold valid_TCB_log_B.
unfold B_CalTCB_log_real.
simpl.
esplit; auto.
× auto.
× intros.
rewrite H7 in init_pperm_inv.
exploit init_pperm_inv; auto.
intros.
rewrite H18 in H.
rewrite ZMap.gi in H.
elim H; reflexivity.
+ inv sh_mem_inv_re.
constructor; simpl; intros.
case_eq (zeq i main_thread); intros; subst.
{ rewrite ZMap.gss in H2; rewrite ZMap.gso in H17; auto; simpl in ×.
inv H2.
simpl in H18.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
case_eq (zeq j main_thread); intros; subst.
{ rewrite ZMap.gss in H17.
inv H17.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H17; auto.
apply (pperm_disjoint i j pd pd´ H H2 H17 j0 H18). } }
}
Qed.
End E2PBTHREADGENLEMMASCHEDINIT.