Library mcertikos.multithread.highrefins.PHThread2TGenLemmaHASEVENT
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 LoadStoreSem3high.
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 AsmPHThread2T.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import PHThread2TComposeData.
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 ObjVMCS.
Require Import ObjVMX.
Require Import ObjEPT.
Require Import ObjBigThread.
Require Import BigLogThreadConfigFunction.
Require Import StencilImpl.
Require Import PHThread2TGenDef.
Opaque full_thread_list.
Section PHTHREAD2TGENLEMMAHASEVENT.
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 := 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 := SingleOracleImpl.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)}.
Lemma big_palloc_related_t:
∀ kctxt a a´ n res l pd,
relate_RData kctxt a l pd →
big2_palloc_spec (Int.unsigned n) a = Some (a´, res) →
∃ l´ pd´ res´,
single_big_palloc_spec (Int.unsigned n) (uRData l, pd) = Some ((uRData l´, pd´), res´) ∧
relate_RData kctxt a´ l´ pd´ ∧
proc_id (uRData l) = proc_id (uRData l´) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim palloc (Lint n::nil) (choice_check palloc (Lint n::nil) (uRData l) pd)
(snap_func pd))::l) ∧
res = res´.
Proof.
intros.
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H; rewrite <- CPU_ID_re in cid_re; auto. }
unfold big2_palloc_spec in H0.
subdestruct; inv H0; unfold single_big_palloc_spec; substx.
- inv H; simpl in *; rewritesb.
rewrite zeq_true.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; rewrite Hdestruct8.
simpl; rewrite Hdestruct5, Hdestruct9.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_false; [ | destruct a0; omega].
∃ ((LEvent (proc_id (uRData l)) (LogPrim palloc (Lint (Int.repr (proc_id (uRData l)))::nil) 1 (snap_func pd)))::l).
refine_split´; eauto.
+ simpl.
assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
reflexivity.
+ simpl.
assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
rewrite prim_num.
constructor; auto; simpl; try rewrite prim_num; simpl; try unfold single_big_palloc_spec_share;
try (rewritesb; rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11; rewrite zeq_true;
simpl; auto; fail).
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- pg_re; auto.
× rewritesb.
rewrite ZMap.gss; auto.
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- init_re; eauto.
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- CPU_ID_re.
rewrite <- cid_eq.
rewrite <- e; auto.
× rewrite <- e; auto.
× inv inv_re; constructor; simpl; auto.
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl; auto. }
+ assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- CPU_ID_re.
rewrite <- cid_eq.
rewrite e; reflexivity.
+ assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
simpl; unfold choice_check; rewrite prim_num.
unfold single_big_palloc_spec_test; simpl.
rewritesb.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; rewrite Hdestruct8.
simpl; rewrite Hdestruct9.
rewrite <- e.
rewrite Int.repr_unsigned; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; rewrite Hdestruct8.
simpl; rewrite Hdestruct9.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true.
∃ ((LEvent (proc_id (uRData l)) (LogPrim palloc (Lint (Int.repr (proc_id (uRData l)))::nil) 1 (snap_func pd)))::l).
refine_split´; eauto.
+ simpl.
assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11, Hdestruct5; reflexivity.
+ simpl.
assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
constructor; auto; simpl; try rewrite prim_num; simpl; try unfold single_big_palloc_spec_share;
try (rewritesb; rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11; rewrite zeq_true; simpl; auto; fail).
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- pg_re; auto.
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- init_re; auto.
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- CPU_ID_re.
rewrite e.
rewrite <- cid_eq; reflexivity.
× rewrite e; reflexivity.
× inv inv_re; constructor; simpl; auto.
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl; auto. }
+ assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8, Hdestruct10, Hdestruct11.
rewrite zeq_true; simpl.
rewrite <- CPU_ID_re.
rewrite <- cid_eq.
rewrite e; reflexivity.
+ assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
simpl; unfold choice_check; rewrite prim_num.
unfold single_big_palloc_spec_test; simpl.
rewritesb.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; rewrite Hdestruct8.
simpl; rewrite Hdestruct9.
rewrite <- e.
rewrite Int.repr_unsigned; auto.
- inv H; simpl in *; rewritesb.
rewrite zeq_true.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; rewrite Hdestruct8.
simpl; rewrite Hdestruct9, Hdestruct5.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
∃ ((LEvent (proc_id (uRData l)) (LogPrim palloc (Lint (Int.repr (proc_id (uRData l)))::nil) 0 (snap_func pd)))::l).
refine_split´; eauto.
+ simpl.
assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
rewrite prim_num.
unfold single_big_palloc_spec_share; simpl.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
reflexivity.
+ simpl.
assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
constructor; auto; simpl; try rewrite prim_num; simpl; try unfold single_big_palloc_spec_share;
try (rewritesb; rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8; rewrite zeq_false; [simpl; auto | rewrite prim_num; omega]; fail).
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_false; [ | rewrite prim_num; omega].
simpl; rewrite <- pg_re; auto.
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_false; eauto.
{ simpl; rewrite <- init_re; auto. }
{ intro contra.
rewrite prim_num in contra.
inv contra. }
× rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_false; eauto; [ | intros contra; inv contra].
rewrite e; simpl.
rewrite <- CPU_ID_re.
rewrite <- cid_eq; reflexivity.
× rewrite e; reflexivity.
× inv inv_re; constructor; simpl; auto.
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_false; [ | rewrite prim_num; omega].
simpl; auto. }
{ simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_false; [ | rewrite prim_num; omega].
simpl; auto. }
+ assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
simpl; rewrite prim_num; unfold single_big_palloc_spec_share.
rewritesb.
rewrite Hdestruct0, Hdestruct3, Hdestruct6, Hdestruct8.
rewrite zeq_false; [ | rewrite prim_num; omega].
rewrite e; simpl.
rewrite <- CPU_ID_re.
rewrite <- cid_eq; reflexivity.
+ assert (prim_num: prim_id_num palloc = 1).
{ unfold prim_id_num; simpl; auto. }
simpl; unfold choice_check; rewrite prim_num.
unfold single_big_palloc_spec_test; simpl.
rewritesb.
rewrite Hdestruct1, Hdestruct2, Hdestruct4, Hdestruct7.
rewrite e; rewrite Hdestruct8.
simpl; rewrite Hdestruct9.
rewrite <- e.
rewrite Int.repr_unsigned; auto.
Qed.
Lemma big_proc_create_related_t:
∀ b b´ b_uc uc_ofs q kctxt a pd a´ l new_id elf_id,
relate_RData kctxt a l pd →
big2_proc_create_spec a b b´ b_uc uc_ofs (Int.unsigned q) = Some (a´, new_id) →
∃ l´ pd´ new_id´,
single_big_proc_create_spec (uRData l, pd) b b´ b_uc uc_ofs (Int.unsigned q)
= Some ((uRData l´, pd´), new_id´) ∧
relate_RData kctxt a´ l´ pd´ ∧
(proc_id (uRData l´)) = (proc_id (uRData l)) ∧
l´ = (LEvent (proc_id (uRData l))
(LogPrim proc_create ((Lint elf_id)::(Lptr b_uc uc_ofs)::(Lint q)::nil)
(choice_check proc_create ((Lint elf_id)::(Lptr b_uc uc_ofs)::(Lint q)::nil) (uRData l) pd)
(snap_func pd))::l) ∧
new_id = new_id´ ∧
new_id = (choice_check proc_create ((Lint elf_id)::(Lptr b_uc uc_ofs)::(Lint q)::nil) (uRData l) pd).
Proof.
intros.
assert (prim_num: prim_id_num proc_create = 3).
{ unfold prim_id_num; simpl; eauto. }
unfold big2_proc_create_spec in H0.
subdestruct; inv H0; simpl in ×.
set (ch_id := (ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a))
× 8 + 1 + Z.of_nat (length (cchildren (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a)
(AbstractDataType.cid a)) (AbstractDataType.AC a))))).
∃ ((LEvent (proc_id (uRData l)) (LogPrim proc_create ((Lint elf_id)::(Lptr b_uc uc_ofs)::(Lint q)::nil) ch_id (snap_func pd)))::l).
refine_split´; auto.
- unfold single_big_proc_create_spec; simpl in ×.
rewrite prim_num.
unfold single_big_proc_create_spec_share; simpl in ×.
inv H; rewritesb.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3.
unfold ch_id.
unfold B_inLock; simpl.
rewrite Hdestruct9, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7, Hdestruct10, Hdestruct11, Hdestruct12.
case_eq (in_dec zeq (ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) × 8 + 1 +
Z.of_nat (length (cchildren (ZMap.get (ZMap.get (AbstractDataType.CPU_ID a)
(AbstractDataType.cid a))
(AbstractDataType.AC a))))) full_thread_list); intros;
[ | elim n; auto].
reflexivity.
- simpl; inv H.
constructor; simpl; auto;
try (rewrite prim_num; simpl; unfold single_big_proc_create_spec_share;
rewrite <-cid_re, <- pg_re, <- big_log_re, <- big_oracle_re, <- CPU_ID_re, <- init_re;
rewrite Hdestruct, Hdestruct0, Hdestruct9; unfold ch_id in *; rewrite Hdestruct8, Hdestruct11, Hdestruct12; simpl;
auto; fail).
+ rewrite prim_num; simpl; unfold single_big_proc_create_spec_share;
rewrite <-cid_re, <- pg_re, <- big_log_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct, Hdestruct0, Hdestruct9; unfold ch_id in *; rewrite Hdestruct8, Hdestruct11, Hdestruct12; simpl.
rewrite <- pg_re; auto.
+ rewrite ZMap.gss; auto.
+ rewrite prim_num; simpl; unfold single_big_proc_create_spec_share;
rewrite <-cid_re, <- pg_re, <- big_log_re, <- big_oracle_re, <- CPU_ID_re, <- init_re;
rewrite Hdestruct, Hdestruct0, Hdestruct9; unfold ch_id in *; rewrite Hdestruct8, Hdestruct11, Hdestruct12; simpl.
rewrite <- init_re; auto.
+ inv inv_re; constructor; simpl.
{ rewrite prim_num; simpl; unfold single_big_proc_create_spec_share;
rewrite <-cid_re, <- pg_re, <- big_log_re, <- big_oracle_re, <- CPU_ID_re, <- init_re;
rewrite Hdestruct, Hdestruct0, Hdestruct9; unfold ch_id in *; rewrite Hdestruct8, Hdestruct11, Hdestruct12; simpl;
auto. }
{ rewrite prim_num; simpl; unfold single_big_proc_create_spec_share;
rewrite <-cid_re, <- pg_re, <- big_log_re, <- big_oracle_re, <- CPU_ID_re, <- init_re;
rewrite Hdestruct, Hdestruct0, Hdestruct9; unfold ch_id in *; rewrite Hdestruct8, Hdestruct11, Hdestruct12; simpl;
auto. }
- simpl; rewrite prim_num; simpl; unfold single_big_proc_create_spec_share.
inv H.
rewrite <-cid_re, <- pg_re, <- big_log_re, <- big_oracle_re, <- CPU_ID_re, <- init_re.
rewrite Hdestruct, Hdestruct0, Hdestruct9; unfold ch_id in *; rewrite Hdestruct8, Hdestruct11, Hdestruct12; simpl; auto.
- simpl.
unfold choice_check.
rewrite prim_num.
unfold single_big_proc_create_spec_test.
simpl.
unfold ch_id.
inv H; rewrite AC_re; auto.
rewrite <- cid_re.
reflexivity.
- unfold choice_check.
rewrite prim_num.
unfold ch_id.
unfold single_big_proc_create_spec_test.
simpl.
inv H.
rewrite AC_re.
rewrite cid_re.
reflexivity.
Qed.
Lemma big_sched_init_related_t:
∀ mbi_addr kctxt a pd a´ l,
relate_RData kctxt a l pd →
big2_sched_init_spec (Int.unsigned mbi_addr) a = Some a´ →
∃ l´ pd´,
single_big_sched_init_spec (Int.unsigned mbi_addr) ((uRData l), pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
(proc_id (uRData l´)) = (proc_id (uRData l)) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim sched_init (Lint mbi_addr::nil)
(choice_check sched_init (Lint mbi_addr::nil) (uRData l) pd)
(snap_func pd))::l).
Proof.
assert (prim_num: prim_id_num sched_init = 5).
{ unfold prim_id_num; simpl; eauto. }
intros; functional inversion H0; substx; unfold single_big_sched_init_spec;
unfold single_big_sched_init_spec_share; simpl in ×.
inv H; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- CPU_ID_re, <- init_re, <- in_intr_re, <- ioapic_re, <- lapic_re, <- intr_flag_re.
rewrite H4, H5, H6, H7, H8, H9, H10, H11, H12.
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a)
(cid (update init_shared_adt l)))).
{ rewrite <- CPU_ID_re in cid_re; auto. }
rewrite <- cid_eq; rewrite H2.
∃ ((LEvent (proc_id (uRData l)) (LogPrim sched_init (Lint mbi_addr::nil) 42 (snap_func pd)))::l).
simpl. rewrite prim_num.
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.
}
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) by omega.
refine_split´; auto.
- unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; reflexivity.
- constructor.
+ simpl; assumption.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; reflexivity.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; assumption.
+ simpl; assumption.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; reflexivity.
+ simpl; assumption.
+ simpl.
unfold AC_init.
rewrite Hinitcid.
unfold init_real_container.
rewrite Hinj.
simpl.
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 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 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 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 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 init_container; reflexivity. }
{ rewrite i05.
rewrite ZMap.gso; [ | intro contra; inv contra]; rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold init_container; reflexivity. }
{ rewrite i06.
rewrite ZMap.gso; [ | intro contra; inv contra].
rewrite ZMap.gss.
unfold init_container; reflexivity. }
{ rewrite i07.
rewrite ZMap.gss.
unfold init_container; reflexivity. }
+ simpl; assumption.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; reflexivity.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; reflexivity.
+ simpl; assumption.
+ simpl; reflexivity.
+ simpl; rewrite ptp_re; reflexivity.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl.
rewrite <- idpde_re; reflexivity.
+ simpl; rewrite ipt_re; auto.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl.
rewrite <- CPU_ID_re; reflexivity.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl.
rewrite Hinitcid.
rewrite <- CPU_ID_re.
rewrite SingleOracle.main_thread_val.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H.
rewrite ZMap.gss; reflexivity.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; rewrite <- lock_re; reflexivity.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
rewrite Hinitcid.
rewrite _x.
rewrite SingleOracle.main_thread_val.
generalize (CPU_ID_valid l).
simpl.
rewrite <- CPU_ID_re.
intros.
rewrite H; reflexivity.
+ simpl.
rewrite Hinitcid.
rewrite _x in uctxt_re.
rewrite SingleOracle.main_thread_val in uctxt_re.
rewrite current_CPU_IDs_eq_prop in uctxt_re.
inv inv_re.
destruct CPU_ID_inv.
rewrite H.
auto.
+ simpl.
rewrite syncchpool_re; auto.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; reflexivity.
+ simpl; rewrite prim_num.
unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2.
simpl; rewrite <- big_oracle_re; auto.
+ simpl; auto.
+ simpl; auto.
+ simpl; auto.
+ inv inv_re; constructor; simpl; rewrite prim_num.
× unfold single_big_sched_init_spec_share.
rewrite <- cid_re, <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- _x.
rewrite zeq_true.
simpl; auto.
× unfold single_big_sched_init_spec_share.
rewrite <- cid_re, <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- _x.
rewrite zeq_true.
simpl; auto.
- unfold single_big_sched_init_spec_share.
rewrite <- pg_re, <- CPU_ID_re, <- init_re.
rewrite H3, H9, H10.
rewrite <- cid_eq; rewrite H2; simpl.
rewrite <- CPU_ID_re.
rewrite ZMap.gss.
rewrite _x; auto.
- simpl.
unfold choice_check; rewrite prim_num.
rewrite cid_eq; rewrite CPU_ID_re; reflexivity.
Qed.
Lemma big_thread_wakeup_related_t:
∀ cv kctxt a pd a´ res l,
relate_RData kctxt a l pd →
big2_thread_wakeup_spec (Int.unsigned cv) a = Some (a´, res) →
∃ l´ res´,
single_big_thread_wakeup_spec (Int.unsigned cv) ((uRData l), pd) = Some ((uRData l´, pd), res´) ∧
relate_RData kctxt a´ l´ pd ∧
(proc_id (uRData l´)) = (proc_id (uRData l)) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim thread_wakeup (Lint cv::nil)
(choice_check thread_wakeup (Lint cv::nil) (uRData l) pd)
(snap_func pd))::l) ∧
res = res´.
Proof.
generalize int_max; intros max_val; intros.
assert (prim_num: prim_id_num thread_wakeup = 4).
{ unfold prim_id_num; simpl; eauto. }
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H; rewrite <- CPU_ID_re in cid_re; auto. }
functional inversion H0; substx; unfold single_big_thread_wakeup_spec;
unfold single_big_thread_wakeup_spec_share; simpl in ×.
- inv H; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H3, H4, H5, H6, H7, H8, H9, H10; rewrite H9 in H11; rewrite H11, H12.
∃ ((LEvent (proc_id (uRData l)) (LogPrim thread_wakeup (Lint cv::nil) 42 (snap_func pd)))::l), 0.
simpl; rewrite prim_num.
refine_split´; auto.
+ unfold single_big_thread_wakeup_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12; eauto.
+ constructor; auto; simpl; try rewrite prim_num; unfold single_big_thread_wakeup_spec_share;
try (rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite H5, H7, H8, H9, H10, H11, H12; simpl; auto).
× rewrite <- pg_re; auto.
× rewrite <- init_re; auto.
× inv inv_re; constructor; simpl; rewrite prim_num; unfold single_big_thread_wakeup_spec_share.
{ rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12; simpl.
auto. }
{ rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12; simpl.
auto. }
+ unfold single_big_thread_wakeup_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12; simpl.
rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
+ simpl.
unfold choice_check; rewrite prim_num.
rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
- inv H; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H3, H4, H5, H6, H7, H8, H9, H10; rewrite H9 in H11; rewrite H11, H12, H13.
case_eq (in_dec zeq tid full_thread_list); intros; [ | elim n; auto].
∃ ((LEvent (proc_id (uRData l)) (LogPrim thread_wakeup (Lint cv::nil) 42 (snap_func pd)))::l), 1.
simpl; rewrite prim_num.
refine_split´; auto.
+ unfold single_big_thread_wakeup_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H; eauto.
+ constructor; auto; simpl; try rewrite prim_num; unfold single_big_thread_wakeup_spec_share;
try (rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H; simpl; auto).
× rewrite <- pg_re; auto.
× rewrite <- init_re; auto.
× inv inv_re; constructor; simpl; rewrite prim_num; unfold single_big_thread_wakeup_spec_share.
{ rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H; simpl.
auto. }
{ rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H; simpl.
auto. }
+ unfold single_big_thread_wakeup_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H; simpl.
rewrite <- cid_re; auto.
+ simpl.
unfold choice_check; rewrite prim_num.
rewrite <- cid_re; auto.
- inv H; simpl in ×.
rewrite <- cid_re, <- ikern_re, <- ihost_re, <- ipt_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
case_eq (in_dec zeq tid full_thread_list); intros; [ | elim n; auto].
rewrite H3, H4, H5, H6, H7, H8, H9, H10; rewrite H9 in H11; rewrite H11, H12, H13, H14, H15, H.
∃ ((LEvent (proc_id (uRData l)) (LogPrim thread_wakeup (Lint cv::nil) 42 (snap_func pd)))::l), 1.
simpl; rewrite prim_num.
refine_split´; auto.
+ unfold single_big_thread_wakeup_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H14, H15, H; eauto.
+ constructor; auto; simpl;
try (rewrite prim_num; unfold single_big_thread_wakeup_spec_share;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H14, H15, H; simpl; auto).
× rewrite <- pg_re; auto.
× rewrite <- init_re; auto.
× inv inv_re; constructor; simpl; rewrite prim_num; unfold single_big_thread_wakeup_spec_share.
{ rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H14, H15, H; simpl.
auto. }
{ rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H14, H15, H; simpl.
auto. }
+ unfold single_big_thread_wakeup_spec_share.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite H5, H7, H8, H9, H10, H11, H12, H13, H14, H15, H; simpl; auto.
+ simpl.
unfold choice_check; rewrite prim_num.
rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
Qed.
Lemma big_acquire_lock_SC_related_t:
∀ lk_index kctxt a pd a´ l,
relate_RData kctxt a l pd →
big2_acquire_lock_SC_spec (Int.unsigned lk_index) a = Some a´ →
∃ l´ pd´,
single_big_acquire_lock_SC_spec (Int.unsigned lk_index) ((uRData l), pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
(proc_id (uRData l´)) = (proc_id (uRData l)) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim acquire_lock_CHAN (Lint lk_index::nil)
(choice_check acquire_lock_CHAN (Lint lk_index::nil) (uRData l) pd)
(snap_func pd))::l).
Proof.
assert (prim_num: prim_id_num acquire_lock_CHAN = 6).
{ unfold prim_id_num; simpl; eauto. }
intros.
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H; rewrite <- CPU_ID_re in cid_re; auto. }
unfold big2_acquire_lock_SC_spec in *; subdestruct; inv H0.
- substx; unfold single_big_acquire_lock_SC_spec;
unfold single_big_acquire_lock_SC_spec_share; simpl in ×.
inv H; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite <- cid_eq.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6, Hdestruct7.
unfold B_inLock.
rewrite Hdestruct2.
∃ ((LEvent (proc_id (uRData l)) (LogPrim acquire_lock_CHAN (Lint lk_index::nil) 42 (snap_func pd)))::l).
simpl; rewrite prim_num.
refine_split´; auto.
+ unfold single_big_acquire_lock_SC_spec_share.
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
assert (num_chan = 1040); auto.
rewrite H.
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7.
reflexivity.
+ assert (num_chan = 1040); auto.
constructor; simpl; auto;
try (rewrite prim_num; unfold single_big_acquire_lock_SC_spec_share;
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite H;
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto).
× rewrite <- init_re; auto.
× inv inv_re; constructor; simpl; rewrite prim_num; unfold single_big_acquire_lock_SC_spec_share.
{ rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite H;
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto. }
{ rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite H;
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto. }
+ assert (num_chan = 1040); auto.
unfold single_big_acquire_lock_SC_spec_share; rewrite H;
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto.
+ unfold choice_check.
rewrite prim_num; rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
- substx; unfold single_big_acquire_lock_SC_spec;
unfold single_big_acquire_lock_SC_spec_share; simpl in ×.
inv H; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite <- cid_eq.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6.
simpl; rewrite Hdestruct2; rewrite Hdestruct7.
∃ ((LEvent (proc_id (uRData l)) (LogPrim acquire_lock_CHAN (Lint lk_index::nil) 42 (snap_func pd)))::l).
simpl; rewrite prim_num.
refine_split´.
+ unfold single_big_acquire_lock_SC_spec_share.
assert (num_chan = 1040); auto.
rewrite H.
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7.
reflexivity.
+ assert (num_chan = 1040); auto.
constructor; simpl; auto;
try (rewrite prim_num; unfold single_big_acquire_lock_SC_spec_share;
rewrite H;
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto).
× rewrite <- init_re; auto.
× inv inv_re; constructor; simpl; rewrite prim_num; unfold single_big_acquire_lock_SC_spec_share.
{ rewrite H;
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto. }
{ rewrite H;
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re;
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7;
simpl; auto. }
+ assert (num_chan = 1040); auto.
unfold single_big_acquire_lock_SC_spec_share.
rewrite H.
rewrite <- cid_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- big_oracle_re, <- init_re.
rewrite Hdestruct, Hdestruct3, Hdestruct4, Hdestruct5, Hdestruct6; simpl; rewrite Hdestruct2, Hdestruct7; simpl; auto.
+ unfold choice_check.
rewrite prim_num; rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
Qed.
Lemma big_release_lock_SC_related_t:
∀ lk_index kctxt a pd a´ l,
relate_RData kctxt a l pd →
big2_release_lock_SC_spec (Int.unsigned lk_index) a = Some a´ →
∃ l´ pd´,
single_big_release_lock_SC_spec (Int.unsigned lk_index) ((uRData l), pd) = Some (uRData l´, pd´) ∧
relate_RData kctxt a´ l´ pd´ ∧
(proc_id (uRData l´)) = (proc_id (uRData l)) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim release_lock_CHAN (Lint lk_index::nil)
(choice_check release_lock_CHAN (Lint lk_index::nil) (uRData l) pd)
(snap_func pd))::l).
Proof.
generalize int_max; intros max_val.
assert (prim_num: prim_id_num release_lock_CHAN = 7).
{ unfold prim_id_num; simpl; eauto. }
intros.
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H; rewrite <- CPU_ID_re in cid_re; auto. }
unfold big2_release_lock_SC_spec in *; unfold big_release_lock_SC_spec in *; subdestruct; inv H0.
unfold single_big_release_lock_SC_spec;
unfold single_big_release_lock_SC_spec_share; simpl in ×.
inv H; simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re.
rewrite <- cid_eq.
rewrite Hdestruct, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, Hdestruct5.
simpl; rewrite Hdestruct0.
rewrite Hdestruct7.
∃ ((LEvent (proc_id (uRData l)) (LogPrim release_lock_CHAN (Lint lk_index::nil) 42 (snap_func pd)))::l).
simpl; rewrite prim_num.
refine_split´.
- unfold single_big_release_lock_SC_spec_share.
assert (num_chan = 1040); auto.
rewrite H.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re.
rewrite Hdestruct, Hdestruct1, Hdestruct4, Hdestruct5, Hdestruct6.
simpl; rewrite Hdestruct0, Hdestruct7; reflexivity.
- assert (num_chan = 1040); auto.
constructor; auto;
try (simpl; rewrite prim_num; unfold single_big_release_lock_SC_spec_share;
rewrite H;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re;
rewrite Hdestruct, Hdestruct1, Hdestruct4, Hdestruct5, Hdestruct6;
simpl; rewrite Hdestruct0, Hdestruct7; simpl; auto).
+ rewrite <- pg_re; auto.
+ rewrite <- init_re; auto.
+ inv inv_re; constructor; simpl; rewrite prim_num; unfold single_big_release_lock_SC_spec_share.
× rewrite H;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re.
rewrite Hdestruct, Hdestruct1, Hdestruct4, Hdestruct5, Hdestruct6.
simpl; rewrite Hdestruct0, Hdestruct7; simpl; auto.
× rewrite H;
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re.
rewrite Hdestruct, Hdestruct1, Hdestruct4, Hdestruct5, Hdestruct6.
simpl; rewrite Hdestruct0, Hdestruct7; simpl; auto.
- assert (num_chan = 1040); auto.
unfold single_big_release_lock_SC_spec_share.
rewrite H.
rewrite <- cid_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re.
rewrite Hdestruct, Hdestruct1, Hdestruct4, Hdestruct5, Hdestruct6.
simpl; rewrite Hdestruct0, Hdestruct7; simpl; auto.
- unfold choice_check.
rewrite prim_num; rewrite <- CPU_ID_re; rewrite <- cid_eq; auto.
Qed.
Lemma big_ipc_send_body_related_t:
∀ chid vaddr scount kctxt a pd a´ l res,
relate_RData kctxt a l pd →
thread_ipc_send_body_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scount) a = Some (a´, res) →
∃ l´ pd´ res´,
single_big_ipc_send_body_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scount) ((uRData l), pd)
= Some ((uRData l´, pd´), res´) ∧
relate_RData kctxt a´ l´ pd´ ∧
(proc_id (uRData l´)) = (proc_id (uRData l)) ∧
l´ = (LEvent (proc_id (uRData l)) (LogPrim ipc_send_body ((Lint chid)::(Lint vaddr)::(Lint scount)::nil)
(choice_check ipc_send_body
((Lint chid)::(Lint vaddr)::(Lint scount)::nil) (uRData l) pd)
(snap_func pd)))::l ∧
res = res´.
Proof.
generalize int_max; intros max_val.
assert (prim_num: prim_id_num ipc_send_body = 8).
{ unfold prim_id_num; simpl; eauto. }
intros.
assert (cid_eq: ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
(ZMap.get (AbstractDataType.CPU_ID a) (cid (update init_shared_adt l)))).
{ inv H; rewrite <- CPU_ID_re in cid_re; auto. }
unfold thread_ipc_send_body_spec in H0; unfold big_ipc_send_body_spec in H0; subdestruct.
unfold big_page_copy_spec in Hdestruct7.
subdestruct.
inv Hdestruct7.
unfold single_big_ipc_send_body_spec.
unfold single_big_page_copy_spec.
clear Hdestruct2 Hdestruct3 Hdestruct4; subst.
inv H0.
inv H.
simpl in ×.
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re, <- ipt_re, <- pperm_re, <- flatmem_re.
rewrite <- cid_eq.
rewrite Hdestruct, Hdestruct10, Hdestruct13, Hdestruct14, Hdestruct15.
rewrite Hdestruct1, Hdestruct8, Hdestruct9.
unfold B_inLock.
rewrite Hdestruct17, Hdestruct16, Hdestruct0, Hdestruct5, Hdestruct6, Hdestruct11, Hdestruct12.
rewrite Hdestruct19, Hdestruct20.
∃ ((LEvent (proc_id (uRData l)) (LogPrim ipc_send_body (Lint chid::Lint vaddr::Lint scount::nil) 42 (snap_func pd)))::l).
simpl; rewrite prim_num.
refine_split´.
- simpl.
unfold single_big_ipc_send_body_spec.
unfold single_big_page_copy_spec.
simpl.
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re, <- ipt_re, <- pperm_re, <- flatmem_re.
rewrite <- cid_eq.
rewrite Hdestruct, Hdestruct10, Hdestruct13, Hdestruct14, Hdestruct15.
rewrite Hdestruct1, Hdestruct8, Hdestruct9.
unfold B_inLock.
rewrite Hdestruct17, Hdestruct16, Hdestruct0, Hdestruct5, Hdestruct6, Hdestruct11, Hdestruct12.
rewrite Hdestruct19, Hdestruct20.
simpl.
reflexivity.
- constructor; auto; simpl;
try (rewrite prim_num;
unfold single_big_ipc_send_body_spec; unfold single_big_page_copy_spec; unfold single_get_kernel_pa_spec; simpl;
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re, <- ipt_re, <- pperm_re, <- flatmem_re; rewrite <- cid_eq;
rewrite Hdestruct, Hdestruct10, Hdestruct13, Hdestruct14, Hdestruct15;
rewrite Hdestruct1, Hdestruct8, Hdestruct9;
unfold B_inLock;
rewrite Hdestruct17, Hdestruct16, Hdestruct0, Hdestruct5, Hdestruct6, Hdestruct11, Hdestruct12;
rewrite Hdestruct19, Hdestruct20; simpl in *; auto).
+ rewrite <- pg_re; auto.
+ rewrite <- init_re; auto.
+ inv inv_re; constructor; simpl; rewrite prim_num;
unfold single_big_ipc_send_body_spec; unfold single_big_page_copy_spec; unfold single_get_kernel_pa_spec; simpl;
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re, <- ipt_re, <- pperm_re, <- flatmem_re; rewrite <- cid_eq;
rewrite Hdestruct, Hdestruct10, Hdestruct13, Hdestruct14, Hdestruct15;
rewrite Hdestruct1, Hdestruct8, Hdestruct9;
unfold B_inLock;
rewrite Hdestruct17, Hdestruct16, Hdestruct0, Hdestruct5, Hdestruct6, Hdestruct11, Hdestruct12;
rewrite Hdestruct19, Hdestruct20.
× simpl; auto.
× simpl; auto.
- unfold single_big_ipc_send_body_spec; unfold single_big_page_copy_spec; unfold single_get_kernel_pa_spec; simpl;
rewrite <- ikern_re, <- ihost_re, <- pg_re, <- big_log_re, <- lock_re, <- CPU_ID_re, <- init_re, <- syncchpool_re, <- ipt_re, <- pperm_re, <- flatmem_re; rewrite <- cid_eq;
rewrite Hdestruct, Hdestruct10, Hdestruct13, Hdestruct14, Hdestruct15;
rewrite Hdestruct1, Hdestruct8, Hdestruct9;
unfold B_inLock;
rewrite Hdestruct17, Hdestruct16, Hdestruct0, Hdestruct5, Hdestruct6, Hdestruct11, Hdestruct12;
rewrite Hdestruct19, Hdestruct20.
simpl; auto.
- rewrite cid_eq.
unfold choice_check.
rewrite prim_num.
rewrite CPU_ID_re.
auto.
- reflexivity.
Qed.
End PHTHREAD2TGENLEMMAHASEVENT.