diff --git a/exercises/ex_03_spinlock.v b/exercises/ex_03_spinlock.v
index d2d6d67ff40475cfa716d0f33609a75394998d64..5cc7f2fcb2decee1aa359a3275dc9236f65502a5 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 3afcb906423bf7880f41298d096df4edc8736e01..c562a7fb7348ffa362bf7d557bdf92622b4c6bb2 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 206e61170902a104e91bb1730c6a832f4b089b9f..40eb712f4f9de88cde36ba819d8e3c294270283b 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