Verification of Concurrent Machine Code Running on a Single-Core Machine

In this paper, we propose a machine-independent logic to verify concurrent machine code running on a single-core machine, using a combination of separation logic and rely/guarantee reasoning. Separation logic is employed to reason about local resources, and rely/guarantee reasoning is used to analyze the shared state. We formalize and prove the soundness of this logic. To illustrate the applicability of the logic in realistic platforms, we instantiate it with ARMv7 architecture and apply the instantiated logic to verify a UART driver in the presence of interrupts.