Abstract
This chapter presents the SimSoC virtual prototyping framework, a full system simulation framework, based on SystemC and Transaction Level Modeling. SimSoC takes as input a binary executable file, which can be a full operating system, and simulates the behavior of the target hardware on the host system. It is using internally dynamic binary translation from target code to host code to simulate the application software. A potential issue with simulators is that they might not accurately simulate the real hardware. We aimed at filling this gap by proving that the ARM instruction set simulator coded in C is a high fidelity implementation of the ARM architecture, using the Coq theorem prover, and starting from a formal architectural model in Coq. The first part of the chapter presents the general architecture and features of SimSoC. The second part describes the proof of the ARM simulator.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Note that this problem is the same as for the work done by Cambridge University.
References
J. Alglave, A. Fox, S. Ishtiaq, M.O. Myreen, S. Sarkar, P. Sewell, F.Z. Nardelli, The semantics of power and ARM multiprocessor machine code. In DAMP’09 (ACM, New York, NY, USA, 2008), pp. 13–24
V. Bala, E. Duesterwald, S. Banerjia, Dynamo: a transparent dynamic optimization system. SIGPLAN Not. 35 (5), 1–12 (2000)
F. Bellard, Qemu, a fast and portable dynamic translator. In ATEC ’05: Proceedings of the Annual Conference on USENIX Annual Technical Conference (USENIX Association, Berkeley, CA, USA, 2005), pp. 41–41
Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science (Springer, New York, 2004)
F. Bobot, J.C. Filliâtre, C. Marché, A. Paskevich, Why3: Shepherd your herd of provers. Boogie 2011, 53–64 (2011)
D. Burger, T.M. Austin, The simplescalar tool set, version 2.0. SIGARCH Comput. Archit. News 25 (3), 13–25 (1997)
B. Campbell, An executable semantics for Compcert C. In Certified Programs and Proofs (Springer, New York, 2012), pp. 60–75
G. Canet, P. Cuoq, B. Monate, A value analysis for C programs. In SCAM’09 (IEEE, Los Alamitos, 2009), pp. 123–124
B. Cmelik, D. Keppel, Shade: A fast instruction-set simulator for execution profiling. In SIGMETRICS ’94: Proceedings of the 1994 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems (ACM, New York, NY, USA, 1994), pp. 128–137
Coq Development Team, The Coq Reference Manual, Version 8.2. INRIA Rocquencourt, France, 2008. http://coq.inria.fr/
J.-C. Filliâtre, C. Marché, The Why/Krakatoa/Caduceus platform for deductive program verification. In Proceedings of the 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science 4590, 2007. http://why.lri.fr/
A.C.J. Fox, M.O. Myreen, A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In ITP, pp. 243–258, 2010
Y. Futamura, Partial evaluation of computation process—an approach to a compiler-compiler. Higher Order Symb. Comput. 12 (4), 381–391 (1999)
F. Ghenassia (ed.), Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems (Springer, New York, 2005). ISBN 0-387-26232-6
G. Hamerly, E. Perelman, B. Calder, How to use simpoint to pick simulation points. SIGMETRICS Perform. Eval. Rev. 31 (4), 25–30 (2004)
C. Helmstetter, V. Joloboff, SimSoC: A SystemC TLM integrated ISS for full system simulation. In IEEE Asia Pacific Conference on Circuits and Systems - APCCAS’08, November 2008. http://formes.asia/cms/software/simsoc
H. Hongwei, S. Jiajia, C. Helmstetter, V. Joloboff, Generation of executable representation for processor simulation with dynamic translation. In Proceedings of the International Conference on Computer Science and Software Engineering (IEEE, Wuhan, China, 2008)
IEEE, Open SystemC Language Reference Manual, 2011. http://standards.ieee.org/getieee/1666/download/1666-2011.pdf
V. Joloboff, X. Zhou, C. Helmstetter, X. Gao, Fast Instruction Set Simulation Using LLVM-based Dynamic Translation. In International MultiConference of Engineers and Computer Scientists 2011, vol. 2188, IAENG (Springer, Hong Kong, China, 2011), pp. 212–216
D. Jones, N. Topham, High speed cpu simulation using ltu dynamic binary translation. In Proceedings of the 4th International Conference on High Performance Embedded Architectures and Compilers, HiPEAC ’09 (Springer, Berlin, Heidelberg, 2009), pp. 50–64
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood, sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP ’09 (ACM, New York, NY, USA, 2009), pp. 207–220
C. Lattner, V. Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO’04), Palo Alto, California, Mar 2004
X. Leroy, Formal verification of a realistic compiler. Commun. ACM 52 (7), 107–115 (2009)
X. Leroy, The CompCert C verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt, March 2012. http://creativecommons.org/licenses/by-nc-sa/3.0/
W. Liu, M.C. Huang, Expert: expedited simulation exploiting program behavior repetition. In Proceedings of the 18th Annual International Conference on Supercomputing, ICS ’04 (ACM, New York, NY, USA, 2004), pp. 126–135
J.-F. Monin, X. Shi, Handcrafted inversions made operational on operational semantics. In ITP 2013 vol. 7998 of LNCS, ed. by S. Blazy, C. Paulin, D. Pichardie (Springer, Rennes, France, 2013), pp. 338–353
A. Nohl, G. Braun, O. Schliebusch, R. Leupers, H. Meyr, A. Hoffmann, A universal technique for fast and flexible instruction-set architecture simulation. In DAC ’02: Proceedings of the 39th Conference on Design Automation, DAC ’02 (ACM, New York, NY, USA, 2002), pp. 22–27
Open SystemC Initiative, OSCI SystemC TLM 2.0 User Manual, 2008. http://www.systemc.org/
C. Pusch, Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In TACAS’99 (Springer, New York, 1999), pp. 89–103
W. Qin, J. D’Errico, X. Zhu, A multiprocessing approach to accelerate retargetable and portable dynamic-compiled instruction-set simulation. In CODES+ISSS’06 (ACM, New York, NY, USA, 2006), pp. 193–198
M. Reshadi, P. Mishra, N. Dutt, Instruction set compiled simulation: a technique for fast and flexible instruction set simulation. In Design Automation Conference, 2003. Proceedings, pp. 758–763, 2003
K. Scott, N. Kumar, S. Velusamy, B. Childers, J.W. Davidson, M.L. Soffa, Retargetable and reconfigurable software dynamic translation. In Proceedings of the International Symposium on Code Generation and Optimization (CGO’03), 2003
D. Seal, ARM Architecture Reference Manual (Addison-Wesley Longman Publishing, Boston, 2000)
H. Shi, Y. Wang, H. Guan, A. Liang, An intermediate language level optimization framework for dynamic binary translation. SIGPLAN Not. 42 (5), 3–9 (2007)
E. Witchel, M. Rosenblum, Embra: fast and flexible machine simulation. In SIGMETRICS ’96: Proceedings of the 1996 ACM SIGMETRICS International Conference on Measurement and Modeling of Computer Systems (ACM, New York, NY, USA, 1996), pp. 68–79
R.E. Wunderlich, T.F. Wenisch, B. Falsafi, J.C. Hoe, Smarts: accelerating microarchitecture simulation via rigorous statistical sampling. In Proceedings. 30th Annual International Symposium on Computer Architecture, 2003, pp. 84–95, 2003
Z. Zhang, V. Joloboff, X. Zhou, C. Helmstetter, Fast dynamic translation using llvm on multi-core hosts. In 5th Workshop on Architectural and Microarchitectural Support for Binary Translation (AMAS-BT) (Intel Corporation, Portland, Oregon, USA, June 2012)
Acknowledgements
This work has been partly funded by the international collaboration support of France ANR and NSFC China in the SIVES project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Joloboff, V., Monin, JF., Shi, X. (2017). SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework. In: Molnos, A., Fabre, C. (eds) Model-Implementation Fidelity in Cyber Physical System Design. Springer, Cham. https://doi.org/10.1007/978-3-319-47307-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-47307-9_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47306-2
Online ISBN: 978-3-319-47307-9
eBook Packages: EngineeringEngineering (R0)