Library zoo_parabs.ws_hub_fifo
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.excl
lib.ghost_list.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option.
From zoo_saturn Require Import
mpmc_queue_1.
From zoo_parabs Require Export
base
ws_hub_fifo__code.
From zoo_parabs Require Import
ws_hub_fifo__types
waiters.
From zoo Require Import
options.
Implicit Types b closed : bool.
Implicit Types num_active : Z.
Implicit Types 𝑡 : location.
Implicit Types v t notification notify pred : val.
Implicit Types ws : list val.
Implicit Types vs : gmultiset val.
Implicit Types status : status.
Implicit Types empty : emptiness.
Implicit Types emptys : list emptiness.
Class WsHubFifoG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_hub_fifo_G_queue_G :: MpmcQueue1G Σ
; #[local] ws_hub_fifo_G_waiters_G :: WaitersG Σ
; #[local] ws_hub_fifo_G_owner_G :: ExclG Σ unitO
; #[local] ws_hub_fifo_G_emptiness_G :: GhostListG Σ emptiness
}.
Definition ws_hub_fifo_Σ :=
#[mpmc_queue_1_Σ
; waiters_Σ
; excl_Σ unitO
; ghost_list_Σ emptiness
].
#[global] Instance subG_ws_hub_fifo_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_hub_fifo_Σ Σ →
WsHubFifoG Σ.
#[local] Definition consistent vs ws :=
vs = list_to_set_disj ws.
#[local] Lemma consistent_nil_inv vs :
consistent vs [] →
vs = ∅.
#[local] Lemma consistent_push {vs ws} v :
consistent vs ws →
consistent ({[+v+]} ⊎ vs) (ws ++ [v]).
#[local] Lemma consistent_pop vs v ws :
consistent vs (v :: ws) →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' ws.
Opaque consistent.
Section ws_hub_fifo_G.
Context `{ws_hub_fifo_G : WsHubFifoG Σ}.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Record metadata :=
{ metadata_size : nat
; metadata_queue : val
; metadata_waiters : val
; metadata_owners : list gname
; metadata_emptiness : gname
}.
Implicit Types γ : metadata.
Implicit Types γ_owners : list gname.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition owner' γ_owners sz i : iProp Σ :=
∃ γ_owner,
⌜γ_owners !! i = Some γ_owner⌝ ∗
⌜length γ_owners = sz⌝ ∗
excl γ_owner ().
#[local] Definition owner γ i :=
owner' γ.(metadata_owners) γ.(metadata_size) i.
#[local] Instance : CustomIpat "owner_" :=
" ( %γ_owner{} & %Hlookup{} & %Hlength{_{}} & Howner{} ) ".
#[local] Definition emptiness_auth' γ_emptiness sz vs : iProp Σ :=
∃ emptys,
ghost_list_auth γ_emptiness emptys ∗
⌜length emptys = sz⌝ ∗
⌜ vs = ∅
∨ ∃ 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_fifo_inv t ι (sz : nat) : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
⌜sz = γ.(metadata_size)⌝ ∗
meta 𝑡 nroot γ ∗
𝑡.[size] ↦□ #γ.(metadata_size) ∗
𝑡.[queue] ↦□ γ.(metadata_queue) ∗
𝑡.[waiters] ↦□ γ.(metadata_waiters) ∗
mpmc_queue_1_inv γ.(metadata_queue) ι ∗
waiters_inv γ.(metadata_waiters) sz ∗
inv nroot (inv_inner 𝑡).
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & -> & #Hmeta{} & #H𝑡{}_size & #H𝑡{}_queue & #H𝑡{}_waiters & #Hqueue{}_inv & #Hwaiters{}_inv & #Hinv{} ) ".
Definition ws_hub_fifo_model t vs : iProp Σ :=
∃ 𝑡 γ ws,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
mpmc_queue_1_model γ.(metadata_queue) ws ∗
⌜consistent vs ws⌝ ∗
emptiness_auth γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l_ & %γ_ & %ws & %Heq & Hmeta_ & Hqueue_model & %Hconsistent & Hemptiness_auth ) ".
Definition ws_hub_fifo_owner t i status empty : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
owner γ i ∗
emptiness_at γ i empty.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} & Hemptiness_at{_{}} ) ".
#[global] Instance ws_hub_fifo_model_timeless t vs :
Timeless (ws_hub_fifo_model t vs).
#[global] Instance ws_hub_fifo_inv_persistent t ι sz :
Persistent (ws_hub_fifo_inv t ι sz).
#[local] Lemma owner_alloc sz :
⊢ |==>
∃ γ_owners,
[∗ list] i ∈ seq 0 sz,
owner' γ_owners sz i.
#[local] Lemma owner_valid γ i :
owner γ i ⊢
⌜i < γ.(metadata_size)⌝.
#[local] Lemma owner_exclusive γ i :
owner γ i -∗
owner γ i -∗
False.
Opaque owner'.
#[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 i empty :
emptiness_auth γ vs -∗
emptiness_at γ i empty -∗
⌜i < γ.(metadata_size)⌝.
#[local] Lemma emptiness_empty γ vs :
emptiness_auth γ vs -∗
( [∗ list] i ∈ seq 0 γ.(metadata_size),
emptiness_at γ i Empty
) -∗
⌜vs = ∅⌝.
#[local] Lemma emptiness_update_auth γ v vs :
emptiness_auth γ ({[+v+]} ⊎ vs) ⊢
emptiness_auth γ vs.
#[local] Lemma emptiness_update_Nonempty {γ vs i empty} vs' :
emptiness_auth γ vs -∗
emptiness_at γ i empty ==∗
emptiness_auth γ vs' ∗
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_fifo_inv_agree t ι sz1 sz2 :
ws_hub_fifo_inv t ι sz1 -∗
ws_hub_fifo_inv t ι sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_hub_fifo_owner_exclusive t i status1 empty1 status2 empty2 :
ws_hub_fifo_owner t i status1 empty1 -∗
ws_hub_fifo_owner t i status2 empty2 -∗
False.
Lemma ws_hub_fifo_inv_owner t ι sz i status empty :
ws_hub_fifo_inv t ι sz -∗
ws_hub_fifo_owner t i status empty -∗
⌜i < sz⌝.
Lemma ws_hub_fifo_model_empty t ι sz vs :
ws_hub_fifo_inv t ι sz -∗
ws_hub_fifo_model t vs -∗
( [∗ list] i ∈ seq 0 sz,
∃ status,
ws_hub_fifo_owner t i status Empty
) -∗
⌜vs = ∅⌝.
Lemma ws_hub_fifo٠create𑁒spec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_hub_fifo٠create #sz
{{{
t
, RET t;
ws_hub_fifo_inv t ι ₊sz ∗
ws_hub_fifo_model t ∅ ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_hub_fifo_owner t i Nonblocked Empty
}}}.
Lemma ws_hub_fifo٠size𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠size t
{{{
RET #sz;
True
}}}.
#[local] Lemma ws_hub_fifo٠begin_inactive𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠begin_inactive t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_fifo٠end_inactive𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠end_inactive t
{{{
RET ();
True
}}}.
Lemma ws_hub_fifo٠block𑁒spec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
}}}
ws_hub_fifo٠block t #i
{{{
RET ();
ws_hub_fifo_owner t i_ Blocked empty
}}}.
Lemma ws_hub_fifo٠unblock𑁒spec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Blocked empty
}}}
ws_hub_fifo٠unblock t #i
{{{
RET ();
ws_hub_fifo_owner t i_ Nonblocked empty
}}}.
Lemma ws_hub_fifo٠closed𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠closed t
{{{
closed
, RET #closed;
True
}}}.
#[local] Lemma ws_hub_fifo٠notify𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠notify t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_fifo٠notify_all𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠notify_all t
{{{
RET ();
True
}}}.
Lemma ws_hub_fifo٠push𑁒spec t ι sz i i_ empty v :
i = ⁺i_ →
<<<
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠push t #i v @ ↑ι
<<<
ws_hub_fifo_model t ({[+v+]} ⊎ vs)
| RET ();
ws_hub_fifo_owner t i_ Nonblocked Nonempty
>>>.
#[local] Lemma ws_hub_fifo٠pop'𑁒spec_aux (owner : option (nat × emptiness)) t ι sz :
<<<
ws_hub_fifo_inv t ι sz ∗
match owner with
| None ⇒
True
| Some (i, empty) ⇒
ws_hub_fifo_owner t i Nonblocked empty
end
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop' t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
match owner with
| None ⇒
True
| Some (i, empty) ⇒
ws_hub_fifo_owner t i Nonblocked (if o then empty else Empty)
end
>>>.
#[local] Lemma ws_hub_fifo٠pop'𑁒spec t ι sz :
<<<
ws_hub_fifo_inv t ι sz
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop' t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
True
>>>.
#[local] Lemma ws_hub_fifo٠pop'𑁒spec_owner t ι sz i empty :
<<<
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop' t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i Nonblocked (if o then empty else Empty)
>>>.
Lemma ws_hub_fifo٠pop𑁒spec t ι sz i i_ empty :
i = ⁺i_ →
<<<
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop t #i @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i_ Nonblocked (if o then empty else Empty)
>>>.
#[local] Lemma ws_hub_fifo٠steal_aux𑁒spec P_notification P_pred Q_pred t ι (sz : nat) i notification pred :
(0 ≤ i < sz)%Z →
<<<
ws_hub_fifo_inv t ι sz ∗
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_fifo_model t vs
>>>
ws_hub_fifo٠steal_aux t #i notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_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_fifo_model t vs
>>>
ws_hub_fifo٠steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i_ (if o then Nonblocked else Blocked) empty
>>>.
Lemma ws_hub_fifo٠close𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠close t
{{{
RET ();
True
}}}.
End ws_hub_fifo_G.
#[global] Opaque ws_hub_fifo_inv.
#[global] Opaque ws_hub_fifo_model.
#[global] Opaque ws_hub_fifo_owner.
Section ws_hub_fifo_G.
Context `{ws_hub_fifo_G : WsHubFifoG Σ}.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_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_fifo_model t vs
>>>
ws_hub_fifo٠pop_steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| empty,
RET o;
ws_hub_fifo_owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop_steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| empty,
RET o;
ws_hub_fifo_owner t i_ (if o then Nonblocked else Blocked) empty ∗
if o then
True
else
⌜empty = Empty⌝
>>>.
End ws_hub_fifo_G.
From zoo_parabs Require
ws_hub_fifo__opaque.
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.excl
lib.ghost_list.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option.
From zoo_saturn Require Import
mpmc_queue_1.
From zoo_parabs Require Export
base
ws_hub_fifo__code.
From zoo_parabs Require Import
ws_hub_fifo__types
waiters.
From zoo Require Import
options.
Implicit Types b closed : bool.
Implicit Types num_active : Z.
Implicit Types 𝑡 : location.
Implicit Types v t notification notify pred : val.
Implicit Types ws : list val.
Implicit Types vs : gmultiset val.
Implicit Types status : status.
Implicit Types empty : emptiness.
Implicit Types emptys : list emptiness.
Class WsHubFifoG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_hub_fifo_G_queue_G :: MpmcQueue1G Σ
; #[local] ws_hub_fifo_G_waiters_G :: WaitersG Σ
; #[local] ws_hub_fifo_G_owner_G :: ExclG Σ unitO
; #[local] ws_hub_fifo_G_emptiness_G :: GhostListG Σ emptiness
}.
Definition ws_hub_fifo_Σ :=
#[mpmc_queue_1_Σ
; waiters_Σ
; excl_Σ unitO
; ghost_list_Σ emptiness
].
#[global] Instance subG_ws_hub_fifo_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_hub_fifo_Σ Σ →
WsHubFifoG Σ.
#[local] Definition consistent vs ws :=
vs = list_to_set_disj ws.
#[local] Lemma consistent_nil_inv vs :
consistent vs [] →
vs = ∅.
#[local] Lemma consistent_push {vs ws} v :
consistent vs ws →
consistent ({[+v+]} ⊎ vs) (ws ++ [v]).
#[local] Lemma consistent_pop vs v ws :
consistent vs (v :: ws) →
∃ vs',
vs = {[+v+]} ⊎ vs' ∧
consistent vs' ws.
Opaque consistent.
Section ws_hub_fifo_G.
Context `{ws_hub_fifo_G : WsHubFifoG Σ}.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Record metadata :=
{ metadata_size : nat
; metadata_queue : val
; metadata_waiters : val
; metadata_owners : list gname
; metadata_emptiness : gname
}.
Implicit Types γ : metadata.
Implicit Types γ_owners : list gname.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition owner' γ_owners sz i : iProp Σ :=
∃ γ_owner,
⌜γ_owners !! i = Some γ_owner⌝ ∗
⌜length γ_owners = sz⌝ ∗
excl γ_owner ().
#[local] Definition owner γ i :=
owner' γ.(metadata_owners) γ.(metadata_size) i.
#[local] Instance : CustomIpat "owner_" :=
" ( %γ_owner{} & %Hlookup{} & %Hlength{_{}} & Howner{} ) ".
#[local] Definition emptiness_auth' γ_emptiness sz vs : iProp Σ :=
∃ emptys,
ghost_list_auth γ_emptiness emptys ∗
⌜length emptys = sz⌝ ∗
⌜ vs = ∅
∨ ∃ 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_fifo_inv t ι (sz : nat) : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
⌜sz = γ.(metadata_size)⌝ ∗
meta 𝑡 nroot γ ∗
𝑡.[size] ↦□ #γ.(metadata_size) ∗
𝑡.[queue] ↦□ γ.(metadata_queue) ∗
𝑡.[waiters] ↦□ γ.(metadata_waiters) ∗
mpmc_queue_1_inv γ.(metadata_queue) ι ∗
waiters_inv γ.(metadata_waiters) sz ∗
inv nroot (inv_inner 𝑡).
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & -> & #Hmeta{} & #H𝑡{}_size & #H𝑡{}_queue & #H𝑡{}_waiters & #Hqueue{}_inv & #Hwaiters{}_inv & #Hinv{} ) ".
Definition ws_hub_fifo_model t vs : iProp Σ :=
∃ 𝑡 γ ws,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
mpmc_queue_1_model γ.(metadata_queue) ws ∗
⌜consistent vs ws⌝ ∗
emptiness_auth γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l_ & %γ_ & %ws & %Heq & Hmeta_ & Hqueue_model & %Hconsistent & Hemptiness_auth ) ".
Definition ws_hub_fifo_owner t i status empty : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
owner γ i ∗
emptiness_at γ i empty.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} & Hemptiness_at{_{}} ) ".
#[global] Instance ws_hub_fifo_model_timeless t vs :
Timeless (ws_hub_fifo_model t vs).
#[global] Instance ws_hub_fifo_inv_persistent t ι sz :
Persistent (ws_hub_fifo_inv t ι sz).
#[local] Lemma owner_alloc sz :
⊢ |==>
∃ γ_owners,
[∗ list] i ∈ seq 0 sz,
owner' γ_owners sz i.
#[local] Lemma owner_valid γ i :
owner γ i ⊢
⌜i < γ.(metadata_size)⌝.
#[local] Lemma owner_exclusive γ i :
owner γ i -∗
owner γ i -∗
False.
Opaque owner'.
#[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 i empty :
emptiness_auth γ vs -∗
emptiness_at γ i empty -∗
⌜i < γ.(metadata_size)⌝.
#[local] Lemma emptiness_empty γ vs :
emptiness_auth γ vs -∗
( [∗ list] i ∈ seq 0 γ.(metadata_size),
emptiness_at γ i Empty
) -∗
⌜vs = ∅⌝.
#[local] Lemma emptiness_update_auth γ v vs :
emptiness_auth γ ({[+v+]} ⊎ vs) ⊢
emptiness_auth γ vs.
#[local] Lemma emptiness_update_Nonempty {γ vs i empty} vs' :
emptiness_auth γ vs -∗
emptiness_at γ i empty ==∗
emptiness_auth γ vs' ∗
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_fifo_inv_agree t ι sz1 sz2 :
ws_hub_fifo_inv t ι sz1 -∗
ws_hub_fifo_inv t ι sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_hub_fifo_owner_exclusive t i status1 empty1 status2 empty2 :
ws_hub_fifo_owner t i status1 empty1 -∗
ws_hub_fifo_owner t i status2 empty2 -∗
False.
Lemma ws_hub_fifo_inv_owner t ι sz i status empty :
ws_hub_fifo_inv t ι sz -∗
ws_hub_fifo_owner t i status empty -∗
⌜i < sz⌝.
Lemma ws_hub_fifo_model_empty t ι sz vs :
ws_hub_fifo_inv t ι sz -∗
ws_hub_fifo_model t vs -∗
( [∗ list] i ∈ seq 0 sz,
∃ status,
ws_hub_fifo_owner t i status Empty
) -∗
⌜vs = ∅⌝.
Lemma ws_hub_fifo٠create𑁒spec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_hub_fifo٠create #sz
{{{
t
, RET t;
ws_hub_fifo_inv t ι ₊sz ∗
ws_hub_fifo_model t ∅ ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_hub_fifo_owner t i Nonblocked Empty
}}}.
Lemma ws_hub_fifo٠size𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠size t
{{{
RET #sz;
True
}}}.
#[local] Lemma ws_hub_fifo٠begin_inactive𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠begin_inactive t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_fifo٠end_inactive𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠end_inactive t
{{{
RET ();
True
}}}.
Lemma ws_hub_fifo٠block𑁒spec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
}}}
ws_hub_fifo٠block t #i
{{{
RET ();
ws_hub_fifo_owner t i_ Blocked empty
}}}.
Lemma ws_hub_fifo٠unblock𑁒spec t ι sz i i_ empty :
i = ⁺i_ →
{{{
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Blocked empty
}}}
ws_hub_fifo٠unblock t #i
{{{
RET ();
ws_hub_fifo_owner t i_ Nonblocked empty
}}}.
Lemma ws_hub_fifo٠closed𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠closed t
{{{
closed
, RET #closed;
True
}}}.
#[local] Lemma ws_hub_fifo٠notify𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠notify t
{{{
RET ();
True
}}}.
#[local] Lemma ws_hub_fifo٠notify_all𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠notify_all t
{{{
RET ();
True
}}}.
Lemma ws_hub_fifo٠push𑁒spec t ι sz i i_ empty v :
i = ⁺i_ →
<<<
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠push t #i v @ ↑ι
<<<
ws_hub_fifo_model t ({[+v+]} ⊎ vs)
| RET ();
ws_hub_fifo_owner t i_ Nonblocked Nonempty
>>>.
#[local] Lemma ws_hub_fifo٠pop'𑁒spec_aux (owner : option (nat × emptiness)) t ι sz :
<<<
ws_hub_fifo_inv t ι sz ∗
match owner with
| None ⇒
True
| Some (i, empty) ⇒
ws_hub_fifo_owner t i Nonblocked empty
end
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop' t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
match owner with
| None ⇒
True
| Some (i, empty) ⇒
ws_hub_fifo_owner t i Nonblocked (if o then empty else Empty)
end
>>>.
#[local] Lemma ws_hub_fifo٠pop'𑁒spec t ι sz :
<<<
ws_hub_fifo_inv t ι sz
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop' t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
True
>>>.
#[local] Lemma ws_hub_fifo٠pop'𑁒spec_owner t ι sz i empty :
<<<
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop' t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i Nonblocked (if o then empty else Empty)
>>>.
Lemma ws_hub_fifo٠pop𑁒spec t ι sz i i_ empty :
i = ⁺i_ →
<<<
ws_hub_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop t #i @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i_ Nonblocked (if o then empty else Empty)
>>>.
#[local] Lemma ws_hub_fifo٠steal_aux𑁒spec P_notification P_pred Q_pred t ι (sz : nat) i notification pred :
(0 ≤ i < sz)%Z →
<<<
ws_hub_fifo_inv t ι sz ∗
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_fifo_model t vs
>>>
ws_hub_fifo٠steal_aux t #i notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_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_fifo_model t vs
>>>
ws_hub_fifo٠steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| RET o;
ws_hub_fifo_owner t i_ (if o then Nonblocked else Blocked) empty
>>>.
Lemma ws_hub_fifo٠close𑁒spec t ι sz :
{{{
ws_hub_fifo_inv t ι sz
}}}
ws_hub_fifo٠close t
{{{
RET ();
True
}}}.
End ws_hub_fifo_G.
#[global] Opaque ws_hub_fifo_inv.
#[global] Opaque ws_hub_fifo_model.
#[global] Opaque ws_hub_fifo_owner.
Section ws_hub_fifo_G.
Context `{ws_hub_fifo_G : WsHubFifoG Σ}.
Implicit Types P P_notification P_pred Q Q_pred : iProp Σ.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_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_fifo_model t vs
>>>
ws_hub_fifo٠pop_steal_until t #i #max_round_noyield #max_round_yield notification pred @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| empty,
RET o;
ws_hub_fifo_owner t i_ Nonblocked empty ∗
P_notification ∗
if o then P_pred else Q_pred
>>>.
Lemma ws_hub_fifo٠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_fifo_inv t ι sz ∗
ws_hub_fifo_owner t i_ Nonblocked empty
| ∀∀ vs,
ws_hub_fifo_model t vs
>>>
ws_hub_fifo٠pop_steal t #i #max_round_noyield #max_round_yield @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_hub_fifo_model t vs
| Some v ⇒
∃ vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
ws_hub_fifo_model t vs'
end
| empty,
RET o;
ws_hub_fifo_owner t i_ (if o then Nonblocked else Blocked) empty ∗
if o then
True
else
⌜empty = Empty⌝
>>>.
End ws_hub_fifo_G.
From zoo_parabs Require
ws_hub_fifo__opaque.