Go backward to Send Actions Go up to A.3 The Protocol

Receive Actions

When the program receives a task for evaluation, it pushes this task on the stack (its result must be delivered before the result of any of the other task on the stack).

receiveTask(C) ==

/\

• exists message: Message

  /\

  • receive(message, 2)
  • message.key = task
  • taskStack[taskDepth] = message
  • exists taskid: TaskId, exp: Expression
    • message.body[0] = taskid
    • message.body[1] = exp
  • taskDepth' = taskDepth+1

• S' = C

When the program receives an all message, this message contains a command to be executed.

receiveAll(C) ==

/\

• exists message: Message

  /\

  • receive(message, 1)
  • message.key = all
  • exists c: Command
    • message.body[0] = c

• S' = C

When the program receives a quit message, it terminates execution with a result code.

receiveQuit(C) ==

/\

• exists message: Message

  /\

  • receive(message, 1)
  • message.key = quit
  • exists i: Integer
    • message.body[0] = i

• S' = C

When the program receives an abort message, it terminates execution with an error message.

receiveAbort(C) ==

/\

• exists message: Message

  /\

  • receive(message, 1)
  • message.key = abort
  • exists string: String
    • message.body[0] = string

• S' = C

When the program receives the result corresponding to the wait/nwait message on the top of the wait stack, it can continue the suspended execution.

receiveResult(C) ==

/\

• exists message: Message

  /\

  • receive(message, 2)
  • message.key = result
  • waitDepth > 0
  • exists taskid: TaskId, exp: Expression

    /\

    • message.body[0] = taskid
    • message.body[1] = exp
    • exists i: Integer
      • waitStack[waitDepth-1].body[i] = taskid

  • waitDepth' = waitDepth-1

• S' = C