research-article

Open access

Proof-Directed Parallelization Synthesis by Separation Logic

Authors:

Matko Botinčan,

Suresh JagannathanAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 35, Issue 2

Article No.: 8, Pages 1 - 60

https://doi.org/10.1145/2491522.2491525

Published: 01 July 2013 Publication History

Abstract

We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly synchronized parallelized program and proof of that program. Unlike previous work, ours is not a simple independence analysis that admits parallelization only when threads do not interfere; rather, we insert synchronization to preserve dependencies in the sequential program that might be violated by a naïve translation. Separation logic allows us to parallelize fine-grained patterns of resource usage, moving beyond straightforward points-to analysis. The sequential proof need only represent shape properties, meaning we can handle complex algorithms without verifying every aspect of their behavior.

Our analysis works by using the sequential proof to discover dependencies between different parts of the program. It leverages these discovered dependencies to guide the insertion of synchronization primitives into the parallelized program, and to ensure that the resulting parallelized program satisfies the same specification as the original sequential program, and exhibits the same sequential behavior. Our analysis is built using frame inference and abduction, two techniques supported by an increasing number of separation logic tools.

Supplementary Material

PDF File (a8-botincan_appendix.pdf)

The proof is given in an electronic appendix, available online in the ACM Digital Library.

Download
618.48 KB

References

[1]

Baskaran, M. M., Vydyanathan, N., Bondhugula, U., Ramanujam, J., Rountev, A., and Sadayappan, P. 2009. Compiler-assisted dynamic scheduling for effective parallelization of loop nests on multicore processors. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM, 219--228.

Digital Library

[2]

Bell, C. J., Appel, A., and Walker, D. 2009. Concurrent separation logic for pipelined parallelization. In Proceedings of the International Static Analysis Symposium. 151--166.

Digital Library

[3]

Berdine, J., Calcagno, C., and O’Hearn, P. W. 2005a. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects. Springer, 115--137.

Digital Library

[4]

Berdine, J., Calcagno, C., and O’Hearn, P. W. 2005b. Symbolic execution with separation logic. In Proceedings of the Asian Symposium on Programming Languages and Systems. Springer, 52--68.

Digital Library

[5]

Bergan, T., Anderson, O., Devietti, J., Ceze, L., and Grossman, D. 2010. CoreDet: A compiler and runtime system for deterministic multithreaded execution. SIGPLAN Not. 45, 3, 53--64.

Digital Library

[6]

Berger, E. D., Yang, T., Liu, T., and Novark, G. 2009. Grace: Safe multithreaded programming for C/C+ +. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM, 81--96.

Digital Library

[7]

Bocchino, Jr., R. L., Adve, V. S., Dig, D., Adve, S. V., Heumann, S., Komuravelli, R., Overbey, J., Simmons, P., Sung, H., and Vakilian, M. 2009. A type and effect system for deterministic parallel Java. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM, 91--116.

Digital Library

[8]

Bornat, R., Calcagno, C., O’Hearn, P., and Parkinson, M. 2005. Permission accounting in separation logic. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM, 259--270.

Digital Library

[9]

Botinčan, M., Distefano, D., Dodds, M., Griore, R., Naudžiūnienė, and Parkinson, M. 2011. coreStar: The core of jStar. In Proceedings of the Workshop on Formal Techniques for Java-like Programs. 65--77.

[10]

Burnim, J. and Sen, K. 2010. Asserting and checking determinism for multithreaded programs. Comm. ACM 53, 97--105.

Digital Library

[11]

Calcagno, C., Distefano, D., O’Hearn, P. W., and Yang, H. 2011. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6.

Digital Library

[12]

Calcagno, C., Distefano, D., and Vafeiadis, V. 2009. Bi-abductive resource invariant synthesis. In Proceedings of the Asian Symposium on Programming Languages and Systems. Springer, 259--274.

Digital Library

[13]

Cook, B., Haase, C., Ouaknine, J., Parkinson, M. J., and Worrell, J. 2011. Tractable reasoning in a fragment of separation logic. In Proceedings of the International Conference on Concurrency Theory. Springer, 235--249.

Digital Library

[14]

Cook, B., Magill, S., Raza, M., Simsa, J., and Singh, S. 2010. Making fast hardware with separation logic. http://cs.cmu.edu/~smagill/papers/fast-hardware.pdf.

[15]

Creignou, N. and Zanuttini, B. 2006. A complete classification of the complexity of propositional abduction. SIAM J. Comput. 36, 1, 207--229.

Digital Library

[16]

Deshmukh, J. V., Ramalingam, G., Ranganath, V. P., and Vaswani, K. 2010. Logical concurrency control from sequential proofs. In Proceedings of the European Symposium on Programming. Springer, 226--245.

Digital Library

[17]

Distefano, D. and Filipović, I. 2010. Memory leaks detection in java by bi-abductive inference. In Proceedings of the Conference on Fundamental Approaches to Software Engineering. Springer, 278--292.

Digital Library

[18]

Distefano, D. and Parkinson, M. J. 2008. jStar: Towards practical verification for Java. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM, 213--226.

Digital Library

[19]

Dodds, M., Jagannathan, S., and Parkinson, M. J. 2011. Modular reasoning for deterministic parallelism. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM, 259--270.

Digital Library

[20]

Eiter, T. and Gottlob, G. 1995. The complexity of logic-based abduction. J. ACM 42, 1, 3--42.

Digital Library

[21]

Ghiya, R., Hendren, L. J., and Zhu, Y. 1998. Detecting parallelism in c programs with recursive data structures. In Proceedings of the International Conference on Compiler Construction. Springer, 159--173.

Digital Library

[22]

Golan-Gueta, G., Bronson, N. G., Aiken, A., Ramalingam, G., Sagiv, M., and Yahav, E. 2011. Automatic fine-grain locking using shape properties. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM, 225--242.

Digital Library

[23]

Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., and Sagiv, M. 2007. Local reasoning for storable locks and threads. In Proceedings of the Asian Symposium on Programming Languages and Systems. Springer, 19--37.

Digital Library

[24]

Gupta, R., Pande, S., Psarris, K., and Sarkar, V. 1999. Compilation techniques for parallel systems. Parallel Comput. 25, 13--14, 1741--1783.

Digital Library

[25]

Haack, C., Huisman, M., and Hurlin, C. 2008. Reasoning about Java’s reentrant locks. In Proceedings of the Asian Symposium on Programming Languages and Systems. Springer, 171--187.

Digital Library

[26]

Hendren, L. J. and Nicolau, A. 1990. Parallelizing programs with recursive data structures. IEEE Trans. Parallel Distrib. Syst. 1, 1, 35--47.

Digital Library

[27]

Hoare, C. A. R. and O’Hearn, P. W. 2008. Separation logic semantics for communicating processes. Electron. Notes Theor. Comput. Sci. 212, 3--25.

Digital Library

[28]

Hobor, A., Appel, A. W., and Zappa Nardelli, F. 2008. Oracle semantics for concurrent separation logic. In Proceedings of the European Symposium on Programming. Springer.

Digital Library

[29]

Horwitz, S., Pfeiffer, P., and Reps, T. W. 1989. Dependence analysis for pointer variables. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, 28--40.

Digital Library

[30]

Hurlin, C. 2009. Automatic parallelization and optimization of programs by proof rewriting. In Proceedings of the International Static Analysis Symposium. Springer, 52--68.

Digital Library

[31]

Jacobs, B. and Piessens, F. 2009. Modular full functional specification and verification of lock-free data structures. Tech. rep. CW 551, Department of Computer Science, Katholieke Universiteit Leuven.

[32]

Leino, K. R. M., Müller, P., and Smans, J. 2010. Deadlock-free channels and locks. In Proceedings of the European Symposium on Programming. Springer, 407--426.

Digital Library

[33]

Liu, T., Curtsinger, C., and Berger, E. D. 2011. Dthreads: Efficient deterministic multithreading. In Proceedings of the ACM Symposium on Operating Systems Principles. ACM, 327--336.

Digital Library

[34]

Navabi, A., Zhang, X., and Jagannathan, S. 2008. Quasi-static scheduling for safe futures. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM, 23--32.

Digital Library

[35]

O’Hearn, P. W. 2007. Resources, concurrency and local reasoning. Theor. Comput. Sci. 375, 271--307.

Digital Library

[36]

Ottoni, G., Rangan, R., Stoler, A., and August, D. I. 2005. Automatic thread extraction with decoupled software pipelining. In Proceedings of the Annual ACM/IEEE International Symposium on Microarchitecture. IEEE, 105--118.

Digital Library

[37]

Pingali, K., Nguyen, D., Kulkarni, M., Burtscher, M., Hassaan, M. A., Kaleem, R., Lee, T.-H., Lenharth, A., Manevich, R., Méndez-Lojo, M., Prountzos, D., and Sui, X. 2011. The tao of parallelism in algorithms. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, 12--25.

Digital Library

[38]

Raychev, V., Vechev, M., and Yahav, E. 2013. Automatic synthesis of deterministic concurrency. In Proceedings of the International Static Analysis Symposium. Springer.

[39]

Raza, M., Calcagno, C., and Gardner, P. 2009. Automatic parallelization with separation logic. In Proceedings of the European Symposium on Programming. Springer, 348--362.

Digital Library

[40]

Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science. IEEE, 55--74.

Digital Library

[41]

SV-Comp. 2013. http://sv-comp.sosy-lab.org/2013/.

[42]

Tang, P., Tang, P., Zigman, J. N., and Zigman, J. N. 1994. Reducing data communication overhead for DOACROSS loop nests. In Proceedings of the International Conference on Supercomputing. ACM, 44--53.

Digital Library

[43]

Villard, J., Lozes, É., and Calcagno, C. 2010. Tracking heaps that hop with Heap-Hop. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 275--279.

Digital Library

[44]

Welc, A., Jagannathan, S., and Hosking, A. 2005. Safe futures for Java. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM, 439--435.

Digital Library

[45]

Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., and O’Hearn, P. W. 2008. Scalable shape analysis for systems code. In Proceedings of the International Conference on Computer Aided Verification. Springer, 385--398.

Digital Library

Cited By

Blom SDarabi SHuisman MSafari M(2021)Correct program parallelisationsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00601-z23:5(741-763)Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s10009-020-00601-z
DeLozier CEizenberg ALucia BDevietti J(2018)SOFRITASACM SIGPLAN Notices10.1145/3296957.317319253:2(286-300)Online publication date: 19-Mar-2018
https://dl.acm.org/doi/10.1145/3296957.3173192
DeLozier CEizenberg ALucia BDevietti JShen XTuck JBianchini RSarkar V(2018)SOFRITASProceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3173162.3173192(286-300)Online publication date: 19-Mar-2018
https://dl.acm.org/doi/10.1145/3173162.3173192
Show More Cited By

Index Terms

Proof-Directed Parallelization Synthesis by Separation Logic
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Concurrent programming structures
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory

Recommendations

Resource-sensitive synchronization inference by abduction
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly-synchronized parallelized ...
Resource-sensitive synchronization inference by abduction
POPL '12

We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly-synchronized parallelized ...
Automated mutual induction proof in separation logic
Special Issue on Extended Versions of Papers Presented at FM 2016
Abstract
We present a deductive proof system to automatically prove separation logic entailments by mathematical induction. Our technique is called the mutual induction proof. It is an instance of the well-founded induction, a.k.a., Noetherian induction. ...

Reviews

Reviewer: Wolfgang Schreiner

The parallelization of sequential programs is a tedious and error-prone task; the incorrect use of synchronization primitives may yield a program that produces different results than the original code, or even different results in different runs. This paper proposes an alternative approach that borrows concepts from program verification to generate a parallel program guaranteed to produce the same result as the sequential version. The core idea is that, in addition to potential parallelization points, the programmer provides a specification of the sequential program behavior and a proof (an annotation of the program with crucial assertions) that the program meets this specification. The specification is expressed in a class of separation logic formulas called symbolic heaps, which describe both logical conditions and the shape of data structures, and, in particular, which parts of the data do not overlap. From this and the proof, a symbolic analysis determines program points where synchronization primitives are to be inserted, based on various inference queries supported by automated separation logic provers. The paper introduces the technique for the more casual reader using examples. The main part then provides the technical background for the expert, in particular the details of the analysis and the proof of its soundness. The paper demonstrates in a fascinating fashion how automated proving techniques find their way into compilation technology. Thus, the task of the programmer may gradually shift from writing low-level code to providing high-level specifications. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 35, Issue 2

July 2013

136 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/2491522

Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2013

Accepted: 01 March 2013

Revised: 01 January 2013

Received: 01 February 2012

Published in TOPLAS Volume 35, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
386
Total Downloads

Downloads (Last 12 months)65
Downloads (Last 6 weeks)14

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Blom SDarabi SHuisman MSafari M(2021)Correct program parallelisationsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00601-z23:5(741-763)Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s10009-020-00601-z
DeLozier CEizenberg ALucia BDevietti J(2018)SOFRITASACM SIGPLAN Notices10.1145/3296957.317319253:2(286-300)Online publication date: 19-Mar-2018
https://dl.acm.org/doi/10.1145/3296957.3173192
DeLozier CEizenberg ALucia BDevietti JShen XTuck JBianchini RSarkar V(2018)SOFRITASProceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3173162.3173192(286-300)Online publication date: 19-Mar-2018
https://dl.acm.org/doi/10.1145/3173162.3173192
Krogh-Jespersen MSvendsen KBirkedal L(2017)A relational model of types-and-effects in higher-order concurrent separation logicACM SIGPLAN Notices10.1145/3093333.300987752:1(218-231)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009877
Krogh-Jespersen MSvendsen KBirkedal LCastagna GGordon A(2017)A relational model of types-and-effects in higher-order concurrent separation logicProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009877(218-231)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009877
Darabi SBlom SHuisman M(2017)A Verification Technique for Deterministic Parallel ProgramsNASA Formal Methods10.1007/978-3-319-57288-8_17(247-264)Online publication date: 9-Apr-2017
https://doi.org/10.1007/978-3-319-57288-8_17
Winterstein FWinterstein F(2017)BackgroundSeparation Logic for High-level Synthesis10.1007/978-3-319-53222-6_3(35-55)Online publication date: 28-Feb-2017
https://doi.org/10.1007/978-3-319-53222-6_3
Winterstein FBayliss SConstantinides G(2015)Separation Logic for High-Level SynthesisACM Transactions on Reconfigurable Technology and Systems10.1145/28361699:2(1-23)Online publication date: 17-Dec-2015
https://dl.acm.org/doi/10.1145/2836169
Winterstein FBayliss SConstantinides G(2014)Separation Logic-Assisted Code Transformations for Efficient High-Level Synthesis2014 IEEE 22nd Annual International Symposium on Field-Programmable Custom Computing Machines10.1109/FCCM.2014.11(1-8)Online publication date: May-2014
https://doi.org/10.1109/FCCM.2014.11
Bell C(2013)Certifiably Sound Parallelizing TransformationsCertified Programs and Proofs10.1007/978-3-319-03545-1_15(227-242)Online publication date: 11-Dec-2013
https://dl.acm.org/doi/10.1007/978-3-319-03545-1_15

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents