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
George Pirlea
Iris
Commits
2b7a62bf
Commit
2b7a62bf
authored
Mar 02, 2016
by
Ralf Jung
Browse files
notation for locations
parent
ecbac61a
Changes
3
Hide whitespace changes
Inline
Side-by-side
barrier/client.v
View file @
2b7a62bf
...
...
@@ -27,7 +27,7 @@ Section client.
Lemma
worker_safe
q
(
n
:
Z
)
(
b
y
:
loc
)
:
(
heap_ctx
heapN
★
recv
heapN
N
b
(
y_inv
q
y
))
⊑
||
worker
n
(
Loc
b
)
(
Loc
y
)
{{
λ
_
,
True
}}.
⊑
||
worker
n
(
%
b
)
(%
y
)
{{
λ
_
,
True
}}.
Proof
.
rewrite
/
worker
.
wp_lam
.
wp_let
.
ewp
apply
wait_spec
.
rewrite
comm
.
apply
sep_mono_r
.
apply
wand_intro_l
.
...
...
barrier/proof.v
View file @
2b7a62bf
...
...
@@ -125,7 +125,7 @@ Qed.
(** Actual proofs *)
Lemma
newbarrier_spec
(
P
:
iProp
)
(
Φ
:
val
→
iProp
)
:
heapN
⊥
N
→
(
heap_ctx
heapN
★
∀
l
,
recv
l
P
★
send
l
P
-
★
Φ
(
LocV
l
))
(
heap_ctx
heapN
★
∀
l
,
recv
l
P
★
send
l
P
-
★
Φ
(
%
l
))
⊑
||
newbarrier
#()
{{
Φ
}}.
Proof
.
intros
HN
.
rewrite
/
newbarrier
.
wp_seq
.
...
...
@@ -172,7 +172,7 @@ Proof.
Qed
.
Lemma
signal_spec
l
P
(
Φ
:
val
→
iProp
)
:
(
send
l
P
★
P
★
Φ
#())
⊑
||
signal
(
LocV
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
.
...
...
@@ -199,7 +199,7 @@ Proof.
Qed
.
Lemma
wait_spec
l
P
(
Φ
:
val
→
iProp
)
:
(
recv
l
P
★
(
P
-
★
Φ
#()))
⊑
||
wait
(
LocV
l
)
{{
Φ
}}.
(
recv
l
P
★
(
P
-
★
Φ
#()))
⊑
||
wait
(
%
l
)
{{
Φ
}}.
Proof
.
rename
P
into
R
.
wp_rec
.
rewrite
{
1
}/
recv
/
barrier_ctx
.
rewrite
!
sep_exist_r
.
...
...
heap_lang/notation.v
View file @
2b7a62bf
...
...
@@ -21,18 +21,16 @@ Notation "<>" := BAnon : binder_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* We have overlapping notation for values and expressions, with the expressions
coming first. This way, parsing as a value will be preferred. If an expression
was needed, the coercion of_val will be called. The notations for literals
are not put in any scope so as to avoid lots of annoying %L scopes while
pretty printing. *)
(* No scope, does not conflict and scope is often not inferred properly. *)
Notation
"# l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"# l"
).
Notation
"% l"
:
=
(
LocV
l
)
(
at
level
8
,
format
"% l"
).
Notation
"( e1 , e2 , .. , en )"
:
=
(
Pair
..
(
Pair
e1
e2
)
..
en
)
:
lang_scope
.
Notation
"'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'"
:
=
(
Match
e0
x1
e1
x2
e2
)
(
e0
,
x1
,
e1
,
x2
,
e2
at
level
200
)
:
lang_scope
.
Notation
"()"
:
=
LitUnit
:
val_scope
.
(* No scope, does not conflict and scope is often not inferred properly. *)
Notation
"# l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"# l"
).
Notation
"! e"
:
=
(
Load
e
%
L
)
(
at
level
9
,
right
associativity
)
:
lang_scope
.
Notation
"'ref' e"
:
=
(
Alloc
e
%
L
)
(
at
level
30
,
right
associativity
)
:
lang_scope
.
...
...
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