Library zoo_parabs.vertex
From zoo Require Import
prelude.
From zoo.common Require Import
countable
gmultiset.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.auth_gmultiset
lib.mono_gmultiset
lib.subprops
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
clist
option.
From zoo_saturn Require Import
mpmc_stack_2.
From zoo_parabs Require Export
base
vertex__code.
From zoo_parabs Require Import
vertex__types
pool.
From zoo Require Import
options.
Implicit Types b finished : bool.
Implicit Types preds : nat.
Implicit Types succ : location.
Implicit Types task ctx : val.
Implicit Types own : ownership.
Variant state :=
| Init
| Released
| Ready
| Finished.
Implicit Types state : state.
#[local] Instance state_inhabited : Inhabited state :=
populate Init.
#[local] Instance state_eq_dec : EqDecision state :=
ltac:(solve_decision).
Record vertex_name :=
{ vertex_name_successors : val
; vertex_name_state : gname
; vertex_name_iteration : gname
; vertex_name_predecessors : gname
; vertex_name_output : gname
}.
Implicit Types γ δ π : vertex_name.
#[local] Instance vertex_name_eq_dec : EqDecision vertex_name :=
ltac:(solve_decision).
#[local] Instance vertex_name_countable :
Countable vertex_name.
Implicit Types Δ Π : gmultiset vertex_name.
Definition vertex_iteration :=
gname.
Implicit Types iter : vertex_iteration.
Class VertexG Σ `{pool_G : PoolG Σ} :=
{ #[local] vertex_G_stack_G :: MpmcStack2G Σ
; #[local] vertex_G_state_G :: TwinsG Σ (leibnizO state)
; #[local] vertex_G_iteration_G :: TwinsG Σ (leibnizO vertex_iteration)
; #[local] vertex_G_dependencies_G :: MonoGmultisetG Σ vertex_name
; #[local] vertex_G_predecessors_G :: AuthGmultisetG Σ vertex_name
; #[local] vertex_G_output_G :: SubpropsG Σ
}.
Definition vertex_Σ :=
#[mpmc_stack_2_Σ
; twins_Σ (leibnizO state)
; twins_Σ (leibnizO vertex_iteration)
; mono_gmultiset_Σ vertex_name
; auth_gmultiset_Σ vertex_name
; subprops_Σ
].
#[global] Instance subG_vertex_Σ Σ `{pool_G : PoolG Σ}:
subG vertex_Σ Σ →
VertexG Σ.
Module base.
Section vertex_G.
Context `{vertex_G : VertexG Σ}.
Implicit Types t : location.
Implicit Types P Q R : iProp Σ.
#[local] Definition state₁' γ_state own state :=
twins_twin1 (twins_G := vertex_G_state_G) γ_state own state.
#[local] Definition state₁ γ :=
state₁' γ.(vertex_name_state).
#[local] Definition state₂' γ_state state :=
twins_twin2 (twins_G := vertex_G_state_G) γ_state state.
#[local] Definition state₂ γ :=
state₂' γ.(vertex_name_state).
#[local] Definition iteration₁' γ_iteration iter :=
twins_twin1 γ_iteration (DfracOwn 1) iter.
#[local] Definition iteration₁ γ :=
iteration₁' γ.(vertex_name_iteration).
#[local] Definition iteration₂' γ_iteration iter :=
twins_twin2 γ_iteration iter.
#[local] Definition iteration₂ γ :=
iteration₂' γ.(vertex_name_iteration).
#[local] Definition dependencies_auth iter own :=
mono_gmultiset_auth iter own.
#[local] Definition dependencies_elem iter :=
mono_gmultiset_elem iter.
#[local] Definition predecessors_auth' γ_predecessors Π :=
auth_gmultiset_auth γ_predecessors (DfracOwn 1) Π.
#[local] Definition predecessors_auth γ Π :=
predecessors_auth' γ.(vertex_name_predecessors) Π.
#[local] Definition predecessors_elem γ π :=
auth_gmultiset_frag γ.(vertex_name_predecessors) {[+π+]}.
#[local] Definition output_auth' γ_output :=
subprops_auth γ_output.
#[local] Definition output_auth γ :=
subprops_auth γ.(vertex_name_output).
#[local] Definition output_frag' γ_output :=
subprops_frag γ_output.
#[local] Definition output_frag γ :=
output_frag' γ.(vertex_name_output).
#[local] Definition model' t γ task state iter : iProp Σ :=
t.[task] ↦ task ∗
state₁ γ Own state ∗
iteration₁ γ iter.
#[local] Instance : CustomIpat "model'" :=
" ( Ht{which;}_task{_{}} & Hstate{which;}₁{_{}} & Hiteration{which;}₁{_{}} ) ".
Definition vertex_model t γ task iter : iProp Σ :=
model' t γ task Init iter.
#[local] Instance : CustomIpat "model" :=
" (:model') ".
Definition vertex_ready iter : iProp Σ :=
∃ Δ,
dependencies_auth iter Discard Δ ∗
[∗ mset] δ ∈ Δ, state₁ δ Discard Finished.
#[local] Instance : CustomIpat "ready" :=
" ( %Δ{} & #Hdependencies{which;}_auth{_{}} & #HΔ{} ) ".
Definition vertex_finished γ :=
state₁ γ Discard Finished.
#[local] Instance : CustomIpat "finished" :=
" #Hstate{which;}₁{_{}} ".
Definition vertex_wp_body t γ P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool_context pool ctx scope -∗
vertex_ready iter -∗
vertex_model t γ task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool_context pool ctx scope ∗
vertex_model t γ task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex_wp_pre
: location → vertex_name → iProp Σ → iProp Σ →
(val -d> vertex_iteration -d> iProp Σ) →
val -d> vertex_iteration -d> iProp Σ
:=
vertex_wp_body.
#[local] Instance vertex_wp_pre_contractive t γ P R :
Contractive (vertex_wp_pre t γ P R).
#[local] Instance vertex_wp_pre_ne t γ P R :
NonExpansive (vertex_wp_pre t γ P R).
Definition vertex_wp t γ P R : val → vertex_iteration → iProp Σ :=
fixpoint (vertex_wp_pre t γ P R).
Lemma vertex_wp_unfold t γ P R task iter :
vertex_wp t γ P R task iter ⊣⊢
vertex_wp_body t γ P R (vertex_wp t γ P R) task iter.
#[global] Instance vertex_wp_ne n :
Proper (
(=) ==>
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex_wp.
#[local] Definition inv_state_init preds iter Π : iProp Σ :=
∃ Δ,
dependencies_auth iter Own (Δ ⊎ Π) ∗
⌜preds = S (size Π)⌝ ∗
[∗ mset] δ ∈ Δ, vertex_finished δ.
#[local] Instance : CustomIpat "inv_state_init" :=
" ( %Δ & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ ) ".
#[local] Definition inv_state_released t γ P R preds iter Π : iProp Σ :=
∃ task Δ,
model' t γ task Released iter ∗
dependencies_auth iter Discard (Δ ⊎ Π) ∗
⌜preds = size Π⌝ ∗
([∗ mset] δ ∈ Δ, vertex_finished δ) ∗
vertex_wp t γ P R task iter.
#[local] Instance : CustomIpat "inv_state_released" :=
" ( %task & %Δ & (:model') & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ & Htask ) ".
#[local] Definition inv_state_ready Π : iProp Σ :=
⌜Π = ∅⌝.
#[local] Instance : CustomIpat "inv_state_ready" :=
" {>;}-> ".
#[local] Definition inv_state_finished γ R preds Π : iProp Σ :=
vertex_finished γ ∗
⌜preds = S (size Π)⌝ ∗
□ R.
#[local] Instance : CustomIpat "inv_state_finished" :=
" ( {>;}#Hstate{which;}₁ & {>;}-> & #HR{which;} ) ".
#[local] Definition inv_state t γ P R state preds iter Π : iProp Σ :=
match state with
| Init ⇒
inv_state_init preds iter Π
| Released ⇒
inv_state_released t γ P R preds iter Π
| Ready ⇒
inv_state_ready Π
| Finished ⇒
inv_state_finished γ R preds Π
end.
#[local] Definition inv_successor (inv : location → vertex_name → iProp Σ → iProp Σ → iProp Σ) γ succ : iProp Σ :=
∃ γ_succ P_succ R_succ,
inv succ γ_succ P_succ R_succ ∗
predecessors_elem γ_succ γ.
#[local] Instance : CustomIpat "inv_successor" :=
" ( %γ_succ & %P_succ & %R_succ & #Hinv_succ & Hpredecessors_elem ) ".
#[local] Definition inv_successors inv γ finished :=
if finished then (
mpmc_stack_2_model γ.(vertex_name_successors) None
) else (
∃ succs,
mpmc_stack_2_model γ.(vertex_name_successors) (Some $ #*@{location} succs) ∗
[∗ list] succ ∈ succs, inv_successor inv γ succ
)%I.
#[local] Instance : CustomIpat "inv_successors_finished" :=
" >Hsuccessors{which;}_model ".
#[local] Instance : CustomIpat "inv_successors" :=
" ( %succs & >Hsuccessors{which;}_model & Hsuccs ) ".
#[local] Definition inv_inner inv t γ P R : iProp Σ :=
∃ preds state iter Π,
t.[preds] ↦ #preds ∗
state₂ γ state ∗
iteration₂ γ iter ∗
predecessors_auth γ Π ∗
output_auth γ P (bool_decide (state = Finished)) ∗
inv_state t γ P R state preds iter Π ∗
inv_successors inv γ (bool_decide (state = Finished)).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %preds{} & %state{} & %iter{} & %Π & Ht{which;}_preds & >Hstate{which;}₂ & >Hiteration{which;}₂ & Hpredecessors{which;}_auth & Houtput{which;}_auth & Hinv_state{which;} & Hinv_successors{which;} ) ".
#[local] Definition inv_pre
: (location -d> vertex_name -d> iProp Σ -d> iProp Σ -d> iProp Σ) →
location -d> vertex_name -d> iProp Σ -d> iProp Σ -d> iProp Σ
:=
λ inv t γ P R, (
t.[succs] ↦□ γ.(vertex_name_successors) ∗
mpmc_stack_2_inv γ.(vertex_name_successors) (nroot.@"successors") ∗
invariants.inv (nroot.@"inv") (inv_inner inv t γ P R)
)%I.
#[local] Instance : CustomIpat "inv_pre" :=
" ( #Ht{}_succs & #Hsuccessors{}_inv & #Hinv{_{}} ) ".
#[local] Instance inv_pre_contractive_2 :
Contractive inv_pre.
Definition vertex_inv : location → vertex_name → iProp Σ → iProp Σ → iProp Σ :=
fixpoint inv_pre.
#[local] Lemma vertex_inv_unfold t γ P R :
vertex_inv t γ P R ⊣⊢
inv_pre vertex_inv t γ P R.
#[local] Instance vertex_inv_contractive t γ n :
Proper (
dist_later n ==>
dist_later n ==>
(≡{n}≡)
) (vertex_inv t γ).
#[global] Instance vertex_inv_ne t γ n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex_inv t γ).
#[global] Instance vertex_inv_proper t γ :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex_inv t γ).
Definition vertex_output γ Q :=
output_frag γ Q.
#[local] Instance : CustomIpat "output" :=
" Houtput{which;}_frag{_{}} ".
#[global] Instance vertex_output_contractive γ :
Contractive (vertex_output γ).
#[global] Instance vertex_output_proper γ :
Proper ((≡) ==> (≡)) (vertex_output γ).
Definition vertex_predecessor γ iter :=
dependencies_elem iter γ.
#[local] Instance : CustomIpat "predecessor" :=
" #Hdependencies{which;}_elem{_{}} ".
#[global] Instance vertex_model_timeless t γ task iter :
Timeless (vertex_model t γ task iter).
#[global] Instance vertex_ready_timeless iter :
Timeless (vertex_ready iter).
#[global] Instance vertex_finished_timeless γ :
Timeless (vertex_finished γ).
#[global] Instance vertex_predecessor_timeless γ iter :
Timeless (vertex_predecessor γ iter).
#[global] Instance vertex_inv_persistent t γ P R :
Persistent (vertex_inv t γ P R).
#[global] Instance vertex_ready_persistent iter :
Persistent (vertex_ready iter).
#[global] Instance vertex_finished_persistent γ :
Persistent (vertex_finished γ).
#[global] Instance vertex_predecessor_persistent γ iter :
Persistent (vertex_predecessor γ iter).
#[local] Lemma state_alloc :
⊢ |==>
∃ γ_state,
state₁' γ_state Own Init ∗
state₂' γ_state Init.
#[local] Lemma state_agree γ own1 state1 state2 :
state₁ γ own1 state1 -∗
state₂ γ state2 -∗
⌜state1 = state2⌝.
#[local] Lemma state₁_exclusive γ state1 own2 state2 :
state₁ γ Own state1 -∗
state₁ γ own2 state2 -∗
False.
#[local] Lemma state_update {γ state1 state2} state :
state₁ γ Own state1 -∗
state₂ γ state2 ==∗
state₁ γ Own state ∗
state₂ γ state.
#[local] Lemma state₁_discard γ state :
state₁ γ Own state ⊢ |==>
state₁ γ Discard state.
#[local] Lemma iteration_alloc iter :
⊢ |==>
∃ γ_iteration,
iteration₁' γ_iteration iter ∗
iteration₂' γ_iteration iter.
#[local] Lemma iteration_agree γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 -∗
⌜iteration1 = iteration2⌝.
#[local] Lemma iteration₁_exclusive γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₁ γ iteration2 -∗
False.
#[local] Lemma iteration_update {γ iteration1 iteration2} iteration :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 ==∗
iteration₁ γ iteration ∗
iteration₂ γ iteration.
#[local] Lemma dependencies_alloc :
⊢ |==>
∃ iter,
dependencies_auth iter Own ∅.
#[local] Lemma dependencies_add {iter Δ} δ :
dependencies_auth iter Own Δ ⊢ |==>
dependencies_auth iter Own ({[+δ+]} ⊎ Δ) ∗
dependencies_elem iter δ.
#[local] Lemma dependencies_elem_of iter own Δ δ :
dependencies_auth iter own Δ -∗
dependencies_elem iter δ -∗
⌜δ ∈ Δ⌝.
#[local] Lemma dependencies_discard iter Δ :
dependencies_auth iter Own Δ ⊢ |==>
dependencies_auth iter Discard Δ.
#[local] Lemma predecessors_alloc :
⊢ |==>
∃ γ_predecessors,
predecessors_auth' γ_predecessors ∅.
#[local] Lemma predecessors_elem_of γ Π π :
predecessors_auth γ Π -∗
predecessors_elem γ π -∗
⌜π ∈ Π⌝.
#[local] Lemma predecessors_add {γ Π} π :
predecessors_auth γ Π ⊢ |==>
predecessors_auth γ ({[+π+]} ⊎ Π) ∗
predecessors_elem γ π.
#[local] Lemma predecessors_remove γ Π π :
predecessors_auth γ Π -∗
predecessors_elem γ π ==∗
predecessors_auth γ (Π ∖ {[+π+]}).
#[local] Lemma output_alloc P :
⊢ |==>
∃ γ_output,
output_auth' γ_output P false ∗
output_frag' γ_output P.
#[local] Lemma output_wand {γ P finished Q1} Q2 E :
▷ output_auth γ P finished -∗
output_frag γ Q1 -∗
(Q1 -∗ Q2) ={E}=∗
▷ output_auth γ P finished ∗
output_frag γ Q2.
#[local] Lemma output_divide {γ P finished} Qs E :
▷ output_auth γ P finished -∗
output_frag γ ([∗ list] Q ∈ Qs, Q) ={E}=∗
▷ output_auth γ P finished ∗
[∗ list] Q ∈ Qs, output_frag γ Q.
#[local] Lemma output_produce γ P :
▷ output_auth γ P false -∗
P -∗
▷ output_auth γ P true.
#[local] Lemma output_consume γ P Q E :
▷ output_auth γ P true -∗
output_frag γ Q ={E}=∗
▷ output_auth γ P true ∗
▷^2 Q.
Lemma vertex_model_exclusive t γ task1 iter1 task2 iter2 :
vertex_model t γ task1 iter1 -∗
vertex_model t γ task2 iter2 -∗
False.
Lemma vertex_model_finished t γ task iter :
vertex_model t γ task iter -∗
vertex_finished γ -∗
False.
Lemma vertex_output_wand {t γ P R Q1} Q2 :
vertex_inv t γ P R -∗
vertex_output γ Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex_output γ Q2.
Lemma vertex_output_divide {t γ P R} Qs :
vertex_inv t γ P R -∗
vertex_output γ ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex_output γ Q.
Lemma vertex_predecessor_finished γ iter :
vertex_predecessor γ iter -∗
vertex_ready iter -∗
vertex_finished γ.
Lemma vertex_inv_finished t γ P R :
vertex_inv t γ P R -∗
vertex_finished γ ={⊤}=∗
▷ □ R.
Lemma vertex_inv_finished_output t γ P R Q :
vertex_inv t γ P R -∗
vertex_finished γ -∗
vertex_output γ Q ={⊤}=∗
▷^2 Q.
Lemma vertex٠create𑁒spec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex_inv t γ P R ∗
vertex_model t γ (default (fun: ≠ ⇒ true)%V task) iter ∗
vertex_output γ P
}}}.
Lemma vertex٠create'𑁒spec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex_inv t γ P R ∗
vertex_model t γ (fun: "ctx" ⇒ task "ctx" ;; true) iter ∗
vertex_output γ P
}}}.
Lemma vertex٠task𑁒spec t γ task iter :
{{{
vertex_model t γ task iter
}}}
vertex٠task #t
{{{
RET task;
vertex_model t γ task iter
}}}.
Lemma vertex٠set_task𑁒spec t γ task1 iter task2 :
{{{
vertex_model t γ task1 iter
}}}
vertex٠set_task #t task2
{{{
RET ();
vertex_model t γ task2 iter
}}}.
Lemma vertex٠precede𑁒spec t1 γ1 P1 R1 t2 γ2 P2 R2 task iter :
{{{
vertex_inv t1 γ1 P1 R1 ∗
vertex_inv t2 γ2 P2 R2 ∗
vertex_model t2 γ2 task iter
}}}
vertex٠precede #t1 #t2
{{{
RET ();
vertex_model t2 γ2 task iter ∗
vertex_predecessor γ1 iter
}}}.
#[local] Lemma vertex٠release_run𑁒spec :
⊢ (
∀ pool ctx scope t γ P R task iter,
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
vertex_model t γ task iter ∗
vertex_wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ P R π,
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
predecessors_elem γ π ∗
vertex_finished π
}}}
vertex٠release ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ iter P R task,
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
vertex_ready iter ∗
model' t γ task Ready iter ∗
vertex_wp t γ P R task iter
}}}
vertex٠run ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}
).
Lemma vertex٠release𑁒spec pool ctx scope t γ P R task iter :
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
vertex_model t γ task iter ∗
vertex_wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}.
Lemma vertex٠yield𑁒spec t γ task' iter task :
{{{
vertex_model t γ task' iter
}}}
vertex٠yield #t task
{{{
RET false;
vertex_model t γ task iter
}}}.
End vertex_G.
#[global] Opaque vertex_inv.
#[global] Opaque vertex_model.
#[global] Opaque vertex_output.
#[global] Opaque vertex_ready.
#[global] Opaque vertex_finished.
#[global] Opaque vertex_predecessor.
End base.
From zoo_parabs Require
vertex__opaque.
Section vertex_G.
Context `{vertex_G : VertexG Σ}.
Implicit Types 𝑡 : location.
Definition vertex_inv t P R : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_inv 𝑡 γ P R.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & #Hinv{_{}} ) ".
#[global] Instance vertex_inv_ne t n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex_inv t).
#[global] Instance vertex_inv_proper t :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex_inv t).
Definition vertex_model t task iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_model 𝑡 γ task iter.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hmodel{_{}} ) ".
Definition vertex_output t Q : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_output γ Q.
#[local] Instance : CustomIpat "output" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Houtput{_{}} ) ".
Definition vertex_ready :=
base.vertex_ready.
Definition vertex_finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hfinished{_{}} ) ".
Definition vertex_predecessor t iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_predecessor γ iter.
#[local] Instance : CustomIpat "predecessor" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hpredecessor{_{}} ) ".
Definition vertex_wp_body t P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool_context pool ctx scope -∗
vertex_ready iter -∗
vertex_model t task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool_context pool ctx scope ∗
vertex_model t task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex_wp_pre
: val → iProp Σ → iProp Σ →
(val -d> vertex_iteration -d> iProp Σ) →
val -d> vertex_iteration -d> iProp Σ
:=
vertex_wp_body.
#[local] Instance vertex_wp_pre_contractive t P R :
Contractive (vertex_wp_pre t P R).
#[local] Instance vertex_wp_pre_ne t P R :
NonExpansive (vertex_wp_pre t P R).
Definition vertex_wp t P R : val → vertex_iteration → iProp Σ :=
fixpoint (vertex_wp_pre t P R).
Lemma vertex_wp_unfold t P R task iter :
vertex_wp t P R task iter ⊣⊢
vertex_wp_body t P R (vertex_wp t P R) task iter.
#[global] Instance vertex_wp_ne n :
Proper (
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex_wp.
#[local] Lemma vertex_wp_to_base 𝑡 γ P R task iter :
meta 𝑡 nroot γ -∗
vertex_wp #𝑡 P R task iter -∗
base.vertex_wp 𝑡 γ P R task iter.
#[global] Instance vertex_output_contractive t :
Contractive (vertex_output t).
#[global] Instance vertex_output_proper t :
Proper ((≡) ==> (≡)) (vertex_output t).
#[global] Instance vertex_model_timeless t task iter :
Timeless (vertex_model t task iter).
#[global] Instance vertex_ready_timeless iter :
Timeless (vertex_ready iter).
#[global] Instance vertex_finished_timeless t :
Timeless (vertex_finished t).
#[global] Instance vertex_predecessor_timeless t iter :
Timeless (vertex_predecessor t iter).
#[global] Instance vertex_inv_persistent t P R :
Persistent (vertex_inv t P R).
#[global] Instance vertex_ready_persistent iter :
Persistent (vertex_ready iter).
#[global] Instance vertex_finished_persistent t :
Persistent (vertex_finished t).
#[global] Instance vertex_predecessor_persistent t iter :
Persistent (vertex_predecessor t iter).
Lemma vertex_model_exclusive t task1 iter1 task2 iter2 :
vertex_model t task1 iter1 -∗
vertex_model t task2 iter2 -∗
False.
Lemma vertex_model_finished t task iter :
vertex_model t task iter -∗
vertex_finished t -∗
False.
Lemma vertex_output_wand {t P R Q1} Q2 :
vertex_inv t P R -∗
vertex_output t Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex_output t Q2.
Lemma vertex_output_divide {t P R} Qs :
vertex_inv t P R -∗
vertex_output t ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex_output t Q.
Lemma vertex_output_split {t P R} Q1 Q2 :
vertex_inv t P R -∗
vertex_output t (Q1 ∗ Q2) ={⊤}=∗
vertex_output t Q1 ∗
vertex_output t Q2.
Lemma vertex_predecessor_finished t iter :
vertex_predecessor t iter -∗
vertex_ready iter -∗
vertex_finished t.
Lemma vertex_inv_finished t P R :
vertex_inv t P R -∗
vertex_finished t ={⊤}=∗
▷ □ R.
Lemma vertex_inv_finished' t P R :
£ 1 -∗
vertex_inv t P R -∗
vertex_finished t ={⊤}=∗
□ R.
Lemma vertex_inv_finished_output t P R Q :
vertex_inv t P R -∗
vertex_finished t -∗
vertex_output t Q ={⊤}=∗
▷^2 Q.
Lemma vertex_inv_finished_output' t P R Q :
£ 2 -∗
vertex_inv t P R -∗
vertex_finished t -∗
vertex_output t Q ={⊤}=∗
Q.
Lemma vertex٠create𑁒spec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t iter
, RET t;
vertex_inv t P R ∗
vertex_model t (default (fun: ≠ ⇒ true)%V task) iter ∗
vertex_output t P
}}}.
Lemma vertex٠create'𑁒spec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t iter
, RET t;
vertex_inv t P R ∗
vertex_model t (fun: "ctx" ⇒ task "ctx" ;; true) iter ∗
vertex_output t P
}}}.
Lemma vertex٠task𑁒spec t task iter :
{{{
vertex_model t task iter
}}}
vertex٠task t
{{{
RET task;
vertex_model t task iter
}}}.
Lemma vertex٠set_task𑁒spec t task1 iter task2 :
{{{
vertex_model t task1 iter
}}}
vertex٠set_task t task2
{{{
RET ();
vertex_model t task2 iter
}}}.
Lemma vertex٠precede𑁒spec t1 P1 R1 t2 P2 R2 task iter :
{{{
vertex_inv t1 P1 R1 ∗
vertex_inv t2 P2 R2 ∗
vertex_model t2 task iter
}}}
vertex٠precede t1 t2
{{{
RET ();
vertex_model t2 task iter ∗
vertex_predecessor t1 iter
}}}.
Lemma vertex٠release𑁒spec pool ctx scope t P R task iter :
{{{
pool_context pool ctx scope ∗
vertex_inv t P R ∗
vertex_model t task iter ∗
vertex_wp t P R task iter
}}}
vertex٠release ctx t
{{{
RET ();
pool_context pool ctx scope
}}}.
Lemma vertex٠release𑁒spec' pool ctx scope t P R task iter :
{{{
pool_context pool ctx scope ∗
vertex_inv t P R ∗
vertex_model t task iter ∗
( ∀ pool ctx scope,
pool_context pool ctx scope -∗
vertex_ready iter -∗
WP task ctx {{ res,
⌜res = true%V⌝ ∗
pool_context pool ctx scope ∗
▷ P ∗
▷ □ R
}}
)
}}}
vertex٠release ctx t
{{{
RET ();
pool_context pool ctx scope
}}}.
Lemma vertex٠yield𑁒spec t task' iter task :
{{{
vertex_model t task' iter
}}}
vertex٠yield t task
{{{
RET false;
vertex_model t task iter
}}}.
End vertex_G.
#[global] Opaque vertex_inv.
#[global] Opaque vertex_model.
#[global] Opaque vertex_output.
#[global] Opaque vertex_ready.
#[global] Opaque vertex_finished.
#[global] Opaque vertex_predecessor.
prelude.
From zoo.common Require Import
countable
gmultiset.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.auth_gmultiset
lib.mono_gmultiset
lib.subprops
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
clist
option.
From zoo_saturn Require Import
mpmc_stack_2.
From zoo_parabs Require Export
base
vertex__code.
From zoo_parabs Require Import
vertex__types
pool.
From zoo Require Import
options.
Implicit Types b finished : bool.
Implicit Types preds : nat.
Implicit Types succ : location.
Implicit Types task ctx : val.
Implicit Types own : ownership.
Variant state :=
| Init
| Released
| Ready
| Finished.
Implicit Types state : state.
#[local] Instance state_inhabited : Inhabited state :=
populate Init.
#[local] Instance state_eq_dec : EqDecision state :=
ltac:(solve_decision).
Record vertex_name :=
{ vertex_name_successors : val
; vertex_name_state : gname
; vertex_name_iteration : gname
; vertex_name_predecessors : gname
; vertex_name_output : gname
}.
Implicit Types γ δ π : vertex_name.
#[local] Instance vertex_name_eq_dec : EqDecision vertex_name :=
ltac:(solve_decision).
#[local] Instance vertex_name_countable :
Countable vertex_name.
Implicit Types Δ Π : gmultiset vertex_name.
Definition vertex_iteration :=
gname.
Implicit Types iter : vertex_iteration.
Class VertexG Σ `{pool_G : PoolG Σ} :=
{ #[local] vertex_G_stack_G :: MpmcStack2G Σ
; #[local] vertex_G_state_G :: TwinsG Σ (leibnizO state)
; #[local] vertex_G_iteration_G :: TwinsG Σ (leibnizO vertex_iteration)
; #[local] vertex_G_dependencies_G :: MonoGmultisetG Σ vertex_name
; #[local] vertex_G_predecessors_G :: AuthGmultisetG Σ vertex_name
; #[local] vertex_G_output_G :: SubpropsG Σ
}.
Definition vertex_Σ :=
#[mpmc_stack_2_Σ
; twins_Σ (leibnizO state)
; twins_Σ (leibnizO vertex_iteration)
; mono_gmultiset_Σ vertex_name
; auth_gmultiset_Σ vertex_name
; subprops_Σ
].
#[global] Instance subG_vertex_Σ Σ `{pool_G : PoolG Σ}:
subG vertex_Σ Σ →
VertexG Σ.
Module base.
Section vertex_G.
Context `{vertex_G : VertexG Σ}.
Implicit Types t : location.
Implicit Types P Q R : iProp Σ.
#[local] Definition state₁' γ_state own state :=
twins_twin1 (twins_G := vertex_G_state_G) γ_state own state.
#[local] Definition state₁ γ :=
state₁' γ.(vertex_name_state).
#[local] Definition state₂' γ_state state :=
twins_twin2 (twins_G := vertex_G_state_G) γ_state state.
#[local] Definition state₂ γ :=
state₂' γ.(vertex_name_state).
#[local] Definition iteration₁' γ_iteration iter :=
twins_twin1 γ_iteration (DfracOwn 1) iter.
#[local] Definition iteration₁ γ :=
iteration₁' γ.(vertex_name_iteration).
#[local] Definition iteration₂' γ_iteration iter :=
twins_twin2 γ_iteration iter.
#[local] Definition iteration₂ γ :=
iteration₂' γ.(vertex_name_iteration).
#[local] Definition dependencies_auth iter own :=
mono_gmultiset_auth iter own.
#[local] Definition dependencies_elem iter :=
mono_gmultiset_elem iter.
#[local] Definition predecessors_auth' γ_predecessors Π :=
auth_gmultiset_auth γ_predecessors (DfracOwn 1) Π.
#[local] Definition predecessors_auth γ Π :=
predecessors_auth' γ.(vertex_name_predecessors) Π.
#[local] Definition predecessors_elem γ π :=
auth_gmultiset_frag γ.(vertex_name_predecessors) {[+π+]}.
#[local] Definition output_auth' γ_output :=
subprops_auth γ_output.
#[local] Definition output_auth γ :=
subprops_auth γ.(vertex_name_output).
#[local] Definition output_frag' γ_output :=
subprops_frag γ_output.
#[local] Definition output_frag γ :=
output_frag' γ.(vertex_name_output).
#[local] Definition model' t γ task state iter : iProp Σ :=
t.[task] ↦ task ∗
state₁ γ Own state ∗
iteration₁ γ iter.
#[local] Instance : CustomIpat "model'" :=
" ( Ht{which;}_task{_{}} & Hstate{which;}₁{_{}} & Hiteration{which;}₁{_{}} ) ".
Definition vertex_model t γ task iter : iProp Σ :=
model' t γ task Init iter.
#[local] Instance : CustomIpat "model" :=
" (:model') ".
Definition vertex_ready iter : iProp Σ :=
∃ Δ,
dependencies_auth iter Discard Δ ∗
[∗ mset] δ ∈ Δ, state₁ δ Discard Finished.
#[local] Instance : CustomIpat "ready" :=
" ( %Δ{} & #Hdependencies{which;}_auth{_{}} & #HΔ{} ) ".
Definition vertex_finished γ :=
state₁ γ Discard Finished.
#[local] Instance : CustomIpat "finished" :=
" #Hstate{which;}₁{_{}} ".
Definition vertex_wp_body t γ P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool_context pool ctx scope -∗
vertex_ready iter -∗
vertex_model t γ task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool_context pool ctx scope ∗
vertex_model t γ task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex_wp_pre
: location → vertex_name → iProp Σ → iProp Σ →
(val -d> vertex_iteration -d> iProp Σ) →
val -d> vertex_iteration -d> iProp Σ
:=
vertex_wp_body.
#[local] Instance vertex_wp_pre_contractive t γ P R :
Contractive (vertex_wp_pre t γ P R).
#[local] Instance vertex_wp_pre_ne t γ P R :
NonExpansive (vertex_wp_pre t γ P R).
Definition vertex_wp t γ P R : val → vertex_iteration → iProp Σ :=
fixpoint (vertex_wp_pre t γ P R).
Lemma vertex_wp_unfold t γ P R task iter :
vertex_wp t γ P R task iter ⊣⊢
vertex_wp_body t γ P R (vertex_wp t γ P R) task iter.
#[global] Instance vertex_wp_ne n :
Proper (
(=) ==>
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex_wp.
#[local] Definition inv_state_init preds iter Π : iProp Σ :=
∃ Δ,
dependencies_auth iter Own (Δ ⊎ Π) ∗
⌜preds = S (size Π)⌝ ∗
[∗ mset] δ ∈ Δ, vertex_finished δ.
#[local] Instance : CustomIpat "inv_state_init" :=
" ( %Δ & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ ) ".
#[local] Definition inv_state_released t γ P R preds iter Π : iProp Σ :=
∃ task Δ,
model' t γ task Released iter ∗
dependencies_auth iter Discard (Δ ⊎ Π) ∗
⌜preds = size Π⌝ ∗
([∗ mset] δ ∈ Δ, vertex_finished δ) ∗
vertex_wp t γ P R task iter.
#[local] Instance : CustomIpat "inv_state_released" :=
" ( %task & %Δ & (:model') & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ & Htask ) ".
#[local] Definition inv_state_ready Π : iProp Σ :=
⌜Π = ∅⌝.
#[local] Instance : CustomIpat "inv_state_ready" :=
" {>;}-> ".
#[local] Definition inv_state_finished γ R preds Π : iProp Σ :=
vertex_finished γ ∗
⌜preds = S (size Π)⌝ ∗
□ R.
#[local] Instance : CustomIpat "inv_state_finished" :=
" ( {>;}#Hstate{which;}₁ & {>;}-> & #HR{which;} ) ".
#[local] Definition inv_state t γ P R state preds iter Π : iProp Σ :=
match state with
| Init ⇒
inv_state_init preds iter Π
| Released ⇒
inv_state_released t γ P R preds iter Π
| Ready ⇒
inv_state_ready Π
| Finished ⇒
inv_state_finished γ R preds Π
end.
#[local] Definition inv_successor (inv : location → vertex_name → iProp Σ → iProp Σ → iProp Σ) γ succ : iProp Σ :=
∃ γ_succ P_succ R_succ,
inv succ γ_succ P_succ R_succ ∗
predecessors_elem γ_succ γ.
#[local] Instance : CustomIpat "inv_successor" :=
" ( %γ_succ & %P_succ & %R_succ & #Hinv_succ & Hpredecessors_elem ) ".
#[local] Definition inv_successors inv γ finished :=
if finished then (
mpmc_stack_2_model γ.(vertex_name_successors) None
) else (
∃ succs,
mpmc_stack_2_model γ.(vertex_name_successors) (Some $ #*@{location} succs) ∗
[∗ list] succ ∈ succs, inv_successor inv γ succ
)%I.
#[local] Instance : CustomIpat "inv_successors_finished" :=
" >Hsuccessors{which;}_model ".
#[local] Instance : CustomIpat "inv_successors" :=
" ( %succs & >Hsuccessors{which;}_model & Hsuccs ) ".
#[local] Definition inv_inner inv t γ P R : iProp Σ :=
∃ preds state iter Π,
t.[preds] ↦ #preds ∗
state₂ γ state ∗
iteration₂ γ iter ∗
predecessors_auth γ Π ∗
output_auth γ P (bool_decide (state = Finished)) ∗
inv_state t γ P R state preds iter Π ∗
inv_successors inv γ (bool_decide (state = Finished)).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %preds{} & %state{} & %iter{} & %Π & Ht{which;}_preds & >Hstate{which;}₂ & >Hiteration{which;}₂ & Hpredecessors{which;}_auth & Houtput{which;}_auth & Hinv_state{which;} & Hinv_successors{which;} ) ".
#[local] Definition inv_pre
: (location -d> vertex_name -d> iProp Σ -d> iProp Σ -d> iProp Σ) →
location -d> vertex_name -d> iProp Σ -d> iProp Σ -d> iProp Σ
:=
λ inv t γ P R, (
t.[succs] ↦□ γ.(vertex_name_successors) ∗
mpmc_stack_2_inv γ.(vertex_name_successors) (nroot.@"successors") ∗
invariants.inv (nroot.@"inv") (inv_inner inv t γ P R)
)%I.
#[local] Instance : CustomIpat "inv_pre" :=
" ( #Ht{}_succs & #Hsuccessors{}_inv & #Hinv{_{}} ) ".
#[local] Instance inv_pre_contractive_2 :
Contractive inv_pre.
Definition vertex_inv : location → vertex_name → iProp Σ → iProp Σ → iProp Σ :=
fixpoint inv_pre.
#[local] Lemma vertex_inv_unfold t γ P R :
vertex_inv t γ P R ⊣⊢
inv_pre vertex_inv t γ P R.
#[local] Instance vertex_inv_contractive t γ n :
Proper (
dist_later n ==>
dist_later n ==>
(≡{n}≡)
) (vertex_inv t γ).
#[global] Instance vertex_inv_ne t γ n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex_inv t γ).
#[global] Instance vertex_inv_proper t γ :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex_inv t γ).
Definition vertex_output γ Q :=
output_frag γ Q.
#[local] Instance : CustomIpat "output" :=
" Houtput{which;}_frag{_{}} ".
#[global] Instance vertex_output_contractive γ :
Contractive (vertex_output γ).
#[global] Instance vertex_output_proper γ :
Proper ((≡) ==> (≡)) (vertex_output γ).
Definition vertex_predecessor γ iter :=
dependencies_elem iter γ.
#[local] Instance : CustomIpat "predecessor" :=
" #Hdependencies{which;}_elem{_{}} ".
#[global] Instance vertex_model_timeless t γ task iter :
Timeless (vertex_model t γ task iter).
#[global] Instance vertex_ready_timeless iter :
Timeless (vertex_ready iter).
#[global] Instance vertex_finished_timeless γ :
Timeless (vertex_finished γ).
#[global] Instance vertex_predecessor_timeless γ iter :
Timeless (vertex_predecessor γ iter).
#[global] Instance vertex_inv_persistent t γ P R :
Persistent (vertex_inv t γ P R).
#[global] Instance vertex_ready_persistent iter :
Persistent (vertex_ready iter).
#[global] Instance vertex_finished_persistent γ :
Persistent (vertex_finished γ).
#[global] Instance vertex_predecessor_persistent γ iter :
Persistent (vertex_predecessor γ iter).
#[local] Lemma state_alloc :
⊢ |==>
∃ γ_state,
state₁' γ_state Own Init ∗
state₂' γ_state Init.
#[local] Lemma state_agree γ own1 state1 state2 :
state₁ γ own1 state1 -∗
state₂ γ state2 -∗
⌜state1 = state2⌝.
#[local] Lemma state₁_exclusive γ state1 own2 state2 :
state₁ γ Own state1 -∗
state₁ γ own2 state2 -∗
False.
#[local] Lemma state_update {γ state1 state2} state :
state₁ γ Own state1 -∗
state₂ γ state2 ==∗
state₁ γ Own state ∗
state₂ γ state.
#[local] Lemma state₁_discard γ state :
state₁ γ Own state ⊢ |==>
state₁ γ Discard state.
#[local] Lemma iteration_alloc iter :
⊢ |==>
∃ γ_iteration,
iteration₁' γ_iteration iter ∗
iteration₂' γ_iteration iter.
#[local] Lemma iteration_agree γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 -∗
⌜iteration1 = iteration2⌝.
#[local] Lemma iteration₁_exclusive γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₁ γ iteration2 -∗
False.
#[local] Lemma iteration_update {γ iteration1 iteration2} iteration :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 ==∗
iteration₁ γ iteration ∗
iteration₂ γ iteration.
#[local] Lemma dependencies_alloc :
⊢ |==>
∃ iter,
dependencies_auth iter Own ∅.
#[local] Lemma dependencies_add {iter Δ} δ :
dependencies_auth iter Own Δ ⊢ |==>
dependencies_auth iter Own ({[+δ+]} ⊎ Δ) ∗
dependencies_elem iter δ.
#[local] Lemma dependencies_elem_of iter own Δ δ :
dependencies_auth iter own Δ -∗
dependencies_elem iter δ -∗
⌜δ ∈ Δ⌝.
#[local] Lemma dependencies_discard iter Δ :
dependencies_auth iter Own Δ ⊢ |==>
dependencies_auth iter Discard Δ.
#[local] Lemma predecessors_alloc :
⊢ |==>
∃ γ_predecessors,
predecessors_auth' γ_predecessors ∅.
#[local] Lemma predecessors_elem_of γ Π π :
predecessors_auth γ Π -∗
predecessors_elem γ π -∗
⌜π ∈ Π⌝.
#[local] Lemma predecessors_add {γ Π} π :
predecessors_auth γ Π ⊢ |==>
predecessors_auth γ ({[+π+]} ⊎ Π) ∗
predecessors_elem γ π.
#[local] Lemma predecessors_remove γ Π π :
predecessors_auth γ Π -∗
predecessors_elem γ π ==∗
predecessors_auth γ (Π ∖ {[+π+]}).
#[local] Lemma output_alloc P :
⊢ |==>
∃ γ_output,
output_auth' γ_output P false ∗
output_frag' γ_output P.
#[local] Lemma output_wand {γ P finished Q1} Q2 E :
▷ output_auth γ P finished -∗
output_frag γ Q1 -∗
(Q1 -∗ Q2) ={E}=∗
▷ output_auth γ P finished ∗
output_frag γ Q2.
#[local] Lemma output_divide {γ P finished} Qs E :
▷ output_auth γ P finished -∗
output_frag γ ([∗ list] Q ∈ Qs, Q) ={E}=∗
▷ output_auth γ P finished ∗
[∗ list] Q ∈ Qs, output_frag γ Q.
#[local] Lemma output_produce γ P :
▷ output_auth γ P false -∗
P -∗
▷ output_auth γ P true.
#[local] Lemma output_consume γ P Q E :
▷ output_auth γ P true -∗
output_frag γ Q ={E}=∗
▷ output_auth γ P true ∗
▷^2 Q.
Lemma vertex_model_exclusive t γ task1 iter1 task2 iter2 :
vertex_model t γ task1 iter1 -∗
vertex_model t γ task2 iter2 -∗
False.
Lemma vertex_model_finished t γ task iter :
vertex_model t γ task iter -∗
vertex_finished γ -∗
False.
Lemma vertex_output_wand {t γ P R Q1} Q2 :
vertex_inv t γ P R -∗
vertex_output γ Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex_output γ Q2.
Lemma vertex_output_divide {t γ P R} Qs :
vertex_inv t γ P R -∗
vertex_output γ ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex_output γ Q.
Lemma vertex_predecessor_finished γ iter :
vertex_predecessor γ iter -∗
vertex_ready iter -∗
vertex_finished γ.
Lemma vertex_inv_finished t γ P R :
vertex_inv t γ P R -∗
vertex_finished γ ={⊤}=∗
▷ □ R.
Lemma vertex_inv_finished_output t γ P R Q :
vertex_inv t γ P R -∗
vertex_finished γ -∗
vertex_output γ Q ={⊤}=∗
▷^2 Q.
Lemma vertex٠create𑁒spec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex_inv t γ P R ∗
vertex_model t γ (default (fun: ≠ ⇒ true)%V task) iter ∗
vertex_output γ P
}}}.
Lemma vertex٠create'𑁒spec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex_inv t γ P R ∗
vertex_model t γ (fun: "ctx" ⇒ task "ctx" ;; true) iter ∗
vertex_output γ P
}}}.
Lemma vertex٠task𑁒spec t γ task iter :
{{{
vertex_model t γ task iter
}}}
vertex٠task #t
{{{
RET task;
vertex_model t γ task iter
}}}.
Lemma vertex٠set_task𑁒spec t γ task1 iter task2 :
{{{
vertex_model t γ task1 iter
}}}
vertex٠set_task #t task2
{{{
RET ();
vertex_model t γ task2 iter
}}}.
Lemma vertex٠precede𑁒spec t1 γ1 P1 R1 t2 γ2 P2 R2 task iter :
{{{
vertex_inv t1 γ1 P1 R1 ∗
vertex_inv t2 γ2 P2 R2 ∗
vertex_model t2 γ2 task iter
}}}
vertex٠precede #t1 #t2
{{{
RET ();
vertex_model t2 γ2 task iter ∗
vertex_predecessor γ1 iter
}}}.
#[local] Lemma vertex٠release_run𑁒spec :
⊢ (
∀ pool ctx scope t γ P R task iter,
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
vertex_model t γ task iter ∗
vertex_wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ P R π,
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
predecessors_elem γ π ∗
vertex_finished π
}}}
vertex٠release ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ iter P R task,
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
vertex_ready iter ∗
model' t γ task Ready iter ∗
vertex_wp t γ P R task iter
}}}
vertex٠run ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}
).
Lemma vertex٠release𑁒spec pool ctx scope t γ P R task iter :
{{{
pool_context pool ctx scope ∗
vertex_inv t γ P R ∗
vertex_model t γ task iter ∗
vertex_wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool_context pool ctx scope
}}}.
Lemma vertex٠yield𑁒spec t γ task' iter task :
{{{
vertex_model t γ task' iter
}}}
vertex٠yield #t task
{{{
RET false;
vertex_model t γ task iter
}}}.
End vertex_G.
#[global] Opaque vertex_inv.
#[global] Opaque vertex_model.
#[global] Opaque vertex_output.
#[global] Opaque vertex_ready.
#[global] Opaque vertex_finished.
#[global] Opaque vertex_predecessor.
End base.
From zoo_parabs Require
vertex__opaque.
Section vertex_G.
Context `{vertex_G : VertexG Σ}.
Implicit Types 𝑡 : location.
Definition vertex_inv t P R : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_inv 𝑡 γ P R.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & #Hinv{_{}} ) ".
#[global] Instance vertex_inv_ne t n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex_inv t).
#[global] Instance vertex_inv_proper t :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex_inv t).
Definition vertex_model t task iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_model 𝑡 γ task iter.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hmodel{_{}} ) ".
Definition vertex_output t Q : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_output γ Q.
#[local] Instance : CustomIpat "output" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Houtput{_{}} ) ".
Definition vertex_ready :=
base.vertex_ready.
Definition vertex_finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hfinished{_{}} ) ".
Definition vertex_predecessor t iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.vertex_predecessor γ iter.
#[local] Instance : CustomIpat "predecessor" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hpredecessor{_{}} ) ".
Definition vertex_wp_body t P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool_context pool ctx scope -∗
vertex_ready iter -∗
vertex_model t task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool_context pool ctx scope ∗
vertex_model t task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex_wp_pre
: val → iProp Σ → iProp Σ →
(val -d> vertex_iteration -d> iProp Σ) →
val -d> vertex_iteration -d> iProp Σ
:=
vertex_wp_body.
#[local] Instance vertex_wp_pre_contractive t P R :
Contractive (vertex_wp_pre t P R).
#[local] Instance vertex_wp_pre_ne t P R :
NonExpansive (vertex_wp_pre t P R).
Definition vertex_wp t P R : val → vertex_iteration → iProp Σ :=
fixpoint (vertex_wp_pre t P R).
Lemma vertex_wp_unfold t P R task iter :
vertex_wp t P R task iter ⊣⊢
vertex_wp_body t P R (vertex_wp t P R) task iter.
#[global] Instance vertex_wp_ne n :
Proper (
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex_wp.
#[local] Lemma vertex_wp_to_base 𝑡 γ P R task iter :
meta 𝑡 nroot γ -∗
vertex_wp #𝑡 P R task iter -∗
base.vertex_wp 𝑡 γ P R task iter.
#[global] Instance vertex_output_contractive t :
Contractive (vertex_output t).
#[global] Instance vertex_output_proper t :
Proper ((≡) ==> (≡)) (vertex_output t).
#[global] Instance vertex_model_timeless t task iter :
Timeless (vertex_model t task iter).
#[global] Instance vertex_ready_timeless iter :
Timeless (vertex_ready iter).
#[global] Instance vertex_finished_timeless t :
Timeless (vertex_finished t).
#[global] Instance vertex_predecessor_timeless t iter :
Timeless (vertex_predecessor t iter).
#[global] Instance vertex_inv_persistent t P R :
Persistent (vertex_inv t P R).
#[global] Instance vertex_ready_persistent iter :
Persistent (vertex_ready iter).
#[global] Instance vertex_finished_persistent t :
Persistent (vertex_finished t).
#[global] Instance vertex_predecessor_persistent t iter :
Persistent (vertex_predecessor t iter).
Lemma vertex_model_exclusive t task1 iter1 task2 iter2 :
vertex_model t task1 iter1 -∗
vertex_model t task2 iter2 -∗
False.
Lemma vertex_model_finished t task iter :
vertex_model t task iter -∗
vertex_finished t -∗
False.
Lemma vertex_output_wand {t P R Q1} Q2 :
vertex_inv t P R -∗
vertex_output t Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex_output t Q2.
Lemma vertex_output_divide {t P R} Qs :
vertex_inv t P R -∗
vertex_output t ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex_output t Q.
Lemma vertex_output_split {t P R} Q1 Q2 :
vertex_inv t P R -∗
vertex_output t (Q1 ∗ Q2) ={⊤}=∗
vertex_output t Q1 ∗
vertex_output t Q2.
Lemma vertex_predecessor_finished t iter :
vertex_predecessor t iter -∗
vertex_ready iter -∗
vertex_finished t.
Lemma vertex_inv_finished t P R :
vertex_inv t P R -∗
vertex_finished t ={⊤}=∗
▷ □ R.
Lemma vertex_inv_finished' t P R :
£ 1 -∗
vertex_inv t P R -∗
vertex_finished t ={⊤}=∗
□ R.
Lemma vertex_inv_finished_output t P R Q :
vertex_inv t P R -∗
vertex_finished t -∗
vertex_output t Q ={⊤}=∗
▷^2 Q.
Lemma vertex_inv_finished_output' t P R Q :
£ 2 -∗
vertex_inv t P R -∗
vertex_finished t -∗
vertex_output t Q ={⊤}=∗
Q.
Lemma vertex٠create𑁒spec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t iter
, RET t;
vertex_inv t P R ∗
vertex_model t (default (fun: ≠ ⇒ true)%V task) iter ∗
vertex_output t P
}}}.
Lemma vertex٠create'𑁒spec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t iter
, RET t;
vertex_inv t P R ∗
vertex_model t (fun: "ctx" ⇒ task "ctx" ;; true) iter ∗
vertex_output t P
}}}.
Lemma vertex٠task𑁒spec t task iter :
{{{
vertex_model t task iter
}}}
vertex٠task t
{{{
RET task;
vertex_model t task iter
}}}.
Lemma vertex٠set_task𑁒spec t task1 iter task2 :
{{{
vertex_model t task1 iter
}}}
vertex٠set_task t task2
{{{
RET ();
vertex_model t task2 iter
}}}.
Lemma vertex٠precede𑁒spec t1 P1 R1 t2 P2 R2 task iter :
{{{
vertex_inv t1 P1 R1 ∗
vertex_inv t2 P2 R2 ∗
vertex_model t2 task iter
}}}
vertex٠precede t1 t2
{{{
RET ();
vertex_model t2 task iter ∗
vertex_predecessor t1 iter
}}}.
Lemma vertex٠release𑁒spec pool ctx scope t P R task iter :
{{{
pool_context pool ctx scope ∗
vertex_inv t P R ∗
vertex_model t task iter ∗
vertex_wp t P R task iter
}}}
vertex٠release ctx t
{{{
RET ();
pool_context pool ctx scope
}}}.
Lemma vertex٠release𑁒spec' pool ctx scope t P R task iter :
{{{
pool_context pool ctx scope ∗
vertex_inv t P R ∗
vertex_model t task iter ∗
( ∀ pool ctx scope,
pool_context pool ctx scope -∗
vertex_ready iter -∗
WP task ctx {{ res,
⌜res = true%V⌝ ∗
pool_context pool ctx scope ∗
▷ P ∗
▷ □ R
}}
)
}}}
vertex٠release ctx t
{{{
RET ();
pool_context pool ctx scope
}}}.
Lemma vertex٠yield𑁒spec t task' iter task :
{{{
vertex_model t task' iter
}}}
vertex٠yield t task
{{{
RET false;
vertex_model t task iter
}}}.
End vertex_G.
#[global] Opaque vertex_inv.
#[global] Opaque vertex_model.
#[global] Opaque vertex_output.
#[global] Opaque vertex_ready.
#[global] Opaque vertex_finished.
#[global] Opaque vertex_predecessor.