From a766f3d6ce912cd4f2a6d2e20e8645a33e2df005 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 24 Jun 2019 15:31:43 +0200 Subject: [PATCH] bump Iris (CmpXchg change) --- exercises/ex_03_spinlock.v | 9 +++++++-- opam | 2 +- solutions/ex_03_spinlock.v | 13 +++++++++---- 3 files changed, 17 insertions(+), 7 deletions(-) diff --git a/exercises/ex_03_spinlock.v b/exercises/ex_03_spinlock.v index d2d6d67..5cc7f2f 100644 --- a/exercises/ex_03_spinlock.v +++ b/exercises/ex_03_spinlock.v @@ -27,6 +27,8 @@ multiple threads could try to acquire the lock at the same time, we use the if the value of the reference [l] is equal to [v], and if so, changes it into [w] and returns [true]. If the value of [l] is unequal to [v], it leaves the value of [l] as if, and returns [false]. +[CAS l v w] is actually a short-hand for [Snd (CmpXchg l v w)], where [CmpXchg] +also returns the old value in [l] before the operation took place. *) (** @@ -83,6 +85,9 @@ Section proof. Proof. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv". wp_rec. + (** We have to "focus on" the atomic [CmpXchg] operation before we can + open the invariant. *) + wp_bind (CmpXchg _ _ _). (** Using the tactic [iInv] we open the invariant. *) iInv lockN as (b) "[Hl HR]" "Hclose". (** The post-condition of the WP is augmented with an *update* modality @@ -94,9 +99,9 @@ Section proof. *) destruct b. - - wp_cas_fail. iMod ("Hclose" with "[Hl]") as "_". + - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_". { iNext. iExists true. iFrame. } - iModIntro. (* exercise *) + iModIntro. wp_proj. (* exercise *) Admitted. (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive diff --git a/opam b/opam index 3afcb90..c562a7f 100644 --- a/opam +++ b/opam @@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] install: [] # This repo does not install remove: [] depends: [ - "coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") } + "coq-iris" { (= "dev.2019-06-24.3.5ef58527") | (= "dev") } ] diff --git a/solutions/ex_03_spinlock.v b/solutions/ex_03_spinlock.v index 206e611..40eb712 100644 --- a/solutions/ex_03_spinlock.v +++ b/solutions/ex_03_spinlock.v @@ -27,6 +27,8 @@ multiple threads could try to acquire the lock at the same time, we use the if the value of the reference [l] is equal to [v], and if so, changes it into [w] and returns [true]. If the value of [l] is unequal to [v], it leaves the value of [l] as if, and returns [false]. +[CAS l v w] is actually a short-hand for [Snd (CmpXchg l v w)], where [CmpXchg] +also returns the old value in [l] before the operation took place. *) (** @@ -83,6 +85,9 @@ Section proof. Proof. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv". wp_rec. + (** We have to "focus on" the atomic [CmpXchg] operation before we can + open the invariant. *) + wp_bind (CmpXchg _ _ _). (** Using the tactic [iInv] we open the invariant. *) iInv lockN as (b) "[Hl HR]" "Hclose". (** The post-condition of the WP is augmented with an *update* modality @@ -94,13 +99,13 @@ Section proof. *) destruct b. - - wp_cas_fail. iMod ("Hclose" with "[Hl]") as "_". + - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_". { iNext. iExists true. iFrame. } - iModIntro. iApply ("HΦ" \$! false). done. - - (* Exercise *) wp_cas_suc. + iModIntro. wp_proj. iApply ("HΦ" \$! false). done. + - (* Exercise *) wp_cmpxchg_suc. iMod ("Hclose" with "[Hl]") as "_". { iNext. iExists true. iFrame. } - iModIntro. by iApply ("HΦ" \$! true with "HR"). + iModIntro. wp_proj. by iApply ("HΦ" \$! true with "HR"). Qed. (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive -- GitLab