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
Gaurav Parthasarathy
examples_rdcss_old
Commits
9542b86d
Commit
9542b86d
authored
Dec 14, 2017
by
Amin Timany
Browse files
Add the spanning tree algorithm
parent
c3a8a2a3
Changes
6
Expand all
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
9542b86d
...
...
@@ -44,6 +44,8 @@ This repository contains the following case studies:
*
Binary logical relations for proving contextual refinements
-
Proof of refinement for a pair of fine-grained/coarse-grained concurrent counter implementations
-
Proof of refinement for a pair of fine-grained/coarse-grained concurrent stack implementations
*
[
spanning-tree
](
theories/spanning_tree
)
: Proof of partial functional
correctness of a concurrent spanning tree algorithm.
## For Developers: How to update the Iris dependency
...
...
_CoqProject
View file @
9542b86d
...
...
@@ -48,3 +48,8 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/spanning_tree/graph.v
theories/spanning_tree/mon.v
theories/spanning_tree/spanning.v
theories/spanning_tree/proof.v
theories/spanning_tree/graph.v
0 → 100644
View file @
9542b86d
From
iris
.
algebra
Require
Import
base
gmap
.
From
stdpp
Require
Import
gmap
mapset
.
Section
Graphs
.
Context
{
T
:
Type
}
{
HD
:
EqDecision
T
}
{
HC
:
@
Countable
T
HD
}.
Definition
graph
:
=
gmap
T
(
option
T
*
option
T
).
Identity
Coercion
graph_to_gmap
:
graph
>->
gmap
.
Definition
get_left
(
g
:
graph
)
x
:
option
T
:
=
g
!!
x
≫
=
fst
.
Definition
get_right
(
g
:
graph
)
x
:
option
T
:
=
g
!!
x
≫
=
snd
.
Definition
strict_sub_child
(
ch
ch'
:
option
T
)
:
=
match
ch
,
ch'
with
|
Some
c
,
Some
c'
=>
c
=
c'
|
Some
c
,
None
=>
True
|
None
,
Some
_
=>
False
|
None
,
None
=>
True
end
.
Definition
strict_sub_children
(
ch
ch'
:
option
T
*
option
T
)
:
Prop
:
=
strict_sub_child
(
ch
.
1
)
(
ch'
.
1
)
∧
strict_sub_child
(
ch
.
2
)
(
ch'
.
2
).
Definition
strict_subgraph
(
g
g'
:
graph
)
:
Prop
:
=
∀
x
,
strict_sub_children
(
get_left
g
x
,
get_right
g
x
)
(
get_left
g'
x
,
get_right
g'
x
).
(* A path is a list of booleans true for left child and false for the right *)
(* The empty list is the identity trace (from x to x). *)
Definition
path
:
=
list
bool
.
Identity
Coercion
path_to_list
:
path
>->
list
.
Inductive
valid_path
(
g
:
graph
)
(
x
y
:
T
)
:
path
→
Prop
:
=
|
valid_path_E
:
x
∈
dom
(
gset
_
)
g
→
x
=
y
→
valid_path
g
x
y
[]
|
valid_path_l
(
xl
:
T
)
p
:
get_left
g
x
=
Some
xl
→
valid_path
g
xl
y
p
→
valid_path
g
x
y
(
true
::
p
)
|
valid_path_r
(
xr
:
T
)
p
:
get_right
g
x
=
Some
xr
→
valid_path
g
xr
y
p
→
valid_path
g
x
y
(
false
::
p
).
Definition
connected
(
g
:
graph
)
(
x
:
T
)
:
=
∀
z
,
z
∈
dom
(
gset
_
)
g
→
∃
p
,
valid_path
g
x
z
p
.
Definition
front
(
g
:
graph
)
(
t
t'
:
gset
T
)
:
=
t
⊆
dom
(
gset
_
)
g
∧
∀
x
v
,
x
∈
t
→
(
get_left
g
x
=
Some
v
)
∨
(
get_right
g
x
=
Some
v
)
→
v
∈
t'
.
Definition
maximal
(
g
:
graph
)
:
=
front
g
(
dom
(
gset
_
)
g
)
(
dom
(
gset
_
)
g
).
Definition
tree
(
g
:
graph
)
(
x
:
T
)
:
=
∀
z
,
z
∈
dom
(
gset
_
)
g
→
exists
!
p
,
valid_path
g
x
z
p
.
(* graph facts *)
Lemma
front_t_t_dom
g
z
t
:
z
∈
t
→
connected
g
z
→
front
g
t
t
→
t
=
dom
(
gset
_
)
g
.
Proof
.
intros
Hz
Hc
[
Hsb
Hdt
].
apply
collection_equiv_spec_L
;
split
;
trivial
.
apply
elem_of_subseteq
=>
x
Hx
.
destruct
(
Hc
x
Hx
)
as
[
p
pv
].
clear
Hc
Hx
;
revert
z
Hz
pv
.
induction
p
=>
z
Hz
pv
.
-
by
inversion
pv
;
subst
.
-
inversion
pv
as
[|?
?
Hpv1
Hpv2
Hpv3
|?
?
Hpv1
Hpv2
Hpv3
]
;
subst
.
+
eapply
IHp
;
[
eapply
Hdt
|
apply
Hpv2
]
;
eauto
.
+
eapply
IHp
;
[
eapply
Hdt
|
apply
Hpv2
]
;
eauto
.
Qed
.
Lemma
front_mono
g
t
t'
s
:
front
g
t
t'
→
t'
⊆
s
→
front
g
t
s
.
Proof
.
intros
[
Htd
Hf
]
Hts
;
split
;
eauto
.
Qed
.
Lemma
front_empty
g
:
front
g
∅
∅
.
Proof
.
split
;
auto
.
intros
?
Hcn
;
inversion
Hcn
.
Qed
.
Lemma
strict_sub_children_refl
v
:
strict_sub_children
v
v
.
Proof
.
by
destruct
v
as
[[]
[]].
Qed
.
Lemma
strict_sub_children_trans
v1
v2
v3
:
strict_sub_children
v1
v2
→
strict_sub_children
v2
v3
→
strict_sub_children
v1
v3
.
Proof
.
destruct
v1
as
[[]
[]]
;
destruct
v2
as
[[]
[]]
;
destruct
v3
as
[[]
[]]
;
cbv
;
by
intuition
subst
.
Qed
.
Lemma
strict_sub_children_None
v
:
strict_sub_children
v
(
None
,
None
).
Proof
.
by
destruct
v
as
[[]
[]].
Qed
.
Lemma
strict_subgraph_empty
g
:
strict_subgraph
g
∅
.
Proof
.
intros
i
.
rewrite
/
get_left
/
get_right
/
strict_sub_child
lookup_empty
//=.
by
destruct
(
g
!!
i
)
as
[[[]
[]]|].
Qed
.
Lemma
get_left_dom
g
x
y
:
get_left
g
x
=
Some
y
→
x
∈
dom
(
gset
_
)
g
.
Proof
.
rewrite
/
get_left
elem_of_dom
.
case
_
:
(
g
!!
x
)
;
inversion
1
;
eauto
.
Qed
.
Lemma
get_right_dom
g
x
y
:
get_right
g
x
=
Some
y
→
x
∈
dom
(
gset
_
)
g
.
Proof
.
rewrite
/
get_right
elem_of_dom
.
case
_
:
(
g
!!
x
)
;
inversion
1
;
eauto
.
Qed
.
Lemma
path_start
g
x
y
p
:
valid_path
g
x
y
p
→
x
∈
dom
(
gset
_
)
g
.
Proof
.
inversion
1
;
subst
;
eauto
using
get_left_dom
,
get_right_dom
.
Qed
.
Lemma
path_end
g
x
y
p
:
valid_path
g
x
y
p
→
y
∈
dom
(
gset
_
)
g
.
Proof
.
induction
1
;
subst
;
eauto
.
Qed
.
End
Graphs
.
Arguments
graph
_
{
_
_
}.
\ No newline at end of file
theories/spanning_tree/mon.v
0 → 100644
View file @
9542b86d
This diff is collapsed.
Click to expand it.
theories/spanning_tree/proof.v
0 → 100644
View file @
9542b86d
From
iris
.
algebra
Require
Import
frac
gmap
auth
.
From
iris
.
base_logic
Require
Export
invariants
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
heap_lang
Require
Export
lifting
notation
.
From
iris
.
heap_lang
.
lib
Require
Import
par
.
From
iris
.
base_logic
Require
Import
cancelable_invariants
.
Import
uPred
.
From
iris_examples
.
spanning_tree
Require
Import
graph
mon
spanning
.
Section
wp_span
.
Context
`
{
heapG
Σ
,
cinvG
Σ
,
inG
Σ
(
authR
markingUR
),
inG
Σ
(
authR
graphUR
),
spawnG
Σ
}.
Lemma
wp_span
g
(
markings
:
gmap
loc
loc
)
(
x
:
val
)
(
l
:
loc
)
:
l
∈
dom
(
gset
loc
)
g
→
maximal
g
→
connected
g
l
→
([
∗
map
]
l
↦
v
∈
g
,
∃
(
m
:
loc
),
⌜
markings
!!
l
=
Some
m
⌝
∗
l
↦
(#
m
,
children_to_val
v
)
∗
m
↦
#
false
)
⊢
WP
span
(
SOME
#
l
)
{{
_
,
∃
g'
,
([
∗
map
]
l
↦
v
∈
g'
,
∃
m
:
loc
,
⌜
markings
!!
l
=
Some
m
⌝
∗
l
↦
(#
m
,
children_to_val
v
)
∗
m
↦
#
true
)
∗
⌜
dom
(
gset
loc
)
g
=
dom
(
gset
loc
)
g'
⌝
∗
⌜
strict_subgraph
g
g'
⌝
∗
⌜
tree
g'
l
⌝
}}.
Proof
.
iIntros
(
Hgl
Hgmx
Hgcn
)
"Hgr"
.
iMod
(
graph_ctx_alloc
_
g
markings
with
"[Hgr]"
)
as
(
Ig
κ
)
"(key & #Hgr & Hg)"
;
eauto
.
iApply
wp_fupd
.
iApply
wp_wand_l
;
iSplitR
;
[|
iApply
((
rec_wp_span
κ
g
markings
1
1
(
SOMEV
#
l
))
with
"[Hg key]"
)
;
eauto
;
iFrame
"#"
;
iFrame
].
iIntros
(
v
)
"[H key]"
.
unfold
graph_ctx
.
iMod
(
cinv_cancel
⊤
graphN
κ
(
graph_inv
g
markings
)
with
"[#] [key]"
)
as
">Hinv"
;
first
done
;
try
by
iFrame
.
iClear
"Hgr"
.
unfold
graph_inv
.
iDestruct
"Hinv"
as
(
G
)
"(Hi1 & Hi2 & Hi3 & Hi4)"
.
iDestruct
"Hi4"
as
%
Hi4
.
iDestruct
"H"
as
"[H|H]"
.
-
iDestruct
"H"
as
"(_ & H)"
.
iDestruct
"H"
as
(
l'
)
"(H1 & H2 & Hl')"
.
iDestruct
"H1"
as
%
Hl
;
inversion
Hl
;
subst
.
iDestruct
"H2"
as
(
G'
gmr
gtr
)
"(Hl1 & Hl2 & Hl3 & Hl4 & Hl5)"
.
iDestruct
"Hl2"
as
%
Hl2
.
iDestruct
"Hl3"
as
%
Hl3
.
iDestruct
"Hl4"
as
%
Hl4
.
iDestruct
(
whole_frac
with
"[Hi1 Hl1]"
)
as
%
Heq
;
[
by
iFrame
|]
;
subst
.
iDestruct
(
marked_is_marked_in_auth_sepS
with
"[Hi2 Hl5]"
)
as
%
Hmrk
;
[
by
iFrame
|].
iDestruct
(
own_graph_valid
with
"Hl1"
)
as
%
Hvl
.
iExists
(
Gmon_graph
G'
).
assert
(
dom
(
gset
positive
)
g
=
dom
(
gset
positive
)
(
Gmon_graph
G'
)).
{
erewrite
front_t_t_dom
;
eauto
.
-
by
rewrite
Gmon_graph_dom
.
-
eapply
front_mono
;
rewrite
Gmon_graph_dom
;
eauto
.
}
iModIntro
.
repeat
iSplitL
;
try
by
iPureIntro
.
rewrite
/
heap_owns
of_graph_dom_eq
//=.
by
rewrite
big_sepM_fmap
/=.
-
iDestruct
"H"
as
"(_ & [H|H] & Hx)"
.
+
iDestruct
"H"
as
%
Heq
.
inversion
Heq
.
+
iDestruct
"H"
as
(
l'
)
"(_ & Hl)"
.
iDestruct
(
marked_is_marked_in_auth
with
"[Hi2 Hl]"
)
as
%
Hmrk
;
[
by
iFrame
|].
iDestruct
(
whole_frac
with
"[Hx Hi1]"
)
as
%
Heq
;
[
by
iFrame
|]
;
subst
.
exfalso
;
revert
Hmrk
.
rewrite
dom_empty
.
inversion
1
.
Qed
.
End
wp_span
.
\ No newline at end of file
theories/spanning_tree/spanning.v
0 → 100644
View file @
9542b86d
This diff is collapsed.
Click to expand it.
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