Abstract
Sustaining scalable performance trends in the multicore era has led many compiler researchers to develop a host of optimizations to parallelize sequential programs. At the same time, formal methods researchers have pushed compiler verification technology forward to the point that real compilers may be checked for correctness by proving that the compiler preserves a simulation relation between the source and target languages. We join these two lines of research by proving a general parallelizing transformation schema sound for an extension of the Calculus of Communicating Systems (CCS) with semaphores and sequential composition. When source programs contain internal nondeterminism, we have found that the simulation relations that underlie the most prominent verified compilers, like CompCert, are too strong to admit a large class of parallelizing transformations. Thus we prove soundness with respect to a new simulation relation, called eventual simulation, that resolves this issue and is equivalent to weak bisimulation when no internal nondeterminism is present. All formal details presented are proven and mechanically checked using the Coq Proof Assistant.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Appel, A.W.: Verified software toolchain - (invited talk). In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011)
Botinčan, M., Dodds, M., Jagannathan, S.: Proof-directed parallelization synthesis by separation logic. ACM Trans. Program. Lang. Syst. 35(2), 8:1–8:60 (2013)
van Glabbeek, R.J.: The linear time - branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
Hurlin, C.: Automatic parallelization and optimization of programs by proof rewriting. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 52–68. Springer, Heidelberg (2009)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Milner, R.: A Calculus of Communicating Systems. Springer-Verlag New York, Inc., Secaucus (1982)
Padua, D.A., Wolfe, M.J.: Advanced compiler optimizations for supercomputers. Communications of the ACM 29(12), 1184–1201 (1986)
Parrow, J., Sjödin, P.: The complete axiomatization of cs-congruence. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol. 775, pp. 557–568. Springer, Heidelberg (1994)
Rangan, R., Vachharajani, N., Vachharajani, M., August, D.I.: Decoupled software pipelining with the synchronization array. In: IEEE PACT, pp. 177–188 (2004)
Ŝevčik, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. SIGPLAN Not. 46(1), 43–54 (2011)
Tatlock, Z., Lerner, S.: Bringing extensibility to verified compilers. SIGPLAN Not. 45(6), 111–121 (2010)
Voorhoeve, M., Mauw, S.: Impossible futures and determinism. Inf. Process. Lett. 80(1), 51–58 (2001)
Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. SIGPLAN Not. 47(1), 427–440 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Bell, C.J. (2013). Certifiably Sound Parallelizing Transformations. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-03545-1_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03544-4
Online ISBN: 978-3-319-03545-1
eBook Packages: Computer ScienceComputer Science (R0)