Library zoo_std.mutex__code

From zoo Require Import
  prelude.
From zoo.language Require Import
  typeclasses
  notations.
From zoo_std Require Import
  mutex__types.
From zoo Require Import
  options.

Definition mutex ٠ create : val :=
  fun : ≠ ⇒
    ref false.

Definition mutex ٠ lock : val :=
  rec : "lock" "t" ⇒
    if : ¬ CAS "t".[contents ] false true then (
      "lock" "t"
    ).

Definition mutex ٠ create_lock : val :=
  fun : ≠ ⇒
    ref true.

Definition mutex ٠ unlock : val :=
  fun : "t" ⇒
    "t" <- false.

Definition mutex ٠ synchronize : val :=
  fun : "t" ⇒
    mutex ٠ lock "t" ;;
    mutex ٠ unlock "t".

Definition mutex ٠ protect : val :=
  fun : "t" "fn" ⇒
    mutex ٠ lock "t" ;;
    let : "res" := "fn" () in
    mutex ٠ unlock "t" ;;
    "res".