barrier.v 261 Bytes
Newer Older
1
From iris.heap_lang Require Export notation.
2
Set Default Proof Using "Type*".
3

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