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
Iris
Commits
0c0ee757
Commit
0c0ee757
authored
Mar 10, 2016
by
Ralf Jung
Browse files
now that we use # for wp, use a different symbol for values
parent
94216199
Changes
8
Hide whitespace changes
Inline
Side-by-side
barrier/barrier.v
View file @
0c0ee757
From
iris
.
heap_lang
Require
Export
notation
.
Definition
newbarrier
:
val
:
=
λ
:
<>,
ref
#
0
.
Definition
signal
:
val
:
=
λ
:
"x"
,
'
"x"
<-
#
1
.
Definition
newbarrier
:
val
:
=
λ
:
<>,
ref
§
0
.
Definition
signal
:
val
:
=
λ
:
"x"
,
'
"x"
<-
§
1
.
Definition
wait
:
val
:
=
rec
:
"wait"
"x"
:
=
if
:
!
'
"x"
=
#
1
then
#
()
else
'
"wait"
'
"x"
.
rec
:
"wait"
"x"
:
=
if
:
!
'
"x"
=
§
1
then
§
()
else
'
"wait"
'
"x"
.
barrier/client.v
View file @
0c0ee757
...
...
@@ -4,11 +4,11 @@ From iris.program_logic Require Import auth sts saved_prop hoare ownership.
Import
uPred
.
Definition
worker
(
n
:
Z
)
:
val
:
=
λ
:
"b"
"y"
,
^
wait
'
"b"
;;
!
'
"y"
#
n
.
λ
:
"b"
"y"
,
^
wait
'
"b"
;;
!
'
"y"
§
n
.
Definition
client
:
expr
[]
:
=
let
:
"y"
:
=
ref
#
0
in
let
:
"b"
:
=
^
newbarrier
#
()
in
(
'
"y"
<-
(
λ
:
"z"
,
'
"z"
+
#
42
)
;;
^
signal
'
"b"
)
||
let
:
"y"
:
=
ref
§
0
in
let
:
"b"
:
=
^
newbarrier
§
()
in
(
'
"y"
<-
(
λ
:
"z"
,
'
"z"
+
§
42
)
;;
^
signal
'
"b"
)
||
(^(
worker
12
)
'
"b"
'
"y"
||
^(
worker
17
)
'
"b"
'
"y"
).
Section
client
.
...
...
@@ -16,7 +16,7 @@ Section client.
Local
Notation
iProp
:
=
(
iPropG
heap_lang
Σ
).
Definition
y_inv
q
y
:
iProp
:
=
(
∃
f
:
val
,
y
↦
{
q
}
f
★
□
∀
n
:
Z
,
#>
f
#
n
{{
λ
v
,
v
=
#
(
n
+
42
)
}})%
I
.
(
∃
f
:
val
,
y
↦
{
q
}
f
★
□
∀
n
:
Z
,
#>
f
§
n
{{
λ
v
,
v
=
§
(
n
+
42
)
}})%
I
.
Lemma
y_inv_split
q
y
:
y_inv
q
y
⊑
(
y_inv
(
q
/
2
)
y
★
y_inv
(
q
/
2
)
y
).
...
...
@@ -60,7 +60,7 @@ Section client.
(
ewp
eapply
wp_store
)
;
eauto
with
I
.
strip_later
.
ecancel
[
y
↦
_
]%
I
.
apply
wand_intro_l
.
wp_seq
.
rewrite
-
signal_spec
right_id
assoc
sep_elim_l
comm
.
apply
sep_mono_r
.
rewrite
/
y_inv
-(
exist_intro
(
λ
:
"z"
,
'
"z"
+
#
42
)%
V
).
apply
sep_mono_r
.
rewrite
/
y_inv
-(
exist_intro
(
λ
:
"z"
,
'
"z"
+
§
42
)%
V
).
apply
sep_intro_True_r
;
first
done
.
apply
:
always_intro
.
apply
forall_intro
=>
n
.
wp_let
.
wp_op
.
by
apply
const_intro
.
-
(* The two spawned threads, the waiters. *)
...
...
barrier/proof.v
View file @
0c0ee757
...
...
@@ -29,7 +29,7 @@ Definition ress (P : iProp) (I : gset gname) : iProp :=
▷
(
P
-
★
Π★
{
set
I
}
Ψ
)
★
Π★
{
set
I
}
(
λ
i
,
saved_prop_own
i
(
Ψ
i
)))%
I
.
Coercion
state_to_val
(
s
:
state
)
:
val
:
=
match
s
with
State
Low
_
=>
#
0
|
State
High
_
=>
#
1
end
.
match
s
with
State
Low
_
=>
§
0
|
State
High
_
=>
§
1
end
.
Arguments
state_to_val
!
_
/.
Definition
state_to_prop
(
s
:
state
)
(
P
:
iProp
)
:
iProp
:
=
...
...
@@ -112,7 +112,7 @@ Qed.
Lemma
newbarrier_spec
(
P
:
iProp
)
(
Φ
:
val
→
iProp
)
:
heapN
⊥
N
→
(
heap_ctx
heapN
★
∀
l
,
recv
l
P
★
send
l
P
-
★
Φ
(%
l
))
⊑
#>
newbarrier
#
()
{{
Φ
}}.
⊑
#>
newbarrier
§
()
{{
Φ
}}.
Proof
.
intros
HN
.
rewrite
/
newbarrier
.
wp_seq
.
rewrite
-
wp_pvs
.
wp
eapply
wp_alloc
;
eauto
with
I
ndisj
.
...
...
@@ -126,7 +126,7 @@ Proof.
▷
(
barrier_inv
l
P
(
State
Low
{[
i
]}))
★
saved_prop_own
i
P
)).
-
rewrite
-
pvs_intro
.
cancel
[
heap_ctx
heapN
].
rewrite
{
1
}[
saved_prop_own
_
_
]
always_sep_dup
.
cancel
[
saved_prop_own
i
P
].
rewrite
/
barrier_inv
/
ress
-
later_intro
.
cancel
[
l
↦
#
0
]%
I
.
rewrite
/
barrier_inv
/
ress
-
later_intro
.
cancel
[
l
↦
§
0
]%
I
.
rewrite
-(
exist_intro
(
const
P
))
/=.
rewrite
-[
saved_prop_own
_
_
](
left_id
True
%
I
(
★
)%
I
).
by
rewrite
!
big_sepS_singleton
/=
wand_diag
-
later_intro
.
-
rewrite
(
sts_alloc
(
barrier_inv
l
P
)
⊤
N
)
;
last
by
eauto
.
...
...
@@ -151,7 +151,7 @@ Proof.
Qed
.
Lemma
signal_spec
l
P
(
Φ
:
val
→
iProp
)
:
(
send
l
P
★
P
★
Φ
#
())
⊑
#>
signal
(%
l
)
{{
Φ
}}.
(
send
l
P
★
P
★
Φ
§
())
⊑
#>
signal
(%
l
)
{{
Φ
}}.
Proof
.
rewrite
/
signal
/
send
/
barrier_ctx
.
rewrite
sep_exist_r
.
apply
exist_elim
=>
γ
.
rewrite
-!
assoc
.
apply
const_elim_sep_l
=>?.
wp_let
.
...
...
@@ -162,8 +162,8 @@ Proof.
apply
forall_intro
=>-[
p
I
].
apply
wand_intro_l
.
rewrite
-!
assoc
.
apply
const_elim_sep_l
=>
Hs
.
destruct
p
;
last
done
.
rewrite
{
1
}/
barrier_inv
=>/={
Hs
}.
rewrite
later_sep
.
eapply
wp_store
with
(
v'
:
=
#
0
)
;
eauto
with
I
ndisj
.
strip_later
.
cancel
[
l
↦
#
0
]%
I
.
eapply
wp_store
with
(
v'
:
=
§
0
)
;
eauto
with
I
ndisj
.
strip_later
.
cancel
[
l
↦
§
0
]%
I
.
apply
wand_intro_l
.
rewrite
-(
exist_intro
(
State
High
I
)).
rewrite
-(
exist_intro
∅
).
rewrite
const_equiv
/=
;
last
by
eauto
using
signal_step
.
rewrite
left_id
-
later_intro
{
2
}/
barrier_inv
-!
assoc
.
apply
sep_mono_r
.
...
...
@@ -176,7 +176,7 @@ Proof.
Qed
.
Lemma
wait_spec
l
P
(
Φ
:
val
→
iProp
)
:
(
recv
l
P
★
(
P
-
★
Φ
#
()))
⊑
#>
wait
(%
l
)
{{
Φ
}}.
(
recv
l
P
★
(
P
-
★
Φ
§
()))
⊑
#>
wait
(%
l
)
{{
Φ
}}.
Proof
.
rename
P
into
R
.
wp_rec
.
rewrite
{
1
}/
recv
/
barrier_ctx
.
rewrite
!
sep_exist_r
.
...
...
barrier/specification.v
View file @
0c0ee757
...
...
@@ -12,7 +12,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma
barrier_spec
(
heapN
N
:
namespace
)
:
heapN
⊥
N
→
∃
recv
send
:
loc
→
iProp
-
n
>
iProp
,
(
∀
P
,
heap_ctx
heapN
⊑
{{
True
}}
newbarrier
#
()
{{
λ
v
,
(
∀
P
,
heap_ctx
heapN
⊑
{{
True
}}
newbarrier
§
()
{{
λ
v
,
∃
l
:
loc
,
v
=
LocV
l
★
recv
l
P
★
send
l
P
}})
∧
(
∀
l
P
,
{{
send
l
P
★
P
}}
signal
(
LocV
l
)
{{
λ
_
,
True
}})
∧
(
∀
l
P
,
{{
recv
l
P
}}
wait
(
LocV
l
)
{{
λ
_
,
P
}})
∧
...
...
heap_lang/notation.v
View file @
0c0ee757
...
...
@@ -19,11 +19,11 @@ Notation "<>" := BAnon : binder_scope.
Notation
"<>"
:
=
BAnon
:
expr_scope
.
(* No scope for the values, does not conflict and scope is often not inferred properly. *)
Notation
"
#
l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"
#
l"
).
Notation
"
§
l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"
§
l"
).
Notation
"% l"
:
=
(
LocV
l
)
(
at
level
8
,
format
"% l"
).
Notation
"
#
l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"
#
l"
)
:
val_scope
.
Notation
"
§
l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"
§
l"
)
:
val_scope
.
Notation
"% l"
:
=
(
LocV
l
)
(
at
level
8
,
format
"% l"
)
:
val_scope
.
Notation
"
#
l"
:
=
(
Lit
l
%
Z
%
V
)
(
at
level
8
,
format
"
#
l"
)
:
expr_scope
.
Notation
"
§
l"
:
=
(
Lit
l
%
Z
%
V
)
(
at
level
8
,
format
"
§
l"
)
:
expr_scope
.
Notation
"% l"
:
=
(
Loc
l
)
(
at
level
8
,
format
"% l"
)
:
expr_scope
.
Notation
"' x"
:
=
(
Var
x
)
(
at
level
8
,
format
"' x"
)
:
expr_scope
.
...
...
heap_lang/par.v
View file @
0c0ee757
...
...
@@ -5,7 +5,7 @@ Import uPred.
Definition
par
:
val
:
=
λ
:
"fs"
,
let
:
"handle"
:
=
^
spawn
(
Fst
'
"fs"
)
in
let
:
"v2"
:
=
Snd
'
"fs"
#
()
in
let
:
"v2"
:
=
Snd
'
"fs"
§
()
in
let
:
"v1"
:
=
^
join
'
"handle"
in
Pair
'
"v1"
'
"v2"
.
Notation
Par
e1
e2
:
=
(^
par
(
Pair
(
λ
:
<>,
e1
)
(
λ
:
<>,
e2
)))%
E
.
...
...
@@ -21,7 +21,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma
par_spec
(
Ψ
1
Ψ
2
:
val
→
iProp
)
e
(
f1
f2
:
val
)
(
Φ
:
val
→
iProp
)
:
heapN
⊥
N
→
to_val
e
=
Some
(
f1
,
f2
)%
V
→
(
heap_ctx
heapN
★
#>
f1
#
()
{{
Ψ
1
}}
★
#>
f2
#
()
{{
Ψ
2
}}
★
(
heap_ctx
heapN
★
#>
f1
§
()
{{
Ψ
1
}}
★
#>
f2
§
()
{{
Ψ
2
}}
★
∀
v1
v2
,
Ψ
1
v1
★
Ψ
2
v2
-
★
▷
Φ
(
v1
,
v2
)%
V
)
⊑
#>
par
e
{{
Φ
}}.
Proof
.
...
...
heap_lang/spawn.v
View file @
0c0ee757
...
...
@@ -5,8 +5,8 @@ Import uPred.
Definition
spawn
:
val
:
=
λ
:
"f"
,
let
:
"c"
:
=
ref
(
InjL
#
0
)
in
Fork
(
'
"c"
<-
InjR
(
'
"f"
#
()))
;;
'
"c"
.
let
:
"c"
:
=
ref
(
InjL
§
0
)
in
Fork
(
'
"c"
<-
InjR
(
'
"f"
§
()))
;;
'
"c"
.
Definition
join
:
val
:
=
rec
:
"join"
"c"
:
=
match
:
!
'
"c"
with
...
...
@@ -33,7 +33,7 @@ Context (heapN N : namespace).
Local
Notation
iProp
:
=
(
iPropG
heap_lang
Σ
).
Definition
spawn_inv
(
γ
:
gname
)
(
l
:
loc
)
(
Ψ
:
val
→
iProp
)
:
iProp
:
=
(
∃
lv
,
l
↦
lv
★
(
lv
=
InjLV
#
0
∨
∃
v
,
lv
=
InjRV
v
★
(
Ψ
v
∨
own
γ
(
Excl
()))))%
I
.
(
∃
lv
,
l
↦
lv
★
(
lv
=
InjLV
§
0
∨
∃
v
,
lv
=
InjRV
v
★
(
Ψ
v
∨
own
γ
(
Excl
()))))%
I
.
Definition
join_handle
(
l
:
loc
)
(
Ψ
:
val
→
iProp
)
:
iProp
:
=
(
■
(
heapN
⊥
N
)
★
∃
γ
,
heap_ctx
heapN
★
own
γ
(
Excl
())
★
...
...
@@ -50,7 +50,7 @@ Proof. solve_proper. Qed.
Lemma
spawn_spec
(
Ψ
:
val
→
iProp
)
e
(
f
:
val
)
(
Φ
:
val
→
iProp
)
:
to_val
e
=
Some
f
→
heapN
⊥
N
→
(
heap_ctx
heapN
★
#>
f
#
()
{{
Ψ
}}
★
∀
l
,
join_handle
l
Ψ
-
★
Φ
(%
l
))
(
heap_ctx
heapN
★
#>
f
§
()
{{
Ψ
}}
★
∀
l
,
join_handle
l
Ψ
-
★
Φ
(%
l
))
⊑
#>
spawn
e
{{
Φ
}}.
Proof
.
intros
Hval
Hdisj
.
rewrite
/
spawn
.
ewp
(
by
eapply
wp_value
).
wp_let
.
...
...
@@ -61,11 +61,11 @@ Proof.
rewrite
!
pvs_frame_r
.
eapply
wp_strip_pvs
.
rewrite
!
sep_exist_r
.
apply
exist_elim
=>
γ
.
(* TODO: Figure out a better way to say "I want to establish ▷ spawn_inv". *)
trans
(
heap_ctx
heapN
★
#>
f
#
()
{{
Ψ
}}
★
(
join_handle
l
Ψ
-
★
Φ
(%
l
)%
V
)
★
trans
(
heap_ctx
heapN
★
#>
f
§
()
{{
Ψ
}}
★
(
join_handle
l
Ψ
-
★
Φ
(%
l
)%
V
)
★
own
γ
(
Excl
())
★
▷
(
spawn_inv
γ
l
Ψ
))%
I
.
{
ecancel
[
#>
_
{{
_
}}
;
_
-
★
_;
heap_ctx
_;
own
_
_
]%
I
.
rewrite
-
later_intro
/
spawn_inv
-(
exist_intro
(
InjLV
#
0
)).
cancel
[
l
↦
InjLV
#
0
]%
I
.
by
apply
or_intro_l'
,
const_intro
.
}
rewrite
-
later_intro
/
spawn_inv
-(
exist_intro
(
InjLV
§
0
)).
cancel
[
l
↦
InjLV
§
0
]%
I
.
by
apply
or_intro_l'
,
const_intro
.
}
rewrite
(
inv_alloc
N
)
//
!
pvs_frame_l
.
eapply
wp_strip_pvs
.
ewp
eapply
wp_fork
.
rewrite
[
heap_ctx
_
]
always_sep_dup
[
inv
_
_
]
always_sep_dup
.
sep_split
left
:
[
_
-
★
_;
inv
_
_;
own
_
_;
heap_ctx
_
]%
I
.
...
...
heap_lang/tests.v
View file @
0c0ee757
...
...
@@ -4,14 +4,14 @@ From iris.heap_lang Require Import wp_tactics heap notation.
Import
uPred
.
Section
LangTests
.
Definition
add
:
expr
[]
:
=
(
#
21
+
#
21
)%
E
.
Goal
∀
σ
,
prim_step
add
σ
(
#
42
)
σ
None
.
Definition
add
:
expr
[]
:
=
(
§
21
+
§
21
)%
E
.
Goal
∀
σ
,
prim_step
add
σ
(
§
42
)
σ
None
.
Proof
.
intros
;
do_step
done
.
Qed
.
Definition
rec_app
:
expr
[]
:
=
((
rec
:
"f"
"x"
:
=
'
"f"
'
"x"
)
#
0
)%
E
.
Definition
rec_app
:
expr
[]
:
=
((
rec
:
"f"
"x"
:
=
'
"f"
'
"x"
)
§
0
)%
E
.
Goal
∀
σ
,
prim_step
rec_app
σ
rec_app
σ
None
.
Proof
.
intros
.
rewrite
/
rec_app
.
do_step
done
.
Qed
.
Definition
lam
:
expr
[]
:
=
(
λ
:
"x"
,
'
"x"
+
#
21
)%
E
.
Goal
∀
σ
,
prim_step
(
lam
#
21
)%
E
σ
add
σ
None
.
Definition
lam
:
expr
[]
:
=
(
λ
:
"x"
,
'
"x"
+
§
21
)%
E
.
Goal
∀
σ
,
prim_step
(
lam
§
21
)%
E
σ
add
σ
None
.
Proof
.
intros
.
rewrite
/
lam
.
do_step
done
.
Qed
.
End
LangTests
.
...
...
@@ -22,9 +22,9 @@ Section LiftingTests.
Implicit
Types
Φ
:
val
→
iPropG
heap_lang
Σ
.
Definition
heap_e
:
expr
[]
:
=
let
:
"x"
:
=
ref
#
1
in
'
"x"
<-
!
'
"x"
+
#
1
;;
!
'
"x"
.
let
:
"x"
:
=
ref
§
1
in
'
"x"
<-
!
'
"x"
+
§
1
;;
!
'
"x"
.
Lemma
heap_e_spec
E
N
:
nclose
N
⊆
E
→
heap_ctx
N
⊑
#>
heap_e
@
E
{{
λ
v
,
v
=
#
2
}}.
nclose
N
⊆
E
→
heap_ctx
N
⊑
#>
heap_e
@
E
{{
λ
v
,
v
=
§
2
}}.
Proof
.
rewrite
/
heap_e
=>
HN
.
rewrite
-(
wp_mask_weaken
N
E
)
//.
wp
eapply
wp_alloc
;
eauto
.
apply
forall_intro
=>
l
;
apply
wand_intro_l
.
...
...
@@ -36,15 +36,15 @@ Section LiftingTests.
Definition
FindPred
:
val
:
=
rec
:
"pred"
"x"
"y"
:
=
let
:
"yp"
:
=
'
"y"
+
#
1
in
let
:
"yp"
:
=
'
"y"
+
§
1
in
if
:
'
"yp"
<
'
"x"
then
'
"pred"
'
"x"
'
"yp"
else
'
"y"
.
Definition
Pred
:
val
:
=
λ
:
"x"
,
if
:
'
"x"
≤
#
0
then
-^
FindPred
(-
'
"x"
+
#
2
)
#
0
else
^
FindPred
'
"x"
#
0
.
if
:
'
"x"
≤
§
0
then
-^
FindPred
(-
'
"x"
+
§
2
)
§
0
else
^
FindPred
'
"x"
§
0
.
Lemma
FindPred_spec
n1
n2
E
Φ
:
n1
<
n2
→
Φ
#
(
n2
-
1
)
⊑
#>
FindPred
#
n2
#
n1
@
E
{{
Φ
}}.
Φ
§
(
n2
-
1
)
⊑
#>
FindPred
§
n2
§
n1
@
E
{{
Φ
}}.
Proof
.
revert
n1
.
wp_rec
=>
n1
Hn
.
wp_let
.
wp_op
.
wp_let
.
wp_op
=>
?
;
wp_if
.
...
...
@@ -53,7 +53,7 @@ Section LiftingTests.
-
assert
(
n1
=
n2
-
1
)
as
->
by
omega
;
auto
with
I
.
Qed
.
Lemma
Pred_spec
n
E
Φ
:
▷
Φ
#
(
n
-
1
)
⊑
#>
Pred
#
n
@
E
{{
Φ
}}.
Lemma
Pred_spec
n
E
Φ
:
▷
Φ
§
(
n
-
1
)
⊑
#>
Pred
§
n
@
E
{{
Φ
}}.
Proof
.
wp_lam
.
wp_op
=>
?
;
wp_if
.
-
wp_op
.
wp_op
.
...
...
@@ -63,7 +63,7 @@ Section LiftingTests.
Qed
.
Lemma
Pred_user
E
:
(
True
:
iProp
)
⊑
#>
let
:
"x"
:
=
Pred
#
42
in
^
Pred
'
"x"
@
E
{{
λ
v
,
v
=
#
40
}}.
(
True
:
iProp
)
⊑
#>
let
:
"x"
:
=
Pred
§
42
in
^
Pred
'
"x"
@
E
{{
λ
v
,
v
=
§
40
}}.
Proof
.
intros
.
ewp
apply
Pred_spec
.
wp_let
.
ewp
apply
Pred_spec
.
auto
with
I
.
Qed
.
...
...
@@ -73,7 +73,7 @@ Section ClosedProofs.
Definition
Σ
:
gFunctors
:
=
#[
heapGF
].
Notation
iProp
:
=
(
iPropG
heap_lang
Σ
).
Lemma
heap_e_closed
σ
:
{{
ownP
σ
:
iProp
}}
heap_e
{{
λ
v
,
v
=
#
2
}}.
Lemma
heap_e_closed
σ
:
{{
ownP
σ
:
iProp
}}
heap_e
{{
λ
v
,
v
=
§
2
}}.
Proof
.
apply
ht_alt
.
rewrite
(
heap_alloc
nroot
⊤
)
;
last
by
rewrite
nclose_nroot
.
apply
wp_strip_pvs
,
exist_elim
=>
?.
rewrite
and_elim_l
.
...
...
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