Go backward to A.1 Protocol Variables Go up to A The Scheduler Protocol Go forward to A.3 The Protocol

A.2 Message Passing

The application program communicates with the scheduler by sending respectively receiving sequences of messages via some input respectively output channel. A message is written to a channel as a sequence of strings seperated by newline characters such that the first string denotes the message key and the remaining strings denote the body of the message. We use in our specification the predicate

send(m, n)

to denote the action that writes the sequence of lines

m.key
m.body[0]
...
m.body[n-1]

to the output channel. Likewise, the predicate

receive(m, n)

denotes the action of writing n+1 lines from the input channel and constructing a corresponding message m. The actions

write(s)
reads

write/read a string s to/from the output channel.