From 38b54f0da699996831e0851af2d3c7325e6afddb Mon Sep 17 00:00:00 2001 From: Shengyi Wang Date: Fri, 14 Jan 2022 15:31:03 +0800 Subject: [PATCH] 1. Permit Coq 8.15.0 in Makefile 2. Make the concurrency part compatible with Coq 8.15.0 --- Makefile | 2 +- atomics/general_locks.v | 14 ++++---- atomics/hashtable.v | 2 +- atomics/verif_hashtable_atomic.v | 59 ++++++++++++++++++++------------ concurrency/invariants.v | 8 ++--- 5 files changed, 51 insertions(+), 34 deletions(-) diff --git a/Makefile b/Makefile index a188a13a67..533fcbd8ae 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/') # Check Coq version -COQVERSION= 8.13.0 or-else 8.13.1 or-else 8.13.2 or-else 8.14.0 or-else 8.14.1 +COQVERSION= 8.13.0 or-else 8.13.1 or-else 8.13.2 or-else 8.14.0 or-else 8.14.1 or-else 8.15.0 COQV=$(shell $(COQC) -v) ifneq ($(IGNORECOQVERSION),true) diff --git a/atomics/general_locks.v b/atomics/general_locks.v index dd3a8ba7c3..5c72a05ebc 100644 --- a/atomics/general_locks.v +++ b/atomics/general_locks.v @@ -105,7 +105,7 @@ Lemma sync_commit_gen : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> m (atomic_shift a Ei Eo b Q * my_half g sh x0 * R |-- |==> EX y, Q y * R' y)%I. Proof. intros; rewrite sepcon_assoc. - apply atomic_commit with (R'0 := fun y => R' y). + apply (@atomic_commit CS) with (R' := fun y => R' y). intros; iIntros "((my & R) & a)". iMod (Ha with "[$]") as (?) "[public a']". iPoseProof (ref_sub(P := P) with "[$my $public]") as "%". @@ -120,7 +120,7 @@ Lemma sync_commit_same : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> (atomic_shift a Ei Eo b Q * my_half g sh x0 * R |-- |==> EX y, Q y * R' y)%I. Proof. intros; rewrite sepcon_assoc. - apply atomic_commit with (R'0 := fun y => R' y). + apply (@atomic_commit CS) with (R' := fun y => R' y). intros; iIntros "((my & R) & a)". iMod (Ha with "[$]") as (?) "[public a']". iPoseProof (ref_sub(P := P) with "[$my $public]") as "%". @@ -133,7 +133,8 @@ Lemma sync_commit_gen1 : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> |==> (EX x0' x1' : G, !!(forall b, sepalg.join x0 b x1 -> sepalg.join x0' b x1') && (my_half g sh x0' * public_half g x1' -* |==> (EX y, b x y) * R')))%I)%I), (atomic_shift a Ei Eo b (fun _ => Q) * my_half g sh x0 * R |-- |==> Q * R')%I. Proof. - intros; rewrite sepcon_assoc; eapply derives_trans; [apply atomic_commit with (R'0 := fun _ => R')|]. + intros; rewrite sepcon_assoc; eapply derives_trans; [apply (@atomic_commit CS) with + (R' := fun _ => R')|]. - intros; iIntros "((my & R) & a)". iMod (Ha with "[$]") as (?) "[public a']". iPoseProof (ref_sub(P := P) with "[$my $public]") as "%". @@ -149,7 +150,8 @@ Lemma sync_commit_same1 : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> |==> (my_half g sh x0 * public_half g x1 -* |==> (EX y, b x y * R')))%I)%I), (atomic_shift a Ei Eo b (fun _ => Q) * my_half g sh x0 * R |-- |==> Q * R')%I. Proof. - intros; rewrite sepcon_assoc; eapply derives_trans; [apply atomic_commit with (R'0 := fun _ => R')|]. + intros; rewrite sepcon_assoc; eapply derives_trans; [apply (@atomic_commit CS) with + (R' := fun _ => R')|]. intros; iIntros "((my & R) & a)". iMod (Ha with "[$]") as (?) "[public a']". iPoseProof (ref_sub(P := P) with "[$my $public]") as "%". @@ -197,7 +199,7 @@ Lemma two_sync_commit : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> m (atomic_shift a Ei Eo b Q * my_half g1 sh1 x1 * my_half g2 sh2 x2 * R |-- |==> EX y, Q y * R' y)%I. Proof. intros; rewrite -> 2sepcon_assoc. - apply atomic_commit with (R'0 := fun y => R' y). + apply (@atomic_commit CS) with (R' := fun y => R' y). intros; iIntros "((my1 & my2 & R) & a)". iMod (Ha with "[$]") as (??) "((public1 & public2) & a')". iPoseProof (ref_sub(P := P) with "[$my1 $public1]") as "%". @@ -217,7 +219,7 @@ Lemma two_sync_commit1 : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> (atomic_shift a Ei Eo b (fun _ => Q) * my_half g1 sh1 x1 * my_half g2 sh2 x2 * R |-- |==> Q * R')%I. Proof. intros; rewrite -> 2sepcon_assoc. - eapply derives_trans; [apply atomic_commit with (R'0 := fun _ => R')|]. + eapply derives_trans; [apply (@atomic_commit CS) with (R' := fun _ => R')|]. intros; iIntros "((my1 & my2 & R) & a)". iMod (Ha with "[$]") as (??) "((public1 & public2) & a')". iPoseProof (ref_sub(P := P) with "[$my1 $public1]") as "%". diff --git a/atomics/hashtable.v b/atomics/hashtable.v index ffc96302ea..d77574c16e 100644 --- a/atomics/hashtable.v +++ b/atomics/hashtable.v @@ -419,7 +419,7 @@ Proof. intro Heq; apply In_Znth in Hin' as (i & Hi & ?); subst x. rewrite Zlength_sublist in Hi; try lia. rewrite Znth_sublist, Znth_rebase, Z.add_0_r in Heq by lia. - eapply NoDup_Znth_inj with (i0 := z)(j := (i + hash k) mod (Zlength m)) in Hwf. + eapply @NoDup_Znth_inj with (i := z)(j := (i + hash k) mod (Zlength m)) in Hwf. subst z. rewrite Zminus_mod_idemp_l, Z.add_simpl_r, Z.sub_0_r, Zmod_small in Hi; try lia. * destruct Hi; split; auto. diff --git a/atomics/verif_hashtable_atomic.v b/atomics/verif_hashtable_atomic.v index 470711c6f9..db8288891e 100644 --- a/atomics/verif_hashtable_atomic.v +++ b/atomics/verif_hashtable_atomic.v @@ -318,8 +318,9 @@ Proof. { rewrite <- Hi1; intro Heq. apply Zmod_plus_inv in Heq; [|apply size_pos]. rewrite !Zmod_small in Heq; lia. } - rewrite -> iter_sepcon_Znth_remove with (i0 := (j + hash k) mod size), - iter_sepcon_Znth' with (i0 := j)(l := upto _) + rewrite -> @iter_sepcon_Znth_remove with (d := Inhabitant_Z) + (i := (j + hash k) mod size), + @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := j)(l := upto _) by (auto; rewrite -> Zlength_upto, Z2Nat.id; try lia). rewrite -> !Znth_upto by (rewrite -> Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -330,7 +331,7 @@ Proof. rewrite <- !sepcon_assoc, snap_master_join1 by auto. Intros; apply prop_right; simpl. eapply Forall_Znth in Hfail. - rewrite -> Znth_sublist, Z.add_0_r, Znth_rebase with (i0 := j) in Hfail; auto; try lia. + rewrite -> Znth_sublist, Z.add_0_r, @Znth_rebase with (i := j) in Hfail; auto; try lia. replace (Zlength keys) with size in Hfail; intuition; subst; intuition. { rewrite -> Zlength_sublist; auto; try lia. rewrite Zlength_rebase; lia. } @@ -434,7 +435,7 @@ Proof. iIntros "([AS1 _] & P)". iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". - rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size) + rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size) by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia). erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -497,7 +498,9 @@ Proof. iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size) + (f := hashtable_entry _ _ _) by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; try lia). erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -522,7 +525,8 @@ Proof. iFrame "snap snaps". iDestruct "Hclose" as "[Hclose _]"; iApply "Hclose". unfold hashtable; iExists (upd_Znth (i1 mod size) T (if eq_dec ki 0 then k else ki, vi)); iFrame "excl". - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size) + (l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -558,7 +562,7 @@ Proof. iIntros "(([AS1 _] & snap) & P)". iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". - rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size) + rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size) by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia). erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -613,7 +617,8 @@ Proof. iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(f := hashtable_entry _ _ _) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -634,7 +639,8 @@ Proof. unfold hashtable. iFrame. iExists (upd_Znth (i1 mod size) T (k, v)). - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -726,7 +732,8 @@ Proof. iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(f := hashtable_entry _ _ _) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -753,7 +760,8 @@ Proof. rewrite Hindex; congruence. } unfold hashtable; iExists T. iSplitL ""; [auto|]. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -762,7 +770,8 @@ Proof. iFrame "snap snaps". iDestruct "Hclose" as "[Hclose _]"; iApply "Hclose". unfold hashtable; iExists T. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -778,7 +787,8 @@ Proof. iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(f := hashtable_entry _ _ _) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -812,7 +822,8 @@ Proof. rewrite HHi; auto. } unfold hashtable; iExists T. iSplitL ""; [iSplit; auto; iPureIntro; split; auto; tauto|]. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -919,7 +930,7 @@ Proof. iIntros "([AS1 _] & P)". iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". - rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size) + rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size) by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia). erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -983,7 +994,8 @@ Proof. iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) + (i := i1 mod size)(f := hashtable_entry _ _ _) by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; try lia). erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -1008,7 +1020,8 @@ Proof. iFrame "snap snaps". iDestruct "Hclose" as "[Hclose _]"; iApply "Hclose". unfold hashtable; iExists (upd_Znth (i1 mod size) T (if eq_dec ki 0 then k else ki, vi)); iFrame "excl". - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size) + (l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -1042,7 +1055,7 @@ Proof. iIntros "(([AS1 _] & snap) & P)". iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". - rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size) + rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size) by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia). erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -1099,7 +1112,8 @@ Proof. iMod ("AS1" with "P") as (HT) "[hashtable Hclose]". iDestruct "hashtable" as (T) "((% & excl) & entries)". match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end. - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size) + (f := hashtable_entry _ _ _) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia). unfold hashtable_entry at 1. @@ -1124,7 +1138,8 @@ Proof. unfold hashtable. rewrite exp_andp2. iExists ((if eq_dec vi 0 then upd_Znth (i1 mod size) T (k, v) else T)). - rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size)) + rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size) + (l := upto (Z.to_nat size)) by (rewrite -> Zlength_upto, Z2Nat.id; lia). rewrite -> Znth_upto by (rewrite Z2Nat.id; lia). unfold hashtable_entry. @@ -1857,7 +1872,7 @@ Proof. destruct (eq_dec j i). + subst; rewrite -> upd_Znth_same by auto; apply derives_refl. + rewrite -> upd_Znth_diff by auto. - setoid_rewrite Znth_repeat with (n0 := 3%nat); apply stronger_default_val. } + setoid_rewrite @Znth_repeat with (n := 3%nat); apply stronger_default_val. } rewrite <- !sepcon_assoc, (sepcon_comm _ (data_at (Znth i shs) _ _ (gv _results))), !sepcon_assoc; apply sepcon_derives. { apply stronger_array_ext. @@ -1866,7 +1881,7 @@ Proof. destruct (eq_dec j i). + subst; rewrite -> upd_Znth_same by auto; apply derives_refl. + rewrite -> upd_Znth_diff' by auto. - setoid_rewrite Znth_repeat with (n0 := 3%nat); apply stronger_default_val. } + setoid_rewrite @Znth_repeat with (n := 3%nat); apply stronger_default_val. } erewrite sublist_next by (auto; lia); simpl; fast_cancel. { intro; subst; contradiction unreadable_bot. eapply join_readable1, readable_share_list_join; eauto. } } diff --git a/concurrency/invariants.v b/concurrency/invariants.v index 147a8d6793..b3ad2fd117 100644 --- a/concurrency/invariants.v +++ b/concurrency/invariants.v @@ -215,7 +215,7 @@ Proof. destruct b. erewrite ghost_list_nth with (n := i) by (erewrite nth_map' with (d' := None), Hi'; eauto; lia). iDestruct "dis" as "[token dis]". - rewrite -> iter_sepcon_eq, iter_sepcon_Znth with (i0 := Z.of_nat i) + rewrite -> @iter_sepcon_eq, iter_sepcon_Znth with (i := Z.of_nat i) by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia). erewrite Znth_upto, Hi by lia. iDestruct "I" as "((agree' & HP) & I)". @@ -244,7 +244,7 @@ Proof. + destruct (eq_dec x i); [subst; right; constructor | left]. unfold Ensembles.In in *. rewrite nth_replace_nth' in X; auto. - - erewrite iter_sepcon_Znth with (i0 := Z.of_nat i)(l0 := upto _) + - erewrite @iter_sepcon_Znth with (i := Z.of_nat i)(l := upto _) by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia). erewrite Znth_upto, Znth_replace_nth by lia; iFrame. erewrite iter_sepcon_func_strong; auto. @@ -322,9 +322,9 @@ Proof. * intro X'; inv X'. unfold Ensembles.In in X. rewrite -> nth_replace_nth in X by lia; inv X. - - erewrite !iter_sepcon_eq, iter_sepcon_Znth with (i0 := Z.of_nat i) + - erewrite !iter_sepcon_eq, @iter_sepcon_Znth with (i := Z.of_nat i) by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia). - erewrite iter_sepcon_Znth with (i0 := Z.of_nat i)(l0 := upto _) + erewrite @iter_sepcon_Znth with (i := Z.of_nat i)(l := upto _) by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia). erewrite !Znth_upto, !Znth_replace_nth by lia. rewrite Hi.