Library zoo_parabs.ws_hub_hybrid
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_hub_hybrid__code.
Require Import zoo_parabs.ws_hub_hybrid__types.
Require Import zoo.options.
Implicit Type b yield closed : bool.
Implicit Type num_active : Z.
Implicit Type 𝑡 : location.
Implicit Type v t notification notify pred : val.
Implicit Type vs : gmultiset val.
Implicit Type ws us vs_queue : list val.
Implicit Type vss : list $ list val.
Implicit Type status : status.
Implicit Type empty : emptiness.
Class WsHubHybridG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_hub_hybrid۰G۰deques۰G :: WsBdequesPublicG Σ
; #[local] ws_hub_hybrid۰G۰queue۰G :: QueueMpmc1G Σ
; #[local] ws_hub_hybrid۰G۰waiters۰G :: WaitersG Σ
; #[local] ws_hub_hybrid۰G۰emptiness۰G :: GhostListG Σ emptiness
}.
Definition ws_hub_hybrid۰Σ :=
#[ws_bdeques_public۰Σ
; queue_mpmc_1۰Σ
; waiters۰Σ
; ghost_list۰Σ emptiness
].
#[global] Instance subGｰws_hub_hybrid۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_hub_hybrid۰Σ Σ →
WsHubHybridG Σ.
Section consistent.
#[local] Definition consistent vs vss vs_queue :=
vs =
⋃+ (list_to_set_disj <$> vss) ⊎
list_to_set_disj vs_queue.
#[local] Lemma consistentｰalloc sz :
consistent ∅ (replicate sz []) [].
#[local] Lemma consistentｰempty vs vss vs_queue :
consistent vs vss vs_queue →
vs = ∅ ↔
( ∀ i us,
vss !! i = Some us →
us = []
) ∧
vs_queue = [].
#[local] Lemma consistentｰdequeｰpush {vs vss vs_queue i us} v :
vss !! i = Some us →
consistent vs vss vs_queue →
consistent ({[+v+]} ⊎ vs) (<[i := us ++ [v]]> vss) vs_queue.
#[local] Lemma consistentｰdequeｰremove {vs vss vs_queue i us} us1 v us2 :
vss !! i = Some us →
us = us1 ++ v :: us2 →
consistent vs vss vs_queue →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' (<[i := us1 ++ us2]> vss) vs_queue.
#[local] Lemma consistentｰdequeｰpop vs vss vs_queue i us v :
vss !! i = Some (us ++ [v]) →
consistent vs vss vs_queue →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' (<[i := us]> vss) vs_queue.
#[local] Lemma consistentｰdequeｰsteal vs vss vs_queue i v us :
vss !! i = Some (v :: us) →
consistent vs vss vs_queue →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' (<[i := us]> vss) vs_queue.
#[local] Lemma consistentｰqueueｰpush {vs vss vs_queue} v :
consistent vs vss vs_queue →
consistent ({[+v+]} ⊎ vs) vss (vs_queue ++ [v]).
#[local] Lemma consistentｰqueueｰpop vs vss v vs_queue :
consistent vs vss (v :: vs_queue) →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' vss vs_queue.
End consistent.
Opaque consistent.
Section ws_hub_hybrid۰G.
Context `{ws_hub_hybrid۰G : WsHubHybridG Σ}.
Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.
Record metadata :=
{ metadata۰size : nat
; metadata۰deques : val
; metadata۰rounds : val
; metadata۰queue : val
; metadata۰waiters : val
; metadata۰emptiness : gname
}.
Implicit Type γ : metadata.
#[local] Instance metadataｰeq_dec :
EqDecision metadata.
#[local] Instance metadataｰcountable :
Countable metadata.
#[local] Definition emptiness۰auth' γ_emptiness sz vs_queue : iProp Σ :=
∃ emptys,
ghost_list۰auth γ_emptiness emptys ∗
⌜length emptys = sz⌝ ∗
⌜ vs_queue = []
∨ ∃ i,
emptys !! i = Some Nonempty
⌝.
#[local] Definition emptiness۰auth γ :=
emptiness۰auth' γ.(metadata۰emptiness) γ.(metadata۰size).
#[local] Instance : CustomIpat "emptiness۰auth" :=
" ( %emptys & Hauth & %Hemptys & %Hemptiness ) ".
#[local] Definition emptiness۰at' γ_emptiness i :=
ghost_list۰at γ_emptiness i (DfracOwn 1).
#[local] Definition emptiness۰at γ :=
emptiness۰at' γ.(metadata۰emptiness).
#[local] Definition inv۰inner 𝑡 : iProp Σ :=
∃ num_active,
𝑡.[num_active] ↦ #num_active.
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %num_active & H𝑡_num_active ) ".
Definition ws_hub_hybrid۰inv t ι sz : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
⌜sz = γ.(metadata۰size)⌝ ∗
𝑡.[deques] ↦□ γ.(metadata۰deques) ∗
𝑡.[rounds] ↦□ γ.(metadata۰rounds) ∗
𝑡.[queue] ↦□ γ.(metadata۰queue) ∗
𝑡.[waiters] ↦□ γ.(metadata۰waiters) ∗
ws_bdeques_public۰inv γ.(metadata۰deques) ι γ.(metadata۰size) ∗
array۰inv γ.(metadata۰rounds) γ.(metadata۰size) ∗
queue_mpmc_1۰inv γ.(metadata۰queue) ι ∗
waiters۰inv γ.(metadata۰waiters) sz ∗
inv nroot (inv۰inner 𝑡).
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{} & -> & #H𝑡{}_deques & #H𝑡{}_queue & #H𝑡{}_rounds & #H𝑡{}_waiters & #Hdeques{}_inv & #Hrounds{}_inv & #Hqueue{}_inv & #Hwaiters{}_inv & #Hinv{} ) ".
Definition ws_hub_hybrid۰model t vs : iProp Σ :=
∃ 𝑡 γ vss vs_queue,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
ws_bdeques_public۰model γ.(metadata۰deques) vss ∗
queue_mpmc_1۰model γ.(metadata۰queue) vs_queue ∗
⌜consistent vs vss vs_queue⌝ ∗
emptiness۰auth γ vs_queue.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡_ & %γ_ & %vss & %vs_queue & %Heq & Hmeta_ & Hdeques_model & Hqueue_model & %Hconsistent & Hemptiness_auth ) ".
Definition ws_hub_hybrid۰owner t i status empty : iProp Σ :=
∃ 𝑡 γ ws round n,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
ws_bdeques_public۰owner γ.(metadata۰deques) i status ws ∗
⌜empty = Empty → ws = []⌝ ∗
array۰slice γ.(metadata۰rounds) i DfracDiscarded [round] ∗
random_round۰model' round (γ.(metadata۰size) - 1) n ∗
emptiness۰at γ i empty.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{;_} & %γ{;_} & %ws{} & %round{} & %n{} & %Heq{} & Hmeta{;_} & Hdeques_owner{} & %Hempty{} & #Hrounds{} & Hround{} & Hemptiness_at{_{}} ) ".
#[global] Instance ws_hub_hybrid۰modelｰtimeless t vs :
Timeless (ws_hub_hybrid۰model t vs).
#[global] Instance ws_hub_hybrid۰invｰpersistent t ι sz :
Persistent (ws_hub_hybrid۰inv t ι sz).
#[local] Lemma emptinessｰalloc sz :
⊢ |==>
∃ γ_emptiness,
emptiness۰auth' γ_emptiness sz [] ∗
[∗ list] i ∈ seq 0 sz,
emptiness۰at' γ_emptiness i Empty.
#[local] Lemma emptiness۰atｰvalid γ vs_queue i empty :
emptiness۰auth γ vs_queue -∗
emptiness۰at γ i empty -∗
⌜i < γ.(metadata۰size)⌝.
#[local] Lemma emptinessｰempty γ vs_queue :
emptiness۰auth γ vs_queue -∗
( [∗ list] i ∈ seq 0 γ.(metadata۰size),
emptiness۰at γ i Empty
) -∗
⌜vs_queue = []⌝.
#[local] Lemma emptinessｰupdateｰauth γ v vs_queue :
emptiness۰auth γ (v :: vs_queue) ⊢
emptiness۰auth γ vs_queue.
#[local] Lemma emptinessｰupdateｰNonempty {γ vs_queue i empty} vs_queue' :
emptiness۰auth γ vs_queue -∗
emptiness۰at γ i empty ==∗
emptiness۰auth γ vs_queue' ∗
emptiness۰at γ i Nonempty.
#[local] Lemma emptinessｰupdateｰEmpty γ i empty :
emptiness۰auth γ [] -∗
emptiness۰at γ i empty ==∗
emptiness۰auth γ [] ∗
emptiness۰at γ i Empty.
Opaque emptiness۰auth'.
Lemma ws_hub_hybrid۰invｰagree t ι sz1 sz2 :
ws_hub_hybrid۰inv t ι sz1 -∗
ws_hub_hybrid۰inv t ι sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_hub_hybrid۰ownerｰexclusive t i status1 empty1 status2 empty2 :
ws_hub_hybrid۰owner t i status1 empty1 -∗
ws_hub_hybrid۰owner t i status2 empty2 -∗
False.
Lemma ws_hub_hybrid۰invｰowner t ι sz i status empty :
ws_hub_hybrid۰inv t ι sz -∗
ws_hub_hybrid۰owner t i status empty -∗
⌜i < sz⌝.
Lemma ws_hub_hybrid۰modelｰempty t ι sz vs :
ws_hub_hybrid۰inv t ι sz -∗
ws_hub_hybrid۰model t vs -∗
( [∗ list] i ∈ seq 0 sz,
∃ status,
ws_hub_hybrid۰owner t i status Empty
) -∗
⌜vs = ∅⌝.
Lemma ws_hub_hybrid٠createｰspec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_hub_hybrid٠create #sz
{{{
t
, RET t;
ws_hub_hybrid۰inv t ι ₊sz ∗
ws_hub_hybrid۰model t ∅ ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_hub_hybrid۰owner t i Nonblocked Empty
}}}.
Lemma ws_hub_hybrid٠sizeｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠size t
{{{
RET #sz;
True
}}}.
#[local] Lemma ws_hub_hybrid٠begin_inactiveｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠begin_inactive t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_hybrid٠end_inactiveｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠end_inactive t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_hybrid٠block_activeｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}
ws_hub_hybrid٠block_active t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Blocked empty
}}}.
#[local] Lemma ws_hub_hybrid٠unblock_activeｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty
}}}
ws_hub_hybrid٠unblock_active t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}.
Lemma ws_hub_hybrid٠blockｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}
ws_hub_hybrid٠block t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Blocked empty
}}}.
Lemma ws_hub_hybrid٠unblockｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty
}}}
ws_hub_hybrid٠unblock t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}.
Lemma ws_hub_hybrid٠closedｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠closed t
{{{
closed
, RET #closed;
True
}}}.
#[local] Lemma ws_hub_hybrid٠notifyｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠notify t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_hybrid٠notify_allｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠notify_all t
{{{
RET ();
True
}}}.
Lemma ws_hub_hybrid٠pushｰspec t ι sz i i_ empty v :
i = ⁺i_ →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠push t #i v @ ↑ι
<<<
ws_hub_hybrid۰model t ({[+v+]} ⊎ vs)
| RET ();
ws_hub_hybrid۰owner t i_ Nonblocked Nonempty
>>>.
Lemma ws_hub_hybrid٠popｰspec t ι sz i i_ empty :
i = ⁺i_ →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠pop t #i @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Nonblocked (if o then empty else Empty)
>>>.
#[local] Lemma ws_hub_hybrid٠try_steal_onceｰspec t ι sz i i_ empty :
i = ⁺i_ →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠try_steal_once t #i @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Blocked empty
>>>.
#[local] Lemma ws_hub_hybrid٠try_steal₁ｰspec P Q t ι sz i i_ empty yield max_round pred :
i = ⁺i_ →
(0 ≤ max_round)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty ∗
P ∗
□ (
P -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q else P
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠try_steal₁ t #i #yield #max_round pred @ ↑ι
<<<
∃∃ o,
match o with
| Nothing
| Anything ⇒
ws_hub_hybrid۰model t vs
| Something v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Blocked empty ∗
if o is Anything then Q else P
>>>.
#[local] Lemma ws_hub_hybrid٠try_stealｰspec P Q t ι sz i i_ empty max_round_noyield max_round_yield pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty ∗
P ∗
□ (
P -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q else P
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠try_steal t #i #max_round_noyield #max_round_yield pred @ ↑ι
<<<
∃∃ o,
match o with
| Nothing
| Anything ⇒
ws_hub_hybrid۰model t vs
| Something v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Blocked empty ∗
if o is Anything then Q else P
>>>.
#[local] Lemma ws_hub_hybrid٠steal_auxｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty ∗
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
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠steal_aux t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ (if o then Nonblocked else Blocked) empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_hybrid٠steal_untilｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
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
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_hybrid٠stealｰspec t ι sz i i_ empty max_round_noyield max_round_yield :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ (if o then Nonblocked else Blocked) empty
>>>.
Lemma ws_hub_hybrid٠closeｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠close t
{{{
RET ();
True
}}}.
End ws_hub_hybrid۰G.
#[global] Opaque ws_hub_hybrid۰inv.
#[global] Opaque ws_hub_hybrid۰model.
#[global] Opaque ws_hub_hybrid۰owner.
Section ws_hub_hybrid۰G.
Context `{ws_hub_hybrid۰G : WsHubHybridG Σ}.
Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.
Lemma ws_hub_hybrid٠pop_steal_untilｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
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
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠pop_steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| empty,
RET o;
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_hybrid٠pop_stealｰspec t ι sz i i_ empty max_round_noyield max_round_yield :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠pop_steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| empty,
RET o;
ws_hub_hybrid۰owner t i_ (if o then Nonblocked else Blocked) empty ∗
if o then
True
else
⌜empty = Empty⌝
>>>.
End ws_hub_hybrid۰G.
Require zoo_parabs.ws_hub_hybrid__opaque.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_hub_hybrid__code.
Require Import zoo_parabs.ws_hub_hybrid__types.
Require Import zoo.options.
Implicit Type b yield closed : bool.
Implicit Type num_active : Z.
Implicit Type 𝑡 : location.
Implicit Type v t notification notify pred : val.
Implicit Type vs : gmultiset val.
Implicit Type ws us vs_queue : list val.
Implicit Type vss : list $ list val.
Implicit Type status : status.
Implicit Type empty : emptiness.
Class WsHubHybridG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_hub_hybrid۰G۰deques۰G :: WsBdequesPublicG Σ
; #[local] ws_hub_hybrid۰G۰queue۰G :: QueueMpmc1G Σ
; #[local] ws_hub_hybrid۰G۰waiters۰G :: WaitersG Σ
; #[local] ws_hub_hybrid۰G۰emptiness۰G :: GhostListG Σ emptiness
}.
Definition ws_hub_hybrid۰Σ :=
#[ws_bdeques_public۰Σ
; queue_mpmc_1۰Σ
; waiters۰Σ
; ghost_list۰Σ emptiness
].
#[global] Instance subGｰws_hub_hybrid۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_hub_hybrid۰Σ Σ →
WsHubHybridG Σ.
Section consistent.
#[local] Definition consistent vs vss vs_queue :=
vs =
⋃+ (list_to_set_disj <$> vss) ⊎
list_to_set_disj vs_queue.
#[local] Lemma consistentｰalloc sz :
consistent ∅ (replicate sz []) [].
#[local] Lemma consistentｰempty vs vss vs_queue :
consistent vs vss vs_queue →
vs = ∅ ↔
( ∀ i us,
vss !! i = Some us →
us = []
) ∧
vs_queue = [].
#[local] Lemma consistentｰdequeｰpush {vs vss vs_queue i us} v :
vss !! i = Some us →
consistent vs vss vs_queue →
consistent ({[+v+]} ⊎ vs) (<[i := us ++ [v]]> vss) vs_queue.
#[local] Lemma consistentｰdequeｰremove {vs vss vs_queue i us} us1 v us2 :
vss !! i = Some us →
us = us1 ++ v :: us2 →
consistent vs vss vs_queue →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' (<[i := us1 ++ us2]> vss) vs_queue.
#[local] Lemma consistentｰdequeｰpop vs vss vs_queue i us v :
vss !! i = Some (us ++ [v]) →
consistent vs vss vs_queue →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' (<[i := us]> vss) vs_queue.
#[local] Lemma consistentｰdequeｰsteal vs vss vs_queue i v us :
vss !! i = Some (v :: us) →
consistent vs vss vs_queue →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' (<[i := us]> vss) vs_queue.
#[local] Lemma consistentｰqueueｰpush {vs vss vs_queue} v :
consistent vs vss vs_queue →
consistent ({[+v+]} ⊎ vs) vss (vs_queue ++ [v]).
#[local] Lemma consistentｰqueueｰpop vs vss v vs_queue :
consistent vs vss (v :: vs_queue) →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' vss vs_queue.
End consistent.
Opaque consistent.
Section ws_hub_hybrid۰G.
Context `{ws_hub_hybrid۰G : WsHubHybridG Σ}.
Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.
Record metadata :=
{ metadata۰size : nat
; metadata۰deques : val
; metadata۰rounds : val
; metadata۰queue : val
; metadata۰waiters : val
; metadata۰emptiness : gname
}.
Implicit Type γ : metadata.
#[local] Instance metadataｰeq_dec :
EqDecision metadata.
#[local] Instance metadataｰcountable :
Countable metadata.
#[local] Definition emptiness۰auth' γ_emptiness sz vs_queue : iProp Σ :=
∃ emptys,
ghost_list۰auth γ_emptiness emptys ∗
⌜length emptys = sz⌝ ∗
⌜ vs_queue = []
∨ ∃ i,
emptys !! i = Some Nonempty
⌝.
#[local] Definition emptiness۰auth γ :=
emptiness۰auth' γ.(metadata۰emptiness) γ.(metadata۰size).
#[local] Instance : CustomIpat "emptiness۰auth" :=
" ( %emptys & Hauth & %Hemptys & %Hemptiness ) ".
#[local] Definition emptiness۰at' γ_emptiness i :=
ghost_list۰at γ_emptiness i (DfracOwn 1).
#[local] Definition emptiness۰at γ :=
emptiness۰at' γ.(metadata۰emptiness).
#[local] Definition inv۰inner 𝑡 : iProp Σ :=
∃ num_active,
𝑡.[num_active] ↦ #num_active.
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %num_active & H𝑡_num_active ) ".
Definition ws_hub_hybrid۰inv t ι sz : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
⌜sz = γ.(metadata۰size)⌝ ∗
𝑡.[deques] ↦□ γ.(metadata۰deques) ∗
𝑡.[rounds] ↦□ γ.(metadata۰rounds) ∗
𝑡.[queue] ↦□ γ.(metadata۰queue) ∗
𝑡.[waiters] ↦□ γ.(metadata۰waiters) ∗
ws_bdeques_public۰inv γ.(metadata۰deques) ι γ.(metadata۰size) ∗
array۰inv γ.(metadata۰rounds) γ.(metadata۰size) ∗
queue_mpmc_1۰inv γ.(metadata۰queue) ι ∗
waiters۰inv γ.(metadata۰waiters) sz ∗
inv nroot (inv۰inner 𝑡).
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{} & -> & #H𝑡{}_deques & #H𝑡{}_queue & #H𝑡{}_rounds & #H𝑡{}_waiters & #Hdeques{}_inv & #Hrounds{}_inv & #Hqueue{}_inv & #Hwaiters{}_inv & #Hinv{} ) ".
Definition ws_hub_hybrid۰model t vs : iProp Σ :=
∃ 𝑡 γ vss vs_queue,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
ws_bdeques_public۰model γ.(metadata۰deques) vss ∗
queue_mpmc_1۰model γ.(metadata۰queue) vs_queue ∗
⌜consistent vs vss vs_queue⌝ ∗
emptiness۰auth γ vs_queue.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡_ & %γ_ & %vss & %vs_queue & %Heq & Hmeta_ & Hdeques_model & Hqueue_model & %Hconsistent & Hemptiness_auth ) ".
Definition ws_hub_hybrid۰owner t i status empty : iProp Σ :=
∃ 𝑡 γ ws round n,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
ws_bdeques_public۰owner γ.(metadata۰deques) i status ws ∗
⌜empty = Empty → ws = []⌝ ∗
array۰slice γ.(metadata۰rounds) i DfracDiscarded [round] ∗
random_round۰model' round (γ.(metadata۰size) - 1) n ∗
emptiness۰at γ i empty.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{;_} & %γ{;_} & %ws{} & %round{} & %n{} & %Heq{} & Hmeta{;_} & Hdeques_owner{} & %Hempty{} & #Hrounds{} & Hround{} & Hemptiness_at{_{}} ) ".
#[global] Instance ws_hub_hybrid۰modelｰtimeless t vs :
Timeless (ws_hub_hybrid۰model t vs).
#[global] Instance ws_hub_hybrid۰invｰpersistent t ι sz :
Persistent (ws_hub_hybrid۰inv t ι sz).
#[local] Lemma emptinessｰalloc sz :
⊢ |==>
∃ γ_emptiness,
emptiness۰auth' γ_emptiness sz [] ∗
[∗ list] i ∈ seq 0 sz,
emptiness۰at' γ_emptiness i Empty.
#[local] Lemma emptiness۰atｰvalid γ vs_queue i empty :
emptiness۰auth γ vs_queue -∗
emptiness۰at γ i empty -∗
⌜i < γ.(metadata۰size)⌝.
#[local] Lemma emptinessｰempty γ vs_queue :
emptiness۰auth γ vs_queue -∗
( [∗ list] i ∈ seq 0 γ.(metadata۰size),
emptiness۰at γ i Empty
) -∗
⌜vs_queue = []⌝.
#[local] Lemma emptinessｰupdateｰauth γ v vs_queue :
emptiness۰auth γ (v :: vs_queue) ⊢
emptiness۰auth γ vs_queue.
#[local] Lemma emptinessｰupdateｰNonempty {γ vs_queue i empty} vs_queue' :
emptiness۰auth γ vs_queue -∗
emptiness۰at γ i empty ==∗
emptiness۰auth γ vs_queue' ∗
emptiness۰at γ i Nonempty.
#[local] Lemma emptinessｰupdateｰEmpty γ i empty :
emptiness۰auth γ [] -∗
emptiness۰at γ i empty ==∗
emptiness۰auth γ [] ∗
emptiness۰at γ i Empty.
Opaque emptiness۰auth'.
Lemma ws_hub_hybrid۰invｰagree t ι sz1 sz2 :
ws_hub_hybrid۰inv t ι sz1 -∗
ws_hub_hybrid۰inv t ι sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_hub_hybrid۰ownerｰexclusive t i status1 empty1 status2 empty2 :
ws_hub_hybrid۰owner t i status1 empty1 -∗
ws_hub_hybrid۰owner t i status2 empty2 -∗
False.
Lemma ws_hub_hybrid۰invｰowner t ι sz i status empty :
ws_hub_hybrid۰inv t ι sz -∗
ws_hub_hybrid۰owner t i status empty -∗
⌜i < sz⌝.
Lemma ws_hub_hybrid۰modelｰempty t ι sz vs :
ws_hub_hybrid۰inv t ι sz -∗
ws_hub_hybrid۰model t vs -∗
( [∗ list] i ∈ seq 0 sz,
∃ status,
ws_hub_hybrid۰owner t i status Empty
) -∗
⌜vs = ∅⌝.
Lemma ws_hub_hybrid٠createｰspec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_hub_hybrid٠create #sz
{{{
t
, RET t;
ws_hub_hybrid۰inv t ι ₊sz ∗
ws_hub_hybrid۰model t ∅ ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_hub_hybrid۰owner t i Nonblocked Empty
}}}.
Lemma ws_hub_hybrid٠sizeｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠size t
{{{
RET #sz;
True
}}}.
#[local] Lemma ws_hub_hybrid٠begin_inactiveｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠begin_inactive t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_hybrid٠end_inactiveｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠end_inactive t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_hybrid٠block_activeｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}
ws_hub_hybrid٠block_active t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Blocked empty
}}}.
#[local] Lemma ws_hub_hybrid٠unblock_activeｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty
}}}
ws_hub_hybrid٠unblock_active t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}.
Lemma ws_hub_hybrid٠blockｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}
ws_hub_hybrid٠block t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Blocked empty
}}}.
Lemma ws_hub_hybrid٠unblockｰspec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty
}}}
ws_hub_hybrid٠unblock t #i
{{{
RET ();
ws_hub_hybrid۰owner t i_ Nonblocked empty
}}}.
Lemma ws_hub_hybrid٠closedｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠closed t
{{{
closed
, RET #closed;
True
}}}.
#[local] Lemma ws_hub_hybrid٠notifyｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠notify t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_hybrid٠notify_allｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠notify_all t
{{{
RET ();
True
}}}.
Lemma ws_hub_hybrid٠pushｰspec t ι sz i i_ empty v :
i = ⁺i_ →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠push t #i v @ ↑ι
<<<
ws_hub_hybrid۰model t ({[+v+]} ⊎ vs)
| RET ();
ws_hub_hybrid۰owner t i_ Nonblocked Nonempty
>>>.
Lemma ws_hub_hybrid٠popｰspec t ι sz i i_ empty :
i = ⁺i_ →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠pop t #i @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Nonblocked (if o then empty else Empty)
>>>.
#[local] Lemma ws_hub_hybrid٠try_steal_onceｰspec t ι sz i i_ empty :
i = ⁺i_ →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠try_steal_once t #i @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Blocked empty
>>>.
#[local] Lemma ws_hub_hybrid٠try_steal₁ｰspec P Q t ι sz i i_ empty yield max_round pred :
i = ⁺i_ →
(0 ≤ max_round)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty ∗
P ∗
□ (
P -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q else P
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠try_steal₁ t #i #yield #max_round pred @ ↑ι
<<<
∃∃ o,
match o with
| Nothing
| Anything ⇒
ws_hub_hybrid۰model t vs
| Something v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Blocked empty ∗
if o is Anything then Q else P
>>>.
#[local] Lemma ws_hub_hybrid٠try_stealｰspec P Q t ι sz i i_ empty max_round_noyield max_round_yield pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty ∗
P ∗
□ (
P -∗
WP pred () {{ res,
∃ b,
⌜res = #b⌝ ∗
if b then Q else P
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠try_steal t #i #max_round_noyield #max_round_yield pred @ ↑ι
<<<
∃∃ o,
match o with
| Nothing
| Anything ⇒
ws_hub_hybrid۰model t vs
| Something v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Blocked empty ∗
if o is Anything then Q else P
>>>.
#[local] Lemma ws_hub_hybrid٠steal_auxｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Blocked empty ∗
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
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠steal_aux t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ (if o then Nonblocked else Blocked) empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_hybrid٠steal_untilｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
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
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_hybrid٠stealｰspec t ι sz i i_ empty max_round_noyield max_round_yield :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| RET o;
ws_hub_hybrid۰owner t i_ (if o then Nonblocked else Blocked) empty
>>>.
Lemma ws_hub_hybrid٠closeｰspec t ι sz :
{{{
ws_hub_hybrid۰inv t ι sz
}}}
ws_hub_hybrid٠close t
{{{
RET ();
True
}}}.
End ws_hub_hybrid۰G.
#[global] Opaque ws_hub_hybrid۰inv.
#[global] Opaque ws_hub_hybrid۰model.
#[global] Opaque ws_hub_hybrid۰owner.
Section ws_hub_hybrid۰G.
Context `{ws_hub_hybrid۰G : WsHubHybridG Σ}.
Implicit Type P P_notification P_pred Q Q_pred : iProp Σ.
Lemma ws_hub_hybrid٠pop_steal_untilｰspec P_notification P_pred Q_pred t ι sz i i_ empty max_round_noyield max_round_yield notification pred :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
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
}}
)
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠pop_steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| empty,
RET o;
ws_hub_hybrid۰owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_hybrid٠pop_stealｰspec t ι sz i i_ empty max_round_noyield max_round_yield :
i = ⁺i_ →
(0 ≤ max_round_noyield)%Z →
(0 ≤ max_round_yield)%Z →
<<<
ws_hub_hybrid۰inv t ι sz ∗
ws_hub_hybrid۰owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_hybrid۰model t vs
>>>
ws_hub_hybrid٠pop_steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_hybrid۰model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_hybrid۰model t vs'
end
| empty,
RET o;
ws_hub_hybrid۰owner t i_ (if o then Nonblocked else Blocked) empty ∗
if o then
True
else
⌜empty = Empty⌝
>>>.
End ws_hub_hybrid۰G.
Require zoo_parabs.ws_hub_hybrid__opaque.