Library mcertikos.multithread.phbthread.ObjPHBThreadReplayFunction
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Integers.
Require Import Values.
Require Import ASTExtra.
Require Import Constant.
Require Import Constant.
Require Import GlobIdent.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import RealParams.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import ObjInterruptDriver.
Require Import ObjConsole.
Require Import OracleInstances.
Require Import ObjSerialDriver.
Require Import ObjVMMDef.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import AuxSingleAbstractDataType.
Require Import ObjPHBFlatMem.
Require Import ObjPHBThreadVMM.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadSCHED.
Require Import AlgebraicMem.
Require Import GlobalOracleProp.
Require Import SingleConfiguration.
Require Import BigLogThreadConfigFunction.
Definition has_event (name : ident) :=
if peq name palloc then true else
if peq name pt_resv then true else
if peq name proc_create then true else
if peq name thread_wakeup then true else
if peq name sched_init then true else
if peq name acquire_lock_CHAN then true else
if peq name release_lock_CHAN then true else
if peq name ipc_send_body then true else false.
Notation palloc_num := 1%Z.
Notation pt_resv_num := 2%Z.
Notation proc_create_num := 3%Z.
Notation thread_wakeup_num := 4%Z.
Notation sched_init_num := 5%Z.
Notation acquire_lock_CHAN_num := 6%Z.
Notation release_lock_CHAN_num := 7%Z.
Notation ipc_send_body_num := 8%Z.
Definition prim_id_num (name : positive) : Z :=
if peq name palloc then palloc_num else
if peq name pt_resv then pt_resv_num else
if peq name proc_create then proc_create_num else
if peq name thread_wakeup then thread_wakeup_num else
if peq name sched_init then sched_init_num else
if peq name acquire_lock_CHAN then acquire_lock_CHAN_num else
if peq name release_lock_CHAN then release_lock_CHAN_num else
if peq name ipc_send_body then ipc_send_body_num else 0.
Section PHBSPECSReplay.
Context `{real_param_ops : RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{threads_conf_ops: ThreadsConfigurationOps}.
Lemma In_dec_in_implies_In:
∀ tid lst,
match (In_dec zeq) tid lst with
| left _ ⇒ In tid lst
| right _ ⇒ ¬In tid lst
end.
Proof.
induction lst; intros.
- simpl; intro contra; inv contra.
- simpl.
case_eq (zeq a tid); intros.
subst.
+ left; auto.
+ destruct (in_dec zeq tid lst).
× right; auto.
× intro contra.
destruct contra; [elim n | elim IHlst]; auto.
Qed.
Definition option_z_check (tid : option Z) : bool :=
match tid with
| Some tid´ ⇒ (In_dec zeq) tid´ full_thread_list
| _ ⇒ false
end.
Definition z_check (tid : Z) : bool :=
(In_dec zeq) tid full_thread_list.
Section CHOICE_CHECK.
Definition choice_check (name : ident) (largs : list lval) (sd: sharedData) (pd: privData) : Z :=
match prim_id_num name with
| palloc_num ⇒
match largs with
| (Lint n)::nil ⇒ single_big_palloc_spec_test (Int.unsigned n) (sd, pd)
| _ ⇒ 42
end
| pt_resv_num ⇒
match largs with
| (Lint n)::(Lint vadr)::(Lint perm)::nil ⇒ single_big_ptResv_spec_test (Int.unsigned n)
(Int.unsigned vadr)
(Int.unsigned perm) (sd, pd)
| _ ⇒ 42
end
| proc_create_num ⇒
match largs with
| (Lint elf_id)::(Lptr buc uc_ofs)::(Lint q)::nil ⇒ single_big_proc_create_spec_test
(sd, pd) buc uc_ofs (Int.unsigned q)
| _ ⇒ 0
end
| _ ⇒ 42
end.
End CHOICE_CHECK.
Section SYNCCHPOOL_CHECK.
Definition sync_chpool_check (name : ident) (largs : list lval) (sd: sharedData) (pd: privData) : option SyncChanPool :=
if peq name thread_sleep then
match largs with
| (Lint cv)::nil ⇒ Some (syncchpool pd)
| _ ⇒ None
end
else None.
End SYNCCHPOOL_CHECK.
Section SNAPFUNCDEF.
Definition snap_func (pd : privData) : privDataSnap :=
{|
tiSnap := ti pd;
ikernSnap := ikern pd;
ihostSnap := ihost pd;
HPSnap := HP pd;
ACSnap := AC pd;
uctxtSnap := uctxt pd;
ppermSnap := pperm pd;
PTSnap := PT pd;
ptpoolSnap := ptpool pd;
iptSnap := ipt pd;
syncchpoolSnap := syncchpool pd;
bufferSnap := buffer pd;
eptSnap := ept pd;
vmcsSnap := vmcs pd;
vmxSnap := vmx pd;
com1Snap := com1 pd;
drv_serialSnap := drv_serial pd;
console_concreteSnap := console_concrete pd;
consoleSnap := console pd;
ioapicSnap := ioapic pd;
lapicSnap := lapic pd;
tfSnap := tf pd;
tf_regSnap := tf_reg pd;
temporary place to save an intermediate tf regiter
curr_intr_numSnap := curr_intr_num pd;
intr_flagSnap := intr_flag pd;
saved_intr_flagsSnap := saved_intr_flags pd;
in_intrSnap := in_intr pd;
i_dev_serialSnap := i_dev_serial pd
|}.
End SNAPFUNCDEF.
Section REVSNAPFUNCDEF.
Definition snap_rev_func (pdSnap : privDataSnap) : privData :=
{|
ti := tiSnap pdSnap;
ikern := ikernSnap pdSnap;
ihost := ihostSnap pdSnap;
HP := HPSnap pdSnap;
AC := ACSnap pdSnap;
uctxt := uctxtSnap pdSnap;
pperm := ppermSnap pdSnap;
PT := PTSnap pdSnap;
ptpool := ptpoolSnap pdSnap;
ipt := iptSnap pdSnap;
syncchpool := syncchpoolSnap pdSnap;
buffer := bufferSnap pdSnap;
ept := eptSnap pdSnap;
vmcs := vmcsSnap pdSnap;
vmx := vmxSnap pdSnap;
com1 := com1Snap pdSnap;
drv_serial := drv_serialSnap pdSnap;
console_concrete := console_concreteSnap pdSnap;
console := consoleSnap pdSnap;
ioapic := ioapicSnap pdSnap;
lapic := lapicSnap pdSnap;
tf := tfSnap pdSnap;
tf_reg := tf_regSnap pdSnap;
intr_flagSnap := intr_flag pd;
saved_intr_flagsSnap := saved_intr_flags pd;
in_intrSnap := in_intr pd;
i_dev_serialSnap := i_dev_serial pd
|}.
End SNAPFUNCDEF.
Section REVSNAPFUNCDEF.
Definition snap_rev_func (pdSnap : privDataSnap) : privData :=
{|
ti := tiSnap pdSnap;
ikern := ikernSnap pdSnap;
ihost := ihostSnap pdSnap;
HP := HPSnap pdSnap;
AC := ACSnap pdSnap;
uctxt := uctxtSnap pdSnap;
pperm := ppermSnap pdSnap;
PT := PTSnap pdSnap;
ptpool := ptpoolSnap pdSnap;
ipt := iptSnap pdSnap;
syncchpool := syncchpoolSnap pdSnap;
buffer := bufferSnap pdSnap;
ept := eptSnap pdSnap;
vmcs := vmcsSnap pdSnap;
vmx := vmxSnap pdSnap;
com1 := com1Snap pdSnap;
drv_serial := drv_serialSnap pdSnap;
console_concrete := console_concreteSnap pdSnap;
console := consoleSnap pdSnap;
ioapic := ioapicSnap pdSnap;
lapic := lapicSnap pdSnap;
tf := tfSnap pdSnap;
tf_reg := tf_regSnap pdSnap;
temporary place to save an intermediate tf regiter
curr_intr_num := curr_intr_numSnap pdSnap;
intr_flag := intr_flagSnap pdSnap;
saved_intr_flags := saved_intr_flagsSnap pdSnap;
in_intr := in_intrSnap pdSnap;
i_dev_serial := i_dev_serialSnap pdSnap
|}.
End REVSNAPFUNCDEF.
Section REPLAYFUNC.
Definition apply_event (ev : LogEvent) (adt : dshare) : option dshare :=
match ev with
| LEvent tid ev_unit ⇒
match ev_unit with
| LogPrim prim_id args choice dSnapShot ⇒
match prim_id_num prim_id with
| palloc_num ⇒
match args with
| (Lint n)::nil ⇒
match single_big_palloc_spec_share (Int.unsigned n) choice adt with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| pt_resv_num ⇒
match args with
| (Lint n)::(Lint vadr)::(Lint perm)::nil ⇒
match choice with
| 0 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 0 adt with
| Some (adt´, i) ⇒ if zeq i 0 then Some adt´ else None
| _ ⇒ None
end
| 1 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then Some adt´ else None
| _ ⇒ None
end
| 2 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then None else Some adt´
| _ ⇒ None
end
| 3 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then None else
match single_big_palloc_spec_share (Int.unsigned n) 0 adt´ with
| Some (adt´´, i´) ⇒ if zeq i´ 0 then Some adt´´ else None
| _ ⇒ None
end
| _ ⇒ None
end
| 4 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then None else
match single_big_palloc_spec_share (Int.unsigned n) 1 adt´ with
| Some (adt´´, _) ⇒ Some adt´´
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| proc_create_num ⇒
match args with
| (Lint elf_id)::(Lptr buc uc_ofs)::(Lint q)::nil ⇒
match single_big_proc_create_spec_share adt buc uc_ofs (Int.unsigned q) choice with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| thread_wakeup_num ⇒
match args with
| (Lint cv)::nil ⇒
match single_big_thread_wakeup_spec_share (Int.unsigned cv) adt with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| sched_init_num ⇒
match args with
| (Lint mbi_adr)::nil ⇒ single_big_sched_init_spec_share (Int.unsigned mbi_adr) adt
| _ ⇒ None
end
| acquire_lock_CHAN_num ⇒
match args with
| (Lint lk_index)::nil ⇒
match single_big_acquire_lock_SC_spec_share (Int.unsigned lk_index) adt with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| release_lock_CHAN_num ⇒
match args with
| (Lint lk_index)::nil ⇒
single_big_release_lock_SC_spec_share (Int.unsigned lk_index)
(syncchpool (snap_rev_func dSnapShot))
adt
| _ ⇒ None
end
| ipc_send_body_num ⇒
match args with
| (Lint chid)::(Lint vaddr)::(Lint scound)::nil ⇒
match single_big_ipc_send_body_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scound)
(adt, (snap_rev_func dSnapShot)) with
| Some ((adt´, _), _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| LogYield _ ⇒
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
match (init adt, pg adt, B_inLock cpu (big_log adt)) with
| (true, true, false) ⇒
match big_log adt, ZMap.get (msg_q_id cpu + ID_AT_range) (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDYIELD curid) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if B_GetContainerUsed_opt t cpu l then
if option_z_check t then
if z_check la then
Some (adt {sh_big_log: BigDef l´}
{sh_cid: (ZMap.set cpu la (cid adt))})
else None
else None
else None
else None
else None
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
| LogSleep cv _ optSync ⇒
match optSync with
| Some sync_val ⇒
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
match (init adt, pg adt,
B_inLock cpu (big_log adt)) with
| (true, true, true) ⇒
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get abid (lock adt), ZMap.get sc_id (lock adt) with
| BigDef l, LockFalse, LockOwn true ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSLEEP curid cv sync_val) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´, B_CalLock sc_id l, B_CalLock sc_id l1 with
| Some (TCB_RID la), Some (S (S _), LHOLD, Some cpu´), Some _ ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if zeq cpu cpu´ then
if z_check la then
Some (adt {sh_big_log: BigDef l´}
{sh_cid: (ZMap.set cpu la (cid adt))}
{sh_lock: ZMap.set sc_id LockFalse
(ZMap.set abid LockFalse (lock adt))})
else None
else None
else None
else None
| _,_,_ ⇒ None
end
| _,_,_ ⇒ None
end
else None
else None
| _ ⇒ None
end
| _ ⇒ None
end
| LogYieldBack ⇒ Some adt
end
end.
Fixpoint update (adt: dshare) (sh_log : Log) {struct sh_log} : dshare :=
match sh_log with
| nil ⇒ adt
| hd::tl ⇒ let adt´ := update adt tl in
match apply_event hd adt´ with
| Some adt´´ ⇒ adt´´
| _ ⇒ adt´
end
end.
Lemma update_invariant (I: dshare → Prop):
(∀ e d d´, apply_event e d = Some d´ → I d → I d´) →
(∀ d l, I d → I (update d l)).
Proof.
induction l; simpl; eauto.
destruct (apply_event a _) eqn:Hd´; eauto.
Qed.
End REPLAYFUNC.
Section STATE_CHECK.
Function thread_yield_state_check (d: PData) : Prop :=
let sd := (fst d) in
let pd := (snd d) in
let cpu := CPU_ID sd in
let curid := (ZMap.get cpu (cid sd)) in
match (init sd, pg sd, ikern pd, ihost pd, ipt pd,
PT pd, in_intr pd, intr_flag pd, B_inLock cpu (big_log sd)) with
| (true, true, true, true, true, 0, false, true, false) ⇒
match big_log sd, ZMap.get (msg_q_id cpu + ID_AT_range) (lock sd), (snd (ti pd)) with
| BigDef l, LockFalse, Vint ti_val ⇒
if B_GetContainerUsed curid cpu l then
if Int.eq ti_val Int.zero then
if Int.eq Int.zero (fst (ti pd)) then
let to := big_oracle sd in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDYIELD curid) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if B_GetContainerUsed_opt t cpu l then
if option_z_check t then
if z_check la then
True
else False
else False
else False
else False
else False
| _ ⇒ False
end
else False
else False
else False
| _,_,_ ⇒ False
end
| _ ⇒ False
end.
Function thread_sleep_state_check (cv: Z) (d: PData): Prop :=
let sd := (fst d) in
let pd := (snd d) in
let cpu := (CPU_ID sd) in
let curid := (ZMap.get cpu (cid sd)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
match (init sd, pg sd, ikern pd, ihost pd, ipt pd,
PT pd, in_intr pd, intr_flag pd,
B_inLock cpu (big_log sd)) with
| (true, true, true, true, true, 0, false, true, true) ⇒
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match big_log sd, ZMap.get abid (lock sd), ZMap.get sc_id (lock sd),
snd (ti pd) with
| BigDef l, LockFalse, LockOwn true, Vint ti_val ⇒
if B_GetContainerUsed curid cpu l then
if Int.eq ti_val Int.zero then
if Int.eq Int.zero (fst (ti pd)) then
let to := big_oracle sd in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSLEEP curid cv (syncchpool pd) ) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´, B_CalLock sc_id l, B_CalLock sc_id l1 with
| Some (TCB_RID la), Some (S (S _), LHOLD, Some cpu´), Some _ ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if zeq cpu cpu´ then
if z_check la then
True
else False
else False
else False
else False
| _,_,_ ⇒ False
end
else False
else False
else False
| _,_,_,_ ⇒ False
end
else False
else False
| _ ⇒ False
end.
Definition state_check (name : ident) (largs : list lval) (l : Log) (pd: dproc) : Prop :=
if peq name thread_yield then
match largs with
| nil ⇒ thread_yield_state_check (update init_shared_adt l, pd)
| _ ⇒ False
end
else if peq name thread_sleep then
match largs with
| (Lint cv)::nil ⇒ thread_sleep_state_check (Int.unsigned cv) (update init_shared_adt l, pd)
| _ ⇒ False
end
else False.
End STATE_CHECK.
End PHBSPECSReplay.
intr_flag := intr_flagSnap pdSnap;
saved_intr_flags := saved_intr_flagsSnap pdSnap;
in_intr := in_intrSnap pdSnap;
i_dev_serial := i_dev_serialSnap pdSnap
|}.
End REVSNAPFUNCDEF.
Section REPLAYFUNC.
Definition apply_event (ev : LogEvent) (adt : dshare) : option dshare :=
match ev with
| LEvent tid ev_unit ⇒
match ev_unit with
| LogPrim prim_id args choice dSnapShot ⇒
match prim_id_num prim_id with
| palloc_num ⇒
match args with
| (Lint n)::nil ⇒
match single_big_palloc_spec_share (Int.unsigned n) choice adt with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| pt_resv_num ⇒
match args with
| (Lint n)::(Lint vadr)::(Lint perm)::nil ⇒
match choice with
| 0 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 0 adt with
| Some (adt´, i) ⇒ if zeq i 0 then Some adt´ else None
| _ ⇒ None
end
| 1 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then Some adt´ else None
| _ ⇒ None
end
| 2 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then None else Some adt´
| _ ⇒ None
end
| 3 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then None else
match single_big_palloc_spec_share (Int.unsigned n) 0 adt´ with
| Some (adt´´, i´) ⇒ if zeq i´ 0 then Some adt´´ else None
| _ ⇒ None
end
| _ ⇒ None
end
| 4 ⇒ match single_big_palloc_spec_share (Int.unsigned n) 1 adt with
| Some (adt´, i) ⇒ if zeq i 0 then None else
match single_big_palloc_spec_share (Int.unsigned n) 1 adt´ with
| Some (adt´´, _) ⇒ Some adt´´
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| proc_create_num ⇒
match args with
| (Lint elf_id)::(Lptr buc uc_ofs)::(Lint q)::nil ⇒
match single_big_proc_create_spec_share adt buc uc_ofs (Int.unsigned q) choice with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| thread_wakeup_num ⇒
match args with
| (Lint cv)::nil ⇒
match single_big_thread_wakeup_spec_share (Int.unsigned cv) adt with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| sched_init_num ⇒
match args with
| (Lint mbi_adr)::nil ⇒ single_big_sched_init_spec_share (Int.unsigned mbi_adr) adt
| _ ⇒ None
end
| acquire_lock_CHAN_num ⇒
match args with
| (Lint lk_index)::nil ⇒
match single_big_acquire_lock_SC_spec_share (Int.unsigned lk_index) adt with
| Some (adt´, _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| release_lock_CHAN_num ⇒
match args with
| (Lint lk_index)::nil ⇒
single_big_release_lock_SC_spec_share (Int.unsigned lk_index)
(syncchpool (snap_rev_func dSnapShot))
adt
| _ ⇒ None
end
| ipc_send_body_num ⇒
match args with
| (Lint chid)::(Lint vaddr)::(Lint scound)::nil ⇒
match single_big_ipc_send_body_spec (Int.unsigned chid) (Int.unsigned vaddr) (Int.unsigned scound)
(adt, (snap_rev_func dSnapShot)) with
| Some ((adt´, _), _) ⇒ Some adt´
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| LogYield _ ⇒
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
match (init adt, pg adt, B_inLock cpu (big_log adt)) with
| (true, true, false) ⇒
match big_log adt, ZMap.get (msg_q_id cpu + ID_AT_range) (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDYIELD curid) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if B_GetContainerUsed_opt t cpu l then
if option_z_check t then
if z_check la then
Some (adt {sh_big_log: BigDef l´}
{sh_cid: (ZMap.set cpu la (cid adt))})
else None
else None
else None
else None
else None
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
| LogSleep cv _ optSync ⇒
match optSync with
| Some sync_val ⇒
let cpu := (CPU_ID adt) in
let curid := (ZMap.get cpu (cid adt)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
match (init adt, pg adt,
B_inLock cpu (big_log adt)) with
| (true, true, true) ⇒
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get abid (lock adt), ZMap.get sc_id (lock adt) with
| BigDef l, LockFalse, LockOwn true ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSLEEP curid cv sync_val) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´, B_CalLock sc_id l, B_CalLock sc_id l1 with
| Some (TCB_RID la), Some (S (S _), LHOLD, Some cpu´), Some _ ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if zeq cpu cpu´ then
if z_check la then
Some (adt {sh_big_log: BigDef l´}
{sh_cid: (ZMap.set cpu la (cid adt))}
{sh_lock: ZMap.set sc_id LockFalse
(ZMap.set abid LockFalse (lock adt))})
else None
else None
else None
else None
| _,_,_ ⇒ None
end
| _,_,_ ⇒ None
end
else None
else None
| _ ⇒ None
end
| _ ⇒ None
end
| LogYieldBack ⇒ Some adt
end
end.
Fixpoint update (adt: dshare) (sh_log : Log) {struct sh_log} : dshare :=
match sh_log with
| nil ⇒ adt
| hd::tl ⇒ let adt´ := update adt tl in
match apply_event hd adt´ with
| Some adt´´ ⇒ adt´´
| _ ⇒ adt´
end
end.
Lemma update_invariant (I: dshare → Prop):
(∀ e d d´, apply_event e d = Some d´ → I d → I d´) →
(∀ d l, I d → I (update d l)).
Proof.
induction l; simpl; eauto.
destruct (apply_event a _) eqn:Hd´; eauto.
Qed.
End REPLAYFUNC.
Section STATE_CHECK.
Function thread_yield_state_check (d: PData) : Prop :=
let sd := (fst d) in
let pd := (snd d) in
let cpu := CPU_ID sd in
let curid := (ZMap.get cpu (cid sd)) in
match (init sd, pg sd, ikern pd, ihost pd, ipt pd,
PT pd, in_intr pd, intr_flag pd, B_inLock cpu (big_log sd)) with
| (true, true, true, true, true, 0, false, true, false) ⇒
match big_log sd, ZMap.get (msg_q_id cpu + ID_AT_range) (lock sd), (snd (ti pd)) with
| BigDef l, LockFalse, Vint ti_val ⇒
if B_GetContainerUsed curid cpu l then
if Int.eq ti_val Int.zero then
if Int.eq Int.zero (fst (ti pd)) then
let to := big_oracle sd in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDYIELD curid) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCB_YIELD la t) ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if B_GetContainerUsed_opt t cpu l then
if option_z_check t then
if z_check la then
True
else False
else False
else False
else False
else False
| _ ⇒ False
end
else False
else False
else False
| _,_,_ ⇒ False
end
| _ ⇒ False
end.
Function thread_sleep_state_check (cv: Z) (d: PData): Prop :=
let sd := (fst d) in
let pd := (snd d) in
let cpu := (CPU_ID sd) in
let curid := (ZMap.get cpu (cid sd)) in
let n := slp_q_id cv 0 in
let abid := (n + ID_AT_range) in
let sc_id := n + lock_TCB_range in
match (init sd, pg sd, ikern pd, ihost pd, ipt pd,
PT pd, in_intr pd, intr_flag pd,
B_inLock cpu (big_log sd)) with
| (true, true, true, true, true, 0, false, true, true) ⇒
if zlt_lt 0 curid num_proc then
if zle_lt 0 cv num_cv then
match big_log sd, ZMap.get abid (lock sd), ZMap.get sc_id (lock sd),
snd (ti pd) with
| BigDef l, LockFalse, LockOwn true, Vint ti_val ⇒
if B_GetContainerUsed curid cpu l then
if Int.eq ti_val Int.zero then
if Int.eq Int.zero (fst (ti pd)) then
let to := big_oracle sd in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSLEEP curid cv (syncchpool pd) ) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´, B_CalLock sc_id l, B_CalLock sc_id l1 with
| Some (TCB_RID la), Some (S (S _), LHOLD, Some cpu´), Some _ ⇒
if zle_lt 0 la num_proc then
if B_GetContainerUsed la cpu l then
if zeq cpu cpu´ then
if z_check la then
True
else False
else False
else False
else False
| _,_,_ ⇒ False
end
else False
else False
else False
| _,_,_,_ ⇒ False
end
else False
else False
| _ ⇒ False
end.
Definition state_check (name : ident) (largs : list lval) (l : Log) (pd: dproc) : Prop :=
if peq name thread_yield then
match largs with
| nil ⇒ thread_yield_state_check (update init_shared_adt l, pd)
| _ ⇒ False
end
else if peq name thread_sleep then
match largs with
| (Lint cv)::nil ⇒ thread_sleep_state_check (Int.unsigned cv) (update init_shared_adt l, pd)
| _ ⇒ False
end
else False.
End STATE_CHECK.
End PHBSPECSReplay.