Compilers maintain resource-based program logic through compilation
Preserving Separation Logic Specifications through Compilation
Programming Languages
Summary
When computer programs are turned into machine code, their detailed rules about how they use resources can be lost, making it hard to check if they still behave correctly. The authors show a way to keep these rules intact during the translation, so that the program’s resource ownership can still be reasoned about after compiling. They develop a mathematical method to track resources precisely and prove it works, even when programs are broken into separate pieces and linked. This helps ensure that verified source code remains trustworthy as compiled machine code.
What this means in practice
- •For program verification engineers: Verify that resource usage properties in source code remain correct after compiling and linking modules in low-level code.
- •For systems programmers: Build compilers that preserve ownership and resource assertions from high-level code to assembly-like targets, improving reliability.
Authors
Carmine Abate, Kleio Liotati, František Farka, Sebastian Ertel
Abstract
Program specifications in separation logic describe ownership of resources and serve as logical interfaces for local reasoning. Compiler correctness, expressed as semantics preservation, does not by itself supply such an interface for compiled code, because it does not explicitly relate source and target resources and assertions. We investigate WP-preserving compilation: when a compiler translates a source program, the weakest preconditions that the program satisfies in a separation logic carry over to the compiled program. Our proof technique consists of a resource-aware simulation over interaction trees: it relates the resources required by corresponding source and target events, and tracks ownership through target operations, such as register accesses, that have no source counterpart. We apply the approach to a compiler from a structured imperative language to an assembly-like language, first for closed programs and then extended with modules and function calls. In the extended setting, each module can be verified in the source logic and compiled separately; its specifications carry over to the compiled module and are preserved when compiled modules are linked. All results are mechanized in Rocq.