Library mcertikos.mcslock.StarvationFreedomMCSLockPassLock
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}.
Lemma relate_mcs_log_inv : ∀ e ll hl tq,
relate_mcs_log (e::ll) = Some (hl, tq) →
∃ hl´ tq´,
relate_mcs_log ll = Some (hl´, tq´).
Proof.
intros until tq.
simpl.
destruct e as [i e];
destruct e as [e | e];
destruct e;
destruct (relate_mcs_log ll) as [[? ?] | ];
simpl; try congruence;
inversion 1; subst; eauto.
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.
Transparent QS_CalLock relate_mcs_log.
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 pass_lock_extend_other_threads_onestep : ∀ j e ll self_c rel_c i q slow tq hl self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: q, slow, tq) →
relate_mcs_log ll = Some (hl, tq) →
¬ In i q →
QS_CalLock (TEVENT j e :: ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
j ≠ i →
(∃ q0,
self_c´ = self_c
∧ rel_c´ = rel_c
∧ b´ = LHOLD
∧ q´ = i :: q0
∧ ¬ In i q0
∧ relate_mcs_log ((TEVENT j e) :: ll) = Some (hl, tq´)).
Proof.
Transparent QS_CalLock.
intros until tq´.
intros HCal Hrelate HnotIn HCal´ Hj.
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 ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
end;
try congruence.
+
simpl in HCal´.
∃ (q ++ j :: nil).
repeat split; try congruence.
- rewrite in_app.
simpl in ×.
tauto.
- simpl. rewrite Hrelate.
simpl; congruence.
+
∃ q.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
+
∃ q.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
Qed.
Lemma pass_lock_extend_other_threads´ : ∀ ll0 i self_c0 rel_c0 q0 slow0 tq0 hl0 ll1 self_c rel_c b q slow tq,
QS_CalLock ll0 = Some (self_c0, rel_c0, LHOLD, i :: q0, slow0, tq0) →
QS_CalLock (ll1 ++ ll0) = Some (self_c, rel_c, b, q, slow, tq) →
relate_mcs_log ll0 = Some (hl0, tq0) →
¬ In i q0 →
(∀ k e, In (TEVENT k e) ll1 → k≠i) →
(∃ qtail´ tq´,
self_c = self_c0
∧ rel_c = rel_c0
∧ b = LHOLD
∧ q = i :: qtail´
∧ ¬ In i qtail´
∧ relate_mcs_log (ll1 ++ ll0) = Some (hl0, tq´)).
Proof.
Opaque QS_CalLock relate_mcs_log.
induction ll1 as [|e ll1].
× simpl.
intros.
∃ q0. ∃ tq0.
repeat split; try congruence.
× intros until tq.
intros HCal0 HCal Hrelate0 HnotIn Hdomain.
simpl in ×.
destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal) as [self_c´ [rel_c´ [b´ [q´ [slow´ [tq´ HCal´]]]]]].
destruct (IHll1 self_c´ rel_c´ b´ q´ slow´ tq´ HCal0 HCal´ Hrelate0 HnotIn) as [qtail1 [rtq1 [Hself_c´ [Hrel_c´ [Hb´ [Hq´ [HnotIn´ Hrelate1]]]]]]].
{ intros k1 e1.
specialize Hdomain with k1 e1.
auto. }
rewrite Hb´ in HCal´.
rewrite Hq´ in HCal´.
destruct e as [k e].
rewrite (QS_CalLock_relate_mcs_log_eq _ _ _ _ _ _ _ rtq1 tq´ Hrelate1 HCal´) in Hrelate1.
assert (k ≠ i) as Hik.
{ specialize Hdomain with k e.
auto. }
destruct (pass_lock_extend_other_threads_onestep k e _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal´ Hrelate1 HnotIn´ HCal Hik)
as [q0´´ [Hself_c´´ [Hrel_c´´ [Hb´´ [Hq´´ [HnotIn´´ Hrelate´´]]]]]].
∃ q0´´. ∃ tq.
repeat split; try congruence.
Qed.
Lemma pass_lock_extend_other_threads : ∀ lo ll self_c rel_c i q slow tq hl,
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: q, slow, tq) →
relate_mcs_log ll = Some (hl, tq) →
¬ In i q →
valid_qs_oracle lo →
valid_multi_oracle_domain lo →
(∃ q´ slow´ tq´,
QS_CalLock (lo i ll ++ ll) = Some (self_c, rel_c, LHOLD, i :: q´, slow´, tq´)
∧ ¬ In i q´
∧ relate_mcs_log (lo i ll ++ ll) = Some (hl, tq´)).
Proof.
intros until hl.
intros HCal Hrelate HnotIn Hvalid_qs Hvalid_domain.
destruct (Hvalid_qs i ll self_c rel_c LHOLD (i::q) slow tq HCal) as [self_c1 [rel_c1 [b1 [q1 [slow1 [tq1 [HCal1 _]]]]]]].
pose (ll1 := lo i ll).
fold ll1 in HCal1.
assert (∀ k e, In (TEVENT k e) ll1 → k≠i).
{
unfold valid_multi_oracle_domain in Hvalid_domain.
intros k e.
unfold ll1.
apply Hvalid_domain.
}
destruct (pass_lock_extend_other_threads´ ll i self_c rel_c q slow tq hl ll1 self_c1 rel_c1 b1 q1 slow1 tq1)
as [qtail [rtq1 [Hself_c1 [Hrel_c1 [Hb1 [Hq1 [HnotIn1 Hrelate1]]]]]]]; auto.
subst.
∃ qtail. ∃ slow1. ∃ tq1.
split.
+ auto.
+ rewrite <- (QS_CalLock_relate_mcs_log_eq _ _ _ _ _ _ _ rtq1 tq1 Hrelate1 HCal1).
auto.
Qed.
Lemma pass_lock_wait_slow_other_threads_onestep_slow : ∀ k e ll self_c rel_c i j q slow tq rtq hl self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: j :: q, slow, tq) →
ZSet.mem j slow = true →
relate_mcs_log ll = Some (hl, rtq) →
QS_CalLock (TEVENT k e :: ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
i ≠ j →
k ≠ i →
(O < (CalBound j (TEVENT k e :: ll)))%nat →
(∃ q0, ∃ rtq´,
self_c´ = self_c
∧ rel_c´ = rel_c
∧ b´ = LHOLD
∧ q´ = i :: j :: q0
∧ relate_mcs_log (TEVENT k e :: ll) = Some (hl, rtq´)
∧ ((ZSet.mem j slow´ = true ∧ ((CalBound j (TEVENT k e :: ll)) < (CalBound j ll))%nat)
∨ ZSet.mem j slow´ = false)).
Proof.
Transparent QS_CalLock relate_mcs_log.
intros until tq´.
intros HCal Hslow Hrelate HCal´ Hij Hk Hbound.
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 ?X with | nil ⇒ _ | (_ :: _) ⇒ _ 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[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
end;
destruct (zeq j k);
try congruence.
+
subst.
contradict n2. simpl; auto.
+
simpl in HCal´.
∃ (q++k::nil). ∃ (rtq ++ n :: nil).
repeat split; try congruence.
- simpl. rewrite Hrelate. simpl; congruence.
- left;split.
× replace slow´ with (ZSet.add k slow) by congruence.
rewrite ZSet_gso by auto.
auto.
× eauto using CalBound_inv, CalBound_decreasing.
+
∃ q. ∃ rtq.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
- right.
subst.
replace slow´ with (ZSet.remove k slow) by congruence.
apply ZSet_mem_remove.
+
∃ q. ∃ rtq.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
- left; split.
× replace slow´ with (ZSet.remove k slow) by congruence.
rewrite ZSet_remove_gso by auto.
auto.
× eauto using CalBound_inv, CalBound_decreasing.
+
∃ q. ∃ rtq.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
- left; split.
× congruence.
× eauto using CalBound_inv, CalBound_decreasing.
Qed.
Lemma pass_lock_wait_slow_other_threads_onestep_nonslow : ∀ k e ll self_c rel_c i j q slow tq rtq hl self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: j :: q, slow, tq) →
ZSet.mem j slow = false →
relate_mcs_log ll = Some (hl, rtq) →
QS_CalLock (TEVENT k e :: ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
i ≠ j →
k ≠ i →
(∃ q0 rtq´,
self_c´ = self_c
∧ rel_c´ = rel_c
∧ b´ = LHOLD
∧ q´ = i :: j :: q0
∧ relate_mcs_log (TEVENT k e :: ll) = Some (hl, rtq´)
∧ ZSet.mem j slow´ = false).
Proof.
Transparent QS_CalLock.
intros until tq´.
intros HCal Hslow Hrelate HCal´ Hij Hk .
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 ?X with | nil ⇒ _ | (_ :: _) ⇒ _ 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[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
end;
destruct (zeq j k);
try congruence.
+
subst.
contradict n2. simpl; auto.
+
simpl in HCal´.
∃ (q++k::nil). ∃ (rtq ++ n :: nil).
repeat split; try congruence.
- simpl. rewrite Hrelate. simpl; congruence.
- replace slow´ with (ZSet.add k slow) by congruence.
rewrite ZSet_gso by auto.
auto.
+
∃ q. ∃ rtq.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
- replace slow´ with (ZSet.remove k slow) by congruence.
rewrite ZSet_remove_preserves_not_in; auto.
+
∃ q. ∃ rtq.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
+
∃ q. ∃ rtq.
repeat split; try congruence.
- simpl. rewrite Hrelate. congruence.
Qed.
Lemma CalBound_inv : ∀ i e l, (0 < (CalBound i (e::l)))%nat → (0 < (CalBound i l))%nat.
Proof.
intros i e l.
simpl.
destruct e; destruct (CalBound i l); omega.
Qed.
Lemma pass_lock_wait_slow_other_threads_nonslow´ : ∀ ll0 i j self_c0 rel_c0 q0 slow0 tq0 rtq0 hl0 ll1 self_c rel_c b q slow tq,
i ≠ j →
QS_CalLock ll0 = Some (self_c0, rel_c0, LHOLD, i :: j :: q0, slow0, tq0) →
QS_CalLock (ll1 ++ ll0) = Some (self_c, rel_c, b, q, slow, tq) →
ZSet.mem j slow0 = false →
relate_mcs_log ll0 = Some (hl0, rtq0) →
(∀ k e, In (TEVENT k e) ll1 → k≠i) →
∃ qtail rtq,
self_c = self_c0
∧ rel_c = rel_c0
∧ b = LHOLD
∧ q = i :: j :: qtail
∧ relate_mcs_log (ll1 ++ ll0) = Some (hl0, rtq)
∧ ZSet.mem j slow = false.
Proof.
Opaque QS_CalLock CalBound relate_mcs_log.
induction ll1 as [|e ll1].
× simpl.
intros.
∃ q0. ∃ rtq0.
repeat split; try congruence.
× intros until tq.
intros Hij HCal0 HCal Hslow Hrelate0 Hdomain.
simpl in ×.
destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal) as [self_c´ [rel_c´ [b´ [q´ [slow´ [tq´ HCal´]]]]]].
destruct (IHll1 self_c´ rel_c´ b´ q´ slow´ tq´ Hij HCal0 HCal´ Hslow Hrelate0) as [qtail1 [rtq1 [Hself_c´ [Hrel_c´ [Hb´ [Hq´ [Hrelate1 IH]]]]]]].
{ intros k1 e1.
specialize Hdomain with k1 e1.
auto. }
rewrite Hb´ in HCal´.
rewrite Hq´ in HCal´.
destruct e as [k e].
destruct (pass_lock_wait_slow_other_threads_onestep_nonslow k e _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal´ IH Hrelate1 HCal Hij)
as [q0´´ [rtq´´ [Hself_c´´ [Hrel_c´´ [Hb´´ [Hq´´ [Hrelate´´ H]]]]]]].
{ specialize Hdomain with k e.
auto. }
∃ q0´´. ∃ rtq´´.
repeat split; try congruence.
Qed.
Lemma pass_lock_wait_slow_other_threads_slow´ : ∀ ll0 i j self_c0 rel_c0 q0 slow0 tq0 rtq0 hl0 ll1 self_c rel_c b q slow tq,
i ≠ j →
QS_CalLock ll0 = Some (self_c0, rel_c0, LHOLD, i :: j :: q0, slow0, tq0) →
QS_CalLock (ll1 ++ ll0) = Some (self_c, rel_c, b, q, slow, tq) →
lt O (CalBound j (ll1 ++ ll0)) →
ZSet.mem j slow0 = true →
relate_mcs_log ll0 = Some (hl0, rtq0) →
(∀ k e, In (TEVENT k e) ll1 → k≠i) →
(∃ qtail rtq,
self_c = self_c0
∧ rel_c = rel_c0
∧ b = LHOLD
∧ q = i :: j :: qtail
∧ relate_mcs_log (ll1 ++ ll0) = Some (hl0, rtq)
∧ (( ZSet.mem j slow = true ∧ ((CalBound j (ll1 ++ ll0)) ≤ (CalBound j ll0))%nat)
∨ ZSet.mem j slow = false)).
Proof.
Opaque QS_CalLock CalBound relate_log.
induction ll1 as [|e ll1].
× simpl.
intros.
∃ q0. ∃ rtq0.
repeat split; try congruence.
replace slow with slow0 by congruence.
auto.
× intros until tq.
intros Hij HCal0 HCal Hbound Hslow Hrelate0 Hdomain.
simpl in ×.
assert (Hbound1 : (0 < CalBound j (ll1 ++ ll0))%nat)
by (apply CalBound_inv with e; auto).
destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal) as [self_c´ [rel_c´ [b´ [q´ [slow´ [tq´ HCal´]]]]]].
destruct (IHll1 self_c´ rel_c´ b´ q´ slow´ tq´ Hij HCal0 HCal´ Hbound1 Hslow Hrelate0) as [qtail1 [rtq1 [Hself_c´ [Hrel_c´ [Hb´ [Hq´ [Hrelate1 IH]]]]]]].
{ intros k1 e1.
specialize Hdomain with k1 e1.
auto. }
destruct IH as [[Hslow´ IH] | IH].
+ rewrite Hb´ in HCal´.
rewrite Hq´ in HCal´.
destruct e as [k e].
destruct (pass_lock_wait_slow_other_threads_onestep_slow k e _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal´ Hslow´ Hrelate1 HCal Hij)
as [q0´´ [rtq´´ [Hself_c´´ [Hrel_c´´ [Hb´´ [Hq´´ [ Hrelate´´ H]]]]]]].
{ specialize Hdomain with k e.
auto. }
{ assumption. }
destruct H as [[Hslow´´ Hdecrease] | Hnonslow´´].
- ∃ q0´´. ∃ rtq´´.
repeat split; try congruence.
left; split; auto; eauto with arith.
- ∃ q0´´. ∃ rtq´´.
repeat split; try congruence.
auto.
+ rewrite Hb´ in HCal´.
rewrite Hq´ in HCal´.
destruct e as [k e].
destruct (pass_lock_wait_slow_other_threads_onestep_nonslow k e _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal´ IH Hrelate1 HCal Hij)
as [q0´´ [rtq´´ [Hself_c´´ [Hrel_c´´ [Hb´´ [Hq´´ [ Hrelate´´ H]]]]]]].
{ specialize Hdomain with k e.
auto. }
∃ q0´´. ∃ rtq´´.
repeat split; try congruence.
right; auto.
Qed.
Lemma pass_lock_wait_nonslow_other_threads : ∀ lo ll self_c rel_c i j q slow tq rtq hl,
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: j :: q, slow, tq) →
relate_mcs_log ll = Some (hl, rtq) →
ZSet.mem j slow = false →
i≠j →
valid_qs_oracle lo →
valid_multi_oracle_domain lo →
(∃ q´ slow´ tq´ rtq´,
QS_CalLock (lo i ll ++ ll) = Some (self_c, rel_c, LHOLD, i :: j :: q´, slow´, tq´)
∧ relate_mcs_log (lo i ll ++ ll) = Some (hl, rtq´)
∧ ZSet.mem j slow´ = false).
Proof.
intros until hl.
intros HCal Hrelate Hslow Hij Hvalid_qs Hvalid_domain.
destruct (Hvalid_qs i ll self_c rel_c LHOLD (i::j::q) slow tq HCal)
as [self_c1 [rel_c1 [b1 [q1 [slow1 [tq1 [HCal1 Hfair]]]]]]].
pose (ll1 := lo i ll).
fold ll1 in HCal1.
assert (lt O (CalBound j (ll1 ++ ll))).
{
unfold valid_qs_oracle in Hvalid_qs.
unfold ll1; apply Hfair.
simpl; auto.
}
assert (∀ k e, In (TEVENT k e) ll1 → k≠i).
{
unfold valid_multi_oracle_domain in Hvalid_domain.
intros k e.
unfold ll1.
apply Hvalid_domain.
}
destruct (pass_lock_wait_slow_other_threads_nonslow´ ll i j self_c rel_c q slow tq rtq hl ll1 self_c1 rel_c1 b1 q1 slow1 tq1)
as [qtail [rtq1 [Hself_c1 [Hrel_c1 [Hb1 [Hq1 [Hrelate1 Hdecrease]]]]]]];
auto.
∃ qtail. ∃ slow1. ∃ tq1. ∃ rtq1.
repeat split.
+ rewrite Hself_c1, Hrel_c1, Hq1, Hb1 in HCal1; apply HCal1.
+ apply Hrelate1.
+ auto.
Qed.
Lemma pass_lock_wait_slow_other_threads : ∀ lo ll self_c rel_c i j q slow tq rtq hl,
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: j :: q, slow, tq) →
relate_mcs_log ll = Some (hl, rtq) →
i ≠ j →
valid_qs_oracle lo →
valid_multi_oracle_domain lo →
(∃ q´ slow´ tq´ rtq´,
QS_CalLock (lo i ll ++ ll) = Some (self_c, rel_c, LHOLD, i :: j :: q´, slow´, tq´)
∧ relate_mcs_log (lo i ll ++ ll) = Some (hl, rtq´)
∧ (ZSet.mem j slow´ = true ∧ ((CalBound j (lo i ll ++ ll)) ≤ (CalBound j ll))%nat
∨ ZSet.mem j slow´ = false)).
Proof.
intros until hl.
intros HCal Hrelate Hij Hvalid_qs Hvalid_domain.
destruct (Hvalid_qs i ll self_c rel_c LHOLD (i::j::q) slow tq HCal)
as [self_c1 [rel_c1 [b1 [q1 [slow1 [tq1 [HCal1 Hfair]]]]]]].
pose (ll1 := lo i ll).
fold ll1 in HCal1.
assert (lt O (CalBound j (ll1 ++ ll))).
{
unfold valid_qs_oracle in Hvalid_qs.
unfold ll1; apply Hfair.
simpl; auto.
}
assert (∀ k e, In (TEVENT k e) ll1 → k≠i).
{
unfold valid_multi_oracle_domain in Hvalid_domain.
intros k e.
unfold ll1.
apply Hvalid_domain.
}
destruct (ZSet.mem j slow) eqn:Hslow.
× destruct (pass_lock_wait_slow_other_threads_slow´ ll i j self_c rel_c q slow tq rtq hl ll1 self_c1 rel_c1 b1 q1 slow1 tq1)
as [qtail [rtq1 [Hself_c1 [Hrel_c1 [Hb1 [Hq1 [Hrelate1 Hdecrease]]]]]]];
auto.
∃ qtail. ∃ slow1. ∃ tq1. ∃ rtq1.
repeat split.
+ rewrite Hself_c1, Hrel_c1, Hq1, Hb1 in HCal1; apply HCal1.
+ apply Hrelate1.
+ fold ll1.
destruct Hdecrease as [[? ?] | ?]; auto.
× destruct (pass_lock_wait_slow_other_threads_nonslow´ ll i j self_c rel_c q slow tq rtq hl ll1 self_c1 rel_c1 b1 q1 slow1 tq1)
as [qtail [rtq1 [Hself_c1 [Hrel_c1 [Hb1 [Hq1 [Hrelate1 Hdecrease]]]]]]];
auto.
∃ qtail. ∃ slow1. ∃ tq1. ∃ rtq1.
repeat split.
+ rewrite Hself_c1, Hrel_c1, Hq1, Hb1 in HCal1; apply HCal1.
+ apply Hrelate1.
+ right.
auto.
Qed.
Definition pass_lock_final1 l cpu o :=
let l1 := (TEVENT cpu (TTICKET GET_NEXT)) :: l in
(o cpu l1) ++ l1.
Definition pass_lock_final l cpu o :=
let l1 := (TEVENT cpu (TTICKET GET_NEXT)) :: l in
(TEVENT cpu (TTICKET SET_BUSY)) :: pass_lock_final1 l cpu o.
Lemma CalWaitRel_exist´ : ∀ n self_c rel_c i j q slow tq rtq ll hl lo,
valid_qs_oracle lo →
valid_multi_oracle_domain lo →
i ≠ j →
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: j :: q, slow, tq) →
relate_mcs_log ll = Some (hl, rtq) →
(CalBound j ll < n)%nat →
(n < rel_c)%nat →
∃ l´ rtq´,
QS_CalWaitRel n i j ll lo = Some l´
∧ (∃ self_c´ rel_c´ q0´ q´ slow´ tq´,
QS_CalLock (pass_lock_final1 l´ i lo) = Some (self_c´, rel_c´, q0´::q´, slow´, tq´))
∧ relate_mcs_log (pass_lock_final l´ i lo) = Some (TEVENT i (TTICKET REL_LOCK) :: hl, rtq´).
Proof.
induction n; [intros; omega|].
intros until lo.
intros Hvalid_qs Hvalid_domain Hij HCal Hrelate Hbound Hbound_self.
Transparent QS_CalWaitRel.
simpl.
destruct (pass_lock_wait_slow_other_threads lo ll self_c rel_c i j q slow tq rtq hl)
as [q1 [slow1 [tq1 [rtq1 [HCal1 [Hrelate1 Hpost]]]]]];
auto.
rewrite HCal1.
pose (ll1 := lo i ll ++ ll).
fold ll1.
fold ll1 in Hrelate1, HCal1, Hpost.
assert (Hbound1 : (0 < CalBound j ll1)%nat).
{
unfold valid_qs_oracle in Hvalid_qs.
destruct (Hvalid_qs i ll _ _ _ _ _ _ HCal) as [? [? [? [? [? [? [? Hfair]]]]]]].
unfold ll1.
apply (Hfair j).
simpl; auto.
}
clearbody ll1.
clear q slow tq rtq HCal Hrelate.
pose (ll2 := (TEVENT i (TTICKET GET_NEXT)) :: ll1).
fold ll2.
assert (HCal2 : QS_CalLock ll2 = Some (self_c, pred rel_c, LHOLD, i :: j :: q1, slow1, tq1)).
{
Transparent QS_CalLock.
unfold ll2.
simpl.
rewrite HCal1.
destruct tq1.
+ apply QS_CalLock_q_length_same in HCal1.
simpl in HCal1.
congruence.
+ rewrite zeq_true.
destruct rel_c as [|rel_c´].
- omega.
- reflexivity.
}
assert (Hrelate2 : relate_mcs_log ll2 = Some (hl, rtq1)).
{
unfold ll2.
Transparent relate_mcs_log.
simpl.
rewrite Hrelate1.
reflexivity.
}
destruct Hpost as [[Hslow Hdecrease] | Hslow].
+ rewrite Hslow.
assert (Hbound2 : (CalBound j ll2 < n)%nat).
{
unfold ll2.
Transparent CalBound.
simpl.
destruct (CalBound j ll1) as [|m] eqn:Hm.
omega.
rewrite zeq_false by auto. omega.
}
destruct rel_c as [|rel_c´] ; [omega|].
apply IHn with (self_c := self_c) (rel_c := rel_c´) (q := q1) (slow:=slow1) (tq:=tq1) (rtq:=rtq1); auto; omega.
+ rewrite Hslow.
destruct (pass_lock_wait_nonslow_other_threads lo ll2 self_c (pred rel_c) i j q1 slow1 tq1 rtq1 hl)
as [q3 [slow3 [tq3 [rtq3 [HCal3 [Hrelate3 Hslow3]]]]]];
auto.
destruct rel_c as [|[|rel_c´]]; [omega | omega | ].
∃ ll1.
unfold pass_lock_final.
unfold pass_lock_final1.
fold ll2.
pose (ll3 := lo i ll2 ++ ll2).
fold ll3.
fold ll3 in HCal3, Hrelate3.
clearbody ll2 ll3.
clear q1 slow1 tq1 HCal1 Hbound1 Hrelate1 Hslow HCal2 Hrelate2.
replace rtq3 with tq3 in Hrelate3
by (symmetry; eauto using (QS_CalLock_relate_mcs_log_eq ll3 hl)).
destruct tq3 as [|? tq3´] eqn:Htq3; [apply QS_CalLock_q_length_same in HCal3; simpl in HCal3; congruence | ].
∃ tq3´. split; [reflexivity|].
split; [repeat eexists; exact HCal3 | ].
simpl.
rewrite Hrelate3.
reflexivity.
Qed.
Lemma le_lt_S : ∀ n m, (n ≤ m)%nat → (n < S m)%nat.
Proof.
intros.
unfold lt.
auto with arith.
Qed.
Lemma CalWaitRel_exist : ∀ self_c rel_c i j q slow tq rtq ll hl lo,
valid_qs_oracle lo →
valid_multi_oracle_domain lo →
i ≠ j →
QS_CalLock ll = Some (self_c, rel_c, LHOLD, i :: j :: q, slow, tq) →
relate_mcs_log ll = Some (hl, rtq) →
(S fairness < rel_c)%nat →
∃ l´ rtq´,
QS_CalWaitRel (S fairness) i j ll lo = Some l´
∧ (∃ self_c´ rel_c´ q0´ q´ slow´ tq´,
QS_CalLock (pass_lock_final1 l´ i lo) = Some (self_c´, rel_c´, q0´::q´, slow´, tq´))
∧ relate_mcs_log (pass_lock_final l´ i lo) = Some (TEVENT i (TTICKET REL_LOCK) :: hl, rtq´).
Proof.
intros.
apply (CalWaitRel_exist´ (S fairness) self_c rel_c i j q slow tq rtq ll hl lo); auto.
apply le_lt_S; apply CalBound_upper_bound.
Qed.
End WITHMEM.
End Refinement.