Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-08T02:31:21.579Z Has data issue: false hasContentIssue false
  • English
  • Français

Maurer computers for pipelined instruction processing†

Published online by Cambridge University Press:  01 April 2008

J. A. BERGSTRA  and
C. A. MIDDELBURG
J. A. BERGSTRA
Affiliation:
Programming Research Group, University of Amsterdam, P.O. Box 41882, 1009 DB Amsterdam, the Netherlands and Department of Philosophy, Utrecht University, P.O. Box 80126, 3508 TC Utrecht, the Netherlands Email: J.A.Bergstra@uva.nl
C. A. MIDDELBURG
Affiliation:
Programming Research Group, University of Amsterdam, P.O. Box 41882, 1009 DB Amsterdam, the Netherlands Email: C.A.Middelburg@uva.nl
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We model micro-architectures with non-pipelined instruction processing and pipelined instruction processing using Maurer machines, basic thread algebra and program algebra. We show that stored programs are executed as intended with these micro-architectures. We believe that this work provides a new mathematical approach to the modelling of micro-architectures and the verification of their correctness and the anticipated speed-up results.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 18 , Issue 2 , April 2008 , pp. 373 - 409
Copyright
Copyright © Cambridge University Press 2008

References

Baeten, J. C. M. and Weijland, W. P. (1990) Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press.CrossRefGoogle Scholar
Bergstra, J. A. and Bethke, I. (2003) Polarized process algebra and program equivalence. In: Baeten, J. C. M., Lenstra, J. K., Parrow, J. and Woeginger, G. J. (eds.) Proceedings 30th ICALP. Springer-Verlag Lecture Notes in Computer Science 2719 1–21.CrossRefGoogle Scholar
Bergstra, J. A., Heering, J. and Klint, P. (1990) Module algebra. Journal of the ACM 37 (2)335–372.CrossRefGoogle Scholar
Bergstra, J. A. and Klop, J. W. (1984) Process algebra for synchronous communication. Information and Control 60 (1/3)109–137.CrossRefGoogle Scholar
Bergstra, J. A. and Loots, M. E. (2002) Program algebra for sequential code. Journal of Logic and Algebraic Programming 51 (2)125–156.CrossRefGoogle Scholar
Bergstra, J. A. and Middelburg, C. A. (2005) A thread algebra with multi-level strategic interleaving. In: Cooper, S. B., Löwe, B. and Torenvliet, L. (eds.) CiE 2005. Springer-Verlag Lecture Notes in Computer Science 3526 35–48.CrossRefGoogle Scholar
Bergstra, J. A. and Middelburg, C. A. (2006a) Splitting bisimulations and retrospective conditions. Information and Computation 204 (7)1083–1138.CrossRefGoogle Scholar
Bergstra, J. A. and Middelburg, C. A. (2006b) Thread algebra with multi-level strategies. Fundamenta Informaticae 71 (2/3)153–182.Google Scholar
Bergstra, J. A. and Middelburg, C. A. (2007a) {Maurer} computers with single-thread control. Fundamenta Informaticae 80 (4)333–362.Google Scholar
Bergstra, J. A. and Middelburg, C. A. (2007b) Simulating Turing machines on Maurer machines. Journal of Applied Logic, doi:10.1016/j.jal.2007.04.001.CrossRefGoogle Scholar
Bergstra, J. A. and Middelburg, C. A. (2007c) Thread algebra for strategic interleaving. Formal Aspects of Computing 19 (4)445–474.CrossRefGoogle Scholar
Bergstra, J. A. and Ponse, A. (2002) Combining programs and state machines. Journal of Logic and Algebraic Programming 51 (2)175–192.CrossRefGoogle Scholar
Bolychevsky, A., Jesshope, C. R. and Muchnick, V. (1996) Dynamic scheduling in {RISC} architectures. IEE Proceedings Computers and Digital Techniques 143 (5) 309–317.CrossRefGoogle Scholar
Brookes, S. D., Hoare, C. A. R. and Roscoe, A. W. (1984) A theory of communicating sequential processes. Journal of the ACM 31 (3)560–599.CrossRefGoogle Scholar
Fox, A. J. C. (1998) Algebraic Representation of Advanced Microprocessors, Ph.D. thesis, Department of Computer Science, Swansea University.Google Scholar
Fox, A. J. C. and Harman, N. A. (2003) Algebraic models of correctness for abstract pipelines. Journal of Logic and Algebraic Programming 57 (1/2)71–107.CrossRefGoogle Scholar
Harman, N. A. and Tucker, J. V. (1996) Algebraic models of microprocessors: Architecture and organisation. Acta Informatica 33 421–456.CrossRefGoogle Scholar
Hehner, E. C. R., Gupta, L. E. and Malton, A. J. (1986) Predicative methodology. Acta Informatica 23 487–505.CrossRefGoogle Scholar
Hennessy, J. L. and Patterson, D. A. (2003) Computer Architecture: A Quantitative Approach, third edition, Morgan Kaufmann.Google Scholar
Hoare, C. A. R. (1985) Communicating Sequential Processes, Prentice-Hall.Google Scholar
Hoe, J. C. and Arvind, (2004) Operation-centric hardware description and synthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 23 (9)1277–1288.CrossRefGoogle Scholar
Hopcroft, J. E., Motwani, R. and Ullman, J. D. (2001) Introduction to Automata Theory, Languages and Computation, second edition, Addison-Wesley.Google Scholar
Jesshope, C. R. and Luo, B. (2000) Micro-threading: A new approach to future RISC. In: ACAC 2000, IEEE Computer Society Press 34–41.Google Scholar
Maurer, W. D. (1966) A theory of computer instructions. Journal of the ACM 13 (2)226–235.CrossRefGoogle Scholar
Maurer, W. D. (2006) A theory of computer instructions. Science of Computer Programming 60 244–273.CrossRefGoogle Scholar
Milner, R. (1980) A Calculus of Communicating Systems. Springer-Verlag Lecture Notes in Computer Science 92.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency, Prentice-Hall.Google Scholar
Ponse, A. (2002) Program algebra with unit instruction operators. Journal of Logic and Algebraic Programming 51 (2)157–174.CrossRefGoogle Scholar
Sima, D. (2004) Decisive aspects in the evolution of microprocessors. Proceedings of the IEEE 92 (12) 1896–1926.CrossRefGoogle Scholar
Thornton, J. (1970) Design of a Computer – The Control Data 6600, Scott, Foresman and Co.Google Scholar