Matko Botinčan
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.
Supplemental Material
Available for Download
The proof is given in an electronic appendix, available online in the ACM Digital Library.
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Burnim, J. and Sen, K. 2010. Asserting and checking determinism for multithreaded programs. Comm. ACM 53, 97--105. Google ScholarDigital Library
- Calcagno, C., Distefano, D., O’Hearn, P. W., and Yang, H. 2011. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Creignou, N. and Zanuttini, B. 2006. A complete classification of the complexity of propositional abduction. SIAM J. Comput. 36, 1, 207--229. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Eiter, T. and Gottlob, G. 1995. The complexity of logic-based abduction. J. ACM 42, 1, 3--42. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Gupta, R., Pande, S., Psarris, K., and Sarkar, V. 1999. Compilation techniques for parallel systems. Parallel Comput. 25, 13--14, 1741--1783. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Hendren, L. J. and Nicolau, A. 1990. Parallelizing programs with recursive data structures. IEEE Trans. Parallel Distrib. Syst. 1, 1, 35--47. Google ScholarDigital Library
- Hoare, C. A. R. and O’Hearn, P. W. 2008. Separation logic semantics for communicating processes. Electron. Notes Theor. Comput. Sci. 212, 3--25. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Hurlin, C. 2009. Automatic parallelization and optimization of programs by proof rewriting. In Proceedings of the International Static Analysis Symposium. Springer, 52--68. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- O’Hearn, P. W. 2007. Resources, concurrency and local reasoning. Theor. Comput. Sci. 375, 271--307. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Raychev, V., Vechev, M., and Yahav, E. 2013. Automatic synthesis of deterministic concurrency. In Proceedings of the International Static Analysis Symposium. Springer.Google Scholar
- Raza, M., Calcagno, C., and Gardner, P. 2009. Automatic parallelization with separation logic. In Proceedings of the European Symposium on Programming. Springer, 348--362. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- SV-Comp. 2013. http://sv-comp.sosy-lab.org/2013/.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Proof-Directed Parallelization Synthesis by Separation Logic
Recommendations
Resource-sensitive synchronization inference by abduction
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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 '12We 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 2016AbstractWe 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
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