Go backward to A.2 Message Passing Go up to A The Scheduler Protocol

A.3 The Protocol

The protocol is based on the following condition that describes the initial values of some program variables:

Init ==

/\

• T = null
• taskDepth = 0
• waitDepth = 0

The protocol is then specified by the following temporal formula:

Protocol ==

/\

• (Init /\ S = initExecuting) => [] Program
• (Init /\ S = initServer) => [] Program

This formula covers the two cases of an external application program that starts its life with the execution of a program (such as the Maple kernel connected to the user interface) respectively of a program that starts its live as a server for evaluating tasks (such as the Maple kernels that are remotely started).

The following predicate describes the individual actions that may be performed; as a general convention we parameterize each predicate over the value of the successor state S':

Program ==

\/

• (program entry)

  /\

  • S = initExecuting
  • initialize(executing)

• (server entry)

  /\

  • S = initServer
  • initialze(server)

• (execute a program)

  /\

  • S = executing
  • (actions)

    \/

    • sendTask(executing)
    • sendWait(server)
    • sendNWait(server)
    • sendAll(executing)
    • sendQuit(terminate)
    • sendAbort(terminate)
    • sendStart(executing)
    • sendDelete(executing)
    • sendFlush(executing)
    • sendReset(executing)
    • sendResult(server)

• (run as a server)

  /\

  • S = server
  • (actions)

    \/

    • receiveTask(executing)
    • receiveAll(server)
    • receiveQuit(terminate)
    • receiveAbort(terminate)
    • receiveResult(executing)

When the program is in status "executing", it may switch to status "server" by sending a (n)wait request (which may result in another task to be evaluated if the request cannot be immediately satisfied) or by sending the result of a task (that was previously received when in server mode). When the program is in status "server", it may switch to status "executing", if it receives a new task to execute or if it receives the result of a task it has previously sent a request for. In status "server", it also has to expect "all" messages (to evaluate some command) respectively "quit" or "abort" messages (to terminate execution).

The individual actions are described in the following sections.