Library zoo_saturn.inf_queue_mpmc_1

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.function.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_nat.
Require Import zoo_std.option.
Require Export zoo_saturn.inf_queue_mpmc_1__code.
Require Import zoo_saturn.inf_queue_mpmc_1__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type front back : nat.
Implicit Type v : val.
Implicit Type vs hist : list val.
Implicit Type slot : optional val.
Implicit Type slots : nat → optional val.
Implicit Type η : gname.
Implicit Type ηs : list gname.

Class InfQueueMpmc1G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] inf_queue_mpmc_1 ۰ G ۰ inf_array ۰ G :: InfArrayG Σ
  ; #[local] inf_queue_mpmc_1 ۰ G ۰ model ۰ G :: TwinsG Σ (leibnizO (list val))
  ; #[local] inf_queue_mpmc_1 ۰ G ۰ history ۰ G :: MonoListG Σ val
  ; #[local] inf_queue_mpmc_1 ۰ G ۰ consumer ۰ G :: SavedPredG Σ val
  ; #[local] inf_queue_mpmc_1 ۰ G ۰ consumers ۰ G :: MonoListG Σ gname
  ; #[local] inf_queue_mpmc_1 ۰ G ۰ token ۰ G :: OneshotG Σ () ()
  ; #[local] inf_queue_mpmc_1 ۰ G ۰ tokens ۰ G :: MonoListG Σ gname
  }.

Definition inf_queue_mpmc_1 ۰ Σ :=
  #[inf_array ۰ Σ
  ; twins ۰ Σ (leibnizO (list val))
  ; mono_list ۰ Σ val
  ; saved_pred ۰ Σ val
  ; mono_list ۰ Σ gname
  ; oneshot ۰ Σ () ()
  ; mono_list ۰ Σ gname
  ].
#[global] Instance subG ｰ inf_queue_mpmc_1 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG inf_queue_mpmc_1 ۰ Σ Σ →
  InfQueueMpmc1G Σ.

Module base.
  Section inf_queue_mpmc_1 ۰ G.
    Context `{inf_queue_mpmc_1 ۰ G : InfQueueMpmc1G Σ}.

    Implicit Type t : location.
    Implicit Type Ψ : val → iProp Σ.

    Record inf_queue_mpmc_1 ۰ name :=
      { inf_queue_mpmc_1 ۰ name ۰ data : val
      ; inf_queue_mpmc_1 ۰ name ۰ inv : namespace
      ; inf_queue_mpmc_1 ۰ name ۰ model : gname
      ; inf_queue_mpmc_1 ۰ name ۰ history : gname
      ; inf_queue_mpmc_1 ۰ name ۰ consumers : gname
      ; inf_queue_mpmc_1 ۰ name ۰ tokens : gname
      }.
    Implicit Type γ : inf_queue_mpmc_1 ۰ name.

    #[global] Instance inf_queue_mpmc_1 ۰ name ｰ eq_dec : EqDecision inf_queue_mpmc_1 ۰ name :=
      ltac:(solve_decision).
    #[global] Instance inf_queue_mpmc_1 ۰ name ｰ countable :
      Countable inf_queue_mpmc_1 ۰ name.

    #[local] Definition model₁' γ_model vs :=
      twins ۰ twin₁ γ_model (DfracOwn 1) vs.
    #[local] Definition model₁ γ :=
      model₁' γ.(inf_queue_mpmc_1 ۰ name ۰ model).
    #[local] Definition model₂' γ_model vs :=
      twins ۰ twin₂ γ_model vs.
    #[local] Definition model₂ γ :=
      model₂' γ.(inf_queue_mpmc_1 ۰ name ۰ model).

    #[local] Definition history ۰ auth' γ_history hist :=
      mono_list ۰ auth γ_history (DfracOwn 1) hist.
    #[local] Definition history ۰ auth γ :=
      history ۰ auth' γ.(inf_queue_mpmc_1 ۰ name ۰ history).
    #[local] Definition history ۰ at γ i v :=
      mono_list ۰ at γ.(inf_queue_mpmc_1 ۰ name ۰ history) i v.

    #[local] Definition consumers ۰ auth' γ_consumers i : iProp Σ :=
      ∃ ηs ,
      mono_list ۰ auth γ_consumers (DfracOwn 1) ηs ∗
      ⌜length ηs = i ⌝.
    #[local] Definition consumers ۰ auth γ i :=
      consumers ۰ auth' γ.(inf_queue_mpmc_1 ۰ name ۰ consumers) i.
    #[local] Instance : CustomIpat "consumers۰auth" :=
      " ( %ηs{} & Hauth{} & %Hηs{} ) ".
    #[local] Definition consumers ۰ at γ i Ψ : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_1 ۰ name ۰ consumers) i η ∗
      saved_pred η Ψ.
    #[local] Instance : CustomIpat "consumers۰at" :=
      " ( %η{} & Hat{} & HΨ{} ) ".
    #[local] Definition consumers ۰ lb γ i : iProp Σ :=
      ∃ ηs ,
      ⌜length ηs = i ⌝ ∗
      mono_list ۰ lb γ.(inf_queue_mpmc_1 ۰ name ۰ consumers) ηs.
    #[local] Instance : CustomIpat "consumers۰lb" :=
      " ( %ηs{} & %Hηs{} & Hlb{} ) ".

    #[local] Definition tokens ۰ auth' γ_tokens i : iProp Σ :=
      ∃ ηs ,
      mono_list ۰ auth γ_tokens (DfracOwn 1) ηs ∗
      ⌜length ηs = i ⌝.
    #[local] Definition tokens ۰ auth γ i :=
      tokens ۰ auth' γ.(inf_queue_mpmc_1 ۰ name ۰ tokens) i.
    #[local] Instance : CustomIpat "tokens۰auth" :=
      " ( %ηs{} & Hauth{} & %Hηs{} ) ".
    #[local] Definition tokens ۰ pending γ i : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_1 ۰ name ۰ tokens) i η ∗
      oneshot ۰ pending η (DfracOwn 1) ().
    #[local] Instance : CustomIpat "tokens۰pending" :=
      " ( %η{} & Hat{} & Hpending{} ) ".
    #[local] Definition tokens ۰ done γ i : iProp Σ :=
      ∃ η ,
      mono_list ۰ at γ.(inf_queue_mpmc_1 ۰ name ۰ tokens) i η ∗
      oneshot ۰ shot η ().
    #[local] Instance : CustomIpat "tokens۰done" :=
      " ( %η{} & Hat{} & Hshot{} ) ".

    #[local] Definition consumer ۰ au γ Ψ : iProp Σ :=
      AU <{
        ∃∃ vs ,
        model₁ γ vs
      }> @ ⊤ ∖ ↑γ.(inf_queue_mpmc_1 ۰ name ۰ inv), ∅ <{
        ∀∀ v vs',
        ⌜vs = v :: vs'⌝ ∗
        model₁ γ vs'
      , COMM
        Ψ v
      }>.

    #[local] Definition slot ۰ model γ i slot : iProp Σ :=
      match slot with
      | Something v ⇒
          history ۰ at γ i v
      | Anything ⇒
          tokens ۰ done γ i
      | Nothing ⇒
          True
      end.
    #[local] Definition inv ۰ inner t γ : iProp Σ :=
      ∃ front back hist slots ,
      t .[front ] ↦ #front ∗
      t .[back ] ↦ #back ∗
      inf_array ۰ model γ.(inf_queue_mpmc_1 ۰ name ۰ data) (optional ۰ to_val ∘ slots) ∗
      history ۰ auth γ hist ∗
      ⌜length hist = back ⌝ ∗
      model₂ γ (drop front hist) ∗
      consumers ۰ auth γ front ∗
      tokens ۰ auth γ (front `max ` back) ∗
      ( [∗ list ] i ∈ seq 0 back ,
          tokens ۰ pending γ i
        ∨ ∃ Ψ ,
          consumers ۰ at γ i Ψ ∗
          ( tokens ۰ done γ i
          ∨ ∃ v ,
            history ۰ at γ i v ∗
            Ψ v
          )
      ) ∗
      ( [∗ list ] i ∈ seq back (front - back),
        ∃ Ψ ,
        consumers ۰ at γ i Ψ ∗
        consumer ۰ au γ Ψ
      ) ∗
      (∀ i , slot ۰ model γ i (slots i)).
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %front{} & %back{} & %hist{} & %slots{} & Ht_front & Ht_back & >Hdata_model & >Hhistory_auth & >%Hhist{} & Hmodel₂ & Hconsumers_auth & Htokens_auth & Hpast & Hwaiters & Hslots ) ".
    Definition inv' t γ : iProp Σ :=
      t .[data ] ↦□ γ.(inf_queue_mpmc_1 ۰ name ۰ data) ∗
      inf_array ۰ inv γ.(inf_queue_mpmc_1 ۰ name ۰ data) ∗
      inv γ.(inf_queue_mpmc_1 ۰ name ۰ inv) (inv ۰ inner t γ).
    #[local] Instance : CustomIpat "inv'" :=
      " ( #Ht_data & #Hdata_inv & #Hinv ) ".
    Definition inf_queue_mpmc_1 ۰ inv t γ ι : iProp Σ :=
      ⌜ι = γ.(inf_queue_mpmc_1 ۰ name ۰ inv)⌝ ∗
      inv' t γ.
    #[local] Instance : CustomIpat "inv" :=
      " ( -> & (:inv') ) ".

    Definition inf_queue_mpmc_1 ۰ model :=
      model₁.
    #[local] Instance : CustomIpat "model" :=
      " Hmodel₁{_{}} ".

    #[local] Instance tokens ۰ pending ｰ timeless γ i :
      Timeless (tokens ۰ pending γ i).
    #[local] Instance tokens ۰ done ｰ timeless γ i :
      Timeless (tokens ۰ done γ i).
    #[local] Instance slot ۰ model ｰ timeless γ i slot :
      Timeless (slot ۰ model γ i slot).
    #[global] Instance inf_queue_mpmc_1 ۰ model ｰ timeless γ vs :
      Timeless (inf_queue_mpmc_1 ۰ model γ vs).

    #[local] Instance consumers ۰ at ｰ persistent γ i Ψ :
      Persistent (consumers ۰ at γ i Ψ).
    #[local] Instance consumers ۰ lb ｰ persistent γ i :
      Persistent (consumers ۰ lb γ i).
    #[local] Instance tokens ۰ done ｰ persistent γ i :
      Persistent (tokens ۰ done γ i).
    #[local] Instance slot ۰ model ｰ persistent γ i slot :
      Persistent (slot ۰ model γ i slot).
    #[global] Instance inf_queue_mpmc_1 ۰ inv ｰ persistent t γ ι :
      Persistent (inf_queue_mpmc_1 ۰ inv t γ ι).

    #[local] Lemma model ｰ alloc :
      ⊢ |==>
        ∃ γ_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 ｰ update {γ vs1 vs2} vs :
      model₁ γ vs1 -∗
      model₂ γ vs2 ==∗
        model₁ γ vs ∗
        model₂ γ vs.

    #[local] Lemma history ｰ alloc :
      ⊢ |==>
        ∃ γ_history ,
        history ۰ auth' γ_history [].
    #[local] Lemma history ۰ at ｰ valid γ hist i v :
      history ۰ auth γ hist -∗
      history ۰ at γ i v -∗
      ⌜hist !! i = Some v ⌝.
    #[local] Lemma history ۰ at ｰ agree γ i v1 v2 :
      history ۰ at γ i v1 -∗
      history ۰ at γ i v2 -∗
      ⌜v1 = v2 ⌝.
    #[local] Lemma history ۰ at ｰ get {γ hist} i v :
      hist !! i = Some v →
      history ۰ auth γ hist ⊢
      history ۰ at γ i v.
    #[local] Lemma history ｰ update {γ hist} v :
      history ۰ auth γ hist ⊢ |==>
        history ۰ auth γ (hist ++ [v]) ∗
        history ۰ at γ (length hist) v.

    #[local] Lemma consumers ｰ alloc :
      ⊢ |==>
        ∃ γ_consumers ,
        consumers ۰ auth' γ_consumers 0.
    #[local] Lemma consumers ۰ at ｰ valid γ i j Ψ :
      consumers ۰ auth γ i -∗
      consumers ۰ at γ j Ψ -∗
      ⌜j < i ⌝.
    #[local] Lemma consumers ۰ at ｰ agree γ i Ψ1 Ψ2 v :
      consumers ۰ at γ i Ψ1 -∗
      ▷ consumers ۰ at γ i Ψ2 -∗
      ▷ Ψ2 v -∗
      ▷^2 Ψ1 v.
    #[local] Lemma consumers ۰ lb ｰ valid γ i j :
      consumers ۰ auth γ i -∗
      consumers ۰ lb γ j -∗
      ⌜j ≤ i ⌝.
    #[local] Lemma consumers ۰ lb ｰ get γ i :
      consumers ۰ auth γ i ⊢
      consumers ۰ lb γ i.
    #[local] Lemma consumers ｰ update {γ i} Ψ :
      consumers ۰ auth γ i ⊢ |==>
        consumers ۰ auth γ ˖i ∗
        consumers ۰ at γ i Ψ.
    Opaque consumers ۰ auth'.
    Opaque consumers ۰ at.
    Opaque consumers ۰ lb.

    #[local] Lemma tokens ｰ alloc :
      ⊢ |==>
        ∃ γ_tokens ,
        tokens ۰ auth' γ_tokens 0.
    #[local] Lemma tokens ۰ pending ｰ exclusive γ i :
      tokens ۰ pending γ i -∗
      tokens ۰ pending γ i -∗
      False.
    #[local] Lemma tokens ۰ pending ｰ done γ i :
      tokens ۰ pending γ i -∗
      tokens ۰ done γ i -∗
      False.
    #[local] Lemma tokens ｰ update {γ} i :
      tokens ۰ auth γ i ⊢ |==>
        tokens ۰ auth γ ˖i ∗
        tokens ۰ pending γ i.
    #[local] Lemma tokens ۰ pending ｰ update γ i :
      tokens ۰ pending γ i ⊢ |==>
      tokens ۰ done γ i.
    Opaque tokens ۰ auth'.
    Opaque tokens ۰ pending.
    Opaque tokens ۰ done.

    Lemma inf_queue_mpmc_1 ۰ model ｰ exclusive γ vs1 vs2 :
      inf_queue_mpmc_1 ۰ model γ vs1 -∗
      inf_queue_mpmc_1 ۰ model γ vs2 -∗
      False.

    Lemma inf_queue_mpmc_1 ٠ create ｰ spec ι :
      {{{
        True
      }}}
        inf_queue_mpmc_1 ٠ create ()
      {{{
        t γ
      , RET #t ;
        meta_token t ⊤ ∗
        inf_queue_mpmc_1 ۰ inv t γ ι ∗
        inf_queue_mpmc_1 ۰ model γ []
      }}}.

    Lemma inf_queue_mpmc_1 ٠ size ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_1 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_1 ۰ model γ vs
      >>>
        inf_queue_mpmc_1 ٠ size #t @ ↑ι
      <<<
        inf_queue_mpmc_1 ۰ model γ vs
      | RET #(length vs );
        True
      >>>.

    Lemma inf_queue_mpmc_1 ٠ is_empty ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_1 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_1 ۰ model γ vs
      >>>
        inf_queue_mpmc_1 ٠ is_empty #t @ ↑ι
      <<<
        inf_queue_mpmc_1 ۰ model γ vs
      | RET #(bool_decide (vs = []%list));
        True
      >>>.

    Lemma inf_queue_mpmc_1 ٠ is_empty_weak ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_1 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_1 ۰ model γ vs
      >>>
        inf_queue_mpmc_1 ٠ is_empty_weak #t @ ↑ι
      <<<
        ∃∃ b ,
        ⌜if b then vs = [] else True ⌝ ∗
        inf_queue_mpmc_1 ۰ model γ vs
      | RET #b ;
        True
      >>>.

    Lemma inf_queue_mpmc_1 ٠ push ｰ spec t γ ι v :
      <<<
        inf_queue_mpmc_1 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_1 ۰ model γ vs
      >>>
        inf_queue_mpmc_1 ٠ push #t v @ ↑ι
      <<<
        inf_queue_mpmc_1 ۰ model γ (vs ++ [v])
      | RET ();
        True
      >>>.

    #[local] Lemma inf_queue_mpmc_1 ٠ pop₁ ｰ spec t γ front Ψ :
      {{{
        inv' t γ ∗
        consumers ۰ at γ front Ψ ∗
        tokens ۰ pending γ front
      }}}
        inf_queue_mpmc_1 ٠ pop₁ #t #front
      {{{
        v
      , RET v ;
        Ψ v
      }}}.
    Lemma inf_queue_mpmc_1 ٠ pop ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_1 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_1 ۰ model γ vs
      >>>
        inf_queue_mpmc_1 ٠ pop #t @ ↑ι
      <<<
        ∃∃ v vs',
        ⌜vs = v :: vs'⌝ ∗
        inf_queue_mpmc_1 ۰ model γ vs'
      | RET v ;
        True
      >>>.

    Lemma inf_queue_mpmc_1 ٠ try_pop ｰ spec t γ ι :
      <<<
        inf_queue_mpmc_1 ۰ inv t γ ι
      | ∀∀ vs ,
        inf_queue_mpmc_1 ۰ model γ vs
      >>>
        inf_queue_mpmc_1 ٠ try_pop #t @ ↑ι
      <<<
        inf_queue_mpmc_1 ۰ model γ (tail vs)
      | RET head vs ;
        True
      >>>.
  End inf_queue_mpmc_1 ۰ G.

  #[global] Opaque inf_queue_mpmc_1 ۰ inv.
  #[global] Opaque inf_queue_mpmc_1 ۰ model.
End base.

Require zoo_saturn.inf_queue_mpmc_1__opaque.

Section inf_queue_mpmc_1 ۰ G.
  Context `{inf_queue_mpmc_1 ۰ G : InfQueueMpmc1G Σ}.

  Implicit Type 𝑡 : location.
  Implicit Type t : val.

  Definition inf_queue_mpmc_1 ۰ inv t ι : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    base.inf_queue_mpmc_1 ۰ inv 𝑡 γ ι.
  #[local] Instance : CustomIpat "inv" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".

  Definition inf_queue_mpmc_1 ۰ model t vs : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    base.inf_queue_mpmc_1 ۰ model γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".

  #[global] Instance inf_queue_mpmc_1 ۰ model ｰ timeless t vs :
    Timeless (inf_queue_mpmc_1 ۰ model t vs).

  #[global] Instance inf_queue_mpmc_1 ۰ inv ｰ persistent t ι :
    Persistent (inf_queue_mpmc_1 ۰ inv t ι).

  Lemma inf_queue_mpmc_1 ۰ model ｰ exclusive t vs1 vs2 :
    inf_queue_mpmc_1 ۰ model t vs1 -∗
    inf_queue_mpmc_1 ۰ model t vs2 -∗
    False.

  Lemma inf_queue_mpmc_1 ٠ create ｰ spec ι :
    {{{
      True
    }}}
      inf_queue_mpmc_1 ٠ create ()
    {{{
      t
    , RET t ;
      inf_queue_mpmc_1 ۰ inv t ι ∗
      inf_queue_mpmc_1 ۰ model t []
    }}}.

  Lemma inf_queue_mpmc_1 ٠ size ｰ spec t ι :
    <<<
      inf_queue_mpmc_1 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_1 ۰ model t vs
    >>>
      inf_queue_mpmc_1 ٠ size t @ ↑ι
    <<<
      inf_queue_mpmc_1 ۰ model t vs
    | RET #(length vs );
      True
    >>>.

  Lemma inf_queue_mpmc_1 ٠ is_empty ｰ spec t ι :
    <<<
      inf_queue_mpmc_1 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_1 ۰ model t vs
    >>>
      inf_queue_mpmc_1 ٠ is_empty t @ ↑ι
    <<<
      inf_queue_mpmc_1 ۰ model t vs
    | RET #(bool_decide (vs = []%list));
      True
    >>>.

  Lemma inf_queue_mpmc_1 ٠ is_empty_weak ｰ spec t ι :
    <<<
      inf_queue_mpmc_1 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_1 ۰ model t vs
    >>>
      inf_queue_mpmc_1 ٠ is_empty_weak t @ ↑ι
    <<<
      ∃∃ b ,
      ⌜if b then vs = [] else True ⌝ ∗
      inf_queue_mpmc_1 ۰ model t vs
    | RET #b ;
      True
    >>>.

  Lemma inf_queue_mpmc_1 ٠ push ｰ spec t ι v :
    <<<
      inf_queue_mpmc_1 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_1 ۰ model t vs
    >>>
      inf_queue_mpmc_1 ٠ push t v @ ↑ι
    <<<
      inf_queue_mpmc_1 ۰ model t (vs ++ [v])
    | RET ();
      True
    >>>.

  Lemma inf_queue_mpmc_1 ٠ pop ｰ spec t ι :
    <<<
      inf_queue_mpmc_1 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_1 ۰ model t vs
    >>>
      inf_queue_mpmc_1 ٠ pop t @ ↑ι
    <<<
      ∃∃ v vs',
      ⌜vs = v :: vs'⌝ ∗
      inf_queue_mpmc_1 ۰ model t vs'
    | RET v ;
      True
    >>>.

  Lemma inf_queue_mpmc_1 ٠ try_pop ｰ spec t ι :
    <<<
      inf_queue_mpmc_1 ۰ inv t ι
    | ∀∀ vs ,
      inf_queue_mpmc_1 ۰ model t vs
    >>>
      inf_queue_mpmc_1 ٠ try_pop t @ ↑ι
    <<<
      inf_queue_mpmc_1 ۰ model t (tail vs)
    | RET head vs ;
      True
    >>>.
End inf_queue_mpmc_1 ۰ G.

#[global] Opaque inf_queue_mpmc_1 ۰ inv.
#[global] Opaque inf_queue_mpmc_1 ۰ model.