Operational semantics for signal handling
Maxim Strygin (School of Computer Science University of Birmingham),, Hayo Thielecke (School of Computer Science University of Birmingham)

TL;DR
This paper explores formal operational semantics for Unix signal handling, comparing approaches and integrating exception handling to accurately model complex interactions in a clear, big-step style framework.
Contribution
It introduces a big-step operational semantics for signal handling and integrates exception handling, providing a formal basis for understanding signal and exception interactions.
Findings
Big-step semantics effectively model signal handling.
Exception handling can be integrated into signal semantics.
The approach clarifies complex interactions between signals and exceptions.
Abstract
Signals are a lightweight form of interprocess communication in Unix. When a process receives a signal, the control flow is interrupted and a previously installed signal handler is run. Signal handling is reminiscent both of exception handling and concurrent interleaving of processes. In this paper, we investigate different approaches to formalizing signal handling in operational semantics, and compare them in a series of examples. We find the big-step style of operational semantics to be well suited to modelling signal handling. We integrate exception handling with our big-step semantics of signal handling, by adopting the exception convention as defined in the Definition of Standard ML. The semantics needs to capture the complex interactions between signal handling and exception handling.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
