Library mcertikos.multithread.phbthread.SingleOracleImpl
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 LoadStoreSem2.
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 AuxSingleAbstractDataType.
Require Import PHThread2TComposeData.
Require Import ObjPHBThreadReplayFunction.
Require Import AlgebraicMemImpl.
Require Import INVLemmaProc.
Ltac smart_unfold adt :=
match goal with
| |- context [?fspec adt] ⇒ unfold fspec
| |- context [?fspec _ adt] ⇒ unfold fspec
| |- context [?fspec _ _ adt] ⇒ unfold fspec
| |- context [?fspec _ _ _ adt] ⇒ unfold fspec
| |- context [?fspec _ _ _ _ adt] ⇒ unfold fspec
end.
Ltac divide_tac adt :=
match goal with
| |- context [(ipt adt)] ⇒ destruct (ipt adt); auto
| |- context [(ikern adt)] ⇒ destruct (ikern adt); auto
| |- context [(ihost adt)] ⇒ destruct (ihost adt); auto
| |- context [(init adt)] ⇒ destruct (init adt); auto
| |- context [(pg adt)] ⇒ destruct (pg adt); auto
| |- context [(intr_flag adt)] ⇒ destruct (intr_flag adt); auto
| |- context [(in_intr adt)] ⇒ destruct (in_intr adt); auto
| |- context [(nth_error (IoApicIrqs (s (ioapic adt))) _)] ⇒
destruct ((nth_error (IoApicIrqs (s (ioapic adt))) _)); auto
| |- context [(nth_error (IoApicEnables (s (ioapic adt))) _)] ⇒
destruct (nth_error (IoApicEnables (s (ioapic adt))) _); auto
end.
Ltac divide_repeat adt :=
repeat match goal with
| |- context [(ipt adt)] ⇒ destruct (ipt adt); auto
| |- context [(ikern adt)] ⇒ destruct (ikern adt); auto
| |- context [(ihost adt)] ⇒ destruct (ihost adt); auto
| |- context [(init adt)] ⇒ destruct (init adt); auto
| |- context [(pg adt)] ⇒ destruct (pg adt); auto
| |- context [(intr_flag adt)] ⇒ destruct (intr_flag adt); auto
| |- context [(in_intr adt)] ⇒ destruct (intr_flag adt); auto
end.
Opaque full_thread_list.
Section SINGLEORACLEINSTANCE.
Section SORACLEDEF.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params_ops: RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Definition prim_thread_init_pc {F V} (ge : Genv.t F V) (name : ident) (args : list lval): option val :=
if peq name proc_create
then match Genv.find_symbol ge START_USER_FUN_LOC with
| Some b´ ⇒ Some (Vptr b´ Int.zero)
| _ ⇒ None
end
else None.
Definition cal_init_dproc (pv_adt : dproc) (parent: Z) (q: Z) (buc : block) (uc_ofs : int): dproc:=
let uctx0 := uctxt pv_adt in
let uctx1 := ZMap.set U_SS CPU_GDT_UDATA
(ZMap.set U_CS CPU_GDT_UCODE
(ZMap.set U_DS CPU_GDT_UDATA
(ZMap.set U_ES CPU_GDT_UDATA uctx0))) in
let uctx2 := ZMap.set U_EIP Vzero
(ZMap.set U_EFLAGS FL_IF
(ZMap.set U_ESP (Vint STACK_TOP) uctx1)) in
(pv_adt {pv_AC: (mkContainer q 0 parent nil true)} {pv_uctxt: uctx2}).
Fixpoint thread_init_dproc_iter (curid: Z) (l : Log) : option dproc :=
match l with
| nil ⇒ None
| ev::l´ ⇒
match ev with
| LEvent id ev_detail ⇒
match ev_detail with
| LogPrim name largs new_id _⇒
if peq name proc_create
then if zeq curid new_id
then match largs with
| (Lint elf_id)::(Lptr buc uc_ofs)::(Lint q)::nil ⇒
match (zle_lt (id × Constant.max_children + 1) curid (id × Constant.max_children
+ 1 + Constant.max_children),
zlt_lt Constant.TOTAL_CPU curid num_proc,
zle_le 0 (Int.unsigned q) Int.max_unsigned,
pg (update init_shared_adt l),
init (update init_shared_adt l)) with
| (left _, left _, left _, true, true)
⇒ Some (cal_init_dproc nomain_init_priv_adt id (Int.unsigned q) buc uc_ofs)
| ( _, _, _, _) ⇒ None
end
| _ ⇒ None
end
else thread_init_dproc_iter curid l´
else thread_init_dproc_iter curid l´
| _ ⇒ thread_init_dproc_iter curid l´
end
end
end.
Definition thread_init_dproc_aux (curid: Z) (l : Log) : option dproc :=
if zeq curid main_thread
then match l with
| nil ⇒ Some main_init_dproc
| _ ⇒ None
end
else thread_init_dproc_iter curid l.
Definition thread_init_dproc (curid: Z) : dproc :=
match thread_init_dproc_aux curid init_log with
| Some init_dproc_val ⇒ init_dproc_val
| _ ⇒ if zeq curid main_thread then main_init_dproc else nomain_init_priv_adt
end.
Program Instance s_oracle_prf : SingleOracle (single_data := AuxSingleAbstractDataType.single_data)
(single_oracle_ops := s_oracle_ops)
(threads_conf_ops := s_threads_ops):=
{
has_event := has_event;
update := update;
thread_init_dproc := thread_init_dproc;
state_check := state_check;
sync_chpool_check := ObjPHBThreadReplayFunction.sync_chpool_check;
snap_func := snap_func;
snap_rev_func := snap_rev_func;
choice_check := ObjPHBThreadReplayFunction.choice_check;
PHThread2TCompose := PHThread2TComposeData.combine_data;
prim_thread_init_pc := @prim_thread_init_pc
}.
End SORACLEDEF.
Section SORACLEBASICPROP.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params_ops: RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Class SingleOracleBasicProp `{single_oracle_prf : SingleOracle}
`{s_threads_ops: ThreadsConfigurationOps} :=
{
current_CPU_IDs_eq_prop: SingleOracle.current_CPU_ID = GlobalOracle.current_CPU_ID;
current_thread_eq_current_curid_prop: SingleOracle.current_thread = GlobalOracle.current_curid;
main_thread_init_log_prop: SingleOracle.current_thread = SingleOracle.main_thread → SingleOracle.init_log = nil;
nomain_thread_init_log_prop: SingleOracle.current_thread ≠ SingleOracle.main_thread → SingleOracle.init_log ≠ nil
}.
End SORACLEBASICPROP.
Section SINGLEORACLEPROPDEF.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params_ops: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
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)}.
Section SINGLE_ORACLE_PROP_INSTANCE.
Program Instance s_oracle_prop_prf : SingleOracleProp (thread_conf_prf := s_threads_prf) := { }.
Transparent update.
Next Obligation.
set (adt := update d l); unfold apply_event.
destruct a; destruct l0; [simpl; inv H0 | simpl; inv H0 | | auto ].
destruct (prim_id_num id); try congruence.
repeat (destruct p; simpl; try auto).
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *;auto.
case_eq (ObjPHBThreadIPC.single_big_release_lock_SC_spec_share (Int.unsigned n) (syncchpoolSnap dprocSnap) adt); intros;
[ | reflexivity].
functional inversion H; simpl; auto.
-
destruct args; auto; destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadSCHED.single_big_sched_init_spec_share (Int.unsigned n) adt); intros;
[ | reflexivity].
functional inversion H; simpl in ×.
inv H; simpl.
assert (prev_id: ZMap.get (CPU_ID adt) (cid adt) = main_thread) by omega.
rewrite prev_id; rewrite ZMap.gss; auto.
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadSCHED.single_big_proc_create_spec_share adt b ofs
(Int.unsigned n0) choice);
intros; simpl; [ | reflexivity].
functional inversion H; simpl; auto.
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
case_eq (ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share (Int.unsigned n) adt); intros;
[ | reflexivity].
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in H; subdestruct; inv H; simpl; auto.
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
case_eq (ObjPHBThreadIPC.single_big_ipc_send_body_spec (Int.unsigned n) (Int.unsigned n0) (Int.unsigned n1)
(adt, snap_rev_func dprocSnap)); intros;
[ | reflexivity].
destruct p.
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in H; subdestruct.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in Hdestruct7; subdestruct.
inv Hdestruct7; inv H.
simpl.
auto.
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share (Int.unsigned n) adt); simpl; [ | reflexivity].
intros; functional inversion H; simpl; auto.
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
case_eq (zeq choice 0); intros; subst.
+ case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 0 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H1; subdestruct; substx; inv H1; simpl in ×.
reflexivity.
+ case_eq (zeq choice 1); intros; subst.
× case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H2; subdestruct; substx; inv H2; simpl in *; auto.
rewrite zeq_false; auto.
destruct a0; omega.
× case_eq (zeq choice 2); intros; subst.
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
{ destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H3; subdestruct; substx; inv H3; simpl in *; auto.
rewrite zeq_false; auto.
destruct a0; omega. }
{ case_eq (zeq choice 3); intros; subst.
- case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H4; subdestruct; substx; inv H4; simpl in *; auto.
substx.
rewrite zeq_false; auto; [ | destruct a0; omega].
set (adt´ := (update d l) {sh_big_log : BigDef (TBEVENT (CPU_ID (update d l))
(TBSHARED (BPALLOCE (ZMap.get (CPU_ID (update d l))
(cid (update d l))) z0))
:: big_oracle (update d l) (CPU_ID (update d l)) l0 ++
l0)}).
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 0 adt´); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H4; subdestruct; substx; inv H4; simpl in *; auto.
- case_eq (zeq choice 4); intros; subst.
+ case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H5; subdestruct; substx; inv H5; simpl in *; auto.
substx.
rewrite zeq_false; auto; [ | destruct a0; omega].
set (adt´ := (update d l) {sh_big_log : BigDef (TBEVENT (CPU_ID (update d l))
(TBSHARED (BPALLOCE (ZMap.get (CPU_ID (update d l))
(cid (update d l))) z0))
:: big_oracle (update d l) (CPU_ID (update d l)) l0 ++
l0)}).
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt´); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H5; subdestruct; substx; inv H5; simpl in *; auto.
+ destruct choice; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega. }
-
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) choice adt); intros; [ | reflexivity].
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H; subdestruct; substx; inv H; simpl in *; auto.
Qed.
Next Obligation.
set (adt := update d l); unfold apply_event.
destruct a; destruct l0; [ | | | auto ].
- destruct (init adt); simpl; auto.
destruct (pg adt); simpl; auto.
destruct (BigLogThreadConfigFunction.B_inLock (CPU_ID adt) (big_log adt)); simpl; auto.
destruct (big_log adt); simpl; auto.
destruct (ZMap.get (msg_q_id (CPU_ID adt) + ID_AT_range) (lock adt)); simpl; auto.
destruct (B_CalTCB_log_real (TBEVENT (CPU_ID adt)
(TBSHARED (BTDYIELD (ZMap.get (CPU_ID adt) (cid adt))))
:: big_oracle adt (CPU_ID adt) l0 ++ l0)); simpl; auto.
destruct t; simpl; auto.
destruct (zle_lt 0 run_id 1024); simpl; auto.
destruct (BigLogThreadConfigFunction.B_GetContainerUsed run_id (CPU_ID adt) l0); simpl; auto.
destruct (BigLogThreadConfigFunction.B_GetContainerUsed_opt msg (CPU_ID adt) l0); simpl; auto.
destruct (option_z_check msg); simpl; auto.
destruct (z_check run_id); simpl; auto.
- destruct syncch; simpl; auto.
destruct (init adt); simpl; auto.
destruct (pg adt); simpl; auto.
destruct (BigLogThreadConfigFunction.B_inLock (CPU_ID adt) (big_log adt)); simpl; auto.
destruct (zlt_lt 0 (ZMap.get (CPU_ID adt) (cid adt)) 1024); simpl; auto.
destruct (zle_lt 0 i 1024); simpl; auto.
destruct (big_log adt); simpl; auto.
destruct (ZMap.get (slp_q_id i 0 + ID_AT_range) (lock adt)); simpl; auto.
destruct (ZMap.get (slp_q_id i 0 + lock_TCB_range) (lock adt)); simpl; auto.
destruct b; simpl; auto.
destruct (B_CalTCB_log_real (TBEVENT (CPU_ID adt)
(TBSHARED (BTDSLEEP (ZMap.get (CPU_ID adt) (cid adt)) i s))
:: big_oracle adt (CPU_ID adt) l0 ++ l0)); simpl; auto.
destruct t; simpl; auto.
destruct (B_CalLock (slp_q_id i 0 + lock_TCB_range) l0); simpl; auto.
destruct p; destruct p.
destruct n0; simpl; auto.
destruct n0; simpl; auto.
destruct h; simpl; auto.
destruct o; simpl; auto.
destruct (B_CalLock (slp_q_id i 0 + lock_TCB_range) (big_oracle adt (CPU_ID adt) l0 ++ l0)); simpl; auto.
destruct (zle_lt 0 run_id 1024); simpl; auto.
destruct (BigLogThreadConfigFunction.B_GetContainerUsed run_id (CPU_ID adt) l0); simpl; auto.
destruct (zeq (CPU_ID adt) z0); simpl; auto.
destruct (z_check run_id); simpl; auto.
- destruct (prim_id_num id); try congruence.
repeat (destruct p; simpl; try auto).
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *;auto.
case_eq (ObjPHBThreadIPC.single_big_release_lock_SC_spec_share (Int.unsigned n) (syncchpoolSnap dprocSnap) adt); intros;
[ | reflexivity].
functional inversion H; simpl; auto.
+
destruct args; auto; destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadSCHED.single_big_sched_init_spec_share (Int.unsigned n) adt); intros;
[ | reflexivity].
functional inversion H; simpl in *; auto.
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadSCHED.single_big_proc_create_spec_share adt b ofs (Int.unsigned n0) choice); intros; simpl; [ | reflexivity].
functional inversion H; simpl; auto.
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
case_eq (ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share (Int.unsigned n) adt); intros;
[ | reflexivity].
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in H; subdestruct; inv H; simpl; auto.
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
destruct l0; auto; destruct args; simpl in *; auto.
case_eq (ObjPHBThreadIPC.single_big_ipc_send_body_spec (Int.unsigned n) (Int.unsigned n0) (Int.unsigned n1)
(adt, snap_rev_func dprocSnap)); intros;
[ | reflexivity].
destruct p.
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in H; subdestruct.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in Hdestruct7; subdestruct.
inv Hdestruct7; inv H.
simpl.
auto.
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share (Int.unsigned n) adt); simpl; [ | reflexivity].
intros; functional inversion H; simpl; auto.
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
destruct l0; auto; destruct args; auto.
case_eq (zeq choice 0); intros; subst.
{ case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 0 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H0; subdestruct; substx; inv H0; simpl in ×.
reflexivity. }
{ case_eq (zeq choice 1); intros; subst.
- case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H1; subdestruct; substx; inv H1; simpl in *; auto.
rewrite zeq_false; auto.
destruct a0; omega.
- case_eq (zeq choice 2); intros; subst.
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
+ destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H2; subdestruct; substx; inv H2; simpl in *; auto.
rewrite zeq_false; auto.
destruct a0; omega.
+ case_eq (zeq choice 3); intros; subst.
× case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H3; subdestruct; substx; inv H3; simpl in *; auto.
substx.
rewrite zeq_false; auto; [ | destruct a0; omega].
set (adt´ := (update d l) {sh_big_log : BigDef (TBEVENT (CPU_ID (update d l))
(TBSHARED (BPALLOCE (ZMap.get (CPU_ID (update d l))
(cid (update d l)))
z0))
:: big_oracle (update d l) (CPU_ID (update d l)) l0 ++
l0)}).
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 0 adt´); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H3; subdestruct; substx; inv H3; simpl in *; auto.
× case_eq (zeq choice 4); intros; subst.
{ case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H4; subdestruct; substx; inv H4; simpl in *; auto.
substx.
rewrite zeq_false; auto; [ | destruct a0; omega].
set (adt´ := (update d l) {sh_big_log : BigDef (TBEVENT (CPU_ID (update d l))
(TBSHARED (BPALLOCE (ZMap.get (CPU_ID (update d l))
(cid (update d l)))
z0))
:: big_oracle (update d l) (CPU_ID (update d l)) l0 ++
l0)}).
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) 1 adt´); intros; eauto.
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H4; subdestruct; substx; inv H4; simpl in *; auto. }
{ destruct choice; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega.
destruct p; simpl; eauto; try omega. }
}
+
destruct args; simpl in *; auto.
destruct l0; auto; destruct args; auto.
case_eq (ObjPHBThreadVMM.single_big_palloc_spec_share (Int.unsigned n) choice adt); intros; [ | reflexivity].
destruct p.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in H; subdestruct; substx; inv H; simpl in *; auto.
Qed.
Opaque update.
Lemma thread_init_dproc_iter_preserve_fields:
∀ log curid new_init_dproc,
thread_init_dproc_iter curid log = Some new_init_dproc →
ti new_init_dproc = ti nomain_init_priv_adt ∧
ikern new_init_dproc = ikern nomain_init_priv_adt ∧
ihost new_init_dproc = ihost nomain_init_priv_adt ∧
HP new_init_dproc = HP nomain_init_priv_adt ∧
pperm new_init_dproc = pperm nomain_init_priv_adt ∧
PT new_init_dproc = PT nomain_init_priv_adt ∧
ptpool new_init_dproc = ptpool nomain_init_priv_adt ∧
ipt new_init_dproc = ipt nomain_init_priv_adt ∧
syncchpool new_init_dproc = syncchpool nomain_init_priv_adt ∧
ept new_init_dproc = ept nomain_init_priv_adt ∧
vmcs new_init_dproc = vmcs nomain_init_priv_adt ∧
vmx new_init_dproc = vmx nomain_init_priv_adt ∧
com1 new_init_dproc = com1 nomain_init_priv_adt ∧
drv_serial new_init_dproc = drv_serial nomain_init_priv_adt ∧
console_concrete new_init_dproc = console_concrete nomain_init_priv_adt ∧
console new_init_dproc = console nomain_init_priv_adt ∧
ioapic new_init_dproc = ioapic nomain_init_priv_adt ∧
lapic new_init_dproc = lapic nomain_init_priv_adt ∧
tf new_init_dproc = tf nomain_init_priv_adt ∧
tf_reg new_init_dproc = tf_reg nomain_init_priv_adt ∧
curr_intr_num new_init_dproc = curr_intr_num nomain_init_priv_adt ∧
intr_flag new_init_dproc = intr_flag nomain_init_priv_adt ∧
saved_intr_flags new_init_dproc = saved_intr_flags nomain_init_priv_adt ∧
in_intr new_init_dproc = in_intr nomain_init_priv_adt ∧
i_dev_serial new_init_dproc = i_dev_serial nomain_init_priv_adt.
Proof.
intro log; induction log.
- intros; simpl in *; inv H; tauto.
- intros; simpl in H.
generalize (IHlog curid); intro IHlog´; clear IHlog.
destruct a; subst.
destruct l; try (eapply IHlog´; eassumption).
subdestruct; subst.
+ unfold cal_init_dproc in H; inv H; simpl; repeat (split; try reflexivity).
+ eapply IHlog´; eauto.
+ eapply IHlog´; eauto.
Qed.
Lemma cal_init_dproc_uctxt_val:
∀ parent q buc uc_ofs d,
cal_init_dproc nomain_init_priv_adt parent q buc uc_ofs = d →
(uctxt d) =
let uctx0 := (ZMap.init Vundef) in
let uctx1 := ZMap.set U_SS CPU_GDT_UDATA
(ZMap.set U_CS CPU_GDT_UCODE
(ZMap.set U_DS CPU_GDT_UDATA
(ZMap.set U_ES CPU_GDT_UDATA uctx0))) in
let uctx2 := ZMap.set U_EIP Vzero
(ZMap.set U_EFLAGS FL_IF
(ZMap.set U_ESP (Vint STACK_TOP) uctx1)) in
uctx2.
Proof.
unfold cal_init_dproc; simpl.
intros.
inv H; simpl.
reflexivity.
Qed.
Lemma thread_init_iter_uctxt_val:
∀ l curid d,
thread_init_dproc_iter curid l = Some d →
(uctxt d) =
let uctx0 := (ZMap.init Vundef) in
let uctx1 := ZMap.set U_SS CPU_GDT_UDATA
(ZMap.set U_CS CPU_GDT_UCODE
(ZMap.set U_DS CPU_GDT_UDATA
(ZMap.set U_ES CPU_GDT_UDATA uctx0))) in
let uctx2 := ZMap.set U_EIP Vzero
(ZMap.set U_EFLAGS FL_IF
(ZMap.set U_ESP (Vint STACK_TOP) uctx1)) in
uctx2.
Proof.
induction l; intros.
- simpl in H.
inv H.
- simpl in H.
generalize (IHl curid); intro IHl´; clear IHl.
destruct a; subst.
destruct l0; try (eapply IHl´; eassumption).
subdestruct; subst.
+ inv H.
eapply cal_init_dproc_uctxt_val; eauto.
+ eapply IHl´; eauto.
+ eapply IHl´; eauto.
Qed.
Next Obligation.
unfold combine_data; simpl.
constructor; simpl.
-
simpl.
unfold thread_init_dproc; simpl; unfold thread_init_dproc_aux.
case_eq (zeq current_thread main_thread); intros; subst.
+ simpl.
destruct init_log; simpl; econstructor.
+ induction init_log; [ simpl; constructor | ].
simpl; case_eq a.
intros; simpl; subst.
destruct l0; simpl; try (case_eq l; intros; subst; try econstructor; eassumption; fail).
case_eq (peq id proc_create); simpl; intros; subst; try eassumption.
case_eq (zeq current_thread choice); simpl; intros; subst; try eassumption.
repeat (destruct args; simpl; intros; subst; try econstructor;
destruct l0; simpl; intros; subst; try econstructor).
destruct args; simpl; intros; subst; try econstructor.
destruct (zle_lt (z × 8 + 1) current_thread (z × 8 + 1 + 8)); intros; simpl; try econstructor.
destruct (zlt_lt 8 current_thread 1024); intros; simpl; try econstructor.
destruct (zle_le 0 (Int.unsigned n2) Int.max_unsigned); intros; simpl; try econstructor.
destruct (pg (update init_shared_adt (LEvent z (LogPrim proc_create
(Lint n1 :: Lptr b ofs :: Lint n2 :: nil)
current_thread dprocSnap) :: l)));
intros; simpl; try econstructor.
destruct (init (update init_shared_adt (LEvent z (LogPrim proc_create
(Lint n1 :: Lptr b ofs :: Lint n2 :: nil)
current_thread dprocSnap) :: l)));
intros; simpl; try econstructor.
-
unfold thread_init_dproc; simpl; unfold thread_init_dproc_aux.
case_eq (zeq current_thread main_thread); intros; subst.
+ simpl; destruct init_log; simpl; econstructor.
+ case_eq (thread_init_dproc_iter current_thread init_log); intros; [ | simpl; econstructor].
× induction init_log; [simpl in *; inv H0; simpl; constructor | ].
simpl in H0; case_eq a.
intros; simpl; subst.
destruct l0; simpl; try ( case_eq l; intros; subst; try (inv H0; fail); eapply IHl; auto; fail).
case_eq (peq id proc_create); simpl; intros; subst;
[ | rewrite peq_false in H0; [ eapply IHl; eauto | intro contra; elim n1; eauto]].
rewrite peq_true in H0.
case_eq (zeq current_thread choice); simpl; intros; subst; [ | rewrite zeq_false in H0; eauto; eapply IHl; eauto].
rewrite zeq_true in H0.
repeat (destruct args; simpl; intros; subst; try (inv H0; fail);
destruct l0; simpl; intros; subst; try (inv H0; fail)).
destruct args; simpl; intros; subst; try (inv H0; fail).
destruct (zle_lt (z × 8 + 1) current_thread (z × 8 + 1 + 8));
intros; simpl; subst; try (inv H0; fail).
destruct (zlt_lt 8 current_thread 1024); intros; simpl; subst; try (inv H0; fail).
destruct (zle_le 0 (Int.unsigned n2) Int.max_unsigned); intros; simpl; try (inv H0; fail).
destruct (pg (update init_shared_adt (LEvent z (LogPrim proc_create
(Lint n1 :: Lptr b ofs :: Lint n2 :: nil)
current_thread dprocSnap) :: l)));
intros; simpl; try (inv H0; fail).
destruct (init (update init_shared_adt (LEvent z (LogPrim proc_create
(Lint n1 :: Lptr b ofs :: Lint n2 :: nil)
current_thread dprocSnap) :: l)));
intros; simpl; try (inv H0; fail).
unfold cal_init_dproc in H0.
simpl; inv H0.
simpl; auto.
-
econstructor; eauto; simpl; rewrite ZMap.gi; econstructor.
-
unfold thread_init_dproc; simpl; unfold thread_init_dproc_aux.
case_eq (zeq current_thread main_thread); intros; subst.
+ simpl; destruct init_log; simpl; econstructor; eauto; simpl.
× case_eq (zeq ii (ZMap.get (CPU_ID (update init_shared_adt nil))
(cid (update init_shared_adt nil)))); intros.
{ rewrite e0.
rewrite ZMap.gss; rewrite ZMap.gi; constructor. }
{ rewrite ZMap.gso; auto; rewrite ZMap.gi; rewrite ZMap.gi; constructor. }
× case_eq (zeq ii (ZMap.get (CPU_ID (update init_shared_adt nil))
(cid (update init_shared_adt nil)))); intros.
{ rewrite e0.
rewrite ZMap.gss; rewrite ZMap.gi; constructor. }
{ rewrite ZMap.gso; auto; rewrite ZMap.gi; rewrite ZMap.gi; constructor. }
× case_eq (zeq ii (ZMap.get (CPU_ID (update init_shared_adt (l :: l0)))
(cid (update init_shared_adt (l :: l0))))); intros.
{ rewrite e0.
rewrite ZMap.gss; rewrite ZMap.gi; constructor. }
{ rewrite ZMap.gso; auto; rewrite ZMap.gi; rewrite ZMap.gi; constructor. }
× case_eq (zeq ii (ZMap.get (CPU_ID (update init_shared_adt (l :: l0)))
(cid (update init_shared_adt (l :: l0))))); intros.
{ rewrite e0.
rewrite ZMap.gss; rewrite ZMap.gi; constructor. }
{ rewrite ZMap.gso; auto; rewrite ZMap.gi; rewrite ZMap.gi; constructor. }
+ inv s_threads_prf.
simpl in init_log_proc_id.
case_eq (thread_init_dproc_iter current_thread init_log); intros; [ | simpl].
× inv s_oracle_basic_prop_prf.
exploit thread_init_iter_uctxt_val; eauto.
intros.
rewrite H1.
simpl.
assert (uctxt_inject_neutral (ZMap.init (ZMap.init Vundef)) n).
{ unfold uctxt_inject_neutral.
intros.
rewrite ZMap.gi.
rewrite ZMap.gi.
split; constructor. }
eapply uctxt_inject_neutral_gss; eauto.
repeat eapply uctxt_inject_neutral0_gss;
try eapply uctxt_inject_neutral0_Vint.
intros.
rewrite ZMap.gi.
split; constructor.
× constructor; simpl.
{ case_eq (zeq ii (ZMap.get (CPU_ID (update init_shared_adt init_log))
(cid (update init_shared_adt init_log)))); intros.
{ rewrite e; rewrite ZMap.gss; rewrite ZMap.gi; constructor. }
{ rewrite ZMap.gso; auto; rewrite ZMap.gi; rewrite ZMap.gi; constructor. } }
{ case_eq (zeq ii (ZMap.get (CPU_ID (update init_shared_adt init_log))
(cid (update init_shared_adt init_log)))); intros.
{ rewrite e; rewrite ZMap.gss; rewrite ZMap.gi; constructor. }
{ rewrite ZMap.gso; auto; rewrite ZMap.gi; rewrite ZMap.gi; constructor. } }
-
unfold thread_init_dproc.
unfold thread_init_dproc_aux.
case_eq (zeq current_thread main_thread).
+ intros.
destruct init_log.
× simpl.
unfold VMCSPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt nil)) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
× simpl.
unfold VMCSPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt (l :: l0))) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
+ intros.
case_eq (thread_init_dproc_iter current_thread init_log); intros.
× simpl.
assert ((vmcs d) = (VMCSValid Vzero Vzero (ZMap.init Vundef))).
{ exploit thread_init_dproc_iter_preserve_fields; eauto.
intros.
blast H1; simpl in ×.
rewrite H24; auto. }
rewrite H1.
unfold VMCSPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt init_log)) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
× simpl.
unfold VMCSPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt init_log)) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
-
unfold thread_init_dproc.
unfold thread_init_dproc_aux.
case_eq (zeq current_thread main_thread).
+ intros.
destruct init_log.
× simpl.
unfold VMXPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt nil)) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
× simpl.
unfold VMXPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt (l :: l0))) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
+ intros.
case_eq (thread_init_dproc_iter current_thread init_log); intros.
× simpl.
assert ((vmx d) = (ZMap.init Vundef)).
{ exploit thread_init_dproc_iter_preserve_fields; eauto.
intros.
blast H1; simpl in ×.
reflexivity. }
rewrite H1.
unfold VMXPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt init_log)) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
× simpl.
unfold VMXPool_inject_neutral in *; intros.
case_eq (zeq (CPU_ID (update init_shared_adt init_log)) vmid).
{ intros; subst.
rewrite ZMap.gss.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
{ intros; subst.
rewrite ZMap.gso; auto.
rewrite ZMap.gi.
econstructor; intros; unfold v; rewrite ZMap.gi; split; eauto; econstructor. }
-
unfold thread_init_dproc; simpl; unfold thread_init_dproc_aux.
case_eq (zeq current_thread main_thread); intros; subst.
+ destruct init_log; simpl; econstructor.
+ induction init_log; [simpl; constructor | ].
simpl; case_eq a.
intros; simpl; subst.
destruct l0; simpl; try (case_eq l; intros; subst; try econstructor; eassumption).
case_eq (peq id proc_create); simpl; intros; subst; try eassumption.
case_eq (zeq current_thread choice); simpl; intros; subst; try eassumption.
repeat (destruct args; simpl; intros; subst; try econstructor;
destruct l0; simpl; intros; subst; try econstructor).
destruct args; simpl; intros; subst; try econstructor.
destruct (zle_lt (z × 8 + 1) current_thread (z × 8 + 1 + 8)); intros; simpl; try econstructor.
destruct (zlt_lt 8 current_thread 1024); intros; simpl; try econstructor.
destruct (zle_le 0 (Int.unsigned n2) Int.max_unsigned); intros; simpl; try econstructor.
destruct (pg (update init_shared_adt
(LEvent z (LogPrim proc_create (Lint n1 :: Lptr b ofs :: Lint n2 :: nil)
current_thread dprocSnap) :: l))); intros; simpl; try econstructor.
destruct (init (update init_shared_adt
(LEvent z (LogPrim proc_create (Lint n1 :: Lptr b ofs :: Lint n2 :: nil)
current_thread dprocSnap) :: l))); intros; simpl; try econstructor.
Qed.
Section INV_AUX_LEMMAS.
Opaque update.
Lemma pg_true_implies_nps:
∀ lst, pg (update init_shared_adt lst) = true →
262144 ≤ nps (update init_shared_adt lst) ≤ 1048576.
Proof.
induction lst; simpl; intros.
+ simpl in H; inv H.
+ simpl in H.
Transparent update.
simpl in H.
case_eq (apply_event a (update init_shared_adt lst)); intros; subst.
× rewrite H0 in H.
unfold apply_event in H0; simpl.
case_eq a; intros; subst.
destruct l.
{ subdestruct; inv H0; simpl; eauto.
inv H; rewrite Hdestruct; simpl; auto. }
{ subdestruct; inv H0; simpl; eauto.
inv H; rewrite Hdestruct; simpl; auto. }
{ subdestruct; try (inv H0; fail); subst.
- rewrite Hdestruct.
unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in ×.
subdestruct; inv H0; simpl; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in ×.
subdestruct; inv H0; simpl in ×.
apply real_nps_range.
- rewrite Hdestruct.
unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in ×.
subdestruct; inv Hdestruct9; simpl in *; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in ×.
subdestruct; inv Hdestruct6; simpl in *; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in ×.
subdestruct; inv Hdestruct6; simpl in *; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct10; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct15; inv H0; simpl in *; eauto.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12.
subdestruct; inv Hdestruct12; simpl in *; eauto.
inv Hdestruct12; simpl in *; auto.
- rewrite Hdestruct.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct16; inv H0; simpl in *; eauto;
try (inv Hdestruct13; simpl in *; simpl in *; eauto).
- rewrite Hdestruct.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct12; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct11; inv H0; simpl in *; eauto.
- rewrite Hdestruct.
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4.
subdestruct; inv Hdestruct4; inv H0; simpl in *; eauto. }
{ inv H0; eapply IHlst; eauto. }
× rewrite H0 in H.
simpl.
rewrite H0.
eapply IHlst in H; eauto.
Qed.
Lemma ipt_false_implies_pg_true:
∀ tid lst,
ipt (thread_init_dproc tid) = false →
pg (update init_shared_adt lst) = true.
Proof.
intro tid.
induction lst; simpl in *; intros.
- unfold thread_init_dproc in H; simpl.
unfold thread_init_dproc_aux in H.
destruct (zeq tid main_thread); subst.
+ destruct init_log; simpl in *; inv H.
+ case_eq (thread_init_dproc_iter tid init_log); intros; simpl.
× unfold thread_init_dproc in H; simpl.
exploit thread_init_dproc_iter_preserve_fields; eauto; intros H1; blast H1.
rewrite H0 in H; rewrite H18 in H; inv H.
× rewrite H0 in H; simpl in H; inv H.
- case_eq (apply_event a (update init_shared_adt lst)); intros; subst.
+ unfold apply_event in H0; simpl.
case_eq a; intros; subst.
destruct l.
{ subdestruct; inv H0; simpl; eauto. }
{ subdestruct; inv H0; simpl; eauto. }
{ subdestruct; try (inv H0; fail); subst.
- unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in ×.
subdestruct; inv H0; simpl; eauto.
- unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in ×.
subdestruct; inv H0; simpl in ×.
reflexivity.
- unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in ×.
subdestruct; inv Hdestruct9; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in ×.
subdestruct; inv Hdestruct6; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in ×.
subdestruct; inv Hdestruct6; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct10; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct15; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct16; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct12; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct11; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4.
subdestruct; inv Hdestruct4; inv H0; simpl in *; eauto. }
{ inv H0; eapply IHlst; eauto. }
+ eapply IHlst.
auto.
Qed.
Lemma ipt_true_implies_ikern_true:
∀ tid, ipt (thread_init_dproc tid) = true → ikern (thread_init_dproc tid) = true.
Proof.
intros.
unfold thread_init_dproc in *; unfold thread_init_dproc_aux in *; simpl in ×.
case_eq (zeq tid main_thread).
- intros; subst; repeat rewrite zeq_true in *; destruct init_log; auto.
- intros; rewrite zeq_false in *; trivial.
rewrite zeq_false in *; trivial.
case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
+ rewrite H1 in H; auto.
Qed.
Lemma ikern_false_implies_ipt_false:
∀ tid, ikern (thread_init_dproc tid) = false → ipt (thread_init_dproc tid) = false.
Proof.
intros.
unfold thread_init_dproc in *; unfold thread_init_dproc_aux in *; simpl in ×.
case_eq (zeq tid main_thread).
- intros; subst; repeat rewrite zeq_true in *; destruct init_log; auto.
- intros; rewrite zeq_false in *; trivial.
rewrite zeq_false in *; trivial.
case_eq (thread_init_dproc_iter tid init_log); intros.
+ rewrite H1 in H.
exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
simpl in H2.
rewrite H in H2; inv H2.
+ rewrite H1 in H; auto.
Qed.
Lemma ihost_false_implies_pg_true_and_ikern_true:
∀ tid, ihost (thread_init_dproc tid) = false →
pg (update init_shared_adt init_log) = true ∧ ikern (thread_init_dproc tid) = true.
Proof.
intros.
unfold thread_init_dproc in H.
unfold thread_init_dproc_aux in H.
case_eq (zeq tid main_thread); intros; subst.
- repeat rewrite zeq_true in H; simpl; destruct init_log; simpl in H; inv H.
- rewrite zeq_false in H; rewrite zeq_false in H; auto.
case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2.
rewrite H1 in H.
rewrite H4 in H; simpl in H; inv H.
+ rewrite H1 in H; simpl in H; inv H.
Qed.
Lemma thread_container_inv:
∀ tid lst,
INVLemmaThreadContainer.Thread_Container_valid
(ZMap.set
(ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))
(AC (thread_init_dproc tid)) (ZMap.init Container_unused)).
Proof.
generalize max_unsigned_val; intros muval; intros.
case_eq (zeq tid main_thread); intros; subst.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
repeat rewrite zeq_true.
assert (match
match init_log with
| nil ⇒ Some main_init_dproc
| _ :: _ ⇒ None
end
with
| Some init_dproc_val ⇒ init_dproc_val
| None ⇒ main_init_dproc
end = main_init_dproc).
{ destruct init_log; simpl; reflexivity. }
rewrite H0; clear H0.
constructor; simpl; intros.
+ case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros.
× subst; rewrite ZMap.gss in H0; simpl in H0; inv H0.
× rewrite ZMap.gso in H0; auto.
rewrite ZMap.gi in H0; simpl in H0; inv H0.
+ case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros.
× subst; rewrite ZMap.gss; simpl; omega.
× subst; rewrite ZMap.gso; auto; rewrite ZMap.gi; simpl; omega.
+ case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros.
× subst; rewrite ZMap.gss; simpl; omega.
× subst; rewrite ZMap.gso; auto; rewrite ZMap.gi; simpl; omega.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; auto.
rewrite zeq_false; auto.
case_eq (thread_init_dproc_iter tid init_log); intros.
+ induction init_log; simpl; [simpl in H0; inv H0 | ].
simpl in H0.
destruct a.
destruct l0.
× generalize (IHl H0); intros IHl´.
clear IHl.
set (curid := (ZMap.get (CPU_ID (update init_shared_adt lst)) (cid (update init_shared_adt lst)))).
fold curid in IHl´; inv IHl´.
econstructor; simpl in *; intros; case_eq (zeq i curid); intros; subst; simpl in *; subst; auto.
× generalize (IHl H0); intros IHl´.
clear IHl.
set (curid := (ZMap.get (CPU_ID (update init_shared_adt lst)) (cid (update init_shared_adt lst)))).
fold curid in IHl´; inv IHl´.
econstructor; simpl in *; intros; case_eq (zeq i curid); intros; subst; simpl in *; subst; auto.
× case_eq (apply_event (LEvent z (LogPrim id args choice dprocSnap)) (update init_shared_adt l)); intros;
rewrite H1 in H0.
{ case_eq (peq id proc_create); intros; [ subst; rewrite peq_true in H0 | rewrite peq_false in H0; auto].
case_eq (zeq tid choice); intros; [ subst; rewrite zeq_true in H0 | rewrite zeq_false in H0; auto].
repeat (destruct args; try (inversion H0; fail); destruct l0; try (inversion H0; fail)).
destruct args; [ | inversion H0].
case_eq (zle_lt (z × 8 + 1) choice (z × 8 + 1 + 8)); intros; rewrite H4 in H0; [ | inv H0].
case_eq (zlt_lt 8 choice 1024); intros; rewrite H5 in H0; [ | inv H0].
case_eq (zle_le 0 (Int.unsigned n1) Int.max_unsigned); intros; rewrite H6 in H0; [ | inv H0].
case_eq (pg d0); intros; rewrite H7 in H0; [ | inv H0].
case_eq (init d0); intros; rewrite H8 in H0; [ | inv H0].
unfold cal_init_dproc in H0.
clear IHl.
inv H0.
econstructor.
- intros; case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; subst.
+
inv s_threads_prf.
generalize (all_cid_in_full_thread_list lst); intros.
unfold proc_id, uRData in H10; simpl in H10.
generalize (valid_thread_list (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; simpl in H11.
eapply H11 in H10; omega.
+ rewrite ZMap.gso in H0; auto; rewrite ZMap.gi in H0; simpl in H0; inv H0.
- intros; case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; subst.
+ rewrite ZMap.gss; simpl; omega.
+ rewrite ZMap.gso; simpl; auto; rewrite ZMap.gi; simpl; omega.
- intros; case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; subst.
+ rewrite ZMap.gss; simpl; omega.
+ rewrite ZMap.gso; simpl; auto; rewrite ZMap.gi; simpl; omega. }
{ case_eq (peq id proc_create); intros; [ subst; rewrite peq_true in H0 | rewrite peq_false in H0; auto].
case_eq (zeq tid choice); intros; [ subst; rewrite zeq_true in H0 | rewrite zeq_false in H0; auto].
repeat (destruct args; try (inversion H0; fail); destruct l0; try (inversion H0; fail)).
destruct args; [ | inversion H0].
case_eq (zle_lt (z × 8 + 1) choice (z × 8 + 1 + 8)); intros; rewrite H4 in H0; [ | inv H0].
case_eq (zlt_lt 8 choice 1024); intros; rewrite H5 in H0; [ | inv H0].
case_eq (zle_le 0 (Int.unsigned n1) Int.max_unsigned); intros; rewrite H6 in H0; [ | inv H0].
case_eq (pg (update init_shared_adt l)); intros; rewrite H7 in H0; [ | inv H0].
case_eq (init (update init_shared_adt l)); intros; rewrite H8 in H0; [ | inv H0].
unfold cal_init_dproc in H0.
clear IHl.
inv H0.
econstructor.
- intros; case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; subst.
+
inv s_threads_prf.
generalize (all_cid_in_full_thread_list lst); intros.
unfold proc_id, uRData in H10; simpl in H10.
generalize (valid_thread_list (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; simpl in H11.
eapply H11 in H10; omega.
+ rewrite ZMap.gso in H0; auto; rewrite ZMap.gi in H0; simpl in H0; inv H0.
- intros; case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; subst.
+ rewrite ZMap.gss; simpl; omega.
+ rewrite ZMap.gso; simpl; auto; rewrite ZMap.gi; simpl; omega.
- intros; case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros; subst.
+ rewrite ZMap.gss; simpl; omega.
+ rewrite ZMap.gso; simpl; auto; rewrite ZMap.gi; simpl; omega. }
× generalize (IHl H0); intros IHl´.
clear IHl.
set (curid := (ZMap.get (CPU_ID (update init_shared_adt lst)) (cid (update init_shared_adt lst)))).
fold curid in IHl´; inv IHl´.
econstructor; simpl in *; intros; case_eq (zeq i curid); intros; subst; simpl in *; subst; auto.
+ constructor; simpl; intros.
× case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros.
{ subst; rewrite ZMap.gss in H1; simpl in H1; inv H1. }
{ rewrite ZMap.gso in H1; auto.
rewrite ZMap.gi in H1; simpl in H1; inv H1. }
× case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros.
{ subst; rewrite ZMap.gss; simpl; omega. }
{ subst; rewrite ZMap.gso; auto; rewrite ZMap.gi; simpl; omega. }
× case_eq (zeq i (ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)))); intros.
{ subst; rewrite ZMap.gss; simpl; omega. }
{ subst; rewrite ZMap.gso; auto; rewrite ZMap.gi; simpl; omega. }
Qed.
Lemma thread_init_dproc_pperm_val:
∀ tid, pperm (thread_init_dproc tid) = ZMap.init PGUndef.
Proof.
intros; unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; simpl.
- destruct init_log; simpl; auto.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
+ simpl; auto.
Qed.
Lemma pg_false_implies_pperm_default:
∀ tid lst, pg (update init_shared_adt lst) = false → pperm (thread_init_dproc tid) = ZMap.init PGUndef.
Proof.
intros; unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; simpl.
- destruct init_log; simpl; auto.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
+ simpl; auto.
Qed.
Lemma pg_true_implies_PMap_valid:
∀ i,
pg (update init_shared_adt init_log) = true →
0 ≤ i < num_proc → PMap_valid (ZMap.get i (ptpool (thread_init_dproc current_thread))).
Proof.
intros.
case_eq (zeq current_thread main_thread); intros.
- subst.
assert (init_log = nil) by (inv s_oracle_basic_prop_prf; eauto).
rewrite H2 in H.
simpl in H; inv H.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
+ case_eq (thread_init_dproc_iter current_thread init_log); intros.
× exploit thread_init_dproc_iter_preserve_fields; eauto; intros.
blast H3; rewrite H18; eapply CalRealPT.real_pt_PMap_valid; eauto.
× eapply CalRealPT.real_pt_PMap_valid; eauto.
Qed.
Lemma pg_true_ipt_true_implies_PT_val:
pg (update init_shared_adt init_log) = true →
ipt (thread_init_dproc current_thread) = true → PT (thread_init_dproc current_thread) = 0.
Proof.
case_eq (zeq current_thread main_thread); intros.
- subst.
assert (init_log = nil) by (inv s_oracle_basic_prop_prf; eauto).
rewrite H2 in H0.
simpl in H0; inv H0.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
+ case_eq (thread_init_dproc_iter current_thread init_log); intros.
× exploit thread_init_dproc_iter_preserve_fields; eauto; intros H3; blast H3; auto.
× simpl; reflexivity.
Qed.
Lemma pg_true_PMap_kern:
pg (update init_shared_adt init_log) = true →
PMap_kern (ZMap.get 0 (ptpool (thread_init_dproc current_thread))).
Proof.
case_eq (zeq current_thread main_thread); intros.
- subst.
assert (init_log = nil) by (inv s_oracle_basic_prop_prf; eauto).
rewrite H1 in H0.
simpl in H0; inv H0.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
+ case_eq (thread_init_dproc_iter current_thread init_log); intros.
× exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
rewrite H17; rewrite H15; apply CalRealPT.real_pt_PMap_kern; eauto.
× simpl; apply CalRealPT.real_pt_PMap_kern; eauto.
Qed.
Lemma pg_true_PT_in_range:
pg (update init_shared_adt init_log) = true →
0 ≤ PT (thread_init_dproc current_thread) < 1024.
Proof.
case_eq (zeq current_thread main_thread); intros.
- subst.
assert (init_log = nil) by (inv s_oracle_basic_prop_prf; eauto).
rewrite H1 in H0.
simpl in H0; inv H0.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
+ case_eq (thread_init_dproc_iter current_thread init_log); intros.
× exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto; omega.
× simpl; omega.
Qed.
Lemma dirty_ppage_preserve:
∀ tid, dirty_ppage (pperm (thread_init_dproc tid)) (HP (thread_init_dproc tid)).
Proof.
intros.
intros; unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; simpl; subst.
- destruct init_log; simpl; eapply dirty_ppage_init.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
rewrite H10; rewrite H12; eapply dirty_ppage_init.
+ simpl; eapply dirty_ppage_init.
Qed.
Lemma dirty_ppage´_preserve:
∀ tid, dirty_ppage´ (pperm (thread_init_dproc tid)) (HP (thread_init_dproc tid)).
Proof.
intros.
intros; unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; simpl; subst.
- destruct init_log; simpl; eapply dirty_ppage´_init.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
rewrite H10; rewrite H12; eapply dirty_ppage´_init.
+ simpl; eapply dirty_ppage´_init.
Qed.
Lemma pg_true_implies_IDPDE_init_real:
∀ lst,
pg (update init_shared_adt lst) = true →
IDPDE_init (idpde (update init_shared_adt lst)).
Proof.
induction lst; simpl in *; intros.
- inv H.
- case_eq (apply_event a (update init_shared_adt lst)); simpl; intros.
+ rewrite H0 in H.
unfold apply_event in H0.
simpl.
case_eq a; intros; subst.
destruct l.
{ subdestruct; inv H0; simpl; eauto. }
{ subdestruct; inv H0; simpl; eauto. }
{ subdestruct; try (inv H0; fail); subst.
- unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in ×.
subdestruct; inv H0; simpl; eauto.
- unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in ×.
subdestruct; inv H0; simpl in ×.
apply CalRealIDPDE.real_idpde_init.
- unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in ×.
subdestruct; inv Hdestruct9; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in ×.
subdestruct; inv Hdestruct6; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in ×.
subdestruct; inv Hdestruct6; simpl in *; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct10; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct15; inv Hdestruct12; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct16; inv Hdestruct13; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct12; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in ×.
subdestruct; inv Hdestruct11; inv H0; simpl in *; eauto.
- unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4.
subdestruct; inv Hdestruct4; inv H0; simpl in *; eauto. }
{ inv H0; eapply IHlst; eauto. }
+ rewrite H0 in H; auto.
Qed.
Lemma cons_rpos_range:
∀ tid, 0 ≤ rpos (console (thread_init_dproc tid)) < 512.
intros.
intros; unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; simpl; subst.
- destruct init_log; simpl; omega.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
rewrite H34; simpl; omega.
+ simpl; omega.
Qed.
Lemma cons_buf_console_range:
∀ tid, 0 ≤ Zlength (cons_buf (console (thread_init_dproc tid))) < 512.
Proof.
intros.
intros; unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; simpl; subst.
- Transparent Zlength.
unfold Zlength.
destruct init_log; simpl; omega.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2; auto.
rewrite H34; simpl.
unfold Zlength; simpl; omega.
+ simpl; auto.
unfold Zlength; simpl; omega.
Qed.
Lemma CPU_ID_in_range:
∀ lst, 0 ≤ (CPU_ID (update init_shared_adt lst)) < TOTAL_CPU.
Proof.
inv s_threads_prf.
inv s_oracle_basic_prop_prf.
induction lst; intros; subst.
- simpl.
rewrite <- current_CPU_IDs_eq_prop0.
omega.
- simpl.
case_eq (apply_event a (update init_shared_adt lst)); intros; subst; try auto.
unfold apply_event in H.
destruct a.
destruct l.
+ subdestruct; inv H; auto.
+ subdestruct; inv H; auto.
+ subdestruct.
× unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H; subdestruct; inv H; auto.
× unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H; subdestruct; inv H; auto.
× unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in Hdestruct9; simpl in *; subdestruct; inv H;
inv Hdestruct9; auto.
× unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in Hdestruct6;
subdestruct; inv H; inv Hdestruct6; simpl in *; auto.
× unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H; simpl in *; eauto.
× unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in Hdestruct6;
subdestruct; inv H; inv Hdestruct6; simpl in *; auto.
× unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct10; subdestruct; inv H;
inv Hdestruct10; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in *; subdestruct;
inv Hdestruct12; inv Hdestruct15; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in *; subdestruct;
inv Hdestruct13; inv Hdestruct16; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12; subdestruct;
inv Hdestruct12; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct11; subdestruct;
inv Hdestruct11; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4; subdestruct;
inv Hdestruct4; inv H; simpl in *; auto.
+ inv H; assumption.
Qed.
Lemma cid_in_range:
∀ lst, 0 ≤ ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)) < 1024.
Proof.
inv s_threads_prf.
induction lst; intros; subst.
- simpl.
unfold init_real_cidpool.
simpl.
case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; [rewrite e; rewrite ZMap.gss; omega | rewrite ZMap.gso; auto].
rewrite ZMap.gi; omega.
- simpl.
case_eq (apply_event a (update init_shared_adt lst)); intros; subst; try auto.
unfold apply_event in H.
destruct a.
destruct l.
+ subdestruct.
inv H; simpl; rewrite ZMap.gss; eauto.
+ subdestruct.
inv H; simpl; rewrite ZMap.gss; eauto.
+ subdestruct.
× unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H; subdestruct; inv H; auto.
× unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H; subdestruct; inv H; simpl.
rewrite ZMap.gss.
rewrite main_thread_val.
omega.
× unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in Hdestruct9; simpl in *; subdestruct; inv H;
inv Hdestruct9; auto.
× unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in Hdestruct6;
subdestruct; inv H; inv Hdestruct6; simpl in *; auto.
× unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H; simpl in *; eauto.
× unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in Hdestruct6;
subdestruct; inv H; inv Hdestruct6; simpl in *; auto.
× unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct10; subdestruct; inv H;
inv Hdestruct10; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in *; subdestruct;
inv Hdestruct12; inv Hdestruct15; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in *; subdestruct;
inv Hdestruct13; inv Hdestruct16; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12; subdestruct;
inv Hdestruct12; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct11; subdestruct;
inv Hdestruct11; inv H; simpl in *; auto.
× subst; unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4; subdestruct;
inv Hdestruct4; inv H; simpl in *; auto.
+ inv H; assumption.
Qed.
Lemma ikern_false_PT_cid:
∀ tid lst, ikern (thread_init_dproc tid) = false →
PT (thread_init_dproc tid)
= ZMap.get (CPU_ID (update init_shared_adt lst))
(cid (update init_shared_adt lst)).
Proof.
intros.
unfold thread_init_dproc in H.
unfold thread_init_dproc_aux in H.
case_eq (zeq tid main_thread); intros; subst.
- repeat rewrite zeq_true in ×.
destruct init_log; simpl in H; inv H.
- rewrite zeq_false in H; auto.
rewrite zeq_false in H; auto.
case_eq (thread_init_dproc_iter tid init_log); intros.
+ rewrite H1 in H.
exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2.
rewrite H2 in H.
simpl in H; inv H.
+ rewrite H1 in H.
simpl in H; inv H.
Qed.
Lemma ikern_eq_ipt:
∀ tid, ikern (thread_init_dproc tid) = ipt (thread_init_dproc tid).
Proof.
intros.
unfold thread_init_dproc; unfold thread_init_dproc_aux.
case_eq (zeq tid main_thread); intros; subst.
- destruct init_log; simpl; reflexivity.
- case_eq (thread_init_dproc_iter tid init_log); intros.
+ exploit thread_init_dproc_iter_preserve_fields; eauto; intros H1; blast H1.
rewrite H6, H18; reflexivity.
+ simpl; reflexivity.
Qed.
Lemma ikern_false_implies_pg_true:
∀ tid lst, ikern (thread_init_dproc tid) = false →
pg (update init_shared_adt lst) = true.
Proof.
intros.
unfold thread_init_dproc in H.
unfold thread_init_dproc_aux in H.
case_eq (zeq tid main_thread); intros; subst.
- repeat rewrite zeq_true in ×.
destruct init_log; simpl in H; inv H.
- rewrite zeq_false in H; auto.
rewrite zeq_false in H; auto.
case_eq (thread_init_dproc_iter tid init_log); intros.
+ rewrite H1 in H.
exploit thread_init_dproc_iter_preserve_fields; eauto; intros H2; blast H2.
rewrite H7 in H; simpl in H; inv H.
+ rewrite H1 in H; simpl in H; inv H.
Qed.
Lemma pg_true_ikern_true_implies_PT_val:
pg (update init_shared_adt init_log) = true →
ikern (thread_init_dproc current_thread) = true → PT (thread_init_dproc current_thread) = 0.
Proof.
case_eq (zeq current_thread main_thread); intros.
- subst.
assert (init_log = nil) by (inv s_oracle_basic_prop_prf; eauto).
rewrite H2 in H0.
simpl in H0; inv H0.
- unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
+ case_eq (thread_init_dproc_iter current_thread init_log); intros.
× exploit thread_init_dproc_iter_preserve_fields; eauto; intros H3; blast H3; auto.
× simpl; reflexivity.
Qed.
Lemma init_true_vmx_info_real:
∀ lst,
init (update init_shared_adt lst) = true →
vmxinfo (update init_shared_adt lst) = real_vmxinfo.
Proof.
induction lst; intros; simpl in ×.
- inv H.
- case_eq (apply_event a (update init_shared_adt lst)); intros.
+ rewrite H0 in H.
unfold apply_event in H0.
destruct a.
destruct l.
× subdestruct; inv H0; simpl in *; apply IHlst; auto.
× subdestruct; inv H0; simpl in *; apply IHlst; auto.
× subdestruct.
{ unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H0; subdestruct; inv H0; simpl in *;
apply IHlst; auto. }
{ unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H0; subdestruct; inv H0; simpl in *;
reflexivity. }
{ unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in Hdestruct9; subdestruct; inv Hdestruct9;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in Hdestruct6; subdestruct; inv Hdestruct6;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H0; simpl in *; eauto. }
{ unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in Hdestruct6; subdestruct; inv Hdestruct6;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct10; subdestruct; inv Hdestruct10;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12;
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct15;
subdestruct; inv Hdestruct12; inv Hdestruct15;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct13;
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct16;
subdestruct; inv Hdestruct13; inv Hdestruct16;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12; subdestruct; inv Hdestruct12;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct11; subdestruct; inv Hdestruct11;
inv H0; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4; subdestruct; inv Hdestruct4;
inv H0; simpl in *; apply IHlst; auto. }
× inv H0; apply IHlst; auto.
+ rewrite H0 in H.
apply IHlst; auto.
Qed.
Lemma big_oracle_unchange :
∀ lst,
big_oracle (update init_shared_adt lst) = big_oracle init_shared_adt.
Proof.
intros.
induction lst.
- simpl; auto.
- case_eq (apply_event a (update init_shared_adt lst)); intros; simpl.
+ rewrite H.
unfold apply_event in H.
destruct a.
destruct l.
× subdestruct; inv H; simpl in *; auto.
× subdestruct; inv H; simpl in *; auto.
× subdestruct.
{ unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H; subdestruct; inv H; simpl in *;
apply IHlst; auto. }
{ unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H; subdestruct; inv H; simpl in *;
apply IHlst; auto. }
{ unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in Hdestruct9; subdestruct; inv Hdestruct9;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in Hdestruct6; subdestruct; inv Hdestruct6;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H; simpl in *; eauto. }
{ unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in Hdestruct6; subdestruct; inv Hdestruct6;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct10; subdestruct; inv Hdestruct10;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12;
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct15;
subdestruct; inv Hdestruct12; inv Hdestruct15;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct13;
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct16;
subdestruct; inv Hdestruct13; inv Hdestruct16;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12; subdestruct; inv Hdestruct12;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct11; subdestruct; inv Hdestruct11;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4; subdestruct; inv Hdestruct4;
inv H; simpl in *; apply IHlst; auto. }
× inv H; apply IHlst; auto.
+ rewrite H; auto.
Qed.
Lemma CPU_ID_unchange :
∀ lst,
CPU_ID (update init_shared_adt lst) = CPU_ID init_shared_adt.
Proof.
intros.
induction lst.
- simpl; auto.
- case_eq (apply_event a (update init_shared_adt lst)); intros; simpl.
+ rewrite H.
unfold apply_event in H.
destruct a.
destruct l.
× subdestruct; inv H; simpl in *; auto.
× subdestruct; inv H; simpl in *; auto.
× subdestruct.
{ unfold ObjPHBThreadIPC.single_big_release_lock_SC_spec_share in H; subdestruct; inv H; simpl in *;
apply IHlst; auto. }
{ unfold ObjPHBThreadSCHED.single_big_sched_init_spec_share in H; subdestruct; inv H; simpl in *;
apply IHlst; auto. }
{ unfold ObjPHBThreadSCHED.single_big_proc_create_spec_share in Hdestruct9; subdestruct; inv Hdestruct9;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadIPC.single_big_acquire_lock_SC_spec_share in Hdestruct6; subdestruct; inv Hdestruct6;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadIPC.single_big_ipc_send_body_spec in ×.
unfold ObjPHBThreadIPC.single_big_page_copy_spec in ×.
subdestruct; inv Hdestruct11; simpl in *; inv H; simpl in *; eauto. }
{ unfold ObjPHBThreadSCHED.single_big_thread_wakeup_spec_share in Hdestruct6; subdestruct; inv Hdestruct6;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct10; subdestruct; inv Hdestruct10;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12;
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct15;
subdestruct; inv Hdestruct12; inv Hdestruct15;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct13;
unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct16;
subdestruct; inv Hdestruct13; inv Hdestruct16;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct12; subdestruct; inv Hdestruct12;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct11; subdestruct; inv Hdestruct11;
inv H; simpl in *; apply IHlst; auto. }
{ unfold ObjPHBThreadVMM.single_big_palloc_spec_share in Hdestruct4; subdestruct; inv Hdestruct4;
inv H; simpl in *; apply IHlst; auto. }
× inv H; apply IHlst; auto.
+ rewrite H; auto.
Qed.
End INV_AUX_LEMMAS.
Next Obligation.
simpl; econstructor; simpl.
-
eauto using pg_true_implies_nps.
-
eauto using ikern_false_implies_pg_true.
-
eauto using ipt_true_implies_ikern_true.
-
eauto using ikern_false_implies_ipt_false.
-
eauto using ihost_false_implies_pg_true_and_ikern_true.
-
eauto using thread_container_inv.
-
eauto using pg_false_implies_pperm_default.
-
eauto using pg_true_implies_PMap_valid.
-
eauto using pg_true_ikern_true_implies_PT_val.
-
eauto using pg_true_PMap_kern.
-
eauto using pg_true_PT_in_range.
-
eauto using dirty_ppage´_preserve.
-
eauto using pg_true_implies_IDPDE_init_real.
-
eauto using ikern_false_PT_cid.
-
eauto using ikern_eq_ipt.
-
eauto using cons_rpos_range.
-
eauto using cons_buf_console_range.
-
eauto using CPU_ID_in_range.
-
eauto using cid_in_range.
Qed.
Next Obligation.
simpl; econstructor; simpl.
-
eauto using pg_true_implies_nps.
-
eauto using ikern_false_implies_pg_true.
-
eauto using ipt_true_implies_ikern_true.
-
eauto using ikern_false_implies_ipt_false.
-
eauto using ihost_false_implies_pg_true_and_ikern_true.
-
eauto using thread_container_inv.
-
eauto using pg_false_implies_pperm_default.
-
eauto using pg_true_implies_PMap_valid.
-
eauto using pg_true_ikern_true_implies_PT_val.
-
eauto using pg_true_PMap_kern.
-
eauto using pg_true_PT_in_range.
-
eauto using dirty_ppage´_preserve.
-
eauto using pg_true_implies_IDPDE_init_real.
-
eauto using ikern_false_PT_cid.
-
eauto using ikern_eq_ipt.
-
eauto using cons_rpos_range.
-
eauto using cons_buf_console_range.
-
eauto using CPU_ID_in_range.
-
eauto using cid_in_range.
Qed.
Next Obligation.
unfold symbol_offset.
simpl in ×.
unfold prim_thread_init_pc in H.
subdestruct.
inv H.
∃ START_USER_FUN_LOC, Int.zero.
rewrite Hdestruct0.
reflexivity.
Qed.
Next Obligation.
unfold prim_thread_init_pc in ×.
case_eq (peq f proc_create); intros; try reflexivity.
assert (Genv.find_symbol ge1 START_USER_FUN_LOC = Genv.find_symbol ge2 START_USER_FUN_LOC) by eauto using H.
rewrite H1.
case_eq (Genv.find_symbol ge2 START_USER_FUN_LOC); intros; try reflexivity.
Qed.
End SINGLE_ORACLE_PROP_INSTANCE.
End SINGLEORACLEPROPDEF.
Section SINGLECONFIGURATIONINSTANCE.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)}.
Context `{Hmem: Mem.MemoryModelX}.
Program Instance s_config : SingleConfiguration (spl_data := AuxSingleAbstractDataType.single_data)
mem (spl_mem_ops := memory_model_ops) :=
{
spl_threads_ops := s_threads_ops;
spl_oracle_ops := s_oracle_ops;
spl_oracle_prf := s_oracle_prf;
spl_threads_prf := s_threads_prf;
spl_oracle_prf_prop := s_oracle_prop_prf;
spl_mem_prf := Hmem;
spl_algebraic_mem := algebraicmem
}.
End SINGLECONFIGURATIONINSTANCE.
Section SINGLEBASICLINKPROPDEF.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params_ops: RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Class SingleOracleBasicLinkProp `{single_oracle_prf : SingleOracle}
`{s_threads_ops: ThreadsConfigurationOps} :=
{
oracle_le_nb_prop: ∀ l, (last_nb l ≤ last_nb (Single_Oracle l :: l)) % positive;
oracle_event_yield_back_prop: ∀ l, lastEvType l = Some LogYieldTy → ∃ i, Single_Oracle l = LEvent i LogYieldBack;
oracle_init_log_prop: ∀ (l´: Log) (e: LogEvent) (lg: Log), init_log = l´ ++ (e :: lg) → Single_Oracle lg = e;
init_log_structure_prop: init_log = nil ∨
∃ l e, init_log = LEvent (proc_id (uRData l)) LogYieldBack :: l ∧
proc_id (uRData l) ≠ proc_id (uRData nil) ∧
last_op l = Some e ∧ getLogEventNB e ≠ None ∧
∀ e l1 l2, l = l1 ++ e :: l2 →proc_id (uRData l2) ≠ proc_id (uRData init_log)
}.
End SINGLEBASICLINKPROPDEF.
Section SINGLE_ORACLE_LINK_PROP_INSTANCE.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params_ops: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Program Instance s_oracle_link_prop_prf : SingleOracleLinkProp (thread_conf_prf := s_threads_prf) := { }.
Next Obligation. inv s_oracle_basic_link_prop_prf; eauto. Qed.
Next Obligation. inv s_oracle_basic_link_prop_prf; eauto. Qed.
Next Obligation. inv s_oracle_basic_link_prop_prf; eauto. Qed.
Next Obligation. inv s_oracle_basic_link_prop_prf; eauto. Qed.
End SINGLE_ORACLE_LINK_PROP_INSTANCE.
Section SINGLELINKCONFIGURATIONINSTANCE.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)}.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)}.
Context `{Hmem: Mem.MemoryModelX}.
Program Instance s_link_config : SingleLinkConfiguration (spl_data := AuxSingleAbstractDataType.single_data)
mem (spl_mem_ops := memory_model_ops) :=
{
spl_conf_prf := s_config;
spl_oracle_link_prf_prop := s_oracle_link_prop_prf
}.
End SINGLELINKCONFIGURATIONINSTANCE.
End SINGLEORACLEINSTANCE.