Library mcertikos.objects.BigStepLogReplay
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Import BigStepGlobalOracle.
Require Import GlobalOracle.
Require Import CommonTactic.
Section Cal_TICKET_LOCK.
Fixpoint B_CalLock (li: Z) (l: BigLog) :=
match l with
| nil ⇒ Some (O, LEMPTY, None)
| (TBEVENT i e) :: l´ ⇒
match B_CalLock li l´ with
| Some (self_c, b, res) ⇒
match e with
| TBLOCK li´ e0 ⇒
if zle_lt lock_TCB_range li´ (lock_TCB_range + num_chan) then
if (zeq li li´) then
match self_c, res with
| S (S self_c´), Some i0 ⇒
if (zeq i i0) then
match e0, b with
| BREL_LOCK _ _, LHOLD ⇒
Some (O, LEMPTY, None)
| _,_ ⇒ None
end
else None
| _, None ⇒
match e0, b with
| BWAIT_LOCK _ (S n), LEMPTY ⇒
Some (n, LHOLD, Some i)
| _,_ ⇒ None
end
| _,_ ⇒ None
end
else Some (self_c, b, res)
else None
| TBSHARED (BTDSLEEP slp_id cv _) ⇒
if zle_lt 0 cv num_cv then
let li´ := (slp_q_id cv 0) + lock_TCB_range in
if (zeq li li´) then
match self_c, res, b with
| S (S self_c´), Some i0, LHOLD ⇒
if (zeq i i0) then
Some (O, LEMPTY, None)
else None
| _, _, _ ⇒ None
end
else Some (self_c, b, res)
else None
| TBSHARED (BBUFFERE _ cv _) ⇒
if zle_lt 0 cv num_cv then
let li´ := (slp_q_id cv 0) + lock_TCB_range in
if (zeq li li´) then
match self_c, res, b with
| S self_c´, Some i0, LHOLD ⇒
if (zeq i i0) then
Some (self_c´, LHOLD, Some i0)
else None
| _, _, _ ⇒ None
end
else Some (self_c, b, res)
else None
| _ ⇒ Some (self_c, b, res)
end
| _ ⇒ None
end
end.
Global Opaque B_CalLock.
End Cal_TICKET_LOCK.
Section CAL_AT.
Require Import RealParams.
Context `{real_params: RealParams}.
Fixpoint B_CalAT_log (l: BigLog) (a: ATable) :=
match l with
| nil ⇒ Some a
| (TBEVENT _ e) :: l´ ⇒
match B_CalAT_log l´ a with
| Some a´ ⇒
match e with
| TBSHARED (BPALLOCE _ i) ⇒
if zeq i 0 then Some a´
else
match ZMap.get i a´ with
| ATValid false ATNorm ⇒
Some (ZMap.set i (ATValid true ATNorm) a´)
| _ ⇒ None
end
| _ ⇒ Some a´
end
| _ ⇒ None
end
end.
Definition B_CalAT_log_real (l: BigLog) :=
B_CalAT_log l (real_AT (ZMap.init ATUndef)).
Section B_CalAT_log_property.
Lemma B_CalAT_log_sub_log_exist:
∀ l l´ def_atable atable,
B_CalAT_log (l++l´) def_atable = Some atable→
∃ atable´, B_CalAT_log l´ def_atable = Some atable´.
Proof.
induction l; simpl; intros.
- ∃ atable; auto.
- subdestruct; simpl; subst; inv H; eapply IHl; eauto.
Qed.
Lemma B_CalAT_log_keeps_allocated_pages:
∀ l l´ def_atable atable atable´,
B_CalAT_log l´ def_atable = Some atable´ →
B_CalAT_log (l++l´) def_atable = Some atable →
∀ i, ZMap.get i atable´ = (ATValid true ATNorm) →
ZMap.get i atable = (ATValid true ATNorm).
Proof.
induction l; intros.
- simpl in H0.
rewrite H in H0; inv H0; auto.
- simpl in H0; subdestruct; inv H0; try eauto using IHl.
case_eq (zeq i b); intros; subst.
+ rewrite ZMap.gss; auto.
+ rewrite ZMap.gso; auto.
eauto using IHl.
Qed.
End B_CalAT_log_property.
End CAL_AT.
Section CAL_TCB.
Require Import CalRealProcModule.
Require Import LogReplay.
Context`{oracle_ops: MultiOracleOps}.
Fixpoint B_CalTCB_split_log (l: BigLog) (t: AbTCBPool) (q: AbQueuePool) (slp: Z) (cid: Z)
(cache: ZMap.t (option (prod AbTCBPool AbQueuePool))):=
match l with
| nil ⇒ Some (t, q, slp, cid, cache, TCB_NORES)
| (TBEVENT cpu e) :: l´ ⇒
let rdyq := rdy_q_id cpu in
match B_CalTCB_split_log l´ t q slp cid cache with
| Some (t´, q´, slp´, cid´, cache´, res´) ⇒
match e with
| TBSHARED (BTDSPAWN _ new_id _ _ _ _) ⇒
match (ZMap.get rdyq q´, ZMap.get new_id t´) with
| (AbQValid l, AbTCBValid _ _ (-1)) ⇒
let (rt, rq) := if zeq cpu current_CPU_ID then
(ZMap.set new_id (AbTCBValid READY cpu rdyq) t´,
ZMap.set rdyq (AbQValid (l++ (new_id :: nil))) q´)
else (t´, q´) in
Some (rt, rq, slp´, cid´, cache´, TCB_NORES)
| _ ⇒ None
end
| TBSHARED (BTDSLEEP _ cv _) ⇒
let slpq := slp_q_id cv 0 in
let (nt, nq) := match ZMap.get slpq cache´ with
| Some (t0, q0) ⇒ (t0, q0)
| _ ⇒ (t´, q´)
end in
match (ZMap.get slpq nq, ZMap.get rdyq nq) with
| (AbQValid l0, AbQValid (nextt :: l)) ⇒
match (ZMap.get cid´ nt, ZMap.get nextt nt) with
| (AbTCBValid RUN cpu_t b, AbTCBValid READY cpu_t´ q_id) ⇒
if zeq cpu_t cpu then
if zeq b (-1) then
if zeq cpu_t´ cpu then
if zeq q_id rdyq then
if zeq nextt cid´ then None
else
let n := slp´ + 1 in
if zlt_lt 0 n num_proc then
let cache_t := ZMap.set cid´ (AbTCBValid RUN cpu slpq) nt in
let cache_q := ZMap.set slpq (AbQValid (l0 ++ (cid´::nil))) nq in
let (rt, rq) :=
if zeq cpu current_CPU_ID then
(ZMap.set nextt (AbTCBValid RUN cpu (-1))
(ZMap.set cid´ (AbTCBValid SLEEP cpu slpq) nt),
ZMap.set rdyq (AbQValid l)
(ZMap.set slpq (AbQValid (l0 ++ (cid´::nil))) nq))
else (t´, q´) in
let (rslp, rcid) := if zeq cpu current_CPU_ID then (n, nextt) else (slp´, cid´) in
Some (rt, rq, rslp, rcid,
ZMap.set slpq (Some (cache_t, cache_q)) cache´,
TCB_RID nextt)
else None
else None
else None
else None
else None
| _ ⇒ None
end
| _ ⇒ None
end
| TBSHARED (BTDWAKE _ cv_id) ⇒
let n := slp_q_id cv_id 0 in
let (nt, nq) := match ZMap.get n cache´ with
| Some (t0, q0) ⇒ (t0, q0)
| _ ⇒ (t´, q´)
end in
match (ZMap.get n nq) with
| AbQValid ll ⇒
match ll with
| nil ⇒
let (rt, rq) := if zeq cpu current_CPU_ID then (nt, nq) else (t´, q´) in
Some (rt, rq, slp´, cid´, ZMap.set n (Some (nt, nq)) cache´, TCBWAKE_F)
| la :: l ⇒
if zle_lt 0 la num_proc then
match (ZMap.get la nt) with
| AbTCBValid tds cpu´ _ ⇒
if zeq cpu cpu´ then
match ZMap.get rdyq nq with
| AbQValid l0 ⇒
let cache_t := (ZMap.set la (AbTCBValid tds cpu (-1)) nt): AbTCBPool in
let cache_q := (ZMap.set n (AbQValid l) nq): AbQueuePool in
let (rt, rq) :=
(if zeq cpu current_CPU_ID then
(ZMap.set la (AbTCBValid READY cpu rdyq) nt,
ZMap.set rdyq (AbQValid (l0 ++ (la :: nil)))
(ZMap.set n (AbQValid l) nq))
else (t´, q´)) : (prod AbTCBPool AbQueuePool) in
Some (rt, rq, slp´, cid´,
ZMap.set n (Some (cache_t, cache_q)) cache´,
TCBWAKE_T la)
| _ ⇒ None
end
else
if zle_lt 0 cpu´ 8 then
let cache_t := ZMap.set la (AbTCBValid tds cpu´ (-1)) nt in
let cache_q := ZMap.set n (AbQValid l) nq in
let (rt, rq) := if zeq cpu current_CPU_ID then (cache_t, cache_q) else (t´, q´) in
Some (rt, rq, slp´, cid´,
ZMap.set n (Some (cache_t, cache_q)) cache´, TCBWAKE la cpu´)
else None
| _ ⇒ None
end
else None
end
| _ ⇒ None
end
| TBSHARED (BTDWAKE_DIFF _ _ la cpu´) ⇒
let msgq := msg_q_id cpu´ in
let (nt, nq) := match ZMap.get msgq cache´ with
| Some (t0, q0) ⇒ (t0, q0)
| _ ⇒ (t´, q´)
end in
match ZMap.get msgq nq, ZMap.get la nt with
| AbQValid l0, AbTCBValid tds0 cpu0 b ⇒
if zeq cpu0 cpu´ then
if zeq b (-1) then
let cache_t := ZMap.set la (AbTCBValid tds0 cpu´ msgq) nt in
let cache_q := ZMap.set msgq (AbQValid (l0 ++ (la :: nil))) nq in
let (rt, rq) :=
if zeq cpu current_CPU_ID then
(ZMap.set la (AbTCBValid tds0 cpu´ msgq) nt, cache_q)
else (t´, q´) in
Some (rt, rq, slp´, cid´, ZMap.set msgq (Some (cache_t, cache_q)) cache´, TCB_NORES)
else None
else None
| _,_ ⇒ None
end
| TBSHARED (BTDYIELD _) ⇒
let msgq := msg_q_id cpu in
let (nt, nq) := match ZMap.get msgq cache´ with
| Some (t0, q0) ⇒ (t0, q0)
| _ ⇒ (t´, q´)
end in
match (ZMap.get msgq nq) with
| AbQValid ll ⇒
match ll with
| nil ⇒
match ZMap.get rdyq nq, ZMap.get cid´ nt with
| AbQValid (la0 :: l0), AbTCBValid RUN cpu_t q_id ⇒
if zeq cpu_t cpu then
if zeq q_id (-1) then
match ZMap.get la0 nt with
| AbTCBValid _ cpu_t´ _ ⇒
if zeq cpu_t´ cpu then
let (rt, rq) :=
if zeq cpu current_CPU_ID then
(ZMap.set la0 (AbTCBValid RUN cpu (-1))
(ZMap.set cid´ (AbTCBValid READY cpu rdyq) nt),
ZMap.set rdyq (AbQValid (l0 ++ (cid´::nil))) nq)
else (t´, q´) in
let rcid := if zeq cpu current_CPU_ID then la0 else cid´ in
Some (rt, rq, slp´, rcid, ZMap.set msgq (Some (nt, nq)) cache´,
TCB_YIELD la0 None)
else None
| _ ⇒ None
end
else None
else None
| _,_ ⇒ None
end
| la :: l ⇒
if zle_lt 0 la num_proc then
if zeq la cid´ then None
else
match ZMap.get rdyq nq, ZMap.get la nt, ZMap.get cid´ nt with
| AbQValid l0, AbTCBValid tds cpu_la _, AbTCBValid RUN cpu_t q_id ⇒
if zeq cpu_t cpu then
if zeq q_id (-1) then
match (l0 ++ (la :: nil)) with
| nil ⇒ None
| la0 :: l1 ⇒
match ZMap.get la0 nt with
| AbTCBValid _ cpu_t´ _ ⇒
if zeq cpu_t´ cpu then
let n := slp´ - 1 in
if zle_lt 0 n (num_proc - 1) then
let cache_t := ZMap.set la (AbTCBValid tds cpu_la (-1)) nt in
let cache_q := ZMap.set msgq (AbQValid l) nq in
let (rt, rq) :=
if zeq cpu current_CPU_ID then
(ZMap.set
la0 (AbTCBValid RUN cpu (-1))
(ZMap.set
cid´ (AbTCBValid READY cpu rdyq)
(ZMap.set la (AbTCBValid READY cpu rdyq) nt)),
ZMap.set rdyq (AbQValid (l1 ++ (cid´ :: nil)))
(ZMap.set msgq (AbQValid l) nq))
else (t´, q´) in
let (rslp, rcid) :=
if zeq cpu current_CPU_ID then (n, la0) else (slp´, cid´) in
Some (rt, rq, rslp, rcid,
ZMap.set msgq (Some (cache_t, cache_q)) cache´,
TCB_YIELD la0 (Some la))
else None
else None
| _ ⇒ None
end
end
else None
else None
| _, _,_ ⇒ None
end
else None
end
| _ ⇒ None
end
| _ ⇒ Some (t´, q´, slp´, cid´, cache´, res´)
end
| _ ⇒ None
end
end.
Definition B_CalTCB_log (l: BigLog) :=
B_CalTCB_split_log l (ZMap.set 0 (AbTCBValid RUN current_CPU_ID (-1)) (real_abtcb (ZMap.init AbTCBUndef)))
(real_abq (ZMap.init AbQUndef)) 0 (current_CPU_ID + 1) (ZMap.init None).
Definition B_CalTCB_log_real (l: BigLog) :=
match B_CalTCB_log l with
| Some (_,_,_,_,_, r) ⇒ Some r
| _ ⇒ None
end.
End CAL_TCB.
Section Cal_SyncChan.
Fixpoint B_GetSharedSC (lid: Z) (l: BigLog):=
match l with
| nil ⇒ None
| TBEVENT _ e :: l´ ⇒
let l0 := B_GetSharedSC lid l´ in
match e with
| TBLOCK lock_id (BREL_LOCK _ s´) ⇒
if zeq lid lock_id then Some s´ else l0
| TBSHARED (BTDSLEEP _ cv s´) ⇒
let n := slp_q_id cv 0 in
let sc_id := n + lock_TCB_range in
if zeq lid sc_id then Some s´ else l0
| _ ⇒ l0
end
end.
Fixpoint B_GetSharedBuffer (lid: Z) (l: BigLog):=
match l with
| nil ⇒ None
| TBEVENT _ e :: l´ ⇒
let b0 := B_GetSharedBuffer lid l´ in
match e with
| TBSHARED (BBUFFERE _ cv b) ⇒
let n := slp_q_id cv 0 in
let sc_id := n + lock_TCB_range in
if zeq lid sc_id then Some b else b0
| _ ⇒ b0
end
end.
End Cal_SyncChan.
Section Def_Invariant.
Context `{real_params: RealParams}.
Definition valid_big_oracle_domain (o: BigOracle):=
∀ i i0 e l
(Hin: In (TBEVENT i0 e) (o i l)),
i0 ≠ i.
Definition valid_AT_log_B l :=
∃ a, B_CalAT_log_real l = Some a.
Definition valid_AT_log_type_B l :=
∀ q (Hdef: l = BigDef q),
valid_AT_log_B q.
Definition valid_AT_oracle_B (o: BigOracle) :=
∀ q i (Hvalid: valid_AT_log_B q),
valid_AT_log_B ((o i q) ++ q).
Definition valid_lock_B li l :=
∃ self_c b q, B_CalLock li l = Some (self_c, b, q).
Definition valid_lock_pool_B l :=
∀ q li (Hdef: l = BigDef q)
(Hrange: li = ID_AT ∨ li = lock_range ∨
(∃ ofs, index2Z ID_SC ofs = Some li)),
valid_lock_B li q.
Definition valid_lock_oracle_B (o: BigOracle):=
∀ q li i (Hvalid: valid_lock_B li q)
(Hrange: li = ID_AT ∨ li = lock_range ∨
(∃ ofs, index2Z ID_SC ofs = Some li)),
valid_lock_B li ((o i q) ++ q).
Section WITH_OPS.
Context`{oracle_ops: MultiOracleOps}.
Definition valid_TCB_log_B l :=
∃ res, B_CalTCB_log_real l = Some (res).
Definition valid_TCB_log_type_B l :=
∀ q (Hdef: l = BigDef q),
valid_TCB_log_B q.
Definition valid_TCB_oracle_B (o: BigOracle) :=
∀ q i (Hvalid: valid_TCB_log_B q),
valid_TCB_log_B ((o i q) ++ q).
Definition valid_big_oracle (o: BigOracle):=
valid_big_oracle_domain o
∧ valid_TCB_oracle_B o
∧ valid_AT_oracle_B o
∧ valid_lock_oracle_B o.
End WITH_OPS.
Definition valid_big_log (l: BigLogType) (i: Z):=
match l with
| BigDef (TBEVENT i´ _ :: _) ⇒ i´ = i
| _ ⇒ True
end.
Definition is_my_spawn (ev: BigOracleEventUnit) (curid : Z) : Prop :=
match ev with
| TBSHARED ev´ ⇒
match ev´ with
| BTDSPAWN _ new_id _ _ _ _ ⇒ if zeq curid new_id then True else False
| _ ⇒ False
end
| _ ⇒ False
end.
Definition get_ev_curid (ev: BigOracleEventUnit) : Z :=
match ev with
| TBSHARED ev´ ⇒
match ev´ with
| BPALLOCE curid _ ⇒ curid
| BBUFFERE curid _ _ ⇒ curid
| BTDSPAWN curid _ _ _ _ _ ⇒ curid
| BTDYIELD curid ⇒ curid
| BTDSLEEP curid _ _ ⇒ curid
| BTDWAKE curid _ ⇒ curid
| BTDWAKE_DIFF curid _ _ _ ⇒ curid
end
| TBLOCK _ ev´ ⇒
match ev´ with
| BWAIT_LOCK curid _ ⇒ curid
| BGET_LOCK curid ⇒ curid
| BREL_LOCK curid _ ⇒ curid
end
end.
Section WithBigOracleOps.
Context `{big_oracle_ops : BigOracleOps}.
Definition valid_big_oracle_env_fun_domain (o: BigOracle):=
∀ limit cpuid curid l l´
(Hbig_oracle_fun: big_oracle_env_fun limit cpuid curid o l = l´),
∃ l´´, l´ = l´´++ l ∧
(∀ i0 ev, In (TBEVENT i0 ev) l´´ →
(get_ev_curid ev ≠ curid) ∧
(¬is_my_spawn ev curid)).
Definition valid_big_oracle_env_fun (o: BigOracle):=
valid_big_oracle_env_fun_domain o.
End WithBigOracleOps.
End Def_Invariant.