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
Rice Wine
Iris
Commits
adb5b54a
Commit
adb5b54a
authored
Dec 04, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add atomic fetch-and-add operation to heap_lang.
parent
43830b67
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
70 additions
and
6 deletions
+70
-6
theories/heap_lang/lang.v
theories/heap_lang/lang.v
+17
-4
theories/heap_lang/lifting.v
theories/heap_lang/lifting.v
+13
-0
theories/heap_lang/proofmode.v
theories/heap_lang/proofmode.v
+30
-0
theories/heap_lang/tactics.v
theories/heap_lang/tactics.v
+10
-2
No files found.
theories/heap_lang/lang.v
View file @
adb5b54a
...
...
@@ -57,7 +57,8 @@ Inductive expr :=
|
Alloc
(
e
:
expr
)
|
Load
(
e
:
expr
)
|
Store
(
e1
:
expr
)
(
e2
:
expr
)
|
CAS
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
).
|
CAS
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
)
|
FAA
(
e1
:
expr
)
(
e2
:
expr
).
Bind
Scope
expr_scope
with
expr
.
...
...
@@ -68,7 +69,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
|
Lit
_
=>
true
|
UnOp
_
e
|
Fst
e
|
Snd
e
|
InjL
e
|
InjR
e
|
Fork
e
|
Alloc
e
|
Load
e
=>
is_closed
X
e
|
App
e1
e2
|
BinOp
_
e1
e2
|
Pair
e1
e2
|
Store
e1
e2
=>
|
App
e1
e2
|
BinOp
_
e1
e2
|
Pair
e1
e2
|
Store
e1
e2
|
FAA
e1
e2
=>
is_closed
X
e1
&&
is_closed
X
e2
|
If
e0
e1
e2
|
Case
e0
e1
e2
|
CAS
e0
e1
e2
=>
is_closed
X
e0
&&
is_closed
X
e1
&&
is_closed
X
e2
...
...
@@ -189,6 +190,7 @@ Proof.
|
Load
e
=>
GenNode
13
[
go
e
]
|
Store
e1
e2
=>
GenNode
14
[
go
e1
;
go
e2
]
|
CAS
e0
e1
e2
=>
GenNode
15
[
go
e0
;
go
e1
;
go
e2
]
|
FAA
e1
e2
=>
GenNode
16
[
go
e1
;
go
e2
]
end
).
set
(
dec
:
=
fix
go
e
:
=
match
e
with
...
...
@@ -210,6 +212,7 @@ Proof.
|
GenNode
13
[
e
]
=>
Load
(
go
e
)
|
GenNode
14
[
e1
;
e2
]
=>
Store
(
go
e1
)
(
go
e2
)
|
GenNode
15
[
e0
;
e1
;
e2
]
=>
CAS
(
go
e0
)
(
go
e1
)
(
go
e2
)
|
GenNode
16
[
e1
;
e2
]
=>
FAA
(
go
e1
)
(
go
e2
)
|
_
=>
Lit
LitUnit
(* dummy *)
end
).
refine
(
inj_countable'
enc
dec
_
).
intros
e
.
induction
e
;
f_equal
/=
;
auto
.
...
...
@@ -245,7 +248,9 @@ Inductive ectx_item :=
|
StoreRCtx
(
v1
:
val
)
|
CasLCtx
(
e1
:
expr
)
(
e2
:
expr
)
|
CasMCtx
(
v0
:
val
)
(
e2
:
expr
)
|
CasRCtx
(
v0
:
val
)
(
v1
:
val
).
|
CasRCtx
(
v0
:
val
)
(
v1
:
val
)
|
FaaLCtx
(
e2
:
expr
)
|
FaaRCtx
(
v1
:
val
).
Definition
fill_item
(
Ki
:
ectx_item
)
(
e
:
expr
)
:
expr
:
=
match
Ki
with
...
...
@@ -269,6 +274,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
|
CasLCtx
e1
e2
=>
CAS
e
e1
e2
|
CasMCtx
v0
e2
=>
CAS
(
of_val
v0
)
e
e2
|
CasRCtx
v0
v1
=>
CAS
(
of_val
v0
)
(
of_val
v1
)
e
|
FaaLCtx
e2
=>
FAA
e
e2
|
FaaRCtx
v1
=>
FAA
(
of_val
v1
)
e
end
.
(** Substitution *)
...
...
@@ -293,6 +300,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
|
Load
e
=>
Load
(
subst
x
es
e
)
|
Store
e1
e2
=>
Store
(
subst
x
es
e1
)
(
subst
x
es
e2
)
|
CAS
e0
e1
e2
=>
CAS
(
subst
x
es
e0
)
(
subst
x
es
e1
)
(
subst
x
es
e2
)
|
FAA
e1
e2
=>
FAA
(
subst
x
es
e1
)
(
subst
x
es
e2
)
end
.
Definition
subst'
(
mx
:
binder
)
(
es
:
expr
)
:
expr
→
expr
:
=
...
...
@@ -364,7 +372,12 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
|
CasSucS
l
e1
v1
e2
v2
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v1
→
head_step
(
CAS
(
Lit
$
LitLoc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
true
)
(<[
l
:
=
v2
]>
σ
)
[].
head_step
(
CAS
(
Lit
$
LitLoc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
true
)
(<[
l
:
=
v2
]>
σ
)
[]
|
FaaS
l
i1
e2
i2
σ
:
to_val
e2
=
Some
(
LitV
(
LitInt
i2
))
→
σ
!!
l
=
Some
(
LitV
(
LitInt
i1
))
→
head_step
(
FAA
(
Lit
$
LitLoc
l
)
e2
)
σ
(
Lit
$
LitInt
i1
)
(<[
l
:
=
LitV
(
LitInt
(
i1
+
i2
))]>
σ
)
[].
(** Basic properties about the language *)
Instance
fill_item_inj
Ki
:
Inj
(=)
(=)
(
fill_item
Ki
).
...
...
theories/heap_lang/lifting.v
View file @
adb5b54a
...
...
@@ -179,4 +179,17 @@ Proof.
iMod
(@
gen_heap_update
with
"Hσ Hl"
)
as
"[$ Hl]"
.
iModIntro
.
iSplit
=>//.
by
iApply
"HΦ"
.
Qed
.
Lemma
wp_faa
E
l
i1
e2
i2
:
IntoVal
e2
(
LitV
(
LitInt
i2
))
→
{{{
▷
l
↦
LitV
(
LitInt
i1
)
}}}
FAA
(
Lit
(
LitLoc
l
))
e2
@
E
{{{
RET
LitV
(
LitInt
i1
)
;
l
↦
LitV
(
LitInt
(
i1
+
i2
))
}}}.
Proof
.
iIntros
(<-%
of_to_val
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2'
σ
2
efs
Hstep
)
;
inv_head_step
.
iMod
(@
gen_heap_update
with
"Hσ Hl"
)
as
"[$ Hl]"
.
iModIntro
.
iSplit
=>//.
by
iApply
"HΦ"
.
Qed
.
End
lifting
.
theories/heap_lang/proofmode.v
View file @
adb5b54a
...
...
@@ -161,6 +161,20 @@ Proof.
rewrite
into_laterN_env_sound
-
later_sep
envs_simple_replace_sound
//
;
simpl
.
rewrite
right_id
.
by
apply
later_mono
,
sep_mono_r
,
wand_mono
.
Qed
.
Lemma
tac_wp_faa
Δ
Δ
'
Δ
''
E
i
K
l
i1
e2
i2
Φ
:
IntoVal
e2
(
LitV
(
LitInt
i2
))
→
IntoLaterNEnvs
1
Δ
Δ
'
→
envs_lookup
i
Δ
'
=
Some
(
false
,
l
↦
LitV
(
LitInt
i1
))%
I
→
envs_simple_replace
i
false
(
Esnoc
Enil
i
(
l
↦
LitV
(
LitInt
(
i1
+
i2
))))
Δ
'
=
Some
Δ
''
→
envs_entails
Δ
''
(
WP
fill
K
(
Lit
(
LitInt
i1
))
@
E
{{
Φ
}})
→
envs_entails
Δ
(
WP
fill
K
(
FAA
(
Lit
(
LitLoc
l
))
e2
)
@
E
{{
Φ
}}).
Proof
.
rewrite
/
envs_entails
=>
?????
;
subst
.
rewrite
-
wp_bind
.
eapply
wand_apply
;
first
exact
:
(
wp_faa
_
_
i1
_
i2
).
rewrite
into_laterN_env_sound
-
later_sep
envs_simple_replace_sound
//
;
simpl
.
rewrite
right_id
.
by
apply
later_mono
,
sep_mono_r
,
wand_mono
.
Qed
.
End
heap
.
Tactic
Notation
"wp_apply"
open_constr
(
lem
)
:
=
...
...
@@ -256,3 +270,19 @@ Tactic Notation "wp_cas_suc" :=
|
wp_expr_simpl
;
try
wp_value_head
]
|
_
=>
fail
"wp_cas_suc: not a 'wp'"
end
.
Tactic
Notation
"wp_faa"
:
=
iStartProof
;
lazymatch
goal
with
|
|-
envs_entails
_
(
wp
?E
?e
?Q
)
=>
first
[
reshape_expr
e
ltac
:
(
fun
K
e'
=>
eapply
(
tac_wp_faa
_
_
_
_
_
K
)
;
[
apply
_
|..])
|
fail
1
"wp_faa: cannot find 'CAS' in"
e
]
;
[
apply
_
|
let
l
:
=
match
goal
with
|-
_
=
Some
(
_
,
(
?l
↦
{
_
}
_
)%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_cas_suc: cannot find"
l
"↦ ?"
|
env_cbv
;
reflexivity
|
wp_expr_simpl
;
try
wp_value_head
]
|
_
=>
fail
"wp_faa: not a 'wp'"
end
.
theories/heap_lang/tactics.v
View file @
adb5b54a
...
...
@@ -34,7 +34,8 @@ Inductive expr :=
|
Alloc
(
e
:
expr
)
|
Load
(
e
:
expr
)
|
Store
(
e1
:
expr
)
(
e2
:
expr
)
|
CAS
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
).
|
CAS
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
)
|
FAA
(
e1
:
expr
)
(
e2
:
expr
).
Fixpoint
to_expr
(
e
:
expr
)
:
heap_lang
.
expr
:
=
match
e
with
...
...
@@ -58,6 +59,7 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
|
Load
e
=>
heap_lang
.
Load
(
to_expr
e
)
|
Store
e1
e2
=>
heap_lang
.
Store
(
to_expr
e1
)
(
to_expr
e2
)
|
CAS
e0
e1
e2
=>
heap_lang
.
CAS
(
to_expr
e0
)
(
to_expr
e1
)
(
to_expr
e2
)
|
FAA
e1
e2
=>
heap_lang
.
FAA
(
to_expr
e1
)
(
to_expr
e2
)
end
.
Ltac
of_expr
e
:
=
...
...
@@ -90,6 +92,8 @@ Ltac of_expr e :=
|
heap_lang
.
CAS
?e0
?e1
?e2
=>
let
e0
:
=
of_expr
e0
in
let
e1
:
=
of_expr
e1
in
let
e2
:
=
of_expr
e2
in
constr
:
(
CAS
e0
e1
e2
)
|
heap_lang
.
FAA
?e1
?e2
=>
let
e1
:
=
of_expr
e1
in
let
e2
:
=
of_expr
e2
in
constr
:
(
FAA
e1
e2
)
|
to_expr
?e
=>
e
|
of_val
?v
=>
constr
:
(
Val
v
(
of_val
v
)
(
to_of_val
v
))
|
_
=>
match
goal
with
...
...
@@ -106,7 +110,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
|
Lit
_
=>
true
|
UnOp
_
e
|
Fst
e
|
Snd
e
|
InjL
e
|
InjR
e
|
Fork
e
|
Alloc
e
|
Load
e
=>
is_closed
X
e
|
App
e1
e2
|
BinOp
_
e1
e2
|
Pair
e1
e2
|
Store
e1
e2
=>
|
App
e1
e2
|
BinOp
_
e1
e2
|
Pair
e1
e2
|
Store
e1
e2
|
FAA
e1
e2
=>
is_closed
X
e1
&&
is_closed
X
e2
|
If
e0
e1
e2
|
Case
e0
e1
e2
|
CAS
e0
e1
e2
=>
is_closed
X
e0
&&
is_closed
X
e1
&&
is_closed
X
e2
...
...
@@ -167,6 +171,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
|
Load
e
=>
Load
(
subst
x
es
e
)
|
Store
e1
e2
=>
Store
(
subst
x
es
e1
)
(
subst
x
es
e2
)
|
CAS
e0
e1
e2
=>
CAS
(
subst
x
es
e0
)
(
subst
x
es
e1
)
(
subst
x
es
e2
)
|
FAA
e1
e2
=>
FAA
(
subst
x
es
e1
)
(
subst
x
es
e2
)
end
.
Lemma
to_expr_subst
x
er
e
:
to_expr
(
subst
x
er
e
)
=
heap_lang
.
subst
x
(
to_expr
er
)
(
to_expr
e
).
...
...
@@ -182,6 +187,7 @@ Definition is_atomic (e : expr) :=
|
Store
e1
e2
=>
bool_decide
(
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
))
|
CAS
e0
e1
e2
=>
bool_decide
(
is_Some
(
to_val
e0
)
∧
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
))
|
FAA
e1
e2
=>
bool_decide
(
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
))
|
Fork
_
=>
true
(* Make "skip" atomic *)
|
App
(
Rec
_
_
(
Lit
_
))
(
Lit
_
)
=>
true
...
...
@@ -287,4 +293,6 @@ Ltac reshape_expr e tac :=
[
reshape_val
e1
ltac
:
(
fun
v1
=>
go
(
CasRCtx
v0
v1
::
K
)
e2
)
|
go
(
CasMCtx
v0
e2
::
K
)
e1
])
|
CAS
?e0
?e1
?e2
=>
go
(
CasLCtx
e1
e2
::
K
)
e0
|
FAA
?e1
?e2
=>
reshape_val
e1
ltac
:
(
fun
v1
=>
go
(
FaaRCtx
v1
::
K
)
e2
)
|
FAA
?e1
?e2
=>
go
(
FaaLCtx
e2
::
K
)
e1
end
in
go
(@
nil
ectx_item
)
e
.
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