Frama-C API - Task
High Level Interface to Command.
Task
val pretty : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a status -> unit
Monadic Constructors
val nop : unit task
The task that immediately returns unit
val return : 'a -> 'a task
The task that immediately returns a result
val raised : exn -> 'a task
The task that immediately fails with an exception
val canceled : unit -> 'a task
The task that is immediately canceled
val failed : ('a, Stdlib.Format.formatter, unit, 'b task) Stdlib.format4 -> 'a
The task that immediately fails by raising a Failure
exception. Typically: [let exit d : 'a task = failed "exit status %d" k]
val call : ?canceled:('a -> unit) -> ('a -> 'b) -> 'a -> 'b task
The task that, when started, invokes a function and immediately returns the result.
The task that, when started, compute a task to continue with.
bind t k
first runs t
. Then, when t
exit with status s
, it starts task k s
.
<b>Remark:</b> If t
was cancelled, k s
is still evaluated, but immediately canceled as well. This allows finally
-like behaviors to be implemented. To evaluate k r
only when t
terminates normally, make use of the sequence
operator.
sequence t k
first runs t
. If t
terminates with Result r
, then task k r
is started. Otherwise, failure or cancelation of t
is returned.
finally t cb
runs task t
and always calls cb s
when t
exits with status s
. Then s
is returned. If the callback cb
raises an exception, the returned status is emitted.
Same as finally
but the status of the task is discarded.
low level command for managing ressource with active wait
Synchronous Command
val mutex : unit -> mutex
Schedules a task such that only one can run simultaneously for a given mutex.
System Command
val command : ?timeout:float -> ?time:float Stdlib.ref -> ?stdout:Stdlib.Buffer.t -> ?stderr:Stdlib.Buffer.t -> string -> string array -> int task
Immediately launch a system-process. Default timeout is 0
, which means no-timeout at all. Standard outputs are discarded unless optional buffers are provided. To make the task start later, simply use todo (command ...)
.
Shared Tasks
When two tasks A
and B
share a common sub-task S
, cancelling A
will make B
fail either. To prevent this, it is necessary to make S
shareable and to use two distinct instances of S
in A
and B
.
Shared tasks manage the number of their instance and actually run or cancel a unique task on demand. In particular, shared tasks can be canceled and re-started later.
Shareable tasks.
Build a shareable task. The build function is called whenever a new instance is required but no shared instance task is actually running. Interrupted tasks (by Cancel or Timeout) are retried for further instances. If the task failed, it can be re-launch if retry
is true
. Otherwise, further instances will return Failed
status.
New instance of shared task.
Task Thread
val cancel : thread -> unit
val progress : thread -> bool
Make the thread progress and return true
if still running
val is_running : thread -> bool
Don't make the thread progress, just returns true
if not terminated or not started yet
val run : thread -> unit
Runs one single task in the background. Typically using on_idle
.
Task Pool
val pool : unit -> pool
val flush : pool -> unit
Clean all terminated tasks
val size : pool -> int
Auto-flush. Number of living tasks
Task Server
val server : ?stages:int -> ?procs:int -> unit -> server
Creates a server of commands.
Schedules a task on the server. The task is not immediately started.
val launch : server -> unit
Starts the server if not running yet
val cancel_all : server -> unit
Cancel all scheduled tasks
val get_procs : server -> int
Maximum number of running process
val set_procs : server -> int -> unit
Adjusts the maximum number of running process.
val on_server_activity : server -> (unit -> unit) -> unit
Idle server callback
val on_server_start : server -> (unit -> unit) -> unit
On-start server callback
val on_server_stop : server -> (unit -> unit) -> unit
On-stop server callback
val on_server_wait : server -> (unit -> unit) -> unit
On-wait server callback (all tasks are scheduled)
val terminated : server -> int
Number of terminated process
val remaining : server -> int
Number of remaining process
val scheduled : server -> int
Total number of scheduled process
val running : server -> int
Number of active process
val waiting : server -> int option
All task scheduled and server is waiting for termination