Abstract
This paper extends previous work in compiler derivation and verification to languages with true-concurrency semantics. We extend the λ-calculus to model process-centered concurrent computation, and give the semantics of a small language in terms of this calculus. We then define a target abstract machine whose states have denotations in the same calculus. We prove the correctness of a compiler for our language: the denotation of the compiled code is shown to be strongly bisimilar to the denotation of the source program, and the abstract machine running the compiled code is shown to be branching-bisimilar to the source program's denotation.
Work supported by the National Science Foundation under grant numbers CCR-901463 and CCR-9304144.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. M. Amadio. Translating core Facile. Technical Report ECRC-1994-3, ECRC, Feb. 1994.
P. America, J. de Bakker, J. N. Kok, and J. Rutten. Operational semantics of a parallel object-oriented language. In Conf. Rec. 13th ACM Symposium on Principles of Programming Languages, pages 194–208, 1986.
A. W. Appel. Compiling with Continuations. Cambridge University Press, Cambridge, 1992.
J. Armstrong, R. Virding, and M. Williams. Concurrent Programming in Erlang. Prentice Hall, 1993.
J. S. Auerbach et al. Concurrent/C Tutorial and User's Guide: An Introduction to a Language for Distributed C Programming. IBM T. J. Watson Research Center, June 1994.
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1984.
B. Bloom. Chocolate: Calculi of higher order communication and lambda terms. In Conf. Rec. 21st ACM Symposium on Principles of Programming Languages, pages 339–347, 1994.
N. Carriero and D. Gelernter. How to Write Parallel Programs: A First Course. MIT Press, 1990.
W. Clinger. The Scheme 311 compiler: An exercise in denotational semantics. In Proc. 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, Aug. 1984.
A. Geist et al. PVM 3 User's Guide and Reference Manual. Oak Ridge National Laboratory, May 1993.
A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming, 18(2):121–160, 1989.
A. Giacalone, P. Mishra, and S. Prasad. Operational and algebraic semantics for facile: A symmetric integration of concurrent and functional programming. In Proc. ICALP '90, volume 443 of Lecture Notes in Computer Science, pages 765–7780, Berlin, Heidelberg, and New York, 1990. Springer-Verlag.
D. Gladstein. Compiler Correctness for Concurrent Languages. PhD thesis, Northeastern University, Dec. 1994. Available via anonymous ftp from ftp.ccs.neu.edu as /pub/people/daveg/thesis.ps.Z.
R. Gorrieri and C. Laneve. Split and ST bisimulation semantics. Information and Computation, 118:272–288, 1995.
J. D. Guttman, V. Swarup, and J. Ramsdell. The VLISP verified scheme system. Lisp and Symbolic Computation, 8(1/2), 1995.
M. Hennessy. Axiomatising finite concurrent processes. SIAM Journal of Computation, 15(5):997–1017, 1995.
C. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985.
R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2:119–141, 1992.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (parts i and ii). Information and Computation, 100:1–77, 1992.
F. Nielson and H. R. Nielson. From CML to process algebras. In Proceesings of CONCUR '93, pages 493–508, Berlin, Heidelberg, and New York, 1993. Springer-Verlag.
D. P. Oliva, J. D. Ramsdell, and M. Wand. The VLISP verified PreScheme compiler. Lisp and Symbolic Computation, 8(1/2), 1995.
J. C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6(3/4):233–248, 1993.
G. Springer and D. P. Friedman. Scheme and the Art of Programming. MIT Press, 1989.
B. Thomsen. A calculus of higher order communicating systems. In Conf. Rec. 16th ACM Symposium on Principles of Programming Languages, pages 143–154, 1989.
R. van Glabbeek and F. Vaandrager. The difference between splitting in n and n+1 (abstract). In E. Best and G. Rozenberg, editors, Proceedings 3rd Workshop on Concurrency and Compositionality, Sankt Augustin, Germany, February 1991. GMD-Studien Nr. 191.
D. Walker. π-calculus semantics of object-oriented programming languages. In Proc. Conference on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Berlin, Heidelberg, and New York, 1991. Springer-Verlag.
M. Wand. Deriving target code as a representation of continuation semantics. ACM Transactions on Programming Languages and Systems, 4(3):496–517, July 1982.
M. Wand. Semantics-directed machine architecture. In Conf. Rec. 9th ACM Symposium on Principles of Programming Languages, pages 234–241, 1982.
M. Wand. Loops in combinator-based compilers. Information and Control, 57(2–3):148–164, May/June 1983.
M. Wand. Compiler correctness for parallel languages. In 1995 Symposium on Functional Languages and Computer Architecture, June 1995.
M. Wand and D. P. Oliva. Proving the correctness of storage representations. In Proc. 1992 ACM Symposium on Lisp and Functional Programming, pages 151–160, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gladstein, D.S., Wand, M. (1996). Compiler correctness for concurrent languages. In: Ciancarini, P., Hankin, C. (eds) Coordination Languages and Models. COORDINATION 1996. Lecture Notes in Computer Science, vol 1061. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61052-9_49
Download citation
DOI: https://doi.org/10.1007/3-540-61052-9_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61052-6
Online ISBN: 978-3-540-49936-7
eBook Packages: Springer Book Archive