Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
iris-coq
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Janno
iris-coq
Commits
0523bbf3
Commit
0523bbf3
authored
Dec 05, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
add dedicated type for atomicity
parent
45ab3f31
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
41 additions
and
38 deletions
+41
-38
theories/heap_lang/tactics.v
theories/heap_lang/tactics.v
+1
-1
theories/program_logic/ectx_language.v
theories/program_logic/ectx_language.v
+4
-4
theories/program_logic/hoare.v
theories/program_logic/hoare.v
+2
-2
theories/program_logic/language.v
theories/program_logic/language.v
+14
-25
theories/program_logic/weakestpre.v
theories/program_logic/weakestpre.v
+19
-5
theories/tests/ipm_paper.v
theories/tests/ipm_paper.v
+1
-1
No files found.
theories/heap_lang/tactics.v
View file @
0523bbf3
...
...
@@ -189,7 +189,7 @@ Definition is_atomic (e : expr) :=
end
.
Lemma
is_atomic_correct
s
e
:
is_atomic
e
→
Atomic
s
(
to_expr
e
).
Proof
.
enough
(
is_atomic
e
→
Atomic
maybe_stuck
(
to_expr
e
)).
enough
(
is_atomic
e
→
Atomic
strongly_atomic
(
to_expr
e
)).
{
destruct
s
;
auto
using
strongly_atomic_atomic
.
}
intros
He
.
apply
ectx_language_atomic
.
-
intros
σ
e'
σ
'
ef
Hstep
;
simpl
in
*.
revert
Hstep
.
...
...
theories/program_logic/ectx_language.v
View file @
0523bbf3
...
...
@@ -129,10 +129,10 @@ Section ectx_language.
Canonical
Structure
ectx_lang
:
language
:
=
Language
ectx_lang_mixin
.
Definition
HeadAtomic
(
s
:
stuckness
)
(
e
:
expr
Λ
)
:
Prop
:
=
Definition
head_atomic
(
a
:
atomicity
)
(
e
:
expr
Λ
)
:
Prop
:
=
∀
σ
e'
σ
'
efs
,
head_step
e
σ
e'
σ
'
efs
→
if
s
is
not_stuck
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
if
a
is
weakly_atomic
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
(* Some lemmas about this language *)
Lemma
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
.
...
...
@@ -173,8 +173,8 @@ Section ectx_language.
apply
(
Hirr
empty_ectx
).
by
rewrite
fill_empty
.
Qed
.
Lemma
ectx_language_atomic
s
e
:
HeadAtomic
s
e
→
sub_redexes_are_values
e
→
Atomic
s
e
.
Lemma
ectx_language_atomic
a
e
:
head_atomic
a
e
→
sub_redexes_are_values
e
→
Atomic
a
e
.
Proof
.
intros
Hatomic_step
Hatomic_fill
σ
e'
σ
'
efs
[
K
e1'
e2'
->
->
Hstep
].
assert
(
K
=
empty_ectx
)
as
->
by
eauto
10
using
val_head_stuck
.
...
...
theories/program_logic/hoare.v
View file @
0523bbf3
...
...
@@ -58,7 +58,7 @@ Lemma ht_mono s E P P' Φ Φ' e :
(
P
⊢
P'
)
→
(
∀
v
,
Φ
'
v
⊢
Φ
v
)
→
{{
P'
}}
e
@
s
;
E
{{
Φ
'
}}
⊢
{{
P
}}
e
@
s
;
E
{{
Φ
}}.
Proof
.
by
intros
;
apply
persistently_mono
,
wand_mono
,
wp_mono
.
Qed
.
Lemma
ht_stuck_mono
s1
s2
E
P
Φ
e
:
(
s1
≤
s2
)%
stuckness
→
{{
P
}}
e
@
s1
;
E
{{
Φ
}}
⊢
{{
P
}}
e
@
s2
;
E
{{
Φ
}}.
stuckness_le
s1
s2
→
{{
P
}}
e
@
s1
;
E
{{
Φ
}}
⊢
{{
P
}}
e
@
s2
;
E
{{
Φ
}}.
Proof
.
by
intros
;
apply
persistently_mono
,
wand_mono
,
wp_stuck_mono
.
Qed
.
Global
Instance
ht_mono'
s
E
:
Proper
(
flip
(
⊢
)
==>
eq
==>
pointwise_relation
_
(
⊢
)
==>
(
⊢
))
(
ht
s
E
).
...
...
@@ -79,7 +79,7 @@ Proof.
iIntros
(
v
)
"Hv"
.
by
iApply
"HΦ"
.
Qed
.
Lemma
ht_atomic
s
E1
E2
P
P'
Φ
Φ
'
e
`
{!
Atomic
s
e
}
:
Lemma
ht_atomic
s
E1
E2
P
P'
Φ
Φ
'
e
`
{!
Atomic
(
stuckness_to_atomicity
s
)
e
}
:
(
P
={
E1
,
E2
}=>
P'
)
∧
{{
P'
}}
e
@
s
;
E2
{{
Φ
'
}}
∧
(
∀
v
,
Φ
'
v
={
E2
,
E1
}=>
Φ
v
)
⊢
{{
P
}}
e
@
s
;
E1
{{
Φ
}}.
Proof
.
...
...
theories/program_logic/language.v
View file @
0523bbf3
...
...
@@ -53,19 +53,7 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
Instance
language_ctx_id
Λ
:
LanguageCtx
(@
id
(
expr
Λ
)).
Proof
.
constructor
;
naive_solver
.
Qed
.
Variant
stuckness
:
=
not_stuck
|
maybe_stuck
.
Definition
stuckness_le
(
s1
s2
:
stuckness
)
:
bool
:
=
match
s1
,
s2
with
|
maybe_stuck
,
not_stuck
=>
false
|
_
,
_
=>
true
end
.
Instance
:
@
PreOrder
stuckness
stuckness_le
.
Proof
.
split
;
first
by
case
.
move
=>
s1
s2
s3
.
by
case
:
s1
;
case
:
s2
;
case
:
s3
.
Qed
.
Bind
Scope
stuckness_scope
with
stuckness
.
Delimit
Scope
stuckness_scope
with
stuckness
.
Infix
"≤"
:
=
stuckness_le
:
stuckness_scope
.
Inductive
atomicity
:
=
strongly_atomic
|
weakly_atomic
.
Section
language
.
Context
{
Λ
:
language
}.
...
...
@@ -86,21 +74,21 @@ Section language.
Definition
stuck
(
e
:
expr
Λ
)
(
σ
:
state
Λ
)
:
=
to_val
e
=
None
∧
irreducible
e
σ
.
(* [Atomic
not_stuck]: This (weak) form of atomicity is enough to open invariants when WP ensures
safety, i.e., programs never can get stuck. We have an example in
lambdaRust of an expression that is atomic in this sense, but not in the
s
tronger sense defined below, and we have to be able to open invariants
around that expression. See `CasStuckS` in
(* [Atomic
weakly_atomic]: This (weak) form of atomicity is enough to open
invariants when WP ensures safety, i.e., programs never can get stuck. We
have an example in lambdaRust of an expression that is atomic in this
s
ense, but not in the stronger sense defined below, and we have to be able
to open invariants
around that expression. See `CasStuckS` in
[lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
[Atomic
maybe_stuck]: To open invariants with a WP that does not ensure safety, we need a
s
tronger form of atomicity. With the above definition, in case `e` reduces
to a stuck non-value, there is no proof that the invariants have been
established again. *)
Class
Atomic
(
s
:
stuckness
)
(
e
:
expr
Λ
)
:
Prop
:
=
[Atomic
strongly_atomic]: To open invariants with a WP that does not ensure
s
afety, we need a stronger form of atomicity. With the above definition,
in case `e` reduces to a stuck non-value, there is no proof that the
invariants have been
established again. *)
Class
Atomic
(
a
:
atomicity
)
(
e
:
expr
Λ
)
:
Prop
:
=
atomic
σ
e'
σ
'
efs
:
prim_step
e
σ
e'
σ
'
efs
→
if
s
is
not_stuck
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
if
a
is
weakly_atomic
then
irreducible
e'
σ
'
else
is_Some
(
to_val
e'
).
Inductive
step
(
ρ
1
ρ
2
:
cfg
Λ
)
:
Prop
:
=
|
step_atomic
e1
σ
1 e2
σ
2
efs
t1
t2
:
...
...
@@ -121,7 +109,8 @@ Section language.
Global
Instance
of_val_inj
:
Inj
(=)
(=)
(@
of_val
Λ
).
Proof
.
by
intros
v
v'
Hv
;
apply
(
inj
Some
)
;
rewrite
-!
to_of_val
Hv
.
Qed
.
Lemma
strongly_atomic_atomic
e
:
Atomic
maybe_stuck
e
→
Atomic
not_stuck
e
.
Lemma
strongly_atomic_atomic
e
:
Atomic
strongly_atomic
e
→
Atomic
weakly_atomic
e
.
Proof
.
unfold
Atomic
.
eauto
using
val_irreducible
.
Qed
.
Lemma
reducible_fill
`
{
LanguageCtx
Λ
K
}
e
σ
:
...
...
theories/program_logic/weakestpre.v
View file @
0523bbf3
...
...
@@ -11,6 +11,17 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
}.
Notation
irisG
Λ
Σ
:
=
(
irisG'
(
state
Λ
)
Σ
).
Inductive
stuckness
:
=
not_stuck
|
maybe_stuck
.
Definition
stuckness_le
(
s1
s2
:
stuckness
)
:
bool
:
=
match
s1
,
s2
with
|
maybe_stuck
,
not_stuck
=>
false
|
_
,
_
=>
true
end
.
Instance
:
PreOrder
stuckness_le
.
Proof
.
split
;
first
by
case
.
move
=>
s1
s2
s3
.
by
case
:
s1
;
case
:
s2
;
case
:
s3
.
Qed
.
Definition
wp_pre
`
{
irisG
Λ
Σ
}
(
s
:
stuckness
)
(
wp
:
coPset
-
c
>
expr
Λ
-
c
>
(
val
Λ
-
c
>
iProp
Σ
)
-
c
>
iProp
Σ
)
:
coPset
-
c
>
expr
Λ
-
c
>
(
val
Λ
-
c
>
iProp
Σ
)
-
c
>
iProp
Σ
:
=
λ
E
e1
Φ
,
...
...
@@ -233,7 +244,10 @@ Qed.
Lemma
wp_fupd
s
E
e
Φ
:
WP
e
@
s
;
E
{{
v
,
|={
E
}=>
Φ
v
}}
⊢
WP
e
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
"H"
.
iApply
(
wp_strong_mono
s
E
)
;
try
iFrame
;
auto
.
Qed
.
Lemma
wp_atomic
s
E1
E2
e
Φ
`
{
Hatomic
:
!
Atomic
s
e
}
:
Definition
stuckness_to_atomicity
s
:
=
if
s
is
maybe_stuck
then
strongly_atomic
else
weakly_atomic
.
Lemma
wp_atomic
s
E1
E2
e
Φ
`
{!
Atomic
(
stuckness_to_atomicity
s
)
e
}
:
(|={
E1
,
E2
}=>
WP
e
@
s
;
E2
{{
v
,
|={
E2
,
E1
}=>
Φ
v
}})
⊢
WP
e
@
s
;
E1
{{
Φ
}}.
Proof
.
iIntros
"H"
.
rewrite
!
wp_unfold
/
wp_pre
.
...
...
@@ -245,8 +259,8 @@ Proof.
rewrite
!
wp_unfold
/
wp_pre
.
destruct
(
to_val
e2
)
as
[
v2
|]
eqn
:
He2
.
+
iDestruct
"H"
as
">> $"
.
by
iFrame
.
+
iMod
(
"H"
with
"[$]"
)
as
"[H _]"
.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
by
edestruct
(
H
atomic
_
_
_
_
Hstep
).
-
destruct
(
H
atomic
_
_
_
_
Hstep
)
as
[
v
<-%
of_to_val
].
by
edestruct
(
atomic
_
_
_
_
Hstep
).
-
destruct
(
atomic
_
_
_
_
Hstep
)
as
[
v
<-%
of_to_val
].
iMod
(
"H"
with
"[#]"
)
as
"($ & H & $)"
;
first
done
.
iMod
(
wp_value_inv
with
"H"
)
as
">H"
.
by
iApply
wp_value'
.
Qed
.
...
...
@@ -300,7 +314,7 @@ Proof.
iIntros
"{$H}"
(
v
)
"?"
.
by
iApply
H
Φ
.
Qed
.
Lemma
wp_stuck_mono
s1
s2
E
e
Φ
:
(
s1
≤
s2
)%
stuckness
→
WP
e
@
s1
;
E
{{
Φ
}}
⊢
WP
e
@
s2
;
E
{{
Φ
}}.
stuckness_le
s1
s2
→
WP
e
@
s1
;
E
{{
Φ
}}
⊢
WP
e
@
s2
;
E
{{
Φ
}}.
Proof
.
case
:
s1
;
case
:
s2
=>
//
_
.
exact
:
wp_stuck_weaken
.
Qed
.
Lemma
wp_mask_mono
s
E1
E2
e
Φ
:
E1
⊆
E2
→
WP
e
@
s
;
E1
{{
Φ
}}
⊢
WP
e
@
s
;
E2
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
;
iApply
(
wp_strong_mono
s
E1
E2
)
;
auto
.
iFrame
;
eauto
.
Qed
.
...
...
@@ -379,7 +393,7 @@ Section proofmode_classes.
(* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
Global
Instance
elim_modal_fupd_wp_atomic
s
E1
E2
e
P
Φ
:
Atomic
s
e
→
Atomic
(
stuckness_to_atomicity
s
)
e
→
ElimModal
(|={
E1
,
E2
}=>
P
)
P
(
WP
e
@
s
;
E1
{{
Φ
}})
(
WP
e
@
s
;
E2
{{
v
,
|={
E2
,
E1
}=>
Φ
v
}})%
I
|
100
.
Proof
.
intros
.
by
rewrite
/
ElimModal
fupd_frame_r
wand_elim_r
wp_atomic
.
Qed
.
...
...
theories/tests/ipm_paper.v
View file @
0523bbf3
...
...
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
mask changing update modalities directly in our proofs, but in this file we use
the first prove the rule as a lemma, and then use that. *)
Lemma
wp_inv_open
`
{
irisG
Λ
Σ
}
N
E
P
e
Φ
:
nclose
N
⊆
E
→
Atomic
not_stuck
e
→
nclose
N
⊆
E
→
Atomic
weakly_atomic
e
→
inv
N
P
∗
(
▷
P
-
∗
WP
e
@
E
∖
↑
N
{{
v
,
▷
P
∗
Φ
v
}})
⊢
WP
e
@
E
{{
Φ
}}.
Proof
.
iIntros
(??)
"[#Hinv Hwp]"
.
...
...
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