Library iris.locks.clh

From iris.heap_lang Require Export lang notation.


Definition newlock : val :=
  λ: ≠,
       let: "dummy" := ref #false in
       ( ref "dummy", ref "dummy").

Definition wait_loop: val :=
  rec: "wait_loop" "me" "prev" "lk" :=
    let: "wait" := !"prev" in
    if: "wait"
      then "wait_loop" "me" "prev" "lk"
      else (Fst "lk") <- "me" .

Definition acquire : val :=
  λ: "lk",
    let: "me" := ref #true in
    let: "prev" := Swap (Snd "lk") "me" in
    wait_loop "me" "prev" "lk".

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