Module type Messaging.S

type relay_message
type output_message =
| Log of int * string

Log message with level

| Stat of string

Statistics

| Progress of int

Progress

A message to be output to the user

type control_message =
| Ready

Process is ready

| Ping

Request reply from process

| Terminate

Request termination of process

| Resend of int

Request resending of relay message

A message internal to the messaging system

type message =
| OutputMessage of output_message

Output to user

| ControlMessage of control_message

Message internal to the messaging system

| RelayMessage of int * relay_message

Message to be broadcast to worker processes

A message

type ctx

Messaging context

type socket

Socket

type thread

Thread

val init_im : unit -> (ctx * socket * socket) * (string * string)

Create a messaging context and bind ports for the invariant manager. Return a pair of pub socket and pull socket and pair of addresses of pub and pull sockets for workers to connect to.

Call this function before forking the processes, the first return argument must only be used by the parent process, the child processes must use the socket addresses in the second return argument.

val init_worker : Lib.kind_module -> string -> string -> ctx * socket * socket

Create a messaging context and bind given ports for a worker process. Return a messaging context and a pair of sub and push sockets.

val run_im : (ctx * socket * socket) -> (int * Lib.kind_module) list -> (exn -> unit) -> unit

Start the background thread for the invariant manager, using the given context and sockets. The second parameter is a list of PIDs and the kind of worker processes to watch, the third argument is the function to call to handle exceptions.

val run_worker : (ctx * socket * socket) -> Lib.kind_module -> (exn -> unit) -> thread

Start the background thread for a worker process, using the given context and sockets. The second parameter is type of worker process, the third is the function to call to handle exceptions.

val send_relay_message : relay_message -> unit

Broadcast a message to the worker processes

val send_output_message : output_message -> unit

Send a message to the invariant manager for output to the user

val send_term_message : unit -> unit

Send a termination message to the invariant manager

val recv : unit -> (Lib.kind_module * message) list

Receive messages queued by the background thread

val update_child_processes_list : (int * Lib.kind_module) list -> unit

Notifies the background thread of a new list of child processes. Used by the supervisor in a modular analysis when restarting.

val purge_im_mailbox : (ctx * socket * socket) -> unit

Purge the invariant manager mailbox. Should be called before calling update_child_processes_list in order to get rid of messages from the previous analysis.

val check_termination : unit -> bool

Returns true if a termination message was received. Does NOT modify received message in any way.

val exit : thread -> unit

Request the background thread of a worker process to terminate