Mailbox Actors

3.4. System-Level Operations🔗

MailboxActors.OpStep defines the system-level transition relation, labelled by MailboxActors.OpLabel. Six rules cover the full lifecycle:

  • S-Node (sNode) — create a new empty node.

  • S-Clean (sClean) — remove a terminated processing engine. Per Remark 4.4 of the paper, the paired mailbox engine persists so that in-flight messages are not orphaned.

  • M-Send (mSend) — route a message into transit, targeting the recipient's mailbox (not the processing engine directly).

  • M-Enqueue (mEnqueue) — deliver an in-transit message to a ready mailbox engine, transitioning it from ready f to busy w.

  • S-SpawnWithMailbox (sSpawnMbox) — spawn a processing engine paired with its dedicated mailbox in a single atomic step.

  • M-Dequeue (mDequeue) — transfer a message from a mailbox engine to its paired processing engine, transitioning the processing engine from ready f to busy v.