Abstract
We present the highlights of an algorithm and correctness proof for compiling programs written in Joy, a simple parallel language, into delay-insensitive circuits. The proof relies heavily on techniques of structural operational semantics, many of which should generalize to similar settings.
Supported by NSF grants CCR-9003441 and CCR-9058180.
Supported by NSF grant CCR-9003441.
Supported by a NSF grant CCR-9058180
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic. North-Holland, 1981. Revised Edition, 1984.
H. Bisseling, H. Eemers, M. Kamps, and A. Peeters. Designing delay-insensitive circuits. Technical report, 1990.
B. Bloom. Partial traces and the semantics and logic of ccs-like languages. Technical Report 89–1066, Cornell, 1989.
B. Bloom. Ready Simulation, Bisimulation, and the Semantics of CCS-Like Languages. PhD thesis, Massachusetts Institute of Technology, Aug. 1989.
E. Brunvand and R. F. Sproull. Translating concurrent communicating programs into delay-insensitive circuits. Technical Report CMU-CS-89-126, Carnegie-Mellon University, 1989.
S. M. Burns and A. J. Martin. Syntax-directed translation of concurrent programs into self-timed circuits. In Advanced Research in VLSI: Proceedings of the 5th MIT Conference, pages 35–50, 1988.
W. A. Clark and C. E. Molnar. Macromodular computer systems. In B. Waxman and R. Stacey, editors, Biomedical Research Vol. IV, pages 45–85. Academic, New York.
D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1989.
J. Hyland. A syntactic characterization of the equality in some models of the λ-calculus. J. London Math. Soc, 2(12):361–370, 1976.
R. M. Keller. Towards a theory of universal speed-independent modules. IEEE Transactions on Computers, C-23(1):21–33, January 1974.
A. J. Martin. Compiling communicating processes into delay-insensitive VLSI circuits. Distributed Computing, 1:226–234, 1986.
G. J. Milne. The Correctness of a Simple Silicon Compiler., pages 1–12. North-Holland, 1983.
R. Milner. A modal characterisation of observable machine-behaviour. In E. Astesiano and C. Böhm, editors, CAAP '81: Trees in Algebra and Programming, 6th Colloquium, volume 112 of Lect. Notes in Computer Sci., pages 25–34. Springer-Verlag, 1981.
R. Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, New York, 1989.
C. E. Molnar, T.-P. Fang, and F. U. Rosenbeiger. Synthesis of delay-insensitive modules. In H. Fuchs, editor, Chapel Hill Conference on VLSI, pages 67–86, 1985.
D. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Theoretical Computer Science, Lect. Notes in Computer Sci., page 261. Springer-Verlag, 1981.
G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Computer Science Department, Denmark, 1981.
G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5(3):223–255, 1977.
R. Sproull and I. E. Sutherland. Asynchronous Systems. Sutherland, Sproull & Associates, 1986.
J. Staunstrup and M. Greenstreet. Atomicity, programs, and hardware. Technical Report ID-TR 198-46, Technical University of Denmark, 1990.
M. J. F. T. S. Anantharaman, E. M. Clarke and B. Mishra. Compiling path expressions into vlsi circuits. Distributed Computing, 1:150–166, 1986.
F. Vaandrager. On the relationship between process algebra and input/output automata. In Sixth annual IEEE symposium on Logic in Computer Science, pages 387–389. IEEE Computer Society Press, 1991.
C. H. K. van Berkel, C. Niessen, M. Rem, and R. W. Saeijs. VLSI programming and silicon compilation; a novel approach from philips research. In ICCD, 1988.
K. van Berkel. Handshake Circuits: an intermediary between communicating processes and VLSI. PhD thesis, Technische Universiteit Eindhoven, 1992.
C. Wadsworth. The relation between computational and denotational properties for Scott's D∞-models of the λ-calculus. SIAM J. Comput., 5:488–521, 1976.
S. Weber, B. Bloom, and G. Brown. Compiling Joy to silicon: A verified silicon compilation scheme. In T. Knight and J. Savage, editors, Proceedings of the Advanced Research in VLSI and Parallel Systems Conference, pages 79–98. 1992.
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Rice University, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weber, S., Bloom, B., Brown, G. (1993). Compiling joy into Silicon: An exercise in applied structural operational semantics. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Semantics: Foundations and Applications. REX 1992. Lecture Notes in Computer Science, vol 666. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56596-5_50
Download citation
DOI: https://doi.org/10.1007/3-540-56596-5_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56596-3
Online ISBN: 978-3-540-47595-8
eBook Packages: Springer Book Archive