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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:633384 |
| Date | January 2014 |
| Creators | Strygin, Maxim |
| Publisher | University of Birmingham |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://etheses.bham.ac.uk//id/eprint/5530/ |
Page generated in 0.1287 seconds