barrier.v 209 Bytes
Newer Older
1
From heap_lang Require Export notation.
2
3
4

Definition newchan := (λ: "", ref '0)%L.
Definition signal := (λ: "x", "x" <- '1)%L.
5
Definition wait := (rec: "wait" "x" :=if: !"x" = '1 then '() else "wait" "x")%L.