Abstract
We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating proof trees and a rewrite system on proof trees.
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
Proof trees of the examples, additional examples, and open source implementation, http://www-sop.inria.fr/everest/Clement.Hurlin/eterlou/eterlou.shtml
Aiken, A., Nicolau, A.: Optimal loop parallelization. ACM SIGPLAN Notices 23(7) (1988)
Artigas, P., Gupta, M., Midkiff, S., Moreira, J.: Automatic loop transformations and parallelization for Java. In: International Conference on Supercomputing. ACM Press, New York (2000)
Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom: Piggybacking rewriting on Java. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 36–47. Springer, Heidelberg (2007)
Barthe, G., Grégoire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 301–317. Springer, Heidelberg (2006)
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178–192. Springer, Heidelberg (2007)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111. Springer, Heidelberg (2006)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)
Bik, A., Gannon, D.: Automatically exploiting implicit parallelism in Java. Concurrency: Practice and Experience 9 (1997)
Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. In: Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol. 155. Elsevier, Amsterdam (2005)
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM Press, New York (2002)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)
Calcagno, C., Distefano, D., OHearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Shao, Z., Pierce, B.C. (eds.) Principles of Programming Languages. ACM Press, New York (to appear, 2009)
Chin, W., David, C., Nguyen, H., Qin, S.: Enhancing modular OO verification with separation logic. In: Necula, G.C., Wadler, P. (eds.) Principles of Programming Languages. ACM Press, New York (2008)
Cunningham, D., Gudka, K., Eisenbach, S.: Keep off the grass: Locking the right path for atomicity. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 276–290. Springer, Heidelberg (2008)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)
DiStefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, vol. 43. ACM Press, New York (2008)
Ergin, O., Balkan, D., Ponomarev, D., Ghose, K.: Early register deallocation mechanisms using checkpointed register files. IEEE Computer 55 (2006)
Ghiya, R., Hendren, L.J., Zhu, Y.: Detecting parallelism in c programs with recursive data structures. In: Koskimies, K. (ed.) CC 1998, vol. 1383. Springer, Heidelberg (1998)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007)
Gupta, R., Pande, S., Psarris, K., Sarkar, V.: Compilation techniques for parallel systems. Parallel Computing 25(13) (1999)
Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java’s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 171–187. Springer, Heidelberg (2008)
Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork/join. In: Meseguer, J., Rosu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 199–215. Springer, Heidelberg (2008)
Hendren, L.J., Nicolau, A.: Parallelizing programs with recursive data structures. IEEE Transactions on Parallel and Distributed Systems 1 (1990)
Hurlin, C.: Automatic parallelization and optimization of programs by proof rewriting. Technical Report 6806, INRIA. Initial version: January 2009, revised version: April 2009
Jacobs, B., Piessens, F.: The verifast program verifier. Technical Report CW520, Katholieke Universiteit Leuven (2008)
Lamport, L.: The parallel execution of do loops. Communications of the ACM 17(2) (1974)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Principles of Programming Languages. ACM Press, New York (2006)
Necula, G.C.: Translation validation for an optimizing compiler. ACM SIGPLAN Notices 35(5) (2000)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3) (2007)
O’Hearn, P.W., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 1. Springer, Heidelberg (2001) (invited paper)
Parkinson, M.: Local Reasoning for Java. Ph.D thesis, University of Cambridge (2005)
Raza, M., Calcagno, C., Gardner, P.: Automatic parallelization with separation logic. In: European Symposium on Programming (to appear, 2009)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science. IEEE Press, Los Alamitos (2002)
Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol. 2392, p. 63. Springer, Heidelberg (2002)
Xue, C., Shao, Z., Sha, E.-M.: Maximize parallelism minimize overhead for nested loops via loop striping. Journal of VLSI Signal Processing Systems 47(2) (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hurlin, C. (2009). Automatic Parallelization and Optimization of Programs by Proof Rewriting. In: Palsberg, J., Su, Z. (eds) Static Analysis. SAS 2009. Lecture Notes in Computer Science, vol 5673. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03237-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-03237-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03236-3
Online ISBN: 978-3-642-03237-0
eBook Packages: Computer ScienceComputer Science (R0)