Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
3f520e3b
Commit
3f520e3b
authored
Mar 10, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
go back to # for values, now that this does not look like wp anymore
parent
c7390af8
Pipeline
#304
passed with stage
Changes
8
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
42 additions
and
42 deletions
+42
-42
barrier/barrier.v
barrier/barrier.v
+3
-3
barrier/client.v
barrier/client.v
+6
-6
barrier/proof.v
barrier/proof.v
+7
-7
barrier/specification.v
barrier/specification.v
+1
-1
heap_lang/notation.v
heap_lang/notation.v
+3
-3
heap_lang/par.v
heap_lang/par.v
+2
-2
heap_lang/spawn.v
heap_lang/spawn.v
+7
-7
heap_lang/tests.v
heap_lang/tests.v
+13
-13
No files found.
barrier/barrier.v
View file @
3f520e3b
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 @
3f520e3b
...
...
@@ -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
,
WP
f
§
n
{{
λ
v
,
v
=
§
(
n
+
42
)
}})%
I
.
(
∃
f
:
val
,
y
↦
{
q
}
f
★
□
∀
n
:
Z
,
WP
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 @
3f520e3b
...
...
@@ -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
))
⊢
WP
newbarrier
§
()
{{
Φ
}}.
⊢
WP
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
★
Φ
§
())
⊢
WP
signal
(%
l
)
{{
Φ
}}.
(
send
l
P
★
P
★
Φ
#
())
⊢
WP
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
-
★
Φ
§
()))
⊢
WP
wait
(%
l
)
{{
Φ
}}.
(
recv
l
P
★
(
P
-
★
Φ
#
()))
⊢
WP
wait
(%
l
)
{{
Φ
}}.
Proof
.
rename
P
into
R
.
wp_rec
.
rewrite
{
1
}/
recv
/
barrier_ctx
.
rewrite
!
sep_exist_r
.
...
...
barrier/specification.v
View file @
3f520e3b
...
...
@@ -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 @
3f520e3b
...
...
@@ -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 @
3f520e3b
...
...
@@ -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
★
WP
f1
§
()
{{
Ψ
1
}}
★
WP
f2
§
()
{{
Ψ
2
}}
★
(
heap_ctx
heapN
★
WP
f1
#
()
{{
Ψ
1
}}
★
WP
f2
#
()
{{
Ψ
2
}}
★
∀
v1
v2
,
Ψ
1
v1
★
Ψ
2
v2
-
★
▷
Φ
(
v1
,
v2
)%
V
)
⊢
WP
par
e
{{
Φ
}}.
Proof
.
...
...
heap_lang/spawn.v
View file @
3f520e3b
...
...
@@ -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
★
WP
f
§
()
{{
Ψ
}}
★
∀
l
,
join_handle
l
Ψ
-
★
Φ
(%
l
))
(
heap_ctx
heapN
★
WP
f
#
()
{{
Ψ
}}
★
∀
l
,
join_handle
l
Ψ
-
★
Φ
(%
l
))
⊢
WP
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
★
WP
f
§
()
{{
Ψ
}}
★
(
join_handle
l
Ψ
-
★
Φ
(%
l
)%
V
)
★
trans
(
heap_ctx
heapN
★
WP
f
#
()
{{
Ψ
}}
★
(
join_handle
l
Ψ
-
★
Φ
(%
l
)%
V
)
★
own
γ
(
Excl
())
★
▷
(
spawn_inv
γ
l
Ψ
))%
I
.
{
ecancel
[
WP
_
{{
_
}}
;
_
-
★
_;
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 @
3f520e3b
...
...
@@ -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
⊢
WP
heap_e
@
E
{{
λ
v
,
v
=
§
2
}}.
nclose
N
⊆
E
→
heap_ctx
N
⊢
WP
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
)
⊢
WP
FindPred
§
n2
§
n1
@
E
{{
Φ
}}.
Φ
#
(
n2
-
1
)
⊢
WP
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
)
⊢
WP
Pred
§
n
@
E
{{
Φ
}}.
Lemma
Pred_spec
n
E
Φ
:
▷
Φ
#
(
n
-
1
)
⊢
WP
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
)
⊢
WP
let
:
"x"
:
=
Pred
§
42
in
^
Pred
'
"x"
@
E
{{
λ
v
,
v
=
§
40
}}.
(
True
:
iProp
)
⊢
WP
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
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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