Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Tutorial POPL18
Commits
a766f3d6
Commit
a766f3d6
authored
Jun 24, 2019
by
Ralf Jung
Browse files
bump Iris (CmpXchg change)
parent
638eac93
Pipeline
#18105
passed with stage
in 8 minutes and 43 seconds
Changes
3
Pipelines
9
Hide whitespace changes
Inline
Sidebyside
exercises/ex_03_spinlock.v
View file @
a766f3d6
...
...
@@ 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 shorthand 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 postcondition of the WP is augmented with an *update* modality
...
...
@@ 94,9 +99,9 @@ Section proof.
*)
destruct
b
.

wp_c
as
_fail
.
iMod
(
"Hclose"
with
"[Hl]"
)
as
"_"
.

wp_c
mpxchg
_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
...
...
opam
View file @
a766f3d6
...
...
@@ 9,5 +9,5 @@ build: [make "j%{jobs}%"]
install: [] # This repo does not install
remove: []
depends: [
"coqiris" { (= "dev.201906
18.2.e039d7c
7")  (= "dev") }
"coqiris" { (= "dev.201906
24.3.5ef5852
7")  (= "dev") }
]
solutions/ex_03_spinlock.v
View file @
a766f3d6
...
...
@@ 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 shorthand 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 postcondition of the WP is augmented with an *update* modality
...
...
@@ 94,13 +99,13 @@ Section proof.
*)
destruct
b
.

wp_c
as
_fail
.
iMod
(
"Hclose"
with
"[Hl]"
)
as
"_"
.

wp_c
mpxchg
_fail
.
iMod
(
"Hclose"
with
"[Hl]"
)
as
"_"
.
{
iNext
.
iExists
true
.
iFrame
.
}
iModIntro
.
iApply
(
"HΦ"
$!
false
).
done
.

(* Exercise *)
wp_c
as
_suc
.
iModIntro
.
wp_proj
.
iApply
(
"HΦ"
$!
false
).
done
.

(* Exercise *)
wp_c
mpxchg
_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
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment