Library iris.locks.ticket

From iris.heap_lang Require Export lang notation.


Definition wait_loop: val :=
  rec: "wait_loop" "x" "lk" :=
    let: "o" := !(Fst "lk") in
    if: "x" = "o"
      then #()
      else "wait_loop" "x" "lk".

Definition newlock : val := λ: ≠, ( ref #0, ref #0).

Definition acquire : val :=
  λ: "lk",
    let: "n" := FAI (Snd "lk") in
    wait_loop "n" "lk".

Definition release : val := λ: "lk",
  (Fst "lk") <- !(Fst "lk") + #1.