2012/08/12 by Maxim Strygin, Hayo Thielecke
Computer Science · #Concurrency #Distributed systems and fault tolerance #Exception handling #Formal Methods in Verification #Inter-process communication #Interleaving #Logic, programming, and type systems #Operational semantics #Process (computing) #SIGNAL (programming language) #Semantics (computer science) #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.89.11
published as EPTCS 89, 2012, pp. 149-163 · In Proceedings EXPRESS/SOS 2012, arXiv:1208.2440
openalex publication_date 2012/08/12 · arxiv created 2012/08/14 · arxiv updated 2012/08/15 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
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.