Abstract
We study thread-modular static analysis by abstract interpretation to infer the values of variables in concurrent programs. We show how to go beyond the state of the art and increase an analysis precision by adding the ability to infer some relational and history-sensitive properties of thread interferences. The fundamental basis of this work is the formalization by abstract interpretation of a rely-guarantee concrete semantics which is thread-modular, constructive, and complete for safety properties. We then show that previous analyses based on non-relational interferences can be retrieved as coarse computable abstractions of this semantics; additionally, we present novel abstraction examples exploiting our ability to reason more precisely about interferences, including domains to infer relational lock invariants and the monotonicity of counters. Our method and domains have been implemented in the AstréeA static analyzer that checks for run-time errors in embedded concurrent C programs, where they enabled a significant reduction of the number of false alarms.
This work is supported by the INRIA project “Abstraction” common to CNRS and ENS in France and by the project ANR-11-INSE-014 from the French Agence nationale de la recherche.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Amjad, H., Bornat, R.: Towards automatic stability analysis for rely-guarantee proofs. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 14–28. Springer, Heidelberg (2009)
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL 2010, pp. 7–18. ACM (January 2010)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI 2003, pp. 196–207. ACM (June 2003)
Carré, J.-L., Hymans, C.: From single-thread to multithreaded: An efficient static analysis algorithm. Technical Report arXiv:0910.5833v1, EADS (October 2009)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science 277(1-2), 47–103 (2002)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: ISP 1976, pp. 106–130, Dunod, Paris (1976)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252. ACM (January 1977)
Cousot, P., Cousot, R.: Invariance proof methods and analysis techniques for parallel programs. In: Automatic Program Construction Techniques, ch. 2, pp. 243–271. Macmillan, New York (1984)
Delmas, D., Souyris, J.: Astrée: From research to industry. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 437–451. Springer, Heidelberg (2007)
Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theoretical Computer Science 338(1-3), 153–183 (2005)
Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213–224. Springer, Heidelberg (2003)
Jeannet, B.: Relational interprocedural verification of concurrent programs. Software & Systems Modeling 12(2), 285–306 (2013)
Jones, C.B.: Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University (June 1981)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. on Computers 28, 690–691 (1979)
Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is cartesian abstract interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 183–197. Springer, Heidelberg (2006)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Miné, A.: Static analysis by abstract interpretation of sequential and multi-thread programs. In: MOVEP 2012, pp. 35–48 (December 2012)
Miné, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Logical Methods in Computer Science 8(26), 63 (2012)
Miné, A.: Static analysis by abstract interpretation of concurrent programs. Habilitation report, École normale supérieure (May 2013)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6(4), 319–340 (1976)
Rinard, M.: Analysis of multithreaded programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 1–19. Springer, Heidelberg (2001)
Watkins, C.B., Walter, R.: Transitioning from federated avionics architectures to integrated modular avionics. In: DASC 2007, vol. 2.A.1, pp. 1–10. IEEE (October 2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miné, A. (2014). Relational Thread-Modular Static Value Analysis by Abstract Interpretation. In: McMillan, K.L., Rival, X. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2014. Lecture Notes in Computer Science, vol 8318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54013-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-54013-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54012-7
Online ISBN: 978-3-642-54013-4
eBook Packages: Computer ScienceComputer Science (R0)