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

3
4
Definition newbarrier : val := locked (λ: <>, ref #false)%V.
Definition signal : val := locked (λ: "x", "x" <- #true)%V.
5
Definition wait : val :=
6
  locked (rec: "wait" "x" := if: !"x" then #() else "wait" "x")%V.