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
Rice Wine
Iris
Commits
c24ee497
Commit
c24ee497
authored
Dec 06, 2016
by
Ralf Jung
Browse files
Revert "use lock-based opaqueness for everything in heap_lang"
This reverts commit
b115ff3f
.
parent
6e00aa34
Changes
6
Hide whitespace changes
Inline
Side-by-side
heap_lang/lib/assert.v
View file @
c24ee497
...
...
@@ -4,13 +4,15 @@ From iris.proofmode Require Import tactics.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
Definition
assert
:
val
:
=
locked
(
λ
:
"v"
,
if
:
"v"
#()
then
#()
else
#
0
#
0
)%
V
.
(* #0 #0 is unsafe *)
λ
:
"v"
,
if
:
"v"
#()
then
#()
else
#
0
#
0
.
(* #0 #0 is unsafe *)
(* just below ;; *)
Notation
"'assert:' e"
:
=
(
assert
(
λ
:
<>,
e
))%
E
(
at
level
99
)
:
expr_scope
.
Lemma
wp_assert
`
{
heapG
Σ
}
E
(
Φ
:
val
→
iProp
Σ
)
e
`
{!
Closed
[]
e
}
:
WP
e
@
E
{{
v
,
⌜
v
=
#
true
⌝
∧
▷
Φ
#()
}}
⊢
WP
assert
:
e
@
E
{{
Φ
}}.
Proof
.
iIntros
"HΦ"
.
rewrite
/
assert
-
lock
.
wp_let
.
wp_seq
.
iIntros
"HΦ"
.
rewrite
/
assert
.
wp_let
.
wp_seq
.
iApply
(
wp_wand
with
"HΦ"
).
iIntros
(
v
)
"[% ?]"
;
subst
.
by
wp_if
.
Qed
.
Global
Opaque
assert
.
heap_lang/lib/barrier/barrier.v
View file @
c24ee497
From
iris
.
heap_lang
Require
Export
notation
.
Definition
newbarrier
:
val
:
=
locked
(
λ
:
<>,
ref
#
false
)%
V
.
Definition
signal
:
val
:
=
locked
(
λ
:
"x"
,
"x"
<-
#
true
)%
V
.
Definition
newbarrier
:
val
:
=
λ
:
<>,
ref
#
false
.
Definition
signal
:
val
:
=
λ
:
"x"
,
"x"
<-
#
true
.
Definition
wait
:
val
:
=
locked
(
rec
:
"wait"
"x"
:
=
if
:
!
"x"
then
#()
else
"wait"
"x"
)%
V
.
rec
:
"wait"
"x"
:
=
if
:
!
"x"
then
#()
else
"wait"
"x"
.
Global
Opaque
newbarrier
signal
wait
.
heap_lang/lib/barrier/proof.v
View file @
c24ee497
...
...
@@ -22,6 +22,8 @@ Section proof.
Context
`
{!
heapG
Σ
,
!
barrierG
Σ
}
(
N
:
namespace
).
Implicit
Types
I
:
gset
gname
.
Local
Transparent
newbarrier
signal
wait
.
Definition
ress
(
P
:
iProp
Σ
)
(
I
:
gset
gname
)
:
iProp
Σ
:
=
(
∃
Ψ
:
gname
→
iProp
Σ
,
▷
(
P
-
∗
[
∗
set
]
i
∈
I
,
Ψ
i
)
∗
[
∗
set
]
i
∈
I
,
saved_prop_own
i
(
Ψ
i
))%
I
.
...
...
@@ -95,7 +97,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
{{{
heap_ctx
}}}
newbarrier
#()
{{{
l
,
RET
#
l
;
recv
l
P
∗
send
l
P
}}}.
Proof
.
iIntros
(
HN
Φ
)
"#? HΦ"
.
rewrite
-
wp_fupd
/
newbarrier
-
lock
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
rewrite
-
wp_fupd
/
newbarrier
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iApply
(
"HΦ"
with
">[-]"
).
iMod
(
saved_prop_alloc
(
F
:
=
idCF
)
P
)
as
(
γ
)
"#?"
.
iMod
(
sts_alloc
(
barrier_inv
l
P
)
_
N
(
State
Low
{[
γ
]})
with
"[-]"
)
...
...
@@ -119,7 +121,7 @@ Qed.
Lemma
signal_spec
l
P
:
{{{
send
l
P
∗
P
}}}
signal
#
l
{{{
RET
#()
;
True
}}}.
Proof
.
rewrite
/
signal
/
send
/
barrier_ctx
-
lock
/=.
rewrite
/
signal
/
send
/
barrier_ctx
/=.
iIntros
(
Φ
)
"(Hs&HP) HΦ"
;
iDestruct
"Hs"
as
(
γ
)
"[#(%&Hh&Hsts) Hγ]"
.
wp_let
.
iMod
(
sts_openS
(
barrier_inv
l
P
)
_
_
γ
with
"[Hγ]"
)
as
([
p
I
])
"(% & [Hl Hr] & Hclose)"
;
eauto
.
...
...
heap_lang/lib/par.v
View file @
c24ee497
...
...
@@ -5,11 +5,11 @@ Import uPred.
Definition
parN
:
namespace
:
=
nroot
.@
"par"
.
Definition
par
:
val
:
=
locked
(
λ
:
"fs"
,
λ
:
"fs"
,
let
:
"handle"
:
=
spawn
(
Fst
"fs"
)
in
let
:
"v2"
:
=
Snd
"fs"
#()
in
let
:
"v1"
:
=
join
"handle"
in
(
"v1"
,
"v2"
)
)%
V
.
(
"v1"
,
"v2"
).
Notation
"e1 ||| e2"
:
=
(
par
(
Pair
(
λ
:
<>,
e1
)
(
λ
:
<>,
e2
)))%
E
:
expr_scope
.
Section
proof
.
...
...
@@ -26,7 +26,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
⊢
WP
par
e
{{
Φ
}}.
Proof
.
iIntros
(?)
"(#Hh&Hf1&Hf2&HΦ)"
.
rewrite
/
par
-
lock
.
wp_value
.
wp_let
.
wp_proj
.
rewrite
/
par
.
wp_value
.
wp_let
.
wp_proj
.
wp_apply
(
spawn_spec
parN
with
"[$Hh $Hf1]"
)
;
try
wp_done
;
try
solve_ndisj
.
iIntros
(
l
)
"Hl"
.
wp_let
.
wp_proj
.
wp_bind
(
f2
_
).
iApply
(
wp_wand
with
"Hf2"
)
;
iIntros
(
v
)
"H2"
.
wp_let
.
...
...
heap_lang/lib/spawn.v
View file @
c24ee497
...
...
@@ -5,15 +5,15 @@ From iris.heap_lang Require Import proofmode notation.
From
iris
.
algebra
Require
Import
excl
.
Definition
spawn
:
val
:
=
locked
(
λ
:
"f"
,
λ
:
"f"
,
let
:
"c"
:
=
ref
NONE
in
Fork
(
"c"
<-
SOME
(
"f"
#()))
;;
"c"
)%
V
.
Fork
(
"c"
<-
SOME
(
"f"
#()))
;;
"c"
.
Definition
join
:
val
:
=
locked
(
rec
:
"join"
"c"
:
=
rec
:
"join"
"c"
:
=
match
:
!
"c"
with
SOME
"x"
=>
"x"
|
NONE
=>
"join"
"c"
end
)%
V
.
end
.
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
...
...
@@ -50,7 +50,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
heapN
⊥
N
→
{{{
heap_ctx
∗
WP
f
#()
{{
Ψ
}}
}}}
spawn
e
{{{
l
,
RET
#
l
;
join_handle
l
Ψ
}}}.
Proof
.
iIntros
(<-%
of_to_val
?
Φ
)
"(#Hh & Hf) HΦ"
.
rewrite
/
spawn
-
lock
/=.
iIntros
(<-%
of_to_val
?
Φ
)
"(#Hh & Hf) HΦ"
.
rewrite
/
spawn
/=.
wp_let
.
wp_alloc
l
as
"Hl"
.
wp_let
.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
)
"Hγ"
;
first
done
.
iMod
(
inv_alloc
N
_
(
spawn_inv
γ
l
Ψ
)
with
"[Hl]"
)
as
"#?"
.
...
...
@@ -78,3 +78,4 @@ Qed.
End
proof
.
Typeclasses
Opaque
join_handle
.
Global
Opaque
spawn
join
.
heap_lang/lib/spin_lock.v
View file @
c24ee497
...
...
@@ -5,11 +5,11 @@ From iris.heap_lang Require Import proofmode notation.
From
iris
.
algebra
Require
Import
excl
.
From
iris
.
heap_lang
.
lib
Require
Import
lock
.
Definition
newlock
:
val
:
=
ssreflect
.
locked
(
λ
:
<>,
ref
#
false
)%
V
.
Definition
try_acquire
:
val
:
=
ssreflect
.
locked
(
λ
:
"l"
,
CAS
"l"
#
false
#
true
)%
V
.
Definition
newlock
:
val
:
=
λ
:
<>,
ref
#
false
.
Definition
try_acquire
:
val
:
=
λ
:
"l"
,
CAS
"l"
#
false
#
true
.
Definition
acquire
:
val
:
=
ssreflect
.
locked
(
rec
:
"acquire"
"l"
:
=
if
:
try_acquire
"l"
then
#()
else
"acquire"
"l"
)%
V
.
Definition
release
:
val
:
=
ssreflect
.
locked
(
λ
:
"l"
,
"l"
<-
#
false
)%
V
.
rec
:
"acquire"
"l"
:
=
if
:
try_acquire
"l"
then
#()
else
"acquire"
"l"
.
Definition
release
:
val
:
=
λ
:
"l"
,
"l"
<-
#
false
.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
...
...
@@ -48,7 +48,7 @@ Section proof.
heapN
⊥
N
→
{{{
heap_ctx
∗
R
}}}
newlock
#()
{{{
lk
γ
,
RET
lk
;
is_lock
γ
lk
R
}}}.
Proof
.
iIntros
(?
Φ
)
"[#Hh HR] HΦ"
.
rewrite
-
wp_fupd
/
newlock
.
unlock
.
iIntros
(?
Φ
)
"[#Hh HR] HΦ"
.
rewrite
-
wp_fupd
/
newlock
/=
.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
)
"Hγ"
;
first
done
.
iMod
(
inv_alloc
N
_
(
lock_inv
γ
l
R
)
with
"[-HΦ]"
)
as
"#?"
.
...
...
@@ -83,12 +83,13 @@ Section proof.
Proof
.
iIntros
(
Φ
)
"(Hlock & Hlocked & HR) HΦ"
.
iDestruct
"Hlock"
as
(
l
)
"(% & #? & % & #?)"
.
subst
.
rewrite
/
release
.
unlock
.
wp_let
.
iInv
N
as
(
b
)
"[Hl _]"
"Hclose"
.
rewrite
/
release
/=
.
wp_let
.
iInv
N
as
(
b
)
"[Hl _]"
"Hclose"
.
wp_store
.
iApply
"HΦ"
.
iApply
"Hclose"
.
iNext
.
iExists
false
.
by
iFrame
.
Qed
.
End
proof
.
Typeclasses
Opaque
is_lock
locked
.
Global
Opaque
newlock
try_acquire
acquire
release
.
Definition
spin_lock
`
{!
heapG
Σ
,
!
lockG
Σ
}
:
lock
Σ
:
=
{|
lock
.
locked_exclusive
:
=
locked_exclusive
;
lock
.
newlock_spec
:
=
newlock_spec
;
...
...
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