Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
E
examples
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
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
Paolo G. Giarrusso
examples
Commits
31b7db5f
Verified
Commit
31b7db5f
authored
Jun 04, 2019
by
Rodolphe Lepigre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
New conditional increment example.
parent
08108eb8
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
986 additions
and
0 deletions
+986
0
_CoqProject
_CoqProject
+1
0
theories/logatom/cinc.v
theories/logatom/cinc.v
+985
0
No files found.
_CoqProject
View file @
31b7db5f
...
...
@@ 91,6 +91,7 @@ theories/hocap/lib/oneshot.v
theories/hocap/concurrent_runners.v
theories/hocap/parfib.v
theories/logatom/cinc.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/elimination_stack/hocap_spec.v
...
...
theories/logatom/cinc.v
0 → 100644
View file @
31b7db5f
From
iris
.
algebra
Require
Import
excl
auth
agree
frac
list
cmra
.
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
From
iris
.
program_logic
Require
Export
atomic
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
Import
uPred
bi
List
Decidable
.
Set
Default
Proof
Using
"Type"
.
(** Using prophecy variables with helping: implementing conditional counter from
"Logical Relations for FineGrained Concurrency" by Turon et al. (POPL 2013) *)
(** * Implementation of the functions. *)
(*
new_counter() :=
let c = ref (injL 0) in
let f = ref false in
ref (f, c)
*)
Definition
new_counter
:
val
:
=
λ
:
<>,
let
:
"c"
:
=
ref
(
ref
(
InjL
#
0
))
in
let
:
"f"
:
=
ref
#
true
in
(
"f"
,
"c"
).
(*
set_flag(ctr, b) :=
ctr.1 < b
*)
Definition
set_flag
:
val
:
=
λ
:
"ctr"
"b"
,
Fst
"ctr"
<
"b"
.
(*
complete(c, f, x, n, p) :=
Resolve CAS(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
*)
Definition
complete
:
val
:
=
λ
:
"c"
"f"
"x"
"n"
"p"
,
Resolve
(
CAS
"c"
"x"
(
ref
(
InjL
(
if
:
!
"f"
then
"n"
+
#
1
else
"n"
))))
"p"
(
ref
#())
;;
#().
(*
get(c, f) :=
let x = !c in
match !x with
 injL n => n
 injR (n, p) => complete c f x n p; get(c, f)
*)
Definition
get
:
val
:
=
rec
:
"get"
"ctr"
:
=
let
:
"f"
:
=
Fst
"ctr"
in
let
:
"c"
:
=
Snd
"ctr"
in
let
:
"x"
:
=
!
"c"
in
match
:
!
"x"
with
InjL
"n"
=>
"n"

InjR
"args"
=>
complete
"c"
"f"
"x"
(
Fst
"args"
)
(
Snd
"args"
)
;;
"get"
"ctr"
end
.
(*
cinc(c, f) :=
let x = !c in
match !x with
 injL n =>
let p := new proph in
let y := ref (injR (n, p)) in
if CAS(c, x, y) then complete(c, f, y, n, p)
else cinc(c, f)
 injR (n, p) =>
complete(c, f, x, n, p);
cinc(c, f)
*)
Definition
cinc
:
val
:
=
rec
:
"cinc"
"ctr"
:
=
let
:
"f"
:
=
Fst
"ctr"
in
let
:
"c"
:
=
Snd
"ctr"
in
let
:
"x"
:
=
!
"c"
in
match
:
!
"x"
with
InjL
"n"
=>
let
:
"p"
:
=
NewProph
in
let
:
"y"
:
=
ref
(
InjR
(
"n"
,
"p"
))
in
if
:
CAS
"c"
"x"
"y"
then
complete
"c"
"f"
"y"
"n"
"p"
;;
Skip
else
"cinc"
"ctr"

InjR
"args'"
=>
complete
"c"
"f"
"x"
(
Fst
"args'"
)
(
Snd
"args'"
)
;;
"cinc"
"ctr"
end
.
(** ** Proof setup *)
(** To represent histories of allocated locations, we need some helper lemmas
about suffixes on lists. *)
Section
suffixes
.
Lemma
suffix_trans
(
h1
h2
h3
:
list
loc
)
:
h1
`
suffix_of
`
h2
→
h2
`
suffix_of
`
h3
→
h1
`
suffix_of
`
h3
.
Proof
.
intros
[?
>]
[?
>].
rewrite
app_assoc
.
by
eexists
.
Qed
.
Lemma
suffix_eq
(
h1
h2
:
list
loc
)
:
h1
`
suffix_of
`
h2
→
h2
`
suffix_of
`
h1
→
h1
=
h2
.
Proof
.
intros
[
xs
>]
[
ys
Heq
].
rewrite
<
app_nil_l
in
Heq
at
1
.
rewrite
app_assoc
in
Heq
.
apply
app_inv_tail
,
eq_sym
in
Heq
.
by
apply
app_eq_nil
in
Heq
as
[
_
>].
Qed
.
Lemma
suffix_in
(
h1
h2
:
list
loc
)
l
:
h1
`
suffix_of
`
h2
→
In
l
h1
→
In
l
h2
.
Proof
.
destruct
h1
as
[
y
ys
]
;
first
done
.
intros
Hs
Hin
.
destruct
Hs
as
[
l2'
>].
apply
in_or_app
.
by
right
.
Qed
.
Lemma
suffix_in_head
(
h1
h2
:
list
loc
)
l
:
h1
`
suffix_of
`
h2
→
Some
l
=
head
h1
→
In
l
h2
.
Proof
.
destruct
h1
as
[
y
ys
]
;
first
done
.
intros
Hs
[=>].
eapply
suffix_in
;
first
done
.
apply
in_eq
.
Qed
.
(** A helper lemma that will come up in the proof of [complete] *)
Lemma
nodup_suffix_contradiction
(
l1
l2
l3
:
loc
)
(
H1
H2
H3
:
list
loc
)
:
Some
l1
=
hd_error
H1
→
Some
l2
=
hd_error
H2
→
Some
l3
=
hd_error
H3
→
In
l3
H1
→
H1
`
suffix_of
`
H2
→
H2
`
suffix_of
`
H3
→
l2
≠
l3
→
NoDup
H3
→
False
.
Proof
.
intros
Heq
Heq'
Heq''
Hin
Hs
Hs'
Hn
Hd
.
destruct
Hs'
as
[
xs
>].
destruct
Hs
as
[
ys
>].
destruct
(
in_split
_
_
Hin
)
as
(
x
&
y
&
>).
do
2
rewrite
app_assoc
in
Hd
.
apply
NoDup_remove_2
in
Hd
.
(* xs, ys, and x must be empty *)
destruct
xs
as
[
x'
xs
]
;
last
first
.
{
simpl
in
*.
inversion
Heq''
.
subst
.
contradict
Hd
.
by
left
.
}
destruct
ys
as
[
y'
ys
]
;
last
first
.
{
simpl
in
*.
inversion
Heq''
;
subst
.
contradict
Hd
.
by
left
.
}
destruct
x
as
[
z'
zs
]
;
last
first
.
{
simpl
in
*.
inversion
Heq''
;
subst
.
contradict
Hd
.
by
left
.
}
simpl
in
*.
inversion
Heq'
;
done
.
Qed
.
End
suffixes
.
(** Resource algebra for histories *)
Section
histories
.
Inductive
hist
:
=

histv
(
h
:
list
loc
)
:
hist

histbot
:
hist
.
Inductive
hist_equiv
:
Equiv
hist
:
=

Hist_equiv
h1
h2
:
h1
=
h2
→
h1
≡
h2
.
Existing
Instance
hist_equiv
.
Instance
hist_equiv_Equivalence
:
@
Equivalence
hist
equiv
.
Proof
.
split
.

move
=>
[]
;
by
constructor
.

move
=>
[?]
[]
;
inversion
1
;
subst
;
by
constructor
.

move
=>
[?]
[]
[]
;
inversion
1
;
inversion
1
;
subst
;
by
constructor
.
Qed
.
Canonical
Structure
histC
:
ofeT
:
=
discreteC
hist
.
Instance
hist_valid
:
Valid
hist
:
=
λ
x
,
match
x
with
histv
_
=>
True

histbot
=>
False
end
.
Instance
hist_op
:
Op
hist
:
=
λ
h1
h2
,
match
h1
,
h2
with

histv
h1'
,
histv
h2'
=>
if
decide
(
h1'
`
suffix_of
`
h2'
)
then
h2
else
if
decide
(
h2'
`
suffix_of
`
h1'
)
then
h1
else
histbot

_
,
_
=>
histbot
end
.
Arguments
op
_
_
!
_
!
_
/.
Instance
hist_PCore
:
PCore
hist
:
=
Some
.
Global
Instance
hist_op_comm
:
Comm
equiv
hist_op
.
Proof
.
intros
[
h1
]
[
h2
]
;
auto
.
simpl
.
case_decide
as
H1
;
[
case_decide
as
H2

auto
]
;
last
auto
.
constructor
.
destruct
H1
.
subst
.
destruct
H2
.
rewrite
<
app_nil_l
in
H
at
1
.
rewrite
app_assoc
in
H
.
by
apply
app_inv_tail
,
eq_sym
,
app_eq_nil
in
H
as
[>
>].
Qed
.
Global
Instance
hist_op_idemp
:
IdemP
eq
hist_op
.
Proof
.
intros
[]
;
[
by
simpl
;
rewrite
decide_True

auto
].
Qed
.
Lemma
hist_op_l
h1
h2
(
Le
:
h1
`
suffix_of
`
h2
)
:
histv
h1
⋅
histv
h2
=
histv
h2
.
Proof
.
simpl
.
case_decide
;
done
.
Qed
.
Lemma
hist_op_r
h1
h2
(
Le
:
h1
`
suffix_of
`
h2
)
:
histv
h2
⋅
histv
h1
=
histv
h2
.
Proof
.
simpl
.
case_decide
.

f_equal
.
by
apply
suffix_eq
.

by
case_decide
.
Qed
.
Global
Instance
hist_op_assoc
:
Assoc
equiv
(
op
:
Op
hist
).
Proof
.
intros
[
h1
]
[
h2
]
[
h3
]
;
eauto
;
simpl
.

repeat
(
case_decide
;
auto
).
+
rewrite
!
hist_op_l
;
auto
.
etrans
;
eauto
.
+
simpl
.
repeat
case_decide
;
last
done
.
*
destruct
H
as
[
xs
>].
destruct
H2
as
[
ys
[[
k
[>>]]

[
k
[>>]]]%
app_eq_inv
].
**
contradict
H1
.
by
apply
suffix_app_r
.
**
contradict
H0
.
by
apply
suffix_app_r
.
*
contradict
H1
.
by
etrans
.
+
rewrite
hist_op_l
;
[
by
rewrite
hist_op_r

auto
].
+
rewrite
!
hist_op_r
;
auto
.
by
etrans
.
+
simpl
.
rewrite
!
decide_False
;
auto
.
+
simpl
.
rewrite
!
decide_False
;
auto
.
+
simpl
.
case_decide
.
*
exfalso
.
apply
H
.
by
etrans
.
*
case_decide
;
last
done
.
exfalso
.
destruct
H4
as
[
xs
>].
destruct
H2
as
[
ys
[[
k
[>>]]

[
k
[>>]]]%
app_eq_inv
].
**
contradict
H0
.
by
apply
suffix_app_r
.
**
contradict
H
.
by
apply
suffix_app_r
.

simpl
.
repeat
case_decide
;
auto
.
Qed
.
Lemma
hist_included
h1
h2
:
histv
h1
≼
histv
h2
↔
h1
`
suffix_of
`
h2
.
Proof
.
split
.

move
=>
[[?]]
;
simpl
;
last
by
inversion
1
.
case_decide
.
*
inversion
1
.
naive_solver
.
*
case_decide
;
inversion
1
;
naive_solver
.

intros
.
exists
(
histv
h2
).
by
rewrite
hist_op_l
.
Qed
.
Lemma
hist_valid_op
h1
h2
:
✓
(
histv
h1
⋅
histv
h2
)
→
h1
`
suffix_of
`
h2
∨
h2
`
suffix_of
`
h1
.
Proof
.
simpl
.
case_decide
;
first
by
left
.
case_decide
;
[
by
right

done
].
Qed
.
Lemma
hist_core_self
(
X
:
hist
)
:
core
X
=
X
.
Proof
.
done
.
Qed
.
Instance
hist_unit
:
Unit
hist
:
=
histv
nil
.
Definition
hist_ra_mixin
:
RAMixin
hist
.
Proof
.
apply
ra_total_mixin
;
eauto
.

intros
[?]
[?]
[?]
;
auto
;
inversion
1
;
naive_solver
.

by
destruct
1
;
constructor
.

destruct
1
.
naive_solver
.

apply
hist_op_assoc
.

apply
hist_op_comm
.

intros
?.
by
rewrite
hist_core_self
idemp_L
.

intros
[]
[]
;
simpl
;
done
.
Qed
.
Canonical
Structure
histR
:
=
discreteR
hist
hist_ra_mixin
.
Global
Instance
hist_cmra_discrete
:
CmraDiscrete
histR
.
Proof
.
apply
discrete_cmra_discrete
.
Qed
.
Global
Instance
hist_core
(
h
:
hist
)
:
CoreId
h
.
Proof
.
rewrite
/
CoreId
.
reflexivity
.
Qed
.
Definition
hist_ucmra_mixin
:
UcmraMixin
hist
.
Proof
.
split
;
[
done


auto
].
intros
[]
;
[
simpl

done
].
done
.
Qed
.
Lemma
hist_local_update
h1
X
h2
:
h1
`
suffix_of
`
h2
→
(
histv
h1
,
X
)
~l
~>
(
histv
h2
,
histv
h2
).
Proof
.
intros
Le
.
rewrite
local_update_discrete
.
move
=>
[[
h3
]]
/=
?
Eq
;
split
=>
//
;
last
first
;
move
:
Eq
.

destruct
X
;
by
inversion
1
.

destruct
X
;
rewrite
/
cmra_op
/=
=>
Eq
;
repeat
case_decide
;
auto
;
inversion
Eq
;
subst
;
try
naive_solver
.
+
constructor
.
inversion
H1
.
subst
.
f_equal
.
by
apply
suffix_eq
.
+
constructor
.
inversion
H2
.
subst
.
f_equal
.
apply
suffix_eq
;
by
etrans
.
+
inversion
H3
;
subst
.
by
apply
(
suffix_trans
_
_
_
H0
)
in
Le
.
Qed
.
Canonical
Structure
histUR
:
=
UcmraT
hist
hist_ucmra_mixin
.
End
histories
.
Definition
histListUR
:
=
optionUR
$
prodR
fracR
$
agreeR
$
listC
locC
.
Definition
historyUR
:
=
prodUR
(
authUR
histListUR
)
(
authUR
histUR
).
Definition
flagUR
:
=
authR
$
optionUR
$
exclR
boolC
.
Definition
numUR
:
=
authR
$
optionUR
$
exclR
ZC
.
Definition
tokenUR
:
=
authR
$
optionUR
$
exclR
valC
.
Class
cincG
Σ
:
=
ConditionalIncrementG
{
cinc_historyG
:
>
inG
Σ
historyUR
;
cinc_flagG
:
>
inG
Σ
flagUR
;
cinc_numG
:
>
inG
Σ
numUR
;
cinc_tokenG
:
>
inG
Σ
tokenUR
;
}.
Definition
cinc
Σ
:
gFunctors
:
=
#[
GFunctor
historyUR
;
GFunctor
flagUR
;
GFunctor
numUR
;
GFunctor
tokenUR
].
Instance
subG_cinc
Σ
{
Σ
}
:
subG
cinc
Σ
Σ
→
cincG
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
conditional_counter
.
Context
{
Σ
}
`
{!
heapG
Σ
,
!
cincG
Σ
}.
Context
(
N
:
namespace
).
Local
Definition
stateN
:
=
N
.@
"state"
.
Local
Definition
counterN
:
=
N
.@
"counter"
.
Definition
token
:
tokenUR
:
=
●
Excl'
#().
Definition
histList
(
H
:
list
loc
)
(
q
:
Qp
)
:
histListUR
:
=
Some
(
q
,
to_agree
H
).
Definition
half_history_frag
(
H
:
list
loc
)
:
historyUR
:
=
(
◯
(
histList
H
(
1
/
2
)%
Qp
),
◯
(
histv
H
)).
Definition
full_history_frag
(
H
:
list
loc
)
:
historyUR
:
=
(
◯
(
histList
H
1
%
Qp
),
◯
(
histv
H
)).
Definition
full_history_auth
(
H
:
list
loc
)
:
historyUR
:
=
(
●
(
histList
H
1
%
Qp
),
●
(
histv
H
)).
Definition
hist_snapshot
H
:
historyUR
:
=
(
◯
None
,
◯
histv
H
).
Global
Instance
snapshot_persistent
H
γ
_h
:
Persistent
(
own
γ
_h
(
hist_snapshot
H
)).
Proof
.
apply
own_core_persistent
.
rewrite
/
CoreId
.
done
.
Qed
.
(** Updating and synchronizing history RAs *)
Lemma
sync_histories
H1
H2
γ
_h
:
own
γ
_h
(
half_history_frag
H1
)

∗
own
γ
_h
(
half_history_frag
H2
)

∗
⌜
H1
=
H2
⌝
.
Proof
.
iIntros
"H1 H2"
.
iCombine
"H1"
"H2"
as
"H"
.
iPoseProof
(
own_valid
with
"H"
)
as
"H"
.
iDestruct
"H"
as
%
H
.
iPureIntro
.
destruct
H
as
[[
_
Hl1
%
agree_op_inv
]
_
].
by
apply
to_agree_inj
,
leibniz_equiv
in
Hl1
.
Qed
.
Lemma
add_half_histories
(
H
:
list
loc
)
γ
_h
:
own
γ
_h
(
half_history_frag
H
)

∗
own
γ
_h
(
half_history_frag
H
)

∗
own
γ
_h
(
full_history_frag
H
).
Proof
.
iIntros
"H1 H2"
.
iCombine
"H1"
"H2"
as
"H"
.
done
.
Qed
.
Lemma
update_history
H
H'
l
γ
_h
:
own
γ
_h
(
full_history_auth
H
)

∗
own
γ
_h
(
half_history_frag
H
)

∗
own
γ
_h
(
half_history_frag
H'
)
==
∗
own
γ
_h
(
full_history_auth
(
l
::
H
))
∗
own
γ
_h
(
half_history_frag
(
l
::
H
))
∗
own
γ
_h
(
half_history_frag
(
l
::
H
)).
Proof
.
iIntros
"H● H1◯ H2◯"
.
iDestruct
(
sync_histories
with
"H1◯ H2◯"
)
as
%<.
iDestruct
(
add_half_histories
with
"H1◯ H2◯"
)
as
"H◯"
.
iCombine
"H● H◯"
as
"H"
.
rewrite

own_op

own_op
.
iApply
(
own_update
with
"H"
).
apply
prod_update
.

apply
auth_update
,
option_local_update
.
rewrite
pair_op
frac_op'
agree_idemp
.
rewrite
Qp_div_2
.
apply
exclusive_local_update
.
by
constructor
.

apply
auth_update
.
simpl
.
rewrite
hist_op_l
;
last
done
.
by
apply
hist_local_update
,
suffix_cons_r
.
Qed
.
Lemma
sync_snapshot
H1
H2
H2'
γ
_h
:
own
γ
_h
(
full_history_auth
H1
)

∗
own
γ
_h
(
◯
H2'
,
◯
histv
H2
)

∗
⌜
H2
`
suffix_of
`
H1
⌝
.
Proof
.
iIntros
"H● H◯"
.
iCombine
"H●"
"H◯"
as
"H"
.
by
iDestruct
(
own_valid
with
"H"
)
as
%[
_
[
Hs
%
hist_included
_
]%
auth_both_valid
].
Qed
.
Lemma
extract_snapshot
H
γ
_h
:
own
γ
_h
(
half_history_frag
H
)

∗
□
own
γ
_h
(
hist_snapshot
H
).
Proof
.
iIntros
"H"
.
iAssert
(
own
γ
_h
(
half_history_frag
H
)
∗
own
γ
_h
(
hist_snapshot
H
))%
I
with
"[H]"
as
"[_ H2]"
.
{
rewrite

own_op
pair_op
.
assert
(
◯
histList
H
(
1
/
2
)
⋅
◯
None
=
◯
(
histList
H
(
1
/
2
)
⋅
None
))
as
Heq
by
apply
auth_frag_op
.
assert
(
◯
histv
H
⋅
◯
histv
H
=
◯
(
histv
H
⋅
histv
H
))
as
Heq'
by
apply
auth_frag_op
.
rewrite
Heq
Heq'
right_id
.
rewrite
<
core_id_dup
;
first
done
.
by
rewrite
/
CoreId
.
}
rewrite
intuitionistically_into_persistently
.
by
iApply
persistent
.
Qed
.
Lemma
sync_counter_values
γ
_n
(
n
m
:
Z
)
:
own
γ
_n
(
●
Excl'
n
)

∗
own
γ
_n
(
◯
Excl'
m
)

∗
⌜
n
=
m
⌝
.
Proof
.
iIntros
"H● H◯"
.
iCombine
"H●"
"H◯"
as
"H"
.
iDestruct
(
own_valid
with
"H"
)
as
"H"
.
by
iDestruct
"H"
as
%[
H
%
Excl_included
%
leibniz_equiv
_
]%
auth_both_valid
.
Qed
.
(** Updating and synchronizing the counter and flag RAs *)
Lemma
sync_flag_values
γ
_n
(
b1
b2
:
bool
)
:
own
γ
_n
(
●
Excl'
b1
)

∗
own
γ
_n
(
◯
Excl'
b2
)

∗
⌜
b1
=
b2
⌝
.
Proof
.
iIntros
"H● H◯"
.
iCombine
"H●"
"H◯"
as
"H"
.
iDestruct
(
own_valid
with
"H"
)
as
"H"
.
by
iDestruct
"H"
as
%[
H
%
Excl_included
%
leibniz_equiv
_
]%
auth_both_valid
.
Qed
.
Lemma
update_counter_value
γ
_n
(
n1
n2
m
:
Z
)
:
own
γ
_n
(
●
Excl'
n1
)

∗
own
γ
_n
(
◯
Excl'
n2
)
==
∗
own
γ
_n
(
●
Excl'
m
)
∗
own
γ
_n
(
◯
Excl'
m
).
Proof
.
iIntros
"H● H◯"
.
iCombine
"H●"
"H◯"
as
"H"
.
rewrite

own_op
.
iApply
(
own_update
with
"H"
).
by
apply
auth_update
,
option_local_update
,
exclusive_local_update
.
Qed
.
Lemma
update_flag_value
γ
_n
(
b1
b2
b
:
bool
)
:
own
γ
_n
(
●
Excl'
b1
)

∗
own
γ
_n
(
◯
Excl'
b2
)
==
∗
own
γ
_n
(
●
Excl'
b
)
∗
own
γ
_n
(
◯
Excl'
b
).
Proof
.
iIntros
"H● H◯"
.
iCombine
"H●"
"H◯"
as
"H"
.
rewrite

own_op
.
iApply
(
own_update
with
"H"
).
by
apply
auth_update
,
option_local_update
,
exclusive_local_update
.
Qed
.
Definition
counter_content
(
γ
s
:
gname
*
gname
*
gname
)
(
c
:
bool
*
Z
)
:
=
(
own
γ
s
.
1
.
2
(
◯
Excl'
c
.
1
)
∗
own
γ
s
.
2
(
◯
Excl'
c
.
2
))%
I
.
(** Definition of the invariant *)
Fixpoint
val_to_some_loc
(
vs
:
list
(
val
*
val
))
:
option
loc
:
=
match
vs
with

(#
true
,
LitV
(
LitLoc
l
))
::
_
=>
Some
l

_
::
vs
=>
val_to_some_loc
vs

_
=>
None
end
.
Lemma
val_to_some_loc_some
vs
l
:
val_to_some_loc
vs
=
Some
l
→
∃
v1
v2
vs'
,
vs
=
(
v1
,
v2
)
::
vs'
∧
(
(
v1
=
#
true
∧
v2
=
LitV
(
LitLoc
l
))
∨
val_to_some_loc
vs'
=
Some
l
).
Proof
.
intros
H
.
destruct
vs
as
[[
v1
v2
]
vs'
]
;
first
done
.
exists
v1
,
v2
,
vs'
.
split
;
first
done
.
destruct
v1
;
try
by
right
.
destruct
l0
;
try
by
right
.
destruct
b
;
try
by
right
.
destruct
v2
;
try
by
right
.
destruct
l0
;
try
by
right
.
simpl
in
H
.
inversion
H
.
by
left
.
Qed
.
Inductive
abstract_state
:
Set
:
=

injl
:
Z
→
abstract_state

injr
:
Z
→
proph_id
→
abstract_state
.
Definition
own_token
γ
_t
:
=
(
own
γ
_t
token
)%
I
.
Definition
used_up
l
γ
_h
:
=
(
∃
H
,
□
own
γ
_h
(
hist_snapshot
H
)
∗
⌜
In
l
H
∧
Some
l
≠
head
H
⌝
)%
I
.
Definition
not_done_state
H
l
(
γ
_h
:
gname
)
:
=
(
own
γ
_h
(
half_history_frag
H
)
∗
⌜
Some
l
=
head
H
⌝
)%
I
.
Definition
pending_state
P
(
n
:
Z
)
vs
l_ghost
(
γ
_h
γ
_n
:
gname
)
:
=
(
P
∗
⌜
match
val_to_some_loc
vs
with
None
=>
True

Some
l
=>
l
=
l_ghost
end
⌝
∗
own
γ
_n
(
●
Excl'
n
))%
I
.
Definition
accepted_state
Q
vs
(
l
l_ghost
:
loc
)
(
γ
_h
:
gname
)
:
=
(
l_ghost
↦
{
1
/
2
}

∗
match
val_to_some_loc
vs
with
None
=>
True

Some
l
=>
⌜
l
=
l_ghost
⌝
∗
Q
end
)%
I
.
Definition
done_state
Q
(
l
l_ghost
:
loc
)
(
γ
_t
γ
_h
:
gname
)
:
=
((
Q
∨
own_token
γ
_t
)
∗
l_ghost
↦

∗
used_up
l
γ
_h
)%
I
.
Definition
state_inv
P
Q
(
p
:
proph_id
)
n
l
l_ghost
H
γ
_h
γ
_n
γ
_t
:
iProp
Σ
:
=
(
∃
vs
,
proph
p
vs
∗
((
not_done_state
H
l
γ
_h
∗
(
pending_state
P
n
vs
l_ghost
γ
_h
γ
_n
∨
accepted_state
Q
vs
l
l_ghost
γ
_h
))
∨
done_state
Q
l
l_ghost
γ
_t
γ
_h
))%
I
.
Definition
pau
P
Q
γ
s
:
=
(
▷
P

∗
◇
AU
<<
∀
(
b
:
bool
)
(
n
:
Z
),
counter_content
γ
s
(
b
,
n
)
>>
@
⊤
∖↑
N
,
∅
<<
counter_content
γ
s
(
b
,
(
if
b
then
n
+
1
else
n
)),
COMM
Q
>>)%
I
.
Definition
counter_inv
γ
_h
γ
_b
γ
_n
f
c
:
=
(
∃
(
b
:
bool
)
(
l
:
loc
)
(
H
:
list
loc
)
(
q
:
Qp
)
(
v
:
val
),
f
↦
#
b
∗
c
↦
#
l
∗
l
↦
{
q
}
v
∗
own
γ
_h
(
full_history_auth
H
)
∗
own
γ
_h
(
half_history_frag
H
)
∗
([
∗
list
]
l
∈
H
,
∃
q
,
l
↦
{
q
}
)
∗
⌜
Some
l
=
head
H
∧
NoDup
H
⌝
∗
own
γ
_b
(
●
Excl'
b
)
∗
((
∃
(
n
:
Z
),
⌜
v
=
InjLV
#
n
⌝
∗
own
γ
_h
(
half_history_frag
H
)
∗
own
γ
_n
(
●
Excl'
n
))
∨
(
∃
(
n
:
Z
)
(
p
:
proph_id
),
⌜
v
=
InjRV
(#
n
,#
p
)
⌝
∗
∃
P
Q
l_ghost
γ
_t
,
inv
stateN
(
state_inv
P
Q
p
n
l
l_ghost
H
γ
_h
γ
_n
γ
_t
)
∗
□
pau
P
Q
(
γ
_h
,
γ
_b
,
γ
_n
))))%
I
.
Definition
is_counter
(
γ
s
:
gname
*
gname
*
gname
)
(
ctr
:
val
)
:
=
(
∃
(
γ
_h
γ
_b
γ
_n
:
gname
)
(
f
c
:
loc
),
⌜γ
s
=
(
γ
_h
,
γ
_b
,
γ
_n
)
∧
ctr
=
(#
f
,
#
c
)%
V
⌝
∗
inv
counterN
(
counter_inv
γ
_h
γ
_b
γ
_n
f
c
))%
I
.
Global
Instance
is_counter_persistent
γ
s
ctr
:
Persistent
(
is_counter
γ
s
ctr
)
:
=
_
.
Global
Instance
counter_content_timeless
γ
s
ctr
:
Timeless
(
counter_content
γ
s
ctr
)
:
=
_
.
Global
Instance
abstract_state_inhabited
:
Inhabited
abstract_state
:
=
populate
(
injl
0
).
(** A few more helper lemmas that will come up later *)
Lemma
mapsto_valid_3
l
v1
v2
q
:
l
↦
v1

∗
l
↦
{
q
}
v2

∗
⌜
False
⌝
.
Proof
.
iIntros
"Hl1 Hl2"
.
iDestruct
(
mapsto_valid_2
with
"Hl1 Hl2"
)
as
%
Hv
.
apply
(
iffLR
(
frac_valid'
_
))
in
Hv
.
by
apply
Qp_not_plus_q_ge_1
in
Hv
.
Qed
.
Instance
in_dec
(
l
:
loc
)
H
:
Decision
(
In
l
H
).
Proof
.
induction
H
as
[
a
H
IH
].

right
.
naive_solver
.

destruct
(
decide
(
l
=
a
)).
+
left
.
naive_solver
.
+
destruct
IH
;
[
left

right
]
;
naive_solver
.
Qed
.
Lemma
nodup_fresh_loc
l
v
H
:
NoDup
H
→
l
↦
v

∗
([
∗
list
]
l
∈
H
,
∃
q
,
l
↦
{
q
}
)

∗
⌜
NoDup
(
l
::
H
)
⌝
.
Proof
.
intros
Hd
.
iIntros
"Hl Hls"
.
destruct
(
decide
(
In
l
H
))
as
[(
x1
&
x2
&
>)%
in_split

Hn
%
NoDup_cons
]
;
last
done
.

destruct
x1
as
[
x1
x1s
]
;
[
rewrite
app_nil_l
in
Hd
;
rewrite
app_nil_l
;
iDestruct
"Hls"
as
"[Hl' _]"

iDestruct
"Hls"
as
"[_ [Hl' _]]"
]
;
iDestruct
"Hl'"
as
(
q
v'
)
"Hl'"
;
by
iDestruct
(
mapsto_valid_3
with
"Hl Hl'"
)
as
%?.

by
iPureIntro
.
Qed
.
(** ** Proof of [complete] *)
(** The part of [complete] for the succeeding thread that moves from [pending] to [accepted] state *)