Library zoo_saturn.spsc_bqueue
From zoo Require Import
prelude.
From zoo.common Require Import
countable
relations
list.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_twins
lib.auth_nat_max
lib.mono_list.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
array.
From zoo_saturn Require Export
base
spsc_bqueue__code.
From zoo_saturn Require Import
spsc_bqueue__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types i front front_cache back back_cache : nat.
Implicit Types l : location.
Implicit Types v w t : val.
Implicit Types vs ws hist : list val.
Variant stability :=
| Stable
| Unstable.
Implicit Types stable : stability.
#[local] Instance stability_inhabited : Inhabited stability :=
populate Stable.
Class SpscBqueueG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] spsc_bqueue_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] spsc_bqueue_G_history_G :: MonoListG Σ val
; #[local] spsc_bqueue_G_stability_G :: TwinsG Σ (leibnizO stability)
; #[local] spsc_bqueue_G_mono_nat_G :: AuthNatMaxG Σ
}.
Definition spsc_bqueue_Σ :=
#[auth_twins_Σ (leibnizO (list val)) suffix
; mono_list_Σ val
; twins_Σ (leibnizO stability)
; auth_nat_max_Σ
].
Lemma subG_spsc_bqueue_Σ Σ `{zoo_G : !ZooG Σ} :
subG spsc_bqueue_Σ Σ →
SpscBqueueG Σ.
Section spsc_bqueue_G.
Context `{spsc_bqueue_G : SpscBqueueG Σ}.
Record metadata :=
{ metadata_capacity : nat
; metadata_data : val
; metadata_inv : namespace
; metadata_model : auth_twins_name
; metadata_history : gname
; metadata_producer : gname
; metadata_back : gname
; metadata_consumer : gname
; metadata_front : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 (auth_twins_G := spsc_bqueue_G_model_G) _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(metadata_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 (auth_twins_G := spsc_bqueue_G_model_G) _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(metadata_model).
#[local] Definition history_auth' γ_history :=
mono_list_auth γ_history (DfracOwn 1).
#[local] Definition history_auth γ :=
history_auth' γ.(metadata_history).
#[local] Definition history_at γ :=
mono_list_at γ.(metadata_history).
#[local] Definition producer₁' γ_producer γ_back γ_model stable back ws : iProp Σ :=
twins_twin1 γ_producer (DfracOwn 1) stable ∗
auth_nat_max_auth γ_back (DfracOwn (1/2)) back ∗
auth_twins_auth _ (auth_twins_G := spsc_bqueue_G_model_G) γ_model ws.
#[local] Definition producer₁ γ :=
producer₁' γ.(metadata_producer) γ.(metadata_back) γ.(metadata_model).
#[local] Instance : CustomIpat "producer₁" :=
" ( Hproducer₁ & Hback_auth₁ & Hmodel_auth ) ".
#[local] Definition producer₂' γ_producer γ_back stable back : iProp Σ :=
twins_twin2 γ_producer stable ∗
auth_nat_max_auth γ_back (DfracOwn (1/2)) back.
#[local] Definition producer₂ γ :=
producer₂' γ.(metadata_producer) γ.(metadata_back).
#[local] Instance : CustomIpat "producer₂" :=
" ( Hproducer₂ & Hback_auth₂ ) ".
#[local] Definition back_lb γ :=
auth_nat_max_lb γ.(metadata_back).
#[local] Definition consumer₁' γ_consumer γ_front stable front : iProp Σ :=
twins_twin1 γ_consumer (DfracOwn 1) stable ∗
auth_nat_max_auth γ_front (DfracOwn (1/2)) front.
#[local] Definition consumer₁ γ :=
consumer₁' γ.(metadata_consumer) γ.(metadata_front).
#[local] Instance : CustomIpat "consumer₁" :=
" ( Hconsumer₁ & Hfront_auth₁ ) ".
#[local] Definition consumer₂' γ_consumer γ_front stable front : iProp Σ :=
twins_twin2 γ_consumer stable ∗
auth_nat_max_auth γ_front (DfracOwn (1/2)) front.
#[local] Definition consumer₂ γ :=
consumer₂' γ.(metadata_consumer) γ.(metadata_front).
#[local] Instance : CustomIpat "consumer₂" :=
" ( Hconsumer₂ & Hfront_auth₂ ) ".
#[local] Definition front_lb γ :=
auth_nat_max_lb γ.(metadata_front).
#[local] Definition inv_inner l γ : iProp Σ :=
∃ cstable front pstable back vs hist,
⌜back = (front + length vs)%nat⌝ ∗
⌜back ≤ front + γ.(metadata_capacity)⌝ ∗
⌜length hist = back⌝ ∗
⌜vs = drop front hist⌝ ∗
l.[front] ↦ #front ∗
consumer₂ γ cstable front ∗
l.[back] ↦ #back ∗
producer₂ γ pstable back ∗
model₂ γ vs ∗
history_auth γ hist ∗
( if cstable then
array_cslice γ.(metadata_data) γ.(metadata_capacity) front (DfracOwn 1) ((λ v, ‘Some( v )%V) <$> take 1 vs)
else
True
) ∗
array_cslice γ.(metadata_data) γ.(metadata_capacity) (S front) (DfracOwn 1) ((λ v, ‘Some( v )%V) <$> drop 1 vs) ∗
( if pstable then
array_cslice γ.(metadata_data) γ.(metadata_capacity) back (DfracOwn 1) (if decide (back = front + γ.(metadata_capacity)) then [] else [§None%V])
else
True
) ∗
array_cslice γ.(metadata_data) γ.(metadata_capacity) (S back) (DfracOwn 1) (replicate (γ.(metadata_capacity) - (back - front) - 1) §None%V).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %cstable{} & %front{} & %pstable{} & %back{} & %vs{} & %hist{} & >%Hback{} & >%Hback{}_le & >%Hhist{}_len & >%Hvs{} & >Hl_front & >Hconsumer₂ & >Hl_back & >Hproducer₂ & >Hmodel₂ & >Hhistory_auth & >Hfront & >Hvs & >Hback & >Hextra ) ".
#[local] Definition inv' l γ : iProp Σ :=
meta l nroot γ ∗
l.[data] ↦□ γ.(metadata_data) ∗
array_inv γ.(metadata_data) γ.(metadata_capacity) ∗
inv γ.(metadata_inv) (inv_inner l γ).
#[local] Instance : CustomIpat "inv'" :=
" ( #Hmeta{_{}} & #Hl_data & #Hdata_inv & #Hinv ) ".
Definition spsc_bqueue_inv t ι cap : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata_inv)⌝ ∗
⌜cap = γ.(metadata_capacity)⌝ ∗
inv' l γ.
#[local] Instance : CustomIpat "inv" :=
" ( %l{} & %γ{} & {%Heq{};->} & -> & -> & (:inv') ) ".
Definition spsc_bqueue_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs ∗
⌜length vs ≤ γ.(metadata_capacity)⌝.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} & %Hvs{} ) ".
Definition spsc_bqueue_producer t ws : iProp Σ :=
∃ l γ front_cache back,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[front_cache] ↦ #front_cache ∗
producer₁ γ Stable back ws ∗
front_lb γ front_cache.
#[local] Instance : CustomIpat "producer" :=
" ( %l{;_} & %γ{;_} & %front_cache & %back & %Heq{} & #Hmeta_{} & Hl_front_cache & Hproducer₁ & #Hfront_lb ) ".
Definition spsc_bqueue_consumer t : iProp Σ :=
∃ l γ front back_cache,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[back_cache] ↦ #back_cache ∗
consumer₁ γ Stable front ∗
back_lb γ back_cache.
#[local] Instance : CustomIpat "consumer" :=
" ( %l{;_} & %γ{;_} & %front & %back_cache & %Heq{} & #Hmeta_{} & Hl_back_cache & Hconsumer₁ & #Hback_lb ) ".
#[global] Instance spsc_bqueue_inv_persistent t ι cap :
Persistent (spsc_bqueue_inv t ι cap).
#[global] Instance spsc_bqueue_model_timeless t vs :
Timeless (spsc_bqueue_model t vs).
#[local] Instance producer₂_timeless γ stable back :
Timeless (producer₂ γ stable back).
#[global] Instance spsc_bqueue_producer_timeless t ws :
Timeless (spsc_bqueue_producer t ws).
#[local] Instance consumer₂_timeless γ stable front :
Timeless (consumer₂ γ stable front).
#[global] Instance spsc_bqueue_consumer_timeless t :
Timeless (spsc_bqueue_consumer t).
#[local] Lemma model_producer_alloc :
⊢ |==>
∃ γ_model γ_producer γ_back,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
producer₁' γ_producer γ_back γ_model Stable 0 [] ∗
producer₂' γ_producer γ_back Stable 0.
#[local] Lemma model_valid γ stable back ws vs :
producer₁ γ stable back ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_push {γ stable back ws vs1 vs2} v :
producer₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
producer₁ γ stable back (vs1 ++ [v]) ∗
model₁ γ (vs1 ++ [v]) ∗
model₂ γ (vs1 ++ [v]).
#[local] Lemma model_pop γ v vs1 vs2 :
model₁ γ (v :: vs1) -∗
model₂ γ vs2 ==∗
model₁ γ vs1 ∗
model₂ γ vs1.
#[local] Lemma history_alloc :
⊢ |==>
∃ γ_history,
history_auth' γ_history [].
#[local] Lemma history_at_get {γ hist} i v :
hist !! i = Some v →
history_auth γ hist ⊢
history_at γ i v.
#[local] Lemma history_agree γ hist i v :
history_auth γ hist -∗
history_at γ i v -∗
⌜hist !! i = Some v⌝.
#[local] Lemma history_update {γ hist} v :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [v]).
#[local] Lemma producer_agree γ stable1 back1 ws stable2 back2 :
producer₁ γ stable1 back1 ws -∗
producer₂ γ stable2 back2 -∗
⌜stable1 = stable2⌝ ∗
⌜back1 = back2⌝.
#[local] Lemma producer_update_stability {γ stable1 back1 ws stable2 back2} stable :
producer₁ γ stable1 back1 ws -∗
producer₂ γ stable2 back2 ==∗
producer₁ γ stable back1 ws ∗
producer₂ γ stable back2.
#[local] Lemma producer_update_back {γ stable1 back1 ws stable2 back2} back :
back1 ≤ back →
producer₁ γ stable1 back1 ws -∗
producer₂ γ stable2 back2 ==∗
producer₁ γ stable1 back ws ∗
producer₂ γ stable2 back.
#[local] Lemma back_lb_get γ stable back :
producer₂ γ stable back ⊢
back_lb γ back.
#[local] Lemma back_lb_valid γ stable back1 back2 :
producer₂ γ stable back1 -∗
back_lb γ back2 -∗
⌜back2 ≤ back1⌝.
#[local] Lemma consumer_alloc :
⊢ |==>
∃ γ_consumer γ_front,
consumer₁' γ_consumer γ_front Stable 0 ∗
consumer₂' γ_consumer γ_front Stable 0.
#[local] Lemma consumer_agree γ stable1 front1 stable2 front2 :
consumer₁ γ stable1 front1 -∗
consumer₂ γ stable2 front2 -∗
⌜stable1 = stable2⌝ ∗
⌜front1 = front2⌝.
#[local] Lemma consumer_update_front {γ stable1 front1 stable2 front2} front :
front1 ≤ front →
consumer₁ γ stable1 front1 -∗
consumer₂ γ stable2 front2 ==∗
consumer₁ γ stable1 front ∗
consumer₂ γ stable2 front.
#[local] Lemma consumer_update_stability {γ stable1 front1 stable2 front2} stable :
consumer₁ γ stable1 front1 -∗
consumer₂ γ stable2 front2 ==∗
consumer₁ γ stable front1 ∗
consumer₂ γ stable front2.
#[local] Lemma front_lb_get γ stable front :
consumer₂ γ stable front ⊢
front_lb γ front.
#[local] Lemma front_lb_valid γ stable front1 front2 :
consumer₂ γ stable front1 -∗
front_lb γ front2 -∗
⌜front2 ≤ front1⌝.
Opaque producer₁'.
Opaque producer₂'.
Opaque consumer₁'.
Opaque consumer₂'.
Lemma spsc_bqueue_model_valid t ι cap vs :
spsc_bqueue_inv t ι cap -∗
spsc_bqueue_model t vs -∗
⌜length vs ≤ cap⌝.
Lemma spsc_bqueue_model_exclusive t vs1 vs2 :
spsc_bqueue_model t vs1 -∗
spsc_bqueue_model t vs2 -∗
False.
Lemma spsc_bqueue_producer_exclusive t ws :
spsc_bqueue_producer t ws -∗
spsc_bqueue_producer t ws -∗
False.
Lemma spsc_bqueue_producer_model t ws vs :
spsc_bqueue_producer t ws -∗
spsc_bqueue_model t vs -∗
⌜vs `suffix_of` ws⌝.
Lemma spsc_bqueue_consumer_exclusive t :
spsc_bqueue_consumer t -∗
spsc_bqueue_consumer t -∗
False.
#[local] Instance hint_array_cslice_nil t cap i dq :
HINT ε₁ ✱ [- ;
array_inv t cap
] ⊫ [id];
array_cslice t cap i dq []
✱ [
emp
].
Lemma spsc_bqueue٠create𑁒spec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
spsc_bqueue٠create #cap
{{{
t
, RET t;
spsc_bqueue_inv t ι ₊cap ∗
spsc_bqueue_model t [] ∗
spsc_bqueue_producer t [] ∗
spsc_bqueue_consumer t
}}}.
Lemma spsc_bqueue٠capacity𑁒spec t ι cap :
{{{
spsc_bqueue_inv t ι cap
}}}
spsc_bqueue٠capacity t
{{{
RET #cap;
True
}}}.
#[local] Lemma front𑁒spec l γ stable front :
{{{
inv' l γ ∗
consumer₁ γ stable front
}}}
(#l).{front}
{{{
RET #front;
consumer₁ γ stable front
}}}.
#[local] Lemma back𑁒spec l γ stable back ws :
{{{
inv' l γ ∗
producer₁ γ stable back ws
}}}
(#l).{back}
{{{
RET #back;
producer₁ γ stable back ws
}}}.
Lemma spsc_bqueue٠size𑁒spec_producer t ι cap ws :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_producer t ws
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠size t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(length vs);
spsc_bqueue_producer t ws
>>>.
Lemma spsc_bqueue٠size𑁒spec_consumer t ι cap :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_consumer t
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠size t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(length vs);
spsc_bqueue_consumer t
>>>.
Lemma spsc_bqueue٠is_empty𑁒spec_producer t ι cap ws :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_producer t ws
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠is_empty t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(bool_decide (vs = []%list));
spsc_bqueue_producer t ws
>>>.
Lemma spsc_bqueue٠is_empty𑁒spec_consumer t ι cap :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_consumer t
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠is_empty t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(bool_decide (vs = []%list));
spsc_bqueue_consumer t
>>>.
#[local] Definition au_push l γ v Ψ : iProp Σ :=
AU <{
∃∃ vs,
spsc_bqueue_model #l vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
∀∀ b,
⌜b = bool_decide (length vs = γ.(metadata_capacity))⌝ ∗
spsc_bqueue_model #l (if b then vs else vs ++ [v]),
COMM
Ψ vs b
}>.
#[local] Lemma spsc_bqueue٠push₀𑁒spec l γ front_cache stable back ws v Ψ :
{{{
inv' l γ ∗
l.[front_cache] ↦ #front_cache ∗
producer₁ γ stable back ws ∗
front_lb γ front_cache ∗
au_push l γ v Ψ
}}}
spsc_bqueue٠push₀ #l γ.(metadata_data) #back
{{{
b front_cache
, RET #b;
⌜b = bool_decide (back < front_cache + γ.(metadata_capacity))⌝ ∗
l.[front_cache] ↦ #front_cache ∗
producer₁ γ stable back ws ∗
front_lb γ front_cache ∗
if b then
au_push l γ v Ψ
else
∃ vs,
⌜length vs = γ.(metadata_capacity)⌝ ∗
Ψ vs true
}}}.
Lemma spsc_bqueue٠push𑁒spec t ι cap ws v :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_producer t ws
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs = cap)⌝ ∗
spsc_bqueue_model t (if b then vs else vs ++ [v])
| RET #b;
spsc_bqueue_producer t (if b then ws else vs ++ [v])
>>>.
#[local] Definition au_pop l γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
spsc_bqueue_model #l vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
spsc_bqueue_model #l (tail vs),
COMM
spsc_bqueue_consumer #l -∗
Ψ (head vs : val)
}>.
#[local] Lemma spsc_bqueue٠pop₀𑁒spec l γ back_cache stable front Ψ :
{{{
inv' l γ ∗
l.[back_cache] ↦ #back_cache ∗
consumer₁ γ stable front ∗
back_lb γ back_cache ∗
au_pop l γ Ψ
}}}
spsc_bqueue٠pop₀ #l #front
{{{
b back_cache
, RET #b;
⌜b = bool_decide (front < back_cache)⌝ ∗
l.[back_cache] ↦ #back_cache ∗
consumer₁ γ stable front ∗
back_lb γ back_cache ∗
if b then
au_pop l γ Ψ
else
spsc_bqueue_consumer #l -∗
Ψ None
}}}.
Lemma spsc_bqueue٠pop𑁒spec t ι cap :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_consumer t
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠pop t @ ↑ι
<<<
spsc_bqueue_model t (tail vs)
| RET head vs;
spsc_bqueue_consumer t
>>>.
End spsc_bqueue_G.
From zoo_saturn Require
spsc_bqueue__opaque.
#[global] Opaque spsc_bqueue_inv.
#[global] Opaque spsc_bqueue_model.
#[global] Opaque spsc_bqueue_producer.
#[global] Opaque spsc_bqueue_consumer.
prelude.
From zoo.common Require Import
countable
relations
list.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_twins
lib.auth_nat_max
lib.mono_list.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
array.
From zoo_saturn Require Export
base
spsc_bqueue__code.
From zoo_saturn Require Import
spsc_bqueue__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types i front front_cache back back_cache : nat.
Implicit Types l : location.
Implicit Types v w t : val.
Implicit Types vs ws hist : list val.
Variant stability :=
| Stable
| Unstable.
Implicit Types stable : stability.
#[local] Instance stability_inhabited : Inhabited stability :=
populate Stable.
Class SpscBqueueG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] spsc_bqueue_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] spsc_bqueue_G_history_G :: MonoListG Σ val
; #[local] spsc_bqueue_G_stability_G :: TwinsG Σ (leibnizO stability)
; #[local] spsc_bqueue_G_mono_nat_G :: AuthNatMaxG Σ
}.
Definition spsc_bqueue_Σ :=
#[auth_twins_Σ (leibnizO (list val)) suffix
; mono_list_Σ val
; twins_Σ (leibnizO stability)
; auth_nat_max_Σ
].
Lemma subG_spsc_bqueue_Σ Σ `{zoo_G : !ZooG Σ} :
subG spsc_bqueue_Σ Σ →
SpscBqueueG Σ.
Section spsc_bqueue_G.
Context `{spsc_bqueue_G : SpscBqueueG Σ}.
Record metadata :=
{ metadata_capacity : nat
; metadata_data : val
; metadata_inv : namespace
; metadata_model : auth_twins_name
; metadata_history : gname
; metadata_producer : gname
; metadata_back : gname
; metadata_consumer : gname
; metadata_front : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 (auth_twins_G := spsc_bqueue_G_model_G) _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(metadata_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 (auth_twins_G := spsc_bqueue_G_model_G) _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(metadata_model).
#[local] Definition history_auth' γ_history :=
mono_list_auth γ_history (DfracOwn 1).
#[local] Definition history_auth γ :=
history_auth' γ.(metadata_history).
#[local] Definition history_at γ :=
mono_list_at γ.(metadata_history).
#[local] Definition producer₁' γ_producer γ_back γ_model stable back ws : iProp Σ :=
twins_twin1 γ_producer (DfracOwn 1) stable ∗
auth_nat_max_auth γ_back (DfracOwn (1/2)) back ∗
auth_twins_auth _ (auth_twins_G := spsc_bqueue_G_model_G) γ_model ws.
#[local] Definition producer₁ γ :=
producer₁' γ.(metadata_producer) γ.(metadata_back) γ.(metadata_model).
#[local] Instance : CustomIpat "producer₁" :=
" ( Hproducer₁ & Hback_auth₁ & Hmodel_auth ) ".
#[local] Definition producer₂' γ_producer γ_back stable back : iProp Σ :=
twins_twin2 γ_producer stable ∗
auth_nat_max_auth γ_back (DfracOwn (1/2)) back.
#[local] Definition producer₂ γ :=
producer₂' γ.(metadata_producer) γ.(metadata_back).
#[local] Instance : CustomIpat "producer₂" :=
" ( Hproducer₂ & Hback_auth₂ ) ".
#[local] Definition back_lb γ :=
auth_nat_max_lb γ.(metadata_back).
#[local] Definition consumer₁' γ_consumer γ_front stable front : iProp Σ :=
twins_twin1 γ_consumer (DfracOwn 1) stable ∗
auth_nat_max_auth γ_front (DfracOwn (1/2)) front.
#[local] Definition consumer₁ γ :=
consumer₁' γ.(metadata_consumer) γ.(metadata_front).
#[local] Instance : CustomIpat "consumer₁" :=
" ( Hconsumer₁ & Hfront_auth₁ ) ".
#[local] Definition consumer₂' γ_consumer γ_front stable front : iProp Σ :=
twins_twin2 γ_consumer stable ∗
auth_nat_max_auth γ_front (DfracOwn (1/2)) front.
#[local] Definition consumer₂ γ :=
consumer₂' γ.(metadata_consumer) γ.(metadata_front).
#[local] Instance : CustomIpat "consumer₂" :=
" ( Hconsumer₂ & Hfront_auth₂ ) ".
#[local] Definition front_lb γ :=
auth_nat_max_lb γ.(metadata_front).
#[local] Definition inv_inner l γ : iProp Σ :=
∃ cstable front pstable back vs hist,
⌜back = (front + length vs)%nat⌝ ∗
⌜back ≤ front + γ.(metadata_capacity)⌝ ∗
⌜length hist = back⌝ ∗
⌜vs = drop front hist⌝ ∗
l.[front] ↦ #front ∗
consumer₂ γ cstable front ∗
l.[back] ↦ #back ∗
producer₂ γ pstable back ∗
model₂ γ vs ∗
history_auth γ hist ∗
( if cstable then
array_cslice γ.(metadata_data) γ.(metadata_capacity) front (DfracOwn 1) ((λ v, ‘Some( v )%V) <$> take 1 vs)
else
True
) ∗
array_cslice γ.(metadata_data) γ.(metadata_capacity) (S front) (DfracOwn 1) ((λ v, ‘Some( v )%V) <$> drop 1 vs) ∗
( if pstable then
array_cslice γ.(metadata_data) γ.(metadata_capacity) back (DfracOwn 1) (if decide (back = front + γ.(metadata_capacity)) then [] else [§None%V])
else
True
) ∗
array_cslice γ.(metadata_data) γ.(metadata_capacity) (S back) (DfracOwn 1) (replicate (γ.(metadata_capacity) - (back - front) - 1) §None%V).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %cstable{} & %front{} & %pstable{} & %back{} & %vs{} & %hist{} & >%Hback{} & >%Hback{}_le & >%Hhist{}_len & >%Hvs{} & >Hl_front & >Hconsumer₂ & >Hl_back & >Hproducer₂ & >Hmodel₂ & >Hhistory_auth & >Hfront & >Hvs & >Hback & >Hextra ) ".
#[local] Definition inv' l γ : iProp Σ :=
meta l nroot γ ∗
l.[data] ↦□ γ.(metadata_data) ∗
array_inv γ.(metadata_data) γ.(metadata_capacity) ∗
inv γ.(metadata_inv) (inv_inner l γ).
#[local] Instance : CustomIpat "inv'" :=
" ( #Hmeta{_{}} & #Hl_data & #Hdata_inv & #Hinv ) ".
Definition spsc_bqueue_inv t ι cap : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata_inv)⌝ ∗
⌜cap = γ.(metadata_capacity)⌝ ∗
inv' l γ.
#[local] Instance : CustomIpat "inv" :=
" ( %l{} & %γ{} & {%Heq{};->} & -> & -> & (:inv') ) ".
Definition spsc_bqueue_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs ∗
⌜length vs ≤ γ.(metadata_capacity)⌝.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} & %Hvs{} ) ".
Definition spsc_bqueue_producer t ws : iProp Σ :=
∃ l γ front_cache back,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[front_cache] ↦ #front_cache ∗
producer₁ γ Stable back ws ∗
front_lb γ front_cache.
#[local] Instance : CustomIpat "producer" :=
" ( %l{;_} & %γ{;_} & %front_cache & %back & %Heq{} & #Hmeta_{} & Hl_front_cache & Hproducer₁ & #Hfront_lb ) ".
Definition spsc_bqueue_consumer t : iProp Σ :=
∃ l γ front back_cache,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[back_cache] ↦ #back_cache ∗
consumer₁ γ Stable front ∗
back_lb γ back_cache.
#[local] Instance : CustomIpat "consumer" :=
" ( %l{;_} & %γ{;_} & %front & %back_cache & %Heq{} & #Hmeta_{} & Hl_back_cache & Hconsumer₁ & #Hback_lb ) ".
#[global] Instance spsc_bqueue_inv_persistent t ι cap :
Persistent (spsc_bqueue_inv t ι cap).
#[global] Instance spsc_bqueue_model_timeless t vs :
Timeless (spsc_bqueue_model t vs).
#[local] Instance producer₂_timeless γ stable back :
Timeless (producer₂ γ stable back).
#[global] Instance spsc_bqueue_producer_timeless t ws :
Timeless (spsc_bqueue_producer t ws).
#[local] Instance consumer₂_timeless γ stable front :
Timeless (consumer₂ γ stable front).
#[global] Instance spsc_bqueue_consumer_timeless t :
Timeless (spsc_bqueue_consumer t).
#[local] Lemma model_producer_alloc :
⊢ |==>
∃ γ_model γ_producer γ_back,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
producer₁' γ_producer γ_back γ_model Stable 0 [] ∗
producer₂' γ_producer γ_back Stable 0.
#[local] Lemma model_valid γ stable back ws vs :
producer₁ γ stable back ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_push {γ stable back ws vs1 vs2} v :
producer₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
producer₁ γ stable back (vs1 ++ [v]) ∗
model₁ γ (vs1 ++ [v]) ∗
model₂ γ (vs1 ++ [v]).
#[local] Lemma model_pop γ v vs1 vs2 :
model₁ γ (v :: vs1) -∗
model₂ γ vs2 ==∗
model₁ γ vs1 ∗
model₂ γ vs1.
#[local] Lemma history_alloc :
⊢ |==>
∃ γ_history,
history_auth' γ_history [].
#[local] Lemma history_at_get {γ hist} i v :
hist !! i = Some v →
history_auth γ hist ⊢
history_at γ i v.
#[local] Lemma history_agree γ hist i v :
history_auth γ hist -∗
history_at γ i v -∗
⌜hist !! i = Some v⌝.
#[local] Lemma history_update {γ hist} v :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [v]).
#[local] Lemma producer_agree γ stable1 back1 ws stable2 back2 :
producer₁ γ stable1 back1 ws -∗
producer₂ γ stable2 back2 -∗
⌜stable1 = stable2⌝ ∗
⌜back1 = back2⌝.
#[local] Lemma producer_update_stability {γ stable1 back1 ws stable2 back2} stable :
producer₁ γ stable1 back1 ws -∗
producer₂ γ stable2 back2 ==∗
producer₁ γ stable back1 ws ∗
producer₂ γ stable back2.
#[local] Lemma producer_update_back {γ stable1 back1 ws stable2 back2} back :
back1 ≤ back →
producer₁ γ stable1 back1 ws -∗
producer₂ γ stable2 back2 ==∗
producer₁ γ stable1 back ws ∗
producer₂ γ stable2 back.
#[local] Lemma back_lb_get γ stable back :
producer₂ γ stable back ⊢
back_lb γ back.
#[local] Lemma back_lb_valid γ stable back1 back2 :
producer₂ γ stable back1 -∗
back_lb γ back2 -∗
⌜back2 ≤ back1⌝.
#[local] Lemma consumer_alloc :
⊢ |==>
∃ γ_consumer γ_front,
consumer₁' γ_consumer γ_front Stable 0 ∗
consumer₂' γ_consumer γ_front Stable 0.
#[local] Lemma consumer_agree γ stable1 front1 stable2 front2 :
consumer₁ γ stable1 front1 -∗
consumer₂ γ stable2 front2 -∗
⌜stable1 = stable2⌝ ∗
⌜front1 = front2⌝.
#[local] Lemma consumer_update_front {γ stable1 front1 stable2 front2} front :
front1 ≤ front →
consumer₁ γ stable1 front1 -∗
consumer₂ γ stable2 front2 ==∗
consumer₁ γ stable1 front ∗
consumer₂ γ stable2 front.
#[local] Lemma consumer_update_stability {γ stable1 front1 stable2 front2} stable :
consumer₁ γ stable1 front1 -∗
consumer₂ γ stable2 front2 ==∗
consumer₁ γ stable front1 ∗
consumer₂ γ stable front2.
#[local] Lemma front_lb_get γ stable front :
consumer₂ γ stable front ⊢
front_lb γ front.
#[local] Lemma front_lb_valid γ stable front1 front2 :
consumer₂ γ stable front1 -∗
front_lb γ front2 -∗
⌜front2 ≤ front1⌝.
Opaque producer₁'.
Opaque producer₂'.
Opaque consumer₁'.
Opaque consumer₂'.
Lemma spsc_bqueue_model_valid t ι cap vs :
spsc_bqueue_inv t ι cap -∗
spsc_bqueue_model t vs -∗
⌜length vs ≤ cap⌝.
Lemma spsc_bqueue_model_exclusive t vs1 vs2 :
spsc_bqueue_model t vs1 -∗
spsc_bqueue_model t vs2 -∗
False.
Lemma spsc_bqueue_producer_exclusive t ws :
spsc_bqueue_producer t ws -∗
spsc_bqueue_producer t ws -∗
False.
Lemma spsc_bqueue_producer_model t ws vs :
spsc_bqueue_producer t ws -∗
spsc_bqueue_model t vs -∗
⌜vs `suffix_of` ws⌝.
Lemma spsc_bqueue_consumer_exclusive t :
spsc_bqueue_consumer t -∗
spsc_bqueue_consumer t -∗
False.
#[local] Instance hint_array_cslice_nil t cap i dq :
HINT ε₁ ✱ [- ;
array_inv t cap
] ⊫ [id];
array_cslice t cap i dq []
✱ [
emp
].
Lemma spsc_bqueue٠create𑁒spec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
spsc_bqueue٠create #cap
{{{
t
, RET t;
spsc_bqueue_inv t ι ₊cap ∗
spsc_bqueue_model t [] ∗
spsc_bqueue_producer t [] ∗
spsc_bqueue_consumer t
}}}.
Lemma spsc_bqueue٠capacity𑁒spec t ι cap :
{{{
spsc_bqueue_inv t ι cap
}}}
spsc_bqueue٠capacity t
{{{
RET #cap;
True
}}}.
#[local] Lemma front𑁒spec l γ stable front :
{{{
inv' l γ ∗
consumer₁ γ stable front
}}}
(#l).{front}
{{{
RET #front;
consumer₁ γ stable front
}}}.
#[local] Lemma back𑁒spec l γ stable back ws :
{{{
inv' l γ ∗
producer₁ γ stable back ws
}}}
(#l).{back}
{{{
RET #back;
producer₁ γ stable back ws
}}}.
Lemma spsc_bqueue٠size𑁒spec_producer t ι cap ws :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_producer t ws
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠size t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(length vs);
spsc_bqueue_producer t ws
>>>.
Lemma spsc_bqueue٠size𑁒spec_consumer t ι cap :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_consumer t
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠size t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(length vs);
spsc_bqueue_consumer t
>>>.
Lemma spsc_bqueue٠is_empty𑁒spec_producer t ι cap ws :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_producer t ws
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠is_empty t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(bool_decide (vs = []%list));
spsc_bqueue_producer t ws
>>>.
Lemma spsc_bqueue٠is_empty𑁒spec_consumer t ι cap :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_consumer t
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠is_empty t @ ↑ι
<<<
spsc_bqueue_model t vs
| RET #(bool_decide (vs = []%list));
spsc_bqueue_consumer t
>>>.
#[local] Definition au_push l γ v Ψ : iProp Σ :=
AU <{
∃∃ vs,
spsc_bqueue_model #l vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
∀∀ b,
⌜b = bool_decide (length vs = γ.(metadata_capacity))⌝ ∗
spsc_bqueue_model #l (if b then vs else vs ++ [v]),
COMM
Ψ vs b
}>.
#[local] Lemma spsc_bqueue٠push₀𑁒spec l γ front_cache stable back ws v Ψ :
{{{
inv' l γ ∗
l.[front_cache] ↦ #front_cache ∗
producer₁ γ stable back ws ∗
front_lb γ front_cache ∗
au_push l γ v Ψ
}}}
spsc_bqueue٠push₀ #l γ.(metadata_data) #back
{{{
b front_cache
, RET #b;
⌜b = bool_decide (back < front_cache + γ.(metadata_capacity))⌝ ∗
l.[front_cache] ↦ #front_cache ∗
producer₁ γ stable back ws ∗
front_lb γ front_cache ∗
if b then
au_push l γ v Ψ
else
∃ vs,
⌜length vs = γ.(metadata_capacity)⌝ ∗
Ψ vs true
}}}.
Lemma spsc_bqueue٠push𑁒spec t ι cap ws v :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_producer t ws
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs = cap)⌝ ∗
spsc_bqueue_model t (if b then vs else vs ++ [v])
| RET #b;
spsc_bqueue_producer t (if b then ws else vs ++ [v])
>>>.
#[local] Definition au_pop l γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
spsc_bqueue_model #l vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
spsc_bqueue_model #l (tail vs),
COMM
spsc_bqueue_consumer #l -∗
Ψ (head vs : val)
}>.
#[local] Lemma spsc_bqueue٠pop₀𑁒spec l γ back_cache stable front Ψ :
{{{
inv' l γ ∗
l.[back_cache] ↦ #back_cache ∗
consumer₁ γ stable front ∗
back_lb γ back_cache ∗
au_pop l γ Ψ
}}}
spsc_bqueue٠pop₀ #l #front
{{{
b back_cache
, RET #b;
⌜b = bool_decide (front < back_cache)⌝ ∗
l.[back_cache] ↦ #back_cache ∗
consumer₁ γ stable front ∗
back_lb γ back_cache ∗
if b then
au_pop l γ Ψ
else
spsc_bqueue_consumer #l -∗
Ψ None
}}}.
Lemma spsc_bqueue٠pop𑁒spec t ι cap :
<<<
spsc_bqueue_inv t ι cap ∗
spsc_bqueue_consumer t
| ∀∀ vs,
spsc_bqueue_model t vs
>>>
spsc_bqueue٠pop t @ ↑ι
<<<
spsc_bqueue_model t (tail vs)
| RET head vs;
spsc_bqueue_consumer t
>>>.
End spsc_bqueue_G.
From zoo_saturn Require
spsc_bqueue__opaque.
#[global] Opaque spsc_bqueue_inv.
#[global] Opaque spsc_bqueue_model.
#[global] Opaque spsc_bqueue_producer.
#[global] Opaque spsc_bqueue_consumer.