Module ThreadPoolExecutor

The type of thread pools to be used for futures.

make core_pool_size:cps max_pool_size:mps kat u reh returns a new thread pool with:

• cps as its core pool size (number of threads kept in the pool, even if idle);
• mps as its maximum pool size (maximum number of threads in the pool);
• kat keep alive time (how long to keep alive idle threads not in the core);
• u time unit for kat;
• reh policy for blocked computations.

Raises Java_exception if a size is negative

Waits for pool termination, waiting at most wait for t (time value whose unit is u); see awaitTermination(...).
Raises Java_exception if the thread is interrupted

Returns an estimate of the number of active threads in the pool; see getActiveCount(...).

Returns an estimate of the number of completed computations in the pool; see getCompletedTaskCount(...).

Returns the core size of the pool; see getCorePoolSize(...).

Returns the keep alive time for thread outside of the core; see getKeepAliveTime(...).

Returns the largest size reached by the pool; see getLargestPoolSize(...).

Returns the maximum size of the pool; see getMaximumPoolSize(...).

Returns an estimate of the current pool size; see getPoolSize(...).

Returns the policy for blocked computations; see getRejectedExecutionHandler(...).

Returns an estimate of number of task that have been submitted for execution; see getTaskCount(...).

invoke_all p l submits all functions from l to pool p, and then waits for the completion of all functions. Returns the list of created futures; it is guaranteed that all futures have completed.
Raises Java_exception if the thread is interrupted

invoke_all_time p l t u is similar to invoke_all p l, except that the current thread will at most wait for t (time value whose unit is u).
Raises Java_exception if the thread is interrupted

invoke_any p l submits all function from l to pool p, and then waits for the completion of a function. Returns the value computed by the first function completing its execution.
Raises

• Java_exception if the thread is interrupted
• Java_exception if no function completes without raising an exception

invoke_any_time p l t u is similar to invoke_any p l, except that the current thread will at most wait for t (time value whose unit is u).
Raises

• Java_exception if the thread is interrupted
• Java_exception f time has elapsed without any function completing its execution
• Java_exception if no function completes without raising an exception

Tests whether the pool has been shutdown; see isShutdown(...).

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

Tests whether the pool is in the process of terminating; see isTerminating(...).

Changes the core size of the pool (number of threads kept in the pool, even if idle); see setCorePoolSize(...).

Changes the keep alive time (how long to keep alive idle threads not in the core); see setKeepAliveTime(...).

Changes the maximum pool size (maximum number of threads in the pool); see setMaximumPoolSize(...).

Changes the policy for blocked computations; see setRejectedExecutionHandler(...).

Begins a shutdown, executing all submitted tasks, but refusing new tasks; see shutdown(...).

Begins a shhutdown by cancelling all submitted tasks, and cancelling running tasks; see shutdownNow(...).

submit p f x submits to p and returns a future computing f x.
Raises Java_exception if pool limits are 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.