Abstract
Data race free (DRF) programs constitute an important class of concurrent programs. In this paper we provide a framework for designing and proving the correctness of data flow analyses that target this class of programs, and which are in the same spirit as the “sync-CFG” analysis originally proposed in [9]. To achieve this, we first propose a novel concrete semantics for DRF programs called L-DRF that is thread-local in nature with each thread operating on its own copy of the data state. We show that abstractions of our semantics allow us to reduce the analysis of DRF programs to a sequential analysis. This aids in rapidly porting existing sequential analyses to scalable analyses for DRF programs. Next, we parameterize the semantics with a partitioning of the program variables into “regions” which are accessed atomically. Abstractions of the region-parameterized semantics yield more precise analyses for region-race free concurrent programs. We instantiate these abstractions to devise efficient relational analyses for race free programs, which we have implemented in a prototype tool called RATCOP. On the benchmarks, RATCOP was able to prove upto 65% of the assertions, in comparison to 25% proved by a version of the analysis from [9].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The decision to block a thread releasing a lock it does not own was made to simplify the semantics. Our results hold even if this action aborts the program.
- 2.
Strictly speaking, the various relations we define are between indices \(\{0,\ldots ,\left| {\pi }\right| -1\}\) of an execution, and not transitions, so we should have written, e.g., \(i\xrightarrow {po}_\pi j\) instead of \(\pi _i\xrightarrow {po}_\pi \pi _j\). We use the rather informal latter notation, for readability.
- 3.
The project artifacts are available at https://bitbucket.org/suvam/ratcop.
- 4.
By thread-identifiers we are referring to the abstraction of the versions outlined in Remark 11.
References
Artho, C., Havelund, K., Biere, A.: High-level data races. In: New Technologies for Information Systems, Proceedings of the 3rd International Workshop on New Developments in Digital Libraries, NDDL 2003, pp. 82–93 (2003)
Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_31
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. CoRR, abs/cs/0701193 (2007)
Carre, J.-L., Hymans, C.: From single-thread to multithreaded: an efficient static analysis algorithm. CoRR, abs/0910.5833 (2009)
Chugh, R., Voung, J.W., Jhala, R., Lerner, A.: Dataflow analysis for concurrent programs using datarace detection. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7–13 June 2008, pp. 316–326 (2008)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, Paris, France. Dunod (1976)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages, pp. 84–96. ACM (1978)
De, A., D’Souza, D., Nasre, R.: Dataflow analysis for datarace-free programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 196–215. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19718-5_11
Dwyer, M.B., Clarke, L.A.: Data flow analysis for verifying properties of concurrent programs. In: Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT 1994, New Orleans, Louisiana, USA, 6–9 December 1994, pp. 62–75 (1994)
Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 297–308 (2012)
Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 129–142 (2013)
Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267–286. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11957-6_15
Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp. 266–277 (2007)
Grunwald, D., Srinivasan, H.: Data flow equations for explicitly parallel programs. In: Proceedings of the Fourth ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (PPOPP), pp. 159–168 (1993)
Jeannet, B.: Some experience on the software engineering of abstract interpretation tools. Electron. Notes Theor. Comput. Sci. 267(2), 29–42 (2010)
Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_52
Jones, C.B.: Developing methods for computer programs including a notion of interference. Ph.D. thesis, University of Oxford, UK (1981)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 558–565 (1978)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess progranm. IEEE Trans. Comput. 9, 690–691 (1979)
Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 363–377. Springer, Heidelberg (2008). doi:10.1007/978-3-540-69166-2_24
Miné, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Log. Methods Comput. Sci. 8(1), 1–63 (2012)
Miné, A.: Static analysis by abstract interpretation of concurrent programs. Ph.D. thesis, Ecole Normale Supérieure de Paris-ENS Paris (2013)
Miné, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39–58. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_3
Monat, R., Miné, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 386–404. Springer, Cham (2017). doi:10.1007/978-3-319-52234-0_21
Mukherjee, S., Padon, O., Shoham, S., D’Souza, D., Rinetzky, N.: Thread-local semantics and its efficient sequential abstractions for race-free programs. http://www.csa.iisc.ernet.in/TR/2016/3/sasTechReport.pdf
Naik, M.: Chord: a program analysis platform for Java. http://www.cis.upenn.edu/~mhnaik/chord.html. Accessed 27 Mar 2017
Rinard, M.: Analysis of multithreaded programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 1–19. Springer, Heidelberg (2001). doi:10.1007/3-540-47764-0_1
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multi-threaded programs. In: Proceedings of the Sixteenth ACM Symposium on Operating System Principles, SOSP, pp. 27–37 (1997)
Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot-a Java bytecode optimization framework. In: Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p. 13. IBM Press (1999)
Qiwen, X., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Form. Asp. Comput. 9, 149–174 (1997)
Acknowledgments
We would like to thank the anonymous reviewers for their insightful and helpful comments. This research was supported by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013)/ERC grant agreement n\(^{\circ }\) [321174], by Len Blavatnik and the Blavatnik Family foundation, and by the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Mukherjee, S., Padon, O., Shoham, S., D’Souza, D., Rinetzky, N. (2017). Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. In: Ranzato, F. (eds) Static Analysis. SAS 2017. Lecture Notes in Computer Science(), vol 10422. Springer, Cham. https://doi.org/10.1007/978-3-319-66706-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-66706-5_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66705-8
Online ISBN: 978-3-319-66706-5
eBook Packages: Computer ScienceComputer Science (R0)