Major compiler verification efforts, such as the CompCert project,
have traditionally simplified the verification problem by restricting
attention to the correctness of whole-program compilation, leaving
open the question of how to verify the correctness of separate
compilation.  Recently, a number of sophisticated techniques have been
proposed for proving more flexible, compositional notions of compiler
correctness, but these approaches tend to be quite heavyweight
compared to the simple "closed simulations" used in verifying
whole-program compilation.  Applying such techniques to a compiler
like CompCert, as Stewart et al. have done, involves major changes and
extensions to its original verification.

In this paper, we show that if we aim somewhat lower---to prove
correctness of separate compilation, but only for a *single*
compiler---we can drastically simplify the proof effort.  Toward this
end, we develop several lightweight techniques that recast the
compositional verification problem in terms of whole-program
compilation, thereby enabling us to largely reuse the
closed-simulation proofs from existing compiler verifications.  We
demonstrate the effectiveness of these techniques by applying them to
CompCert 2.4, converting its verification of whole-program compilation
into a verification of separate compilation in less than two
person-months.  This conversion only required a small number of
changes to the original proofs, and uncovered two compiler bugs along
the way.  The result is SepCompCert, the first verification of
separate compilation for the full CompCert compiler.









































%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-PDF-mode: t
%%% End: