Authors
Xinyu Feng
Zhong Shao
Alexander Vaynberg
Sen Xiang
Zhaozhong Ni
Abstract
Runtime stacks are critical components of any modern software---they
are used to implement powerful control structures such as function
call/return, stack cutting and unwinding, coroutines, and thread
context switch. Stack operations, however, are very hard to reason
about: there are no known formal specifications for certifying C-style
setjmp/longjmp, stack cutting and unwinding, or weak
continuations (in C--). In many proof-carrying code (PCC) systems,
return code pointers and exception handlers are treated
as general first-class functions (as in continuation-passing style)
even though both should have more limited scopes.
In this paper we show that stack-based control abstractions follow a
much simpler pattern than general first-class code pointers. We
present a simple but flexible Hoare-style framework for modular
verification of assembly code with all kinds of stack-based control
abstractions, including function call/return, tail call,
setjmp/longjmp, weak continuation, stack cutting, stack
unwinding, multi-return function call, coroutines, and thread context
switch. Instead of presenting a specific logic for each control
structure, we develop all reasoning systems as instances of a generic
framework. This allows program modules and their proofs developed in
different PCC systems to be linked together. Our system is fully
mechanized. We give the complete soundness proof and a full
verification of several examples in the Coq proof assistant.
Published