Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Diaframe
Commits
ec9601fe
Commit
ec9601fe
authored
May 17, 2022
by
Ike Mulder
Browse files
Got ReLoC automation working with logically atomic specs.
parent
b8c2bcf3
Pipeline
#66142
passed with stage
in 8 minutes and 44 seconds
Changes
8
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
theories/examples/external/reloc/atomic_post_update.v
0 → 100644
View file @
ec9601fe
From
iris
.
bi
Require
Export
bi
telescopes
lib
.
atomic
.
From
iris
.
proofmode
Require
Import
tactics
notation
reduction
.
From
iris
.
program_logic
Require
Import
weakestpre
lifting
atomic
.
From
diaframe
Require
Import
proofmode_base
.
From
diaframe
.
lib
Require
Import
greatest_laterable_fixpoint
atomic
.
Section
atomic_post_acc
.
Context
`
{
BiFUpd
PROP
}.
(* atomic accessor where the commiting mask is a parameter. *)
Definition
atomic_post_acc
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
P
(
β
Φ
:
TA
→
TB
→
PROP
)
:
PROP
:
=
|={
Eo
,
Ei
}=>
∃
x
,
α
x
∗
(
α
x
={
Ei
,
Eo
}=
∗
P
)
∧
(
∀
..
y
,
β
x
y
={
Ei
,
Ef
}=
∗
Φ
x
y
).
Lemma
atomic_post_acc_equiv
{
TA
TB
:
tele
}
Eo
Ei
(
α
:
TA
→
PROP
)
P
(
β
Φ
:
TA
→
TB
→
PROP
)
:
atomic_acc
Eo
Ei
α
P
β
Φ
⊣
⊢
atomic_post_acc
Eo
Ei
Eo
α
P
β
Φ
.
Proof
.
rewrite
/
atomic_acc
/
atomic_post_acc
.
apply
(
anti_symm
_
).
-
iIntros
">[%x [Hα Hr]]"
.
iExists
_
.
by
iFrame
.
-
iIntros
">[%x [Hα Hr]]"
.
iExists
_
.
by
iFrame
.
Qed
.
Context
{
TA
TB
:
tele
}.
Context
(
Eo
Ei
Ef
:
coPset
)
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
).
Definition
atomic_post_update_pre
(
Ψ
:
()
→
PROP
)
(
_
:
())
:
PROP
:
=
make_laterable
$
atomic_post_acc
Eo
Ei
Ef
α
(
Ψ
())
β
Φ
.
Instance
atomic_post_update_pre_mono
:
fixpoint
.
BiMonoPred
atomic_post_update_pre
.
Proof
.
constructor
.
-
iIntros
(
P1
P2
??)
"#HP12"
.
iIntros
([])
"AU"
.
iApply
(
make_laterable_intuitionistic_wand
with
"[] AU"
).
iIntros
"!> AA"
.
rewrite
/
atomic_post_acc
.
iMod
"AA"
as
"[%x [H1 H2]]"
.
iExists
_
.
iFrame
.
iIntros
"!>"
.
iSplit
.
*
iIntros
"Ha"
.
iApply
"HP12"
.
by
iApply
"H2"
.
*
iIntros
(
y
)
"Hb"
.
by
iApply
"H2"
.
-
intros
??.
solve_proper
.
Qed
.
Definition
atomic_post_update_def
:
=
fixpoint
.
bi_greatest_fixpoint
atomic_post_update_pre
().
End
atomic_post_acc
.
(** Seal it *)
Definition
atomic_post_update_aux
:
seal
(@
atomic_post_update_def
).
Proof
.
by
eexists
.
Qed
.
Definition
atomic_post_update
:
=
atomic_post_update_aux
.(
unseal
).
Global
Arguments
atomic_post_update
{
PROP
_
TA
TB
}.
Global
Arguments
atomic_post_acc
{
PROP
_
TA
TB
}
Eo
Ei
Ef
_
_
_
_
:
simpl
never
.
Definition
atomic_post_update_eq
:
@
atomic_post_update
=
_
:
=
atomic_post_update_aux
.(
seal_eq
).
From
diaframe
.
symb_exec
Require
Import
defs
weakestpre_logatom
.
Section
lemmas
.
Context
`
{
BiFUpd
PROP
}.
Local
Existing
Instance
atomic_post_update_pre_mono
.
Global
Instance
atomic_update3_laterable
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
:
Laterable
$
atomic_post_update
Eo
Ei
Ef
α
β
Φ
.
Proof
.
rewrite
atomic_post_update_eq
{
1
}/
atomic_post_update_def
fixpoint
.
greatest_fixpoint_unfold
.
apply
_
.
Qed
.
Lemma
atomic_post_update_equiv
{
TA
TB
:
tele
}
Eo
Ei
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
:
atomic_update
Eo
Ei
α
β
Φ
⊣
⊢
atomic_post_update
Eo
Ei
Eo
α
β
Φ
.
Proof
.
rewrite
atomic_update_eq
/
atomic_update_def
.
rewrite
atomic_post_update_eq
/
atomic_post_update_def
.
apply
(
anti_symm
_
).
-
iApply
(
fixpoint
.
greatest_fixpoint_strong_mono
with
"[]"
).
{
apply
atomic_update_pre_mono
.
}
iIntros
"!>"
(
F'
[]).
rewrite
/
atomic_post_update_pre
/
atomic_post_update_pre
.
iApply
make_laterable_intuitionistic_wand
.
iIntros
"!>"
.
rewrite
/
atomic_acc
/
atomic_post_acc
.
iMod
1
as
"[%x [Hα Hx]]"
.
iExists
_
.
by
iFrame
.
-
iApply
(
fixpoint
.
greatest_fixpoint_strong_mono
with
"[]"
).
{
apply
atomic_update_pre_mono
.
}
iIntros
"!>"
(
F'
[]).
rewrite
/
atomic_post_update_pre
/
atomic_post_update_pre
.
iApply
make_laterable_intuitionistic_wand
.
iIntros
"!>"
.
rewrite
/
atomic_acc
/
atomic_post_acc
.
iMod
1
as
"[%x [Hα Hx]]"
.
iExists
_
.
by
iFrame
.
Qed
.
Definition
atomic_post_templateM
(
M
:
coPset
)
(
P1
:
PROP
)
Ef
TT1
TT2
(
P2
:
TT1
-
t
>
PROP
)
(
Q1
Q2
:
TT1
-
t
>
TT2
-
t
>
PROP
)
:
(
TT1
*
TT2
→
PROP
)
→
PROP
:
=
(
λ
Ψ
,
|={
⊤
}=>
P1
∗
atomic_post_update
(
⊤
∖
M
)
∅
Ef
(
tele_app
P2
)
(
tele_app
(
tele_map
tele_app
Q2
))
(
λ
a
b
,
tele_app
(
tele_app
Q1
a
)
b
-
∗
Ψ
(
a
,
b
)))%
I
.
Global
Arguments
atomic_post_templateM
M
P1
Ef
TT1
TT2
P2
Q1
Q2
Ψ
/.
Lemma
atomic_post_templateM_equiv
(
M
:
coPset
)
(
P1
:
PROP
)
TT1
TT2
(
P2
:
TT1
-
t
>
PROP
)
(
Q1
Q2
:
TT1
-
t
>
TT2
-
t
>
PROP
)
Ψ
:
atomic_post_templateM
M
P1
(
⊤
∖
M
)
TT1
TT2
P2
Q1
Q2
Ψ
⊣
⊢
atomic_templateM
M
P1
TT1
TT2
P2
Q1
Q2
Ψ
.
Proof
.
rewrite
/
atomic_post_templateM
/
atomic_templateM
.
rewrite
atomic_post_update_equiv
//.
Qed
.
Lemma
atomic_post_update_mono
{
TA
TB
TB'
:
tele
}
Eo
Ei
Ef1
Ef2
(
α
α
'
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
(
β
'
Ψ
:
TA
→
TB'
→
PROP
)
:
atomic_post_update
Eo
Ei
Ef1
α
β
Φ
-
∗
(
□
((
∀
..
a
,
(|={
Ei
}=>
α
a
)
∗
-
∗
|={
Ei
}=>
α
'
a
)
∧
(
∀
..
a
,
∃
(
f
:
TB'
→
TB
),
(
∀
..
b'
,
β
'
a
b'
={
Ei
}=
∗
β
a
(
f
b'
))
∧
(
∀
..
b'
,
Φ
a
(
f
b'
)
={
Ef1
,
Ef2
}=
∗
Ψ
a
b'
))))
-
∗
atomic_post_update
Eo
Ei
Ef2
α
'
β
'
Ψ
.
Proof
.
rewrite
atomic_post_update_eq
/
atomic_post_update_def
.
iIntros
"HΦ #(Ha & Hf)"
.
iApply
(
fixpoint
.
greatest_fixpoint_strong_mono
with
"[] HΦ"
).
iIntros
"!>"
(
F'
[]).
rewrite
/
atomic_post_update_pre
.
iApply
make_laterable_intuitionistic_wand
.
iIntros
"!>"
.
rewrite
/
atomic_post_acc
.
iMod
1
as
"[%x [Hα Hx]]"
.
iExists
_
.
iAssert
(|={
Ei
}=>
α
x
)%
I
with
"[Hα]"
as
"Hα"
;
first
eauto
.
iDestruct
(
"Ha"
with
"Hα"
)
as
">$"
.
iIntros
"!>"
.
iSplit
.
-
iIntros
"Hα"
.
iDestruct
"Hx"
as
"[Hx _]"
.
iApply
fupd_trans
.
iApply
"Hx"
.
iApply
"Ha"
.
by
iFrame
.
-
iIntros
(
y
)
"Hβ"
.
iDestruct
"Hx"
as
"[_ Hx]"
.
iDestruct
(
"Hf"
$!
x
)
as
"[%f [HB H]]"
.
iApply
fupd_trans
.
iApply
"H"
.
iApply
fupd_trans
.
iApply
"Hx"
.
iApply
"HB"
.
iApply
"Hβ"
.
Qed
.
Lemma
atomic_post_update_mask_change
{
TA
TB
:
tele
}
Eo
Ei
Ef1
Ef2
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
:
atomic_post_update
Eo
Ei
Ef1
α
β
(
λ
a
b
,
fupd
Ef1
Ef2
$
Φ
a
b
)
-
∗
atomic_post_update
Eo
Ei
Ef2
α
β
Φ
.
Proof
.
iIntros
"H"
.
iApply
(
atomic_post_update_mono
with
"H"
).
iIntros
"!>"
.
iSplit
;
eauto
.
iIntros
(
a
).
iExists
id
.
iSplit
;
eauto
.
Qed
.
Lemma
atomic_post_templateM_is_mono
M
P1
Ef
TT1
TT2
P2
Q1
Q2
:
template_mono
(
atomic_post_templateM
M
P1
Ef
TT1
TT2
P2
Q1
Q2
).
Proof
.
move
=>
S
T
HST
/=.
apply
fupd_mono
,
bi
.
sep_mono_r
.
iIntros
"H"
.
iApply
(
atomic_post_update_mono
with
"H"
).
iIntros
"!>"
;
iSplit
;
first
eauto
.
iIntros
(
a
).
iExists
id
.
iSplit
;
first
eauto
.
iIntros
(
b
)
=>
/=.
rewrite
-
fupd_intro
.
iStopProof
.
apply
bi
.
wand_intro_l
.
rewrite
right_id
.
apply
bi
.
wand_mono
;
first
done
.
apply
HST
.
Qed
.
Lemma
atomic_post_templateM_is_absorbing
M
P1
Ef
TT1
TT2
P2
Q1
Q2
:
Laterable
(
emp
:
PROP
)%
I
→
Affine
(
PROP
:
=
PROP
)
True
%
I
→
template_conditionally_absorbing
(
atomic_post_templateM
M
P1
Ef
TT1
TT2
P2
Q1
Q2
)
Laterable
.
Proof
.
move
=>
He
P
Q
HQ
Htrue
/=.
iIntros
"[>[$ H] HQ] !>"
.
rewrite
{
2
}
atomic_post_update_eq
/
atomic_post_update_def
.
iApply
(
fixpoint
.
greatest_fixpoint_coiter
_
(
λ
_
,
_
)
with
"[] [H HQ]"
)
;
last
iAccu
.
iIntros
"!>"
([])
"[HAU HQ]"
.
rewrite
/
atomic_post_update_pre
.
iStepS
.
rewrite
/
atomic_post_acc
.
rewrite
atomic_post_update_eq
{
1
}/
atomic_post_update_def
fixpoint
.
greatest_fixpoint_unfold
/
atomic_post_update_pre
.
rewrite
make_laterable_elim
.
iMod
"HAU"
as
">[%x [HP Hr]]"
.
iExists
_
.
by
iFrame
.
Qed
.
End
lemmas
.
Section
automation
.
Context
`
{
BiFUpd
PROP
}.
Lemma
atomic_post_update_to_gfp
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
:
greatest_laterable_fixpoint_wrt
(
λ
Ψ
,
make_laterable
$
atomic_post_acc
Eo
Ei
Ef
α
Ψ
β
Φ
)
emp
-
∗
atomic_post_update
Eo
Ei
Ef
α
β
Φ
.
Proof
.
rewrite
greatest_laterable_fixpoint_wrt_eq
atomic_post_update_eq
/
atomic_post_update_def
left_id
//=.
Qed
.
(* this instance is necessary to prevent looping TC search *)
Global
Instance
au_later_except_0
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
:
LaterToExcept0
(
atomic_post_update
Eo
Ei
Ef
α
β
Φ
)
(
▷
atomic_post_update
Eo
Ei
Ef
α
β
Φ
)%
I
|
10
.
Proof
.
rewrite
/
LaterToExcept0
//.
eauto
.
Qed
.
(* an atomic post accessor in a shape more accessible to the automation *)
(* We need to use option2 to get around the universe constraints: option < tele *)
Definition
atomic_post_acc'
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
P
(
β
Φ
:
TA
→
TB
→
PROP
)
:
PROP
:
=
|={
Eo
,
Ei
}=>
∃
x
,
α
x
∗
(
∀
my
:
option2
(
tele_arg
TB
),
((
α
x
∧
⌜
my
=
None2
⌝
)
∨
(
∃
..
y
,
β
x
y
∧
⌜
my
=
Some2
y
⌝
))
-
∗
match
my
with
|
None2
=>
|={
Ei
,
Eo
}=>
P
|
Some2
y
=>
|={
Ei
,
Ef
}=>
Φ
x
y
end
).
Lemma
atomic_accs_equiv
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
P
(
β
Φ
:
TA
→
TB
→
PROP
)
:
atomic_post_acc
Eo
Ei
Ef
α
P
β
Φ
⊣
⊢
atomic_post_acc'
Eo
Ei
Ef
α
P
β
Φ
.
Proof
.
(* cannot use automation here since operating on abstract telescopes *)
apply
(
anti_symm
_
)
;
rewrite
/
atomic_post_acc
/
atomic_post_acc'
.
-
iMod
1
as
"[%x [Hα Hx]]"
.
iExists
_
.
iFrame
.
iIntros
"!>"
([
y
|])
"[[Hα %]|[%y' [Hβ %]]]"
;
try
simplify_eq
.
*
iDestruct
"Hx"
as
"[_ Hx]"
.
by
iApply
"Hx"
.
*
iDestruct
"Hx"
as
"[Hx _]"
.
by
iApply
"Hx"
.
-
iMod
1
as
"[%x [Hα Hx]]"
.
iExists
_
.
iFrame
.
iIntros
"!>"
;
iSplit
.
*
iIntros
"Hα"
.
iSpecialize
(
"Hx"
$!
None2
).
iApply
"Hx"
.
iLeft
.
by
iFrame
.
*
iIntros
(
y
)
"Hβ"
.
iSpecialize
(
"Hx"
$!
(
Some2
y
)).
iApply
"Hx"
.
iRight
.
iExists
_
.
by
iFrame
.
Qed
.
(* when we need to prove an atomic update, we first run the greatest laterable fixpoint *)
Global
Instance
abduct_atomic_post_update
{
TA
TB
:
tele
}
Eo
Ei
Ef
(
α
:
TA
→
PROP
)
(
β
Φ
:
TA
→
TB
→
PROP
)
:
HINT1
empty_hyp_last
✱
[
greatest_laterable_fixpoint_wrt
(
λ
Ψ
,
make_laterable
$
atomic_post_acc'
Eo
Ei
Ef
α
Ψ
β
Φ
)
emp
]
⊫
[
id
]
;
atomic_post_update
Eo
Ei
Ef
α
β
Φ
.
Proof
.
rewrite
/
Abduct
/=
empty_hyp_last_eq
left_id
.
rewrite
<-
atomic_post_update_to_gfp
.
rewrite
greatest_laterable_fixpoint_wrt_eq
.
apply
bi
.
wand_mono
=>
//.
rewrite
{
1
}
greatest_fixpoint_proper
//.
move
=>
R
[]
/=.
generalize
(
R
())
=>
R'
{
R
}.
rewrite
make_laterable_proper
//.
rewrite
atomic_accs_equiv
//.
Qed
.
Class
SimplifyMask
(
E
E'
:
coPset
)
:
=
mask_simplify
:
E
=
E'
.
Global
Instance
simplify_sub_emptyset
E
:
SimplifyMask
(
E
∖
∅
)
E
|
10
.
Proof
.
rewrite
/
SimplifyMask
difference_empty_L
//.
Qed
.
Global
Instance
simplify_mask_fallback
E
:
SimplifyMask
E
E
|
20
.
Proof
.
done
.
Qed
.
(* after running the fixpoint and introducing make_laterable, we proceed as follows: *)
Global
Instance
atomic_post_acc_abd
{
TA
TB
:
tele
}
Eo
Eo'
Ei'
Ei
Ef
(
α
:
TA
→
PROP
)
P
(
β
Φ
:
TA
→
TB
→
PROP
)
beq
:
SimplifyMask
Eo
Eo'
→
SimplTeleEq
TB
beq
→
HINT1
empty_hyp_first
✱
[
|={
Eo'
,
Ei'
}=>
∃
..
x
,
α
x
∗
(* A neat trick is that we need Ei ⊆ Ei', but we can actually defer that to below! *)
(
∀
(
b
:
bool
),
⌜
b
=
true
⌝
∨
⌜
b
=
false
⌝
-
∗
∀
..
(
my
:
if
b
then
TB
else
[
tele
]),
α
x
∧
⌜
b
=
false
⌝
∨
(
∃
..
y
:
TB
,
β
x
y
∧
⌜
b
=
true
⌝
∧
⌜
match
b
,
my
with
|
true
,
y'
=>
tele_app
(
tele_app
beq
y'
)
y
|
false
,
_
=>
False
end
⌝
)
-
∗
match
b
,
my
with
|
false
,
_
=>
|={
Ei'
,
Eo'
}=>
⌜
Ei
⊆
Ei'
⌝
∧
P
|
true
,
my
=>
|={
Ei'
,
Ef
}=>
Φ
x
my
end
)
]
⊫
[
id
]
;
atomic_post_acc'
Eo
Ei
Ef
α
P
β
Φ
.
Proof
.
rewrite
/
Abduct
/
atomic_post_acc'
/=
empty_hyp_first_eq
left_id
=>
->
Hbeq
.
iIntros
">[%x (Hα & Hy)]"
.
destruct
(
decide
(
Ei
⊆
Ei'
))
;
last
first
.
{
iSpecialize
(
"Hy"
$!
false
).
simpl
.
iAssert
(|={
Ei'
,
Eo'
}=>
⌜
Ei
⊆
Ei'
⌝
∧
P
)%
I
with
"[Hα Hy]"
as
">[% H]"
.
*
iApply
"Hy"
;
eauto
.
*
contradiction
.
}
iMod
(
fupd_mask_subseteq
)
as
"Hcl"
;
last
iIntros
"!>"
.
exact
s
.
iExists
_
.
iFrame
.
iIntros
(
my
)
"[[Hα ->] | [%y [Hβ ->]]]"
;
iMod
"Hcl"
as
"_"
.
*
iSpecialize
(
"Hy"
$!
false
).
simpl
.
iAssert
(|={
Ei'
,
Eo'
}=>
⌜
Ei
⊆
Ei'
⌝
∧
P
)%
I
with
"[Hy Hα]"
as
">[% $]"
;
last
done
.
iApply
"Hy"
;
eauto
.
*
unshelve
(
iSpecialize
(
"Hy"
$!
true
_
y
))
;
first
eauto
.
iApply
"Hy"
.
iRight
.
iExists
_
.
iFrame
.
iPureIntro
;
split
=>
//.
revert
Hbeq
=>
/(
dep_eval_tele
y
)
/(
dep_eval_tele
y
)
->.
split
;
first
done
.
eapply
tele_eq_app_both
.
Qed
.
End
automation
.
Global
Opaque
atomic_post_acc'
.
Unset
Universe
Polymorphism
.
theories/examples/external/reloc/class_instances_reloc_logatom.v
0 → 100644
View file @
ec9601fe
From
diaframe
.
examples
.
external
.
reloc
Require
Import
reloc_automation_base
atomic_post_update
.
From
diaframe
.
heap_lang
Require
Import
stepping_tacs
atomic_instances_heaplang
.
Section
atomic_compat
.
Context
`
{!
relocG
Σ
}.
Global
Instance
atomic_templateM_satisfies_wp_template_condition
P1
(
TT1
TT2
:
tele
)
P2
Q1
Q2
e
A
Ef
:
(
∀
..
(
tt1
:
TT1
)
(
tt2
:
TT2
),
TCEq
(
tele_app
(
tele_app
Q1
tt1
)
tt2
)
True
%
I
)
→
(* it seems we cant prove this if there is a private postcondition? but why? *)
defs
.
SatisfiesTemplateCondition
(
class_instances_reloc
.
left_template_condition
)
[
tele_arg
e
;
⊤;
A
]
(
atomic_templateM
∅
P1
TT1
TT2
P2
Q1
Q2
)
[
tele_arg
e
;
Ef
;
A
]
(
atomic_post_templateM
∅
P1
Ef
TT1
TT2
P2
Q1
Q2
).
Proof
.
do
3
split
=>
//.
-
move
=>
Ψ
.
iIntros
">[$ H] !> !>"
.
rewrite
atomic_post_update_equiv
.
iApply
atomic_post_update_mask_change
.
iApply
(
atomic_post_update_mono
with
"H"
).
iIntros
"!>"
.
iSplit
;
eauto
.
iIntros
(
a
).
iExists
id
.
iSplit
;
eauto
.
iIntros
(
b
)
"HQ"
.
simpl
.
revert
H
=>
/(
dep_eval_tele
a
)
/(
dep_eval_tele
b
)
->.
iIntros
"!>"
.
rewrite
difference_empty_L
.
iMod
(
"HQ"
with
"[]"
)
as
"$"
;
eauto
.
-
split
=>
//.
apply
atomic_post_templateM_is_mono
.
apply
:
atomic_post_templateM_is_absorbing
.
Qed
.
End
atomic_compat
.
\ No newline at end of file
theories/examples/external/reloc/counter.v
0 → 100644
View file @
ec9601fe
From
reloc
.
lib
Require
Import
lock
counter
.
From
diaframe
.
examples
.
external
.
reloc
Require
Import
reloc_automation_base
class_instances_reloc_logatom
.
From
diaframe
.
heap_lang
Require
Import
stepping_tacs
atomic_instances_heaplang
.
Section
fg_spec
.
Context
`
{!
heapGS
Σ
}.
Global
Instance
fg_increment_spec
(
l
:
loc
)
:
SPEC
(
z
:
Z
),
<<
l
↦
#
z
>>
FG_increment
#
l
<<
RET
#
z
;
l
↦
#(
z
+
1
)
>>.
Proof
.
iStepsS
.
iL
ö
b
as
"IH"
.
wp_lam
.
iSmash
.
Qed
.
End
fg_spec
.
Section
counter_refinement
.
Context
`
{!
relocG
Σ
}.
Lemma
FG_CG_increment_refinement
lk
cnt
cnt'
:
inv
counterN
(
counter_inv
lk
cnt
cnt'
)
-
∗
REL
FG_increment
#
cnt
<<
CG_increment
#
cnt'
lk
:
lrel_int
.
Proof
.
iStepsS
.
rel_rec_r
.
iStepsS
.
Qed
.
End
counter_refinement
.
\ No newline at end of file
theories/examples/external/reloc/reloc_automation_base.v
View file @
ec9601fe
...
...
@@ -93,6 +93,10 @@ Section main.
Global
Opaque
spec_ctx
.
Global
Instance
ghost_mapsto_vals
l
v1
v2
:
HINT
l
↦ₛ
v1
✱
[
⌜
v1
=
v2
⌝
]
⊫
[
id
]
;
l
↦ₛ
v2
✱
[
⌜
v1
=
v2
⌝
]
|
55
.
Proof
.
iStepsS
.
Qed
.
Section
lock_n_stack_specs
.
(* spin lock specs as tp executions, so that automation can apply them *)
(* spec notation only works for wp_red_cond, so this uses the more explicit reductionstep *)
...
...
theories/examples/external/reloc/stack_refinement.v
View file @
ec9601fe
...
...
@@ -147,7 +147,7 @@ Section proof.
rewrite
bi
.
intuitionistically_if_elim
right_id
;
iStepS
.
iDestruct
(
big_sepL2_length
with
"H1"
)
as
%
Hfoo
;
iRevert
"H1"
.
(* TODO: if Hfoo is not cleared, True and False are repeatedly normalized into eachother !! *)
destruct
rs
as
[|
r
rs
]
;
clear
Hfoo
;
iStepsS
.
destruct
rs
as
[|
r
rs
]
;
iStepsS
.
Qed
.
Lemma
FG_CG_pop_refinement
N
st
st'
(
A
:
lrel
Σ
)
:
...
...
theories/examples/external/reloc/ticket_lock_refinement.v
View file @
ec9601fe
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** Ticket lock refines a simple spin lock *)
From
diaframe
.
examples
.
external
.
reloc
Require
Import
reloc_automation_base
.
From
diaframe
.
lib
Require
Import
own_hints
.
From
diaframe
.
examples
.
external
.
reloc
Require
Import
reloc_automation_base
counter
.
From
diaframe
.
lib
Require
Import
own_hints
ticket_cmra
.
From
iris
.
algebra
Require
Export
auth
gset
.
From
reloc
.
lib
Require
Import
lock
counter
.
...
...
@@ -21,37 +21,21 @@ Definition lrel_lock `{relocG Σ} : lrel Σ :=
∃
A
,
(()
→
A
)
*
(
A
→
())
*
(
A
→
()).
Class
tlockG
Σ
:
=
tlock_G
:
>
inG
Σ
(
authR
(
gset_disjUR
nat
))
.
Definition
tlock
Σ
:
gFunctors
:
=
#[
GFunctor
(
authR
$
gset_disjUR
nat
)
].
tlock_G
:
>
inG
Σ
ticketUR
.
Definition
tlock
Σ
:
gFunctors
:
=
#[
GFunctor
ticketUR
].
Global
Instance
subG_tlock
Σ
{
Σ
}
:
subG
tlock
Σ
Σ
→
tlockG
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
set_seq_update
.
Global
Instance
set_seq_disj_union_update
n
m
m'
:
SolveSepSideCondition
(
m'
=
S
m
)
→
FindLocalUpdate
(
GSet
(
set_seq
n
m
))
(
GSet
(
set_seq
n
m'
))
(
GSet
∅
)
(
GSet
{[
n
+
m
]})
True
|
50
.
Proof
.
rewrite
/
SolveSepSideCondition
/
FindLocalUpdate
=>
->
_
.
eapply
set_local_update
.
-
rewrite
difference_empty_L
.
rewrite
set_seq_S_end_union_L
.
assert
(({[
n
+
m
]}
:
gset
nat
)
##
(
set_seq
n
m
)).
{
eapply
set_seq_S_end_disjoint
.
}
set_solver
.
-
rewrite
set_seq_S_end_union_L
.
set_solver
.
Qed
.
End
set_seq_update
.
Section
refinement
.
Context
`
{!
relocG
Σ
,
!
tlockG
Σ
}.
(*, !lockPoolG Σ}.*)
(** * Basic abstractions around the concrete RA *)
(** ticket with the id `n` *)
Definition
ticket
(
γ
:
gname
)
(
n
:
nat
)
:
=
own
γ
(
◯
GSet
{[
n
]}
).
Definition
ticket
(
γ
:
gname
)
(
n
:
nat
)
:
=
own
γ
(
CoPset
$
ticket
n
).
(** total number of issued tickets is `n` *)
Definition
issuedTickets
(
γ
:
gname
)
(
n
:
nat
)
:
=
own
γ
(
●
GSet
(
set_s
eq
0
n
)
)
.
Definition
issuedTickets
(
γ
:
gname
)
(
n
:
nat
)
:
=
own
γ
(
CoPset
$
tickets_g
eq
$
n
).
(** * Invariants and abstracts for them *)
Definition
lockInv
(
lo
ln
:
loc
)
(
γ
:
gname
)
(
l'
:
val
)
:
iProp
Σ
:
=
...
...
@@ -68,9 +52,7 @@ Section refinement.
(* Allocating a new lock *)
Lemma
newlock_refinement
:
⊢
REL
newlock
<<
reloc
.
lib
.
lock
.
newlock
:
()
→
lockInt
.
Proof
.
iStepsS
.
Qed
.
Proof
.
iStepsS
.
Qed
.
(* Acquiring a lock *)
(* helper lemma *)
...
...
@@ -84,120 +66,24 @@ Section refinement.
rel_rec_l
.
iStepsS
.
-
(* pure execution cannot introduce a new variable here! :) *)
case_decide
;
simplify_eq
/=
;
[
set_solver
|
]
.
iStepsS
.
all
:
set_solver
.
case_decide
;
simplify_eq
/=.
iStepsS
.
-
case_decide
;
simplify_eq
/=.
*
iStepsS
;
set_solver
.
*
iStepsS
.
Qed
.
(** Logically atomic spec for `acquire`.
Parameter type: nat
Precondition:
λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n
Postcondition:
λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n ∗ ticket γ o *)
Lemma
acquire_l_logatomic
R
P
γ
E
K
lo
ln
t
A
:
P
-
∗
□
(|={
⊤
,
E
}=>
∃
o
n
:
nat
,
lo
↦
#
o
∗
ln
↦
#
n
∗
issuedTickets
γ
n
∗
R
o
∗
(
∀
o
:
nat
,
(
∃
n
:
nat
,
lo
↦
#
o
∗
ln
↦
#
n
∗
issuedTickets
γ
n
∗
R
o
)
={
E
,
⊤
}=
∗
True
)
∧
(
∀
o
:
nat
,
(
∃
n
:
nat
,
lo
↦
#
o
∗
ln
↦
#
n
∗
issuedTickets
γ
n
∗
ticket
γ
o
∗
R
o
)
-
∗
P
-
∗
REL
fill
K
(
of_val
#())
<<
t
@
E
:
A
))
-
∗
(
REL
fill
K
(
acquire
(#
lo
,
#
ln
)%
V
)
<<
t
:
A
).
Proof
.
iIntros
"HP #H"
.
rewrite
/
acquire
.
iStepsS
.
iIntros
"!>"
.
rel_apply_l
(
FG_increment_atomic_l
(
fun
n
:
nat
=>
∃
o
:
nat
,
lo
↦
#
o
∗
issuedTickets
γ
n
∗
R
o
)%
I
P
%
I
with
"HP"
).
iStepsS
.
iIntros
"!>"
.
iSplit
.
-
iDestruct
"H5"
as
"[H5 _]"
.
iStepsS
.
-
iDestruct
"H5"
as
"[H5 _]"
.
iStepsS
.
iRestore
.
iIntros
"!>"
.
iL
ö
b
as
"IH"
.
rel_rec_l
.
iStepsS
.
case_decide
;
simplify_eq
/=.
(* Whether the ticket is called out *)
+
iDestruct
"H8"
as
"[_ H8]"
.
iStepsS
.
+
iDestruct
"H8"
as
"[H8 _]"
.
iStepsS
.
*
iStepsS
.
Qed
.
Lemma
acquire_refinement
:
⊢
REL
acquire
<<
reloc
.
lib
.
lock
.
acquire
:
lockInt
→
().
Proof
.
do
5
iStepS
.
rel_apply_l
(
acquire_l_logatomic
(
fun
o
=>
∃
st
,
is_locked_r
x0
st
∗
(
ticket
x3
o
∗
⌜
st
=
true
⌝
∨
⌜
st
=
false
⌝
))%
I
True
%
I
x3
)
;
first
done
.
iStepsS
.
all
:
iIntros
"!>"
;
clear
;
iSplit
;
iStepsS
.
*
contradict
H0
.
set_solver
.
*
contradict
H0
.
set_solver
.
Unshelve
.
all
:
apply
inhabitant
.
-
iRestore
.
iApply
wait_loop_refinement
;
iStepsS
.
-
iRestore
.
iApply
wait_loop_refinement
;
iStepsS
.
Qed
.
Lemma
acquire_refinement_direct
:
⊢
REL
acquire
<<
reloc
.
lib
.
lock
.
acquire
:
lockInt
→
().
Proof
.
iStepsS
.
iIntros
"!>"
.
rel_apply_l
(
FG_increment_atomic_l
(
issuedTickets
x3
)%
I
True
%
I
)
;
first
done
.
iStepsS
.
all
:
iIntros
"!>"
;
iSplit
;
iStepsS
.
*
unshelve
iRestore
.
{
set_solver
.
}
iApply
wait_loop_refinement
;
iStepsS
.
set_solver
.
*
iRestore
.
iApply
wait_loop_refinement
;
iStepsS
.
Qed
.
(* Releasing the lock *)
Lemma
wkincr_l
x
(
n
:
nat
)
K
t
A
: