barrier.v 437 Bytes
Newer Older
1
From heap_lang Require Export substitution 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

Ralf Jung's avatar
Ralf Jung committed
8
Instance newbarrier_closed : Closed newbarrier. Proof. solve_closed. Qed.
9
Instance signal_closed : Closed signal. Proof. solve_closed. Qed.
Ralf Jung's avatar
Ralf Jung committed
10
Instance wait_closed : Closed wait. Proof. solve_closed. Qed.