Library zoo_parabs.waiter__code
Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.condition.
Require Import zoo_std.mutex.
Require Import zoo.options.
Notation "'waiterู mutex'" := (
in_type "zoo_parabs.waiter.t" 0
)(in custom zoo_field
).
Notation "'waiterู condition'" := (
in_type "zoo_parabs.waiter.t" 1
)(in custom zoo_field
).
Notation "'waiterู flag'" := (
in_type "zoo_parabs.waiter.t" 2
)(in custom zoo_field
).
Definition waiterู create : val :=
๐ณ๐๐ป โฝ โ
{ mutexู create (), conditionู create (), false }.
Definition waiterู notify : val :=
๐ณ๐๐ป "t" โ
mutexู lock "t".{waiterู mutex} โฎ
๐ถ๐ณ "t".{waiterู flag} ๐๐ต๐ฒ๐ป (
mutexู unlock "t".{waiterู mutex} โฎ
false
) ๐ฒ๐น๐๐ฒ (
"t" <-{waiterู flag} true โฎ
mutexู unlock "t".{waiterู mutex} โฎ
conditionู notify "t".{waiterู condition} โฎ
true
).
Definition waiterู prepare_wait : val :=
๐ณ๐๐ป "t" โ
mutexู protect "t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ "t" <-{waiterู flag} false).
Definition waiterู cancel_wait : val :=
๐ณ๐๐ป "t" โ
mutexู protect "t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ
๐ถ๐ณ "t".{waiterู flag} ๐๐ต๐ฒ๐ป (
false
) ๐ฒ๐น๐๐ฒ (
"t" <-{waiterู flag} true โฎ
true
)).
Definition waiterู commit_wait : val :=
๐ณ๐๐ป "t" โ
mutexู protect "t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ
conditionู wait_until
"t".{waiterู condition}
"t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ "t".{waiterู flag})).
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.condition.
Require Import zoo_std.mutex.
Require Import zoo.options.
Notation "'waiterู mutex'" := (
in_type "zoo_parabs.waiter.t" 0
)(in custom zoo_field
).
Notation "'waiterู condition'" := (
in_type "zoo_parabs.waiter.t" 1
)(in custom zoo_field
).
Notation "'waiterู flag'" := (
in_type "zoo_parabs.waiter.t" 2
)(in custom zoo_field
).
Definition waiterู create : val :=
๐ณ๐๐ป โฝ โ
{ mutexู create (), conditionู create (), false }.
Definition waiterู notify : val :=
๐ณ๐๐ป "t" โ
mutexู lock "t".{waiterู mutex} โฎ
๐ถ๐ณ "t".{waiterู flag} ๐๐ต๐ฒ๐ป (
mutexู unlock "t".{waiterู mutex} โฎ
false
) ๐ฒ๐น๐๐ฒ (
"t" <-{waiterู flag} true โฎ
mutexู unlock "t".{waiterู mutex} โฎ
conditionู notify "t".{waiterู condition} โฎ
true
).
Definition waiterู prepare_wait : val :=
๐ณ๐๐ป "t" โ
mutexู protect "t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ "t" <-{waiterู flag} false).
Definition waiterู cancel_wait : val :=
๐ณ๐๐ป "t" โ
mutexู protect "t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ
๐ถ๐ณ "t".{waiterู flag} ๐๐ต๐ฒ๐ป (
false
) ๐ฒ๐น๐๐ฒ (
"t" <-{waiterู flag} true โฎ
true
)).
Definition waiterู commit_wait : val :=
๐ณ๐๐ป "t" โ
mutexู protect "t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ
conditionู wait_until
"t".{waiterู condition}
"t".{waiterู mutex}
(๐ณ๐๐ป โฝ โ "t".{waiterู flag})).