×

zbMATH — the first resource for mathematics

Synthesizing precise and useful commutativity conditions. (English) Zbl 07268906
Summary: Reasoning about commutativity between data-structure operations is an important problem with many applications. In the sequential setting, commutativity can be used to reason about the correctness of refactoring, compiler transformations, and identify instances of non-determinism. In parallel contexts, commutativity dates back to the database [W. E. Weihl, IEEE Trans. Comput. 37, No. 12, 1488–1505 (1988; Zbl 0674.68016)] and compilers [M. C. Rinard and P. C. Diniz, “Commutativity analysis: a new analysis technique for parallelizing compilers”, ACM Trans. Program. Lang. Syst. 19, No. 6, 942–991 (1997; doi:10.1145/267959.269969)] communities and, more recently, appears in optimistic parallelization [M. Herlihy and E. Koskinen, “ Transactional boosting: a methodology for highly concurrent transactional objects”, in: Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming. PPoPP’08. New York, NY: Association for Computing Machinery (ACM). 207–216 (2008)], dynamic concurrency [O. Tripp et al., “Janus: Exploiting Parallelism via Hindsight”, in: Proceedings of the 33rd ACM SIGPLAN conference on programming language design and implementation. PLDI ’12. New York, NY: Association for Computing Machinery (ACM). 145–156 (2012); D. Dimitrov et al., “Commutativity race detection”, in: Proceedings of the 35th ACM SIGPLAN conference on programming language design and implementation. PLDI’14. New York, NY: Association for Computing Machinery (ACM). (2014)], scalable systems [A. T. Clements et al., “The scalable commutativity rule: designing scalable software for multicore processors”, ACM Trans. Comput. Syst. 32, No. 4, Paper No. 10 (2015; doi:10.1145/2699681)] and even smart contracts [T. Dickerson et al., “Adding concurrency to smart contracts”, in: Proceedings of the ACM symposium on principles of distributed computing. PODC’17. New York, NY: Association for Computing Machinery (ACM). 303–312 (2017)]. There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective. We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers [R. J. Lipton, Commun. ACM 18, 717–721 (1975; Zbl 0316.68015)] and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition. We have implemented our technique in a prototype open-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois first by synthesizing commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. We then show several applications of our work including reasoning about memories and locks, finding vulnerabilities in Ethereum smart contracts, improving transactional memory performance, distributed applications, code refactoring, verification, and synthesis.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Software:
CVC4; GitHub; Servois; Spec#
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Lamport, L., The existence of refinement mappings, Theor. Comput. Sci., 82, 253-284 (1991) · Zbl 0728.68083
[2] Aleen,F., Clark, N.: Commutativity analysis for software parallelization: letting program transformations see the big picture. In: Proceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XII), pp. 241-252. ACM (2009)
[3] Bansal, K., Koskinen, E., Tripp, O.: Automatic generation of precise and useful commutativity conditions. In: Tools and Algorithms for the Construction and Analysis of Systems—24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Greece, April 2018, Proceedings, Part II (2017) · Zbl 1423.68115
[4] Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Proceedings of the 8th International Joint Conference on Automated Reasoning, vol. 9706, pp. 82-98. Springer (2016) · Zbl 06623255
[5] Bansal, K.: Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions. Ph.D. Thesis, New York University (Jan. 2016)
[6] Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS’04, pp. 49-69 (2005)
[7] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.), Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11), vol. 6806, pp. 171-177. Springer (July 2011)
[8] Chechik, M., Stavropoulou, I., Disenfeld, C., Rubin, J.: FPH: efficient non-commutativity analysis of feature-based systems. In: Fundamental Approaches to Software Engineering, 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, pp. 319-336 (2018)
[9] Clements, AT; Kaashoek, MF; Zeldovich, N.; Morris, RT; Kohler, E., The scalable commutativity rule: designing scalable software for multicore processors, ACM Trans. Comput. Syst., 32, 4, 10 (2015)
[10] Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pp. 399-410 (2011) · Zbl 1284.68389
[11] Dickerson, T., Gazzillo, P., Herlihy, M., Koskinen, E.: Adding concurrency to smart contracts. In: Proceedings of the ACM Symposium on Principles of Distributed Computing, PODC ’17, New York, NY, USA, pp. 303-312 (2017). ACM · Zbl 1445.68083
[12] Dimitrov, D., Raychev, V., Vechev, M.T., Koskinen, E.: Commutativity race detection. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom, June 09-11, 2014, p. 33. ACM (2014)
[13] Dimitrov, D., Raychev, V., Vechev, M., Koskinen, E.: Commutativity race detection. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14) (2014)
[14] Ernst, GW; Ogden, WF, Specification of abstract data types in modula, ACM Trans. Program. Lang. Syst., 2, 4, 522-543 (1980) · Zbl 0468.68020
[15] Ethereum. https://ethereum.org/. Accessed 26 Aug 2020
[16] Ettinger, R.: Program sliding. In: ECOOP 2012—Object-Oriented Programming—26th European Conference, Beijing, China, June 11-16, 2012. Proceedings, pp. 713-737 (2012)
[17] Flon, L., Misra, J.: A unified approach to the specification and verification of abstract data types. In: Proceedings of Specifications of Reliable Software Conference. IEEE Computer Society (1979)
[18] Gehr, T., Dimitrov, D., Vechev, M.T.: Learning commutativity specifications. In: Computer Aided Verification—27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pp. 307-323 (2015) · Zbl 1381.68105
[19] Herlihy, M., Koskinen, E.: Transactional boosting: a methodology for highly concurrent transactional objects. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’08) (2008)
[20] Hoare, CAR; Broy, M.; Denert, E., Software pioneers, Proof of Correctness of Data Representations, 385-396 (2002), New York: Springer, New York
[21] Hu, Y., Barrett, C., Goldberg, B.: Theory and algorithms for the generation and validation of speculative loop optimizations. In: Proceedings of the 2nd IEEE International Conference on Software Engineering and Formal Methods (SEFM ’04), pp. 281-289. IEEE Computer Society (Sept. 2004)
[22] Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’10, New York, NY, USA, pp. 36-46 (2010). ACM
[23] Kim, D., Rinard, M.C.: Verification of semantic commutativity conditions and inverse operations on linked data structures. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 528-541. ACM (2011)
[24] Koskinen, E., Parkinson, M.J., Herlihy, M.: Coarse-grained transactions. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 19-30. ACM (2010) · Zbl 1312.68143
[25] Koskinen, E., Parkinson, M.J.: The push/pull model of transactions. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15, Portland, OR, USA, June (2015)
[26] Kulkarni, M., Nguyen, D., Prountzos, D., Sui, X., Pingali, K.: Exploiting the commutativity lattice. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 542-555. ACM (2011)
[27] Leino, K.R.M.: Specifying and verifying programs in spec#. In: Proceedings of the 6th International Perspectives of Systems Informatics, Andrei Ershov Memorial Conference, PSI 2006, p. 20 (2006)
[28] Lipton, RJ, Reduction: a method of proving properties of parallel programs, Commun. ACM, 18, 12, 717-721 (1975) · Zbl 0316.68015
[29] Meyer, B., Applying “design by contract”, IEEE Comput., 25, 10, 40-51 (1992)
[30] Ni, Y., Menon, V., Adl-Tabatabai, A., Hosking, A.L., Hudson, R.L., Moss, J.E.B., Saha, B., Shpeisman, T.: Open nesting in software transactional memory. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2007, pp. 68-78. ACM (2007)
[31] Rinard, MC; Diniz, PC, Commutativity analysis: a new analysis technique for parallelizing compilers, ACM Trans. Program. Lang. Syst., 19, 6, 942-991 (1997)
[32] Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: 1st Workshop on Trusted Smart Contracts (2017)
[33] Servois homepage. http://cs.nyu.edu/ kshitij/projects/servois. Accessed 26 Aug 2020
[34] Servois source code. https://github.com/kbansal/servois. Accessed 26 Aug 2020
[35] Solar-Lezama, A., Jones, C. G., Bodík, R.: Sketching concurrent data structures. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation PLDI 2008, pp. 136-148 (2008)
[36] Solidity programming language. https://solidity.readthedocs.io/en/develop/. Accessed 26 Aug 2020
[37] Tripp, O., Manevich, R., Field, J., Sagiv, M.: Janus: exploiting parallelism via hindsight. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, New York, NY, USA, pp. 145-156 (2012). ACM
[38] Tripp, O., Yorsh, G., Field, J., Sagiv, M.: HAWKEYE: effective discovery of dataflow impediments to parallelization. In: Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22-27, 2011, pp. 207-224 (2011)
[39] Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 327-338 (2010) · Zbl 1312.68043
[40] Vechev, M.T., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp. 125-135 (2008)
[41] Wang, C.; Yang, Z.; Kahlon, V.; Gupta, A.; Vojnar, T.; Zhang, L., Peephole partial order reduction, Tools and Algorithms for the Construction and Analysis of Systems, 382-396 (2008), Berlin: Springer, Berlin · Zbl 1134.68421
[42] Weihl, W., Commutativity-based concurrency control for abstract data types, IEEE Trans. Comput., 37, 12, 1488-1505 (1988) · Zbl 0674.68016
[43] Xiao, T., Zhang, J., Zhou, H., Guo, Z., McDirmid, S., Lin, W., Chen, W., Zhou, L.: Nondeterminism in mapreduce considered harmful? an empirical study on non-commutative aggregators in mapreduce programs. In: Companion Proceedings of the 36th International Conference on Software Engineering, ICSE Companion 2014, New York, NY, USA, pp. 44-53 (2014). ACM
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.