Formally verifying exceptions for low-level code with separation logic

Exceptions in low-level architectures are implemented as synchronous interrupts: upon the execution of a faulty instruction the processor jumps to a piece of code that handles the error. Previous work has shown that assembly programs can be written, verified and run using higher-order separation logic [14]. However, execution of faulty instructions is then specified as either being undefined or terminating with an error. In this paper, we study synchronous interrupts and show their usefulness by implementing a memory allocator. This shows that it is indeed possible to write positive specifications of programs that fault. All of our results are mechanised in the interactive proof assistant Coq.