Library mcertikos.ticketlog.StarvationFreedomTicketLock
This file provide the contextual refinement proof between MALInit layer and MALOp layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import HTicketLockOpGenDef.
Require Import TacticsForTesting.
Require Import DeviceStateDataType.
Require Import CalTicketLock.
Require Import ListLemma2.
Require Export MQTicketLockOp.
Require Export MHTicketLockOp.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import HTicketLockOpGenDef.
Require Import TacticsForTesting.
Require Import DeviceStateDataType.
Require Import CalTicketLock.
Require Import ListLemma2.
Require Export MQTicketLockOp.
Require Export MHTicketLockOp.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mqticketlockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Lemma relate_log_shared:
∀ l1 l0 tq
(Hre: HTicketLockOpGenDef.relate_log l1 = Some (l0, tq)),
GetSharedMemEvent l0 = GetSharedMemEvent l1.
Proof.
induction l1; simpl; intros.
- inv Hre. trivial.
- subdestruct; inv Hre; simpl; eauto.
destruct e0; eauto.
Qed.
Lemma relate_ticket_log_pool_gss:
∀ l l´ o o´ p
(Hrelate_log: relate_ticket_log_type l l´)
(Hrelate:relate_ticket_log_pool o o´),
relate_ticket_log_pool (ZMap.set p l o)
(ZMap.set p l´ o´).
Proof.
intros. constructor. intros.
destruct (zeq p z); subst.
- repeat rewrite ZMap.gss. trivial.
- inv Hrelate. repeat rewrite ZMap.gso; eauto.
Qed.
Lemma relate_ticket_log_shared:
∀ curid l l´ tq e
(Hlog: HTicketLockOpGenDef.relate_log l = Some (l´, tq)),
HTicketLockOpGenDef.relate_log (TEVENT curid (TSHARED e) :: l) =
Some (TEVENT curid (TSHARED e) :: l´, tq).
Proof.
intros. simpl. rewrite Hlog. trivial.
Qed.
Lemma relate_ticket_log_pool_shared:
∀ curid p l l´ t t´ tq e
(Hlog: HTicketLockOpGenDef.relate_log l´ = Some (l,tq))
(Hlog_pool: relate_ticket_log_pool t t´),
relate_ticket_log_pool
(ZMap.set p (MultiDef (TEVENT curid (TSHARED e) :: l)) t)
(ZMap.set p (MultiDef (TEVENT curid (TSHARED e) :: l´)) t´).
Proof.
intros. eapply relate_ticket_log_pool_gss; eauto.
econstructor. eapply relate_ticket_log_shared; eauto.
Qed.
Lemma real_ticket_relate_pb:
∀ n l l´ z
(Hrelate_ticket_log_type : relate_ticket_log_type
(ZMap.get z l) (ZMap.get z l´)),
relate_ticket_log_type
(ZMap.get z (real_multi_log_pb n l))
(ZMap.get z (real_multi_log_pb n l´)).
Proof.
induction n; intros; simpl; trivial.
destruct (zeq z (Z.of_nat n)); subst.
- repeat rewrite ZMap.gss. econstructor. simpl. trivial.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_ticket_relate:
∀ l l´
(Hrelate: relate_ticket_log_pool l l´),
relate_ticket_log_pool (real_multi_log l)
(real_multi_log l´).
Proof.
intros. constructor. intros. inv Hrelate.
specialize (Hrelate_ticket_log_type _ _ _ Hrange).
unfold real_multi_log.
eapply real_ticket_relate_pb; eauto.
Qed.
Section WITH_WAIT.
Local Transparent Q_CalLock Q_CalWait.
Lemma Q_CalLock_q_length_same:
∀ l self_c other_c b q tq
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
length tq = length q.
Proof.
induction l; simpl; intros.
- inv HCal. trivial.
- subdestruct; inv HCal;
exploit IHl; eauto.
+ intros.
repeat rewrite app_comm_cons.
repeat rewrite app_length.
rewrite H. simpl; trivial.
Qed.
Lemma list_head_case:
∀ {A: Type} q´ q q0 (z z0: A)
(Heq: z :: q = q´ ++ z0 :: q0),
(z = z0 ∧ q´ = nil ∧ q0 = q)
∨ (∃ q1, q´ = z :: q1 ∧ q = q1 ++ z0 :: q0).
Proof.
induction q´; simpl; intros.
- inv Heq. left. eauto.
- destruct q.
+ inv Heq.
symmetry in H1. apply list_not_e_nil in H1. inv H1.
+ inv Heq. exploit IHq´; eauto.
Qed.
Lemma CalLock_length:
∀ l´ l tq q self_c self_c´ other_c other_c´ b b´ z bound q0 q1 q´ tq0 tq´´
(Hlen: length tq = length q)
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q ++ z :: q0, tq ++ bound :: tq0))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z ∨ (∀ n, e ≠ TTICKET (INC_TICKET n)))
(Hqlock0: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, q´ ++ z :: q1, tq´´))
(Hnin: ¬ In z q)
(Hnin0: ¬ In z q0),
∃ tq´ tq1, tq´´ = tq´ ++ bound :: tq1 ∧ length tq´ = length q´.
Proof.
induction l´; simpl; intros.
- rewrite Hqlock in Hqlock0. inv Hqlock0.
refine_split´; trivial.
eapply list_unique_element in H3; eauto.
destruct H3 as (? & ?); subst. trivial.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ z ∨ (∀ n, e ≠ TTICKET (INC_TICKET n))).
{ eapply list_valid_In_append´; eauto. }
subdestruct; inv Hqlock0; try (rewrite H3 in Hdestruct0; exploit IHl´; eauto).
+ destruct q´; inv H3.
× specialize (Hin z (TTICKET (INC_TICKET n1))).
elim Hin.
{ intros HF; elim HF; trivial. }
{ intros HF. specialize (HF n1). elim HF. trivial. }
left; trivial.
× symmetry in H1.
eapply list_not_e_nil in H1.
inv H1.
+ rewrite app_comm_cons in Hdestruct0.
exploit IHl´; try eassumption.
intros (tq´ & tq1 & Heq1 & Hlen1).
destruct tq´.
× inv Hlen1.
× rewrite <- app_comm_cons in Heq1.
inv Heq1. inv Hlen1.
refine_split´; trivial.
+ rewrite app_comm_cons in H3.
eapply list_tail_one_element in H3.
destruct H3 as [(? & ?) | HF]; subst.
{
specialize (Hin z (TTICKET (INC_TICKET n5))).
elim Hin.
{ intros HF; elim HF; trivial. }
{ intros HF. specialize (HF n5). elim HF. trivial. }
left; trivial.
}
{
destruct HF as (l2´ & Heq).
rewrite Heq in Hdestruct0.
rewrite app_comm_cons.
exploit IHl´; eauto.
intros (tq´ & tq1 & → & Hlen1).
rewrite <- app_assoc.
rewrite <- app_comm_cons.
refine_split´; trivial.
}
Qed.
Lemma Q_CalLock_relate_log_exists:
∀ l self_c other_c b q tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
∃ l´, HTicketLockOpGenDef.relate_log l = Some (l´, tq).
Proof.
induction l; simpl; intros.
- inv Hcal. refine_split´; trivial.
- subdestruct; inv Hcal;
(exploit IHl; eauto; intros (l´ & ->);
refine_split´; trivial).
Qed.
Lemma Q_CalLock_relate_log_eq:
∀ l l´ self_c other_c b q tq tq´
(Hre: HTicketLockOpGenDef.relate_log l = Some (l´, tq))
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq´)),
tq = tq´.
Proof.
intros.
eapply Q_CalLock_relate_log_exists in Hcal.
destruct Hcal as (l0 & Heq).
rewrite Hre in Heq. inv Heq.
trivial.
Qed.
Lemma Q_CalLock_GET_NOW_imply:
∀ curid l self_c other_c b q tq,
Q_CalLock (TEVENT curid (TTICKET GET_NOW) :: l) = Some (self_c, other_c, b, curid :: q, tq) →
b = LGET.
Proof.
simpl; intros.
subdestruct; inversion H; try subst; eauto; try congruence.
Qed.
Lemma CalWait_exists:
∀ wait_time curid l o l0
(Hwait: Q_CalWait wait_time curid l o = Some l0),
∃ self_c other_c q tq, Q_CalLock l0 = Some (self_c, other_c, LGET, curid :: q, tq)
.
Proof.
Local Opaque Q_CalLock.
induction wait_time; simpl; intros; try (inv Hwait; fail).
subdestruct; try inv Hwait; eauto.
exploit Q_CalLock_GET_NOW_imply; eauto.
intros; subst.
refine_split´; eauto.
Qed.
Lemma CalWait_exists_log:
∀ wait_time curid l o l0
(Hwait: Q_CalWait wait_time curid l o = Some l0)
(Horacle_domain : valid_multi_oracle_domain o),
∃ l´, l0 = l´ ++ l
∧ (∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ curid ∨ (∀ n, e ≠ TTICKET (INC_TICKET n))).
Proof.
Local Opaque Q_CalLock.
induction wait_time; simpl; intros; try (inv Hwait; fail).
subdestruct; try inv Hwait; eauto.
- rewrite app_comm_cons.
refine_split´; eauto. intros.
inv H.
+ right. inv H0. intros. intro HF; inv HF.
+ left. eapply Horacle_domain in H0; eauto. eapply H0.
- exploit IHwait_time; eauto.
intros (l´ & ? & Hp); subst.
rewrite app_comm_cons.
rewrite app_assoc.
refine_split´; eauto.
intros.
eapply in_app_or in H.
destruct H as [Hin | Hin]; auto.
inv Hin.
+ right. inv H. intros. intro HF; inv HF.
+ eapply Horacle_domain in H; eauto.
left. eapply H.
Qed.
Lemma relate_ticket_log_pool_REL:
∀ curid p l l0 l´ t t´ tq tq0
(Hlog: HTicketLockOpGenDef.relate_log l´ = Some (l, tq))
(Hlog´: HTicketLockOpGenDef.relate_log (TEVENT curid (TTICKET INC_NOW) :: l´) = Some (l0, tq0))
(Hlog_pool: relate_ticket_log_pool t t´),
relate_ticket_log_pool
(ZMap.set p (MultiDef (TEVENT curid (TTICKET REL_LOCK) :: l)) t)
(ZMap.set p (MultiDef (TEVENT curid (TTICKET INC_NOW) :: l´)) t´).
Proof.
intros. eapply relate_ticket_log_pool_gss; eauto.
econstructor. simpl in ×. rewrite Hlog in ×.
destruct tq; contra_inv. inv Hlog´. trivial.
Qed.
Local Transparent Q_CalLock.
Lemma Q_CalLock_HOLD_LOCK_exists:
∀ wait_time c l o l0
(Hwait: Q_CalWait wait_time c l o = Some l0),
∃ x,
Q_CalLock (TEVENT c (TTICKET HOLD_LOCK) :: l0) = Some x.
Proof.
simpl; intros.
eapply CalWait_exists in Hwait.
destruct Hwait as (self_c & other_c & q & tq & Hcal).
rewrite Hcal.
exploit Q_CalLock_q_length_same; eauto. intros.
destruct tq; inv H.
rewrite zeq_true. eauto.
Qed.
Lemma Q_CalLock_INC_TICKET_exists:
∀ l self_c other_c b q tq n c
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hnin: ¬ In c q)
(Hpos: other_c ≠ O),
∃ x,
Q_CalLock (TEVENT c (TTICKET (INC_TICKET n)) :: l) = Some x.
Proof.
simpl; intros. rewrite HCal.
exploit Q_CalLock_q_length_same; eauto. intros.
destruct q.
- destruct tq; inv H. eauto.
- destruct tq; inv H.
destruct (zeq c z); subst.
+ elim Hnin. left; trivial.
+ destruct other_c.
× elim Hpos. trivial.
× destruct (in_dec zeq c q); eauto.
elim Hnin. right; trivial.
Qed.
Lemma Q_CalLock_oracle_not_In:
∀ l´ l self_c other_c b q tq self_c´ other_c´ b´ q´ tq´ c
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ c)
(Hnin: ¬ In c q)
(HCal´: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, q´, tq´)),
¬ In c q´.
Proof.
induction l´; simpl; intros.
- rewrite HCal in HCal´. inv HCal´. trivial.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ c).
{ eapply list_valid_In_append; eauto. }
subdestruct; inv HCal´; try (eapply (IHl´ l); eauto; fail).
+ specialize (Hin i (TTICKET (INC_TICKET n1))).
red; intros. simpl in H. destruct H as [HF|HF]; inv HF.
elim Hin. left; trivial. trivial.
+ red; intro. exploit (IHl´ l); eauto.
right. trivial.
+ red; intro HF. exploit (IHl´ l); eauto.
rewrite app_comm_cons in HF.
eapply in_app_or in HF.
destruct HF as [HF´ | HF´]; trivial.
destruct HF´ as [HF|HF]; inv HF.
specialize (Hin c (TTICKET (INC_TICKET n5))).
elim Hin; trivial. left; trivial.
Qed.
Lemma Q_CalLock_oracle:
∀ l self_c other_c b q tq c o
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_multi_oracle_queue o)
(Hin´: ∀ i1 e1,
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast: match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hnin: ¬ In c q),
∃ self_c´ other_c´ b´ q´ tq´,
Q_CalLock (o c l ++ l) = Some (self_c´, other_c´, b´, q´, tq´)
∧ ¬ In c q´
∧ other_c´ ≠ O.
Proof.
intros.
destruct Horacle_domain as (Horacle_domain0 & Horacle_domain1).
unfold valid_multi_oracle_queue in ×.
specialize (Horacle_domain1 c l).
exploit Horacle_domain1; eauto.
{
unfold valid_qlock.
rewrite HCal. refine_split´; trivial.
}
intros (self_c´ & other_c´ & b´ & q´ & tq´ & HCal´ & Hnhead).
assert (HnotIn: ¬ In c q´).
{
eapply (Q_CalLock_oracle_not_In (o c l) l); eauto.
intros. eapply Horacle_domain0; eauto.
}
refine_split´; eauto.
Qed.
Lemma Q_CalLock_INC_TICKET_exists´:
∀ l self_c other_c b q tq n c o
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_multi_oracle_queue o)
(Hin´: ∀ i1 e1,
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast: match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hnin: ¬ In c q),
∃ x,
Q_CalLock (TEVENT c (TTICKET (INC_TICKET n)) :: (o c l ++ l)) = Some x.
Proof.
intros.
exploit Q_CalLock_oracle; eauto.
intros (self_c´ & other_c´ & b´ & q´ & tq´ & HCal´ & HnotIn & Hother).
eapply Q_CalLock_INC_TICKET_exists; eauto.
Qed.
Lemma Q_CalLock_INC_NOW_exists:
∀ l self_c other_c q tq c q´
(HCal: Q_CalLock l = Some (self_c, other_c, LHOLD, q, tq))
(HinQ: q = c :: q´)
,
∃ x,
Q_CalLock (TEVENT c (TTICKET (INC_NOW)) :: l) = Some x.
Proof.
simpl; intros. rewrite HCal. subst.
exploit Q_CalLock_q_length_same; eauto. intros.
destruct tq; inv H.
rewrite zeq_true. eauto.
Qed.
Lemma O_gt_false:
∀ n (Hgt: (O > n)%nat),
False.
Proof.
intros. destruct n; omega.
Qed.
Lemma add_mult_assoc:
∀ (a b c: nat),
(a × c + b × c = (a + b) × c)%nat.
Proof.
induction a.
- simpl. trivial.
- simpl. intros. rewrite <- (IHa b c).
xomega.
Qed.
Lemma lt_plus_trans´ n m p : (n < m → n < p + m)%nat.
Proof.
erewrite (plus_comm p).
eapply lt_plus_trans.
Qed.
Lemma le_plus_trans´ n m p : (n ≤ m → n ≤ p + m)%nat.
Proof.
erewrite (plus_comm p).
eapply le_plus_trans.
Qed.
Lemma lt_less_plus n m p : (n < m → p + n < p + m)%nat.
Proof.
omega.
Qed.
Lemma lt_plus_r n m : 0 < n → m < n + m.
Proof.
omega.
Qed.
Lemma CalLock_progress:
∀ l´ l tq q self_c self_c´ other_c other_c´ b b´ z bound q0 tq0 lq ltq
(Hlen: length tq = length q)
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q ++ z :: q0, tq ++ bound :: tq0))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z )
(Hnin: ¬ In z q)
(HCal: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, lq, ltq)),
∃ q´ q´´ q1 tq´ tq´´ tq1,
lq = q´´ ++ z :: q1
∧ ltq = tq´´++ bound :: tq1
∧ q = q´ ++ q´´
∧ tq = tq´ ++ tq´´
∧ length tq´´ = length q´´
∧ (decrease_number self_c´ other_c´ b´ tq´´ ≤
decrease_number self_c other_c b tq)%nat.
Proof.
induction l´; simpl; intros.
- ∃ nil, q, q0, nil, tq, tq0.
rewrite Hqlock in HCal. inv HCal. refine_split´; eauto.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ z ∨ e = TTICKET GET_NOW).
{ eapply list_valid_In_append´; eauto. }
destruct a.
subdestruct; inv HCal; try (exploit IHl´; eauto);
intros (q´ & q´´ & q1 & tq´ & tq´´ & tq1 & Hlq & Hltq & Hq & htq & Hlen´ & Hdec); subst.
+ symmetry in Hlq.
apply list_not_e_nil in Hlq. inv Hlq.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
simpl.
eapply list_head_case in Hlq.
destruct Hlq as [(? & ? & ?)| (q2 & ? & ?)]; subst.
{
specialize (Hin z (TTICKET GET_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
}
eapply list_head_case in Hltq.
destruct Hltq as [(? & ? & ?)| (tq2 & ? & ?)]; subst.
{ inv Hlen´. }
simpl. apply le_plus_trans´.
repeat rewrite mult_plus_distr_r. omega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
simpl.
repeat rewrite mult_plus_distr_r. omega.
+ eapply list_head_case in Hlq.
destruct Hlq as [(? & ? & ?)| (q2 & ? & ?)]; subst.
{
specialize (Hin z (TTICKET INC_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
}
eapply list_head_case in Hltq.
destruct Hltq as [(? & ? & ?)| (tq2 & ? & ?)]; subst.
{ inv Hlen´. }
∃ (q´ ++ z0 :: nil), q2, q1, (tq´ ++ n :: nil), tq2, tq1.
refine_split´; eauto.
× rewrite <- app_assoc.
rewrite <- app_comm_cons. simpl. trivial.
× rewrite <- app_assoc.
rewrite <- app_comm_cons. simpl. trivial.
× etransitivity; try eapply Hdec.
simpl.
etransitivity.
instantiate (1:=((n0 + HTicketLockOpGenDef.CalSumWait tq2 + 1) × fairness)%nat).
etransitivity.
instantiate (1:=((HTicketLockOpGenDef.CalSumWait tq2 + 1) × fairness)%nat).
repeat rewrite mult_plus_distr_r. omega.
repeat rewrite <- add_mult_assoc.
rewrite plus_assoc_reverse. xomega. xomega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
simpl. omega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
unfold decrease_number.
destruct b´; omega.
+ subst.
∃ q´, q´´, (q1 ++ i::nil), tq´, tq´´, (tq1 ++ n5 :: nil).
refine_split´; eauto.
× repeat rewrite app_comm_cons.
rewrite Hlq.
rewrite <- app_assoc. trivial.
× repeat rewrite app_comm_cons.
rewrite Hltq.
rewrite <- app_assoc. trivial.
× etransitivity; try eapply Hdec.
destruct b´; simpl; omega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
unfold decrease_number.
destruct b´; omega.
Qed.
Lemma CalLock_progress_GET_NOW:
∀ l tq q self_c self_c´ other_c other_c´ b b´ c n tq´
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q, tq++n::tq´))
(HCal: Q_CalLock (TEVENT c (TTICKET GET_NOW):: l) =
Some (self_c´, other_c´, b´, q, tq++n::tq´))
(Hneq: tq ≠ nil),
(decrease_number self_c´ other_c´ b´ tq <
decrease_number self_c other_c b tq)%nat.
Proof.
simpl; intros. rewrite Hqlock in HCal.
subdestruct; inv HCal; simpl.
- symmetry in Hdestruct.
eapply list_head_case in Hdestruct.
destruct Hdestruct as [(? & ? & ?)| (tq2 & ? & ?)]; subst.
{ elim Hneq. trivial. }
simpl.
apply lt_plus_trans´.
pose positive_fairness.
repeat rewrite mult_plus_distr_r. omega.
- destruct b´; simpl; omega.
Qed.
Local Transparent H_CalLock.
Lemma Q_CalLock_nil:
∀ l self_c other_c b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, nil, tq)),
b = LEMPTY.
Proof.
induction l; simpl; intros.
- inv Hcal. trivial.
- subdestruct; inv Hcal; trivial.
Qed.
Lemma Q_CalLock_get:
∀ l self_c other_c q b head tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, head :: tq)),
match b with
| LGET ⇒ head = self_c
| _ ⇒ True
end.
Proof.
induction l; simpl; intros.
- inv Hcal.
- subdestruct; inv Hcal; trivial.
+ destruct b; trivial.
exploit IHl; eauto.
+ destruct b; trivial.
exploit IHl; eauto.
+ destruct b; trivial.
exploit IHl; eauto.
Qed.
Definition get_head_lock (l: list Z) (b: head_status):=
match b with
| LHOLD ⇒
match l with
| nil ⇒ None
| a :: _ ⇒ Some a
end
| _ ⇒ None
end.
Lemma Q_CalLock_relate_log:
∀ l l´ self_c self_c´ other_c b b´ q tq tq0 h
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hcal´: H_CalLock l´ = Some (self_c´, b´, h))
(Hre: HTicketLockOpGenDef.relate_log l = Some (l´, tq0)),
match b with
| LGET ⇒ True
| _ ⇒ self_c´ = self_c
end
∧ match b with
| LHOLD ⇒ b´ = LHOLD
| _ ⇒ b´ = LEMPTY
end
∧ h = get_head_lock q b.
Proof.
induction l; simpl; intros.
- inv Hcal. inv Hre. inv Hcal´. simpl; eauto.
- destruct a. destruct (HTicketLockOpGenDef.relate_log l) eqn: Hre´; contra_inv.
destruct (Q_CalLock l) eqn: Hcal0´; contra_inv.
destruct p. destruct p0. repeat destruct p.
exploit Q_CalLock_relate_log_exists; eauto.
rewrite Hre´. intros (l´0 & Heq). inv Heq.
destruct l2; contra_inv.
+ destruct l1; contra_inv.
destruct e; contra_inv.
destruct e; contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto.
eapply Q_CalLock_nil in Hcal0´. subst. trivial.
+ destruct l1; contra_inv.
destruct (zeq i z); contra_inv.
× destruct h0; contra_inv.
{
destruct e; contra_inv.
destruct e; contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto. simpl.
intros (? & ? & ?).
refine_split´; eauto.
}
{
destruct e; contra_inv.
destruct e; contra_inv.
inv Hcal. inv Hre.
simpl in Hcal´.
destruct (H_CalLock l´0) eqn: Hcal0; contra_inv.
repeat destruct p.
destruct h0; contra_inv.
- destruct o; contra_inv.
inv Hcal´.
eapply Q_CalLock_get in Hcal0´.
inv Hcal0´. eauto.
- destruct o; contra_inv.
destruct (zeq z z0); contra_inv.
}
{
destruct e; contra_inv.
- destruct e; contra_inv.
inv Hcal. inv Hre.
simpl in Hcal´.
destruct (H_CalLock l´0) eqn: Hcal0; contra_inv.
repeat destruct p.
destruct h0; contra_inv.
+ destruct o; contra_inv.
+ destruct o; contra_inv.
destruct (zeq z z0); contra_inv.
inv Hcal´. eauto.
- destruct n; contra_inv. inv Hcal. inv Hre.
simpl in Hcal´.
destruct (H_CalLock l´0) eqn: Hcal0; contra_inv.
repeat destruct p.
destruct h0; contra_inv.
+ destruct o; contra_inv.
+ destruct o; contra_inv.
destruct (zeq z z0); contra_inv.
destruct n; contra_inv. inv Hcal´.
exploit IHl; eauto.
simpl. intros (? & _).
refine_split´; eauto.
}
× destruct n0; contra_inv.
destruct e; contra_inv.
destruct e; contra_inv.
{
destruct (in_dec zeq i l2); contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto.
}
{
inv Hre. inv Hcal.
exploit IHl; eauto.
}
Qed.
Lemma CalSumWait_append:
∀ l l´,
HTicketLockOpGenDef.CalSumWait (l ++ l´)
= (HTicketLockOpGenDef.CalSumWait (l) + HTicketLockOpGenDef.CalSumWait (l´)) % nat.
Proof.
induction l; simpl; intros; trivial.
rewrite IHl. omega.
Qed.
Lemma Q_CalLock_other_c:
∀ l self_c other_c q b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
(other_c ≤ fairness)%nat.
Proof.
induction l; simpl; intros.
- inv Hcal. trivial.
- subdestruct; inv Hcal; trivial; exploit IHl; eauto; intros; try omega.
Qed.
Lemma Q_CalLock_self_c:
∀ l self_c other_c q b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
match tq with
| nil ⇒ self_c = O
| a :: _ ⇒ (self_c ≤ a)%nat
end.
Proof.
induction l; simpl; intros.
- inv Hcal. trivial.
- subdestruct; inv Hcal; trivial; exploit IHl; eauto; intros Hs.
+ simpl in Hs. subst. omega.
+ destruct tq; omega.
+ simpl in Hs. omega.
Qed.
Lemma Q_CalLock_INC_TICKET_status:
∀ l self_c other_c q b tq self_c´ other_c´ q´ b´ tq´ c n
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hcal´: Q_CalLock (TEVENT c (TTICKET (INC_TICKET n)) :: l) = Some (self_c´, other_c´, b´, q´, tq´)),
match q with
| nil ⇒ b´ = LEMPTY
| _ ⇒ True
end.
Proof.
simpl; intros. rewrite Hcal in Hcal´.
subdestruct; inv Hcal´; trivial.
Qed.
Lemma CalLock_status:
∀ l´ l tq q self_c self_c´ other_c other_c´ b b´ z q0 lq ltq
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q ++ z :: q0, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z)
(Hnin: ¬ In z q)
(Hq: match q with
| nil ⇒ b = LEMPTY
| _ ⇒ True
end)
(HCal: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, z ::lq, ltq)),
b´ = LEMPTY.
Proof.
induction l´; simpl; intros.
- rewrite Hqlock in HCal. inv HCal.
destruct q.
+ elim Hq. trivial.
+ inv H3. elim Hnin. left; trivial.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ z).
{ eapply list_valid_In_append´; eauto. }
subdestruct; inv HCal; try (exploit IHl´; eauto; simpl; trivial; intros; congruence); trivial.
+ specialize (Hin z (TTICKET GET_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
+ specialize (Hin z (TTICKET HOLD_LOCK)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
+ specialize (Hin z (TTICKET GET_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
+ specialize (Hin z (TTICKET HOLD_LOCK)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
Qed.
Lemma Q_CalLock_TSHARED_exists:
∀ l l´ self_c self_c´ other_c b b´ q tq e c h tq0
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hcal´: H_CalLock (TEVENT c (TSHARED e) :: l´) = Some (self_c´, b´, h))
(Hre: HTicketLockOpGenDef.relate_log l = Some (l´, tq0)),
∃ x,
Q_CalLock (TEVENT c (TSHARED e) :: l) = Some x.
Proof.
simpl; intros. rewrite HCal. subst.
subdestruct; inv Hcal´.
exploit Q_CalLock_relate_log; eauto.
intros (Hself & Hb & Hz).
destruct b; inv Hb.
exploit Q_CalLock_q_length_same; eauto.
intros Hlen.
destruct q; inv Hz.
destruct tq; inv Hlen.
rewrite zeq_true. eauto.
Qed.
Lemma decrease_number_lt_Wait:
∀ self_c other_c b tq n
(Hother: (other_c ≤ fairness)%nat)
(Hself: match tq with
| nil ⇒ self_c = O
| a :: _ ⇒ (self_c ≤ a)%nat
end),
(decrease_number self_c other_c b tq <
S (fairness + HTicketLockOpGenDef.CalSumWait (tq ++ n :: nil) × fairness)) %nat.
Proof.
unfold decrease_number; intros.
rewrite CalSumWait_append.
destruct b.
- rewrite <- add_mult_assoc. xomega.
- destruct tq; subst; simpl.
+ xomega.
+ simpl. repeat rewrite <- add_mult_assoc.
eapply le_lt_n_Sm.
rewrite (plus_comm fairness ((fairness + (n0 × fairness + HTicketLockOpGenDef.CalSumWait tq × fairness + S (S (S (S (n + 0)))) × fairness)))%nat).
eapply plus_le_compat; eauto.
eapply le_plus_trans´.
eapply le_plus_trans´.
eapply le_plus_trans.
eapply le_plus_trans´.
eapply plus_le_compat; eauto.
× eapply plus_le_compat_r.
apply mult_le_compat_r. omega.
× simpl. xomega.
- destruct tq; subst; simpl.
+ xomega.
+ simpl. repeat rewrite <- add_mult_assoc.
eapply le_lt_n_Sm.
rewrite (plus_comm fairness ((fairness + (n0 × fairness + HTicketLockOpGenDef.CalSumWait tq × fairness + S (S (S (S (n + 0)))) × fairness)))%nat).
eapply plus_le_compat; eauto.
eapply le_plus_trans´.
eapply le_plus_trans´.
eapply le_plus_trans.
eapply le_plus_trans´.
eapply plus_le_compat; eauto.
× eapply plus_le_compat_r.
apply mult_le_compat_r. omega.
× simpl. xomega.
Qed.
Lemma starvation_freedom:
∀ wait_time l self_c other_c b q tq n c o q´ tq´
(HCal: Q_CalLock l = Some (self_c, other_c, b, q ++ c :: q´, tq ++ n :: tq´))
(Hlen: length q = length tq)
(Hgt: (decrease_number self_c other_c b tq < wait_time)%nat)
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_multi_oracle_queue o)
(Hnin: ¬ In c q)
(Hq: match q with
| nil ⇒ b = LEMPTY
| _ ⇒ True
end)
(Hin´: ∀ i1 e1,
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast: match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hc: 0 ≤ c < TOTAL_CPU),
∃ l´, Q_CalWait wait_time c l o = Some l´.
Proof.
Local Opaque Q_CalLock.
induction wait_time; simpl; intros.
- eapply O_gt_false in Hgt. inv Hgt.
- pose proof Horacle_domain as (Horacle_domain1 & Horacle_domain2).
exploit (Horacle_domain2 c l); eauto.
{
unfold valid_qlock. refine_split´; eauto.
}
intros (self_c´ & other_c´ & b´ & q0 & tq0 & HCal´ & nothead).
exploit (CalLock_progress (o c l)); eauto.
{
intros. eapply Horacle_domain; eauto.
}
intros (q´0 & q´´ & q1 & tq´0 & tq´´ & tq1 & ? &? & ? &? & Hlen1 & Hlt); subst.
assert (HCal_Get:
∃ self_c0 other_c0 b0,
Q_CalLock (TEVENT c (TTICKET GET_NOW) :: o c l ++ l)
= Some (self_c0, other_c0, b0, q´´ ++ c :: q1, tq´´ ++ n :: tq1)).
{
Local Transparent Q_CalLock.
simpl. rewrite HCal´.
destruct (q´´ ++ c :: q1) eqn: Hlq.
{
apply list_not_e_nil in Hlq. inv Hlq.
}
destruct (tq´´ ++ n :: tq1) eqn: Hltq.
{
apply list_not_e_nil in Hltq. inv Hltq.
}
symmetry in Hlq.
eapply list_head_case in Hlq.
destruct Hlq as [(? & ? & ?)| (q2 & ? & ?)]; subst.
{
rewrite zeq_true.
assert (Hb´: b´ = LEMPTY).
{
eapply CalLock_status; eauto.
intros. eapply Horacle_domain1; eauto.
}
subst.
destruct other_c´.
- elim nothead. trivial.
- eauto.
}
{
assert (Hneq: c ≠ z).
{
intro HF; subst. elim Hnin.
eapply in_or_app. right.
simpl. left; trivial.
}
rewrite zeq_false; trivial.
destruct other_c´.
{
elim nothead; trivial.
}
refine_split´; trivial.
}
}
destruct HCal_Get as (self_c0 & other_c0 & b0 & HCal´´).
rewrite HCal´´.
destruct (q´´ ++ c :: q1) eqn: Hlq.
{
apply list_not_e_nil in Hlq. inv Hlq.
}
destruct (zeq z c).
{ eauto. }
rewrite <- Hlq in HCal´´.
exploit (IHwait_time (TEVENT c (TTICKET GET_NOW) :: o c l ++ l)); eauto.
+ rewrite Hlq in HCal´´.
exploit (CalLock_progress_GET_NOW (o c l ++ l)); eauto.
{
destruct tq´´.
- destruct q´´; inv Hlen1. inv Hlq. elim n0; trivial.
- intro HF; inv HF.
}
intros Hlt´.
xomega.
+ intro HF. elim Hnin.
eapply in_or_app. right; trivial.
+ destruct q´´.
× inv Hlq. elim n0; trivial.
× trivial.
+ intros. inv H.
× inv H0. eauto.
× destruct Horacle_domain as (Hd & _).
unfold valid_multi_oracle_domain in ×.
apply in_app_iff in H0. inv H0; eauto.
eapply Horacle_domain1; eauto.
Qed.
End WITH_WAIT.
End WITHMEM.
End Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mqticketlockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Lemma relate_log_shared:
∀ l1 l0 tq
(Hre: HTicketLockOpGenDef.relate_log l1 = Some (l0, tq)),
GetSharedMemEvent l0 = GetSharedMemEvent l1.
Proof.
induction l1; simpl; intros.
- inv Hre. trivial.
- subdestruct; inv Hre; simpl; eauto.
destruct e0; eauto.
Qed.
Lemma relate_ticket_log_pool_gss:
∀ l l´ o o´ p
(Hrelate_log: relate_ticket_log_type l l´)
(Hrelate:relate_ticket_log_pool o o´),
relate_ticket_log_pool (ZMap.set p l o)
(ZMap.set p l´ o´).
Proof.
intros. constructor. intros.
destruct (zeq p z); subst.
- repeat rewrite ZMap.gss. trivial.
- inv Hrelate. repeat rewrite ZMap.gso; eauto.
Qed.
Lemma relate_ticket_log_shared:
∀ curid l l´ tq e
(Hlog: HTicketLockOpGenDef.relate_log l = Some (l´, tq)),
HTicketLockOpGenDef.relate_log (TEVENT curid (TSHARED e) :: l) =
Some (TEVENT curid (TSHARED e) :: l´, tq).
Proof.
intros. simpl. rewrite Hlog. trivial.
Qed.
Lemma relate_ticket_log_pool_shared:
∀ curid p l l´ t t´ tq e
(Hlog: HTicketLockOpGenDef.relate_log l´ = Some (l,tq))
(Hlog_pool: relate_ticket_log_pool t t´),
relate_ticket_log_pool
(ZMap.set p (MultiDef (TEVENT curid (TSHARED e) :: l)) t)
(ZMap.set p (MultiDef (TEVENT curid (TSHARED e) :: l´)) t´).
Proof.
intros. eapply relate_ticket_log_pool_gss; eauto.
econstructor. eapply relate_ticket_log_shared; eauto.
Qed.
Lemma real_ticket_relate_pb:
∀ n l l´ z
(Hrelate_ticket_log_type : relate_ticket_log_type
(ZMap.get z l) (ZMap.get z l´)),
relate_ticket_log_type
(ZMap.get z (real_multi_log_pb n l))
(ZMap.get z (real_multi_log_pb n l´)).
Proof.
induction n; intros; simpl; trivial.
destruct (zeq z (Z.of_nat n)); subst.
- repeat rewrite ZMap.gss. econstructor. simpl. trivial.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_ticket_relate:
∀ l l´
(Hrelate: relate_ticket_log_pool l l´),
relate_ticket_log_pool (real_multi_log l)
(real_multi_log l´).
Proof.
intros. constructor. intros. inv Hrelate.
specialize (Hrelate_ticket_log_type _ _ _ Hrange).
unfold real_multi_log.
eapply real_ticket_relate_pb; eauto.
Qed.
Section WITH_WAIT.
Local Transparent Q_CalLock Q_CalWait.
Lemma Q_CalLock_q_length_same:
∀ l self_c other_c b q tq
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
length tq = length q.
Proof.
induction l; simpl; intros.
- inv HCal. trivial.
- subdestruct; inv HCal;
exploit IHl; eauto.
+ intros.
repeat rewrite app_comm_cons.
repeat rewrite app_length.
rewrite H. simpl; trivial.
Qed.
Lemma list_head_case:
∀ {A: Type} q´ q q0 (z z0: A)
(Heq: z :: q = q´ ++ z0 :: q0),
(z = z0 ∧ q´ = nil ∧ q0 = q)
∨ (∃ q1, q´ = z :: q1 ∧ q = q1 ++ z0 :: q0).
Proof.
induction q´; simpl; intros.
- inv Heq. left. eauto.
- destruct q.
+ inv Heq.
symmetry in H1. apply list_not_e_nil in H1. inv H1.
+ inv Heq. exploit IHq´; eauto.
Qed.
Lemma CalLock_length:
∀ l´ l tq q self_c self_c´ other_c other_c´ b b´ z bound q0 q1 q´ tq0 tq´´
(Hlen: length tq = length q)
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q ++ z :: q0, tq ++ bound :: tq0))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z ∨ (∀ n, e ≠ TTICKET (INC_TICKET n)))
(Hqlock0: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, q´ ++ z :: q1, tq´´))
(Hnin: ¬ In z q)
(Hnin0: ¬ In z q0),
∃ tq´ tq1, tq´´ = tq´ ++ bound :: tq1 ∧ length tq´ = length q´.
Proof.
induction l´; simpl; intros.
- rewrite Hqlock in Hqlock0. inv Hqlock0.
refine_split´; trivial.
eapply list_unique_element in H3; eauto.
destruct H3 as (? & ?); subst. trivial.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ z ∨ (∀ n, e ≠ TTICKET (INC_TICKET n))).
{ eapply list_valid_In_append´; eauto. }
subdestruct; inv Hqlock0; try (rewrite H3 in Hdestruct0; exploit IHl´; eauto).
+ destruct q´; inv H3.
× specialize (Hin z (TTICKET (INC_TICKET n1))).
elim Hin.
{ intros HF; elim HF; trivial. }
{ intros HF. specialize (HF n1). elim HF. trivial. }
left; trivial.
× symmetry in H1.
eapply list_not_e_nil in H1.
inv H1.
+ rewrite app_comm_cons in Hdestruct0.
exploit IHl´; try eassumption.
intros (tq´ & tq1 & Heq1 & Hlen1).
destruct tq´.
× inv Hlen1.
× rewrite <- app_comm_cons in Heq1.
inv Heq1. inv Hlen1.
refine_split´; trivial.
+ rewrite app_comm_cons in H3.
eapply list_tail_one_element in H3.
destruct H3 as [(? & ?) | HF]; subst.
{
specialize (Hin z (TTICKET (INC_TICKET n5))).
elim Hin.
{ intros HF; elim HF; trivial. }
{ intros HF. specialize (HF n5). elim HF. trivial. }
left; trivial.
}
{
destruct HF as (l2´ & Heq).
rewrite Heq in Hdestruct0.
rewrite app_comm_cons.
exploit IHl´; eauto.
intros (tq´ & tq1 & → & Hlen1).
rewrite <- app_assoc.
rewrite <- app_comm_cons.
refine_split´; trivial.
}
Qed.
Lemma Q_CalLock_relate_log_exists:
∀ l self_c other_c b q tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
∃ l´, HTicketLockOpGenDef.relate_log l = Some (l´, tq).
Proof.
induction l; simpl; intros.
- inv Hcal. refine_split´; trivial.
- subdestruct; inv Hcal;
(exploit IHl; eauto; intros (l´ & ->);
refine_split´; trivial).
Qed.
Lemma Q_CalLock_relate_log_eq:
∀ l l´ self_c other_c b q tq tq´
(Hre: HTicketLockOpGenDef.relate_log l = Some (l´, tq))
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq´)),
tq = tq´.
Proof.
intros.
eapply Q_CalLock_relate_log_exists in Hcal.
destruct Hcal as (l0 & Heq).
rewrite Hre in Heq. inv Heq.
trivial.
Qed.
Lemma Q_CalLock_GET_NOW_imply:
∀ curid l self_c other_c b q tq,
Q_CalLock (TEVENT curid (TTICKET GET_NOW) :: l) = Some (self_c, other_c, b, curid :: q, tq) →
b = LGET.
Proof.
simpl; intros.
subdestruct; inversion H; try subst; eauto; try congruence.
Qed.
Lemma CalWait_exists:
∀ wait_time curid l o l0
(Hwait: Q_CalWait wait_time curid l o = Some l0),
∃ self_c other_c q tq, Q_CalLock l0 = Some (self_c, other_c, LGET, curid :: q, tq)
.
Proof.
Local Opaque Q_CalLock.
induction wait_time; simpl; intros; try (inv Hwait; fail).
subdestruct; try inv Hwait; eauto.
exploit Q_CalLock_GET_NOW_imply; eauto.
intros; subst.
refine_split´; eauto.
Qed.
Lemma CalWait_exists_log:
∀ wait_time curid l o l0
(Hwait: Q_CalWait wait_time curid l o = Some l0)
(Horacle_domain : valid_multi_oracle_domain o),
∃ l´, l0 = l´ ++ l
∧ (∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ curid ∨ (∀ n, e ≠ TTICKET (INC_TICKET n))).
Proof.
Local Opaque Q_CalLock.
induction wait_time; simpl; intros; try (inv Hwait; fail).
subdestruct; try inv Hwait; eauto.
- rewrite app_comm_cons.
refine_split´; eauto. intros.
inv H.
+ right. inv H0. intros. intro HF; inv HF.
+ left. eapply Horacle_domain in H0; eauto. eapply H0.
- exploit IHwait_time; eauto.
intros (l´ & ? & Hp); subst.
rewrite app_comm_cons.
rewrite app_assoc.
refine_split´; eauto.
intros.
eapply in_app_or in H.
destruct H as [Hin | Hin]; auto.
inv Hin.
+ right. inv H. intros. intro HF; inv HF.
+ eapply Horacle_domain in H; eauto.
left. eapply H.
Qed.
Lemma relate_ticket_log_pool_REL:
∀ curid p l l0 l´ t t´ tq tq0
(Hlog: HTicketLockOpGenDef.relate_log l´ = Some (l, tq))
(Hlog´: HTicketLockOpGenDef.relate_log (TEVENT curid (TTICKET INC_NOW) :: l´) = Some (l0, tq0))
(Hlog_pool: relate_ticket_log_pool t t´),
relate_ticket_log_pool
(ZMap.set p (MultiDef (TEVENT curid (TTICKET REL_LOCK) :: l)) t)
(ZMap.set p (MultiDef (TEVENT curid (TTICKET INC_NOW) :: l´)) t´).
Proof.
intros. eapply relate_ticket_log_pool_gss; eauto.
econstructor. simpl in ×. rewrite Hlog in ×.
destruct tq; contra_inv. inv Hlog´. trivial.
Qed.
Local Transparent Q_CalLock.
Lemma Q_CalLock_HOLD_LOCK_exists:
∀ wait_time c l o l0
(Hwait: Q_CalWait wait_time c l o = Some l0),
∃ x,
Q_CalLock (TEVENT c (TTICKET HOLD_LOCK) :: l0) = Some x.
Proof.
simpl; intros.
eapply CalWait_exists in Hwait.
destruct Hwait as (self_c & other_c & q & tq & Hcal).
rewrite Hcal.
exploit Q_CalLock_q_length_same; eauto. intros.
destruct tq; inv H.
rewrite zeq_true. eauto.
Qed.
Lemma Q_CalLock_INC_TICKET_exists:
∀ l self_c other_c b q tq n c
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hnin: ¬ In c q)
(Hpos: other_c ≠ O),
∃ x,
Q_CalLock (TEVENT c (TTICKET (INC_TICKET n)) :: l) = Some x.
Proof.
simpl; intros. rewrite HCal.
exploit Q_CalLock_q_length_same; eauto. intros.
destruct q.
- destruct tq; inv H. eauto.
- destruct tq; inv H.
destruct (zeq c z); subst.
+ elim Hnin. left; trivial.
+ destruct other_c.
× elim Hpos. trivial.
× destruct (in_dec zeq c q); eauto.
elim Hnin. right; trivial.
Qed.
Lemma Q_CalLock_oracle_not_In:
∀ l´ l self_c other_c b q tq self_c´ other_c´ b´ q´ tq´ c
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ c)
(Hnin: ¬ In c q)
(HCal´: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, q´, tq´)),
¬ In c q´.
Proof.
induction l´; simpl; intros.
- rewrite HCal in HCal´. inv HCal´. trivial.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ c).
{ eapply list_valid_In_append; eauto. }
subdestruct; inv HCal´; try (eapply (IHl´ l); eauto; fail).
+ specialize (Hin i (TTICKET (INC_TICKET n1))).
red; intros. simpl in H. destruct H as [HF|HF]; inv HF.
elim Hin. left; trivial. trivial.
+ red; intro. exploit (IHl´ l); eauto.
right. trivial.
+ red; intro HF. exploit (IHl´ l); eauto.
rewrite app_comm_cons in HF.
eapply in_app_or in HF.
destruct HF as [HF´ | HF´]; trivial.
destruct HF´ as [HF|HF]; inv HF.
specialize (Hin c (TTICKET (INC_TICKET n5))).
elim Hin; trivial. left; trivial.
Qed.
Lemma Q_CalLock_oracle:
∀ l self_c other_c b q tq c o
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_multi_oracle_queue o)
(Hin´: ∀ i1 e1,
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast: match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hnin: ¬ In c q),
∃ self_c´ other_c´ b´ q´ tq´,
Q_CalLock (o c l ++ l) = Some (self_c´, other_c´, b´, q´, tq´)
∧ ¬ In c q´
∧ other_c´ ≠ O.
Proof.
intros.
destruct Horacle_domain as (Horacle_domain0 & Horacle_domain1).
unfold valid_multi_oracle_queue in ×.
specialize (Horacle_domain1 c l).
exploit Horacle_domain1; eauto.
{
unfold valid_qlock.
rewrite HCal. refine_split´; trivial.
}
intros (self_c´ & other_c´ & b´ & q´ & tq´ & HCal´ & Hnhead).
assert (HnotIn: ¬ In c q´).
{
eapply (Q_CalLock_oracle_not_In (o c l) l); eauto.
intros. eapply Horacle_domain0; eauto.
}
refine_split´; eauto.
Qed.
Lemma Q_CalLock_INC_TICKET_exists´:
∀ l self_c other_c b q tq n c o
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_multi_oracle_queue o)
(Hin´: ∀ i1 e1,
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast: match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hnin: ¬ In c q),
∃ x,
Q_CalLock (TEVENT c (TTICKET (INC_TICKET n)) :: (o c l ++ l)) = Some x.
Proof.
intros.
exploit Q_CalLock_oracle; eauto.
intros (self_c´ & other_c´ & b´ & q´ & tq´ & HCal´ & HnotIn & Hother).
eapply Q_CalLock_INC_TICKET_exists; eauto.
Qed.
Lemma Q_CalLock_INC_NOW_exists:
∀ l self_c other_c q tq c q´
(HCal: Q_CalLock l = Some (self_c, other_c, LHOLD, q, tq))
(HinQ: q = c :: q´)
,
∃ x,
Q_CalLock (TEVENT c (TTICKET (INC_NOW)) :: l) = Some x.
Proof.
simpl; intros. rewrite HCal. subst.
exploit Q_CalLock_q_length_same; eauto. intros.
destruct tq; inv H.
rewrite zeq_true. eauto.
Qed.
Lemma O_gt_false:
∀ n (Hgt: (O > n)%nat),
False.
Proof.
intros. destruct n; omega.
Qed.
Lemma add_mult_assoc:
∀ (a b c: nat),
(a × c + b × c = (a + b) × c)%nat.
Proof.
induction a.
- simpl. trivial.
- simpl. intros. rewrite <- (IHa b c).
xomega.
Qed.
Lemma lt_plus_trans´ n m p : (n < m → n < p + m)%nat.
Proof.
erewrite (plus_comm p).
eapply lt_plus_trans.
Qed.
Lemma le_plus_trans´ n m p : (n ≤ m → n ≤ p + m)%nat.
Proof.
erewrite (plus_comm p).
eapply le_plus_trans.
Qed.
Lemma lt_less_plus n m p : (n < m → p + n < p + m)%nat.
Proof.
omega.
Qed.
Lemma lt_plus_r n m : 0 < n → m < n + m.
Proof.
omega.
Qed.
Lemma CalLock_progress:
∀ l´ l tq q self_c self_c´ other_c other_c´ b b´ z bound q0 tq0 lq ltq
(Hlen: length tq = length q)
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q ++ z :: q0, tq ++ bound :: tq0))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z )
(Hnin: ¬ In z q)
(HCal: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, lq, ltq)),
∃ q´ q´´ q1 tq´ tq´´ tq1,
lq = q´´ ++ z :: q1
∧ ltq = tq´´++ bound :: tq1
∧ q = q´ ++ q´´
∧ tq = tq´ ++ tq´´
∧ length tq´´ = length q´´
∧ (decrease_number self_c´ other_c´ b´ tq´´ ≤
decrease_number self_c other_c b tq)%nat.
Proof.
induction l´; simpl; intros.
- ∃ nil, q, q0, nil, tq, tq0.
rewrite Hqlock in HCal. inv HCal. refine_split´; eauto.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ z ∨ e = TTICKET GET_NOW).
{ eapply list_valid_In_append´; eauto. }
destruct a.
subdestruct; inv HCal; try (exploit IHl´; eauto);
intros (q´ & q´´ & q1 & tq´ & tq´´ & tq1 & Hlq & Hltq & Hq & htq & Hlen´ & Hdec); subst.
+ symmetry in Hlq.
apply list_not_e_nil in Hlq. inv Hlq.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
simpl.
eapply list_head_case in Hlq.
destruct Hlq as [(? & ? & ?)| (q2 & ? & ?)]; subst.
{
specialize (Hin z (TTICKET GET_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
}
eapply list_head_case in Hltq.
destruct Hltq as [(? & ? & ?)| (tq2 & ? & ?)]; subst.
{ inv Hlen´. }
simpl. apply le_plus_trans´.
repeat rewrite mult_plus_distr_r. omega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
simpl.
repeat rewrite mult_plus_distr_r. omega.
+ eapply list_head_case in Hlq.
destruct Hlq as [(? & ? & ?)| (q2 & ? & ?)]; subst.
{
specialize (Hin z (TTICKET INC_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
}
eapply list_head_case in Hltq.
destruct Hltq as [(? & ? & ?)| (tq2 & ? & ?)]; subst.
{ inv Hlen´. }
∃ (q´ ++ z0 :: nil), q2, q1, (tq´ ++ n :: nil), tq2, tq1.
refine_split´; eauto.
× rewrite <- app_assoc.
rewrite <- app_comm_cons. simpl. trivial.
× rewrite <- app_assoc.
rewrite <- app_comm_cons. simpl. trivial.
× etransitivity; try eapply Hdec.
simpl.
etransitivity.
instantiate (1:=((n0 + HTicketLockOpGenDef.CalSumWait tq2 + 1) × fairness)%nat).
etransitivity.
instantiate (1:=((HTicketLockOpGenDef.CalSumWait tq2 + 1) × fairness)%nat).
repeat rewrite mult_plus_distr_r. omega.
repeat rewrite <- add_mult_assoc.
rewrite plus_assoc_reverse. xomega. xomega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
simpl. omega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
unfold decrease_number.
destruct b´; omega.
+ subst.
∃ q´, q´´, (q1 ++ i::nil), tq´, tq´´, (tq1 ++ n5 :: nil).
refine_split´; eauto.
× repeat rewrite app_comm_cons.
rewrite Hlq.
rewrite <- app_assoc. trivial.
× repeat rewrite app_comm_cons.
rewrite Hltq.
rewrite <- app_assoc. trivial.
× etransitivity; try eapply Hdec.
destruct b´; simpl; omega.
+ refine_split´; eauto.
etransitivity; try eapply Hdec.
unfold decrease_number.
destruct b´; omega.
Qed.
Lemma CalLock_progress_GET_NOW:
∀ l tq q self_c self_c´ other_c other_c´ b b´ c n tq´
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q, tq++n::tq´))
(HCal: Q_CalLock (TEVENT c (TTICKET GET_NOW):: l) =
Some (self_c´, other_c´, b´, q, tq++n::tq´))
(Hneq: tq ≠ nil),
(decrease_number self_c´ other_c´ b´ tq <
decrease_number self_c other_c b tq)%nat.
Proof.
simpl; intros. rewrite Hqlock in HCal.
subdestruct; inv HCal; simpl.
- symmetry in Hdestruct.
eapply list_head_case in Hdestruct.
destruct Hdestruct as [(? & ? & ?)| (tq2 & ? & ?)]; subst.
{ elim Hneq. trivial. }
simpl.
apply lt_plus_trans´.
pose positive_fairness.
repeat rewrite mult_plus_distr_r. omega.
- destruct b´; simpl; omega.
Qed.
Local Transparent H_CalLock.
Lemma Q_CalLock_nil:
∀ l self_c other_c b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, nil, tq)),
b = LEMPTY.
Proof.
induction l; simpl; intros.
- inv Hcal. trivial.
- subdestruct; inv Hcal; trivial.
Qed.
Lemma Q_CalLock_get:
∀ l self_c other_c q b head tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, head :: tq)),
match b with
| LGET ⇒ head = self_c
| _ ⇒ True
end.
Proof.
induction l; simpl; intros.
- inv Hcal.
- subdestruct; inv Hcal; trivial.
+ destruct b; trivial.
exploit IHl; eauto.
+ destruct b; trivial.
exploit IHl; eauto.
+ destruct b; trivial.
exploit IHl; eauto.
Qed.
Definition get_head_lock (l: list Z) (b: head_status):=
match b with
| LHOLD ⇒
match l with
| nil ⇒ None
| a :: _ ⇒ Some a
end
| _ ⇒ None
end.
Lemma Q_CalLock_relate_log:
∀ l l´ self_c self_c´ other_c b b´ q tq tq0 h
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hcal´: H_CalLock l´ = Some (self_c´, b´, h))
(Hre: HTicketLockOpGenDef.relate_log l = Some (l´, tq0)),
match b with
| LGET ⇒ True
| _ ⇒ self_c´ = self_c
end
∧ match b with
| LHOLD ⇒ b´ = LHOLD
| _ ⇒ b´ = LEMPTY
end
∧ h = get_head_lock q b.
Proof.
induction l; simpl; intros.
- inv Hcal. inv Hre. inv Hcal´. simpl; eauto.
- destruct a. destruct (HTicketLockOpGenDef.relate_log l) eqn: Hre´; contra_inv.
destruct (Q_CalLock l) eqn: Hcal0´; contra_inv.
destruct p. destruct p0. repeat destruct p.
exploit Q_CalLock_relate_log_exists; eauto.
rewrite Hre´. intros (l´0 & Heq). inv Heq.
destruct l2; contra_inv.
+ destruct l1; contra_inv.
destruct e; contra_inv.
destruct e; contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto.
eapply Q_CalLock_nil in Hcal0´. subst. trivial.
+ destruct l1; contra_inv.
destruct (zeq i z); contra_inv.
× destruct h0; contra_inv.
{
destruct e; contra_inv.
destruct e; contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto. simpl.
intros (? & ? & ?).
refine_split´; eauto.
}
{
destruct e; contra_inv.
destruct e; contra_inv.
inv Hcal. inv Hre.
simpl in Hcal´.
destruct (H_CalLock l´0) eqn: Hcal0; contra_inv.
repeat destruct p.
destruct h0; contra_inv.
- destruct o; contra_inv.
inv Hcal´.
eapply Q_CalLock_get in Hcal0´.
inv Hcal0´. eauto.
- destruct o; contra_inv.
destruct (zeq z z0); contra_inv.
}
{
destruct e; contra_inv.
- destruct e; contra_inv.
inv Hcal. inv Hre.
simpl in Hcal´.
destruct (H_CalLock l´0) eqn: Hcal0; contra_inv.
repeat destruct p.
destruct h0; contra_inv.
+ destruct o; contra_inv.
+ destruct o; contra_inv.
destruct (zeq z z0); contra_inv.
inv Hcal´. eauto.
- destruct n; contra_inv. inv Hcal. inv Hre.
simpl in Hcal´.
destruct (H_CalLock l´0) eqn: Hcal0; contra_inv.
repeat destruct p.
destruct h0; contra_inv.
+ destruct o; contra_inv.
+ destruct o; contra_inv.
destruct (zeq z z0); contra_inv.
destruct n; contra_inv. inv Hcal´.
exploit IHl; eauto.
simpl. intros (? & _).
refine_split´; eauto.
}
× destruct n0; contra_inv.
destruct e; contra_inv.
destruct e; contra_inv.
{
destruct (in_dec zeq i l2); contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto.
}
{
inv Hre. inv Hcal.
exploit IHl; eauto.
}
Qed.
Lemma CalSumWait_append:
∀ l l´,
HTicketLockOpGenDef.CalSumWait (l ++ l´)
= (HTicketLockOpGenDef.CalSumWait (l) + HTicketLockOpGenDef.CalSumWait (l´)) % nat.
Proof.
induction l; simpl; intros; trivial.
rewrite IHl. omega.
Qed.
Lemma Q_CalLock_other_c:
∀ l self_c other_c q b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
(other_c ≤ fairness)%nat.
Proof.
induction l; simpl; intros.
- inv Hcal. trivial.
- subdestruct; inv Hcal; trivial; exploit IHl; eauto; intros; try omega.
Qed.
Lemma Q_CalLock_self_c:
∀ l self_c other_c q b tq
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
match tq with
| nil ⇒ self_c = O
| a :: _ ⇒ (self_c ≤ a)%nat
end.
Proof.
induction l; simpl; intros.
- inv Hcal. trivial.
- subdestruct; inv Hcal; trivial; exploit IHl; eauto; intros Hs.
+ simpl in Hs. subst. omega.
+ destruct tq; omega.
+ simpl in Hs. omega.
Qed.
Lemma Q_CalLock_INC_TICKET_status:
∀ l self_c other_c q b tq self_c´ other_c´ q´ b´ tq´ c n
(Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hcal´: Q_CalLock (TEVENT c (TTICKET (INC_TICKET n)) :: l) = Some (self_c´, other_c´, b´, q´, tq´)),
match q with
| nil ⇒ b´ = LEMPTY
| _ ⇒ True
end.
Proof.
simpl; intros. rewrite Hcal in Hcal´.
subdestruct; inv Hcal´; trivial.
Qed.
Lemma CalLock_status:
∀ l´ l tq q self_c self_c´ other_c other_c´ b b´ z q0 lq ltq
(Hqlock: Q_CalLock l = Some (self_c, other_c, b, q ++ z :: q0, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z)
(Hnin: ¬ In z q)
(Hq: match q with
| nil ⇒ b = LEMPTY
| _ ⇒ True
end)
(HCal: Q_CalLock (l´ ++ l) = Some (self_c´, other_c´, b´, z ::lq, ltq)),
b´ = LEMPTY.
Proof.
induction l´; simpl; intros.
- rewrite Hqlock in HCal. inv HCal.
destruct q.
+ elim Hq. trivial.
+ inv H3. elim Hnin. left; trivial.
- assert (Hin_append:
∀ i0 e,
In (TEVENT i0 e) l´ → i0 ≠ z).
{ eapply list_valid_In_append´; eauto. }
subdestruct; inv HCal; try (exploit IHl´; eauto; simpl; trivial; intros; congruence); trivial.
+ specialize (Hin z (TTICKET GET_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
+ specialize (Hin z (TTICKET HOLD_LOCK)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
+ specialize (Hin z (TTICKET GET_NOW)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
+ specialize (Hin z (TTICKET HOLD_LOCK)).
elim Hin; try (intros HF; congruence); trivial.
left; trivial.
Qed.
Lemma Q_CalLock_TSHARED_exists:
∀ l l´ self_c self_c´ other_c b b´ q tq e c h tq0
(HCal: Q_CalLock l = Some (self_c, other_c, b, q, tq))
(Hcal´: H_CalLock (TEVENT c (TSHARED e) :: l´) = Some (self_c´, b´, h))
(Hre: HTicketLockOpGenDef.relate_log l = Some (l´, tq0)),
∃ x,
Q_CalLock (TEVENT c (TSHARED e) :: l) = Some x.
Proof.
simpl; intros. rewrite HCal. subst.
subdestruct; inv Hcal´.
exploit Q_CalLock_relate_log; eauto.
intros (Hself & Hb & Hz).
destruct b; inv Hb.
exploit Q_CalLock_q_length_same; eauto.
intros Hlen.
destruct q; inv Hz.
destruct tq; inv Hlen.
rewrite zeq_true. eauto.
Qed.
Lemma decrease_number_lt_Wait:
∀ self_c other_c b tq n
(Hother: (other_c ≤ fairness)%nat)
(Hself: match tq with
| nil ⇒ self_c = O
| a :: _ ⇒ (self_c ≤ a)%nat
end),
(decrease_number self_c other_c b tq <
S (fairness + HTicketLockOpGenDef.CalSumWait (tq ++ n :: nil) × fairness)) %nat.
Proof.
unfold decrease_number; intros.
rewrite CalSumWait_append.
destruct b.
- rewrite <- add_mult_assoc. xomega.
- destruct tq; subst; simpl.
+ xomega.
+ simpl. repeat rewrite <- add_mult_assoc.
eapply le_lt_n_Sm.
rewrite (plus_comm fairness ((fairness + (n0 × fairness + HTicketLockOpGenDef.CalSumWait tq × fairness + S (S (S (S (n + 0)))) × fairness)))%nat).
eapply plus_le_compat; eauto.
eapply le_plus_trans´.
eapply le_plus_trans´.
eapply le_plus_trans.
eapply le_plus_trans´.
eapply plus_le_compat; eauto.
× eapply plus_le_compat_r.
apply mult_le_compat_r. omega.
× simpl. xomega.
- destruct tq; subst; simpl.
+ xomega.
+ simpl. repeat rewrite <- add_mult_assoc.
eapply le_lt_n_Sm.
rewrite (plus_comm fairness ((fairness + (n0 × fairness + HTicketLockOpGenDef.CalSumWait tq × fairness + S (S (S (S (n + 0)))) × fairness)))%nat).
eapply plus_le_compat; eauto.
eapply le_plus_trans´.
eapply le_plus_trans´.
eapply le_plus_trans.
eapply le_plus_trans´.
eapply plus_le_compat; eauto.
× eapply plus_le_compat_r.
apply mult_le_compat_r. omega.
× simpl. xomega.
Qed.
Lemma starvation_freedom:
∀ wait_time l self_c other_c b q tq n c o q´ tq´
(HCal: Q_CalLock l = Some (self_c, other_c, b, q ++ c :: q´, tq ++ n :: tq´))
(Hlen: length q = length tq)
(Hgt: (decrease_number self_c other_c b tq < wait_time)%nat)
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_multi_oracle_queue o)
(Hnin: ¬ In c q)
(Hq: match q with
| nil ⇒ b = LEMPTY
| _ ⇒ True
end)
(Hin´: ∀ i1 e1,
In (TEVENT i1 e1) l → 0 ≤ i1 < 8)
(Hlast: match l with
| nil ⇒ True
| TEVENT c0 _ :: _ ⇒ c0 = c
end)
(Hc: 0 ≤ c < TOTAL_CPU),
∃ l´, Q_CalWait wait_time c l o = Some l´.
Proof.
Local Opaque Q_CalLock.
induction wait_time; simpl; intros.
- eapply O_gt_false in Hgt. inv Hgt.
- pose proof Horacle_domain as (Horacle_domain1 & Horacle_domain2).
exploit (Horacle_domain2 c l); eauto.
{
unfold valid_qlock. refine_split´; eauto.
}
intros (self_c´ & other_c´ & b´ & q0 & tq0 & HCal´ & nothead).
exploit (CalLock_progress (o c l)); eauto.
{
intros. eapply Horacle_domain; eauto.
}
intros (q´0 & q´´ & q1 & tq´0 & tq´´ & tq1 & ? &? & ? &? & Hlen1 & Hlt); subst.
assert (HCal_Get:
∃ self_c0 other_c0 b0,
Q_CalLock (TEVENT c (TTICKET GET_NOW) :: o c l ++ l)
= Some (self_c0, other_c0, b0, q´´ ++ c :: q1, tq´´ ++ n :: tq1)).
{
Local Transparent Q_CalLock.
simpl. rewrite HCal´.
destruct (q´´ ++ c :: q1) eqn: Hlq.
{
apply list_not_e_nil in Hlq. inv Hlq.
}
destruct (tq´´ ++ n :: tq1) eqn: Hltq.
{
apply list_not_e_nil in Hltq. inv Hltq.
}
symmetry in Hlq.
eapply list_head_case in Hlq.
destruct Hlq as [(? & ? & ?)| (q2 & ? & ?)]; subst.
{
rewrite zeq_true.
assert (Hb´: b´ = LEMPTY).
{
eapply CalLock_status; eauto.
intros. eapply Horacle_domain1; eauto.
}
subst.
destruct other_c´.
- elim nothead. trivial.
- eauto.
}
{
assert (Hneq: c ≠ z).
{
intro HF; subst. elim Hnin.
eapply in_or_app. right.
simpl. left; trivial.
}
rewrite zeq_false; trivial.
destruct other_c´.
{
elim nothead; trivial.
}
refine_split´; trivial.
}
}
destruct HCal_Get as (self_c0 & other_c0 & b0 & HCal´´).
rewrite HCal´´.
destruct (q´´ ++ c :: q1) eqn: Hlq.
{
apply list_not_e_nil in Hlq. inv Hlq.
}
destruct (zeq z c).
{ eauto. }
rewrite <- Hlq in HCal´´.
exploit (IHwait_time (TEVENT c (TTICKET GET_NOW) :: o c l ++ l)); eauto.
+ rewrite Hlq in HCal´´.
exploit (CalLock_progress_GET_NOW (o c l ++ l)); eauto.
{
destruct tq´´.
- destruct q´´; inv Hlen1. inv Hlq. elim n0; trivial.
- intro HF; inv HF.
}
intros Hlt´.
xomega.
+ intro HF. elim Hnin.
eapply in_or_app. right; trivial.
+ destruct q´´.
× inv Hlq. elim n0; trivial.
× trivial.
+ intros. inv H.
× inv H0. eauto.
× destruct Horacle_domain as (Hd & _).
unfold valid_multi_oracle_domain in ×.
apply in_app_iff in H0. inv H0; eauto.
eapply Horacle_domain1; eauto.
Qed.
End WITH_WAIT.
End WITHMEM.
End Refinement.