Commit 4c3c9058 authored by Hai Dang's avatar Hai Dang
Browse files

Major cleanup of graph specs; reuse proofs

parent 91435ea2
......@@ -497,10 +497,7 @@ Proof.
intros ? [CONDv CON2a CON2b [CON3a CON3b] CON4 CON5].
intros e eV egV G'.
constructor; [ |done|..|done| |done].
- (* DView *)
intros e0 eV0. case (decide (e = e0)) => ?.
+ subst e0. by rewrite lookup_app_1_eq => [[<-//]].
+ rewrite lookup_app_1_ne; [by apply CONDv|done].
- (* DView *) by apply graph_insert_event_is_releasing.
- (* 2b *)
intros e1 e2 (? & eV1 & eV2 & ve1 & ve2 & Eq1 & Eq2 & ?)%CON2b.
split; [done|].
......@@ -539,14 +536,9 @@ Proof.
have EqEs' : G'.(Es) = (G.(Es) ++ [Emi]) ++ [Emx] by apply (app_assoc _ [_] [_]).
have Eqemx : emx = length (Es G ++ [Emi]). { rewrite app_length /=. lia. }
constructor; [|split| |split|..].
- (* DView *)
intros e eV. rewrite EqEs'.
case (decide (emi = e)) => ?; last case (decide (emx = e)) => ?.
+ subst e. rewrite lookup_app_1_ne; [|by rewrite -Eqemx].
rewrite lookup_app_1_eq => [[<-]]. clear -LeV11 LeV22; destruct b; done.
+ subst e. rewrite Eqemx lookup_app_1_eq => [[<-]].
clear -LeV11 LeV22; destruct b; done.
+ do 2 (rewrite lookup_app_1_ne; [|lia]). by apply CONDv.
- (* DView *) rewrite /= (app_assoc _ [_]). clear -LeV11 LeV22 CONDv.
apply graph_insert_event_is_releasing;
[apply graph_insert_event_is_releasing|]; [done|..]; by destruct b.
- (* 2a1 *)
intros i j. rewrite /= elem_of_union CON2a1. clear. set_solver.
- (* 2a2 *)
......
......@@ -41,7 +41,7 @@ Definition ExchangerInvT Σ : Type :=
Record ExchangerConsistent (G : graph) : Prop := mkExchangerConsistent {
(* The first one is our own side condition *)
xchg_cons_dview : (* exchange is releasing *)
graph_event_is_releasing G (λ _, True) ;
graph_event_is_releasing G.(Es) (λ _, True) ;
(* (1)-(5) Exchanger spec from Yacovet (POPL'19) paper *)
(* (1) at most 1 Constructor event: we currently don't have initialization events *)
......
......@@ -105,26 +105,26 @@ Record eventgraph_consistent G :=
(** eco must agree with xo : eco ⊆ xo.
This prevents cycles in eco, which doesn't work for exchanger.
See also "Benign Synchronisation Cycles" in the Yacovet (POPL'19) paper. *)
Definition graph_xo_eco G : Prop :=
e1 e2 eV2, G.(Es) !! e2 = Some eV2 e1 eV2.(ge_lview) (e1 e2)%nat
Definition graph_xo_eco E : Prop :=
e1 e2 eV2, E !! e2 = Some eV2 e1 eV2.(ge_lview) (e1 e2)%nat
(* ∧ eV1.(ge_lview) ⊑ eV2.(ge_lview) *)
(* ^^ this doesn't work because we are not rel-acq (have relaxed ops). *)
.
Definition graph_event_is_releasing G (P : eventT Prop) :=
e eV, G.(Es) !! e = Some eV P eV.(ge_event)
Definition graph_event_is_releasing E (P : eventT Prop) :=
e eV, E !! e = Some eV P eV.(ge_event)
eV.(ge_view).(dv_comm) eV.(ge_view).(dv_wrt).
Definition graph_event_is_acquiring G (P : eventT Prop) :=
e eV, G.(Es) !! e = Some eV P eV.(ge_event)
Definition graph_event_is_acquiring E (P : eventT Prop) :=
e eV, E !! e = Some eV P eV.(ge_event)
eV.(ge_view).(dv_wrt) eV.(ge_view).(dv_comm).
Definition graph_event_is_writing G (P : eventT Prop) :=
e eV, G.(Es) !! e = Some eV P eV.(ge_event)
Definition graph_event_is_writing E (P : eventT Prop) :=
e eV, E !! e = Some eV P eV.(ge_event)
eV.(ge_view).(dv_in) eV.(ge_view).(dv_comm).
Definition graph_event_is_relacq G (P : eventT Prop) :=
e eV, G.(Es) !! e = Some eV P eV.(ge_event)
Definition graph_event_is_relacq E (P : eventT Prop) :=
e eV, E !! e = Some eV P eV.(ge_event)
eV.(ge_view).(dv_comm) = eV.(ge_view).(dv_wrt).
Lemma eventgraph_consistent_empty : eventgraph_consistent .
......@@ -138,4 +138,24 @@ Lemma gcons_not_in_com_l G e : (length G.(Es), e) ∉ G.(com).
Proof. intros [Lt _]%gcons_com_included. simpl in Lt. lia. Qed.
Lemma gcons_not_in_com_r G e : (e, length G.(Es)) G.(com).
Proof. intros [_ Lt]%gcons_com_included. simpl in Lt. lia. Qed.
Lemma graph_event_is_relacq_releasing E (P Q : eventT Prop) :
( e, P e Q e)
graph_event_is_relacq E Q graph_event_is_releasing E P.
Proof.
intros PQ RA e eV Eqe Pe%PQ. by rewrite (RA _ _ Eqe Pe).
Qed.
Lemma graph_event_is_relacq_releasing_True E (P : eventT Prop) :
graph_event_is_relacq E (λ _, True) graph_event_is_releasing E P.
Proof. by apply graph_event_is_relacq_releasing. Qed.
Lemma graph_event_is_relacq_acquiring E (P Q : eventT Prop) :
( e, P e Q e)
graph_event_is_relacq E Q graph_event_is_acquiring E P.
Proof.
intros PQ RA e eV Eqe Pe%PQ. by rewrite (RA _ _ Eqe Pe).
Qed.
Lemma graph_event_is_relacq_acquiring_True E (P : eventT Prop) :
graph_event_is_relacq E (λ _, True) graph_event_is_acquiring E P.
Proof. by apply graph_event_is_relacq_acquiring. Qed.
End defs.
......@@ -6,12 +6,54 @@ From gpfsl.examples.graph Require Import graph.
Require Import iris.prelude.options.
Section graph_ex.
Section graph_insert_props.
Context {A : Type}.
Notation graph_event := (graph_event A).
Notation graph := (graph A).
Notation event_list := (event_list A).
Implicit Types (G : graph) (E : event_list) (M : logView) (V : dataView).
Lemma graph_insert_event_is_writing P E eV :
graph_event_is_writing E P
(P eV.(ge_event) eV.(ge_view).(dv_in) eV.(ge_view).(dv_comm))
graph_event_is_writing (E ++ [eV]) P.
Proof. intros RA ??? [?%RA|[-> <-]]%lookup_app_1; done. Qed.
Lemma graph_insert_event_is_relacq P E eV :
graph_event_is_relacq E P
(P eV.(ge_event) eV.(ge_view).(dv_comm) = eV.(ge_view).(dv_wrt))
graph_event_is_relacq (E ++ [eV]) P.
Proof. intros RA ??? [?%RA|[-> <-]]%lookup_app_1; done. Qed.
Lemma graph_insert_event_is_releasing P E eV :
graph_event_is_releasing E P
(P eV.(ge_event) eV.(ge_view).(dv_comm) eV.(ge_view).(dv_wrt))
graph_event_is_releasing (E ++ [eV]) P.
Proof. intros RA ??? [?%RA|[-> <-]]%lookup_app_1; done. Qed.
Lemma graph_insert_event_is_acquiring P E eV :
graph_event_is_acquiring E P
(P eV.(ge_event) eV.(ge_view).(dv_wrt) eV.(ge_view).(dv_comm))
graph_event_is_acquiring (E ++ [eV]) P.
Proof. intros RA ??? [?%RA|[-> <-]]%lookup_app_1; done. Qed.
Lemma graph_insert_xo_eco E eV :
graph_xo_eco E
set_in_bound eV.(ge_lview) (E ++ [eV])
graph_xo_eco (E ++ [eV]).
Proof.
intros EC IN e1 e2 eV2 [Eqe|[-> <-]]%lookup_app_1.
- apply (EC _ _ _ Eqe).
- intros Lt%IN%lookup_lt_is_Some. rewrite app_length /= in Lt. lia.
Qed.
End graph_insert_props.
Implicit Types (G : graph) (M : logView) (V : dataView).
Section graph_ex.
Context {A : Type}.
Notation graph_event := (graph_event A).
Notation graph := (graph A).
Notation event_list := (event_list A).
Implicit Types (G : graph) (E : event_list) (M : logView) (V : dataView).
(** Extending a Graph with a new event *)
Program Definition graph_insert_event eV G : graph :=
......
......@@ -2012,25 +2012,16 @@ Proof.
assert (NI: e1 e2, (e1, e2) G'.(com) e1 enqId e2 enqId).
{ clear. move => ?? /(gcons_com_included G3) [/= ]. lia. }
have QC' : WeakQueueConsistent G'. {
destruct CON3 as [CONW CONRel CONAcq CONNZ CON2 CON3 CON4 CON5 CON6 CON7a CON7b].
split.
- intros e eV. case (decide (enqId = e)) => ?.
+ subst e. rewrite lookup_app_1_eq.
clear -LeV1 LeV2 NEqV23. inversion 1. simpl. intros _ ->.
apply NEqV23. by apply : (anti_symm ()).
+ rewrite lookup_app_1_ne; [by apply CONW|done].
- intros e eV. case (decide (enqId = e)) => ?.
+ subst e. clear. rewrite lookup_app_1_eq. inversion 1. done.
+ rewrite lookup_app_1_ne; [by apply CONRel|done].
- intros e eV Eqe Eqv'.
have ? : e enqId.
{ clear -Eqv' Eqe. intros ->. rewrite lookup_app_1_eq in Eqe. inversion Eqe.
destruct Eqv'. by subst eV. }
rewrite lookup_app_1_ne in Eqe; [by apply (CONAcq _ _ Eqe Eqv')|done].
- intros e eV v'. case (decide (enqId = e)) => ?.
+ subst e. clear -Posx. rewrite lookup_app_1_eq.
inversion 1. simpl. inversion 1. by subst v'.
+ rewrite lookup_app_1_ne; [by apply CONNZ|done].
destruct CON3 as [CONW CONRel CONAcq [CONNZ CON2 CON3 CON4 CON5 CON6 CON7a CON7b]].
constructor; [..|constructor].
- clear -LeV1 LeV2 NEqV23 CONW.
apply graph_insert_event_is_writing; [done|]. simpl. intros _ ->.
apply NEqV23. by apply : (anti_symm ()).
- clear -CONRel. by apply graph_insert_event_is_releasing.
- clear -CONAcq. apply graph_insert_event_is_acquiring; [done|].
simpl; intros []; congruence.
- intros ??? [Eq1|[-> <-]]%lookup_app_1; [by apply (CONNZ _ _ _ Eq1)|].
clear -Posx. simpl. inversion 1. by subst.
- intros e d InG'. destruct (NI _ _ InG').
destruct (CON2 _ _ InG')
as (LteD & eV & dV & v' & Eqe & Eqd & EqeV & EqdV & LeedV).
......@@ -2048,11 +2039,7 @@ Proof.
apply (egcons_logview_closed _ EGCs3 _ _ Eqe), lookup_lt_is_Some in Inee.
clear -Inee. lia.
- done.
- intros e1 e2 eV2. case (decide (e2 = enqId)) => [->|?].
+ rewrite lookup_app_1_eq => EqeV2. inversion EqeV2; clear EqeV2; subst eV2.
rewrite /= elem_of_union elem_of_singleton. move => [-> //|InM1].
by apply Nat.lt_le_incl, lookup_lt_is_Some, SubM, InM1.
+ rewrite lookup_app_1_ne; [by apply CON7a|done].
- clear -CON7a SUB'. by apply graph_insert_xo_eco.
- intros e1 eV1 v1 e2 d2 eV2 Eqe1 Eqv1 In2.
destruct (NI _ _ In2). rewrite lookup_app_1_ne; [|done].
intros Eqe2 IneV2.
......@@ -2301,7 +2288,7 @@ Proof.
iDestruct (view_at_elim with "sVx sζi") as "sζi". rewrite shift_lblock_assoc.
iExists γi, ζi. iFrame "SN sζi". iPureIntro.
exists ti, v. eexists. split; [done|].
apply (wkq_cons_enq_non_zero _ CONx e eV v EqeV Eqv).
apply (bsq_cons_enq_non_zero _ CONx e eV v EqeV Eqv).
- iDestruct "SS" as (L0 EqL0) "SS".
destruct (lookup_lt_is_Some_2 L0 idx) as [γi Eqγi]; [by rewrite EqL0|].
iDestruct (big_sepL_lookup _ _ _ _ Eqγi with "SS") as (ζi) "[sli sζi]".
......@@ -2447,10 +2434,10 @@ Proof.
destruct si as [| |[[vi Mi][Vi]]|[[vi Mi][Vi]]]; [done..| |].
- destruct (HENQ2 e vi Vi) as [(ev & EqeV & Eqev & _) _].
{ exists idx, Mi. apply get_enqInfo_L_enqueued. by rewrite Eqγi. }
apply (wkq_cons_enq_non_zero _ CON3 _ _ _ EqeV Eqev).
apply (bsq_cons_enq_non_zero _ CON3 _ _ _ EqeV Eqev).
- destruct (HENQ2 e vi Vi) as [(ev & EqeV & Eqev & _) _].
{ exists idx, Mi. eapply get_enqInfo_L_dequeued. by rewrite Eqγi. }
apply (wkq_cons_enq_non_zero _ CON3 _ _ _ EqeV Eqev). }
apply (bsq_cons_enq_non_zero _ CON3 _ _ _ EqeV Eqev). }
iExists ti0, LVs0', t1', LVs1'. rewrite shift_lblock_assoc Eqζi2 EqSH.
iFrame "Oi". iSplitR; first by iPureIntro.
iApply (view_at_mono with "OSi"); [done|].
......@@ -2493,7 +2480,7 @@ Proof.
destruct (HDEQ2 e) as [Inso _]. rewrite ->elem_of_list_fmap in Inso.
destruct Inso as [[e' d] [Eqe' Ind%elem_of_elements]].
- exists idx, v, Ve, Me, Vd. by rewrite Eqγi.
- simpl in Eqe'; subst e'. exists d. by rewrite -(wkq_cons_so_com _ CON3). }
- simpl in Eqe'; subst e'. exists d. by rewrite -(bsq_cons_so_com _ CON3). }
have Eqeix : Tx !! e = Some i.
{ apply (enq_map_enqueued_mono_inv _ _ ENTEx ENTE3 SubTx SubEx); [|done].
......@@ -2529,7 +2516,7 @@ Proof.
- destruct (HDEQ2 e) as [Ine _]. rewrite ->elem_of_list_fmap in Ine.
destruct Ine as ([e1 d2] & Eqe1 & Ined1%elem_of_elements).
{ exists idx. do 4 eexists. by rewrite Eqγi. }
simpl in Eqe1. subst e1. rewrite -(wkq_cons_so_com _ CON3). by exists d2.
simpl in Eqe1. subst e1. rewrite -(bsq_cons_so_com _ CON3). by exists d2.
} iClear "IH2".
destruct (toSlotHist_lookup_Some_None Fti NEqz2 Eqvi2 FRti2)
......@@ -2556,7 +2543,7 @@ Proof.
iPureIntro. rewrite Eqeidx in Eq2. clear -LeVr EqeV NIe Eq2.
inversion Eq2. by subst Vi Mi.
- rewrite view_at_view_at. iFrame "SL". }
assert (GtZ := wkq_cons_enq_non_zero _ CON3 _ _ _ Eqee EqeVv).
assert (GtZ := bsq_cons_enq_non_zero _ CON3 _ _ _ Eqee EqeVv).
have SubM : set_in_bound Mx' E3.
{ clear - SubMEx' SubEx. by eapply set_in_bound_mono. }
......@@ -2685,25 +2672,17 @@ Proof.
iDestruct "SE" as (i ? Mi Vi (Lei &?&?&?)) "_". iPureIntro. by eexists. }
have CON6' : G'.(so) = G'.(com).
{ rewrite EqSo' EqCo'. f_equal. apply (wkq_cons_so_com _ CON3). }
{ rewrite EqSo' EqCo'. f_equal. apply (bsq_cons_so_com _ CON3). }
have CON' : WeakQueueConsistent G'.
{ destruct CON3 as [CONW CONRel CONAcq CONNZ CON2 [CON3a CON3b] CON4
CON5 CON6 CON7a CON7b].
split.
- intros e0 eV0. case (decide (deqId = e0)) => ?.
+ subst e0. rewrite lookup_app_1_eq. inversion 1. simpl. intros _ ->.
{ destruct CON3 as [CONW CONRel CONAcq [CONNZ CON2 [CON3a CON3b] CON4
CON5 CON6 CON7a CON7b]].
constructor;[..|constructor].
- apply graph_insert_event_is_writing; [done|]. simpl. intros _ ->.
apply NEqV2. by apply : (anti_symm ()).
+ rewrite lookup_app_1_ne; [by apply CONW|done].
- intros e0 eV0. case (decide (deqId = e0)) => ?.
+ subst e0. clear; rewrite lookup_app_1_eq.
inversion 1; subst eV0. simpl; intros []; congruence.
+ rewrite lookup_app_1_ne; [by apply CONRel|done].
- intros e0 eV0. case (decide (deqId = e0)) => ?.
+ subst e0. rewrite lookup_app_1_eq. inversion 1; subst eV0; done.
+ rewrite lookup_app_1_ne; [by apply CONAcq|done].
- intros e0 eV0 v0. case (decide (deqId = e0)) => ?.
+ subst e0. rewrite lookup_app_1_eq. by inversion 1.
+ rewrite lookup_app_1_ne; [by apply CONNZ|done].
- clear -CONRel. apply graph_insert_event_is_releasing; [done|].
simpl; intros []; congruence.
- clear -CONAcq LeVw3. by apply graph_insert_event_is_acquiring.
- intros ??? [Eq1|[-> <-]]%lookup_app_1; [by apply (CONNZ _ _ _ Eq1)|done].
- (* 2 *)
move => e1 e2 /elem_of_union [/elem_of_singleton|InCom].
+ inversion 1. subst e1 e2. split; [done|].
......@@ -2745,14 +2724,7 @@ Proof.
destruct (CON5 _ _ EqeV EqED ee ve eVe Eqe Eqve Inee) as (de & InG4 & In').
exists de. split; [|done]. set_solver+InG4.
- (* 6 *) done.
- (* 7a MO *)
intros e1 e2 dV2. case (decide (e2 = deqId)) => [->|?].
+ rewrite lookup_app_1_eq => EqdV2. inversion EqdV2; clear EqdV2; subst dV2.
rewrite /= 2!elem_of_union elem_of_singleton. move => [InM1|[->//|IneV]].
* by apply Nat.lt_le_incl, lookup_lt_is_Some, SubM, InM1.
* by apply Nat.lt_le_incl, lookup_lt_is_Some,
(egcons_logview_closed _ EGCs3 _ _ Eqee _ IneV).
+ rewrite lookup_app_1_ne; [by apply CON7a|done].
- (* 7a MO *) clear -CON7a SUB'. by apply graph_insert_xo_eco.
- (* 7b *)
intros e1 eV1 v1 e2 d2 eV2 Eqe1 Eqv1. rewrite elem_of_union elem_of_singleton.
intros [Eq2|In2].
......
......@@ -29,7 +29,7 @@ Local Notation vProp := (vProp Σ).
Hypothesis stk : stack_per_elem_spec Σ.
(** Assuming logical-atomicity graph-based spec of Queue *)
Hypothesis msq : weak_queue_spec Σ.
Hypothesis msq : basic_queue_spec Σ.
(* Message Passing with stack and queue *)
Definition prog : expr :=
......@@ -172,7 +172,7 @@ Proof using All.
(-> & -> & Eqde & EsG' & SoG' & ComG' & EqM' & NInM').
rewrite QueueInv_QueueConsistent.
iDestruct "QI'" as ">%QC". exfalso.
destruct QC as [_ _ _ _ Hcom _ _ HNE HSoCom HBa HBb].
destruct QC as [_ Hcom _ _ HNE HSoCom HBa HBb].
have Eqd : G'.(Es) !! deqId = Some (mkGraphEvent EmpDeq Venq M').
{ by rewrite Eqde EsG' lookup_app_1_eq. }
have Ine' : e M'. { set_solver+EqM' Inm. }
......
......@@ -2207,18 +2207,33 @@ Proof.
assert (NI: e1 e2, (e1, e2) G2'.(com) e1 enqId e2 enqId).
{ clear. move => ?? /(gcons_com_included G2) [/=]. lia. }
have CON' : StrongQueueConsistent G2'.
{ destruct CON as [CONw CONRA CON1 CON2 CON3 CON4 CON5 CON6 CON7a CON7b].
split.
- intros e eV. case (decide (enqId = e)) => ?.
+ subst e. rewrite lookup_app_1_eq => [[<-]] ?. simpl. clear -LeV LeVs NEqV''.
intros ->. apply NEqV''. apply : (anti_symm ()); [done|solve_lat].
+ rewrite lookup_app_1_ne; [by apply CONw|done].
- intros e eV. case (decide (enqId = e)) => ?.
+ subst e. by rewrite lookup_app_1_eq => [[<-]].
+ rewrite lookup_app_1_ne; [by apply CONRA|done].
- intros e' eV' v'. case (decide (enqId = e')) => ?.
+ subst e'. by rewrite lookup_app_1_eq => [[<-]] /= [<-//].
+ rewrite lookup_app_1_ne; [by apply CON1|done].
{ destruct CON as [CONRA [CONw _ _ CON] CON7b].
have CONRA' : graph_event_is_relacq G2'.(Es) (λ _, True).
{ clear -CONRA. by apply graph_insert_event_is_relacq. }
have FIFO' : queue_FIFO_strong G2'.
{ (* 7b *)
intros e1 v1 eV1 e2 d2 Eqe1 Eqv1 InG2 Le12.
rewrite lookup_app_1_ne in Eqe1.
+ apply (CON7b _ _ _ _ _ Eqe1 Eqv1 InG2 Le12).
+ intros ->. rewrite EqCo' in InG2.
apply (Nat.lt_irrefl enqId), (Nat.le_lt_trans _ e2 _ Le12),
(gcons_com_included _ _ InG2). }
constructor; [done| |done]. constructor.
{ clear -LeV LeVs NEqV'' CONw. apply graph_insert_event_is_writing; [done|].
simpl. intros _ ->. apply NEqV''. apply : (anti_symm ()); [done|solve_lat]. }
{ by apply graph_event_is_relacq_releasing_True. }
{ by apply graph_event_is_relacq_acquiring_True. }
destruct CON as [CON0 CON2 CON3 CON4 CON5 CON6 CON7a _].
have EC' : graph_xo_eco G2'.(Es).
{ (* 7a *)
intros e1 e2 eV2 [Eq1|[-> <-]]%lookup_app_1.
+ by apply CON7a.
+ move => /= /Sub'. clear. intros Lt%lookup_lt_is_Some.
rewrite app_length /= in Lt. lia. }
constructor; [..|done|].
- (* 1 *)
intros ??? [Eq1|[-> <-]]%lookup_app_1; [by apply (CON0 _ _ _ Eq1)|].
by move => /= [<-//].
- (* 2 *)
intros e1 e2 InG. destruct (NI _ _ InG).
do 2 (rewrite lookup_app_1_ne; [|done]). by apply CON2.
......@@ -2235,20 +2250,7 @@ Proof.
intros ->. apply (egcons_logview_closed _ EGCs _ _ Eqe),
lookup_lt_is_Some in Inee. clear -Inee. lia.
- (* 6 *) done.
- (* 7a *)
intros e1 e2 eV2.
case (decide (enqId = e2)) => NEq2;
[subst e2; rewrite lookup_app_1_eq|rewrite lookup_app_1_ne //].
+ move => [<-] /= /Sub'. clear. intros Lt%lookup_lt_is_Some.
rewrite app_length /= in Lt. lia.
+ by apply CON7a.
- (* 7b *)
intros e1 v1 eV1 e2 d2 Eqe1 Eqv1 InG2 Le12.
rewrite lookup_app_1_ne in Eqe1.
+ apply (CON7b _ _ _ _ _ Eqe1 Eqv1 InG2 Le12).
+ intros ->. rewrite EqCo' in InG2.
apply (Nat.lt_irrefl enqId), (Nat.le_lt_trans _ e2 _ Le12),
(gcons_com_included _ _ InG2). }
- (* 7a *) by apply queue_FIFO_strong_FIFO. }
(* COMMIT the AU *)
rewrite bi.and_elim_r.
......@@ -2607,7 +2609,7 @@ Proof.
destruct (lookup_lt_is_Some_2 (De.*1 ++ [η2]) j) as [η Eqη].
{ rewrite EQL. apply (lookup_lt_Some _ _ _ Eqde). }
destruct (InG3 _ _ _ Eqη Eqde) as (e & Eqe & InG3c).
destruct (strq_cons_matches _ CON _ _ InG3c)
destruct (bsq_cons_matches _ CON _ _ InG3c)
as (? & eV & dV & ve & ? & EqdVe & ? & ? & ?). by exists dV, ve. }
(* Commit AU with an EMPTY event, commiting point is the read. *)
......@@ -2630,18 +2632,33 @@ Proof.
assert (NI: e1 e2, (e1, e2) G'.(com) e1 deqId e2 deqId).
{ move => ?? /(gcons_com_included G3) [/=]. lia. }
have CON' : StrongQueueConsistent G'.
{ destruct CON as [CONw CONRA CON1 CON2 CON3 CON4 CON5 CON6 CON7a CON7b].
split.
- intros e eV. case (decide (deqId = e)) => ?.
+ subst e. by rewrite lookup_app_1_eq => [[<-]].
+ rewrite lookup_app_1_ne; [by apply CONw|done].
- intros e eV. case (decide (deqId = e)) => ?.
+ subst e. by rewrite lookup_app_1_eq => [[<-//]].
+ rewrite lookup_app_1_ne; [by apply CONRA|done].
{ destruct CON as [CONRA [CONw _ _ CON] CON7b].
have CONRA' : graph_event_is_relacq G'.(Es) (λ _, True).
{ clear -CONRA. by apply graph_insert_event_is_relacq. }
have FIFO' : queue_FIFO_strong G'.
{ (* 7b *)
intros e1 v1 eV1 e2 d2 Eqe1 Eqv1 InG2 Le12.
rewrite lookup_app_1_ne in Eqe1.
+ apply (CON7b _ _ _ _ _ Eqe1 Eqv1 InG2 Le12).
+ intros ->. rewrite /= in InG2.
apply (Nat.lt_irrefl deqId), (Nat.le_lt_trans _ e2 _ Le12),
(gcons_com_included _ _ InG2). }
constructor; [done| |done]. constructor.
{ clear -CONw. by apply graph_insert_event_is_writing. }
{ by apply graph_event_is_relacq_releasing_True. }
{ by apply graph_event_is_relacq_acquiring_True. }
destruct CON as [CON1 CON2 CON3 CON4 CON5 CON6 CON7a _].
have EC' : graph_xo_eco G'.(Es).
{ (* 7a *)
intros e1 e2 eV2 [Eq1|[-> <-]]%lookup_app_1.
+ by apply CON7a.
+ rewrite /= elem_of_union !elem_of_singleton.
intros [?|Inm]; [by subst e1|].
apply Nat.lt_le_incl, lookup_lt_is_Some, SubMMe, Inm. }
constructor; [..|done|].
- (* 1 *)
intros e0 eV0 v0. case (decide (deqId = e0)) => ?.
+ subst e0. by rewrite lookup_app_1_eq => [[<-//]].
+ rewrite lookup_app_1_ne; [by apply CON1|done].
intros e0 eV0 v0 [Eq1|[-> <-]]%lookup_app_1;
[by apply (CON1 _ _ _ Eq1)|done].
- (* 2 *)
intros e1 d2 In1. destruct (NI _ _ In1).
do 2 (rewrite lookup_app_1_ne; [|done]). by apply CON2.
......@@ -2770,21 +2787,7 @@ Proof.
destruct Eqv2 as [? ?%Eqvn2]. by simplify_eq.
+ intros _. exfalso. by apply (NSM _ InCIT1), strict_subseq_adjacent_in.
- (* 6 *) done.
- (* 7a *)
intros e1 e2 eV2.
case (decide (deqId = e2)) => NEq2;
[subst e2; rewrite lookup_app_1_eq|rewrite lookup_app_1_ne //].
+ move => [<-] /=. rewrite elem_of_union !elem_of_singleton.
intros [?|Inm]; [by subst e1|].
apply Nat.lt_le_incl, lookup_lt_is_Some, SubMMe, Inm.
+ by apply CON7a.
- (* 7b *)
intros e1 v1 eV1 e2 d2 Eqe1 Eqv1 InG2 Le12.
rewrite lookup_app_1_ne in Eqe1.
+ apply (CON7b _ _ _ _ _ Eqe1 Eqv1 InG2 Le12).
+ intros ->. rewrite /= in InG2.
apply (Nat.lt_irrefl deqId), (Nat.le_lt_trans _ e2 _ Le12),
(gcons_com_included _ _ InG2). }
- (* 7a *) by apply queue_FIFO_strong_FIFO. }
have CDT' : EM_equiv T3 E'.
{ intros e. rewrite CDT. split; intros [v Eqv].
......@@ -3081,8 +3084,6 @@ Proof.
by iPureIntro. }
assert (EEq := prefix_lookup _ _ _ _ EqeV3 SubE3).
destruct CON as [CONw CONRA CON0 CON2 [CON3a CON3b] CON4
CON5 CON6 CON7a CON7b].
destruct QP4 as [ND DT CDT InjT ET MONO ORD].
set enqId := en2.
......@@ -3101,7 +3102,7 @@ Proof.
split; [done|]. rewrite -LeDL3. by left. }
(* we know that 0 < ve2 *)
assert (NZ := CON0 _ _ _ EEq Eqve2).
assert (NZ := bsq_cons_enq_non_zero _ CON _ _ _ EEq Eqve2).
assert (SubeV := egcons_logview_closed _ EGCs _ _ EEq).
have SubM4: set_in_bound M E4. { clear -SubM SubE3. by eapply set_in_bound_mono. }
......@@ -3128,67 +3129,12 @@ Proof.
- exists L4'. apply prefix_cons_inv_1 in LeDL3. by subst. }
have CON' : StrongQueueConsistent G'.
{ split.
- intros e0 eV0. case (decide (deqId = e0)) => [<-|?].
+ rewrite lookup_app_1_eq => [[<-]] ? /=. clear -SubV5 LeV5 NEqV5'.
intros ->. apply NEqV5'. apply : (anti_symm ()); [done|solve_lat].
+ rewrite lookup_app_1_ne; [by apply CONw|done].
- intros e0 eV0. case (decide (deqId = e0)) => [<-|?].
+ by rewrite lookup_app_1_eq => [[<-//]].
+ rewrite lookup_app_1_ne; [by apply CONRA|done].
- (* 0 *)
intros e0 eV0 v0. case (decide (deqId = e0)) => [<-|?].
+ by rewrite lookup_app_1_eq => [[<-//]].
+ rewrite lookup_app_1_ne; [by apply CON0|done].
- (* 2 *)
move => e1 e2 /elem_of_union [/elem_of_singleton|InCom].
+ inversion 1. subst e1 e2. split; [done|].
exists eV. eexists. exists ve2.
by rewrite (prefix_lookup _ _ _ _ EEq LeE') lookup_app_1_eq /= Eqve2.
+ destruct (NI _ _ InCom). do 2 (rewrite lookup_app_1_ne; [|done]).
by apply CON2.
- split.
+ (* 3a *)
intros [e1 d1] [e2 d2]. rewrite 2!elem_of_union 2!elem_of_singleton /=.
move => [[-> ->]|InG1] [[-> ->]|InG2] //.