Library zoo_parabs.pool
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.ghost_list
lib.mono_gmultiset
lib.saved_prop
lib.spsc_prop.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
array
domain
ivar_4.
From zoo_parabs Require Export
base
pool__code.
From zoo_parabs Require Import
pool__types
ws_hub_std.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types v ctx hub task notification notify pred ivar waiter : val.
Implicit Types empty : emptiness.
Implicit Types own : ownership.
Implicit Types η : spsc_prop_name.
Implicit Types ω : gname.
#[local] Definition max_round_noyield :=
val_to_nat' pool٠max_round_noyield.
#[local] Lemma pool٠max_round_noyield :
pool٠max_round_noyield = #max_round_noyield.
Opaque pool__code.pool٠max_round_noyield.
Opaque max_round_noyield.
#[local] Definition max_round_yield :=
val_to_nat' pool٠max_round_yield.
#[local] Lemma pool٠max_round_yield :
pool٠max_round_yield = #max_round_yield.
Opaque pool__code.pool٠max_round_yield.
Opaque max_round_yield.
Record job :=
{ job_val : val
; job_name : gname
}.
Implicit Types job local global : job.
#[local] Instance job_inhabited : Inhabited job :=
populate
{|job_val := inhabitant
; job_name := inhabitant
|}.
#[local] Instance job_eq_dec : EqDecision job :=
ltac:(solve_decision).
#[local] Instance job_countable :
Countable job.
Implicit Types jobs locals ulocals globals : gmultiset job.
Implicit Types localss : list $ gmultiset job.
Definition pool_scope :=
gmultiset job.
#[global] Instance pool_scope_eq_dec : EqDecision pool_scope :=
_.
#[global] Instance pool_scope_countable :
Countable pool_scope.
Class PoolG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pool_G_domain_G :: DomainG Σ
; #[local] pool_G_ws_hub_G :: WsHubStdG Σ
; #[local] pool_G_saved_prop_G :: SavedPropG Σ
; #[local] pool_G_jobs_G :: MonoGmultisetG Σ job
; #[local] pool_G_locals_G :: GhostListG Σ (gmultiset job)
; #[local] pool_G_consumer_G :: SpscPropG Σ
}.
Definition pool_Σ :=
#[domain_Σ
; ws_hub_std_Σ
; saved_prop_Σ
; mono_gmultiset_Σ job
; ghost_list_Σ (gmultiset job)
; spsc_prop_Σ
].
#[global] Instance subG_pool_Σ Σ `{zoo_G : !ZooG Σ} :
subG pool_Σ Σ →
PoolG Σ.
Module base.
Section pool_G.
Context `{pool_G : PoolG Σ}.
Implicit Types t : location.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Implicit Types Ψ : val → iProp Σ.
Record pool_name :=
{ pool_name_size : nat
; pool_name_hub : val
; pool_name_domains : val
; pool_name_jobs : gname
; pool_name_locals : gname
}.
Implicit Types γ : pool_name.
Implicit Types γ_tokens : list gname.
#[global] Instance pool_name_eq_dec : EqDecision pool_name :=
ltac:(solve_decision).
#[global] Instance pool_name_countable :
Countable pool_name.
#[local] Definition pool_name_context γ (i : nat) :=
( #γ.(pool_name_size),
γ.(pool_name_hub),
#i
)%V.
#[local] Instance pool_name_context_inj γ :
Inj (=) (=) (pool_name_context γ).
#[local] Definition jobs_auth' γ_jobs own :=
mono_gmultiset_auth γ_jobs own.
#[local] Definition jobs_auth γ :=
jobs_auth' γ.(pool_name_jobs).
#[local] Definition jobs_elem γ :=
mono_gmultiset_elem γ.(pool_name_jobs).
#[local] Definition jobs_finished jobs : iProp Σ :=
[∗ mset] job ∈ jobs,
∃ P,
saved_prop job.(job_name) P ∗
□ P.
#[local] Definition locals_auth' sz γ_locals ulocals : iProp Σ :=
∃ localss,
⌜length localss = S sz⌝ ∗
ghost_list_auth γ_locals localss ∗
⌜ulocals = ⋃+ localss⌝.
#[local] Definition locals_auth γ :=
locals_auth' γ.(pool_name_size) γ.(pool_name_locals).
#[local] Instance : CustomIpat "locals_auth" :=
" ( %localss{} & %Hlocalss{} & Hauth{_{}} & -> ) ".
#[local] Definition locals_at_running γ_locals i scope : iProp Σ :=
∃ locals,
ghost_list_at γ_locals i Own (scope ⊎ locals) ∗
jobs_finished locals.
#[local] Instance : CustomIpat "locals_at_running" :=
" ( %locals{} & Hat{_{}} & Hjobs_finished_locals{} ) ".
#[local] Definition locals_at_finished γ_locals i : iProp Σ :=
∃ locals,
ghost_list_at γ_locals i Own locals.
#[local] Instance : CustomIpat "locals_at_finished" :=
" ( %locals{} & Hat{_{}} ) ".
#[local] Definition locals_at' γ_locals i scope : iProp Σ :=
match scope with
| Some scope ⇒
locals_at_running γ_locals i scope
| None ⇒
locals_at_finished γ_locals i
end.
#[local] Definition locals_at γ :=
locals_at' γ.(pool_name_locals).
#[local] Definition globals_model_running γ globals : iProp Σ :=
∃ jobs ulocals,
⌜jobs = globals ⊎ ulocals⌝ ∗
jobs_auth γ Own jobs ∗
locals_auth γ ulocals.
#[local] Instance : CustomIpat "globals_model_running" :=
" ( %jobs & %ulocals & -> & Hjobs_auth & Hlocals_auth ) ".
#[local] Definition globals_model_finished γ : iProp Σ :=
[∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i None.
#[local] Instance : CustomIpat "globals_model_finished" :=
" Hlocals_ats ".
#[local] Definition globals_model γ globals : iProp Σ :=
globals_model_running γ globals
∨ globals_model_finished γ.
#[local] Instance : CustomIpat "globals_model" :=
" [ (:globals_model_running) | (:globals_model_finished) ] ".
#[local] Definition context_1 γ i (scope : pool_scope) : iProp Σ :=
∃ empty,
ws_hub_std_owner γ.(pool_name_hub) i Nonblocked empty ∗
locals_at γ i (Some scope).
#[local] Instance : CustomIpat "context_1" :=
" ( %empty{} & Hhub_owner{_{}} & Hlocals_at{_{}} ) ".
#[local] Definition task_model γ task Ψ : iProp Σ :=
∀ i scope,
⌜i ≤ γ.(pool_name_size)⌝ -∗
context_1 γ i scope -∗
WP task (pool_name_context γ i) {{ v,
context_1 γ i scope ∗
Ψ v
}}.
#[local] Definition inv_inner γ : iProp Σ :=
∃ globals 𝑔𝑙𝑜𝑏𝑎𝑙𝑠,
⌜𝑔𝑙𝑜𝑏𝑎𝑙𝑠 = gmultiset_map job_val globals⌝ ∗
globals_model γ globals ∗
ws_hub_std_model γ.(pool_name_hub) 𝑔𝑙𝑜𝑏𝑎𝑙𝑠 ∗
[∗ mset] global ∈ globals,
task_model γ global.(job_val) (λ _,
∃ P,
saved_prop global.(job_name) P ∗
▷ □ P
).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %globals & %𝑔𝑙𝑜𝑏𝑎𝑙𝑠 & >%H𝑔𝑙𝑜𝑏𝑎𝑙𝑠 & >Hglobals_model & >Hhub_model & Hglobals ) ".
#[local] Definition inv_1 γ : iProp Σ :=
inv (nroot.@"inv") (inv_inner γ).
#[local] Definition inv_2 γ : iProp Σ :=
ws_hub_std_inv γ.(pool_name_hub) (nroot.@"hub") (S γ.(pool_name_size)) ∗
inv_1 γ.
#[local] Instance : CustomIpat "inv_2" :=
" ( #Hhub_inv{_{}} & #Hinv{_{}} ) ".
Definition pool_inv γ sz : iProp Σ :=
⌜sz = γ.(pool_name_size)⌝ ∗
inv_2 γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & {#Hinv_{};(:inv_2)} ) ".
#[local] Definition context_finished γ i : iProp Σ :=
ws_hub_std_owner γ.(pool_name_hub) i Nonblocked Empty ∗
locals_at γ i (Some ∅).
#[local] Instance : CustomIpat "context_finished" :=
" ( Hhub_owner{_{}} & Hlocals_at{_{}} ) ".
#[local] Definition context_2 γ i scope : iProp Σ :=
⌜i ≤ γ.(pool_name_size)⌝ ∗
inv_2 γ ∗
context_1 γ i scope.
#[local] Instance : CustomIpat "context_2" :=
" ( %Hi{} & {#Hinv_{};(:inv_2)} & { {lazy} Hctx{} ; {lazy} Hctx ; (:context_1 ={}) ; (:context_1) } ) ".
Definition pool_context γ ctx scope : iProp Σ :=
∃ i,
⌜ctx = pool_name_context γ i⌝ ∗
context_2 γ i scope.
#[local] Instance : CustomIpat "context" :=
" ( %i{} & {%Heq{};->} & (:context_2) ) ".
#[local] Definition worker_post γ i res : iProp Σ :=
⌜res = ()%V⌝ ∗
context_finished γ i.
#[local] Instance : CustomIpat "worker_post" :=
" ( -> & (:context_finished) ) ".
Definition pool_model t γ : iProp Σ :=
∃ empty doms,
⌜length doms = γ.(pool_name_size)⌝ ∗
t.[size] ↦□ #γ.(pool_name_size) ∗
t.[hub] ↦□ γ.(pool_name_hub) ∗
t.[domains] ↦□ γ.(pool_name_domains) ∗
inv_2 γ ∗
array_model γ.(pool_name_domains) DfracDiscarded doms ∗
( [∗ list] i ↦ dom ∈ doms,
domain_model dom (worker_post γ (S i))
) ∗
ws_hub_std_owner γ.(pool_name_hub) 0 Blocked empty ∗
locals_at γ 0 (Some ∅).
#[local] Instance : CustomIpat "model" :=
" ( %empty{} & %doms{} & %Hdoms{} & #Hl{}_size & #Hl{}_hub & #Hl{}_domains & {#Hinv{};(:inv_2)} & Hdomains{} & Hdoms{} & Hhub{}_owner & Hlocals_at{_{}} ) ".
Definition pool_finished γ : iProp Σ :=
∃ jobs,
jobs_auth γ Discard jobs ∗
jobs_finished jobs.
#[local] Instance : CustomIpat "finished" :=
" ( %jobs{} & Hjobs_auth{_{}} & Hjobs_finished{_jobs{}} ) ".
Definition pool_consumer γ P : iProp Σ :=
pool_finished γ ={⊤}=∗
P.
Definition pool_obligation γ P : iProp Σ :=
□ (
pool_finished γ -∗
▷ □ P
).
#[global] Instance pool_obligation_proper γ :
Proper ((≡) ==> (≡)) (pool_obligation γ).
#[global] Instance pool_consumer_proper γ :
Proper ((≡) ==> (≡)) (pool_consumer γ).
#[local] Instance globals_model_timeless γ globals :
Timeless (globals_model γ globals).
#[local] Instance jobs_elem_persistent γ job :
Persistent (jobs_elem γ job).
#[local] Instance jobs_finished_persistent jobs :
Persistent (jobs_finished jobs).
#[global] Instance pool_inv_persistent γ sz :
Persistent (pool_inv γ sz).
#[global] Instance pool_obligation_persistent γ P :
Persistent (pool_obligation γ P).
#[global] Instance pool_finished_persistent γ :
Persistent (pool_finished γ).
#[local] Lemma jobs_alloc :
⊢ |==>
∃ γ_jobs,
jobs_auth' γ_jobs Own ∅.
#[local] Lemma jobs_auth_discard γ jobs :
jobs_auth γ Own jobs ⊢ |==>
jobs_auth γ Discard jobs.
#[local] Lemma jobs_elem_valid γ own jobs job :
jobs_auth γ own jobs -∗
jobs_elem γ job -∗
⌜job ∈ jobs⌝.
#[local] Lemma jobs_insert {γ jobs} 𝑗𝑜𝑏 P :
jobs_auth γ Own jobs ⊢ |==>
∃ job,
⌜job.(job_val) = 𝑗𝑜𝑏⌝ ∗
jobs_auth γ Own ({[+job+]} ⊎ jobs) ∗
jobs_elem γ job ∗
saved_prop job.(job_name) P.
Opaque jobs_elem.
#[local] Lemma jobs_finished_empty :
⊢ jobs_finished ∅.
#[local] Lemma jobs_finished_elem_of job jobs :
job ∈ jobs →
jobs_finished jobs ⊢
∃ P,
saved_prop job.(job_name) P ∗
□ P.
#[local] Lemma jobs_finished_insert {jobs} job P :
jobs_finished jobs -∗
saved_prop job.(job_name) P -∗
□ P -∗
jobs_finished ({[+job+]} ⊎ jobs).
#[local] Lemma jobs_finished_union localss :
( [∗ list] locals ∈ localss,
jobs_finished locals
) ⊢
jobs_finished (⋃+ localss).
Opaque jobs_finished.
#[local] Lemma locals_alloc sz :
⊢ |==>
∃ γ_locals,
locals_auth' sz γ_locals ∅ ∗
[∗ list] i ∈ seq 0 (S sz),
locals_at' γ_locals i (Some ∅).
#[local] Lemma locals_at_exclusive γ i scope1 scope2 :
locals_at γ i scope1 -∗
locals_at γ i scope2 -∗
False.
#[local] Lemma locals_insert {γ ulocals i scope} local :
locals_auth γ ulocals -∗
locals_at γ i (Some scope) ==∗
locals_auth γ ({[+local+]} ⊎ ulocals) ∗
locals_at γ i (Some ({[+local+]} ⊎ scope)).
#[local] Lemma locals_at_finish γ i local P scope :
locals_at γ i (Some ({[+local+]} ⊎ scope)) -∗
saved_prop local.(job_name) P -∗
□ P -∗
locals_at γ i (Some scope).
#[local] Lemma locals_close γ ulocals :
locals_auth γ ulocals -∗
( [∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i (Some ∅)
) -∗
locals_auth γ ulocals ∗
( [∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i None
) ∗
jobs_finished ulocals.
Opaque locals_auth'.
Opaque locals_at'.
#[local] Lemma globals_model_init γ :
jobs_auth γ Own ∅ -∗
locals_auth γ ∅ -∗
globals_model γ ∅.
#[local] Lemma globals_model_locals_at γ globals i scope :
i ≤ γ.(pool_name_size) →
globals_model γ globals -∗
locals_at γ i scope -∗
globals_model_running γ globals ∗
locals_at γ i scope.
#[local] Lemma globals_model_push {γ globals} 𝑔𝑙𝑜𝑏𝑎𝑙 P i scope :
i ≤ γ.(pool_name_size) →
globals_model γ globals -∗
locals_at γ i scope ==∗
∃ global,
⌜global.(job_val) = 𝑔𝑙𝑜𝑏𝑎𝑙⌝ ∗
globals_model γ ({[+global+]} ⊎ globals) ∗
locals_at γ i scope ∗
jobs_elem γ global ∗
saved_prop global.(job_name) P.
#[local] Lemma globals_model_pop {γ globals} global globals' i scope :
i ≤ γ.(pool_name_size) →
globals = {[+global+]} ⊎ globals' →
globals_model γ globals -∗
locals_at γ i (Some scope) ==∗
globals_model γ globals' ∗
locals_at γ i (Some ({[+global+]} ⊎ scope)).
#[local] Lemma globals_model_close γ :
globals_model γ ∅ -∗
( [∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i (Some ∅)
) ==∗
∃ jobs,
globals_model γ ∅ ∗
jobs_auth γ Discard jobs ∗
jobs_finished jobs.
Opaque globals_model.
Lemma pool_inv_agree γ sz1 sz2 :
pool_inv γ sz1 -∗
pool_inv γ sz2 -∗
⌜sz1 = sz2⌝.
Lemma pool_obligation_wand {γ P1} P2 :
pool_obligation γ P1 -∗
□ (P1 -∗ P2) -∗
pool_obligation γ P2.
Lemma pool_obligation_split γ P1 P2 :
pool_obligation γ (P1 ∗ P2) ⊢
pool_obligation γ P1 ∗
pool_obligation γ P2.
Lemma pool_obligation_combine γ P1 P2 :
pool_obligation γ P1 -∗
pool_obligation γ P2 -∗
pool_obligation γ (P1 ∗ P2).
Lemma pool_obligation_finished γ P :
pool_obligation γ P -∗
pool_finished γ -∗
▷ □ P.
#[local] Lemma pool٠context𑁒spec {sz : Z} {hub} {i : Z} γ (i_ : nat) :
sz = γ.(pool_name_size) →
hub = γ.(pool_name_hub) →
i = i_ →
{{{
True
}}}
pool__code.pool٠context #sz hub #i
{{{
RET pool_name_context γ i_;
True
}}}.
#[local] Lemma pool٠context_main𑁒spec t γ :
{{{
t.[size] ↦□ #γ.(pool_name_size) ∗
t.[hub] ↦□ γ.(pool_name_hub)
}}}
pool٠context_main #t
{{{
RET pool_name_context γ 0;
True
}}}.
#[local] Lemma pool٠execute𑁒spec γ i scope task Ψ :
i ≤ γ.(pool_name_size) →
{{{
context_1 γ i scope ∗
task_model γ task Ψ
}}}
pool٠execute (pool_name_context γ i) task
{{{
v
, RET v;
context_1 γ i scope ∗
Ψ v
}}}.
#[local] Lemma pool٠worker𑁒spec γ i :
{{{
context_2 γ i ∅
}}}
pool٠worker (pool_name_context γ i)
{{{
res
, RET res;
worker_post γ i res
}}}.
Lemma pool٠create𑁒spec sz :
(0 ≤ sz)%Z →
{{{
True
}}}
pool٠create #sz
{{{
t γ
, RET #t;
pool_inv γ ₊sz ∗
pool_model t γ ∗
meta_token t ⊤
}}}.
Lemma pool٠run_on𑁒spec Ψ t γ task :
{{{
pool_model t γ ∗
( ∀ ctx scope,
pool_context γ ctx scope -∗
WP task ctx {{ v,
pool_context γ ctx scope ∗
Ψ v
}}
)
}}}
pool٠run_on #t task
{{{
v
, RET v;
pool_model t γ ∗
Ψ v
}}}.
Lemma pool٠close𑁒spec t γ :
{{{
pool_model t γ
}}}
pool٠close #t
{{{
RET ();
pool_finished γ
}}}.
Lemma pool٠run𑁒spec (Ψ : location → pool_name → val → iProp Σ) sz task :
(0 ≤ sz)%Z →
{{{
∀ t γ ctx scope,
pool_inv γ ₊sz -∗
meta_token t ⊤ -∗
pool_context γ ctx scope -∗
WP task ctx {{ v,
pool_context γ ctx scope ∗
Ψ t γ v
}}
}}}
pool٠run #sz task
{{{
t γ v
, RET v;
pool_finished γ ∗
Ψ t γ v
}}}.
Lemma pool٠size𑁒spec γ sz ctx scope :
{{{
pool_inv γ sz ∗
pool_context γ ctx scope
}}}
pool٠size ctx
{{{
RET #sz;
pool_context γ ctx scope
}}}.
Lemma pool٠async𑁒spec P Q γ ctx scope task :
{{{
pool_context γ ctx scope ∗
( ∀ ctx scope,
pool_context γ ctx scope -∗
WP task ctx {{ res,
pool_context γ ctx scope ∗
▷ P ∗
▷ □ Q
}}
)
}}}
pool٠async ctx task
{{{
RET ();
pool_context γ ctx scope ∗
pool_consumer γ P ∗
pool_obligation γ Q
}}}.
#[local] Lemma pool٠wait₀𑁒spec P_notification P_pred Q_pred γ ctx scope notification pred :
{{{
pool_context γ ctx scope ∗
P_notification ∗
□ (
∀ notify,
P_notification -∗
WP notify () {{ itype_unit }} -∗
WP notification notify {{ res,
⌜res = ()%V⌝ ∗
P_notification
}}
) ∗
P_pred ∗
□ (
P_pred -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q_pred else P_pred
}}
)
}}}
pool٠wait₀ ctx notification pred
{{{
RET ();
pool_context γ ctx scope ∗
Q_pred
}}}.
Lemma pool٠wait𑁒spec P_notification P_pred Q_pred γ ctx scope notification pred :
{{{
pool_context γ ctx scope ∗
P_notification ∗
( ∀ notify,
P_notification -∗
WP notify () {{ itype_unit }} -∗
WP notification notify {{ res,
⌜res = ()%V⌝ ∗
P_notification
}}
) ∗
P_pred ∗
□ (
P_pred -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q_pred else P_pred
}}
)
}}}
pool٠wait ctx notification pred
{{{
RET ();
pool_context γ ctx scope ∗
Q_pred
}}}.
Lemma pool٠wait_ivar𑁒spec `{ivar_G : !Ivar4G Σ} {context_name} γ ctx scope ivar Ψ Ξ (Γ : _ → context_name → _) :
{{{
pool_context γ ctx scope ∗
ivar_4_inv ivar Ψ Ξ Γ
}}}
pool٠wait_ivar ctx ivar
{{{
RET ();
£ 2 ∗
pool_context γ ctx scope ∗
ivar_4_resolved ivar
}}}.
End pool_G.
#[global] Opaque pool_scope.
#[global] Opaque pool_inv.
#[global] Opaque pool_model.
#[global] Opaque pool_context.
#[global] Opaque pool_consumer.
#[global] Opaque pool_obligation.
#[global] Opaque pool_finished.
End base.
From zoo_parabs Require
pool__opaque.
Section pool_G.
Context `{pool_G : PoolG Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Implicit Types γ : base.pool_name.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Implicit Types Ψ : val → iProp Σ.
Definition pool_inv t sz : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_inv γ sz.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition pool_context t ctx scope : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_context γ ctx scope.
#[local] Instance : CustomIpat "context" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hctx{_{}} ) ".
Definition pool_model t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_model 𝑡 γ.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition pool_finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hfinished{_{}} ) ".
Definition pool_consumer t P : iProp Σ :=
pool_finished t ={⊤}=∗
P.
Definition pool_obligation t P : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_obligation γ P.
#[local] Instance : CustomIpat "obligation" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hobligation{_{}} ) ".
#[global] Instance pool_obligation_proper t :
Proper ((≡) ==> (≡)) (pool_obligation t).
#[global] Instance pool_consumer_proper t :
Proper ((≡) ==> (≡)) (pool_consumer t).
#[global] Instance pool_inv_persistent t sz :
Persistent (pool_inv t sz).
#[global] Instance pool_obligation_persistent t P :
Persistent (pool_obligation t P).
#[global] Instance pool_finished_persistent t :
Persistent (pool_finished t).
Lemma pool_inv_agree t sz1 sz2 :
pool_inv t sz1 -∗
pool_inv t sz2 -∗
⌜sz1 = sz2⌝.
Lemma pool_consumer_intro {t} P :
(pool_finished t ={⊤}=∗ P) ⊢
pool_consumer t P.
Lemma pool_consumer_wand {t P1} P2 :
pool_consumer t P1 -∗
(P1 -∗ P2) -∗
pool_consumer t P2.
Lemma pool_consumer_combine t P1 P2 :
pool_consumer t P1 -∗
pool_consumer t P2 -∗
pool_consumer t (P1 ∗ P2).
Lemma pool_consumer_or t P1 P2 :
( pool_consumer t P1
∨ pool_consumer t P2
) ⊢
pool_consumer t (P1 ∨ P2).
Lemma pool_consumer_exist {A} {t} (Φ : A → iProp Σ) x :
pool_consumer t (Φ x) ⊢
pool_consumer t (∃ x, Φ x).
Lemma pool_consumer_forall {A} {t} (Φ : A → iProp Σ) x :
pool_consumer t (∀ x, Φ x) ⊢
pool_consumer t (Φ x).
Lemma pool_consumer_finished t P :
pool_consumer t P -∗
pool_finished t ={⊤}=∗
P.
#[global] Instance pool_consumer_mono t :
Proper ((⊢) ==> (⊢)) (pool_consumer t).
#[global] Instance pool_consumer_flip_mono t :
Proper (flip (⊢) ==> flip (⊢)) (pool_consumer t).
Lemma pool_obligation_wand {t P1} P2 :
pool_obligation t P1 -∗
□ (P1 -∗ P2) -∗
pool_obligation t P2.
Lemma pool_obligation_split t P1 P2 :
pool_obligation t (P1 ∗ P2) ⊢
pool_obligation t P1 ∗
pool_obligation t P2.
Lemma pool_obligation_combine t P1 P2 :
pool_obligation t P1 -∗
pool_obligation t P2 -∗
pool_obligation t (P1 ∗ P2).
Lemma pool_obligation_finished t P :
pool_obligation t P -∗
pool_finished t -∗
▷ □ P.
Lemma pool٠create𑁒spec sz :
(0 ≤ sz)%Z →
{{{
True
}}}
pool٠create #sz
{{{
t
, RET t;
pool_inv t ₊sz ∗
pool_model t
}}}.
Lemma pool٠run_on𑁒spec Ψ t task :
{{{
pool_model t ∗
( ∀ ctx scope,
pool_context t ctx scope -∗
WP task ctx {{ v,
pool_context t ctx scope ∗
Ψ v
}}
)
}}}
pool٠run_on t task
{{{
v
, RET v;
pool_model t ∗
Ψ v
}}}.
Lemma pool٠close𑁒spec t :
{{{
pool_model t
}}}
pool٠close t
{{{
RET ();
pool_finished t
}}}.
Lemma pool٠run𑁒spec (Ψ : val → val → iProp Σ) sz task :
(0 ≤ sz)%Z →
{{{
∀ t ctx scope,
pool_inv t ₊sz -∗
pool_context t ctx scope -∗
WP task ctx {{ v,
pool_context t ctx scope ∗
Ψ t v
}}
}}}
pool٠run #sz task
{{{
t v
, RET v;
pool_finished t ∗
Ψ t v
}}}.
Lemma pool٠size𑁒spec t sz ctx scope :
{{{
pool_inv t sz ∗
pool_context t ctx scope
}}}
pool٠size ctx
{{{
RET #sz;
pool_context t ctx scope
}}}.
Lemma pool٠async𑁒spec P Q t ctx scope task :
{{{
pool_context t ctx scope ∗
( ∀ ctx scope,
pool_context t ctx scope -∗
WP task ctx {{ res,
pool_context t ctx scope ∗
▷ P ∗
▷ □ Q
}}
)
}}}
pool٠async ctx task
{{{
RET ();
pool_context t ctx scope ∗
pool_consumer t P ∗
pool_obligation t Q
}}}.
Lemma pool٠wait𑁒spec P_notification P_pred Q_pred t ctx scope notification pred :
{{{
pool_context t ctx scope ∗
P_notification ∗
( ∀ notify,
P_notification -∗
WP notify () {{ itype_unit }} -∗
WP notification notify {{ res,
⌜res = ()%V⌝ ∗
P_notification
}}
) ∗
P_pred ∗
□ (
P_pred -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q_pred else P_pred
}}
)
}}}
pool٠wait ctx notification pred
{{{
RET ();
pool_context t ctx scope ∗
Q_pred
}}}.
Lemma pool٠wait_ivar𑁒spec `{ivar_G : !Ivar4G Σ} {context_name} t ctx scope ivar Ψ Ξ (Γ : _ → context_name → _) :
{{{
pool_context t ctx scope ∗
ivar_4_inv ivar Ψ Ξ Γ
}}}
pool٠wait_ivar ctx ivar
{{{
RET ();
£ 2 ∗
pool_context t ctx scope ∗
ivar_4_resolved ivar
}}}.
End pool_G.
#[global] Opaque pool_scope.
#[global] Opaque pool_inv.
#[global] Opaque pool_model.
#[global] Opaque pool_context.
#[global] Opaque pool_obligation.
#[global] Opaque pool_consumer.
#[global] Opaque pool_finished.
Section pool_G.
Context `{pool_G : PoolG Σ}.
Implicit Types P Q R : iProp Σ.
#[global] Instance from_assumption_pool_consumer t p P Q :
FromAssumption p P Q →
KnownRFromAssumption p P (pool_consumer t Q).
#[global] Instance from_pure_pool_consumer t a P ϕ :
FromPure a P ϕ →
FromPure a (pool_consumer t P) ϕ.
#[global] Instance into_wand_pool_consumer t p q R P Q :
IntoWand false false R P Q →
IntoWand p q (pool_consumer t R) (pool_consumer t P) (pool_consumer t Q).
#[global] Instance into_wand_pool_consumer_persistent t p q R P Q :
IntoWand false q R P Q →
IntoWand p q (pool_consumer t R) P (pool_consumer t Q).
#[global] Instance into_wand_pool_consumer_args t p q R P Q :
IntoWand p false R P Q →
IntoWand' p q R (pool_consumer t P) (pool_consumer t Q).
#[global] Instance from_sep_pool_consumer t P Q1 Q2 :
FromSep P Q1 Q2 →
FromSep (pool_consumer t P) (pool_consumer t Q1) (pool_consumer t Q2).
#[global] Instance from_or_pool_consumer t P Q1 Q2 :
FromOr P Q1 Q2 →
FromOr (pool_consumer t P) (pool_consumer t Q1) (pool_consumer t Q2).
#[global] Instance from_exist_pool_consumer t {A} P (Φ : A → iProp Σ) :
FromExist P Φ →
FromExist (pool_consumer t P) (λ a, pool_consumer t (Φ a)).
#[global] Instance into_forall_pool_consumer t {A} P (Φ : A → iProp Σ) :
IntoForall P Φ →
IntoForall (pool_consumer t P) (λ a, pool_consumer t (Φ a)).
#[global] Instance from_modal_pool_consumer t P :
FromModal True modality_id (pool_consumer t P) (pool_consumer t P) P.
#[global] Instance elim_modal_pool_consumer t p P Q :
ElimModal True p false (pool_consumer t P) P (pool_consumer t Q) (pool_consumer t Q).
#[global] Instance add_modal_pool_consumer t P Q :
AddModal (pool_consumer t P) P (pool_consumer t Q).
#[global] Instance frame_pool_consumer t p R P Q :
Frame p R P Q →
Frame p R (pool_consumer t P) (pool_consumer t Q)
| 2.
End pool_G.
prelude.
From zoo.common Require Import
countable
gmultiset.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.ghost_list
lib.mono_gmultiset
lib.saved_prop
lib.spsc_prop.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
array
domain
ivar_4.
From zoo_parabs Require Export
base
pool__code.
From zoo_parabs Require Import
pool__types
ws_hub_std.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types v ctx hub task notification notify pred ivar waiter : val.
Implicit Types empty : emptiness.
Implicit Types own : ownership.
Implicit Types η : spsc_prop_name.
Implicit Types ω : gname.
#[local] Definition max_round_noyield :=
val_to_nat' pool٠max_round_noyield.
#[local] Lemma pool٠max_round_noyield :
pool٠max_round_noyield = #max_round_noyield.
Opaque pool__code.pool٠max_round_noyield.
Opaque max_round_noyield.
#[local] Definition max_round_yield :=
val_to_nat' pool٠max_round_yield.
#[local] Lemma pool٠max_round_yield :
pool٠max_round_yield = #max_round_yield.
Opaque pool__code.pool٠max_round_yield.
Opaque max_round_yield.
Record job :=
{ job_val : val
; job_name : gname
}.
Implicit Types job local global : job.
#[local] Instance job_inhabited : Inhabited job :=
populate
{|job_val := inhabitant
; job_name := inhabitant
|}.
#[local] Instance job_eq_dec : EqDecision job :=
ltac:(solve_decision).
#[local] Instance job_countable :
Countable job.
Implicit Types jobs locals ulocals globals : gmultiset job.
Implicit Types localss : list $ gmultiset job.
Definition pool_scope :=
gmultiset job.
#[global] Instance pool_scope_eq_dec : EqDecision pool_scope :=
_.
#[global] Instance pool_scope_countable :
Countable pool_scope.
Class PoolG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pool_G_domain_G :: DomainG Σ
; #[local] pool_G_ws_hub_G :: WsHubStdG Σ
; #[local] pool_G_saved_prop_G :: SavedPropG Σ
; #[local] pool_G_jobs_G :: MonoGmultisetG Σ job
; #[local] pool_G_locals_G :: GhostListG Σ (gmultiset job)
; #[local] pool_G_consumer_G :: SpscPropG Σ
}.
Definition pool_Σ :=
#[domain_Σ
; ws_hub_std_Σ
; saved_prop_Σ
; mono_gmultiset_Σ job
; ghost_list_Σ (gmultiset job)
; spsc_prop_Σ
].
#[global] Instance subG_pool_Σ Σ `{zoo_G : !ZooG Σ} :
subG pool_Σ Σ →
PoolG Σ.
Module base.
Section pool_G.
Context `{pool_G : PoolG Σ}.
Implicit Types t : location.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Implicit Types Ψ : val → iProp Σ.
Record pool_name :=
{ pool_name_size : nat
; pool_name_hub : val
; pool_name_domains : val
; pool_name_jobs : gname
; pool_name_locals : gname
}.
Implicit Types γ : pool_name.
Implicit Types γ_tokens : list gname.
#[global] Instance pool_name_eq_dec : EqDecision pool_name :=
ltac:(solve_decision).
#[global] Instance pool_name_countable :
Countable pool_name.
#[local] Definition pool_name_context γ (i : nat) :=
( #γ.(pool_name_size),
γ.(pool_name_hub),
#i
)%V.
#[local] Instance pool_name_context_inj γ :
Inj (=) (=) (pool_name_context γ).
#[local] Definition jobs_auth' γ_jobs own :=
mono_gmultiset_auth γ_jobs own.
#[local] Definition jobs_auth γ :=
jobs_auth' γ.(pool_name_jobs).
#[local] Definition jobs_elem γ :=
mono_gmultiset_elem γ.(pool_name_jobs).
#[local] Definition jobs_finished jobs : iProp Σ :=
[∗ mset] job ∈ jobs,
∃ P,
saved_prop job.(job_name) P ∗
□ P.
#[local] Definition locals_auth' sz γ_locals ulocals : iProp Σ :=
∃ localss,
⌜length localss = S sz⌝ ∗
ghost_list_auth γ_locals localss ∗
⌜ulocals = ⋃+ localss⌝.
#[local] Definition locals_auth γ :=
locals_auth' γ.(pool_name_size) γ.(pool_name_locals).
#[local] Instance : CustomIpat "locals_auth" :=
" ( %localss{} & %Hlocalss{} & Hauth{_{}} & -> ) ".
#[local] Definition locals_at_running γ_locals i scope : iProp Σ :=
∃ locals,
ghost_list_at γ_locals i Own (scope ⊎ locals) ∗
jobs_finished locals.
#[local] Instance : CustomIpat "locals_at_running" :=
" ( %locals{} & Hat{_{}} & Hjobs_finished_locals{} ) ".
#[local] Definition locals_at_finished γ_locals i : iProp Σ :=
∃ locals,
ghost_list_at γ_locals i Own locals.
#[local] Instance : CustomIpat "locals_at_finished" :=
" ( %locals{} & Hat{_{}} ) ".
#[local] Definition locals_at' γ_locals i scope : iProp Σ :=
match scope with
| Some scope ⇒
locals_at_running γ_locals i scope
| None ⇒
locals_at_finished γ_locals i
end.
#[local] Definition locals_at γ :=
locals_at' γ.(pool_name_locals).
#[local] Definition globals_model_running γ globals : iProp Σ :=
∃ jobs ulocals,
⌜jobs = globals ⊎ ulocals⌝ ∗
jobs_auth γ Own jobs ∗
locals_auth γ ulocals.
#[local] Instance : CustomIpat "globals_model_running" :=
" ( %jobs & %ulocals & -> & Hjobs_auth & Hlocals_auth ) ".
#[local] Definition globals_model_finished γ : iProp Σ :=
[∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i None.
#[local] Instance : CustomIpat "globals_model_finished" :=
" Hlocals_ats ".
#[local] Definition globals_model γ globals : iProp Σ :=
globals_model_running γ globals
∨ globals_model_finished γ.
#[local] Instance : CustomIpat "globals_model" :=
" [ (:globals_model_running) | (:globals_model_finished) ] ".
#[local] Definition context_1 γ i (scope : pool_scope) : iProp Σ :=
∃ empty,
ws_hub_std_owner γ.(pool_name_hub) i Nonblocked empty ∗
locals_at γ i (Some scope).
#[local] Instance : CustomIpat "context_1" :=
" ( %empty{} & Hhub_owner{_{}} & Hlocals_at{_{}} ) ".
#[local] Definition task_model γ task Ψ : iProp Σ :=
∀ i scope,
⌜i ≤ γ.(pool_name_size)⌝ -∗
context_1 γ i scope -∗
WP task (pool_name_context γ i) {{ v,
context_1 γ i scope ∗
Ψ v
}}.
#[local] Definition inv_inner γ : iProp Σ :=
∃ globals 𝑔𝑙𝑜𝑏𝑎𝑙𝑠,
⌜𝑔𝑙𝑜𝑏𝑎𝑙𝑠 = gmultiset_map job_val globals⌝ ∗
globals_model γ globals ∗
ws_hub_std_model γ.(pool_name_hub) 𝑔𝑙𝑜𝑏𝑎𝑙𝑠 ∗
[∗ mset] global ∈ globals,
task_model γ global.(job_val) (λ _,
∃ P,
saved_prop global.(job_name) P ∗
▷ □ P
).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %globals & %𝑔𝑙𝑜𝑏𝑎𝑙𝑠 & >%H𝑔𝑙𝑜𝑏𝑎𝑙𝑠 & >Hglobals_model & >Hhub_model & Hglobals ) ".
#[local] Definition inv_1 γ : iProp Σ :=
inv (nroot.@"inv") (inv_inner γ).
#[local] Definition inv_2 γ : iProp Σ :=
ws_hub_std_inv γ.(pool_name_hub) (nroot.@"hub") (S γ.(pool_name_size)) ∗
inv_1 γ.
#[local] Instance : CustomIpat "inv_2" :=
" ( #Hhub_inv{_{}} & #Hinv{_{}} ) ".
Definition pool_inv γ sz : iProp Σ :=
⌜sz = γ.(pool_name_size)⌝ ∗
inv_2 γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & {#Hinv_{};(:inv_2)} ) ".
#[local] Definition context_finished γ i : iProp Σ :=
ws_hub_std_owner γ.(pool_name_hub) i Nonblocked Empty ∗
locals_at γ i (Some ∅).
#[local] Instance : CustomIpat "context_finished" :=
" ( Hhub_owner{_{}} & Hlocals_at{_{}} ) ".
#[local] Definition context_2 γ i scope : iProp Σ :=
⌜i ≤ γ.(pool_name_size)⌝ ∗
inv_2 γ ∗
context_1 γ i scope.
#[local] Instance : CustomIpat "context_2" :=
" ( %Hi{} & {#Hinv_{};(:inv_2)} & { {lazy} Hctx{} ; {lazy} Hctx ; (:context_1 ={}) ; (:context_1) } ) ".
Definition pool_context γ ctx scope : iProp Σ :=
∃ i,
⌜ctx = pool_name_context γ i⌝ ∗
context_2 γ i scope.
#[local] Instance : CustomIpat "context" :=
" ( %i{} & {%Heq{};->} & (:context_2) ) ".
#[local] Definition worker_post γ i res : iProp Σ :=
⌜res = ()%V⌝ ∗
context_finished γ i.
#[local] Instance : CustomIpat "worker_post" :=
" ( -> & (:context_finished) ) ".
Definition pool_model t γ : iProp Σ :=
∃ empty doms,
⌜length doms = γ.(pool_name_size)⌝ ∗
t.[size] ↦□ #γ.(pool_name_size) ∗
t.[hub] ↦□ γ.(pool_name_hub) ∗
t.[domains] ↦□ γ.(pool_name_domains) ∗
inv_2 γ ∗
array_model γ.(pool_name_domains) DfracDiscarded doms ∗
( [∗ list] i ↦ dom ∈ doms,
domain_model dom (worker_post γ (S i))
) ∗
ws_hub_std_owner γ.(pool_name_hub) 0 Blocked empty ∗
locals_at γ 0 (Some ∅).
#[local] Instance : CustomIpat "model" :=
" ( %empty{} & %doms{} & %Hdoms{} & #Hl{}_size & #Hl{}_hub & #Hl{}_domains & {#Hinv{};(:inv_2)} & Hdomains{} & Hdoms{} & Hhub{}_owner & Hlocals_at{_{}} ) ".
Definition pool_finished γ : iProp Σ :=
∃ jobs,
jobs_auth γ Discard jobs ∗
jobs_finished jobs.
#[local] Instance : CustomIpat "finished" :=
" ( %jobs{} & Hjobs_auth{_{}} & Hjobs_finished{_jobs{}} ) ".
Definition pool_consumer γ P : iProp Σ :=
pool_finished γ ={⊤}=∗
P.
Definition pool_obligation γ P : iProp Σ :=
□ (
pool_finished γ -∗
▷ □ P
).
#[global] Instance pool_obligation_proper γ :
Proper ((≡) ==> (≡)) (pool_obligation γ).
#[global] Instance pool_consumer_proper γ :
Proper ((≡) ==> (≡)) (pool_consumer γ).
#[local] Instance globals_model_timeless γ globals :
Timeless (globals_model γ globals).
#[local] Instance jobs_elem_persistent γ job :
Persistent (jobs_elem γ job).
#[local] Instance jobs_finished_persistent jobs :
Persistent (jobs_finished jobs).
#[global] Instance pool_inv_persistent γ sz :
Persistent (pool_inv γ sz).
#[global] Instance pool_obligation_persistent γ P :
Persistent (pool_obligation γ P).
#[global] Instance pool_finished_persistent γ :
Persistent (pool_finished γ).
#[local] Lemma jobs_alloc :
⊢ |==>
∃ γ_jobs,
jobs_auth' γ_jobs Own ∅.
#[local] Lemma jobs_auth_discard γ jobs :
jobs_auth γ Own jobs ⊢ |==>
jobs_auth γ Discard jobs.
#[local] Lemma jobs_elem_valid γ own jobs job :
jobs_auth γ own jobs -∗
jobs_elem γ job -∗
⌜job ∈ jobs⌝.
#[local] Lemma jobs_insert {γ jobs} 𝑗𝑜𝑏 P :
jobs_auth γ Own jobs ⊢ |==>
∃ job,
⌜job.(job_val) = 𝑗𝑜𝑏⌝ ∗
jobs_auth γ Own ({[+job+]} ⊎ jobs) ∗
jobs_elem γ job ∗
saved_prop job.(job_name) P.
Opaque jobs_elem.
#[local] Lemma jobs_finished_empty :
⊢ jobs_finished ∅.
#[local] Lemma jobs_finished_elem_of job jobs :
job ∈ jobs →
jobs_finished jobs ⊢
∃ P,
saved_prop job.(job_name) P ∗
□ P.
#[local] Lemma jobs_finished_insert {jobs} job P :
jobs_finished jobs -∗
saved_prop job.(job_name) P -∗
□ P -∗
jobs_finished ({[+job+]} ⊎ jobs).
#[local] Lemma jobs_finished_union localss :
( [∗ list] locals ∈ localss,
jobs_finished locals
) ⊢
jobs_finished (⋃+ localss).
Opaque jobs_finished.
#[local] Lemma locals_alloc sz :
⊢ |==>
∃ γ_locals,
locals_auth' sz γ_locals ∅ ∗
[∗ list] i ∈ seq 0 (S sz),
locals_at' γ_locals i (Some ∅).
#[local] Lemma locals_at_exclusive γ i scope1 scope2 :
locals_at γ i scope1 -∗
locals_at γ i scope2 -∗
False.
#[local] Lemma locals_insert {γ ulocals i scope} local :
locals_auth γ ulocals -∗
locals_at γ i (Some scope) ==∗
locals_auth γ ({[+local+]} ⊎ ulocals) ∗
locals_at γ i (Some ({[+local+]} ⊎ scope)).
#[local] Lemma locals_at_finish γ i local P scope :
locals_at γ i (Some ({[+local+]} ⊎ scope)) -∗
saved_prop local.(job_name) P -∗
□ P -∗
locals_at γ i (Some scope).
#[local] Lemma locals_close γ ulocals :
locals_auth γ ulocals -∗
( [∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i (Some ∅)
) -∗
locals_auth γ ulocals ∗
( [∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i None
) ∗
jobs_finished ulocals.
Opaque locals_auth'.
Opaque locals_at'.
#[local] Lemma globals_model_init γ :
jobs_auth γ Own ∅ -∗
locals_auth γ ∅ -∗
globals_model γ ∅.
#[local] Lemma globals_model_locals_at γ globals i scope :
i ≤ γ.(pool_name_size) →
globals_model γ globals -∗
locals_at γ i scope -∗
globals_model_running γ globals ∗
locals_at γ i scope.
#[local] Lemma globals_model_push {γ globals} 𝑔𝑙𝑜𝑏𝑎𝑙 P i scope :
i ≤ γ.(pool_name_size) →
globals_model γ globals -∗
locals_at γ i scope ==∗
∃ global,
⌜global.(job_val) = 𝑔𝑙𝑜𝑏𝑎𝑙⌝ ∗
globals_model γ ({[+global+]} ⊎ globals) ∗
locals_at γ i scope ∗
jobs_elem γ global ∗
saved_prop global.(job_name) P.
#[local] Lemma globals_model_pop {γ globals} global globals' i scope :
i ≤ γ.(pool_name_size) →
globals = {[+global+]} ⊎ globals' →
globals_model γ globals -∗
locals_at γ i (Some scope) ==∗
globals_model γ globals' ∗
locals_at γ i (Some ({[+global+]} ⊎ scope)).
#[local] Lemma globals_model_close γ :
globals_model γ ∅ -∗
( [∗ list] i ∈ seq 0 (S γ.(pool_name_size)),
locals_at γ i (Some ∅)
) ==∗
∃ jobs,
globals_model γ ∅ ∗
jobs_auth γ Discard jobs ∗
jobs_finished jobs.
Opaque globals_model.
Lemma pool_inv_agree γ sz1 sz2 :
pool_inv γ sz1 -∗
pool_inv γ sz2 -∗
⌜sz1 = sz2⌝.
Lemma pool_obligation_wand {γ P1} P2 :
pool_obligation γ P1 -∗
□ (P1 -∗ P2) -∗
pool_obligation γ P2.
Lemma pool_obligation_split γ P1 P2 :
pool_obligation γ (P1 ∗ P2) ⊢
pool_obligation γ P1 ∗
pool_obligation γ P2.
Lemma pool_obligation_combine γ P1 P2 :
pool_obligation γ P1 -∗
pool_obligation γ P2 -∗
pool_obligation γ (P1 ∗ P2).
Lemma pool_obligation_finished γ P :
pool_obligation γ P -∗
pool_finished γ -∗
▷ □ P.
#[local] Lemma pool٠context𑁒spec {sz : Z} {hub} {i : Z} γ (i_ : nat) :
sz = γ.(pool_name_size) →
hub = γ.(pool_name_hub) →
i = i_ →
{{{
True
}}}
pool__code.pool٠context #sz hub #i
{{{
RET pool_name_context γ i_;
True
}}}.
#[local] Lemma pool٠context_main𑁒spec t γ :
{{{
t.[size] ↦□ #γ.(pool_name_size) ∗
t.[hub] ↦□ γ.(pool_name_hub)
}}}
pool٠context_main #t
{{{
RET pool_name_context γ 0;
True
}}}.
#[local] Lemma pool٠execute𑁒spec γ i scope task Ψ :
i ≤ γ.(pool_name_size) →
{{{
context_1 γ i scope ∗
task_model γ task Ψ
}}}
pool٠execute (pool_name_context γ i) task
{{{
v
, RET v;
context_1 γ i scope ∗
Ψ v
}}}.
#[local] Lemma pool٠worker𑁒spec γ i :
{{{
context_2 γ i ∅
}}}
pool٠worker (pool_name_context γ i)
{{{
res
, RET res;
worker_post γ i res
}}}.
Lemma pool٠create𑁒spec sz :
(0 ≤ sz)%Z →
{{{
True
}}}
pool٠create #sz
{{{
t γ
, RET #t;
pool_inv γ ₊sz ∗
pool_model t γ ∗
meta_token t ⊤
}}}.
Lemma pool٠run_on𑁒spec Ψ t γ task :
{{{
pool_model t γ ∗
( ∀ ctx scope,
pool_context γ ctx scope -∗
WP task ctx {{ v,
pool_context γ ctx scope ∗
Ψ v
}}
)
}}}
pool٠run_on #t task
{{{
v
, RET v;
pool_model t γ ∗
Ψ v
}}}.
Lemma pool٠close𑁒spec t γ :
{{{
pool_model t γ
}}}
pool٠close #t
{{{
RET ();
pool_finished γ
}}}.
Lemma pool٠run𑁒spec (Ψ : location → pool_name → val → iProp Σ) sz task :
(0 ≤ sz)%Z →
{{{
∀ t γ ctx scope,
pool_inv γ ₊sz -∗
meta_token t ⊤ -∗
pool_context γ ctx scope -∗
WP task ctx {{ v,
pool_context γ ctx scope ∗
Ψ t γ v
}}
}}}
pool٠run #sz task
{{{
t γ v
, RET v;
pool_finished γ ∗
Ψ t γ v
}}}.
Lemma pool٠size𑁒spec γ sz ctx scope :
{{{
pool_inv γ sz ∗
pool_context γ ctx scope
}}}
pool٠size ctx
{{{
RET #sz;
pool_context γ ctx scope
}}}.
Lemma pool٠async𑁒spec P Q γ ctx scope task :
{{{
pool_context γ ctx scope ∗
( ∀ ctx scope,
pool_context γ ctx scope -∗
WP task ctx {{ res,
pool_context γ ctx scope ∗
▷ P ∗
▷ □ Q
}}
)
}}}
pool٠async ctx task
{{{
RET ();
pool_context γ ctx scope ∗
pool_consumer γ P ∗
pool_obligation γ Q
}}}.
#[local] Lemma pool٠wait₀𑁒spec P_notification P_pred Q_pred γ ctx scope notification pred :
{{{
pool_context γ ctx scope ∗
P_notification ∗
□ (
∀ notify,
P_notification -∗
WP notify () {{ itype_unit }} -∗
WP notification notify {{ res,
⌜res = ()%V⌝ ∗
P_notification
}}
) ∗
P_pred ∗
□ (
P_pred -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q_pred else P_pred
}}
)
}}}
pool٠wait₀ ctx notification pred
{{{
RET ();
pool_context γ ctx scope ∗
Q_pred
}}}.
Lemma pool٠wait𑁒spec P_notification P_pred Q_pred γ ctx scope notification pred :
{{{
pool_context γ ctx scope ∗
P_notification ∗
( ∀ notify,
P_notification -∗
WP notify () {{ itype_unit }} -∗
WP notification notify {{ res,
⌜res = ()%V⌝ ∗
P_notification
}}
) ∗
P_pred ∗
□ (
P_pred -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q_pred else P_pred
}}
)
}}}
pool٠wait ctx notification pred
{{{
RET ();
pool_context γ ctx scope ∗
Q_pred
}}}.
Lemma pool٠wait_ivar𑁒spec `{ivar_G : !Ivar4G Σ} {context_name} γ ctx scope ivar Ψ Ξ (Γ : _ → context_name → _) :
{{{
pool_context γ ctx scope ∗
ivar_4_inv ivar Ψ Ξ Γ
}}}
pool٠wait_ivar ctx ivar
{{{
RET ();
£ 2 ∗
pool_context γ ctx scope ∗
ivar_4_resolved ivar
}}}.
End pool_G.
#[global] Opaque pool_scope.
#[global] Opaque pool_inv.
#[global] Opaque pool_model.
#[global] Opaque pool_context.
#[global] Opaque pool_consumer.
#[global] Opaque pool_obligation.
#[global] Opaque pool_finished.
End base.
From zoo_parabs Require
pool__opaque.
Section pool_G.
Context `{pool_G : PoolG Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Implicit Types γ : base.pool_name.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Implicit Types Ψ : val → iProp Σ.
Definition pool_inv t sz : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_inv γ sz.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition pool_context t ctx scope : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_context γ ctx scope.
#[local] Instance : CustomIpat "context" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hctx{_{}} ) ".
Definition pool_model t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_model 𝑡 γ.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition pool_finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hfinished{_{}} ) ".
Definition pool_consumer t P : iProp Σ :=
pool_finished t ={⊤}=∗
P.
Definition pool_obligation t P : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.pool_obligation γ P.
#[local] Instance : CustomIpat "obligation" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hobligation{_{}} ) ".
#[global] Instance pool_obligation_proper t :
Proper ((≡) ==> (≡)) (pool_obligation t).
#[global] Instance pool_consumer_proper t :
Proper ((≡) ==> (≡)) (pool_consumer t).
#[global] Instance pool_inv_persistent t sz :
Persistent (pool_inv t sz).
#[global] Instance pool_obligation_persistent t P :
Persistent (pool_obligation t P).
#[global] Instance pool_finished_persistent t :
Persistent (pool_finished t).
Lemma pool_inv_agree t sz1 sz2 :
pool_inv t sz1 -∗
pool_inv t sz2 -∗
⌜sz1 = sz2⌝.
Lemma pool_consumer_intro {t} P :
(pool_finished t ={⊤}=∗ P) ⊢
pool_consumer t P.
Lemma pool_consumer_wand {t P1} P2 :
pool_consumer t P1 -∗
(P1 -∗ P2) -∗
pool_consumer t P2.
Lemma pool_consumer_combine t P1 P2 :
pool_consumer t P1 -∗
pool_consumer t P2 -∗
pool_consumer t (P1 ∗ P2).
Lemma pool_consumer_or t P1 P2 :
( pool_consumer t P1
∨ pool_consumer t P2
) ⊢
pool_consumer t (P1 ∨ P2).
Lemma pool_consumer_exist {A} {t} (Φ : A → iProp Σ) x :
pool_consumer t (Φ x) ⊢
pool_consumer t (∃ x, Φ x).
Lemma pool_consumer_forall {A} {t} (Φ : A → iProp Σ) x :
pool_consumer t (∀ x, Φ x) ⊢
pool_consumer t (Φ x).
Lemma pool_consumer_finished t P :
pool_consumer t P -∗
pool_finished t ={⊤}=∗
P.
#[global] Instance pool_consumer_mono t :
Proper ((⊢) ==> (⊢)) (pool_consumer t).
#[global] Instance pool_consumer_flip_mono t :
Proper (flip (⊢) ==> flip (⊢)) (pool_consumer t).
Lemma pool_obligation_wand {t P1} P2 :
pool_obligation t P1 -∗
□ (P1 -∗ P2) -∗
pool_obligation t P2.
Lemma pool_obligation_split t P1 P2 :
pool_obligation t (P1 ∗ P2) ⊢
pool_obligation t P1 ∗
pool_obligation t P2.
Lemma pool_obligation_combine t P1 P2 :
pool_obligation t P1 -∗
pool_obligation t P2 -∗
pool_obligation t (P1 ∗ P2).
Lemma pool_obligation_finished t P :
pool_obligation t P -∗
pool_finished t -∗
▷ □ P.
Lemma pool٠create𑁒spec sz :
(0 ≤ sz)%Z →
{{{
True
}}}
pool٠create #sz
{{{
t
, RET t;
pool_inv t ₊sz ∗
pool_model t
}}}.
Lemma pool٠run_on𑁒spec Ψ t task :
{{{
pool_model t ∗
( ∀ ctx scope,
pool_context t ctx scope -∗
WP task ctx {{ v,
pool_context t ctx scope ∗
Ψ v
}}
)
}}}
pool٠run_on t task
{{{
v
, RET v;
pool_model t ∗
Ψ v
}}}.
Lemma pool٠close𑁒spec t :
{{{
pool_model t
}}}
pool٠close t
{{{
RET ();
pool_finished t
}}}.
Lemma pool٠run𑁒spec (Ψ : val → val → iProp Σ) sz task :
(0 ≤ sz)%Z →
{{{
∀ t ctx scope,
pool_inv t ₊sz -∗
pool_context t ctx scope -∗
WP task ctx {{ v,
pool_context t ctx scope ∗
Ψ t v
}}
}}}
pool٠run #sz task
{{{
t v
, RET v;
pool_finished t ∗
Ψ t v
}}}.
Lemma pool٠size𑁒spec t sz ctx scope :
{{{
pool_inv t sz ∗
pool_context t ctx scope
}}}
pool٠size ctx
{{{
RET #sz;
pool_context t ctx scope
}}}.
Lemma pool٠async𑁒spec P Q t ctx scope task :
{{{
pool_context t ctx scope ∗
( ∀ ctx scope,
pool_context t ctx scope -∗
WP task ctx {{ res,
pool_context t ctx scope ∗
▷ P ∗
▷ □ Q
}}
)
}}}
pool٠async ctx task
{{{
RET ();
pool_context t ctx scope ∗
pool_consumer t P ∗
pool_obligation t Q
}}}.
Lemma pool٠wait𑁒spec P_notification P_pred Q_pred t ctx scope notification pred :
{{{
pool_context t ctx scope ∗
P_notification ∗
( ∀ notify,
P_notification -∗
WP notify () {{ itype_unit }} -∗
WP notification notify {{ res,
⌜res = ()%V⌝ ∗
P_notification
}}
) ∗
P_pred ∗
□ (
P_pred -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q_pred else P_pred
}}
)
}}}
pool٠wait ctx notification pred
{{{
RET ();
pool_context t ctx scope ∗
Q_pred
}}}.
Lemma pool٠wait_ivar𑁒spec `{ivar_G : !Ivar4G Σ} {context_name} t ctx scope ivar Ψ Ξ (Γ : _ → context_name → _) :
{{{
pool_context t ctx scope ∗
ivar_4_inv ivar Ψ Ξ Γ
}}}
pool٠wait_ivar ctx ivar
{{{
RET ();
£ 2 ∗
pool_context t ctx scope ∗
ivar_4_resolved ivar
}}}.
End pool_G.
#[global] Opaque pool_scope.
#[global] Opaque pool_inv.
#[global] Opaque pool_model.
#[global] Opaque pool_context.
#[global] Opaque pool_obligation.
#[global] Opaque pool_consumer.
#[global] Opaque pool_finished.
Section pool_G.
Context `{pool_G : PoolG Σ}.
Implicit Types P Q R : iProp Σ.
#[global] Instance from_assumption_pool_consumer t p P Q :
FromAssumption p P Q →
KnownRFromAssumption p P (pool_consumer t Q).
#[global] Instance from_pure_pool_consumer t a P ϕ :
FromPure a P ϕ →
FromPure a (pool_consumer t P) ϕ.
#[global] Instance into_wand_pool_consumer t p q R P Q :
IntoWand false false R P Q →
IntoWand p q (pool_consumer t R) (pool_consumer t P) (pool_consumer t Q).
#[global] Instance into_wand_pool_consumer_persistent t p q R P Q :
IntoWand false q R P Q →
IntoWand p q (pool_consumer t R) P (pool_consumer t Q).
#[global] Instance into_wand_pool_consumer_args t p q R P Q :
IntoWand p false R P Q →
IntoWand' p q R (pool_consumer t P) (pool_consumer t Q).
#[global] Instance from_sep_pool_consumer t P Q1 Q2 :
FromSep P Q1 Q2 →
FromSep (pool_consumer t P) (pool_consumer t Q1) (pool_consumer t Q2).
#[global] Instance from_or_pool_consumer t P Q1 Q2 :
FromOr P Q1 Q2 →
FromOr (pool_consumer t P) (pool_consumer t Q1) (pool_consumer t Q2).
#[global] Instance from_exist_pool_consumer t {A} P (Φ : A → iProp Σ) :
FromExist P Φ →
FromExist (pool_consumer t P) (λ a, pool_consumer t (Φ a)).
#[global] Instance into_forall_pool_consumer t {A} P (Φ : A → iProp Σ) :
IntoForall P Φ →
IntoForall (pool_consumer t P) (λ a, pool_consumer t (Φ a)).
#[global] Instance from_modal_pool_consumer t P :
FromModal True modality_id (pool_consumer t P) (pool_consumer t P) P.
#[global] Instance elim_modal_pool_consumer t p P Q :
ElimModal True p false (pool_consumer t P) P (pool_consumer t Q) (pool_consumer t Q).
#[global] Instance add_modal_pool_consumer t P Q :
AddModal (pool_consumer t P) P (pool_consumer t Q).
#[global] Instance frame_pool_consumer t p R P Q :
Frame p R P Q →
Frame p R (pool_consumer t P) (pool_consumer t Q)
| 2.
End pool_G.