Module Phaser

The type of phasers, differing from coutdown latches and cyclic barriers by the fact that parties explicitly register.

Phasers are also organized in a tree-like structure, to reduce contention: a phaser is automatically registered/deregistered with its parent when the number of parties becomes respectively non-zero/zero.

The phase number of a phaser starts at zero, and advances when all parties arrive at the phaser.

make ~parent:p ~parties:n returns a new phaser with parent p (defaulting to null), and number of parties n (defaulting to 0l); see Phaser(...).
Raises Java_exception if n is negative

Records that a party has arrived to the phaser without waiting for others, returns the phase number (negative if the phaser is terminated); see arrive(...).
Raises Java_exception if the phase number would be negative while the phaser is not terminated

Records that a party has arrived to the phaser and waits for others, returns the phase number (negative if the phaser is terminated); see arriveAndAwaitAdvance(...).
Raises Java_exception if the phase number would be negative while the phaser is not terminated

Records that a party has arrived to the phaser without waiting for others, deregisters a party, returns the phase number (negative if the phaser is terminated); see arriveAndDeregister(...).
Raises Java_exception if the phase number would be negative while the phaser is not terminated

Waits for the phase number of the phaser to reach the passed value; see awaitAdvance(...).

Similar to Phaser.await_advance except that the thread can be interrupted; see awaitAdvanceInterruptibly(...).
Raises Java_exception if the thread is interrupted

await_advance_interruptibly_time p pn t u is similar to await_advance_interruptibly p pn, except that the current thread will at most wait for t (time value whose unit is u); see awaitAdvanceInterruptibly(...).
Raises

• Java_exception if the thread is interrupted
• Java_exception if time has elapsed without reaching the given phase number

bulk_register p n adds n unarrived parties to phaser p; see bulkRegister(...).
Raises

• Java_exception if n is negative
• Java_exception if the maximum number of parties has already been reached

Forces termination of the phaser, includind children phasers; see forceTermination(...).

Returns the number of registered parties that have arrived to the phaser; see getArrivedParties(...).

Returns the parent of the phaser; see getParent(...).

Returns the phase number; see getPhase(...).

Returns the number of registered parties; see getRegisteredParties(...).

Returns the root that can be reached from the phaser by recursively visiting parents. Returns the passed phaser if it has no parent; see getRoot(...).

Returns the number of registered parties that have not yet arrived to the phaser; see getUnarrivedParties(...).

Tests whether the phaser has been terminated; see isTerminated(...).

Adds a new unarrived party to the phaser, and returns the current phase number; see register(...).
Raises Java_exception if the maximum number of parties has already been reached

The null value.

is_null obj returns true iff obj is equal to null.

is_not_null obj returns false iff obj is equal to null.

wrap obj wraps the reference obj into an option type:

• Some x if obj is not null;
• None if obj is null.

unwrap obj unwraps the option obj into a bare reference:

• Some x is mapped to x;
• None is mapped to null.