Search papers, labs, and topics across Lattice.
This paper introduces a hybrid approach combining small-step and big-step semantics for verified compiler development, enabling the verification of both local and structural transformations like loop optimizations. They define an abstract behavioral semantics as an interface between the two semantic styles and extend coinductive big-step semantics to handle divergence, matching the expressiveness of small-step semantics. The approach is validated by implementing and verifying loop unswitching and full loop unrolling within the CompCert compiler using big-step Cminor.
Achieve verified loop optimizations by cleverly combining small-step and big-step semantics, enabling transformations like full loop unrolling within the CompCert compiler.
Verified compilers aim to guarantee that compilation preserves the observable behavior of source programs. While small-step semantics are widely used in such compilers, they are not always the most convenient framework for structural transformations such as loop optimizations. This paper proposes an approach that leverages both small-step and big-step semantics: small-step semantics are used for local transformations, while big-step semantics are employed for structural transformations. An abstract behavioral semantics is introduced as a common interface between the two styles. Coinductive big-step semantics is extended to correctly handle divergence with both finite and infinite traces, bringing it on par with the expressiveness of small-step semantics. This enables the insertion of big-step transformations into the middle of an existing small-step pipeline, thereby fully preserving all top-level semantic preservation theorems. This approach is practically demonstrated in CompCert by implementing and verifying a few new loop optimizations in big-step Cminor, including loop unswitching and, notably, full loop unrolling.
