Abstract
Much current work on modelling and verifying microprocessors can accommodate pipelined and superscalar processors. However, superscalar and pipelined processors are no longer state-of-the-art: Simultaneous Multithreaded (SMT) and Multi-core, or Chip-Level Multithreaded (CMT) microprocessors enable a single microprocessor implementation to present itself to the programmer as multiple (virtual in the case of SMT) processors with shared state. This paper builds on a series which has developed a hierarchy of many-sorted algebraic models, able to model a variety of processor types, at different levels of temporal and data abstraction. These models address both the behavioural definition of microprocessors, and also the question: what does it mean for a microprocessor implemenation to be correct? They also consider how the process of formal verification can be simplified by indentifying some easily-checked preconditions (the one-step theorems). We extend the existing algebraic tools for modeling microprocessors and their correctness to SMT and CMT. We outline how the one-step theorems for simplifying verification are modified for SMT and CMT processors. The particular problems that are addressed are: how to map multiple (possibly interacting) user-level SMT/CMT models to a single implementation? And how to accommodate the (unavoidable) presence of implementation level components in the user-level model?
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.: Instantiating uninterpreted functional unit and memory system: Functional verification of VAMP. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 51–65. Springer, Heidelberg (2003)
Burch, J., Dill, D.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003)
Cohn, A.: A proof of correctness of the VIPER microprocessor: the first levels. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification and Synthesis, pp. 27–72. Kluwer Academic Publishers, Dordrecht (1987)
Cyrluk, D., Rushby, J., Srivas, M.: Systematic formal verification of interpreters. In: IEE international conference on formal engineering methods ICFEM 1997, pp. 140–149 (1997)
Fox, A.C.J.: Algebraic Representation of Advanced Microprocessors. PhD thesis, Department of Computer Science, University of Wales Swansea (1998)
Fox, A.C.J: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003)
Fox, A.C.J.: An algebraic framework for verifying the correctness of hardware with input and output: a formalization in HOL. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 157–174. Springer, Heidelberg (2005)
Fox, A.C.J., Harman, N.A.: Algebraic models of superscalar microprocessor implementations: A case study. In: Möller, B., Tucker, J.V. (eds.) Prospects for Hardware Foundations. LNCS, vol. 1546, pp. 138–183. Springer, Heidelberg (1998)
Fox, A.C.J., Harman, N.A.: Algebraic models of correctness for abstract pipelines. The Journal of Algebraic and Logic Programming 57, 71–107 (2003)
Gordon, M.: Proving a computer correct with the LCF-LSM hardware verification system. Technical report, Technical Report No. 42, Computer Laboratory, University of Cambridge (1983)
Graham, B., Birtwistle, G.: Formalising the design of an SECD chip. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol. 408, pp. 40–66. Springer, Heidelberg (1990)
Harman, N.A: Algebraic models of simultaneous multi-threaded and chip-level multi-threaded microprocessors. Submitted to the Journal of Algebraic and Logic Programming (2007)
Harman, N.A: Modelling SMT and CMT processors: A simple case study. Technical Report CSR7-2007, University of Wales Swansea, Computer Science Department (2007), http://cs.swan.ac.uk/reports/yr2007/CSR7-2007.pdf
Harman, N.A., Tucker, J.V.: Algebraic models of microprocessors: Architecture and organisation. Acta Informatica 33, 421–456 (1996)
Harman, N.A., Tucker, J.V.: Algebraic models of microprocessors: the verification of a simple computer. In: Stavridou, V. (ed.) Proceedings of the 2nd IMA Conference on Mathematics for Dependable Systems, pp. 135–170 (1997)
Hosabettu, R., Gopalakrishnan, G., Srivas, M.: Formal verification of a complex pipelined processor. Formal Methods in System Design 23(2), 171–213 (2003)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1997)
Miller, S., Srivas, M.: Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods. In: Proceedings of WIFT 1995, Boca Raton (1995)
Ray, S., Hunt, W.A.: Deductive verification of pipelined machines using first-order quantification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 31–43. Springer, Heidelberg (2004)
Stephenson, K.: Algebraic specification of the Java virtual machine. In: Möller, B., Tucker, J.V. (eds.) Prospects for Hardware Foundations. LNCS, vol. 1546, Springer, Heidelberg (1998)
Windley, P.: A theory of generic intepreters. In: Milne, G.J., Pierre, L. (eds.) CHARME 1993. LNCS, vol. 683, pp. 122–134. Springer, Heidelberg (1993)
Windley, P., Burch, J.: Mechanically checking a lemma used in an automatic verification tool. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 362–376. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harman, N.A. (2007). Algebraic Models of Simultaneous Multithreaded and Multi-core Processors. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds) Algebra and Coalgebra in Computer Science. CALCO 2007. Lecture Notes in Computer Science, vol 4624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73859-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-73859-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73857-2
Online ISBN: 978-3-540-73859-6
eBook Packages: Computer ScienceComputer Science (R0)