Library mcertikos.mcslock.QMCSLockOpGenLemma
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 ListLemma2.
Require Import ZSet.
Require Import AbstractDataType.
Require Import CalMCSLock.
Require Import CalMCSLockLemmas.
Require Export QMCSLockOpGenDef.
Section QSMCSLAYERAUXLEMMA.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Transparent CalMCSLock.
Lemma tail_id_of_tail : ∀ q s i bi,
tail_id (q ++ (QT s i bi) :: nil) = i.
Proof.
induction q; auto; destruct a,q; simpl in *; auto.
Qed.
Lemma tail_soundness : ∀ l q,
Q_CalMCSLock l q → ∀ p la tq, CalMCSLock l = Some (MCSLOCK p la tq) → p = tail_id q.
Proof.
induction 1; simpl; try (destruct (CalMCSLock l) as [[? ? ?] |]; [ | now congruence]).
+ unfold init_MCSLock.
congruence.
+ congruence.
+ rewrite tail_id_of_tail.
congruence.
+ auto.
+ destruct (ZMap.get j lock_array).
replace (tail_id (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post))
with (tail_id (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)).
{ rewrite <- H0.
intros.
eapply IHQ_CalMCSLock.
replace tail with p by congruence.
reflexivity. }
clear H0.
induction pre.
- reflexivity.
- destruct a.
destruct pre; simpl in *; auto.
+ eapply IHQ_CalMCSLock.
+ eapply IHQ_CalMCSLock.
+ specialize (IHQ_CalMCSLock tail lock_array bounds eq_refl).
intros.
simpl in ×.
destruct (ZMap.get i lock_array).
destruct (ZMap.get z lock_array).
congruence.
+ auto.
+ intros.
destruct (zeq tail i); congruence.
+ intros; inv H0.
eapply IHQ_CalMCSLock; eauto.
Qed.
Lemma Q_CalMCSLock_not_NULL : ∀ l q i,
Q_CalMCSLock l q → In i (map qthread_tid q) → i≠NULL.
Proof.
induction 1; simpl; intros; try tauto; subst;
repeat rewrite map_app in *;
repeat rewrite in_app in *;
simpl in *;
intuition.
Qed.
Lemma tail_id_In : ∀ (q : Q_MCSLockState),
(tail_id q ≠ NULL) → In (tail_id q) (map qthread_tid q).
Proof.
induction q as [| qt q]; simpl; intros.
+ congruence.
+ destruct q as [|qt´ q]; simpl in ×.
- auto.
- remember (match q with
| nil ⇒ qthread_tid qt´
| _ :: _ ⇒ tail_id q
end) as blah.
tauto.
Qed.
Lemma Q_CalMCSLock_tail_id_nonnil : ∀ q,
tail_id q ≠ NULL →
∃ q0 s bi, q = q0 ++ (QT s (tail_id q) bi) :: nil.
Proof.
induction q as [|qt q]; simpl; intros.
+ congruence.
+ destruct qt.
destruct q as [|qt´ q]; simpl in ×.
- ∃ nil.
simpl; eauto.
- remember (match q with
| nil ⇒ qthread_tid qt´
| _ :: _ ⇒ tail_id q
end) as blah.
destruct IHq as [q2 [s´ [bi IH]]].
assumption.
rewrite IH.
∃ (QT s tid bound ::q2).
simpl.
eauto.
Qed.
Lemma Q_CalMCSLock_tail_id_nil´ : ∀ q,
(∀ i, In i (map qthread_tid q) → i≠NULL) → tail_id q = NULL → q = nil.
Proof.
induction q as [|qt q]; simpl; intros.
+ auto.
+ destruct q as [|qt´ q]; simpl in ×.
- destruct qt.
simpl in ×.
firstorder.
- remember (match q with
| nil ⇒ qthread_tid qt´
| _ :: _ ⇒ tail_id q
end) as blah.
assert (qt´ :: q = nil) by eauto; congruence.
Qed.
Lemma Q_CalMCSLock_tail_id_nil : ∀ l q,
Q_CalMCSLock l q → tail_id q = NULL → q = nil.
Proof.
intros.
apply Q_CalMCSLock_tail_id_nil´;
eauto using Q_CalMCSLock_not_NULL.
Qed.
Lemma Q_CalMCSLock_completeness : ∀ l q,
Q_CalMCSLock l q → ∃ mcs, CalMCSLock l = Some (mcs).
Proof.
induction 1; try destruct IHQ_CalMCSLock as [[tail0 la] IH]; simpl; try rewrite IH; eauto.
+ destruct (ZMap.get j la).
eauto.
+ destruct (ZMap.get i la).
destruct (ZMap.get z la).
eauto.
+ assert (Htail := tail_soundness _ _ H _ _ _ IH).
simpl in Htail.
destruct (zeq tail0 i); [eauto | congruence].
Qed.
Lemma Q_CalMCSLock_NoDup : ∀ l q,
Q_CalMCSLock l q → NoDup (map qthread_tid q).
Proof.
Hint Constructors NoDup.
induction 1; simpl; auto.
+ rewrite map_app; simpl.
apply NoDup_app_commute; simpl; auto.
+ replace ((map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post)))
with ((map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))).
× rewrite <- H0; auto.
× clear H0.
induction pre.
- reflexivity.
- simpl; rewrite IHpre; reflexivity.
+ inversion IHQ_CalMCSLock; subst; auto.
Qed.
Lemma Q_CalMCSLock_functional´´´ : ∀ A (pre pre´ : list A) b c post post´,
(¬In b pre) → (¬In b pre´) →
(¬In c pre) → (¬In c pre´) →
pre ++ b :: post = pre´ ++ c :: post´ →
b = c.
Proof.
induction pre.
+ destruct pre´; simpl; intros.
- congruence.
- contradict H0. left. congruence.
+ destruct pre´; simpl; intros.
- contradict H1. left. congruence.
- apply IHpre with (pre´:=pre´) (post:=post) (post´:=post´); intuition.
Qed.
Lemma Q_CalMCSLock_functional´´ : ∀ A (pre pre´ : list A) b c post post´,
(¬In b pre) → (¬In b pre´) →
pre ++ b :: post = pre´ ++ b :: post´ →
pre ++ c :: post = pre´ ++ c :: post´.
Proof.
induction pre; destruct pre´; simpl; intros.
- congruence.
- contradict H0. left. congruence.
- contradict H. left. congruence.
- replace a0 with a by congruence.
f_equal.
apply IHpre with (b:=b) (c:=c); try tauto; congruence.
Qed.
Lemma Q_CalMCSLock_functional´ : ∀ A (pre pre´ : list A) a a´ b c post post´,
(¬In b pre) → (¬In b pre´) → a≠b → a´≠b →
pre ++ a :: b :: post = pre´ ++ a´ :: b :: post´ →
pre ++ a :: c :: post = pre´ ++ a´ :: c :: post´.
Proof.
intros.
replace (pre ++ a :: c :: post) with ((pre ++ a :: nil) ++ c :: post)
by (rewrite <- app_assoc; reflexivity).
replace (pre´ ++ a´ :: c :: post´) with ((pre´ ++ a´ :: nil) ++ c :: post´)
by (rewrite <- app_assoc; reflexivity).
apply Q_CalMCSLock_functional´´ with (b:=b).
+ rewrite in_app. intuition.
inversion H5. intuition.
inversion H4.
+ rewrite in_app. intuition.
inversion H5. intuition.
inversion H4.
+ replace (pre ++ a :: b :: post) with ((pre ++ a :: nil) ++ b :: post) in H3
by (rewrite <- app_assoc; reflexivity).
replace (pre´ ++ a´ :: b :: post´) with ((pre´ ++ a´ :: nil) ++ b :: post´) in H3
by (rewrite <- app_assoc; reflexivity).
auto.
Qed.
Ltac use_NoDup´ i :=
repeat (simpl in *; subst; (match goal with
| [ H : _ ∧ _ |- _ ] ⇒ destruct H
| [ H : ∀ x, ¬ _ |- _] ⇒ specialize (H i)
| [ H : NoDup ( _ :: _) |- _] ⇒ inversion H; clear H
end)
|| rewrite map_app in ×
|| rewrite NoDup_app in ×
);
simpl in *; subst; auto; intuition.
Ltac use_NoDup :=
match goal with
| [|- (¬ In (QT _ ?i _) _)] ⇒ intros blah; apply (In_map _ _ qthread_tid) in blah; use_NoDup´ i
| [|- QT _ ?i _ ≠ QT _ _ _ ] ⇒ intros blah; inversion blah; use_NoDup´ i
| [|- ?j ≠ _ ] ⇒ intros blah; use_NoDup´ j
end.
Lemma Q_CalMCSLock_functional : ∀ l q q´,
Q_CalMCSLock l q → Q_CalMCSLock l q´ → q = q´.
Proof.
induction l; inversion 1; inversion 1; subst; auto;
try match goal with [ HA : Q_CalMCSLock ?l _, HB : Q_CalMCSLock ?l _ |- _ ]
⇒ pose (e:= IHl _ _ HA HB); try congruence
end.
clearbody e.
apply Q_CalMCSLock_NoDup in H5.
apply Q_CalMCSLock_NoDup in H10.
apply Q_CalMCSLock_NoDup in H.
apply Q_CalMCSLock_NoDup in H2.
assert (QT MCS_BEFORE_SET_NEXT i bi0 = QT MCS_BEFORE_SET_NEXT i bi)
as H_bi_bi0.
{
replace (pre0 ++ QT s0 j bj0 :: QT MCS_BEFORE_SET_NEXT i bi0 :: post0)
with ((pre0 ++ QT s0 j bj0 :: nil) ++ QT MCS_BEFORE_SET_NEXT i bi0 :: post0)
in × by (rewrite <- app_assoc; reflexivity) .
replace (pre ++ QT s j bj :: QT MCS_BEFORE_SET_NEXT i bi :: post)
with ((pre ++ QT s j bj :: nil) ++ QT MCS_BEFORE_SET_NEXT i bi :: post)
in × by (rewrite <- app_assoc; reflexivity) .
clear H. clear H5.
rewrite map_app in ×.
rewrite NoDup_app in ×.
apply Q_CalMCSLock_functional´´´
with (pre:=pre0++ QT s0 j bj0 :: nil)
(pre´:=pre ++ QT s j bj :: nil)
(post := post0)
(post´ := post);
try use_NoDup; auto.
}
rewrite H_bi_bi0 in e.
replace bi0 with bi in × by congruence.
apply Q_CalMCSLock_functional´ with (b:=(QT MCS_BEFORE_SET_NEXT i bi)); try use_NoDup; congruence.
Qed.
Fixpoint next_correct (la : ZMap.t (bool × Z)) (q : Q_MCSLockState) : Prop :=
match q with
| nil ⇒ True
| (QT _ i _) :: q´ ⇒
match q´ with
| nil ⇒ snd (ZMap.get i la) = NULL
| (QT s´ i´ _) :: _ ⇒
(snd (ZMap.get i la) = match s´ with | MCS_BEFORE_SET_NEXT ⇒ NULL | _ ⇒ i´ end)
∧ next_correct la q´
end
end.
Lemma next_correct_BEFORE_SET_NEXT : ∀ la q k b,
next_correct la q
→ ¬ In k (map qthread_tid q)
→ next_correct (ZMap.set k (true, NULL) la) (q ++ (QT MCS_BEFORE_SET_NEXT k b) :: nil).
Proof.
induction q.
+ simpl; intros.
rewrite ZMap.gss.
reflexivity.
+ simpl; intros.
destruct a as [s i b0].
assert (next_correct (ZMap.set k (true, NULL) la)
(q ++ (QT MCS_BEFORE_SET_NEXT k b) :: nil))
by (apply IHq; destruct q as [|[? ? ?] q]; simpl; tauto).
clear IHq.
destruct q as [|[? ? ?] q];
simpl; rewrite (@ZMap.gso _ i k) by auto;
try rewrite ZMap.gss;
tauto.
Qed.
Lemma next_correct_preserved_not_In : ∀ j la s q,
next_correct la q →
¬ In j (map qthread_tid q) →
next_correct (ZMap.set j s la) q.
Proof.
induction q as [| [s´ i´ bi´] q]; simpl.
+ auto.
+ intros.
assert (next_correct (ZMap.set j s la) q)
by (apply IHq; destruct q as [|[? ? ?] q]; simpl; tauto).
rewrite ZMap.gso by tauto.
destruct q as [|[? ? ?] q]; tauto.
Qed.
Lemma next_correct_SET_NEXT´ : ∀ la s j bj i bi post,
next_correct la ((QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)
→ NoDup (map qthread_tid ((QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))
→ next_correct (let (b, _) := ZMap.get j la in ZMap.set j (b, i) la)
((QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post).
Proof.
simpl; intros la s j bj i bi post NC HNoDup.
assert (i ≠ j)
by (inversion HNoDup; intros Heq; subst; simpl in *; auto).
split.
+ destruct (ZMap.get j la).
rewrite ZMap.gss.
reflexivity.
+ destruct post as [| [s´ i´ bi´] q].
- destruct NC.
destruct (ZMap.get j la).
rewrite ZMap.gso; auto.
- split.
× destruct NC as [? [? ?]].
destruct (ZMap.get j la).
rewrite ZMap.gso; auto.
× destruct (ZMap.get j la).
apply next_correct_preserved_not_In.
destruct NC as [? [? ?]]; auto.
inversion HNoDup.
simpl in *; tauto.
Qed.
Lemma next_correct_SET_NEXT : ∀ la pre s j bj i bi post,
next_correct la (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)
→ NoDup (map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))
→ next_correct (let (b, _) := ZMap.get j la in ZMap.set j (b, i) la)
(pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post).
Proof.
induction pre.
+ unfold app.
auto using next_correct_SET_NEXT´.
+ intros.
specialize IHpre with s j bj i bi post.
assert (j ≠ qthread_tid a) as Hj_not_a by use_NoDup.
destruct (ZMap.get j la) as [b z].
destruct a as [s´ i´ bi´].
assert (next_correct la (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)) as H_next_correct
by (simpl in H;
destruct ((pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)) as [|[? ? ?] q]; simpl; tauto).
assert (NoDup ((map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)))) as H_NoDup by (simpl in H0; inversion H0; auto).
assert (IH := IHpre H_next_correct H_NoDup).
clear IHpre H_next_correct H_NoDup.
simpl.
rewrite ZMap.gso by auto.
simpl in H.
destruct pre as [|[? ? ?] q]; simpl in *; intuition.
Qed.
Lemma next_correct_GET_BUSY_false : ∀ la i bi q,
next_correct la ((QT MCS_WAITING_BUSY i bi)::q) →
next_correct la ((QT MCS_INSIDE i bi)::q).
Proof.
simpl; intros.
destruct q; auto.
Qed.
Lemma next_correct_equiv_la : ∀ la la´ q,
(∀ i, snd (ZMap.get i la) = snd (ZMap.get i la´)) →
next_correct la q →
next_correct la´ q.
Proof.
intros la la´ q Hequiv.
induction q as [ |[? ? ? ] [|[? ? ?] ?]]; simpl; try rewrite Hequiv; tauto.
Qed.
Lemma Q_CalMCSLock_next_correct : ∀ l q,
Q_CalMCSLock l q → ∀ t la tq, CalMCSLock l = Some (MCSLOCK t la tq) →
next_correct la q.
Proof.
induction 1; simpl; intros;
try (destruct (CalMCSLock l)as [[tp0 la0 tq0] | ]; [ | now congruence]);
try match goal with [ H : Some (MCSLOCK _ _ _) = Some (MCSLOCK _ _ _) |-_] ⇒ inversion H; subst end.
+
auto.
+
rewrite ZMap.gss.
reflexivity.
+
auto using (IHQ_CalMCSLock tp0 la0 tq0 eq_refl), next_correct_BEFORE_SET_NEXT.
+
apply (IHQ_CalMCSLock t la tq eq_refl).
+
rewrite H0 in IHQ_CalMCSLock.
assert (NC := next_correct_SET_NEXT _ _ _ _ _ _ _ _ (IHQ_CalMCSLock tp0 la0 tq0 eq_refl)).
clear IHQ_CalMCSLock.
destruct (ZMap.get j la0).
replace tp0 with t in × by congruence.
replace la with (ZMap.set j (b, i) la0) in × by congruence.
apply NC.
{
rewrite H0 in H.
apply Q_CalMCSLock_NoDup in H.
auto.
}
+
simpl in ×.
exact (IHQ_CalMCSLock t la tq eq_refl).
+
apply (next_correct_GET_BUSY_false _ _ _ _ (IHQ_CalMCSLock t la tq eq_refl)).
+
simpl in ×.
destruct (ZMap.get i la0) as [b0 t0].
assert (∀ k, snd (ZMap.get k la0) =
snd (ZMap.get k (let (_, t´) := ZMap.get t0 la0 in (ZMap.set t0 (false, t´) la0))))
as Hla_equiv.
{
intros k.
case (zeq t0 k).
intros; subst.
destruct (ZMap.get k la0).
+ rewrite ZMap.gss.
reflexivity.
+ intros.
destruct (ZMap.get t0 la0).
rewrite ZMap.gso by auto.
reflexivity.
}
destruct (ZMap.get t0 la0).
replace ((ZMap.set t0 (false, z) la0)) with la in × by congruence.
injection H0; intros.
replace tp0 with t in IHQ_CalMCSLock by assumption.
apply (next_correct_equiv_la la0 la ( ((QT MCS_WAITING_BUSY j bj)::q)) Hla_equiv).
simpl.
destruct (IHQ_CalMCSLock t la0 tq0 eq_refl).
auto.
+
exact (IHQ_CalMCSLock t la tq eq_refl).
+
auto.
+
eapply IHQ_CalMCSLock; eauto.
Qed.
Corollary Q_CalMCSLock_next_correct_at_head : ∀ l i bi j bj q,
Q_CalMCSLock l ((QT MCS_INSIDE i bi) :: (QT MCS_WAITING_BUSY j bj) :: q) →
∀ tp la tq, CalMCSLock l = Some (MCSLOCK tp la tq) →
snd (ZMap.get i la) = j.
Proof.
intros l i bi j bj q HQ_Cal tp la tq HCal.
assert (NC := Q_CalMCSLock_next_correct _ _ HQ_Cal _ _ _ HCal).
simpl in NC.
destruct NC as [? _].
auto.
Qed.
Lemma ZMap_get_set_fst : ∀ A B i j x (la : ZMap.t (A×B)),
fst (ZMap.get i (ZMap.set j (fst (ZMap.get j la), x) la)) = fst (ZMap.get i la).
Proof.
intros; destruct (Z_eq_dec i j); subst; simpl; destruct (ZMap.get j la);
[rewrite ZMap.gss | rewrite ZMap.gso by auto] ; reflexivity.
Qed.
Lemma ZMap_get_set_fst´ : ∀ A B i j x (la : ZMap.t (A×B)),
fst (ZMap.get i (ZMap.set j (fst (ZMap.get i la), x) la)) = fst (ZMap.get i la).
Proof.
intros; destruct (Z_eq_dec i j); subst; simpl; destruct (ZMap.get j la);
[rewrite ZMap.gss | rewrite ZMap.gso by auto] ; reflexivity.
Qed.
Lemma Q_CalMCSLock_head_not_busy : ∀ l q,
Q_CalMCSLock l q → ∀ i bi q0 t la tq, CalMCSLock l = Some (MCSLOCK t la tq) →
q = ((QT MCS_WAITING_BUSY i bi) :: q0) →
fst (ZMap.get i la) = false.
Proof.
induction 1; simpl; intros.
+
congruence.
+
congruence.
+
destruct (CalMCSLock l) as [[t0 la0 tq0] |]; [|congruence].
replace la with ((ZMap.set i (true, NULL) la0)) by congruence.
destruct q as [|qt q].
- congruence.
- simpl in ×.
replace qt with (QT MCS_WAITING_BUSY i0 bi) in IHQ_CalMCSLock by congruence.
replace qt with (QT MCS_WAITING_BUSY i0 bi) in H2 by congruence. simpl in H2.
rewrite ZMap.gso by auto.
apply IHQ_CalMCSLock with (q0 := q) (t := t0) (bi0 := bi) (tq := tq0); auto.
+
apply IHQ_CalMCSLock with (q0 := q0) (t := t) (bi := bi) (tq:=tq).
destruct (CalMCSLock l) as [[? ? ?]|]; congruence.
auto.
+
destruct (CalMCSLock l) as [[t0 la0 tq0] |]; [|congruence].
assert (fst (ZMap.get i0 (ZMap.set j (fst (ZMap.get j la0), i) la0))
= fst (ZMap.get i0 la0)) as Hget by (apply ZMap_get_set_fst).
destruct (ZMap.get j la0) as [b´ t´].
replace la with ((ZMap.set j (b´,i) la0)) by congruence.
simpl in Hget.
rewrite Hget.
destruct pre as [|p pre].
- simpl in ×.
apply IHQ_CalMCSLock with (q0 := (QT MCS_BEFORE_SET_NEXT i bi) :: post) (t := t0) (bi:=bi0) (tq:=tq0).
auto.
congruence.
- simpl in ×.
apply IHQ_CalMCSLock with (q0 := pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post) (t := t0) (bi:=bi0) (tq:=tq0).
auto.
congruence.
+
eapply IHQ_CalMCSLock with (t:=t) (bi:=bi) (tq:=tq).
- destruct (CalMCSLock l) as [[? ? ?]|]; simpl in *; congruence.
- eassumption.
+
eapply IHQ_CalMCSLock with (t:=t) (q0:=q0) (bi0:=bi) (tq:=tq).
- destruct (CalMCSLock l) as [[? ?]|]; simpl in *; congruence.
- congruence.
+
assert (NC := Q_CalMCSLock_next_correct_at_head l i bi j bj q H).
destruct (CalMCSLock l) as [[tp0 la0 tq0]|]; simpl in *; [|congruence].
assert (NC´ := NC tp0 la0 tq0 eq_refl); clear NC.
destruct (ZMap.get i la0) as [z1 t1].
simpl in NC´.
subst.
destruct (ZMap.get j la0 ) as [z2 t2].
replace la with (ZMap.set j (false, t2) la0) by congruence.
replace i0 with j by congruence.
rewrite ZMap.gss.
reflexivity.
+
eapply IHQ_CalMCSLock with (t:=t) (q0:=q0) (bi:=bi) (tq:=tq).
- destruct (CalMCSLock l) as [[? ? ?]|]; simpl in *; congruence.
- congruence.
+
eapply IHQ_CalMCSLock with (t:=t) (q0:=q0) (bi0:=bi) (tq:=tq).
- destruct (CalMCSLock l) as [[? ? ?]|]; simpl in *; congruence.
- congruence.
+
subdestruct.
inv H1.
eapply IHQ_CalMCSLock; eauto.
Qed.
Lemma Q_CalMCSLock_tail_is_busy_SWAP_not_nil´ : ∀ A (x:A) l y,
In x (l ++ y :: nil) → (In x l ∨ x=y).
Proof.
induction l; simpl; intros; try specialize (IHl y); intuition; congruence.
Qed.
Lemma Q_CalMCSLock_tail_is_busy_SWAP_not_nil : ∀ A (x:A) l y,
In x (tl (l ++ y :: nil)) → (In x (tl l) ∨ x=y).
Proof.
destruct l.
+ simpl. tauto.
+ simpl. auto using Q_CalMCSLock_tail_is_busy_SWAP_not_nil´.
Qed.
Lemma Q_CalMCSLock_tail_is_busy_SET_NEXT : ∀ pre s j bj i bi (post : list QThread),
(map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post))
= (map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)).
Proof.
induction pre; intros; simpl; try rewrite IHpre; auto.
Qed.
Lemma Q_CalMCSLock_tail_is_busy : ∀ l q,
Q_CalMCSLock l q → ∀ t la tq, CalMCSLock l = Some (MCSLOCK t la tq) →
∀ i, In i (tail (map qthread_tid q)) → fst (ZMap.get i la) = true.
Proof.
induction 1; simpl; intros.
+
auto. +
tauto. +
destruct (CalMCSLock l) as [[t0 la0 tq0]|] ; [|congruence].
replace la with (ZMap.set i (true, NULL) la0) by congruence.
rewrite map_app in H4.
simpl in H4.
apply Q_CalMCSLock_tail_is_busy_SWAP_not_nil in H4.
destruct H4.
- rewrite <- (IHQ_CalMCSLock _ _ _ eq_refl i0) by auto.
apply ZMap_get_set_fst´.
- subst; rewrite ZMap.gss; auto.
+
destruct (CalMCSLock l) as [[t0 la0 tq0]|] ; [|congruence].
apply IHQ_CalMCSLock with (t:=t0) (la:=la) (tq:=tq); auto; congruence.
+
destruct (CalMCSLock l) as [[t0 la0 tq0]|] ; [|congruence].
assert (fst (ZMap.get i0 la0) = fst (ZMap.get i0 ((ZMap.set j (fst (ZMap.get j la0), i) la0)))) by (symmetry; apply ZMap_get_set_fst).
destruct (ZMap.get j la0) as [b1 t1].
simpl in ×.
replace la with ((ZMap.set j (b1, i) la0)) by congruence.
rewrite <- H3.
apply IHQ_CalMCSLock with (t:=t0) (la:=la0) (tq:=tq0); auto.
rewrite Q_CalMCSLock_tail_is_busy_SET_NEXT in H2.
rewrite <- H0 in H2.
assumption.
+
destruct (CalMCSLock l) as [[t0 la0 tq0]|] ; [|congruence].
apply IHQ_CalMCSLock with (t:=t0) (la:=la) (tq:=tq0); auto; congruence.
+
destruct (CalMCSLock l) as [[t0 la0 tq0]|] ; [|congruence].
apply IHQ_CalMCSLock with (t:=t0) (la:=la) (tq:=tq0); auto; congruence.
+
assert (Hnext_correct := Q_CalMCSLock_next_correct_at_head _ _ _ _ _ _ H).
destruct (CalMCSLock l); [ | now congruence].
destruct m as [tp0 la0 tq0].
specialize Hnext_correct with tp0 la0 tq0.
destruct (ZMap.get i la0) as [b t0].
replace t0 with j in × by (pose (Hnext_correct eq_refl); simpl in *; congruence).
clear Hnext_correct.
destruct (ZMap.get j la0).
replace la with (ZMap.set j (false, z) la0) by congruence.
rewrite ZMap.gso.
- apply (IHQ_CalMCSLock tp0 la0 tq0 eq_refl).
simpl; auto.
- apply Q_CalMCSLock_NoDup in H; use_NoDup.
+
destruct (CalMCSLock l) as [[t0 la0 tq0]|] ; [|congruence].
apply IHQ_CalMCSLock with (t:=t0) (la:=la) (tq:=tq0); auto; congruence.
+
tauto.
+
subdestruct; inv H0.
eapply IHQ_CalMCSLock; eauto.
Qed.
Lemma Q_CalMCSLock_tail_not_INSIDE : ∀ l i bi q,
Q_CalMCSLock l q → ¬ In (QT MCS_INSIDE i bi) (tail q).
Proof.
induction 1; simpl; intros; subst; simpl in *; auto;
match goal with [|- ¬ (In _ (tl (?pre ++ _)))] ⇒
destruct pre; simpl in *; try rewrite in_app in *; simpl in *; intuition
end.
Qed.
Lemma Q_CalMCS_NoDup_injectivity´ : ∀ q s s´ i bi bi´,
NoDup (map qthread_tid q) →
In (QT s i bi) q → In (QT s´ i bi´) q → (QT s i bi) = (QT s´ i bi´).
Proof.
induction q.
+ simpl. tauto.
+ intros s s´ i bi bi´ HNoDup HIn1 HIn2.
inversion HNoDup as [|? ? HNoDup1 HNoDup2].
subst.
inversion HIn1; inversion HIn2.
- subst. congruence.
- apply (In_map _ _ qthread_tid) in H0.
rewrite H in HNoDup1.
simpl in *; tauto.
- apply (In_map _ _ qthread_tid) in H.
rewrite H0 in HNoDup1.
simpl in *; tauto.
- apply IHq with (i:=i); auto.
Qed.
Lemma Q_CalMCS_NoDup_injectivity : ∀ l q s s´ i bi bi´,
Q_CalMCSLock l q →
In (QT s i bi) q → In (QT s´ i bi´) q → (QT s i bi) = (QT s´ i bi´).
Proof.
intros.
apply Q_CalMCSLock_NoDup in H.
eauto using Q_CalMCS_NoDup_injectivity´.
Qed.
Lemma Q_CalMCSLock_inv_cons : ∀ a l q,
Q_CalMCSLock (a::l) q → ∃ q0, Q_CalMCSLock l q0.
Proof.
inversion 1; subst; eauto.
Qed.
Lemma other_threads_multistep : ∀ i (P :Q_MCSLockState → Prop) l l´ q q´,
(∀ e k l q q´,
P q →
Q_CalMCSLock l q →
Q_CalMCSLock ((TEVENT k e)::l) q´ →
k ≠ i →
P q´) →
Q_CalMCSLock l q →
Q_CalMCSLock (l´++l) q´ →
(∀ k e, In (TEVENT k e) l´ → k ≠ i) →
P q →
P q´.
Proof.
induction l´ as [|[k e] l´].
× simpl. intros.
replace q´ with q by (eauto using Q_CalMCSLock_functional).
auto.
× simpl.
intros q q´ Hstep HCal_l HCal_l´ Hdisjoint H.
destruct (Q_CalMCSLock_inv_cons _ _ _ HCal_l´) as [q0 H_q0].
apply Hstep with (e:=e) (k:=k) (l:=l´++l) (q:=q0).
- apply IHl´ with q; auto; firstorder.
- assumption.
- assumption.
- apply Hdisjoint with (e0:=e); auto.
Qed.
Lemma other_threads_preserve_WAITING_BUSY´ : ∀ i bi l k e q q´,
Q_CalMCSLock l q →
Q_CalMCSLock ((TEVENT k e)::l) q´ →
In (QT MCS_WAITING_BUSY i bi) q →
k ≠ i →
In (QT MCS_WAITING_BUSY i bi) q´.
Proof.
intros i bi l k e q q´ HCal HCal´ H Hk.
inversion HCal´; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst; simpl in *; try rewrite in_app in *; simpl in *; intuition.
Qed.
Lemma other_threads_preserve_WAITING_BUSY : ∀ i bi l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
In (QT MCS_WAITING_BUSY i bi) q →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ In (QT MCS_WAITING_BUSY i bi) q´.
Proof.
induction l´ as [| [k e] l´]; simpl; intros.
× replace q´ with q by (eauto using Q_CalMCSLock_functional); auto.
× destruct (Q_CalMCSLock_inv_cons _ _ _ H) as [q0 H_q0].
apply other_threads_preserve_WAITING_BUSY´ with (e:=e) (k:=k) (l:=l´++l) (q:=q0).
assumption.
assumption.
apply IHl´ with q; auto.
firstorder.
{ apply H2 with e. auto. }
Qed.
Hint Rewrite ZSet.mem_spec not_eq_true ZSet.add_spec ZSet.union_spec : zset.
Ltac solve_zset :=
repeat (progress (autorewrite with zset in *; simpl in ×
|| match goal with [H: ZSet.In _ ZSet.empty |- _] ⇒ apply ZSet.empty_spec in H
| [ |- ?X = ?Y ] ⇒ apply ZSet.eq_leibniz; intro x
end
|| intuition)).
Lemma slowset_of_QMCSLockState_app : ∀ (q q´ : Q_MCSLockState),
slowset_of_QMCSLockState (q ++ q´)
= ZSet.union (slowset_of_QMCSLockState q) (slowset_of_QMCSLockState q´).
Proof.
induction q as [ | [ [ | | ] ? ?]]; intros; simpl; try rewrite IHq; solve_zset.
Qed.
Lemma other_threads_preserve_not_slow´ : ∀ i e k l q q´,
Q_CalMCSLock ((TEVENT k e)::l) q´ →
k ≠ i →
Q_CalMCSLock l q →
ZSet.mem i (slowset_of_QMCSLockState q) = false →
ZSet.mem i (slowset_of_QMCSLockState q´) = false.
Proof.
inversion 1; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst; simpl in *; auto.
+ rewrite slowset_of_QMCSLockState_app; solve_zset.
+ subst q.
rewrite slowset_of_QMCSLockState_app in *; destruct s; solve_zset.
Qed.
Lemma other_threads_preserve_not_slow : ∀ i l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
ZSet.mem i (slowset_of_QMCSLockState q) = false →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ ZSet.mem i (slowset_of_QMCSLockState q´) = false.
Proof.
intros.
apply other_threads_multistep with (P:=fun q ⇒ ZSet.mem i (slowset_of_QMCSLockState q) = false) (i:=i) (l:=l) (l´:=l´) (q:=q); auto.
firstorder.
eauto using other_threads_preserve_not_slow´.
Qed.
Lemma Q_MCSLockThreadState_eq_dec : ∀ (s s´ : Q_MCSLockThreadState),
{s = s´} + {s ≠ s´}.
Proof.
decide equality.
Defined.
Section WITH_WAIT_TIME.
Require Import LogReplay.
Context `{waittime: WaitTime}.
Lemma CalMCS_QSCal_bound : ∀ l tailptr la bounds self_c rel_c b q slow tq,
CalMCSLock l = Some (MCSLOCK tailptr la bounds) →
QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq) →
bounds = tq.
Proof.
Local Transparent CalMCSLock QS_CalLock init_MCSLock.
induction l as [|a l].
× simpl; intros.
unfold init_MCSLock in H.
congruence.
× destruct a as [i e].
destruct e as [e | e ]; destruct e eqn:?;
simpl; intros;
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;
try match goal with
| [H: Some ?m = Some (MCSLOCK _ _ _) |- _ ] ⇒ destruct m as [? ? ?] eqn:?
end;
specialize (IHl _ _ _ _ _ _ _ _ _ eq_refl eq_refl);
subst; simpl in *; congruence.
Qed.
Lemma QS_CalLock_q_nil_same : ∀ ll self_c rel_c b q slow tq,
QS_CalLock ll = Some (self_c, rel_c, b, q, slow, tq) → (q = nil ↔ tq = nil).
Proof.
intros.
apply QS_CalLock_q_length_same in H.
destruct q; destruct tq; simpl in H; split; intros; try congruence; auto.
Qed.
Lemma wait_lock_CalMCS_AcqWait :
∀ o,
relate_mcs_qs_oracle o →
valid_multi_oracle_domain o →
get_free_qslock_oracle o →
∀ n hl hl´ q i bi,
Q_CalMCSLock hl q →
In (QT MCS_WAITING_BUSY i bi) q →
ZSet.mem i (slowset_of_QMCSLockState q) = false →
QState_of_QMCSLockState q (QS_CalLock hl) →
get_free_qslock hl →
QS_CalWaitGet n i hl o = Some hl´ →
CalMCS_AcqWait n i hl o = Some hl´
∧ relate_qs_mcs_log hl´
∧ correct_qslock_status hl´ (LockOwn false) i
∧ CalValidBit hl´ = Some FreeToPull.
Proof.
Transparent CalMCS_AcqWait QS_CalWaitGet QS_CalLock.
intros o Hrelate_oracle Hvalid_oracle Hfree_oracle.
induction n; simpl.
+ intros; congruence.
+ intros hl hl´ q i bi HQCalMCS HIn H_not_slow HQCal Hfree.
inversion Hrelate_oracle. subst.
pose (hl1 := o i hl ++ hl).
assert (Hrelate_log1 : relate_qs_mcs_log hl1).
{
unfold hl1.
apply Hrelate_mcs_qs_oracle_res.
apply RELATE_QS_MCS_LOG with q; assumption.
}
destruct Hrelate_log1 as [q1 HQCalMCS1 HQCal1].
assert (In (QT MCS_WAITING_BUSY i bi) q1) as HIn1.
{
apply other_threads_preserve_WAITING_BUSY with (l:=hl) (l´:=o i hl) (q:=q); auto.
unfold valid_multi_oracle_domain in Hvalid_oracle.
intros; eapply Hvalid_oracle; eauto.
}
assert (ZSet.mem i (slowset_of_QMCSLockState q1) = false) as H_not_slow1.
{
apply other_threads_preserve_not_slow with (l:=hl) (l´:=o i hl) (q:=q); auto.
unfold valid_multi_oracle_domain in Hvalid_oracle.
intros; eapply Hvalid_oracle; eauto.
}
assert (get_free_qslock hl1) as Hfree1 by (apply Hfree_oracle; assumption).
change (o i hl ++ hl) with hl1.
clearbody hl1.
clear hl q HQCalMCS HQCal Hfree HIn H_not_slow.
destruct (Q_CalMCSLock_completeness hl1 q1 HQCalMCS1) as [[t la] Ht_la].
rewrite Ht_la.
inversion HQCal1 as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 HQCal1_inv].
symmetry in HQCal1_inv.
destruct q1 as [| [s j bj] q1_tail]; [simpl in *; tauto | ].
assert (Hbusy_head := Q_CalMCSLock_head_not_busy hl1 ((QT s j bj) :: q1_tail) HQCalMCS1 i bj q1_tail t la bounds Ht_la).
assert (Hbusy_tail := Q_CalMCSLock_tail_is_busy hl1 ((QT s j bj)::q1_tail) HQCalMCS1 t la bounds Ht_la i).
destruct (ZMap.get i la) as [[|] next]; simpl in Hbusy_head, Hbusy_tail.
- assert (In (QT MCS_WAITING_BUSY i bi) q1_tail) as HIn2.
{
destruct HIn1.
+ assert (true=false) by (apply Hbusy_head; congruence).
congruence.
+ auto.
}
assert (i ≠ j).
{
destruct (Q_MCSLockThreadState_eq_dec s MCS_WAITING_BUSY) as [e|e].
+ intros Heq.
subst.
pose (Hbusy_head eq_refl).
congruence.
+ intros Heq.
subst.
inversion HIn1.
- congruence.
- apply Q_CalMCSLock_NoDup in HQCalMCS1.
simpl in HQCalMCS1.
inversion HQCalMCS1. subst.
apply (In_map _ _ qthread_tid) in HIn2.
simpl in HIn2.
auto.
}
intros HCal1´.
assert (QS_CalWaitGet n i (TEVENT i (TTICKET (GET_BUSY true)) :: hl1) o = Some hl´) as HCal1.
{
simpl in Hqs1.
rewrite Hqs1 in HCal1´.
rewrite zeq_false in HCal1´; auto.
}
clear HCal1´.
assert (QState_of_QMCSLockState ((QT s j bj) :: q1_tail) (QS_CalLock (TEVENT i (TTICKET (GET_BUSY true)) :: hl1)))
as HQCal2.
{
simpl.
rewrite HQCal1_inv.
simpl in Hqs1.
rewrite Hqs1.
rewrite zeq_false by auto.
rewrite Hslow1, H_not_slow1.
destruct tq1 as [|tq1_head tq1_tail]; [simpl in Htq1; congruence|].
rewrite <- Hqs1.
rewrite <- Hslow1.
apply (QSTATE_OF_QMCSLOCKSTATE (QT s j bj :: q1_tail) self_c1 rel_c1 b1 qs1 slow1 (tq1_head :: tq1_tail)); try congruence; simpl; congruence.
}
assert (Q_CalMCSLock (TEVENT i (TTICKET (GET_BUSY true)) :: hl1) ((QT s j bj) :: q1_tail)) as HCalMCS2.
{
apply Q_CalMCSLock_GET_BUSY_true.
assumption.
assumption.
}
assert (get_free_qslock (TEVENT i (TTICKET (GET_BUSY true)) :: hl1)) as Hfree2.
{
unfold get_free_qslock in ×.
intros.
simpl in Hcal.
subdestruct.
specialize (Hfree1 _ _ _ _ _ _ eq_refl).
rewrite Hfree1; congruence.
}
exact (IHn ((TEVENT i (TTICKET (GET_BUSY true)) :: hl1)) hl´ _ i _ HCalMCS2 HIn1 H_not_slow1 HQCal2 Hfree2 HCal1).
- assert ((QT s j bj) = (QT MCS_WAITING_BUSY i bi)) as H_sj.
{
inversion HIn1 as [? | HIn].
- auto.
- apply (In_map _ _ qthread_tid) in HIn.
pose (Hbusy_tail HIn).
congruence.
}
replace s with MCS_WAITING_BUSY in × by congruence.
replace j with i in × by congruence.
replace bj with bi in × by congruence.
rewrite Hqs1.
simpl.
rewrite zeq_true.
intros H_hl´.
replace hl´ with (TEVENT i (TTICKET (GET_BUSY false)) :: hl1) by congruence.
assert (tq1 ≠ nil).
{
rewrite <- (QS_CalLock_q_nil_same _ _ _ _ _ _ _ HQCal1_inv).
simpl in Hqs1.
intros ?; congruence.
}
destruct tq1 as [|tq1_head tq1_tail]; [congruence|].
assert (QS_CalLock (TEVENT i (TTICKET (GET_BUSY false)) :: hl1)
= Some (S tq1_head, S CalPassLockTime, LHOLD, qs1, slow1, tq1_head :: tq1_tail))
as HQCal2.
{
simpl.
rewrite HQCal1_inv, Hqs1, Hb1.
simpl.
destruct (zeq i i); congruence.
}
split; [|split; [|split]].
× reflexivity.
× apply RELATE_QS_MCS_LOG with ((QT MCS_INSIDE i bi) :: q1_tail).
apply Q_CalMCSLock_GET_BUSY_false.
assumption.
rewrite HQCal2.
{
apply (QSTATE_OF_QMCSLOCKSTATE _ _ _ LHOLD qs1 slow1 (tq1_head :: tq1_tail));
simpl in *; congruence.
}
× unfold correct_qslock_status.
{
intros; split.
+ intros; congruence.
+ intros.
simpl in ×.
∃ (map qthread_tid q1_tail).
split; [|split].
- congruence.
- congruence.
- split.
× intro contra.
assert (false = true) by auto.
congruence.
× subdestruct.
inv Hcal.
omega.
}
× unfold get_free_qslock in Hfree1.
specialize (Hfree1 _ _ _ _ _ _ HQCal1_inv Hb1).
unfold get_free_qslock.
intros.
simpl.
rewrite Hfree1.
reflexivity.
Qed.
Definition thread_before_set_next (j i : Z) (q : Q_MCSLockState) :=
∃ pre s bj bi post,
q = pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post.
Lemma other_threads_preserve_BEFORE_SET_NEXT´´ : ∀ j i pre k bk post,
k ≠ i →
thread_before_set_next j i (pre ++ (QT MCS_BEFORE_SET_NEXT k bk) :: post) →
thread_before_set_next j i (pre ++ (QT MCS_WAITING_BUSY k bk) :: post).
Proof.
intros.
destruct H0 as [pre0 [s [bj [bi [post0 Heq]]]]].
destruct (split_lists _ _ _ _ _ Heq) as [[? ?] | [? ?]]; subst.
+ rewrite <- app_assoc in Heq.
apply prepend_inj in Heq.
destruct x.
- simpl in Heq.
replace post with ((QT MCS_BEFORE_SET_NEXT i bi) :: post0) by congruence.
∃ pre.
∃ MCS_WAITING_BUSY.
∃ bj.
∃ bi.
∃ post0.
congruence.
- simpl in Heq.
replace post with (x ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post0) by congruence.
∃ (pre ++ (QT MCS_WAITING_BUSY k bk) :: x).
∃ s.
∃ bj.
∃ bi.
∃ post0.
rewrite <- app_assoc.
reflexivity.
+ rewrite <- app_assoc in Heq.
apply prepend_inj in Heq.
destruct x as [|qt q].
- simpl in Heq.
replace post with ((QT MCS_BEFORE_SET_NEXT i bi) :: post0) by congruence.
∃ pre0.
∃ MCS_WAITING_BUSY.
∃ bj.
∃ bi.
∃ post0.
rewrite app_nil_r.
congruence.
- simpl in Heq.
rewrite <- app_assoc.
simpl.
destruct q as [|qt0 q].
× simpl in Heq. congruence.
× simpl in Heq.
simpl.
replace qt with (QT s j bj) by congruence.
replace qt0 with (QT MCS_BEFORE_SET_NEXT i bi) by congruence.
∃ pre0.
∃ s.
∃ bj.
∃ bi.
∃ (q ++ (QT MCS_WAITING_BUSY k bk) :: post).
reflexivity.
Qed.
Lemma other_threads_preserve_BEFORE_SET_NEXT´ : ∀ j i e k l q q´,
Q_CalMCSLock ((TEVENT k e)::l) q´ →
k ≠ i →
Q_CalMCSLock l q →
thread_before_set_next j i q →
thread_before_set_next j i q´.
Proof.
inversion 1; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst;
match goal with [ H : thread_before_set_next _ _ _ |- _ ] ⇒
inversion H as [pre0 [s0 [bj0 [bi0 [post0 Heq]]]]]
end.
+
destruct pre0; simpl in Heq; congruence.
+
∃ pre0.
∃ s0.
∃ bj0.
∃ bi0.
∃ (post0 ++ (QT MCS_BEFORE_SET_NEXT k bound) :: nil).
rewrite Heq.
rewrite <- app_assoc.
reflexivity.
+ auto.
+
replace (pre ++ (QT s j0 bj) :: (QT MCS_WAITING_BUSY k bi) :: post)
with ((pre ++ (QT s j0 bj) :: nil) ++ (QT MCS_WAITING_BUSY k bi) :: post)
by (rewrite <- app_assoc; reflexivity).
replace (pre ++ (QT s j0 bj) :: (QT MCS_BEFORE_SET_NEXT k bi) :: post)
with ((pre ++ (QT s j0 bj) :: nil) ++ (QT MCS_BEFORE_SET_NEXT k bi) :: post)
in Hfunctional
by (rewrite <- app_assoc; reflexivity).
apply other_threads_preserve_BEFORE_SET_NEXT´´; auto.
rewrite Hfunctional; auto.
+ auto.
+
destruct pre0; simpl in ×.
- ∃ nil.
∃ MCS_INSIDE.
∃ bj0.
∃ bi0.
∃ post0.
simpl.
congruence.
- ∃ ((QT MCS_INSIDE k bi) :: pre0).
∃ s0.
∃ bj0.
∃ bi0.
∃ post0.
replace q0 with (pre0 ++ (QT s0 j bj0) :: (QT MCS_BEFORE_SET_NEXT i bi0) :: post0) by congruence.
reflexivity.
+
destruct pre0; simpl in ×.
- congruence.
- replace ((QT MCS_WAITING_BUSY j0 bj) :: q0)
with (pre0 ++ (QT s0 j bj0) :: (QT MCS_BEFORE_SET_NEXT i bi0) :: post0)
by congruence.
∃ pre0.
∃ s0.
∃ bj0.
∃ bi0.
∃ post0.
reflexivity.
+
auto.
+
assert (gt (length ((QT MCS_INSIDE k bi)::nil)) (S O)).
{
rewrite Heq.
destruct pre0; [ |destruct pre0]; simpl; auto with arith.
}
simpl in ×.
omega.
+
auto.
Qed.
Lemma other_threads_preserve_BEFORE_SET_NEXT : ∀ j i l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
thread_before_set_next j i q →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ thread_before_set_next j i q´.
Proof.
induction l´.
× simpl. intros.
replace q´ with q by (eauto using Q_CalMCSLock_functional).
auto.
× simpl.
intros.
destruct (Q_CalMCSLock_inv_cons _ _ _ H) as [q0 H_q0].
destruct a as [k e].
apply other_threads_preserve_BEFORE_SET_NEXT´ with (e:=e) (k:=k) (l:=l´++l) (q:=q0).
assumption.
{ apply H2 with e. auto. }
assumption.
apply IHl´ with q; auto.
firstorder.
Qed.
Lemma other_threads_preserve_Not_In´ : ∀ i e k l q q´,
Q_CalMCSLock ((TEVENT k e)::l) q´ →
k ≠ i →
Q_CalMCSLock l q →
¬In i (map qthread_tid q) →
¬In i (map qthread_tid q´).
Proof.
inversion 1; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst;
(try match goal with [ H : thread_before_set_next _ _ _ |- _ ] ⇒
inversion H as [pre [s [post Heq]]]
end);
intros; simpl in *;
repeat (progress (rewrite map_app in × || rewrite in_app in *); simpl in *; subst); intuition.
Qed.
Lemma other_threads_preserve_Not_In : ∀ i l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
¬In i (map qthread_tid q) →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ ¬In i (map qthread_tid q´).
Proof.
intros.
apply other_threads_multistep with (P:=fun q ⇒ ¬In i (map qthread_tid q)) (i:=i) (l:=l) (l´:=l´) (q:=q); auto.
firstorder.
eauto using other_threads_preserve_Not_In´.
Qed.
Lemma BEFORE_SET_NEXT_is_slow´ : ∀ i (q q´: Q_MCSLockState),
¬ In i (map qthread_tid q) →
ZSet.mem i (slowset_of_QMCSLockState (q ++ q´))
= ZSet.mem i (slowset_of_QMCSLockState q´).
Proof.
induction q.
+ simpl; auto.
+ simpl; intros.
destruct a as [s j].
destruct s.
- rewrite ZSet_gso.
apply IHq; tauto.
simpl in H. intros e.
symmetry in e. tauto.
- auto.
- auto.
Qed.
Lemma BEFORE_SET_NEXT_is_slow :
∀ (pre : Q_MCSLockState) s j bj i bi post,
NoDup (map qthread_tid ((pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))) →
ZSet.mem i (slowset_of_QMCSLockState ((pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))) = true.
Proof.
intros pre s j bj i bi post.
replace ((pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))
with ((pre ++ (QT s j bj) :: nil) ++ (QT MCS_BEFORE_SET_NEXT i bi) :: post)
by (rewrite <- app_assoc; reflexivity).
intros H.
assert (¬In i (map qthread_tid (pre ++ (QT s j bj) :: nil))) by (use_NoDup´ i).
rewrite BEFORE_SET_NEXT_is_slow´ by auto.
simpl.
apply ZSet_gss.
Qed.
Lemma QState_of_QMCSLockState_SET_NEXT_queue : ∀ (pre : Q_MCSLockState) s j bj i bi post,
map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)
= map qthread_tid (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post).
Proof.
induction pre.
+ simpl; auto.
+ simpl; intros; f_equal; auto.
Qed.
Lemma QState_of_QMCSLockState_SET_NEXT_bounds : ∀ (pre : Q_MCSLockState) s j bj i bi post,
map qthread_bound (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)
= map qthread_bound (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post).
Proof.
induction pre.
+ simpl; auto.
+ simpl; intros; f_equal; auto.
Qed.
Lemma QState_of_QMCSLockState_SET_NEXT_head_status : ∀ (pre : Q_MCSLockState) s j bj i bi post,
head_status_of_QMCSLockState (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)
= head_status_of_QMCSLockState (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post).
Proof.
induction pre.
+ simpl; auto.
+ simpl; intros; f_equal; auto.
Qed.
Lemma slowset_queue_subset : ∀ i q,
ZSet.In i (slowset_of_QMCSLockState q) → In i (map qthread_tid q).
Proof.
induction q as [ | [ [ | | ] ? ? ]]; simpl; intros; solve_zset.
Qed.
Lemma QState_of_QMCSLockState_SET_NEXT_slowset´ : ∀ (pre : Q_MCSLockState) i bi post,
NoDup (map qthread_tid (pre ++ (QT MCS_BEFORE_SET_NEXT i bi) :: post)) →
ZSet.remove i (slowset_of_QMCSLockState (pre ++ (QT MCS_BEFORE_SET_NEXT i bi) :: post))
= (slowset_of_QMCSLockState (pre ++ (QT MCS_WAITING_BUSY i bi) :: post)).
Proof.
intros pre i bi post ND.
repeat rewrite slowset_of_QMCSLockState_app.
simpl.
apply ZSet.eq_leibniz.
intros x.
rewrite ZSet.remove_spec.
repeat rewrite ZSet.union_spec.
rewrite ZSet.add_spec.
intuition.
+ subst.
rewrite map_app in ND.
rewrite NoDup_app in ND.
simpl in ND.
destruct ND as [_ [_ ND]].
specialize ND with i.
auto using slowset_queue_subset.
+ rewrite map_app in ND.
rewrite NoDup_app in ND.
simpl in ND.
destruct ND as [_ [ND _]].
apply slowset_queue_subset in H0.
inversion ND; subst; auto.
Qed.
Lemma QState_of_QMCSLockState_SET_NEXT_slowset : ∀ l pre s j bj i bi post,
Q_CalMCSLock l ((pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post)) →
ZSet.remove i (slowset_of_QMCSLockState (pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))
= (slowset_of_QMCSLockState (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post)).
Proof.
intros.
replace ((pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post))
with ((pre ++ (QT s j bj) ::nil ) ++ (QT MCS_BEFORE_SET_NEXT i bi) :: post) by
(rewrite <- app_assoc; reflexivity).
replace ((pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post))
with ((pre ++ (QT s j bj) ::nil ) ++ (QT MCS_WAITING_BUSY i bi) :: post) by
(rewrite <- app_assoc; reflexivity).
apply QState_of_QMCSLockState_SET_NEXT_slowset´.
{
apply Q_CalMCSLock_NoDup in H.
rewrite <- app_assoc.
exact H.
}
Qed.
Lemma slowset_BEFORE_SET_NEXT : ∀ i bi q,
ZSet.add i (slowset_of_QMCSLockState q) =
slowset_of_QMCSLockState (q ++ (QT MCS_BEFORE_SET_NEXT i bi) :: nil).
Proof.
intros. rewrite slowset_of_QMCSLockState_app. solve_zset.
Qed.
Lemma slowset_of_QMCSLockState_SET_NEXT_false :
∀ q0 s old_tail b_old_tail curid b_curid qpost,
NoDup (map qthread_tid (q0 ++ QT s old_tail b_old_tail :: QT MCS_WAITING_BUSY curid b_curid :: qpost)) →
ZSet.mem curid
(slowset_of_QMCSLockState
(q0 ++
QT s old_tail b_old_tail :: QT MCS_WAITING_BUSY curid b_curid :: qpost)) = false.
Proof.
Hint Rewrite slowset_of_QMCSLockState_app : zset.
intros. use_NoDup´ curid.
solve_zset;
repeat (match goal with
| [H : ZSet.In _ (slowset_of_QMCSLockState _) |- _] ⇒ apply slowset_queue_subset in H
| [H : ZSet.In _ (match ?s with MCS_BEFORE_SET_NEXT ⇒ _
| _ ⇒ _ end) |- _ ] ⇒ destruct s
end; solve_zset).
Qed.
Inductive thread_has_lock i : Q_MCSLockState → Prop :=
| THREAD_HAS_LOCK : ∀ bi q0, thread_has_lock i ((QT MCS_INSIDE i bi)::q0).
Lemma CalLock_thread_has_lock : ∀ q i queue,
head_status_of_QMCSLockState q = LHOLD →
map qthread_tid q = (i::queue) →
thread_has_lock i q.
Proof.
intros q i queue H1 H2.
destruct q as [| qt q].
- compute in H1. congruence.
- destruct qt as [s j bj].
simpl in ×.
destruct s; try congruence.
replace i with j by congruence.
apply THREAD_HAS_LOCK.
Qed.
Lemma other_threads_preserve_thread_has_lock´ : ∀ i l k e q q´,
Q_CalMCSLock l q →
Q_CalMCSLock ((TEVENT k e)::l) q´ →
thread_has_lock i q →
k ≠ i →
thread_has_lock i q´.
Proof.
intros i l k e q q´ HCal HCal´ H Hk.
inversion HCal´; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst.
+
inversion H.
+
inversion H.
simpl.
apply THREAD_HAS_LOCK.
+
inversion H.
apply THREAD_HAS_LOCK.
+
inversion H.
destruct pre as [|qt pre]; simpl in ×.
- replace (QT s j bj) with (QT MCS_INSIDE i bi0) by congruence.
apply THREAD_HAS_LOCK.
- replace qt with (QT MCS_INSIDE i bi0) by congruence.
apply THREAD_HAS_LOCK.
+
inversion H.
apply THREAD_HAS_LOCK.
+
inversion H.
+
inversion H.
congruence. +
inversion H.
apply THREAD_HAS_LOCK.
+
inversion H.
congruence. +
assumption.
Qed.
Lemma other_threads_preserve_thread_has_lock : ∀ i l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
thread_has_lock i q →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ thread_has_lock i q´.
Proof.
intros.
apply other_threads_multistep with (i:=i) (l:=l) (l´:=l´) (q:=q); auto.
firstorder.
eauto using other_threads_preserve_thread_has_lock´.
Qed.
Inductive thread_has_lock_next i j : Q_MCSLockState → Prop :=
| THREAD_HAS_LOCK_NEXT : ∀ bi s bj q0, thread_has_lock_next i j ((QT MCS_INSIDE i bi)::(QT s j bj)::q0).
Lemma other_threads_preserve_thread_has_lock_next´ : ∀ i j l k e q q´,
Q_CalMCSLock l q →
Q_CalMCSLock ((TEVENT k e)::l) q´ →
thread_has_lock_next i j q →
k ≠ i →
thread_has_lock_next i j q´.
Proof.
intros i j l k e q q´ HCal HCal´ H Hk.
inversion HCal´; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst;
inversion H; try congruence; try apply THREAD_HAS_LOCK_NEXT.
+ destruct pre as [ | p1 [ | p2 pre´]]; simpl in ×.
- replace (QT s j0 bj) with (QT MCS_INSIDE i bi0) by congruence.
replace k with j by congruence.
apply THREAD_HAS_LOCK_NEXT.
- replace p1 with (QT MCS_INSIDE i bi0) by congruence.
replace j0 with j by congruence.
apply THREAD_HAS_LOCK_NEXT.
- replace p1 with (QT MCS_INSIDE i bi0) by congruence.
replace p2 with (QT s0 j bj0) by congruence.
apply THREAD_HAS_LOCK_NEXT.
Qed.
Lemma other_threads_preserve_thread_has_lock_next : ∀ i j l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
thread_has_lock_next i j q →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ thread_has_lock_next i j q´.
Proof.
intros.
apply other_threads_multistep with (i:=i) (l:=l) (l´:=l´) (q:=q); auto.
firstorder.
eauto using other_threads_preserve_thread_has_lock_next´.
Qed.
Inductive thread_has_lock_next_fast i j : Q_MCSLockState → Prop :=
| THREAD_HAS_LOCK_NEXT_FAST : ∀ bi bj q0, thread_has_lock_next_fast i j ((QT MCS_INSIDE i bi)::(QT MCS_WAITING_BUSY j bj)::q0).
Lemma other_threads_preserve_thread_has_lock_next_fast´ : ∀ i j l k e q q´,
Q_CalMCSLock l q →
Q_CalMCSLock ((TEVENT k e)::l) q´ →
thread_has_lock_next_fast i j q →
k ≠ i →
thread_has_lock_next_fast i j q´.
Proof.
intros i j l k e q q´ HCal HCal´ H Hk.
inversion HCal´; intros;
match goal with [ Ha : Q_CalMCSLock ?l _, Hb : Q_CalMCSLock ?l _ |- _ ] ⇒
assert (Hfunctional := Q_CalMCSLock_functional _ _ _ Ha Hb)
end; subst;
inversion H; try congruence; try apply THREAD_HAS_LOCK_NEXT_FAST.
+ destruct pre as [ | p1 [ | p2 pre´]]; simpl in ×.
- replace (QT s j0 bj) with (QT MCS_INSIDE i bi0) by congruence.
replace k with j by congruence.
apply THREAD_HAS_LOCK_NEXT_FAST.
- replace p1 with (QT MCS_INSIDE i bi0) by congruence.
replace (QT s j0 bj) with (QT MCS_WAITING_BUSY j bj) by congruence.
apply THREAD_HAS_LOCK_NEXT_FAST.
- replace p1 with (QT MCS_INSIDE i bi0) by congruence.
replace p2 with (QT MCS_WAITING_BUSY j bj0) by congruence.
apply THREAD_HAS_LOCK_NEXT_FAST.
Qed.
Lemma other_threads_preserve_thread_has_lock_next_fast : ∀ i j l l´ q q´,
Q_CalMCSLock (l´++l) q´ →
Q_CalMCSLock l q →
thread_has_lock_next_fast i j q →
(∀ k e, In (TEVENT k e) l´ → k ≠ i)
→ thread_has_lock_next_fast i j q´.
Proof.
intros.
apply other_threads_multistep with (i:=i) (l:=l) (l´:=l´) (q:=q); auto.
firstorder.
eauto using other_threads_preserve_thread_has_lock_next_fast´.
Qed.
Lemma not_in_slowset : ∀ i q,
¬ In i (map qthread_tid q) → ZSet.mem i (slowset_of_QMCSLockState q) = false.
Proof.
intros.
rewrite ZSet_mem_spec_false.
pose (slowset_queue_subset i q).
tauto.
Qed.
Lemma other_threads_preserve_rel_c_onestep : ∀ j e ll self_c rel_c b i q slow tq self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock ll = Some (self_c, rel_c, b, i :: q, slow, tq) →
QS_CalLock (TEVENT j e :: ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
j ≠ i →
∃ q0,
rel_c´ = rel_c
∧ q´ = i :: q0.
Proof.
Transparent QS_CalLock.
intros until tq´.
intros HCal 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.
+ ∃ (q ++ j :: nil).
simpl in HCal´.
repeat split; congruence.
+ ∃ q.
split; congruence.
+ ∃ q.
split; congruence.
Qed.
Lemma other_threads_preserve_rel_c´ : ∀ i ll self_c0 rel_c0 b0 q0 slow0 tq0 ll1 self_c rel_c b q slow tq ,
QS_CalLock ll = Some (self_c0, rel_c0, b0, i::q0, slow0, tq0) →
QS_CalLock (ll1 ++ ll) = Some (self_c, rel_c, b, q, slow, tq) →
(∀ k e, In (TEVENT k e) ll1 → k≠i) →
∃ qtail,
rel_c0 = rel_c
∧ q = i :: qtail.
Proof.
Opaque QS_CalLock.
induction ll1 as [|e ll1].
× simpl.
intros.
∃ q0.
repeat split; try congruence.
× intros until tq.
intros HCal0 HCal 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´) as [qtail1 [ Hrel_c´ Hq´]].
{ intros k1 e1.
specialize Hdomain with k1 e1.
auto. }
rewrite Hq´ in HCal´.
destruct e as [k e].
assert (k ≠ i) as Hik.
{ specialize Hdomain with k e.
auto. }
destruct (other_threads_preserve_rel_c_onestep k e _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal´ HCal Hik) as [ q0´´ [Hrel_c´´ Hq´´]].
∃ q0´´.
repeat split; try congruence.
Qed.
Lemma other_threads_preserve_rel_c : ∀ i lo ll self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ ,
QS_CalLock ll = Some (self_c, rel_c, b, i::q, slow, tq) →
QS_CalLock (lo i ll ++ ll) = Some (self_c´, rel_c´, b´, i::q´, slow´, tq´) →
valid_multi_oracle_domain lo →
rel_c = rel_c´.
Proof.
intros until tq´.
intros HCal HCal1 Hvalid_domain.
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 (other_threads_preserve_rel_c´ i ll self_c rel_c b q slow tq ll1 self_c´ rel_c´ b´ (i::q´) slow´ tq´) as [qtail [? ?]]; auto.
Qed.
Lemma other_threads_preserve_FreeToPull_onestep : ∀ j e ll self_c rel_c b i q slow tq self_c´ rel_c´ b´ q´ slow´ tq´,
QS_CalLock ll = Some (self_c, rel_c, b, i :: q, slow, tq) →
QS_CalLock (TEVENT j e :: ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
CalValidBit ll = Some FreeToPull →
j ≠ i →
∃ q0,
CalValidBit (TEVENT j e :: ll) = Some FreeToPull
∧ q´ = i :: q0.
Proof.
Transparent QS_CalLock.
intros until tq´.
intros HCal HCal´ Hvalid 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; rewrite Hvalid.
+ ∃ (q ++ j :: nil).
simpl in HCal´.
simpl.
repeat split; congruence.
+ ∃ q.
split; congruence.
+ ∃ q.
split; congruence.
Qed.
Lemma other_threads_preserve_FreeToPull´ : ∀ i ll self_c0 rel_c0 b0 q0 slow0 tq0 ll1 self_c rel_c b q slow tq ,
QS_CalLock ll = Some (self_c0, rel_c0, b0, i::q0, slow0, tq0) →
QS_CalLock (ll1 ++ ll) = Some (self_c, rel_c, b, q, slow, tq) →
CalValidBit ll = Some FreeToPull →
(∀ k e, In (TEVENT k e) ll1 → k≠i) →
∃ qtail,
CalValidBit (ll1 ++ ll) = Some FreeToPull
∧ q = i :: qtail.
Proof.
Opaque QS_CalLock CalValidBit.
induction ll1 as [|e ll1].
× simpl.
intros.
∃ q0.
repeat split; try congruence.
× intros until tq.
intros HCal0 HCal Hvalid 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´ Hvalid) as [qtail1 [ Hvalid´ Hq´]].
{ intros k1 e1.
specialize Hdomain with k1 e1.
auto. }
rewrite Hq´ in HCal´.
destruct e as [k e].
assert (k ≠ i) as Hik.
{ specialize Hdomain with k e.
auto. }
destruct (other_threads_preserve_FreeToPull_onestep k e _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal´ HCal Hvalid´ Hik) as [ q0´´ [Hvalid´´ Hq´´]].
∃ q0´´.
repeat split; try congruence.
Qed.
Lemma other_threads_preserve_FreeToPull : ∀ i lo ll self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´ ,
QS_CalLock ll = Some (self_c, rel_c, b, i::q, slow, tq) →
QS_CalLock (lo i ll ++ ll) = Some (self_c´, rel_c´, b´, i::q´, slow´, tq´) →
CalValidBit ll = Some FreeToPull →
valid_multi_oracle_domain lo →
CalValidBit (lo i ll ++ ll) = Some FreeToPull.
Proof.
intros until tq´.
intros HCal HCal1 Hvalid Hvalid_domain.
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 (other_threads_preserve_FreeToPull´ i ll self_c rel_c b q slow tq ll1 self_c´ rel_c´ b´ (i::q´) slow´ tq´) as [qtail [? ?]]; 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 pass_lock_CalWaitRel : ∀ i j o,
valid_multi_oracle_domain o →
relate_mcs_qs_oracle o →
∀ n hl hl´ q,
Q_CalMCSLock hl q →
QS_CalWaitRel n i j hl o = Some hl´ →
relate_qs_mcs_log hl →
thread_has_lock_next i j q →
CalValidBit hl = Some FreeToPull →
CalMCS_RelWait n i hl o = Some (pass_lock_final hl´ i o)
∧ relate_qs_mcs_log (pass_lock_final hl´ i o)
∧ (∃ self_c´ rel_c´ q0´ q´ slow´ tq´,
QS_CalLock (pass_lock_final1 hl´ i o) = Some (self_c´, rel_c´, q0´::q´, slow´, tq´))
∧ correct_qslock_status (pass_lock_final hl´ i o) LockFalse i
∧ CalValidBit (pass_lock_final hl´ i o) = Some FreeToPull.
Proof.
Transparent QS_CalLock QS_CalWaitRel CalMCS_RelWait.
intros i j o H_valid_oracle H_relate_oracle.
induction n.
simpl.
- intros.
congruence.
- intros hl hl´ q H_CalMCS H_CalWaitRel H_relate_log H_has_lock_next H_valid.
inversion H_relate_oracle; subst.
pose (hl1 := o i hl ++ hl).
assert (relate_qs_mcs_log hl1) as H_relate_log1 by
(apply Hrelate_mcs_qs_oracle_res; auto).
destruct H_relate_log1 as [q1 H_QCalMCS1 HQCal1].
assert (thread_has_lock_next i j q1) as H_has_lock_next1.
{
apply other_threads_preserve_thread_has_lock_next with (l:=hl) (l´:= o i hl) (q:=q).
exact H_QCalMCS1.
auto.
auto.
intros k e; apply H_valid_oracle.
}
assert (CalValidBit hl1 = Some FreeToPull) as H_valid1.
{
clear IHn Hrelate_mcs_qs_oracle_res H_CalWaitRel.
inversion H_relate_log as [q0 H_CalMCS0 HQCal0].
replace q0 with q in × by (eapply Q_CalMCSLock_functional; eauto).
clear q0.
inversion HQCal0 as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HQCal_inv].
symmetry in HQCal_inv.
inversion H_has_lock_next.
subst.
simpl in ×.
inversion HQCal1 as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 HQCal1_inv].
symmetry in HQCal1_inv.
unfold hl1.
inversion H_has_lock_next1.
subst.
simpl in ×.
apply (other_threads_preserve_FreeToPull _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HQCal_inv HQCal1_inv); auto.
}
simpl.
change (o i hl ++ hl) with hl1.
unfold QS_CalWaitRel in H_CalWaitRel.
change (o i hl ++ hl) with hl1 in H_CalWaitRel.
clearbody hl1.
clear hl q H_CalMCS H_relate_log H_has_lock_next H_valid.
inversion HQCal1 as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 HQCal1_inv].
symmetry in HQCal1_inv.
rewrite HQCal1_inv in H_CalWaitRel.
destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS1) as [[t1 la1] H_CalMCS1].
rewrite H_CalMCS1.
inversion H_has_lock_next1 as [bi s bj q1_tail H_q1_tail].
subst q1.
assert (H_next_correct := Q_CalMCSLock_next_correct hl1 ((QT MCS_INSIDE i bi) :: (QT s j bj) :: q1_tail) H_QCalMCS1 t1 la1 bounds H_CalMCS1).
simpl in H_next_correct. destruct H_next_correct as [H_next_correct _].
destruct (ZMap.get i la1) as [busy next].
destruct (zeq next NULL) as [H_next | H_next]; simpl in H_next_correct.
+
assert (s = MCS_BEFORE_SET_NEXT).
{
assert (In (QT s j bj) ((QT MCS_INSIDE i bi) :: (QT s j bj) :: q1_tail)) as HIn by (right; left; auto).
assert (In j (map qthread_tid ((QT MCS_INSIDE i bi) :: (QT s j bj) :: q1_tail))) as HIn´ by (apply (In_map _ _ qthread_tid _ _ HIn)).
assert (H_j_not_null := Q_CalMCSLock_not_NULL _ _ _ H_QCalMCS1 HIn´).
destruct s.
- reflexivity.
- congruence.
- congruence.
}
subst s.
rewrite Hslow1 in H_CalWaitRel.
simpl in H_CalWaitRel.
rewrite ZSet_gss in H_CalWaitRel.
fold QS_CalWaitRel in H_CalWaitRel.
assert (ZSet.mem j (slowset_of_QMCSLockState q1_tail) = false) as H_j_not_in_slowset
by (apply not_in_slowset; apply Q_CalMCSLock_NoDup in H_QCalMCS1; use_NoDup´ j).
apply IHn with (hl:=(TEVENT i (TTICKET GET_NEXT) :: hl1))
(q:= ((QT MCS_INSIDE i bi) :: (QT MCS_BEFORE_SET_NEXT j bj) :: q1_tail)).
× apply Q_CalMCSLock_GET_NEXT.
assumption.
× destruct rel_c1 as [|?]; [congruence|].
assumption.
× apply RELATE_QS_MCS_LOG with (q:= ((QT MCS_INSIDE i bi) :: (QT MCS_BEFORE_SET_NEXT j bj) :: q1_tail)).
apply Q_CalMCSLock_GET_NEXT; assumption.
unfold QS_CalWaitRel in H_CalWaitRel.
destruct rel_c1 as [|rel_c1´]; [congruence|].
destruct n as [|n]; [congruence|].
destruct (QS_CalLock (o i (TEVENT i (TTICKET GET_NEXT) :: hl1) ++ TEVENT i (TTICKET GET_NEXT) :: hl1))
as [[[[[[self_c01 rel_c01] b01] q01] slow01] tq01] | ] eqn:H01; [|congruence].
destruct (QS_CalLock_inv_app _ _ _ _ _ _ _ _ H01)
as [self_c02 [rel_c02 [b02 [q02 [slow02 [tq02 H02]]]]]].
rewrite H02.
simpl in H02.
rewrite HQCal1_inv in H02.
rewrite Hqs1 in H02.
simpl in H02.
destruct tq1 as [ | ? ?]; [congruence|].
destruct (zeq i i); [|congruence].
rewrite Hb1 in H02.
simpl in H02.
simpl in Hslow1.
simpl in Htq1.
apply QSTATE_OF_QMCSLOCKSTATE; simpl; congruence.
× assumption.
× Transparent CalValidBit.
simpl.
rewrite H_valid1.
reflexivity.
+
assert (s = MCS_WAITING_BUSY) as Hs.
{
destruct s.
- congruence.
- reflexivity.
- elimtype False.
apply (Q_CalMCSLock_tail_not_INSIDE _ j bj _ H_QCalMCS1).
simpl. auto.
}
subst s.
assert (ZSet.mem j (slowset_of_QMCSLockState q1_tail) = false) as H_j_not_in_slowset
by (apply not_in_slowset; apply Q_CalMCSLock_NoDup in H_QCalMCS1; use_NoDup´ j).
rewrite Hslow1 in H_CalWaitRel.
simpl in H_CalWaitRel.
rewrite H_j_not_in_slowset in H_CalWaitRel.
pose (hl2 := o i ((TEVENT i (TTICKET GET_NEXT)) :: hl1) ++ ((TEVENT i (TTICKET GET_NEXT)) :: hl1)).
fold hl2 in H_CalWaitRel.
fold hl2.
destruct rel_c1 as [|rel_c1´] ; [congruence|].
destruct rel_c1´ as [|rel_c1´´] ; [congruence|].
assert (relate_qs_mcs_log hl2) as Hrelate_log2.
{
unfold hl2.
apply Hrelate_mcs_qs_oracle_res.
apply RELATE_QS_MCS_LOG with (q := (QT MCS_INSIDE i bi) :: (QT MCS_WAITING_BUSY j bj) :: q1_tail).
+ Hint Constructors Q_CalMCSLock.
auto.
+ simpl.
rewrite HQCal1_inv.
rewrite Hqs1.
simpl.
assert (tq1 ≠ nil).
{
rewrite <- (QS_CalLock_q_nil_same _ _ _ _ _ _ _ HQCal1_inv).
rewrite Hqs1.
simpl.
discriminate.
}
destruct tq1 as [| ? ?]; [congruence|].
rewrite zeq_true.
rewrite Hb1.
simpl.
apply QSTATE_OF_QMCSLOCKSTATE.
simpl; congruence.
simpl; congruence.
simpl; simpl in *; congruence.
simpl; simpl in *; congruence.
}
destruct Hrelate_log2 as [q2 H_QCalMCS2 H_QCal2].
assert (H_has_lock_next2 : thread_has_lock_next_fast i j q2).
{
apply other_threads_preserve_thread_has_lock_next_fast
with (l:= (TEVENT i (TTICKET GET_NEXT) :: hl1))
(l´:= o i ((TEVENT i (TTICKET GET_NEXT) :: hl1)))
(q:= (QT MCS_INSIDE i bi)::(QT MCS_WAITING_BUSY j bj)::q1_tail).
exact H_QCalMCS2.
auto.
apply THREAD_HAS_LOCK_NEXT_FAST.
intros k e; apply H_valid_oracle.
}
inversion H_has_lock_next2 as [bi´ bj´ q2_tail Hq2].
subst.
assert (ZSet.mem i (slowset_of_QMCSLockState q2_tail) = false) as H_i_not_in_slowset.
{
apply not_in_slowset.
apply Q_CalMCSLock_NoDup in H_QCalMCS2.
simpl in H_QCalMCS2.
match goal with [H : NoDup _ |- _ ] ⇒ inversion H end.
simpl in H1.
tauto.
}
assert (CalValidBit hl2 = Some FreeToPull) as H_valid2.
{
inversion H_QCal2 as [self_c2 rel_c2 b2 qs2 slow2 tq2 Hb2 Hqs2 Hslow2 Htq2 HQCal2_inv].
symmetry in HQCal2_inv.
rewrite Hqs2 in HQCal2_inv; simpl in HQCal2_inv.
simpl in HQCal1_inv.
assert (HQCal1_inv´ : QS_CalLock ((TEVENT i (TTICKET GET_NEXT) :: hl1)) =
Some
(self_c1, (S rel_c1´´), LHOLD,
i :: j :: map qthread_tid q1_tail,
slowset_of_QMCSLockState q1_tail,
bi :: bj :: map qthread_bound q1_tail)).
{ simpl.
rewrite HQCal1_inv.
rewrite zeq_true.
reflexivity.
}
apply (other_threads_preserve_FreeToPull _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HQCal1_inv´ HQCal2_inv); auto.
simpl.
rewrite H_valid1.
reflexivity.
}
inversion H_QCal2 as [self_c2 rel_c2 b2 qs2 slow2 tq2 Hb2 Hqs2 Hslow2 Htq2 HQCal2_inv].
symmetry in HQCal2_inv.
assert (tq2 ≠ nil) by (destruct tq2; [simpl in *; congruence | discriminate]).
destruct tq2 as [|t tq´]; [congruence|].
assert (QS_CalLock (TEVENT i (TTICKET SET_BUSY) :: hl2) =
(Some (0%nat, 0%nat, LEMPTY, j :: map qthread_tid q2_tail, slowset_of_QMCSLockState q2_tail, tq´)))
as HQCal3_inv.
{
simpl.
rewrite HQCal2_inv.
rewrite Hqs2. simpl.
rewrite zeq_true.
rewrite Hb2. simpl.
assert (rel_c2 = S rel_c1´´) as H_rel_c2.
{
unfold hl2 in ×.
simpl in HQCal1_inv, HQCal2_inv.
assert (QS_CalLock (TEVENT i (TTICKET GET_NEXT) :: hl1) =
Some (self_c1, S rel_c1´´, LHOLD, i :: j :: map qthread_tid q1_tail, slowset_of_QMCSLockState q1_tail, bi :: bj :: map qthread_bound q1_tail))
as HQCal1_inv´.
{ simpl.
rewrite HQCal1_inv.
rewrite zeq_true.
reflexivity.
}
subst.
symmetry.
apply (other_threads_preserve_rel_c _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HQCal1_inv´ HQCal2_inv H_valid_oracle).
}
rewrite H_rel_c2.
rewrite Hslow2. simpl.
rewrite H_i_not_in_slowset.
simpl.
reflexivity.
}
assert (relate_qs_mcs_log (TEVENT i (TTICKET SET_BUSY) :: hl2)).
{
apply RELATE_QS_MCS_LOG with (q := (QT MCS_WAITING_BUSY j bj´) :: q2_tail).
+ Hint Constructors Q_CalMCSLock.
eauto.
+ rewrite HQCal3_inv.
eapply QSTATE_OF_QMCSLOCKSTATE.
× reflexivity.
× reflexivity.
× reflexivity.
× simpl in Htq2.
simpl.
congruence.
}
replace hl´ with hl1 by congruence.
assert (Hcalmcs: ∃ tail´ la´ bnd´, CalMCSLock hl2 = Some (MCSLOCK tail´ la´ bnd´) ∧
snd (ZMap.get i la´) ≠ NULL).
{
destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS2) as (mcs´, mcs_exists).
destruct mcs´ as (tail´ & ndpool´).
rewrite mcs_exists.
eexists; eexists; eexists; split; [reflexivity|].
pose (Hnext_correct := Q_CalMCSLock_next_correct _ _ H_QCalMCS2 _ _ _ mcs_exists).
destruct Hnext_correct as [Hnext_correct _].
rewrite Hnext_correct.
assumption.
}
destruct Hcalmcs as (tail´ & la´ & bnd´ & Hcalmcs1 & HCalmcs2).
rewrite Hcalmcs1.
remember (ZMap.get i la´) as ndv´.
destruct ndv´.
simpl in HCalmcs2.
rewrite zeq_false; auto.
split; [reflexivity|].
unfold pass_lock_final, pass_lock_final1.
fold hl2.
split; [|split; [|split]].
× assumption.
× repeat eexists.
rewrite Hqs2 in HQCal2_inv.
exact HQCal2_inv.
× unfold correct_qslock_status.
intros.
split; intros; [| congruence].
rewrite HQCal3_inv in Hcal.
replace q with ( j :: map qthread_tid q2_tail) by congruence.
apply Q_CalMCSLock_NoDup in H_QCalMCS2.
simpl in H_QCalMCS2.
inversion H_QCalMCS2.
assumption.
× simpl.
rewrite H_valid2.
reflexivity.
Qed.
Lemma Q_CalMCSLock_tail_AT_HEAD : ∀ l s i bi q,
Q_CalMCSLock l (QT s i bi ::q) →
∀ t la tq,
CalMCSLock l = Some (MCSLOCK t la tq) →
(t = i ↔ q = nil).
Proof.
intros l s i bi q HQCal t la tq HCal.
assert (NoDup (i :: map qthread_tid q)) as HNoDup
by (eapply Q_CalMCSLock_NoDup with (q := (QT s i bi) :: q); eauto).
assert (Htail_sound : t = tail_id (QT s i bi::q))
by (eauto using tail_soundness).
split.
+ assert (i ≠ NULL).
{
apply (Q_CalMCSLock_not_NULL _ _ _ HQCal).
simpl.
auto.
}
assert (q = nil ∨ t = tail_id q) as Hq.
{
destruct q; simpl in Htail_sound.
left; congruence.
right.
rewrite Htail_sound. reflexivity.
}
destruct Hq.
- auto.
- intros; subst.
assert (In i (map qthread_tid q)).
{
replace i with (tail_id q) in × by congruence.
apply tail_id_In.
assumption.
}
inversion HNoDup.
tauto.
+ intros; subst; simpl in *; auto.
Qed.
Lemma SWAP_TAIL_false_preserves_get_free_qslock : ∀ i bound l,
get_free_qslock l → get_free_qslock (TEVENT i (TTICKET (SWAP_TAIL bound false)) :: l).
Proof.
clear.
unfold get_free_qslock.
intros i bound l Hfree.
intros.
simpl in Hcal.
repeat match goal with | [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match QS_CalLock ?X with Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒
destruct (QS_CalLock X) as [[[[[[? ?] ?] ?] ?] ?] | ] eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MultiUndef ⇒ _ | MultiDef _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
end; try congruence; subdestruct.
specialize (Hfree _ _ _ _ _ _ eq_refl).
replace h with k in Hfree by congruence.
simpl.
rewrite Hfree; congruence.
Qed.
Lemma SET_NEXT_preserves_get_free_qslock : ∀ i ot l,
get_free_qslock l → get_free_qslock (TEVENT i (TTICKET (SET_NEXT ot)) :: l).
Proof.
clear.
unfold get_free_qslock.
intros i bound l Hfree.
intros.
simpl in Hcal.
repeat match goal with | [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X
| [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match QS_CalLock ?X with Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒
destruct (QS_CalLock X) as [[[[[[? ?] ?] ?] ?] ?] | ] eqn:?
| [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒ destruct X eqn:?
| [HCal´ : context[match ?X with | MultiUndef ⇒ _ | MultiDef _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
end; try congruence; subdestruct;
(specialize (Hfree _ _ _ _ _ _ eq_refl);
replace h with k in Hfree by congruence;
simpl; rewrite Hfree; congruence).
Qed.
End WITH_WAIT_TIME.
End QSMCSLAYERAUXLEMMA.