Library zoo_saturn.spmc_queue
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
relations
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.mono_list
lib.auth_nat_max
lib.auth_twins
lib.saved_pred.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
xtchain
domain.
From zoo_saturn Require Export
base
spmc_queue__code.
From zoo_saturn Require Import
spmc_queue__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front node back new_back : location.
Implicit Types hist past nodes : list location.
Implicit Types v : val.
Implicit Types vs ws : list val.
Implicit Types waiter : gname.
Implicit Types waiters : gmap gname nat.
Class SpmcQueueG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] spmc_queue_G_history_G :: MonoListG Σ location
; #[local] spmc_queue_G_front_G :: AuthNatMaxG Σ
; #[local] spmc_queue_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] spmc_queue_G_waiters_G :: ghost_mapG Σ gname nat
; #[local] spmc_queue_G_saved_pred_G :: SavedPredG Σ bool
}.
Definition spmc_queue_Σ :=
#[mono_list_Σ location
; auth_nat_max_Σ
; auth_twins_Σ (leibnizO (list val)) suffix
; ghost_mapΣ gname nat
; saved_pred_Σ bool
].
#[global] Instance subG_spmc_queue_Σ Σ `{zoo_G : !ZooG Σ} :
subG spmc_queue_Σ Σ →
SpmcQueueG Σ.
Module base.
Section spmc_queue_G.
Context `{spmc_queue_G : SpmcQueueG Σ}.
Implicit Types t : location.
Record metadata :=
{ metadata_inv : namespace
; metadata_history : gname
; metadata_front : gname
; metadata_model : auth_twins_name
; metadata_waiters : gname
}.
Implicit Type γ : metadata.
#[global] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[global] Instance metadata_countable :
Countable metadata.
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn (1/2)) hist.
#[local] Definition history_auth γ hist :=
history_auth' γ.(metadata_history) hist.
#[local] Definition history_last' γ_history node : iProp Σ :=
∃ hist,
mono_list_auth γ_history (DfracOwn (1/2)) hist ∗
⌜last hist = Some node⌝.
#[local] Instance : CustomIpat "history_last" :=
" ( %hist{} & Hauth{_{}} & %Hlast ) ".
#[local] Definition history_last γ :=
history_last' γ.(metadata_history).
#[local] Definition history_at γ i node :=
mono_list_at γ.(metadata_history) i node.
#[local] Definition front_auth' γ_front i :=
auth_nat_max_auth γ_front (DfracOwn 1) i.
#[local] Definition front_auth γ i :=
front_auth' γ.(metadata_front) i.
#[local] Definition front_lb γ i :=
auth_nat_max_lb γ.(metadata_front) i.
#[local] Definition producer' γ_model ws :=
auth_twins_auth _ γ_model ws.
#[local] Definition producer γ :=
producer' γ.(metadata_model).
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(metadata_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(metadata_model).
#[local] Definition waiters_auth' γ_waiters waiters :=
ghost_map_auth γ_waiters 1 waiters.
#[local] Definition waiters_auth γ waiters :=
waiters_auth' γ.(metadata_waiters) waiters.
#[local] Definition waiters_at γ waiter i :=
ghost_map_elem γ.(metadata_waiters) waiter (DfracOwn 1) i.
#[local] Definition node_model γ node i b : iProp Σ :=
node ↦ₕ Header §Node 2 ∗
history_at γ i node ∗
if b then front_lb γ i else True%I.
#[local] Instance : CustomIpat "node_model" :=
" ( #H{}_header & #Hhistory_at_{} & {{front}#Hfront_lb_{};_} ) ".
#[local] Definition waiter_au γ (Ψ : bool → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
model₁ γ vs
, COMM
Ψ (bool_decide (vs = []))
}>.
#[local] Definition waiter_model γ past waiter i : iProp Σ :=
∃ Ψ,
saved_pred waiter Ψ ∗
if decide (i < length past) then
Ψ false
else
waiter_au γ Ψ.
#[local] Definition inv_inner t γ : iProp Σ :=
∃ hist past front nodes vs waiters,
⌜hist = past ++ front :: nodes⌝ ∗
t.[front] ↦ #front ∗
xtchain (Header §Node 2) (DfracOwn 1) hist §Null ∗
([∗ list] node; v ∈ nodes; vs, node.[data] ↦ v) ∗
history_auth γ hist ∗
front_auth γ (length past) ∗
model₂ γ vs ∗
waiters_auth γ waiters ∗
([∗ map] waiter ↦ i ∈ waiters, waiter_model γ past waiter i).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %hist{} & %past{} & %front{} & %nodes{} & %vs{} & %waiters{} & >%Hhist{} & >Ht_front & >Hhist & >Hnodes & >Hhistory_auth & >Hfront_auth & >Hmodel₂ & >Hwaiters_auth & Hwaiters ) ".
#[local] Definition inv' t γ :=
inv γ.(metadata_inv) (inv_inner t γ).
Definition spmc_queue_inv t γ ι : iProp Σ :=
⌜ι = γ.(metadata_inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Hinv ) ".
Definition spmc_queue_producer t γ ws : iProp Σ :=
∃ back,
t.[back] ↦ #back ∗
back ↦ₕ Header §Node 2 ∗
history_last γ back ∗
producer γ ws.
#[local] Instance : CustomIpat "producer" :=
" ( %back{} & Ht_back{_{}} & #Hback{}_header & Hhistory_last{_{}} & Hproducer{_{}} ) ".
Definition spmc_queue_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[global] Instance spmc_queue_model_timeless γ vs :
Timeless (spmc_queue_model γ vs).
#[global] Instance spmc_queue_producer_timeless t γ ws :
Timeless (spmc_queue_producer t γ ws).
#[global] Instance spmc_queue_inv_persistent t γ ι :
Persistent (spmc_queue_inv t γ ι).
#[local] Lemma history_alloc front :
⊢ |==>
∃ γ_history,
history_auth' γ_history [front] ∗
history_last' γ_history front.
#[local] Lemma history_at_get {γ hist} i node :
hist !! i = Some node →
history_auth γ hist ⊢
history_at γ i node.
#[local] Lemma history_at_lookup γ hist i node :
history_auth γ hist -∗
history_at γ i node -∗
⌜hist !! i = Some node⌝.
#[local] Lemma history_auth_last γ hist node :
history_auth γ hist -∗
history_last γ node -∗
⌜last hist = Some node⌝.
#[local] Lemma history_update {γ hist node} node' :
history_auth γ hist -∗
history_last γ node ==∗
history_auth γ (hist ++ [node']) ∗
history_last γ node'.
Opaque history_last'.
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front_auth' γ_front 0.
#[local] Lemma front_lb_get γ i :
front_auth γ i ⊢
front_lb γ i.
#[local] Lemma front_lb_valid γ i1 i2 :
front_auth γ i1 -∗
front_lb γ i2 -∗
⌜i2 ≤ i1⌝.
#[local] Lemma front_update {γ i} i' :
i ≤ i' →
front_auth γ i ⊢ |==>
front_auth γ i'.
#[local] Lemma producer_valid_1 γ ws vs :
producer γ ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma producer_exclusive γ ws1 ws2 :
producer γ ws1 -∗
producer γ ws2 -∗
False.
#[local] Lemma model_producer_alloc :
⊢ |==>
∃ γ_model,
producer' γ_model [] ∗
model₁' γ_model [] ∗
model₂' γ_model [].
#[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 {γ ws vs1 vs2} v :
producer γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
producer γ (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 waiters_alloc :
⊢ |==>
∃ γ_waiters,
waiters_auth' γ_waiters ∅.
#[local] Lemma waiters_insert {γ waiters} i Ψ :
waiters_auth γ waiters ⊢ |==>
∃ waiter,
waiters_auth γ (<[waiter := i]> waiters) ∗
saved_pred waiter Ψ ∗
waiters_at γ waiter i.
#[local] Lemma waiters_delete γ waiters waiter i :
waiters_auth γ waiters -∗
waiters_at γ waiter i ==∗
⌜waiters !! waiter = Some i⌝ ∗
waiters_auth γ (delete waiter waiters).
Lemma spmc_queue_model_exclusive γ vs1 vs2 :
spmc_queue_model γ vs1 -∗
spmc_queue_model γ vs2 -∗
False.
Lemma spmc_queue_producer_valid t γ vs ws :
spmc_queue_producer t γ ws -∗
spmc_queue_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma spmc_queue_producer_exclusive t γ ws1 ws2 :
spmc_queue_producer t γ ws1 -∗
spmc_queue_producer t γ ws2 -∗
False.
Lemma spmc_queue٠create𑁒spec ι :
{{{
True
}}}
spmc_queue٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
spmc_queue_inv t γ ι ∗
spmc_queue_model γ [] ∗
spmc_queue_producer t γ []
}}}.
#[local] Lemma front𑁒spec_strong Ψ t γ :
{{{
inv' t γ ∗
if Ψ is Some Ψ then
waiter_au γ Ψ
else
True
}}}
(#t).{front}
{{{
front i
, RET #front;
node_model γ front i true ∗
if Ψ is Some Ψ then
∃ waiter,
saved_pred waiter Ψ ∗
waiters_at γ waiter i
else
True
}}}.
#[local] Lemma front𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front i
, RET #front;
node_model γ front i true
}}}.
Variant operation :=
| IsEmpty waiter (Ψ : bool → iProp Σ)
| Pop (Ψ : option val → iProp Σ)
| Other.
Implicit Types op : operation.
Variant operation' :=
| IsEmpty'
| Pop'
| Other'.
#[local] Instance operation'_eq_dec : EqDecision operation' :=
ltac:(solve_decision).
#[local] Coercion operation_to_operation' op :=
match op with
| IsEmpty _ _ ⇒
IsEmpty'
| Pop _ ⇒
Pop'
| Other ⇒
Other'
end.
#[local] Definition pop_au γ (Ψ : option val → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
model₁ γ (tail vs)
, COMM
Ψ (head vs)
}>.
#[local] Lemma next𑁒spec_aux op t γ i node :
{{{
inv' t γ ∗
history_at γ i node ∗
( if decide (op = Other' :> operation') then True else
front_lb γ i
) ∗
match op with
| IsEmpty waiter Ψ ⇒
saved_pred waiter Ψ ∗
waiters_at γ waiter i ∗
£ 1
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
match op with
| IsEmpty waiter Ψ ⇒
Ψ true
| Pop Ψ ⇒
Ψ None
| Other ⇒
True
end
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false ∗
match op with
| IsEmpty waiter Ψ ⇒
Ψ false
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
}}}.
#[local] Lemma next𑁒spec t γ i node :
{{{
inv' t γ ∗
history_at γ i node
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false
}}}.
#[local] Lemma next𑁒spec_is_empty {t γ i node} waiter Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
front_lb γ i ∗
saved_pred waiter Ψ ∗
waiters_at γ waiter i ∗
£ 1
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ true
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false ∗
Ψ false
}}}.
#[local] Lemma next𑁒spec_pop {t γ i node} Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
front_lb γ i ∗
pop_au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ None
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false ∗
pop_au γ Ψ
}}}.
Lemma spmc_queue٠is_empty𑁒spec t γ ι :
<<<
spmc_queue_inv t γ ι
| ∀∀ vs,
spmc_queue_model γ vs
>>>
spmc_queue٠is_empty #t @ ↑ι
<<<
spmc_queue_model γ vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma spmc_queue٠push𑁒spec t γ ι ws v :
<<<
spmc_queue_inv t γ ι ∗
spmc_queue_producer t γ ws
| ∀∀ vs,
spmc_queue_model γ vs
>>>
spmc_queue٠push #t v @ ↑ι
<<<
spmc_queue_model γ (vs ++ [v])
| RET ();
spmc_queue_producer t γ (vs ++ [v])
>>>.
#[local] Lemma spmc_queue٠pop𑁒spec_aux t γ :
<<<
inv' t γ
| ∀∀ vs,
model₁ γ vs
>>>
spmc_queue٠pop #t @ ↑γ.(metadata_inv)
<<<
model₁ γ (tail vs)
| RET head vs;
True
>>>.
Lemma spmc_queue٠pop𑁒spec t γ ι :
<<<
spmc_queue_inv t γ ι
| ∀∀ vs,
spmc_queue_model γ vs
>>>
spmc_queue٠pop #t @ ↑ι
<<<
spmc_queue_model γ (tail vs)
| RET head vs;
True
>>>.
End spmc_queue_G.
#[global] Opaque spmc_queue_inv.
#[global] Opaque spmc_queue_producer.
#[global] Opaque spmc_queue_model.
End base.
From zoo_saturn Require
spmc_queue__opaque.
Section spmc_queue_G.
Context `{spmc_queue_G : SpmcQueueG Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition spmc_queue_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.spmc_queue_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition spmc_queue_producer t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.spmc_queue_producer 𝑡 γ ws.
#[local] Instance : CustomIpat "producer" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hproducer{_{}} ) ".
Definition spmc_queue_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.spmc_queue_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance spmc_queue_model_timeless t vs :
Timeless (spmc_queue_model t vs).
#[global] Instance spmc_queue_producer_timeless t ws :
Timeless (spmc_queue_producer t ws).
#[global] Instance spmc_queue_inv_persistent t ι :
Persistent (spmc_queue_inv t ι).
Lemma spmc_queue_model_exclusive t vs1 vs2 :
spmc_queue_model t vs1 -∗
spmc_queue_model t vs2 -∗
False.
Lemma spmc_queue_producer_valid t vs ws :
spmc_queue_producer t ws -∗
spmc_queue_model t vs -∗
⌜vs `suffix_of` ws⌝.
Lemma spmc_queue_producer_exclusive t ws1 ws2 :
spmc_queue_producer t ws1 -∗
spmc_queue_producer t ws2 -∗
False.
Lemma spmc_queue٠create𑁒spec ι :
{{{
True
}}}
spmc_queue٠create ()
{{{
t
, RET t;
spmc_queue_inv t ι ∗
spmc_queue_model t [] ∗
spmc_queue_producer t []
}}}.
Lemma spmc_queue٠is_empty𑁒spec t ι :
<<<
spmc_queue_inv t ι
| ∀∀ vs,
spmc_queue_model t vs
>>>
spmc_queue٠is_empty t @ ↑ι
<<<
spmc_queue_model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma spmc_queue٠push𑁒spec t ι ws v :
<<<
spmc_queue_inv t ι ∗
spmc_queue_producer t ws
| ∀∀ vs,
spmc_queue_model t vs
>>>
spmc_queue٠push t v @ ↑ι
<<<
spmc_queue_model t (vs ++ [v])
| RET ();
spmc_queue_producer t (vs ++ [v])
>>>.
Lemma spmc_queue٠pop𑁒spec t ι :
<<<
spmc_queue_inv t ι
| ∀∀ vs,
spmc_queue_model t vs
>>>
spmc_queue٠pop t @ ↑ι
<<<
spmc_queue_model t (tail vs)
| RET head vs;
True
>>>.
End spmc_queue_G.
#[global] Opaque spmc_queue_inv.
#[global] Opaque spmc_queue_producer.
#[global] Opaque spmc_queue_model.
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
relations
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.mono_list
lib.auth_nat_max
lib.auth_twins
lib.saved_pred.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
xtchain
domain.
From zoo_saturn Require Export
base
spmc_queue__code.
From zoo_saturn Require Import
spmc_queue__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front node back new_back : location.
Implicit Types hist past nodes : list location.
Implicit Types v : val.
Implicit Types vs ws : list val.
Implicit Types waiter : gname.
Implicit Types waiters : gmap gname nat.
Class SpmcQueueG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] spmc_queue_G_history_G :: MonoListG Σ location
; #[local] spmc_queue_G_front_G :: AuthNatMaxG Σ
; #[local] spmc_queue_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] spmc_queue_G_waiters_G :: ghost_mapG Σ gname nat
; #[local] spmc_queue_G_saved_pred_G :: SavedPredG Σ bool
}.
Definition spmc_queue_Σ :=
#[mono_list_Σ location
; auth_nat_max_Σ
; auth_twins_Σ (leibnizO (list val)) suffix
; ghost_mapΣ gname nat
; saved_pred_Σ bool
].
#[global] Instance subG_spmc_queue_Σ Σ `{zoo_G : !ZooG Σ} :
subG spmc_queue_Σ Σ →
SpmcQueueG Σ.
Module base.
Section spmc_queue_G.
Context `{spmc_queue_G : SpmcQueueG Σ}.
Implicit Types t : location.
Record metadata :=
{ metadata_inv : namespace
; metadata_history : gname
; metadata_front : gname
; metadata_model : auth_twins_name
; metadata_waiters : gname
}.
Implicit Type γ : metadata.
#[global] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[global] Instance metadata_countable :
Countable metadata.
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn (1/2)) hist.
#[local] Definition history_auth γ hist :=
history_auth' γ.(metadata_history) hist.
#[local] Definition history_last' γ_history node : iProp Σ :=
∃ hist,
mono_list_auth γ_history (DfracOwn (1/2)) hist ∗
⌜last hist = Some node⌝.
#[local] Instance : CustomIpat "history_last" :=
" ( %hist{} & Hauth{_{}} & %Hlast ) ".
#[local] Definition history_last γ :=
history_last' γ.(metadata_history).
#[local] Definition history_at γ i node :=
mono_list_at γ.(metadata_history) i node.
#[local] Definition front_auth' γ_front i :=
auth_nat_max_auth γ_front (DfracOwn 1) i.
#[local] Definition front_auth γ i :=
front_auth' γ.(metadata_front) i.
#[local] Definition front_lb γ i :=
auth_nat_max_lb γ.(metadata_front) i.
#[local] Definition producer' γ_model ws :=
auth_twins_auth _ γ_model ws.
#[local] Definition producer γ :=
producer' γ.(metadata_model).
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(metadata_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(metadata_model).
#[local] Definition waiters_auth' γ_waiters waiters :=
ghost_map_auth γ_waiters 1 waiters.
#[local] Definition waiters_auth γ waiters :=
waiters_auth' γ.(metadata_waiters) waiters.
#[local] Definition waiters_at γ waiter i :=
ghost_map_elem γ.(metadata_waiters) waiter (DfracOwn 1) i.
#[local] Definition node_model γ node i b : iProp Σ :=
node ↦ₕ Header §Node 2 ∗
history_at γ i node ∗
if b then front_lb γ i else True%I.
#[local] Instance : CustomIpat "node_model" :=
" ( #H{}_header & #Hhistory_at_{} & {{front}#Hfront_lb_{};_} ) ".
#[local] Definition waiter_au γ (Ψ : bool → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
model₁ γ vs
, COMM
Ψ (bool_decide (vs = []))
}>.
#[local] Definition waiter_model γ past waiter i : iProp Σ :=
∃ Ψ,
saved_pred waiter Ψ ∗
if decide (i < length past) then
Ψ false
else
waiter_au γ Ψ.
#[local] Definition inv_inner t γ : iProp Σ :=
∃ hist past front nodes vs waiters,
⌜hist = past ++ front :: nodes⌝ ∗
t.[front] ↦ #front ∗
xtchain (Header §Node 2) (DfracOwn 1) hist §Null ∗
([∗ list] node; v ∈ nodes; vs, node.[data] ↦ v) ∗
history_auth γ hist ∗
front_auth γ (length past) ∗
model₂ γ vs ∗
waiters_auth γ waiters ∗
([∗ map] waiter ↦ i ∈ waiters, waiter_model γ past waiter i).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %hist{} & %past{} & %front{} & %nodes{} & %vs{} & %waiters{} & >%Hhist{} & >Ht_front & >Hhist & >Hnodes & >Hhistory_auth & >Hfront_auth & >Hmodel₂ & >Hwaiters_auth & Hwaiters ) ".
#[local] Definition inv' t γ :=
inv γ.(metadata_inv) (inv_inner t γ).
Definition spmc_queue_inv t γ ι : iProp Σ :=
⌜ι = γ.(metadata_inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Hinv ) ".
Definition spmc_queue_producer t γ ws : iProp Σ :=
∃ back,
t.[back] ↦ #back ∗
back ↦ₕ Header §Node 2 ∗
history_last γ back ∗
producer γ ws.
#[local] Instance : CustomIpat "producer" :=
" ( %back{} & Ht_back{_{}} & #Hback{}_header & Hhistory_last{_{}} & Hproducer{_{}} ) ".
Definition spmc_queue_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[global] Instance spmc_queue_model_timeless γ vs :
Timeless (spmc_queue_model γ vs).
#[global] Instance spmc_queue_producer_timeless t γ ws :
Timeless (spmc_queue_producer t γ ws).
#[global] Instance spmc_queue_inv_persistent t γ ι :
Persistent (spmc_queue_inv t γ ι).
#[local] Lemma history_alloc front :
⊢ |==>
∃ γ_history,
history_auth' γ_history [front] ∗
history_last' γ_history front.
#[local] Lemma history_at_get {γ hist} i node :
hist !! i = Some node →
history_auth γ hist ⊢
history_at γ i node.
#[local] Lemma history_at_lookup γ hist i node :
history_auth γ hist -∗
history_at γ i node -∗
⌜hist !! i = Some node⌝.
#[local] Lemma history_auth_last γ hist node :
history_auth γ hist -∗
history_last γ node -∗
⌜last hist = Some node⌝.
#[local] Lemma history_update {γ hist node} node' :
history_auth γ hist -∗
history_last γ node ==∗
history_auth γ (hist ++ [node']) ∗
history_last γ node'.
Opaque history_last'.
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front_auth' γ_front 0.
#[local] Lemma front_lb_get γ i :
front_auth γ i ⊢
front_lb γ i.
#[local] Lemma front_lb_valid γ i1 i2 :
front_auth γ i1 -∗
front_lb γ i2 -∗
⌜i2 ≤ i1⌝.
#[local] Lemma front_update {γ i} i' :
i ≤ i' →
front_auth γ i ⊢ |==>
front_auth γ i'.
#[local] Lemma producer_valid_1 γ ws vs :
producer γ ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma producer_exclusive γ ws1 ws2 :
producer γ ws1 -∗
producer γ ws2 -∗
False.
#[local] Lemma model_producer_alloc :
⊢ |==>
∃ γ_model,
producer' γ_model [] ∗
model₁' γ_model [] ∗
model₂' γ_model [].
#[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 {γ ws vs1 vs2} v :
producer γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
producer γ (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 waiters_alloc :
⊢ |==>
∃ γ_waiters,
waiters_auth' γ_waiters ∅.
#[local] Lemma waiters_insert {γ waiters} i Ψ :
waiters_auth γ waiters ⊢ |==>
∃ waiter,
waiters_auth γ (<[waiter := i]> waiters) ∗
saved_pred waiter Ψ ∗
waiters_at γ waiter i.
#[local] Lemma waiters_delete γ waiters waiter i :
waiters_auth γ waiters -∗
waiters_at γ waiter i ==∗
⌜waiters !! waiter = Some i⌝ ∗
waiters_auth γ (delete waiter waiters).
Lemma spmc_queue_model_exclusive γ vs1 vs2 :
spmc_queue_model γ vs1 -∗
spmc_queue_model γ vs2 -∗
False.
Lemma spmc_queue_producer_valid t γ vs ws :
spmc_queue_producer t γ ws -∗
spmc_queue_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma spmc_queue_producer_exclusive t γ ws1 ws2 :
spmc_queue_producer t γ ws1 -∗
spmc_queue_producer t γ ws2 -∗
False.
Lemma spmc_queue٠create𑁒spec ι :
{{{
True
}}}
spmc_queue٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
spmc_queue_inv t γ ι ∗
spmc_queue_model γ [] ∗
spmc_queue_producer t γ []
}}}.
#[local] Lemma front𑁒spec_strong Ψ t γ :
{{{
inv' t γ ∗
if Ψ is Some Ψ then
waiter_au γ Ψ
else
True
}}}
(#t).{front}
{{{
front i
, RET #front;
node_model γ front i true ∗
if Ψ is Some Ψ then
∃ waiter,
saved_pred waiter Ψ ∗
waiters_at γ waiter i
else
True
}}}.
#[local] Lemma front𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front i
, RET #front;
node_model γ front i true
}}}.
Variant operation :=
| IsEmpty waiter (Ψ : bool → iProp Σ)
| Pop (Ψ : option val → iProp Σ)
| Other.
Implicit Types op : operation.
Variant operation' :=
| IsEmpty'
| Pop'
| Other'.
#[local] Instance operation'_eq_dec : EqDecision operation' :=
ltac:(solve_decision).
#[local] Coercion operation_to_operation' op :=
match op with
| IsEmpty _ _ ⇒
IsEmpty'
| Pop _ ⇒
Pop'
| Other ⇒
Other'
end.
#[local] Definition pop_au γ (Ψ : option val → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(metadata_inv), ∅ <{
model₁ γ (tail vs)
, COMM
Ψ (head vs)
}>.
#[local] Lemma next𑁒spec_aux op t γ i node :
{{{
inv' t γ ∗
history_at γ i node ∗
( if decide (op = Other' :> operation') then True else
front_lb γ i
) ∗
match op with
| IsEmpty waiter Ψ ⇒
saved_pred waiter Ψ ∗
waiters_at γ waiter i ∗
£ 1
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
match op with
| IsEmpty waiter Ψ ⇒
Ψ true
| Pop Ψ ⇒
Ψ None
| Other ⇒
True
end
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false ∗
match op with
| IsEmpty waiter Ψ ⇒
Ψ false
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
}}}.
#[local] Lemma next𑁒spec t γ i node :
{{{
inv' t γ ∗
history_at γ i node
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false
}}}.
#[local] Lemma next𑁒spec_is_empty {t γ i node} waiter Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
front_lb γ i ∗
saved_pred waiter Ψ ∗
waiters_at γ waiter i ∗
£ 1
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ true
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false ∗
Ψ false
}}}.
#[local] Lemma next𑁒spec_pop {t γ i node} Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
front_lb γ i ∗
pop_au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ None
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) false ∗
pop_au γ Ψ
}}}.
Lemma spmc_queue٠is_empty𑁒spec t γ ι :
<<<
spmc_queue_inv t γ ι
| ∀∀ vs,
spmc_queue_model γ vs
>>>
spmc_queue٠is_empty #t @ ↑ι
<<<
spmc_queue_model γ vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma spmc_queue٠push𑁒spec t γ ι ws v :
<<<
spmc_queue_inv t γ ι ∗
spmc_queue_producer t γ ws
| ∀∀ vs,
spmc_queue_model γ vs
>>>
spmc_queue٠push #t v @ ↑ι
<<<
spmc_queue_model γ (vs ++ [v])
| RET ();
spmc_queue_producer t γ (vs ++ [v])
>>>.
#[local] Lemma spmc_queue٠pop𑁒spec_aux t γ :
<<<
inv' t γ
| ∀∀ vs,
model₁ γ vs
>>>
spmc_queue٠pop #t @ ↑γ.(metadata_inv)
<<<
model₁ γ (tail vs)
| RET head vs;
True
>>>.
Lemma spmc_queue٠pop𑁒spec t γ ι :
<<<
spmc_queue_inv t γ ι
| ∀∀ vs,
spmc_queue_model γ vs
>>>
spmc_queue٠pop #t @ ↑ι
<<<
spmc_queue_model γ (tail vs)
| RET head vs;
True
>>>.
End spmc_queue_G.
#[global] Opaque spmc_queue_inv.
#[global] Opaque spmc_queue_producer.
#[global] Opaque spmc_queue_model.
End base.
From zoo_saturn Require
spmc_queue__opaque.
Section spmc_queue_G.
Context `{spmc_queue_G : SpmcQueueG Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition spmc_queue_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.spmc_queue_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition spmc_queue_producer t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.spmc_queue_producer 𝑡 γ ws.
#[local] Instance : CustomIpat "producer" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hproducer{_{}} ) ".
Definition spmc_queue_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.spmc_queue_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance spmc_queue_model_timeless t vs :
Timeless (spmc_queue_model t vs).
#[global] Instance spmc_queue_producer_timeless t ws :
Timeless (spmc_queue_producer t ws).
#[global] Instance spmc_queue_inv_persistent t ι :
Persistent (spmc_queue_inv t ι).
Lemma spmc_queue_model_exclusive t vs1 vs2 :
spmc_queue_model t vs1 -∗
spmc_queue_model t vs2 -∗
False.
Lemma spmc_queue_producer_valid t vs ws :
spmc_queue_producer t ws -∗
spmc_queue_model t vs -∗
⌜vs `suffix_of` ws⌝.
Lemma spmc_queue_producer_exclusive t ws1 ws2 :
spmc_queue_producer t ws1 -∗
spmc_queue_producer t ws2 -∗
False.
Lemma spmc_queue٠create𑁒spec ι :
{{{
True
}}}
spmc_queue٠create ()
{{{
t
, RET t;
spmc_queue_inv t ι ∗
spmc_queue_model t [] ∗
spmc_queue_producer t []
}}}.
Lemma spmc_queue٠is_empty𑁒spec t ι :
<<<
spmc_queue_inv t ι
| ∀∀ vs,
spmc_queue_model t vs
>>>
spmc_queue٠is_empty t @ ↑ι
<<<
spmc_queue_model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma spmc_queue٠push𑁒spec t ι ws v :
<<<
spmc_queue_inv t ι ∗
spmc_queue_producer t ws
| ∀∀ vs,
spmc_queue_model t vs
>>>
spmc_queue٠push t v @ ↑ι
<<<
spmc_queue_model t (vs ++ [v])
| RET ();
spmc_queue_producer t (vs ++ [v])
>>>.
Lemma spmc_queue٠pop𑁒spec t ι :
<<<
spmc_queue_inv t ι
| ∀∀ vs,
spmc_queue_model t vs
>>>
spmc_queue٠pop t @ ↑ι
<<<
spmc_queue_model t (tail vs)
| RET head vs;
True
>>>.
End spmc_queue_G.
#[global] Opaque spmc_queue_inv.
#[global] Opaque spmc_queue_producer.
#[global] Opaque spmc_queue_model.