Semantics and logics for signals

Strygin, Maxim (2014). Semantics and logics for signals. University of Birmingham. Ph.D.


Download (1MB)


In operating systems such as Unix, processes can interact via signals. Signal handling resembles both exception handling and concurrent interleaving of processes. The handlers can be installed dynamically by the main program, but signals arrive non-deterministically; therefore, a handler may interrupt a program at any point. However, the interleaving of actions is not symmetric, in that the handler interrupts the main program, but not conversely. This thesis presents operational semantics and program logic for an idealized form of signal handling. To make signal handling logically tractable, we define handling to be block-structured. To reason about the interleaving of signal handlers, we adopt the idea of binary relations on states from rely-guarantee logics, imposing rely conditions on handlers. Given the one-way interleaving of signal handlers, the logic is less symmetric than rely-guarantee. We combine signal and exception handlers in the same language to investigate their interactions, specifically whether a handler can run more than once or is linearly used. We prove soundness of the program logic relative to a big-step operational semantics for signal handling. Then, we introduce and discuss reentrancy in various domains. Finally, we present our work towards logic with Reentrancy Linear Type System.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: Other
Other Funders: The University of Birmingham
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science


Request a Correction Request a Correction
View Item View Item


Downloads per month over past year