Library mcertikos.objects.CalMCSLock
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 GlobalOracle.
Require Import CalTicketLock.
Require Import LogReplay.
Require Import ZSet.
Opaque Z.of_nat Z.to_nat Z.to_pos.
Section CAL_MCS_LOCK.
Definition mcs_lock_st_size := ((TOTAL_CPU × (2 + 14) + (15 + 1)) × 4).
Definition mcs_node_st_size := 64.
Definition NULL := TOTAL_CPU.
Definition next_pos (lock_index curid : Z) : Z := ((mcs_lock_st_size × lock_index) + 64 + (mcs_node_st_size × curid)).
Definition busy_pos (lock_index curid : Z) : Z := ((mcs_lock_st_size × lock_index) + 64 + (mcs_node_st_size × curid) + 4).
Definition tail_pos (lock_index : Z) : Z := (mcs_lock_st_size × lock_index).
Hint Unfold mcs_lock_st_size mcs_node_st_size NULL next_pos busy_pos tail_pos.
Inductive MCSLock :=
| MCSLOCK (tail: Z) (lock_array: ZMap.t (bool × Z)) (bounds : list nat).
Definition init_MCSLock :=
MCSLOCK NULL (ZMap.init (false, NULL)) nil.
Fixpoint CalMCSLock (l: MultiLog):=
match l with
| nil ⇒ Some init_MCSLock
| (TEVENT i e) :: l´ ⇒
match CalMCSLock l´ with
| Some mcs ⇒
match e, mcs with
| TTICKET e´, MCSLOCK tail0 la bounds ⇒
match e´ with
| SWAP_TAIL p _ ⇒
Some (MCSLOCK i (ZMap.set i (true, NULL) la) (bounds ++ (p::nil)))
| GET_NEXT ⇒ Some mcs
| SET_NEXT old ⇒
match ZMap.get old la with
| (b, t) ⇒
Some (MCSLOCK tail0 (ZMap.set old (b, i) la) bounds)
end
| GET_BUSY _ ⇒ Some mcs
| SET_BUSY ⇒
match ZMap.get i la with
| (b, t) ⇒
match ZMap.get t la with
| (b´, t´) ⇒
Some (MCSLOCK tail0 (ZMap.set t (false, t´) la) (tl bounds))
end
end
| CAS_TAIL false ⇒ Some mcs
| CAS_TAIL true ⇒
if zeq tail0 i then
Some (MCSLOCK NULL la nil)
else None
| _ ⇒ None
end
| _, _ ⇒ Some mcs
end
| _ ⇒ None
end
end.
Global Opaque CalMCSLock.
End CAL_MCS_LOCK.
Section CAL_MCS_WAIT.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
Fixpoint CalMCS_AcqWait (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l´ := (to i l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK tail la _) ⇒
match ZMap.get i la with
| (false, _) ⇒ Some ((TEVENT i (TTICKET (GET_BUSY false))) :: l´)
| _ ⇒
CalMCS_AcqWait n´ i ((TEVENT i (TTICKET (GET_BUSY true))) ::l´) to
end
| _ ⇒ None
end
end.
Global Opaque CalMCS_AcqWait.
Fixpoint CalMCS_RelWait (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l1 := (TEVENT i (TTICKET GET_NEXT)) :: (to i l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK tail la _) ⇒
match ZMap.get i la with
| (_, p) ⇒ if zeq p NULL
then CalMCS_RelWait n´ i l1 to
else
match CalMCSLock (to i l1 ++ l1) with
| Some (MCSLOCK tail´ la´ _) ⇒
match ZMap.get i la´ with
| (_, p´) ⇒ if zeq p´ NULL then None
else Some ((TEVENT i (TTICKET SET_BUSY)) :: (to i l1 ++ l1))
end
| _ ⇒ None
end
end
| _ ⇒ None
end
end.
Global Opaque CalMCS_RelWait.
End WITHWAITTIME.
End CAL_MCS_WAIT.
Section CAL_BOUND_NUM.
Context `{waittime: WaitTime}.
Definition CalPassLockLoopTime :=
(S fairness)%nat.
Definition CalPassLockTime :=
(S CalPassLockLoopTime)%nat.
Fixpoint CalSumWait (l: list nat) :=
match l with
| nil ⇒ O
| a :: l´ ⇒ ((3 + CalPassLockTime + a) + CalSumWait l´) % nat
end.
Definition rm_head {A: Type} (l: list A) :=
match l with
| nil ⇒ nil
| _ :: l´ ⇒ l´
end.
Definition WaitConstant : nat := (2 + CalPassLockTime)%nat.
Lemma WaitConstant_fairness : (fairness < WaitConstant)%nat.
unfold WaitConstant, CalPassLockTime, CalPassLockLoopTime.
omega.
Qed.
Lemma WaitConstant_PassLockTime : (S CalPassLockTime < WaitConstant)%nat.
unfold WaitConstant, CalPassLockTime.
simpl.
omega.
Qed.
Global Opaque WaitConstant.
Definition CalWaitLockTime (tq: list nat) :=
((5 + WaitConstant + length tq + (CalSumWait tq)) × WaitConstant)%nat.
End CAL_BOUND_NUM.
Section CAL_QS_LOCK.
Context `{waittime: WaitTime}.
Require Import ZSet.
Fixpoint QS_CalLock (l: MultiLog) : option (nat × nat × head_status × list Z × ZSet.t × list nat) :=
match l with
| nil ⇒ Some (O, O, LEMPTY, nil, ZSet.empty, nil)
| (TEVENT i e) :: l´ ⇒
match QS_CalLock l´ with
| Some (self_c, rel_c, b, q, slow, tq) ⇒
match q,tq with
| nil, nil ⇒
match e with
| TTICKET (SWAP_TAIL bound true) ⇒
Some (S bound, S CalPassLockTime, LHOLD, (i::nil), ZSet.empty, (bound::nil))
| _ ⇒ None
end
| i0 :: q´, p0 :: tq´ ⇒
if zeq i i0 then
match b, e with
| LHOLD, TTICKET GET_NEXT ⇒
match rel_c with
| O ⇒ None
| S rel_c´ ⇒ Some (self_c, rel_c´, b, q, slow, tq)
end
| LHOLD, TTICKET SET_BUSY ⇒
match rel_c with
| O ⇒ None
| S rel_c´ ⇒
if (negb (ZSet.mem i slow))
then Some (O, O, LEMPTY, q´, slow, tq´)
else None
end
| _, TTICKET (SET_NEXT _) ⇒
if ZSet.mem i slow
then Some (self_c, rel_c, b, q, ZSet.remove i slow, tq)
else None
| LHOLD, TSHARED _ ⇒
match self_c with
| O ⇒ None
| S self_c´ ⇒ Some (self_c´, rel_c, LHOLD, q, slow, tq)
end
| LEMPTY, TTICKET (GET_BUSY false) ⇒
Some (S p0, S CalPassLockTime, LHOLD, q, slow, tq)
| LHOLD, TTICKET (CAS_TAIL false) ⇒
match rel_c with
| O ⇒ None
| S rel_c´ ⇒ Some (self_c, rel_c´, b, q, slow, tq)
end
| LHOLD, TTICKET (CAS_TAIL true) ⇒
match q´ with
| nil ⇒ Some (O, O, LEMPTY, nil, ZSet.empty, nil)
| _ ⇒ None
end
| _, _ ⇒ None
end
else
match b, e with
| _, TTICKET (GET_BUSY true) ⇒
if ZSet.mem i slow
then None
else Some (self_c, rel_c, b, q, slow, tq)
| _, TTICKET (SET_NEXT _) ⇒
if ZSet.mem i slow
then Some (self_c, rel_c, b, q, ZSet.remove i slow, tq)
else None
| _, TTICKET (SWAP_TAIL bound false) ⇒
if in_dec zeq i q
then None
else Some (self_c, rel_c, b, q ++ (i::nil), ZSet.add i slow, tq++(bound::nil))
| _,_ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end
end.
Global Opaque QS_CalLock.
Fixpoint CalBound (j:Z) (l: MultiLog) : nat :=
match l with
| nil ⇒ fairness
| (TEVENT i e) :: l´ ⇒
match (CalBound j l´) with
| (S n´) ⇒
if zeq i j
then fairness
else n´
| O ⇒ O
end
end.
Lemma CalBound_upper_bound : ∀ j l, (CalBound j l ≤ fairness)%nat.
Proof.
induction l; simpl; intros.
+ auto.
+ destruct a.
destruct (CalBound j l); auto.
destruct (zeq i j); omega.
Qed.
Lemma CalBound_decreasing : ∀ j k e l,
j ≠ k → (0 < CalBound j l)%nat →
(CalBound j (TEVENT k e :: l) < CalBound j l)%nat.
Proof.
Local Transparent CalBound.
intros until 1.
simpl.
destruct (CalBound j l) as [|n].
auto.
rewrite zeq_false; auto.
Qed.
Lemma CalBound_inv : ∀ k e l,
(0 < CalBound k (e :: l))%nat →
(0 < CalBound k l)%nat.
Proof.
Transparent CalBound.
intros.
destruct e as [j e].
simpl in ×.
destruct (CalBound k l).
- omega.
- apply lt_0_Sn.
Qed.
Opaque CalBound.
Definition fair_log (l : MultiLog) :=
∀ j, (0 < CalBound j l)%nat.
End CAL_QS_LOCK.
Section CAL_QS_WAIT.
Context `{waittime: WaitTime}.
Fixpoint QS_CalWaitGet (n: nat) (i: Z) (l: MultiLog) (to: MultiOracle):=
match n with
| O ⇒ None
| S n´ ⇒
let l1 := (to i l) ++ l in
match QS_CalLock l1 with
| Some (_, b, q, _, _) ⇒
match q with
| e0 :: q´ ⇒
if (zeq e0 i)
then let l´ := (TEVENT i (TTICKET (GET_BUSY false))) :: l1 in
Some l´
else let l´ := (TEVENT i (TTICKET (GET_BUSY true))) :: l1 in
QS_CalWaitGet n´ i l´ to
| _⇒ None
end
| _ ⇒ None
end
end.
Global Opaque QS_CalWaitGet.
Fixpoint QS_CalWaitRel (n: nat) (i j: Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l1 := (to i l) ++ l in
match QS_CalLock l1 with
| Some (_, rel_c, _, _, slow,_) ⇒
if (ZSet.mem j slow)
then match rel_c with
| S _ ⇒ QS_CalWaitRel n´ i j ((TEVENT i (TTICKET GET_NEXT)) :: l1) to
| _ ⇒ None
end
else
match rel_c with
| (S (S _)) ⇒ Some l1
| _ ⇒ None
end
| _ ⇒ None
end
end.
Global Opaque QS_CalWaitRel.
End CAL_QS_WAIT.
Section MCS_Def_Invariant.
Context `{waittime: WaitTime}.
Definition not_head (i: Z) (l: list Z) :=
match l with
| nil ⇒ True
| i0 :: _ ⇒
if zeq i i0 then False
else True
end.
Definition MCSCorrect (node_value: Z) :=
0 ≤ node_value ≤ TOTAL_CPU.
Definition MCSCorrect_range (mcs: MCSLock) :=
∀ tl lock_arr bnd
(Hmcs: mcs = MCSLOCK tl lock_arr bnd),
0 ≤ tl ≤ TOTAL_CPU ∧
(∀ i , 0 ≤ i < TOTAL_CPU →
0 ≤ (snd (ZMap.get i lock_arr)) ≤ TOTAL_CPU).
Definition valid_MCS_log l :=
∀ mcs,
CalMCSLock l = Some mcs →
MCSCorrect_range mcs.
Definition valid_MCS_log_pool l :=
∀ i q (Hrange: 0 ≤ i < lock_range)
(Hdef: ZMap.get i l = MultiDef q),
valid_MCS_log q.
Definition valid_multi_oracle_mcs (o: MultiOracle) :=
∀ q i
(Hvalid: valid_MCS_log q),
valid_MCS_log ((o i q) ++ q).
Definition valid_multi_oracle_pool_mcs (o: MultiOraclePool):=
∀ i
(Hrange: 0 ≤ i < lock_range),
valid_multi_oracle_domain (ZMap.get i o)
∧ valid_multi_oracle_mcs (ZMap.get i o).
Definition valid_qslock (l: MultiLog) :=
∃ self_c rel_c b q slow tq, QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq).
Definition valid_qslock_pool (l: MultiLogPool):=
∀ i ofs r q
(Hrange: index2Z i ofs = Some r)
(Hdef: ZMap.get r l = MultiDef q),
valid_qslock q.
Definition correct_qslock_status (l: MultiLog) (k: LockStatus) (cpu: Z):=
∀ self_c rel_c b q tq slow
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
(k = LockFalse → ¬ In cpu q)
∧ (∀ lb, k = LockOwn lb → ∃ q´, q = cpu :: q´ ∧ b = LHOLD ∧ ¬ In cpu q´ ∧ (rel_c > CalPassLockTime)%nat ).
Definition correct_qslock_pool_status (l: MultiLogPool) (k: Lock) (cpu: Z):=
∀ i ofs r q
(Hrange: index2Z i ofs = Some r)
(Hdef: ZMap.get r l = MultiDef q),
correct_qslock_status q (ZMap.get r k) cpu.
Definition valid_qs_oracle (o: MultiOracle):=
∀ i l
self_c0 rel_c0 b0 q0 slow0 tq0
(Hin : QS_CalLock l = Some (self_c0, rel_c0, b0, q0, slow0, tq0))
,
∃ self_c rel_c b q slow tq,
QS_CalLock ((o i l) ++ l) = Some (self_c, rel_c, b, q, slow, tq)
∧ (∀ j, In j q0 → (0 < CalBound j (o i l ++ l))%nat ).
Definition valid_qs_oracle_pool (o: MultiOraclePool):=
∀ i ofs r
(Hrange: index2Z i ofs = Some r),
valid_multi_oracle_domain (ZMap.get r o)
∧ valid_qs_oracle (ZMap.get r o).
Definition get_free_qslock (l: MultiLog) :=
∀ k self_c other_c q slow tq
(Hcal: QS_CalLock l = Some (self_c, other_c, k, q, slow, tq))
(Hk: k = LEMPTY),
CalValidBit l = Some FreeToPull.
Definition get_free_qslock_pool (l: MultiLogPool) :=
∀ i ofs r q
(Hrange: index2Z i ofs = Some r)
(Hdef: ZMap.get r l = MultiDef q),
get_free_qslock q.
Definition get_free_qslock_oracle (o: MultiOracle):=
∀ i l
(Hget: get_free_qslock l),
get_free_qslock ((o i l) ++ l).
Definition get_free_qslock_oracle_pool (o: MultiOraclePool) :=
∀ i ofs r
(Hrange: index2Z i ofs = Some r),
get_free_qslock_oracle (ZMap.get r o).
End MCS_Def_Invariant.
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 GlobalOracle.
Require Import CalTicketLock.
Require Import LogReplay.
Require Import ZSet.
Opaque Z.of_nat Z.to_nat Z.to_pos.
Section CAL_MCS_LOCK.
Definition mcs_lock_st_size := ((TOTAL_CPU × (2 + 14) + (15 + 1)) × 4).
Definition mcs_node_st_size := 64.
Definition NULL := TOTAL_CPU.
Definition next_pos (lock_index curid : Z) : Z := ((mcs_lock_st_size × lock_index) + 64 + (mcs_node_st_size × curid)).
Definition busy_pos (lock_index curid : Z) : Z := ((mcs_lock_st_size × lock_index) + 64 + (mcs_node_st_size × curid) + 4).
Definition tail_pos (lock_index : Z) : Z := (mcs_lock_st_size × lock_index).
Hint Unfold mcs_lock_st_size mcs_node_st_size NULL next_pos busy_pos tail_pos.
Inductive MCSLock :=
| MCSLOCK (tail: Z) (lock_array: ZMap.t (bool × Z)) (bounds : list nat).
Definition init_MCSLock :=
MCSLOCK NULL (ZMap.init (false, NULL)) nil.
Fixpoint CalMCSLock (l: MultiLog):=
match l with
| nil ⇒ Some init_MCSLock
| (TEVENT i e) :: l´ ⇒
match CalMCSLock l´ with
| Some mcs ⇒
match e, mcs with
| TTICKET e´, MCSLOCK tail0 la bounds ⇒
match e´ with
| SWAP_TAIL p _ ⇒
Some (MCSLOCK i (ZMap.set i (true, NULL) la) (bounds ++ (p::nil)))
| GET_NEXT ⇒ Some mcs
| SET_NEXT old ⇒
match ZMap.get old la with
| (b, t) ⇒
Some (MCSLOCK tail0 (ZMap.set old (b, i) la) bounds)
end
| GET_BUSY _ ⇒ Some mcs
| SET_BUSY ⇒
match ZMap.get i la with
| (b, t) ⇒
match ZMap.get t la with
| (b´, t´) ⇒
Some (MCSLOCK tail0 (ZMap.set t (false, t´) la) (tl bounds))
end
end
| CAS_TAIL false ⇒ Some mcs
| CAS_TAIL true ⇒
if zeq tail0 i then
Some (MCSLOCK NULL la nil)
else None
| _ ⇒ None
end
| _, _ ⇒ Some mcs
end
| _ ⇒ None
end
end.
Global Opaque CalMCSLock.
End CAL_MCS_LOCK.
Section CAL_MCS_WAIT.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
Fixpoint CalMCS_AcqWait (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l´ := (to i l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK tail la _) ⇒
match ZMap.get i la with
| (false, _) ⇒ Some ((TEVENT i (TTICKET (GET_BUSY false))) :: l´)
| _ ⇒
CalMCS_AcqWait n´ i ((TEVENT i (TTICKET (GET_BUSY true))) ::l´) to
end
| _ ⇒ None
end
end.
Global Opaque CalMCS_AcqWait.
Fixpoint CalMCS_RelWait (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l1 := (TEVENT i (TTICKET GET_NEXT)) :: (to i l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK tail la _) ⇒
match ZMap.get i la with
| (_, p) ⇒ if zeq p NULL
then CalMCS_RelWait n´ i l1 to
else
match CalMCSLock (to i l1 ++ l1) with
| Some (MCSLOCK tail´ la´ _) ⇒
match ZMap.get i la´ with
| (_, p´) ⇒ if zeq p´ NULL then None
else Some ((TEVENT i (TTICKET SET_BUSY)) :: (to i l1 ++ l1))
end
| _ ⇒ None
end
end
| _ ⇒ None
end
end.
Global Opaque CalMCS_RelWait.
End WITHWAITTIME.
End CAL_MCS_WAIT.
Section CAL_BOUND_NUM.
Context `{waittime: WaitTime}.
Definition CalPassLockLoopTime :=
(S fairness)%nat.
Definition CalPassLockTime :=
(S CalPassLockLoopTime)%nat.
Fixpoint CalSumWait (l: list nat) :=
match l with
| nil ⇒ O
| a :: l´ ⇒ ((3 + CalPassLockTime + a) + CalSumWait l´) % nat
end.
Definition rm_head {A: Type} (l: list A) :=
match l with
| nil ⇒ nil
| _ :: l´ ⇒ l´
end.
Definition WaitConstant : nat := (2 + CalPassLockTime)%nat.
Lemma WaitConstant_fairness : (fairness < WaitConstant)%nat.
unfold WaitConstant, CalPassLockTime, CalPassLockLoopTime.
omega.
Qed.
Lemma WaitConstant_PassLockTime : (S CalPassLockTime < WaitConstant)%nat.
unfold WaitConstant, CalPassLockTime.
simpl.
omega.
Qed.
Global Opaque WaitConstant.
Definition CalWaitLockTime (tq: list nat) :=
((5 + WaitConstant + length tq + (CalSumWait tq)) × WaitConstant)%nat.
End CAL_BOUND_NUM.
Section CAL_QS_LOCK.
Context `{waittime: WaitTime}.
Require Import ZSet.
Fixpoint QS_CalLock (l: MultiLog) : option (nat × nat × head_status × list Z × ZSet.t × list nat) :=
match l with
| nil ⇒ Some (O, O, LEMPTY, nil, ZSet.empty, nil)
| (TEVENT i e) :: l´ ⇒
match QS_CalLock l´ with
| Some (self_c, rel_c, b, q, slow, tq) ⇒
match q,tq with
| nil, nil ⇒
match e with
| TTICKET (SWAP_TAIL bound true) ⇒
Some (S bound, S CalPassLockTime, LHOLD, (i::nil), ZSet.empty, (bound::nil))
| _ ⇒ None
end
| i0 :: q´, p0 :: tq´ ⇒
if zeq i i0 then
match b, e with
| LHOLD, TTICKET GET_NEXT ⇒
match rel_c with
| O ⇒ None
| S rel_c´ ⇒ Some (self_c, rel_c´, b, q, slow, tq)
end
| LHOLD, TTICKET SET_BUSY ⇒
match rel_c with
| O ⇒ None
| S rel_c´ ⇒
if (negb (ZSet.mem i slow))
then Some (O, O, LEMPTY, q´, slow, tq´)
else None
end
| _, TTICKET (SET_NEXT _) ⇒
if ZSet.mem i slow
then Some (self_c, rel_c, b, q, ZSet.remove i slow, tq)
else None
| LHOLD, TSHARED _ ⇒
match self_c with
| O ⇒ None
| S self_c´ ⇒ Some (self_c´, rel_c, LHOLD, q, slow, tq)
end
| LEMPTY, TTICKET (GET_BUSY false) ⇒
Some (S p0, S CalPassLockTime, LHOLD, q, slow, tq)
| LHOLD, TTICKET (CAS_TAIL false) ⇒
match rel_c with
| O ⇒ None
| S rel_c´ ⇒ Some (self_c, rel_c´, b, q, slow, tq)
end
| LHOLD, TTICKET (CAS_TAIL true) ⇒
match q´ with
| nil ⇒ Some (O, O, LEMPTY, nil, ZSet.empty, nil)
| _ ⇒ None
end
| _, _ ⇒ None
end
else
match b, e with
| _, TTICKET (GET_BUSY true) ⇒
if ZSet.mem i slow
then None
else Some (self_c, rel_c, b, q, slow, tq)
| _, TTICKET (SET_NEXT _) ⇒
if ZSet.mem i slow
then Some (self_c, rel_c, b, q, ZSet.remove i slow, tq)
else None
| _, TTICKET (SWAP_TAIL bound false) ⇒
if in_dec zeq i q
then None
else Some (self_c, rel_c, b, q ++ (i::nil), ZSet.add i slow, tq++(bound::nil))
| _,_ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end
end.
Global Opaque QS_CalLock.
Fixpoint CalBound (j:Z) (l: MultiLog) : nat :=
match l with
| nil ⇒ fairness
| (TEVENT i e) :: l´ ⇒
match (CalBound j l´) with
| (S n´) ⇒
if zeq i j
then fairness
else n´
| O ⇒ O
end
end.
Lemma CalBound_upper_bound : ∀ j l, (CalBound j l ≤ fairness)%nat.
Proof.
induction l; simpl; intros.
+ auto.
+ destruct a.
destruct (CalBound j l); auto.
destruct (zeq i j); omega.
Qed.
Lemma CalBound_decreasing : ∀ j k e l,
j ≠ k → (0 < CalBound j l)%nat →
(CalBound j (TEVENT k e :: l) < CalBound j l)%nat.
Proof.
Local Transparent CalBound.
intros until 1.
simpl.
destruct (CalBound j l) as [|n].
auto.
rewrite zeq_false; auto.
Qed.
Lemma CalBound_inv : ∀ k e l,
(0 < CalBound k (e :: l))%nat →
(0 < CalBound k l)%nat.
Proof.
Transparent CalBound.
intros.
destruct e as [j e].
simpl in ×.
destruct (CalBound k l).
- omega.
- apply lt_0_Sn.
Qed.
Opaque CalBound.
Definition fair_log (l : MultiLog) :=
∀ j, (0 < CalBound j l)%nat.
End CAL_QS_LOCK.
Section CAL_QS_WAIT.
Context `{waittime: WaitTime}.
Fixpoint QS_CalWaitGet (n: nat) (i: Z) (l: MultiLog) (to: MultiOracle):=
match n with
| O ⇒ None
| S n´ ⇒
let l1 := (to i l) ++ l in
match QS_CalLock l1 with
| Some (_, b, q, _, _) ⇒
match q with
| e0 :: q´ ⇒
if (zeq e0 i)
then let l´ := (TEVENT i (TTICKET (GET_BUSY false))) :: l1 in
Some l´
else let l´ := (TEVENT i (TTICKET (GET_BUSY true))) :: l1 in
QS_CalWaitGet n´ i l´ to
| _⇒ None
end
| _ ⇒ None
end
end.
Global Opaque QS_CalWaitGet.
Fixpoint QS_CalWaitRel (n: nat) (i j: Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l1 := (to i l) ++ l in
match QS_CalLock l1 with
| Some (_, rel_c, _, _, slow,_) ⇒
if (ZSet.mem j slow)
then match rel_c with
| S _ ⇒ QS_CalWaitRel n´ i j ((TEVENT i (TTICKET GET_NEXT)) :: l1) to
| _ ⇒ None
end
else
match rel_c with
| (S (S _)) ⇒ Some l1
| _ ⇒ None
end
| _ ⇒ None
end
end.
Global Opaque QS_CalWaitRel.
End CAL_QS_WAIT.
Section MCS_Def_Invariant.
Context `{waittime: WaitTime}.
Definition not_head (i: Z) (l: list Z) :=
match l with
| nil ⇒ True
| i0 :: _ ⇒
if zeq i i0 then False
else True
end.
Definition MCSCorrect (node_value: Z) :=
0 ≤ node_value ≤ TOTAL_CPU.
Definition MCSCorrect_range (mcs: MCSLock) :=
∀ tl lock_arr bnd
(Hmcs: mcs = MCSLOCK tl lock_arr bnd),
0 ≤ tl ≤ TOTAL_CPU ∧
(∀ i , 0 ≤ i < TOTAL_CPU →
0 ≤ (snd (ZMap.get i lock_arr)) ≤ TOTAL_CPU).
Definition valid_MCS_log l :=
∀ mcs,
CalMCSLock l = Some mcs →
MCSCorrect_range mcs.
Definition valid_MCS_log_pool l :=
∀ i q (Hrange: 0 ≤ i < lock_range)
(Hdef: ZMap.get i l = MultiDef q),
valid_MCS_log q.
Definition valid_multi_oracle_mcs (o: MultiOracle) :=
∀ q i
(Hvalid: valid_MCS_log q),
valid_MCS_log ((o i q) ++ q).
Definition valid_multi_oracle_pool_mcs (o: MultiOraclePool):=
∀ i
(Hrange: 0 ≤ i < lock_range),
valid_multi_oracle_domain (ZMap.get i o)
∧ valid_multi_oracle_mcs (ZMap.get i o).
Definition valid_qslock (l: MultiLog) :=
∃ self_c rel_c b q slow tq, QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq).
Definition valid_qslock_pool (l: MultiLogPool):=
∀ i ofs r q
(Hrange: index2Z i ofs = Some r)
(Hdef: ZMap.get r l = MultiDef q),
valid_qslock q.
Definition correct_qslock_status (l: MultiLog) (k: LockStatus) (cpu: Z):=
∀ self_c rel_c b q tq slow
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
(k = LockFalse → ¬ In cpu q)
∧ (∀ lb, k = LockOwn lb → ∃ q´, q = cpu :: q´ ∧ b = LHOLD ∧ ¬ In cpu q´ ∧ (rel_c > CalPassLockTime)%nat ).
Definition correct_qslock_pool_status (l: MultiLogPool) (k: Lock) (cpu: Z):=
∀ i ofs r q
(Hrange: index2Z i ofs = Some r)
(Hdef: ZMap.get r l = MultiDef q),
correct_qslock_status q (ZMap.get r k) cpu.
Definition valid_qs_oracle (o: MultiOracle):=
∀ i l
self_c0 rel_c0 b0 q0 slow0 tq0
(Hin : QS_CalLock l = Some (self_c0, rel_c0, b0, q0, slow0, tq0))
,
∃ self_c rel_c b q slow tq,
QS_CalLock ((o i l) ++ l) = Some (self_c, rel_c, b, q, slow, tq)
∧ (∀ j, In j q0 → (0 < CalBound j (o i l ++ l))%nat ).
Definition valid_qs_oracle_pool (o: MultiOraclePool):=
∀ i ofs r
(Hrange: index2Z i ofs = Some r),
valid_multi_oracle_domain (ZMap.get r o)
∧ valid_qs_oracle (ZMap.get r o).
Definition get_free_qslock (l: MultiLog) :=
∀ k self_c other_c q slow tq
(Hcal: QS_CalLock l = Some (self_c, other_c, k, q, slow, tq))
(Hk: k = LEMPTY),
CalValidBit l = Some FreeToPull.
Definition get_free_qslock_pool (l: MultiLogPool) :=
∀ i ofs r q
(Hrange: index2Z i ofs = Some r)
(Hdef: ZMap.get r l = MultiDef q),
get_free_qslock q.
Definition get_free_qslock_oracle (o: MultiOracle):=
∀ i l
(Hget: get_free_qslock l),
get_free_qslock ((o i l) ++ l).
Definition get_free_qslock_oracle_pool (o: MultiOraclePool) :=
∀ i ofs r
(Hrange: index2Z i ofs = Some r),
get_free_qslock_oracle (ZMap.get r o).
End MCS_Def_Invariant.