Advertisement

Typing Assembly Programs with Explicit Forwarding

  • Lennart Beringer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)

Abstract

We consider processor architectures where communication of values is achieved through operand queues instead of registers. Explicit forwarding tags in an instruction’s code denote the source of its operands and the destination of its result. We give operational models for sequential and distributed execution, where no assumptions are made about the relative speed of functional units. We introduce type systems which ensure that programs use the forwarding mechanism in a coordinated way, ruling out various run time hazards. Deadlocks due to operand starvation, operand queue mismatches, non-determinism due to race conditions and deadlock due to the finite length of operand queues are eliminated. Types are based on the shape of operand queue configurations, abstracting from the value of an operand and from the order of items in operand queues. Extending ideas from the literature relating program fragments adjacent in the control flow graph, the type system is generalised to forwarding across basic blocks.

Keywords

Functional Unit Type System Basic Block Linear Logic Sequential Execution 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bowen Alpern, Mark N. Wegman, and F. Kenneth Zadeck. Detecting equality of variables in programs. In ACM, editor, POPL’ 88. Proceedings of the conference on Principles of programming languages,January 13-15,1988,San Diego,CA, pages 1–11, New York, NY, USA, 1988. ACM Press.Google Scholar
  2. 2.
    Andrew W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, Cambridge, UK, 1998.Google Scholar
  3. 3.
    Arvind and Xiaowei W. Shen. Using term rewriting systems to design and verify processors. IEEE Micro, 19(3):36–46, May/June 1999.CrossRefGoogle Scholar
  4. 4.
    D.K. Arvind and Robert D. Mullins. A Fully Asynchronous Superscalar Processor. In Proceedings of the International Conference on Parallel Architectures and Compilation Techniques (PACT), 1999.Google Scholar
  5. 5.
    William Coates, Jon Lexau, Ian Jones, Scott Fairbanks, and Ivan Sutherland. FLEETzero: An Asynchronous Switching Experiment. In Proceedings of the Seventh International Symposium on Advanced Research in Asynchronous Circuits and Systems, Salt Lake City, March 2001.Google Scholar
  6. 6.
    Henk Corporaal and Hans Mulder. MOVE: A framework for high-performance processor design. In Anne Copeland MacCallum, editor, Proceedings of the 4th Annual Conference on Supercomputing, pages 692–701, Alburquerque, NM, USA, November 1991. IEEE Computer Society Press.Google Scholar
  7. 7.
    Karl Crary and Greg Morrisett. Type structure for low-level programming languages. Lecture Notes in Computer Science, 1644:40–--, 1999.Google Scholar
  8. 8.
    Werner Damm and Amir Pnueli. Verifying out-of-order executions. In Hon F. Li and David K. Probst, editors, Advances in Hardware Design and Verification: IFIP WG10.5 International Conference on Correct Hardware Design and Verification Methods (CHARME), pages 23–47, Montreal, Canada, October 1997. Chapman & Hall.Google Scholar
  9. 9.
    Philip B. Endecott. SCALP: A Superscalar Asynchronous Low-Power Processor. PhD thesis, Department of Computer Science, University of Manchester, February 1996.Google Scholar
  10. 10.
    Uffe H. Engberg and Glynn Winskel. Linear logic on Petrinets. Technical Report RS-94-3, BRICS, Aarhus, Denmark, 1994.Google Scholar
  11. 11.
    Michael J. Flynn. Computer Architecture: Pipelined and Parallel Processor Design. Jones & Bartlett Publishing, 1995.Google Scholar
  12. 12.
    Stephen N. Freund and John C. Mitchell. A type system for object initialization in the javatm bytecode language. In Proceedings of the 13th Conference on Object-Oriented Programming,Systems,L anguages,and Applications (OOPSLA-98), volume 33, 10 of ACM SIGPLAN Notices, New York, 1998. ACM Press.Google Scholar
  13. 13.
    Stephen N. Freund and John C. Mitchell. A formal framework for the Java bytecode language and verifier. In Proceedings of the Conference on Object-Oriented Programming,Systems,L anguages,and Applications, pages 147–166, 1999.Google Scholar
  14. 14.
    J. D. Garside, S. B. Furber, and S.-H. Chung. AMULET3 revealed. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 51–59, April 1999.Google Scholar
  15. 15.
    D. A. Gilbert and J. D. Garside. A result forwarding mechanism for asynchronous pipelined systems. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 2–11. IEEE Computer Society Press, April 1997.Google Scholar
  16. 16.
    Jean-Yves Girard. Linear logic. Theoretical Computer Science, 46:1–102, 1986.CrossRefMathSciNetGoogle Scholar
  17. 17.
    John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, second edition, 1996.zbMATHGoogle Scholar
  18. 18.
    Martin Hofmann. A type system for bounded space and functional in-place update. In Proceedings of the European Symposium on Programming (ESOP), Berlin, 2000.Google Scholar
  19. 19.
    Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. In Nicolas Halbwachs and Doron Peled, editors, Computer-Aided Verification,CA V’ 99, volume 1633 of Lecture Notes in Computer Science, pages 47–59, Trento, Italy, July 1999. Springer-Verlag.CrossRefGoogle Scholar
  20. 20.
    Shin-ya Katsumata and Atsushi Ohori. Proof-Directed De-compilation of Low-Level Code. In Proceedings of the European Symposium on Programming (ESOP), Genova, 2001.Google Scholar
  21. 21.
    Naoki Kobayashi. Quasi-linear types. In Proceedings of the 26th Symposium on Principles of Programming Languages POPL’99, ACM SIGPLAN Notices, New York, NY, USA, 1999. ACM Press.Google Scholar
  22. 22.
    Alain J. Martin, Andrew Lines, Rajit Manohar, Mika Nystroem, Paul Penzes, Robert Southworth, and Uri Cummings. The design of an asynchronous MIPS R3000 microprocessor. In Advanced Research in VLSI, pages 164–181, September 1997.Google Scholar
  23. 23.
    Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. Lecture Notes in Computer Science, 1473:28–--, 1998.Google Scholar
  24. 24.
    Peter D. Mosses. Semantics, Modularity, and Rewriting Logic. Electronic Notes in Theoretical Computer Science, 15, 1998.Google Scholar
  25. 25.
    Jon Mountjoy, Pieter Hartel, and Henk Corporaal. Modular Operational Semantic Specification of Transport Triggered Architectures. In Proc. 13th IFIP WG 10.5 Conf. on Computer Hardware Description Languages and Their Applications, pages 260–279, Toledo, Spain, April 1997. Chapman and Hall, London.Google Scholar
  26. 26.
    Atsushi Ohori. The logical abstract machine: A curry-howard isomorphism for machine code. In Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming (FLOPS’99), Lecture Notes in Computer Science, LNCS 1722, pages 300–318. Springer, 1999.Google Scholar
  27. 27.
    Gordon Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, University of Aarhus, September 1981.Google Scholar
  28. 28.
    Wolfgang Reisig and Grzegorz Rozenberg. Lectures on Petri Nets I: Basic Models. Lecture Notes in Computer Science 1491. Springer, 1998.zbMATHGoogle Scholar
  29. 29.
    Raymie Stata and Mart’?n Abadi. A type system for Java bytecode subroutines. In Proceedings of the 25th Symposium on Principles of Programming Languages POPL’98, pages 149–160. ACM Press, 1998.Google Scholar
  30. 30.
    R. M. Tomasulo. An efficient algorithm for exploiting multiple arithmitic units. IBM Journal of research and development, 11:25–33, January 1967.zbMATHCrossRefGoogle Scholar
  31. 31.
    David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In 7’th International Conference on Functional Programming and Computer Architecture, pages 1–11, La Jolla, California, June 1995. ACM Press.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Lennart Beringer
    • 1
  1. 1.Laboratory for Foundations of Computer Science, Division of InformaticsThe University of EdinburghEdinburghUK

Personalised recommendations