Library mcertikos.mcslock.StarvationFreedomMCSLockWaitLock
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 LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import ListLemma2.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import HMCSLockOpGenDef.
Require Import CalMCSLock.
Require Import CalMCSLockLemmas.
Require Export MQMCSLockOp.
Require Export MHMCSLockOp.
Require Import ObjMCSLock.
Require Import CalTicketLock.
Require Import INVLemmaQSLock.
Require Import INVLemmaQLock.
Require Import ObjQLock.
Require Import ZSet.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mqmcslockop_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section Auxiliary.
Lemma relate_mcs_log_pool_gss:
∀ l l´ o o´ p
(Hrelate_log: relate_mcs_log_type l l´)
(Hrelate:relate_mcs_log_pool o o´),
relate_mcs_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_mcs_log_shared:
∀ curid l l´ tq e
(Hlog: relate_mcs_log l = Some (l´, tq)),
relate_mcs_log (TEVENT curid (TSHARED e) :: l) =
Some (TEVENT curid (TSHARED e) :: l´, tq).
Proof.
intros. simpl. rewrite Hlog. trivial.
Qed.
Lemma relate_mcs_log_pool_shared:
∀ curid p l l´ t t´ tq e
(Hlog: relate_mcs_log l´ = Some (l,tq))
(Hlog_pool: relate_mcs_log_pool t t´),
relate_mcs_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_mcs_log_pool_gss; eauto.
econstructor. eapply relate_mcs_log_shared; eauto.
Qed.
Lemma real_mcs_relate_pb:
∀ n l l´ z
(Hrelate_mcs_log_type : relate_mcs_log_type
(ZMap.get z l) (ZMap.get z l´)),
relate_mcs_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_mcs_relate:
∀ l l´
(Hrelate: relate_mcs_log_pool l l´),
relate_mcs_log_pool (real_multi_log l)
(real_multi_log l´).
Proof.
intros. constructor. intros. inv Hrelate.
specialize (Hrelate_mcs_log_type _ _ _ Hrange).
unfold real_multi_log.
eapply real_mcs_relate_pb; eauto.
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 CalSumWait_append:
∀ l l´,
CalMCSLock.CalSumWait (l ++ l´) = (CalMCSLock.CalSumWait (l) + CalMCSLock.CalSumWait (l´)) % nat.
Proof.
induction l; simpl; intros; trivial.
rewrite IHl.
omega.
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.
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.
End Auxiliary.
Section WITHCALLOCK.
Local Transparent QS_CalLock QS_CalWaitGet.
Lemma QS_CalLock_q_tq_length_same:
∀ l self_c rel_c b q slow tq
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, 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 QS_CalLock_q_tq_length_same_not_nil:
∀ l self_c rel_c b q slow tq
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
tq ≠ nil ↔ q ≠ nil.
Proof.
intros.
exploit QS_CalLock_q_tq_length_same; eauto.
intros.
split; intros.
- destruct tq.
+ elim H0; reflexivity.
+ destruct q; simpl; try (inversion H; fail).
intro contra; inv contra.
- destruct q.
+ elim H0; reflexivity.
+ destruct tq; simpl; try (inversion H; fail).
intro contra; inv contra.
Qed.
Lemma QS_CalLock_q_tq_length_same_nil:
∀ l self_c rel_c b q slow tq
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
tq = nil ↔ q = nil.
Proof.
intros.
exploit QS_CalLock_q_tq_length_same; eauto.
intros.
split; intros.
- destruct tq; try inversion H0.
destruct q; inversion H; reflexivity.
- destruct q; try inversion H0.
destruct tq; inversion H; reflexivity.
Qed.
Lemma QS_CalLock_relate_mcs_log_exists:
∀ l self_c rel_c b q slow tq
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
∃ l´, relate_mcs_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 QS_CalLock_relate_mcs_log_eq:
∀ l l´ self_c rel_c b q slow tq tq´
(Hre: relate_mcs_log l = Some (l´, tq))
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq´)),
tq = tq´.
Proof.
intros.
eapply QS_CalLock_relate_mcs_log_exists in Hcal.
destruct Hcal as (l0 & Heq).
rewrite Hre in Heq.
inv Heq.
trivial.
Qed.
Lemma QS_CalLock_nil:
∀ l self_c rel_c b q slow tq
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Qval: q = nil),
b = LEMPTY.
Proof.
induction l; intros.
- subst.
simpl in Hcal; inv Hcal; auto.
- subst.
simpl in Hcal.
subdestruct; subst; try (inv Hcal; trivial; fail);
try (eapply IHl; eauto).
Qed.
Lemma QS_CalLock_SWAP_TAIL_false_imply:
∀ curid l self_c rel_c b q slow tq bound,
QS_CalLock (TEVENT curid (TTICKET (SWAP_TAIL bound false)) :: l)
= Some (self_c, rel_c, b, q, slow, tq) →
(∃ q´, q = q´ ++ (curid::nil) ∧ q´ ≠ nil) ∧
(∃ tq´, tq = tq´ ++ (bound::nil) ∧ tq´ ≠ nil).
Proof.
simpl; intros.
subdestruct; inversion H; try subst; eauto; try congruence.
split; [ ∃ (z::l3); split; try auto; intro contras; inversion contras |
∃ (n::l1); split; try auto; intro contras; inversion contras].
Qed.
Lemma QS_CalLock_SWAP_TAIL_false_exists:
∀ l self_c rel_c b q slow tq c bound
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow , tq))
(Hqnnil: q ≠ nil)
(Hnin: ¬ In c q),
∃ x,
QS_CalLock (TEVENT c (TTICKET (SWAP_TAIL bound false)) :: l) = Some x.
Proof.
simpl; intros.
rewrite HCal.
exploit QS_CalLock_q_tq_length_same; eauto.
intros.
destruct q.
- elim Hqnnil; auto.
- destruct tq; inv H.
destruct (zeq c z); subst.
+ elim Hnin.
left; auto.
+ destruct (in_dec zeq c q); eauto.
× elim Hnin.
simpl; auto.
× ∃ (self_c, rel_c, b, (z :: q) ++ c :: nil, ZSet.add c slow,
(n :: tq) ++ bound :: nil).
destruct (in_dec zeq c (z :: q)).
{ simpl in i.
destruct i; try contradiction.
elim n0; subst; reflexivity. }
{ auto. }
Qed.
Lemma QS_CalLock_pre_exist:
∀ e l x,
QS_CalLock (e::l) = Some x →
∃ x´, QS_CalLock l = Some x´.
Proof.
intros.
Local Transparent QS_CalLock.
simpl in H; subdestruct; try (inv H; fail); eauto.
Local Opaque QS_CalLock.
Qed.
Lemma QS_CalLock_app_exist:
∀ l´ l x,
QS_CalLock (l´++l) = Some x →
∃ x´, QS_CalLock l = Some x´.
Proof.
induction l´; intros.
- rewrite app_nil_l in H; eauto.
- simpl in H.
edestruct QS_CalLock_pre_exist; eauto.
Qed.
Lemma QS_CalLock_SET_NEXT_exists:
∀ l self_c rel_c b q slow tq c prev_id
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow , tq))
(Hqnnil: q ≠ nil)
(Hslow: ZSet.mem c slow = true)
(Hnin: ¬ In c q),
∃ x,
QS_CalLock (TEVENT c (TTICKET (SET_NEXT prev_id)) :: l) = Some x.
Proof.
Local Transparent QS_CalLock.
simpl; intros.
rewrite HCal.
exploit QS_CalLock_q_tq_length_same; eauto.
intros.
destruct q.
- elim Hqnnil; auto.
- destruct tq; inv H.
destruct (zeq c z); subst.
+ elim Hnin.
left; auto.
+ destruct (in_dec zeq c q); eauto.
× elim Hnin; simpl; auto.
× rewrite Hslow; eauto.
Qed.
Lemma QS_CalLock_LHOLD_implies_no_nil:
∀ l self_c rel_c b q slow tq
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow , tq))
(Hheadstat: b = LHOLD),
q ≠ nil.
Proof.
intros; simpl.
destruct l; intro; simpl; subst.
- simpl in HCal.
inversion HCal.
- simpl in HCal.
subdestruct.
Qed.
Lemma QS_CalLock_SET_NEXT_imply:
∀ curid l self_c rel_c b q slow tq prev_id,
QS_CalLock ((TEVENT curid (TTICKET (SET_NEXT prev_id)))::l)
= Some (self_c, rel_c, b, q, slow , tq) →
q ≠ nil ∧ tq ≠ nil ∧ ZSet.mem curid slow = false.
Proof.
intros.
simpl in H; subdestruct;
inversion H; subst.
- split. congruence.
split. congruence.
rewrite ZSet_mem_remove; auto.
- split. congruence.
split. congruence.
rewrite ZSet_mem_remove; auto.
- split. congruence.
split. congruence.
rewrite ZSet_mem_remove; auto.
- split. congruence.
split. congruence.
rewrite ZSet_mem_remove; auto.
Qed.
Lemma QS_CalLock_SET_NEXT_imply´:
∀ curid l self_c rel_c b q slow tq prev_id self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq) →
QS_CalLock (TEVENT curid (TTICKET (SET_NEXT prev_id))::l)
= Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
b = b´ ∧ q = q´ ∧ tq = tq´ ∧ slow´ = ZSet.remove curid slow.
Proof.
intros.
simpl in H0.
rewrite H in H0; subdestruct;
inversion H0; subst; tauto.
Qed.
Lemma QS_CalLock_GET_BUSY_false_imply:
∀ curid l self_c rel_c b q slow tq,
QS_CalLock (TEVENT curid (TTICKET (GET_BUSY false)) :: l)
= Some (self_c, rel_c, b, q, slow, tq) →
b = LHOLD ∧ self_c ≠ O ∧ (∃ q´, q = curid::q´).
Proof.
simpl; intros.
subdestruct; inversion H; try subst; eauto; try congruence.
Qed.
Lemma QS_CalLock_GET_BUSY_true_imply:
∀ curid l self_c rel_c b q1 q2 slow tq,
QS_CalLock (TEVENT curid (TTICKET (GET_BUSY true)) :: l)
= Some (self_c, rel_c, b, q1++(curid::q2), slow, tq) →
q1 ≠ nil.
Proof.
simpl; intros.
subdestruct; inversion H; try subst; eauto.
destruct q1.
- rewrite app_nil_l in H4, H.
inversion H4; subst.
elim n2; auto.
- intro contra; inversion contra.
Qed.
Lemma QS_CalLock_SWAP_TAIL_true_imply:
∀ curid bound l self_c rel_c b q slow tq,
QS_CalLock (TEVENT curid (TTICKET (SWAP_TAIL bound true)) :: l)
= Some (self_c, rel_c, b, curid :: q, slow, tq) →
b = LHOLD ∧ self_c ≠ O ∧ q = nil ∧ tq = bound::nil.
Proof.
simpl; intros.
subdestruct; inversion H; try subst; eauto; try congruence.
Qed.
Lemma QS_CalLock_oracle_In_onestep:
∀ j e l self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ c
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hj : j ≠ c)
(Hnin: In c q)
(HCal´: QS_CalLock (TEVENT j e :: l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)),
In c q´.
Proof.
Transparent QS_CalLock.
intros until c.
intros HCal Hj Hnin HCal´.
simpl in HCal´.
rewrite HCal in HCal´. clear HCal.
destruct e as [e | e ]; destruct e eqn:?; try congruence;
repeat match goal with
| [ HCal´ : context [match QS_CalLock ?lis with
| Some _ ⇒ _ | None ⇒ _ end] |- _]
⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
| [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
| [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
| [ HCal´ : context[ZMap.get ?X ?Y] |- _]
⇒ destruct (ZMap.get X Y)
end; try congruence.
+ simpl in Hnin; tauto.
+ replace q´ with ((z :: l0) ++ j :: nil) by congruence.
clear HCal´.
rewrite in_app.
simpl; intuition.
+ subst.
simpl in Hnin; tauto.
+ subst.
replace q´ with l0 by congruence.
simpl in Hnin; tauto.
Qed.
Lemma QS_CalLock_oracle_In:
∀ l´ l self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ c
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ c)
(Hnin: In c q)
(HCal´: QS_CalLock (l´ ++ l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)),
In c q´.
Proof.
Opaque QS_CalLock.
induction l´ as [|e l´].
× simpl.
intros.
replace q´ with q by congruence; auto.
× intros until c.
intros HCal Hdomain Hin HCal´.
simpl in ×.
assert (∀ (i0 : Z) (e0 : MultiOracleEventUnit), In (TEVENT i0 e0) l´ → i0 ≠ c) as Hdomain´.
{
intros k1 e1; specialize Hdomain with k1 e1; auto.
}
destruct e as [i0 e].
assert (i0 ≠ c).
{ eapply Hdomain; left; reflexivity. }
destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal´) as [self_c0 [rel_c0 [b0 [q0 [slow0 [tq0 HCal0]]]]]].
specialize (IHl´ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal Hdomain´ Hin HCal0).
eapply QS_CalLock_oracle_In_onestep; eauto.
Qed.
Lemma QS_CalLock_slowset_subset:
∀ l self_c rel_c b q slow tq c
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hmem: ZSet.mem c slow = true),
In c q.
Proof.
Transparent QS_CalLock.
induction l.
- simpl.
intros.
replace slow with ZSet.empty in Hmem by congruence.
inv HCal.
compute in Hmem0.
congruence.
- intros.
simpl in HCal.
destruct a.
destruct e as [e | e ]; destruct e eqn:?; try congruence;
repeat match goal with
| [ HCal´ : context [match QS_CalLock ?lis with
| Some _ ⇒ _ | None ⇒ _ end] |- _]
⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
| [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
| [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
| [ HCal´ : context[ZMap.get ?X ?Y] |- _]
⇒ destruct (ZMap.get X Y)
end; try congruence;
specialize (IHl _ _ _ _ _ _ c eq_refl);
inversion HCal; subst; clear HCal;
try match goal with [H´ : ZSet.mem _ ZSet.empty = true |- _ ] ⇒ compute in H´; congruence end;
auto.
+ change (z :: l2 ++ i :: nil) with ((z :: l2) ++ i :: nil).
apply in_or_app.
destruct (zeq c i).
× subst; simpl; auto.
× rewrite ZSet_gso in Hmem0 by auto.
change (z :: l2 ++ i :: nil) with ((z :: l2) ++ i :: nil).
left; auto.
+ apply ZSet_remove_preserves_not_in_contra in Hmem0.
auto.
+ apply ZSet_remove_preserves_not_in_contra in Hmem0.
auto.
+ apply ZSet_remove_preserves_not_in_contra in Hmem0.
auto.
+ apply ZSet_remove_preserves_not_in_contra in Hmem0.
auto.
+ destruct (zeq z c).
× subst.
rewrite negb_true_iff in Heqb0.
congruence.
× simpl in IHl.
tauto.
Qed.
Lemma QS_CalLock_q_slow_empty :
∀ l self_c rel_c b q slow tq
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
q = nil → slow = ZSet.empty.
Proof.
intros until tq.
intros HCal Hq.
apply ZSet.eq_leibniz.
intros z.
rewrite <- ZSet.mem_spec.
split.
- intros.
apply QS_CalLock_slowset_subset with (c:=z) in HCal.
subst; simpl in *; tauto.
assumption.
- intros HEmpty. apply ZSet.empty_spec in HEmpty.
tauto.
Qed.
Lemma QS_CalLock_oracle_Mem_onestep:
∀ res j e l self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ c
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hj : j ≠ c)
(Hmem: ZSet.mem c slow = res)
(HCal´: QS_CalLock (TEVENT j e :: l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)),
ZSet.mem c slow´ = res.
Proof.
Transparent QS_CalLock.
intros until c.
intros HCal Hj Hnin HCal´.
simpl in HCal´.
rewrite HCal in HCal´. destruct e as [e | e ]; destruct e eqn:?; try congruence;
repeat match goal with
| [ HCal´ : context [match QS_CalLock ?lis with
| Some _ ⇒ _ | None ⇒ _ end] |- _]
⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
| [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
| [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
| [ HCal´ : context[ZMap.get ?X ?Y] |- _]
⇒ destruct (ZMap.get X Y)
end; try congruence.
+ replace slow´ with (ZSet.empty) by congruence.
destruct res.
- assert (blah := QS_CalLock_slowset_subset _ _ _ _ _ _ _ c HCal Hnin).
simpl in blah.
tauto.
- reflexivity.
+ replace slow´ with (ZSet.add j slow) by congruence.
rewrite ZSet_gso; auto.
+ replace slow´ with ZSet.empty by congruence.
destruct res.
- subst.
assert (blah := QS_CalLock_slowset_subset _ _ _ _ _ _ _ c HCal Hnin).
simpl in blah.
tauto.
- reflexivity.
+ replace slow´ with (ZSet.remove j slow) by congruence.
rewrite ZSet_remove_gso ; auto.
+ replace slow´ with (ZSet.remove j slow) by congruence.
rewrite ZSet_remove_gso ; auto.
+ replace slow´ with (ZSet.remove j slow) by congruence.
rewrite ZSet_remove_gso ; auto.
+ replace slow´ with (ZSet.remove j slow) by congruence.
rewrite ZSet_remove_gso ; auto.
Qed.
Lemma QS_CalLock_oracle_Mem:
∀ l´ l self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ c
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ c)
(HCal´: QS_CalLock (l´ ++ l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)),
ZSet.mem c slow´ = ZSet.mem c slow.
Proof.
Opaque QS_CalLock.
induction l´ as [|e l´].
× simpl.
intros.
replace slow´ with slow by congruence; auto.
× intros until c.
intros HCal Hdomain HCal´.
simpl in ×.
assert (∀ (i0 : Z) (e0 : MultiOracleEventUnit), In (TEVENT i0 e0) l´ → i0 ≠ c) as Hdomain´.
{
intros k1 e1; specialize Hdomain with k1 e1; auto.
}
destruct e as [i0 e].
assert (i0 ≠ c).
{ eapply Hdomain; left; reflexivity. }
destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal´) as [self_c0 [rel_c0 [b0 [q0 [slow0 [tq0 HCal0]]]]]].
specialize (IHl´ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal Hdomain´ HCal0).
rewrite <- IHl´.
erewrite (QS_CalLock_oracle_Mem_onestep (ZSet.mem c slow0)); eauto.
Qed.
Lemma QS_CalLock_oracle_not_In:
∀ l´ l self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ c
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ c)
(Hnin: ¬ In c q)
(HCal´: QS_CalLock (l´ ++ l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)),
¬ In c q´.
Proof.
Local Transparent QS_CalLock.
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. }
destruct a; destruct e as [e|e]; [destruct e|];
subdestruct; inv HCal´; try (eapply (IHl´ l); eauto; fail);
try (red; intro; exploit (IHl´ l); eauto; right; trivial; fail).
× specialize (Hin _ _ (or_introl eq_refl)).
simpl; tauto.
× specialize (Hin _ _ (or_introl eq_refl)).
change (z :: l3 ++ i :: nil) with ((z::l3) ++ i::nil).
intros HF.
rewrite in_app in HF.
destruct HF as [HF | HF].
+ revert HF.
change (In c (z :: l3) → False) with (¬In c (z :: l3) ).
apply (IHl´ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal Hin_append Hnin Hdestruct0).
+ simpl in HF; tauto.
Qed.
Lemma QS_CalLock_oracle:
∀ l self_c rel_c b q slow tq c o
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_qs_oracle o)
(Hnin: ¬ In c q),
∃ self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock (o c l ++ l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)
∧ ¬ In c q´
∧ (∀ j, In j q → (0 < CalBound j (o c l ++ l))%nat).
Proof.
intros.
destruct Horacle_domain as (Horacle_domain0 & Horacle_domain1).
unfold valid_multi_oracle_domain in Horacle_domain0.
unfold valid_qs_oracle in ×.
specialize (Horacle_domain1 c l).
exploit Horacle_domain1.
exact HCal.
intros (self_c´ & rel_c´ & b´ & q´ & slow´ & tq´ & HCal´ & Hnbound´).
assert (HnotIn: ¬ In c q´).
{ eapply (QS_CalLock_oracle_not_In (o c l) l); eauto.
intros.
eapply Horacle_domain0 in H; eauto; tauto. }
refine_split´; eauto.
Qed.
Lemma valid_qslock_prefix_valid´:
∀ ll lh la
(Hli_valid: valid_qslock ll)
(ll_com: ll = lh::la),
valid_qslock la.
Proof.
destruct ll; intros; subst; try (inv ll_com; fail).
inversion ll_com; subst.
unfold valid_qslock in ×.
simpl.
destruct Hli_valid as (self_c & rel_c & b & q & slow & tq & Hli_valid).
Local Transparent QS_CalLock.
simpl in Hli_valid.
Opaque QS_CalLock.
subdestruct; (repeat (eexists); reflexivity).
Qed.
Lemma valid_qslock_prefix_valid:
∀ ll lp la
(Hli_valid: valid_qslock ll)
(ll_com: ll = lp++la),
valid_qslock la.
Proof.
induction ll; simpl; intros.
- destruct lp; simpl in ll_com; try (inv ll_com; fail).
subst; auto.
- destruct lp.
+ simpl in ll_com.
rewrite <- ll_com; auto.
+ simpl in ll_com.
inversion ll_com.
eapply valid_qslock_prefix_valid´ with (ll := a::ll) (lh := a) (la := ll)
in Hli_valid; eauto.
Qed.
Lemma QS_CalLock_oracle´:
∀ l self_c rel_c b slow q1 q2 tq1 tq2 c n o
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q1++c::q2, slow, tq1++n::tq2))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_qs_oracle o)
(Hleneq: length q1 = length tq1)
(Hnin: ¬ In c q1)
,
∃ self_c´ rel_c´ b´ q´ q´´ slow´ tq´,
QS_CalLock (o c l ++ l) = Some (self_c´, rel_c´, b´, q´++c::q´´, slow´, tq´)
∧ ¬ In c q´
∧ (∀ k, In k (q1++c::q2) → 0 < CalBound k (o c l ++ l))%nat.
Proof.
intros.
destruct Horacle_domain as (Horacle_domain & Horacle_valid).
unfold valid_qs_oracle in ×.
specialize (Horacle_valid c l).
exploit Horacle_valid; try exact HCal.
intros (self_c´ & rel_c´ & b´ & q´ & slow´ & tq´ & HCal´ & Hnbound´).
assert (ValidQSLock: CalMCSLock.valid_qslock l).
{ assert (valid_qslock (o c l ++ l)).
{ unfold valid_qslock.
repeat eexists; eauto. }
eapply valid_qslock_prefix_valid with (ll := o c l ++ l) in H; eauto. }
assert (In c q´).
{ assert (Hdomain : ∀ k e, In (TEVENT k e) (o c l) → k ≠ c)
by (intros k e; apply (Horacle_domain c k e)).
assert (Hin : In c (q1 ++ c :: q2))
by (rewrite in_app; simpl; tauto).
apply (QS_CalLock_oracle_In _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal Hdomain Hin HCal´).
}
assert (q´_prop: ∃ q1´ q2´, q´ = q1´++c::q2´).
{ apply in_split; auto. }
destruct q´_prop as (q1´&q2´&q´´_prop).
subst.
∃ self_c´, rel_c´, b´, q1´, q2´, slow´, tq´.
split; try tauto.
split; try tauto.
{
apply QS_CalLock_NoDup in HCal´.
rewrite NoDup_app in HCal´.
destruct HCal´ as [_ [_ Hnodup]].
specialize (Hnodup c).
simpl in Hnodup.
tauto.
}
Qed.
Lemma QS_CalLock_SWAP_TAIL_exists´:
∀ l self_c rel_c b q slow tq n c o
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_qs_oracle o)
(Hnin: ¬ In c q),
∃ x,
QS_CalLock (TEVENT c (TTICKET (SWAP_TAIL n false)) :: (o c l ++ l)) = Some x ∨
QS_CalLock (TEVENT c (TTICKET (SWAP_TAIL n true)) :: (o c l ++ l)) = Some x.
Proof.
intros.
exploit QS_CalLock_oracle; eauto.
intros (self_c´ & rel_c´ & b´ & q´ & slow´ & tq´ & HCal´ & HnotIn & Hother).
destruct q´.
- remember nil as q´.
generalize Heqq´; intros Heqtq´.
Local Transparent QS_CalLock.
rewrite <- QS_CalLock_q_tq_length_same_nil with (tq := tq´) in Heqtq´; eauto; subst.
∃ (S n, S CalPassLockTime, LHOLD, c::nil, ZSet.empty, n::nil); right;
simpl.
rewrite HCal´; auto.
- assert (nnilq´: z::q´ ≠ nil).
{ intros contra; inversion contra. }
generalize nnilq´; intros nniltq´.
rewrite <- QS_CalLock_q_tq_length_same_not_nil with (tq := tq´) in nniltq´; eauto.
destruct tq´; try (elim nniltq´; eauto; fail).
∃ (self_c´, rel_c´, b´, (z::q´)++(c::nil), ZSet.add c slow´, (n0::tq´)++(n::nil)); left;
simpl.
rewrite HCal´; eauto.
rewrite zeq_false; [ | intro contra; elim HnotIn; simpl; auto].
destruct (in_dec zeq c (z::q´)); try auto.
elim HnotIn; auto.
Local Opaque QS_CalLock.
Qed.
Lemma QS_CalLock_SET_NEXT_exists´:
∀ l self_c rel_c b q slow tq c prev_id o
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow , tq))
(Hqnnil: q ≠ nil)
(Hslow: ZSet.mem c slow = true)
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_qs_oracle o)
(Hnin: ¬ In c q),
∃ x,
QS_CalLock (TEVENT c (TTICKET (SET_NEXT prev_id)) ::(o c l ++ l)) = Some x.
Proof.
Local Transparent QS_CalLock.
simpl; intros.
exploit QS_CalLock_oracle; eauto.
intros (self_c´ & rel_c´ & b´ & q´ & slow´ & tq´ & HCal´ & HnotIn & Hother).
generalize HCal´; intros HCal´´.
destruct Horacle_domain.
unfold valid_multi_oracle_domain in H.
eapply QS_CalLock_oracle_Mem with (c := c) in HCal´´; eauto.
rewrite HCal´.
destruct q´.
- assert (tq´ = nil).
{ generalize HCal´; intro HCal´´´.
eapply QS_CalLock_q_tq_length_same_nil in HCal´´´.
destruct HCal´´´.
eauto. }
subst.
eapply QS_CalLock_q_slow_empty in HCal´.
subst.
rewrite ZSet_mem_empty in HCal´´.
rewrite Hslow in HCal´´.
congruence.
reflexivity.
- destruct tq´.
+ eapply QS_CalLock_q_tq_length_same_not_nil in HCal´.
destruct HCal´.
elim H2.
intro contra; inv contra.
reflexivity.
+ rewrite zeq_false.
rewrite HCal´´, Hslow.
eauto.
intro contra; elim HnotIn; subst.
simpl; auto.
- intros.
exploit H; eauto; intros; tauto.
Qed.
End WITHCALLOCK.
Fixpoint CalSumWaitSlow (q : list Z) (slow: ZSet.t) : nat :=
match q with
| nil ⇒ 0%nat
| i :: q´ ⇒ if ZSet.mem i slow
then S (CalSumWaitSlow q´ slow)
else CalSumWaitSlow q´ slow
end.
Lemma CalSumWaitSlow_remove_mono : ∀ q slow i,
(CalSumWaitSlow q (ZSet.remove i slow) ≤ CalSumWaitSlow q slow)%nat.
Proof.
induction q as [| a q].
+ simpl; auto.
+ simpl.
intros slow i.
specialize (IHq slow i).
destruct (zeq a i).
- subst.
destruct (ZSet.mem i slow) eqn:H_mem.
× rewrite ZSet_mem_remove.
auto.
× rewrite ZSet_remove_preserves_not_in by auto.
auto.
- rewrite ZSet_remove_gso by auto.
destruct (ZSet.mem a slow); omega.
Qed.
Lemma CalSumWaitSlow_remove_first : ∀ j q slow,
ZSet.mem j slow = true →
(S (CalSumWaitSlow (j :: q) (ZSet.remove j slow)) ≤ (CalSumWaitSlow (j :: q) slow))%nat.
Proof.
intros.
simpl.
rewrite H.
rewrite ZSet_mem_remove.
pose (CalSumWaitSlow_remove_mono q slow j).
omega.
Qed.
Lemma CalSumWaitSlow_add : ∀ q slow i,
¬In i q →
(CalSumWaitSlow q (ZSet.add i slow) = CalSumWaitSlow q slow)%nat.
Proof.
induction q.
× simpl; auto.
× simpl.
intros.
rewrite ZSet_gso by tauto.
destruct (ZSet.mem a slow); rewrite IHq; auto.
Qed.
Lemma CalSumWaitSlow_cons :∀ z q slow,
(CalSumWaitSlow q slow ≤ CalSumWaitSlow (z :: q) slow)%nat.
Proof.
intros.
simpl.
destruct (ZSet.mem z slow); omega.
Qed.
Opaque CalSumWaitSlow.
Definition decrease_number (self_c rel_c: nat) (h: head_status) (z : Z) (q : list Z) (slow: ZSet.t)
(tq: list nat) (ll: MultiLog) :=
match h with
| LEMPTY ⇒ ((CalBound (hd z q) ll) + (CalSumWaitSlow q slow + CalMCSLock.CalSumWait tq) × CalMCSLock.WaitConstant) % nat
| _ ⇒ ((CalBound (hd z q) ll) +
(rel_c + self_c + CalSumWaitSlow q slow + CalMCSLock.CalSumWait (rm_head tq)) × CalMCSLock.WaitConstant)%nat
end.
Definition until_SWAP_TAIL_true (l: MultiLog) (curid: Z) (bound : nat) (to : MultiOracle) : MultiLog :=
(TEVENT curid (TTICKET (SWAP_TAIL bound true)))::(to curid l++l).
Definition until_SWAP_TAIL_false (l: MultiLog) (curid: Z) (bound : nat) (to : MultiOracle) : MultiLog :=
(TEVENT curid (TTICKET (SWAP_TAIL bound false)))::(to curid l++l).
Definition until_SET_NEXT (l: MultiLog) (curid: Z) (prev_id : Z) (bound : nat) (to : MultiOracle) : MultiLog :=
(TEVENT curid (TTICKET (SET_NEXT prev_id)))::
((to curid ((TEVENT curid (TTICKET (SWAP_TAIL bound false)))::(to curid l++l)))
++((TEVENT curid (TTICKET (SWAP_TAIL bound false)))::(to curid l++l))).
Lemma until_SET_NEXT_imples_until_SWAP_TAIL_false_and_other:
∀ l curid prev_id bound to,
(TEVENT curid (TTICKET (SET_NEXT prev_id)))
:: ((to curid ((TEVENT curid (TTICKET (SWAP_TAIL bound false)))::(to curid l++l)))
++((TEVENT curid (TTICKET (SWAP_TAIL bound false)))::(to curid l++l))) =
(TEVENT curid (TTICKET (SET_NEXT prev_id)))
::(to curid (until_SWAP_TAIL_false l curid bound to))++(until_SWAP_TAIL_false l curid bound to).
Proof.
intros; simpl.
unfold until_SWAP_TAIL_false; auto.
Qed.
Lemma MCS_CalLock_progress_onestep:
∀ j e l tq q self_c self_c´ rel_c rel_c´ b b´ z bound q0 tq0 lq ltq slow slow´
(Hlen: length tq = length q)
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q ++ z :: q0, slow, tq ++ bound :: tq0))
(Hj : j ≠ z)
(Hfairness : ∀ k, In k (q ++ z :: nil) → (0 < CalBound k (TEVENT j e :: l))%nat)
(Hnin: ¬ In z q)
(HCal´: QS_CalLock (TEVENT j e :: l) = Some (self_c´, rel_c´, b´, lq, slow´, 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´ rel_c´ b´ z q´´ slow´ tq´´ (TEVENT j e :: l) <
decrease_number self_c rel_c b z q slow tq l)%nat.
Proof.
Transparent QS_CalLock.
Opaque CalBound.
intros until slow´.
intros Hlen HCal Hj Hfairness Hnin HCal´.
simpl in HCal´.
rewrite HCal in HCal´. clear HCal.
destruct e as [e | e ]; [destruct e eqn:? | ]; try congruence;
repeat match goal with
| [ HCal´ : context [match QS_CalLock ?lis with
| Some _ ⇒ _ | None ⇒ _ end] |- _]
⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
| [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[if ZSet.mem ?X ?Y then _ else _] |- _] ⇒ destruct (ZSet.mem X Y) eqn:?
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
| [ HCal´ : context[ZMap.get ?X ?Y] |- _] ⇒ destruct (ZMap.get X Y)
| [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
end; try congruence;
inversion HCal´.
+
destruct q; simpl in *; congruence.
+
∃ nil. ∃ q.
∃ (q0 ++ j :: nil).
∃ nil. ∃ tq.
∃ (tq0 ++ n :: nil).
split. {
replace (q ++ z :: q0 ++ j :: nil) with ((q ++ z :: q0) ++ j :: nil) by (rewrite <- app_assoc; reflexivity).
congruence.
}
split. {
replace (tq ++ bound :: tq0 ++ n :: nil) with ((tq ++ bound :: tq0) ++ n :: nil) by (rewrite <- app_assoc; reflexivity).
congruence.
}
split. reflexivity.
split. reflexivity.
split. assumption.
assert (CalBound (hd z q) (TEVENT j (TTICKET (SWAP_TAIL n false)) :: l) < CalBound (hd z q) l)%nat.
{
apply CalBound_decreasing.
× destruct q.
- subst; simpl in ×.
assert (z = z0) by congruence; subst; auto.
- simpl in ×.
inversion Heql0.
subst.
auto.
× eapply CalBound_inv.
apply Hfairness.
destruct q; simpl; auto.
}
unfold decrease_number.
assert (¬In j q).
{
replace (z0 :: l0) with (q ++ z :: q0) in n2.
rewrite in_app in n2.
tauto.
}
rewrite CalSumWaitSlow_add by assumption.
destruct b´;
omega.
+
subst.
destruct q.
- simpl in ×. congruence.
- simpl in ×. inversion Heql0.
assert ((length (q ++ z :: q0) > length (@nil Z))%nat).
{
rewrite app_length; simpl; omega.
}
rewrite H1 in H.
simpl in H.
omega.
+
subst.
destruct q.
- simpl in ×. congruence.
- simpl in ×. inversion Heql0.
assert ((length (q ++ z :: q0) > length (@nil Z))%nat).
{
rewrite app_length; simpl; omega.
}
rewrite H1 in H.
simpl in H.
omega.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
unfold decrease_number.
simpl.
assert (0 < CalBound (hd z q) (TEVENT j (TTICKET (CAS_TAIL false)) :: l)) %nat
by (apply Hfairness; destruct q; simpl; auto).
assert (CalBound (hd z q) (TEVENT j (TTICKET (CAS_TAIL false)) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (CalBound (hd z q) l < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
omega.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
unfold decrease_number.
simpl.
assert (0 < CalBound (hd z q) (TEVENT j (TTICKET (CAS_TAIL false)) :: l)) %nat
by (apply Hfairness; destruct q; simpl; auto).
assert (CalBound (hd z q) (TEVENT j (TTICKET (CAS_TAIL false)) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (CalBound (hd z q) l < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
omega.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
replace slow´ with slow by congruence.
unfold decrease_number.
replace ((S rel_c´ + self_c´ + CalSumWaitSlow q slow + CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant)%nat
with (WaitConstant + (rel_c´ + self_c´ + CalSumWaitSlow q slow +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant)%nat
by (replace ((S rel_c´ + self_c´ + CalSumWaitSlow q slow + CalMCSLock.CalSumWait (rm_head tq)))%nat
with (S (rel_c´ + self_c´ + CalSumWaitSlow q slow + CalMCSLock.CalSumWait (rm_head tq)))%nat by omega;
reflexivity).
assert (0 < CalBound (hd z q) (TEVENT j (TTICKET GET_NEXT) :: l)) %nat
by (apply Hfairness; destruct q; simpl; auto).
assert (CalBound (hd z q) (TEVENT j (TTICKET GET_NEXT) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (CalBound (hd z q) l < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
omega.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
destruct (zeq j (hd z q)).
- unfold decrease_number.
destruct q as [|j´ q]; [simpl in *; congruence |].
replace j´ with j in × by (simpl in *; congruence).
simpl in ×.
assert (CalBound j (TEVENT j (TTICKET (SET_NEXT old_tail)) :: l) < WaitConstant)%nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
apply lt_le_trans with
(CalBound j l + (S (CalSumWaitSlow (j :: q) (ZSet.remove j slow)) + CalMCSLock.CalSumWait tq) × WaitConstant)%nat.
× simpl.
replace (CalBound j l + (WaitConstant + (CalSumWaitSlow (j :: q) (ZSet.remove j slow) +
CalMCSLock.CalSumWait tq) × WaitConstant))%nat
with (WaitConstant + (CalBound j l + (CalSumWaitSlow (j :: q) (ZSet.remove j slow) +
CalMCSLock.CalSumWait tq) × WaitConstant))%nat
by omega.
apply plus_lt_le_compat.
assumption.
omega.
× apply plus_le_compat_l.
apply mult_le_compat_r.
apply plus_le_compat_r.
apply (CalSumWaitSlow_remove_first j q slow).
assumption.
- unfold decrease_number.
apply plus_lt_le_compat.
× apply CalBound_decreasing.
{ congruence. }
{ eapply CalBound_inv.
apply Hfairness.
destruct q; simpl; auto. }
× apply mult_le_compat_r.
apply plus_le_compat_r.
apply CalSumWaitSlow_remove_mono.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
destruct (zeq j (hd z q)).
- unfold decrease_number.
destruct q as [|j´ q]; [simpl in *; congruence |].
replace j´ with j in × by (simpl in *; congruence).
simpl in ×.
assert (CalBound j (TEVENT j (TTICKET (SET_NEXT old_tail)) :: l) < WaitConstant)%nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
apply lt_le_trans with
(CalBound j l + (S (CalSumWaitSlow (j :: q) (ZSet.remove j slow)) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant)%nat.
× simpl.
replace (CalBound j l + (WaitConstant + (CalSumWaitSlow (j :: q) (ZSet.remove j slow) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant))%nat
with (WaitConstant + (CalBound j l + (CalSumWaitSlow (j :: q) (ZSet.remove j slow) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant))%nat
by omega.
apply plus_lt_le_compat.
assumption.
replace (CalSumWaitSlow (j :: q) (ZSet.remove j slow) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq))%nat
with (rel_c´ + self_c´ + CalSumWaitSlow (j :: q) (ZSet.remove j slow) +
CalMCSLock.CalSumWait (rm_head tq))%nat by omega.
omega.
× apply plus_le_compat_l.
apply mult_le_compat_r.
apply plus_le_compat_r.
replace (rel_c´ + self_c´ + CalSumWaitSlow (j :: q) slow)%nat
with (CalSumWaitSlow (j :: q) slow + rel_c´ + self_c´)%nat by omega.
apply plus_le_compat_r.
apply plus_le_compat_r.
apply (CalSumWaitSlow_remove_first j q slow).
assumption.
- unfold decrease_number.
apply plus_lt_le_compat.
× apply CalBound_decreasing.
{ congruence. }
{ eapply CalBound_inv.
apply Hfairness.
destruct q; simpl; auto. }
× apply mult_le_compat_r.
apply plus_le_compat_r.
apply plus_le_compat_l.
apply CalSumWaitSlow_remove_mono.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
destruct (zeq j (hd z q)).
- unfold decrease_number.
destruct q as [|j´ q]; [simpl in *; congruence |].
replace j´ with j in × by (simpl in *; congruence).
simpl in ×.
assert (CalBound j (TEVENT j (TTICKET (SET_NEXT old_tail)) :: l) < WaitConstant)%nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
apply lt_le_trans with
(CalBound j l + (S (CalSumWaitSlow (j :: q) (ZSet.remove j slow)) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant)%nat.
× simpl.
replace (CalBound j l + (WaitConstant + (CalSumWaitSlow (j :: q) (ZSet.remove j slow) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant))%nat
with (WaitConstant + (CalBound j l + (CalSumWaitSlow (j :: q) (ZSet.remove j slow) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant))%nat
by omega.
apply plus_lt_le_compat.
assumption.
replace (CalSumWaitSlow (j :: q) (ZSet.remove j slow) + rel_c´ + self_c´ +
CalMCSLock.CalSumWait (rm_head tq))%nat
with (rel_c´ + self_c´ + CalSumWaitSlow (j :: q) (ZSet.remove j slow) +
CalMCSLock.CalSumWait (rm_head tq))%nat by omega.
omega.
× apply plus_le_compat_l.
apply mult_le_compat_r.
apply plus_le_compat_r.
replace (rel_c´ + self_c´ + CalSumWaitSlow (j :: q) slow)%nat
with (CalSumWaitSlow (j :: q) slow + rel_c´ + self_c´)%nat by omega.
apply plus_le_compat_r.
apply plus_le_compat_r.
apply (CalSumWaitSlow_remove_first j q slow).
assumption.
- unfold decrease_number.
apply plus_lt_le_compat.
× apply CalBound_decreasing.
{ congruence. }
{ eapply CalBound_inv.
apply Hfairness.
destruct q; simpl; auto. }
× apply mult_le_compat_r.
apply plus_le_compat_r.
apply plus_le_compat_l.
apply CalSumWaitSlow_remove_mono.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
unfold decrease_number.
assert (CalBound (hd z q) (TEVENT j (TTICKET (SET_NEXT old_tail)) :: l)
< CalBound (hd z q) l)%nat.
{
apply CalBound_decreasing.
destruct q; simpl in *; congruence.
eapply CalBound_inv; apply Hfairness; destruct q; simpl; auto.
}
assert (CalSumWaitSlow q (ZSet.remove j slow) ≤ CalSumWaitSlow q slow)%nat.
{
apply CalSumWaitSlow_remove_mono.
}
destruct b´;
(apply plus_lt_le_compat;
[ assumption
| apply mult_le_compat_r; apply plus_le_compat_r; repeat apply plus_le_compat_l; assumption]).
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
destruct q as [|? ?]; [simpl in *; subst; inversion Heql0; congruence | ].
destruct tq as [|? ?]; [simpl in Hlen; congruence | ].
simpl in ×.
inversion Heql0.
inversion Heql1.
subst.
replace ((fairness + S n + CalSumWaitSlow (z0 :: q) slow´ + CalMCSLock.CalSumWait tq))%nat
with (S (fairness + n + CalMCSLock.CalSumWait tq + CalSumWaitSlow (z0 :: q) slow´))%nat by omega.
replace ((CalSumWaitSlow (z0 :: q) slow´ + S (S (S (S (S (fairness + n + CalMCSLock.CalSumWait tq)))))) )%nat
with (( S (S (S (S (S (fairness + n + CalMCSLock.CalSumWait tq + CalSumWaitSlow (z0 :: q) slow´)))))))%nat
by omega.
simpl.
assert (CalBound z0 (TEVENT z0 (TTICKET (GET_BUSY false)) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (0 < CalBound z0 (TEVENT z0 (TTICKET (GET_BUSY false)) :: l)) %nat
by (apply Hfairness; destruct q; simpl; auto).
omega.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
destruct q as [|? ?]; [simpl in *; subst; inversion Heql0; congruence | ].
destruct tq as [|? ?]; [simpl in Hlen; congruence | ].
simpl in ×.
inversion Heql0.
inversion Heql1.
subst.
replace ((fairness + S n + CalSumWaitSlow (z0 :: q) slow´ + CalMCSLock.CalSumWait tq))%nat
with (S (fairness + n + CalMCSLock.CalSumWait tq + CalSumWaitSlow (z0 :: q) slow´))%nat by omega.
replace ((CalSumWaitSlow (z0 :: q) slow´ + S (S (S (S (S (fairness + n + CalMCSLock.CalSumWait tq)))))) )%nat
with (( S (S (S (S (S (fairness + n + CalMCSLock.CalSumWait tq + CalSumWaitSlow (z0 :: q) slow´)))))))%nat
by omega.
simpl.
assert (CalBound z0 (TEVENT z0 (TTICKET (GET_BUSY false)) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (0 < CalBound z0 (TEVENT z0 (TTICKET (GET_BUSY false)) :: l)) %nat
by (apply Hfairness; destruct q; simpl; auto).
omega.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
assert (CalBound (hd z q) (TEVENT j (TTICKET (GET_BUSY true)) :: l) < CalBound (hd z q) l)%nat.
{
apply CalBound_decreasing.
× destruct q.
- subst; simpl in ×.
assert (z = z0) by congruence; subst; auto.
- simpl in ×.
inversion Heql0.
subst.
auto.
× eapply CalBound_inv.
apply Hfairness.
destruct q; simpl; auto.
}
unfold decrease_number.
destruct b´;
omega.
+
destruct q ; [simpl in *; inversion Heql0; congruence | ].
destruct tq; [simpl in Hlen; congruence | ].
∃ (z0::nil). ∃ q. ∃ q0.
∃ (n::nil). ∃ tq. ∃ tq0.
split. {
simpl in Heql0.
inversion Heql0.
congruence.
}
split. {
simpl in Heql1.
inversion Heql1.
congruence.
}
split. {
simpl in Heql0.
inversion Heql0.
reflexivity.
}
split. {
simpl in Heql1.
inversion Heql1.
reflexivity.
}
split. {
simpl in Hlen.
inversion Hlen.
reflexivity.
}
unfold decrease_number.
simpl.
assert (CalBound (hd z q) (TEVENT j (TTICKET SET_BUSY) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (CalBound (hd z q) l < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
replace (n0 + self_c + CalSumWaitSlow (z1 :: q) slow´ + CalMCSLock.CalSumWait tq)%nat
with ((n0 + self_c) + (CalSumWaitSlow (z1 :: q) slow´ + CalMCSLock.CalSumWait tq))%nat
by omega.
replace ((n0 + self_c + (CalSumWaitSlow (z1 :: q) slow´ + CalMCSLock.CalSumWait tq)) × WaitConstant) %nat
with ((n0 + self_c) × WaitConstant + (CalSumWaitSlow (z1 :: q) slow´ + (CalMCSLock.CalSumWait tq)) × WaitConstant)%nat
by (remember (n0 + self_c)%nat as blah; repeat rewrite mult_plus_distr_r; omega).
repeat rewrite plus_assoc.
apply plus_lt_le_compat.
- apply lt_le_trans with (CalBound z1 l + WaitConstant)%nat; [omega | now apply le_plus_l].
- apply mult_le_compat_r.
apply plus_le_compat_r.
apply CalSumWaitSlow_cons.
+
∃ nil. ∃ q. ∃ q0.
∃ nil. ∃ tq. ∃ tq0.
split. congruence.
split. congruence.
split. reflexivity.
split. reflexivity.
split. assumption.
unfold decrease_number.
replace ((rel_c´ + S self_c´ + CalSumWaitSlow q slow´ + CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant)%nat
with (WaitConstant + (rel_c´ + self_c´ + CalSumWaitSlow q slow´ +
CalMCSLock.CalSumWait (rm_head tq)) × WaitConstant)%nat
by (replace ((rel_c´ + S self_c´ + CalSumWaitSlow q slow´ + CalMCSLock.CalSumWait (rm_head tq)))%nat
with (S (rel_c´ + self_c´ + CalSumWaitSlow q slow´ + CalMCSLock.CalSumWait (rm_head tq)))%nat
by omega; reflexivity).
assert (0 < CalBound (hd z q) (TEVENT j (TSHARED e) :: l)) %nat
by (apply Hfairness; destruct q; simpl; auto).
assert (CalBound (hd z q) (TEVENT j (TSHARED e) :: l) < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
assert (CalBound (hd z q) l < WaitConstant) %nat
by (apply le_lt_trans with fairness; [apply CalBound_upper_bound | apply WaitConstant_fairness]).
omega.
Qed.
Lemma self_c_upper_bound : ∀ l self_c rel_c b q slow tq
(HCal : QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
(self_c ≤ S (hd 0 tq) ∧ rel_c ≤ WaitConstant)%nat.
Proof.
induction l.
+ simpl.
intros.
replace self_c with 0%nat by congruence.
replace rel_c with 0%nat by congruence.
split; omega.
+ simpl.
pose WaitConstant_PassLockTime.
destruct (QS_CalLock l) as [ [[[[[self_c rel_c] b] q] slow] tq ] |];
destruct a as [i e];
intros self_c´ rel_c´ b´ q´ slow´ tq´ HCal´; try congruence.
destruct e as [e | e ]; [destruct e eqn:? | ]; try congruence;
repeat match goal with
| [ HCal´ : context [match QS_CalLock ?lis with
| Some _ ⇒ _ | None ⇒ _ end] |- _]
⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
| [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
| [ HCal´ : context[ZMap.get ?X ?Y] |- _] ⇒ destruct (ZMap.get X Y)
| [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
end; try congruence;
inversion HCal´;
specialize (IHl _ _ _ _ _ _ eq_refl); destruct IHl;
split; simpl in *; omega.
Qed.
Global Opaque WaitConstant.
Global Opaque CalPassLockTime.
Lemma CalSumWaitSlow_le_length : ∀ slow q,
(CalSumWaitSlow q slow ≤ length q)%nat.
Proof.
Local Transparent CalSumWaitSlow.
induction q as [| a q].
+ simpl; auto.
+ simpl; destruct (ZSet.mem a slow); omega.
Opaque CalSumWaitSlow.
Qed.
Lemma le_plus_trans_l : ∀ p n m, (n ≤ m → n ≤ p+m)%nat.
Proof.
intros.
rewrite plus_comm.
apply le_plus_trans; auto.
Qed.
Lemma decrease_number_upper_bound : ∀ self_c rel_c b i q slow tq q´ slow´ tq´ l,
QS_CalLock l = Some (self_c, rel_c, b, q++q´, slow´, tq++tq´) →
tq ≠ nil →
length q = length tq →
((decrease_number self_c rel_c b i q slow tq l) + WaitConstant
< CalWaitLockTime tq)%nat.
Proof.
intros until l.
intros HCal Hnonnil Hlen.
apply self_c_upper_bound in HCal; destruct HCal as [H1 H2].
rewrite plus_comm.
unfold decrease_number.
unfold CalWaitLockTime.
rewrite <- Hlen.
clear Hlen.
destruct tq as [|n tq0]; [congruence|].
destruct b.
+ simpl in ×.
apply plus_lt_compat_l.
apply plus_lt_le_compat.
apply le_lt_trans with fairness.
apply CalBound_upper_bound.
apply WaitConstant_fairness.
apply le_plus_trans_l.
apply le_plus_trans_l.
apply le_plus_trans_l.
replace (WaitConstant + length q)%nat with (length q + WaitConstant)%nat by omega.
apply mult_le_compat_r.
apply plus_le_compat.
- apply le_plus_trans. apply CalSumWaitSlow_le_length.
- auto.
+ simpl in ×.
apply plus_lt_compat_l.
apply plus_lt_le_compat.
{ apply le_lt_trans with fairness.
apply CalBound_upper_bound.
apply WaitConstant_fairness. }
{
apply le_plus_trans_l.
apply le_plus_trans_l.
apply le_plus_trans_l.
apply mult_le_compat_r.
repeat rewrite <- plus_assoc.
apply plus_le_compat.
× assumption.
×
replace (length q + S (S (S (CalPassLockTime + (n + CalMCSLock.CalSumWait tq0)))))%nat
with (S n + (length q + (S (S (CalPassLockTime + (CalMCSLock.CalSumWait tq0))))))%nat
by omega.
apply plus_le_compat.
+ assumption.
+ apply plus_le_compat.
- apply CalSumWaitSlow_le_length.
- omega.
}
+ simpl in ×.
apply plus_lt_compat_l.
apply plus_lt_le_compat.
{ apply le_lt_trans with fairness.
apply CalBound_upper_bound.
apply WaitConstant_fairness. }
{
apply le_plus_trans_l.
apply le_plus_trans_l.
apply le_plus_trans_l.
apply mult_le_compat_r.
repeat rewrite <- plus_assoc.
apply plus_le_compat.
× assumption.
×
replace (length q + S (S (S (CalPassLockTime + (n + CalMCSLock.CalSumWait tq0)))))%nat
with (S n + (length q + (S (S (CalPassLockTime + (CalMCSLock.CalSumWait tq0))))))%nat
by omega.
apply plus_le_compat.
+ assumption.
+ apply plus_le_compat.
- apply CalSumWaitSlow_le_length.
- omega.
}
Qed.
Lemma lt_le : ∀ n m,
(n < m)%nat → (n ≤ m)%nat.
Proof.
intros.
omega.
Qed.
Lemma MCS_CalLock_progress:
∀ l´ l tq q self_c self_c´ rel_c rel_c´ b b´ z bound q0 tq0 lq ltq slow slow´
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q ++ z :: q0, slow, tq ++ bound :: tq0))
(HCal´: QS_CalLock (l´ ++ l) = Some (self_c´, rel_c´, b´, lq, slow´, ltq))
(Hlen: length tq = length q)
(Hdomain: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ z)
(Hfairness : ∀ k, In k (q ++ z :: nil) → (0 < CalBound k (l´ ++ l))%nat)
(Hnin: ¬ In z q),
∃ 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´ rel_c´ b´ z q´´ slow´ tq´´ (l´++l) ≤
decrease_number self_c rel_c b z q slow tq l)%nat.
Proof.
Opaque QS_CalLock.
induction l´; simpl; intros.
- ∃ nil, q, q0, nil, tq, tq0.
rewrite HCal in HCal´.
inv HCal´.
refine_split´; eauto.
- destruct a as [j e].
destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal´)
as [self_cp [rel_cp [bp [qp [slowp [tqp HCalp]]]]]].
assert (Hdomainp : (∀ i0 e0, In (TEVENT i0 e0) l´ → i0 ≠ z))
by (intros; eapply Hdomain; eauto).
assert (Hfairnessp : ∀ k : Z, In k (q ++ z :: nil) → (0 < CalBound k (l´ ++ l))%nat).
{
intros.
apply CalBound_inv with (TEVENT j e).
apply Hfairness; auto.
}
specialize (IHl´ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal HCalp Hlen Hdomainp Hfairnessp Hnin).
destruct IHl´ as [iq´ [iq´´ [iq1 [itq´ [itq´´ [itq1 [Hiqp [Hitqp [Hiq [Hitq [IHlen IHdecrease]]]]]]]]]]].
rewrite Hiqp in HCalp.
rewrite Hitqp in HCalp.
assert (Hj : j ≠ z).
{
eapply Hdomain; auto.
}
assert (Hfairness´ : ∀ k : Z, In k (iq´´ ++ z :: nil) → (0 < CalBound k (TEVENT j e :: l´ ++ l))%nat).
{
intros.
apply Hfairness.
rewrite Hiq.
rewrite <- app_assoc.
repeat rewrite in_app.
rewrite in_app in H.
tauto.
}
assert (Hnin´ : ¬ In z iq´´).
{
rewrite Hiq in Hnin.
rewrite in_app in Hnin.
tauto.
}
destruct (MCS_CalLock_progress_onestep _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ IHlen HCalp Hj Hfairness´ Hnin´ HCal´)
as [rq´ [rq´´ [rq1 [rtq´ [rtq´´ [rtq1 [? [? [? [? [? Hdecrease]]]]]]]]]]].
∃ (iq´ ++ rq´).
∃ rq´´.
∃ rq1.
∃ (itq´ ++ rtq´).
∃ rtq´´.
∃ rtq1.
repeat split; try rewrite <- app_assoc; try congruence.
apply (le_trans _ _ _ (lt_le _ _ Hdecrease) IHdecrease).
Qed.
Lemma CalWaitGet_exist´:
∀ wait_time ll self_c rel_c b lq slow ltq n curid o lq´ ltq´
(HCal: QS_CalLock ll = Some (self_c, rel_c, b, lq ++ curid :: lq´, slow, ltq ++ n :: ltq´))
(Hlen: length lq = length ltq)
(Hgt: (decrease_number self_c rel_c b curid lq slow ltq ll < wait_time)%nat)
(Horacle_domain : valid_multi_oracle_domain o
∧ valid_qs_oracle o)
(Hnin: ¬ In curid lq)
(Hnslow: ZSet.mem curid slow = false),
∃ ll´, QS_CalWaitGet wait_time curid ll o = Some ll´.
Proof.
induction wait_time; intros ; try (inv Hgt; fail).
- destruct Horacle_domain as (Horacle_domain1 & Horacle_domain2).
Local Transparent QS_CalWaitGet.
simpl.
edestruct QS_CalLock_oracle´ as (self_c´ & rel_c´ & b´ & q1´ & q2´ & slow´ & tq´ & HQS_Cal & Hnotin´ & Hbound); eauto.
rewrite HQS_Cal.
destruct q1´.
+ simpl.
rewrite zeq_true.
assert (tq_n_nil: tq´ ≠ nil).
{ assert (length (curid::q2´) = length tq´).
{ eapply QS_CalLock_q_tq_length_same in HQS_Cal.
simpl in HQS_Cal; simpl.
symmetry in HQS_Cal; assumption. }
destruct tq´; try inv H.
intro contra.
inv contra. }
destruct tq´; try (elim tq_n_nil; reflexivity; fail).
eexists; try eauto.
+ simpl.
assert (curid ≠ z).
{ intro contra; elim Hnotin´; simpl; auto. }
rewrite zeq_false; try omega.
assert (∀ k : Z, In k (lq ++ curid :: nil) → (0 < CalBound k (o curid ll ++ ll))%nat).
{
intros k Hk.
apply Hbound.
rewrite in_app.
simpl.
rewrite in_app in Hk.
simpl in Hk.
tauto.
}
exploit MCS_CalLock_progress; eauto.
{ intros.
exploit Horacle_domain1; eauto; intros; tauto. }
intros Hprogress.
destruct Hprogress as (q10 & q1 & q11 & tq10 & tq1 & tq11 & H0a & H0b & H0c & H0d & H0e & H0f).
assert (Hnslow´ : ZSet.mem curid slow´ = false).
{
assert (∀ i0 e, In (TEVENT i0 e) (o curid ll) → i0 ≠ curid) as Hdomain.
{
intros.
unfold valid_multi_oracle_domain in Horacle_domain1.
apply (Horacle_domain1 _ _ e ll); auto.
}
rewrite (QS_CalLock_oracle_Mem (o curid ll) _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal Hdomain HQS_Cal).
exact Hnslow.
}
assert (HCal´´:
QS_CalLock (TEVENT curid (TTICKET (GET_BUSY true)) :: o curid ll ++ ll)
= Some (self_c´, rel_c´, b´, (z::q1´)++ curid :: q2´, slow´, tq1 ++ n :: tq11)).
{
Local Transparent QS_CalLock.
simpl.
rewrite HQS_Cal.
simpl.
assert (tq´ ≠ nil) by (subst; destruct tq1; simpl; congruence).
destruct tq´; [congruence|].
rewrite zeq_false by auto.
rewrite Hnslow´.
subst.
repeat eexists; repeat f_equal; congruence.
}
assert (¬In curid q1).
{
assert (Hnodup : NoDup (q1 ++ curid :: q11)).
{ replace (q1 ++ curid :: q11)
with ((z :: q1´) ++ curid :: q2´)
by congruence.
apply QS_CalLock_NoDup in HCal´´.
assumption.
}
rewrite NoDup_app in Hnodup.
destruct Hnodup as [_ [_ Hnodup]].
specialize Hnodup with curid.
simpl in Hnodup.
intuition.
}
assert (q1 = (z::q1´)) as Hq1.
{
symmetry.
apply (prepend_injectivity _ (z::q1´) curid q2´ q1 q11).
assumption.
+ simpl. intuition.
+ assumption.
}
Transparent QS_CalWaitGet.
simpl.
eapply IHwait_time; eauto.
× congruence.
×
apply lt_le_trans with (decrease_number self_c rel_c b curid lq slow ltq ll) ; [| omega].
apply lt_le_trans with (decrease_number self_c´ rel_c´ b´ curid q1 slow´ tq1 (o curid ll ++ ll)) ; [|assumption].
{
rewrite Hq1.
unfold decrease_number.
simpl.
assert ( CalBound z (TEVENT curid (TTICKET (GET_BUSY true)) :: o curid ll ++ ll)
< CalBound z (o curid ll ++ ll))%nat.
{
apply CalBound_decreasing.
auto.
apply Hbound.
replace lq with (q10 ++ (z :: q1´)) by congruence.
rewrite <- app_assoc.
rewrite in_app.
simpl.
auto.
}
destruct b´; omega.
}
Qed.
Lemma QS_CalLock_relate_mcs_log_always_exists:
∀ l self_c rel_c b q tq
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, tq)),
∃ l´, relate_mcs_log l = Some (l´, tq).
Proof.
induction l; simpl; intros.
- inv Hcal. refine_split´; trivial.
- simpl.
destruct (QS_CalLock l) as [ [[[[[self_c0 rel_c0] b0] q0] slow0] tq0 ] |];
destruct a as [i e];
try congruence.
destruct e as [e | e ]; [destruct e eqn:? | ]; try congruence;
repeat match goal with
| [ HCal´ : context [match QS_CalLock ?lis with
| Some _ ⇒ _ | None ⇒ _ end] |- _]
⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
| [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
| [ HCal´ : context[ZMap.get ?X ?Y] |- _] ⇒ destruct (ZMap.get X Y)
| [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
end; try congruence;
specialize (IHl _ _ _ _ _ eq_refl); destruct IHl as [? IH];
rewrite IH;
simpl in *; eexists; f_equal; f_equal; congruence.
Qed.
Lemma wait_lock_extend_other_threads : ∀ i lo ll self_c rel_c b q slow tq hl,
QS_CalLock ll = Some (self_c, rel_c, b, q, slow, tq) →
relate_mcs_log ll = Some (hl, tq) →
¬ In i q →
valid_qs_oracle lo →
valid_multi_oracle_domain lo →
(∃ hl´ self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock (lo i ll ++ ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)
∧ ¬ In i q´
∧ relate_mcs_log (lo i ll ++ ll) = Some (hl´, tq´)).
Proof.
intros until hl.
intros HCal Hrel Hnin H_valid_oracle H_valid_domain.
destruct (H_valid_oracle i _ _ _ _ _ _ _ HCal)
as [self_c1 [rel_c1 [b1 [q1 [slow1 [tq1 [HCal1 _]]]]]]].
destruct (QS_CalLock_relate_mcs_log_always_exists _ _ _ _ _ _ HCal1) as [hl1 Hrel1].
repeat eexists.
+ exact HCal1.
+ assert (Hdomain : (∀ k e, In (TEVENT k e) (lo i ll) → k ≠ i))
by (intros k e; apply H_valid_domain).
apply (QS_CalLock_oracle_not_In _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal Hdomain Hnin HCal1).
+ exact Hrel1.
Qed.
Lemma decrease_number_remove_slow:
∀ self_c rel_c b c q slow tq l l´,
( (decrease_number self_c rel_c b c q (ZSet.remove c slow) tq l´)
≤ (decrease_number self_c rel_c b c q slow tq l) + WaitConstant)%nat.
Proof.
intros.
rewrite plus_comm.
unfold decrease_number.
assert (CalBound (hd c q) l´ < WaitConstant)%nat.
{
apply le_lt_trans with fairness.
apply CalBound_upper_bound.
apply WaitConstant_fairness.
}
destruct b;
(apply plus_le_compat;
[ omega
| apply le_plus_trans_l;
apply mult_le_compat_r;
apply plus_le_compat_r;
repeat apply plus_le_compat_l;
apply CalSumWaitSlow_remove_mono]).
Qed.
Section Release_shared_mem.
Lemma QS_CalLock_relate_mcs_log:
∀ l l´ self_c self_c´ rel_c b b´ q slow tq tq0 h
(Hcal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hcal´: H_CalLock l´ = Some (self_c´, b´, h))
(Hre: HMCSLockOpGenDef.relate_mcs_log l = Some (l´, tq0)),
match b with
| LEMPTY ⇒ self_c = self_c´
| _ ⇒ self_c = (S 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 (HMCSLockOpGenDef.relate_mcs_log l) eqn: Hre´; contra_inv.
destruct (QS_CalLock l) eqn: Hcal0´; contra_inv.
destruct p. destruct p0. repeat destruct p.
exploit QS_CalLock_relate_mcs_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.
destruct is_null; contra_inv.
inv Hcal. inv Hre.
Transparent H_CalLock.
simpl in Hcal´.
subdestruct; simpl; inv Hcal´.
exploit IHl; eauto.
+ destruct l1; contra_inv.
destruct (zeq i z); contra_inv.
× destruct h0; contra_inv.
{
destruct e; contra_inv.
destruct e; contra_inv.
- case_eq (ZSet.mem z t); subst.
+ intros.
rewrite H in Hcal; inv Hcal.
inv Hre.
exploit IHl; eauto.
+ intros.
rewrite H in Hcal; inv Hcal.
- case_eq busy; intro; subst; try inv Hcal.
inv Hre.
simpl in Hcal´.
subdestruct; contra_inv.
subst.
inv Hcal´.
tauto.
}
{
destruct e; contra_inv.
destruct e; contra_inv.
inv Hre.
case_eq (ZSet.mem z t); subst.
- intros.
rewrite H in Hcal; inv Hcal.
exploit IHl; eauto.
- intros.
rewrite H in Hcal; inv Hcal.
}
{ subst.
destruct e; contra_inv.
- destruct e; contra_inv.
+ destruct success; subst.
× destruct l2.
{ inv Hcal.
inv Hre.
simpl in Hcal´; subdestruct; contra_inv; subst.
inv Hcal´; tauto. }
{ inv Hcal. }
× inv Hre.
destruct n0; try inv Hcal.
exploit IHl; eauto.
+ inv Hre.
destruct n0; try inv Hcal.
exploit IHl; eauto.
+ inv Hre.
case_eq (ZSet.mem z t); intros.
× rewrite H in Hcal; inv Hcal.
exploit IHl; eauto.
× rewrite H in Hcal; inv Hcal.
+ inv Hre.
simpl in Hcal´; subdestruct; subst.
inv Hcal´.
inv Hcal; simpl; tauto.
- destruct n; simpl; auto; try inv Hcal.
inv Hre.
simpl in Hcal´.
subdestruct; contra_inv; subst.
inv Hcal´.
eapply IHl with (self_c0 := S self_c) (self_c´ := S self_c´) in Hdestruct; eauto; simpl.
simpl in Hdestruct.
destruct Hdestruct.
inv H.
eauto.
}
× destruct e; contra_inv.
destruct e; contra_inv.
{
destruct is_null; contra_inv.
destruct (in_dec zeq i (z::l2)); contra_inv.
inv Hcal. inv Hre.
exploit IHl; eauto.
}
{
case_eq ( ZSet.mem i t); intros.
- rewrite H in Hcal; inv Hcal.
inv Hre.
exploit IHl; eauto.
- rewrite H in Hcal; inv Hcal.
}
{
destruct busy.
- destruct (ZSet.mem i t); try inv Hcal.
inv Hre.
exploit IHl; eauto.
- inv Hcal.
}
Qed.
Lemma QS_CalLock_TSHARED_exists:
∀ l l´ self_c self_c´ rel_c b b´ q slow tq e c h tq0
(HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
(Hcal´: H_CalLock (TEVENT c (TSHARED e) :: l´) = Some (self_c´, b´, h))
(Hre: relate_mcs_log l = Some (l´, tq0)),
∃ x,
QS_CalLock (TEVENT c (TSHARED e) :: l) = Some x.
Proof.
Transparent QS_CalLock H_CalLock.
simpl; intros. rewrite HCal. subst.
subdestruct; inv Hcal´.
exploit QS_CalLock_relate_mcs_log; eauto.
intros (Hs & Hb & Hz).
destruct b; inv Hb.
exploit QS_CalLock_q_length_same; eauto.
intros Hlen.
destruct q; inv Hz.
destruct tq; inv Hlen.
rewrite zeq_true.
eauto.
Qed.
End Release_shared_mem.
End WITHMEM.
End Refinement.