barrier.v 264 Bytes
Newer Older
1
From iris.heap_lang Require Export notation.
2

3
Definition newbarrier : val := λ: <>, ref #0.
4
Definition signal : val := λ: "x", "x" <- #1.
5
Definition wait : val :=
6
  rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
7
Global Opaque newbarrier signal wait.