CTL
10 July 2013 - 14h00
Certification of an Instruction Set Simulator (Phd Defense)
by Xiaomu Shi from VERIMAG UJF
Abstract: This thesis introduces the work of certifying a part of a C/C++ program called SimSoC (Simulation of System on Chip), which simulates the behavior of architectures based on a processor such as ARM, PowerPC, MIPS or SH4. Such a simulator can be used for software development of a specific embedded system, to shorten the development and test phases, especially when, as is the case for SimSoC, it offers a realistic simulation speed (about 100 Millions of instructions per second per individual core).
SimSoC is a complex software, including about 60,000 lines of C++ code, many complex features from SystemC library, and optimizations to achieve high simulation speed. The subset of SimSoC dedicated to the ARM processor, one of the most popu- lar processor design, somehow translates in C++ the contents of the ARM reference manual, which is
1138 pages long. Mistakes are then unavoidable for such a complex application. Indeed, some bugs were observed even after the previous version of SimSoC, for ARMv5, was able to boot linux.
Then a critical issue is : does the simulator actually simulate the real hardware ? In our work, we aim at proving a significant part of the correctness of SimSoC in order to support the claim that the implementation of the simulator and the real system will exhibit the same behavior. Then a SimSoC user can trust the simulator, especially in very critical uses.
We focused our efforts on a critical part of SimSoC : the instruction set simulator of the ARMv6 architecture, which is considered in the current version of SimSoC.
Approaches based on axiomatic semantics (typically, Hoare logic) are the most popular for proving the correctness of imperative programs. However, we prefered to try a less usual but more direct approach, based on operational semantics : this was made possible in theory since the development of an operational semantics for the C language formalized in Coq in the CompCert project, and allowed us to use the comfortable logic of Coq, of much help for managing the complexity of the specification. Up to our knowledge, this is the first development of formal correctness proofs based on operational
semantics, at least at this scale.
We provide a formalized representation of the ARM instruction set and addressing modes in Coq, using an automatic code generator from the instruction pseudo-code in the ARM reference manual. We also generate a Coq representation of a corresponding simulator in C, called Simlight, using the abstract syntax defined in CompCert.
From these two Coq representations, we can then state and prove the correctness of Simlight, using the operational semantics of C provided by CompCert. Currently, proofs are available for at least one instruction in each category of the ARM instruction set.
During this work, we improved the technology available in Coq for performing inversions, a kind of proof steps which heavily occurs in our setting.
Jury :
- Yves Bertot
- Sandrine Blazy, rapporteur
- Vania Joloboff, co-directeur
- Xavier Leroy
- Laurent Maillet-Contoz
- Claude Marché, rapporteur
- Jean-François Monin, directeur
- Frédéric Rousseau
