Abstract
We show how to derive a static instruction scheduler from a formal specification of an instruction-level parallel processor. The mathematical formalism used is SCCS, a synchronous process algebra for specifying timed, concurrent systems. We illustrate the technique by specifying a hypothetical processor that shares many properties of commercial processors (such as the MIPS or SuperSparc) including delayed loads and branches, interlocked floating-point instructions, resource constraints, and multiple instruction issue.
We derive parameters necessary for instruction scheduling by developing algorithms that operate on the labeled transition systems generated by the operational semantics of SCCS. From the labeled transition system we also employ a modal logic, the modal μ-calculus to determine whether there are any illegal instruction sequences or instruction sequences that could be executed in parallel.
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
Alfred V. Aho, Mahadevan Ganapathi, and Steven W.K. Tjiang. Code generation using tree matching and dynamic programming. ACM Transactions on Programming Languages and Systems, 11(4):491–516, October 1989.
David Bradlee, Robert Henry, and Susan Eggers. The Marion system for retargetable instruction scheduling. In ACM SIGPLAN '91 Conference on Programming Language Design and Implementation, pages 229–240. ACM, June 1991.
Todd A. Cook, Paul D. Franzon, Ed A. Harcourt, and Thomas K. Miller. System-level specification of instruction sets. In ICCD 93, Proceedings of the International Conference on Computer Design, 1993.
Todd A. Cook and Ed Harcourt. A functional specification language for instruction set architectures. In ICCL: Proceedings of the International Conference on Computer Languages, 1994.
Rance Cleaveland, Joachim Parrow, and Bernhard Steffen. The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, January 1993.
Juanito Camilleri and Glynn Winskel. CCS with priority choice. In LICS 91: IEEE Symposium on Logic in Computer Science, pages 246–255, 1991.
Jack W. Davidson. A retargetable instruction reorganizer. In Proceedings of the SIGPLAN '86 Symposium on Compiler Construction, pages 234–241, 1986.
Christopher W. Fraser. A language for writing code generators. In ACM SIGPLAN '89 Conference on Programming Language Design and Implementation, pages 238–245, 1989.
Robert Giegerich. On the structure of verifiable code generator specifications. In ACM SIGPLAN '90 Conference on Programming Language Design and Implementation, pages 1–8, 1990.
Ed Harcourt, Jon Mauney, and Todd Cook. Specification of instruction-level parallelism. In Proceedings of NAPAW'93, the North American Process Algebra Workshop, 1993.
Ed Harcourt, Jon Mauney, and Todd Cook. Formal specification and simulation of instruction-level parallelism. In Proceedings of the 1994 European Design Automation Conference.IEEE Computer Society Press, 1994.
Ed Harcourt, Jon Mauney, and Todd Cook. Functional specification and simulation of instruction set architectures. In Proceedings of the International Conference on Simulation and Hardware Description Languages. SCS Press, 1994.
Gerry Kane and Joe Heinrich. MIPS RISC Architecture. Prentice Hall, 1992.
Robin Milner. Calculi for synchrony and asynchrony. Journal of Theoretical Computer Science, 25:267–310, 1983.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Todd Proebsting and Chris Fraser. Detecting pipeline structural hazards quickly. In POPL'94, Proceedings of the 21st annual symposium on principles of programming languages, 1994.
Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harcourt, E., Mauney, J., Cook, T. (1994). From processor timing specifications to static instruction scheduling. In: Le Charlier, B. (eds) Static Analysis. SAS 1994. Lecture Notes in Computer Science, vol 864. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58485-4_36
Download citation
DOI: https://doi.org/10.1007/3-540-58485-4_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58485-8
Online ISBN: 978-3-540-49005-0
eBook Packages: Springer Book Archive