A semantics of Core Erlang with handling of signals
summary
A formal small-step semantics for a subset of Core Erlang models asynchronous outbox of signals and both monitor vs symmetric links, including concrete signal tuples, EOP/ended termination values, and two transition levels (terminal and auxiliary). It proves message-order guarantees: per-sender FIFO preserved, inter-sender order nondeterministic, and a down signal rule that deletes the signal and appends a corresponding message to the recipient’s mailbox. An executable model is being implemented for future causal debugging; mechanization/proofs are not yet provided.
AI-written summary · about
chapters (10)
- 0:00Core Erlang semantics with signals
- 1:29Design choices and system model
- 3:37Process state representation
- 7:36Example: process behavior
- 9:46Semantics rules and transitions
- 13:02Evaluating child process expressions
- 15:11Process termination and signals
- 16:38Handling down signals
- 18:28Contributions and future work
- 18:51Q&A