Library zoo_parabs.ws_deques_private__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_std Require Import
  atomic_array
  queue_3
  array
  random_round
  domain.
From zoo_parabs Require Import
  ws_deques_private__types.
From zoo Require Import
  options.

Definition ws_deques_private٠create : val :=
  fun: "sz" ⇒
    { "sz",
      array٠unsafe_init "sz" queue_3٠create,
      array٠unsafe_make "sz" §Nonblocked,
      atomic_array٠make "sz" §RequestNone,
      array٠unsafe_make "sz" §ResponseWaiting,
      ()
    }.

Definition ws_deques_private٠size : val :=
  fun: "t" ⇒
    "t".{size}.

Definition ws_deques_private٠block : val :=
  fun: "t" "i" ⇒
    array٠unsafe_set "t".{statuses} "i" §Blocked ;;
    match: atomic_array٠unsafe_xchg "t".{requests} "i" §RequestBlocked with
    | RequestSome "j" ⇒
        array٠unsafe_set "t".{responses} "j" §ResponseNone
    |_ ⇒
        ()
    end.

Definition ws_deques_private٠unblock : val :=
  fun: "t" "i" ⇒
    atomic_array٠unsafe_set "t".{requests} "i" §RequestNone ;;
    array٠unsafe_set "t".{statuses} "i" §Nonblocked.

Definition ws_deques_private٠respond : val :=
  fun: "t" "i" ⇒
    match: atomic_array٠unsafe_get "t".{requests} "i" with
    | RequestSome "j" ⇒
        let: "response" :=
          match: queue_3٠pop_front (array٠unsafe_get "t".{queues} "i") with
          | Some "v" ⇒
              ‘ResponseSome( "v" )
          |_ ⇒
              §ResponseNone
          end
        in
        array٠unsafe_set "t".{responses} "j" "response" ;;
        atomic_array٠unsafe_set "t".{requests} "i" §RequestNone
    |_ ⇒
        ()
    end.

Definition ws_deques_private٠push : val :=
  fun: "t" "i" "v" ⇒
    queue_3٠push (array٠unsafe_get "t".{queues} "i") "v" ;;
    ws_deques_private٠respond "t" "i".

Definition ws_deques_private٠pop : val :=
  fun: "t" "i" ⇒
    let: "res" := queue_3٠pop_back (array٠unsafe_get "t".{queues} "i") in
    ws_deques_private٠respond "t" "i" ;;
    "res".

Definition ws_deques_private٠steal_to₀ : val :=
  rec: "steal_to" "t" "i" ⇒
    match: array٠unsafe_get "t".{responses} "i" with
    | ResponseWaiting ⇒
        domain٠yield () ;;
        "steal_to" "t" "i"
    | ResponseNone ⇒
        array٠unsafe_set "t".{responses} "i" §ResponseWaiting ;;
        §None
    | ResponseSome "v" ⇒
        array٠unsafe_set "t".{responses} "i" §ResponseWaiting ;;
        ‘Some( "v" )
    end.

Definition ws_deques_private٠steal_to : val :=
  fun: "t" "i" "j" ⇒
    if:
      array٠unsafe_get "t".{statuses} "j" == §Nonblocked
      and
      atomic_array٠unsafe_cas
        "t".{requests}
        "j"
        §RequestNone
        ‘RequestSome( "i" )
    then (
      ws_deques_private٠steal_to₀ "t" "i"
    ) else (
      §None
    ).

Definition ws_deques_private٠steal_as₀ : val :=
  rec: "steal_as" "t" "sz" "i" "round" "n" ⇒
    if: "n" ≤ 0 then (
      §None
    ) else (
      let: "j" := ("i" + 1 + random_round٠next "round") `rem` "sz" in
      match: ws_deques_private٠steal_to "t" "i" "j" with
      | None ⇒
          "steal_as" "t" "sz" "i" "round" ("n" - 1)
      |_ as "res" ⇒
          "res"
      end
    ).

Definition ws_deques_private٠steal_as : val :=
  fun: "t" "i" "round" ⇒
    let: "sz" := ws_deques_private٠size "t" in
    ws_deques_private٠steal_as₀ "t" "sz" "i" "round" ("sz" - 1).