Module type Messaging.S

type relay_message
type output_message =
  1. | Log of int * string
    (*

    Log message with level

    *)
  2. | Stat of string
    (*

    Statistics

    *)
  3. | Progress of int
    (*

    Progress

    *)

A message to be output to the user

type control_message =
  1. | Terminate
    (*

    Request termination of process

    *)

A message internal to the messaging system

type message =
  1. | OutputMessage of output_message
    (*

    Output to user

    *)
  2. | ControlMessage of control_message
    (*

    Message internal to the messaging system

    *)
  3. | RelayMessage of relay_message
    (*

    Message to be broadcast to worker processes

    *)

A message

val pp_print_message : Stdlib.Format.formatter -> message -> unit

Pretty-print a message

type ctx

The messaging system of an analysis, created by the supervisor

type worker

Registration of a worker mailbox

val init_im : unit -> ctx

Create the messaging system in the supervisor.

val init_worker : Lib.kind_module -> int -> ctx -> worker

Create and register the mailbox of a worker with the given kind module and identifier. Call run_worker in the domain of the worker afterwards.

val run_im : ctx -> unit

Take the supervisor role in the calling domain.

val run_worker : worker -> worker

Take the worker role in the calling domain.

val send_relay_message : relay_message -> unit

Broadcast a message to the other engines and, from a worker, to the supervisor

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

Broadcast a termination message to all engines

val send_term_message_to : int -> unit

Send a termination message to the engine with the given identifier

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

Receive the messages queued in the mailbox of the calling domain

val wait_for_message : unit -> unit

Block until a message is queued in the mailbox of the calling domain. Returns immediately if the mailbox is not empty. Any event a domain may wait for arrives as a message, including termination requests, so waiting without a timeout cannot delay shutdown.

val purge_im_mailbox : ctx -> unit

Purge the invariant manager mailbox. Should be called between two analyses, after all engines of the previous analysis have exited.

val check_termination : unit -> bool

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

val disconnect : worker -> unit

Unregister the mailbox of a worker, from any domain. The messages the worker sends from now on are dropped and a termination message is left in its mailbox, so that an engine that outlives its analysis cannot disturb the next one.

val exit : worker -> unit

Unregister the mailbox of a worker, from the worker itself