Thread-modular shape analysis

ABSTRACT

We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.

REFERENCES

• 1: J. Berdine, C. Calcagno, and P. O'Hearn. Symbolic execution with separation logic. In APLAS'05: Asian Symposium on Programming Languages and Systems, volume 3780 of LNCS, pages 52--68. Springer, 2005.
• 2: Richard Bornat , Cristiano Calcagno , Peter O'Hearn , Matthew Parkinson, Permission accounting in separation logic, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.259-270, January 12-14, 2005, Long Beach, California, USA
• 3: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 4: C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In SAS'06: Static Analysis Simposium, volume 4134 of em LNCS, pages 182--203. Springer, 2006.
• 5: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 6: Edmund Clarke, Jr., Synthesis of Resource Invariants for Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.338-358, July 1980 [doi>10.1145/357103.357109]
• 7: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 8: P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.
• 9: D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS'06: Tools and Algorithms for Analysis and Construction of Systems, volume 3920 of LNCS, pages 287--302. Springer, 2006.
• 10: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN'03: Workshop on Model Checking Software, volume 2648 of LNCS, pages 213--224. Springer, 2003.
• 12: A. Gotsman, J. Berdine, and B. Cook. Interprocedural shape analysis with separated heap abstractions. In SAS'06: Static Analysis Symposium, volume 4134 of LNCS, pages 240--260. Springer, 2006.
• 13: A. Gotsman, N. Rinetzky, J. Berdine, B. Cook, D. Distefano, P. W. O'Hearn, M. Sagiv, and H. Yang. Abstract interpretation with state separation. In preparation, 2007.
• 14: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 15: TLev-Ami. Personal communication. 2006.
• 16: T. Lev-Ami, N. Immerman, and M. Sagiv. Abstraction for shape analysis with fast and precise transformers. In CAV'06: Computer Aided Verification, volume 4144 of LNCS, pages 547--561. Springer, 2006.
• 17: Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 18: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 19: P. W. O'Hearn. Resources, concurrency and local reasoning. In CONCUR'04: International Conference on Concurrency Theory, volume 3170 of LNCS, pages 49--67. Springer, 2004.
• 20: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 21: Matthew Parkinson , Richard Bornat , Cristiano Calcagno, Variables as Resource in Hoare Logics, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.137-146, August 12-15, 2006 [doi>10.1109/LICS.2006.52]
• 22: Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 23: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 24: N. Rinetzky, M. Sagiv, and E. Yahav. Interprocedural shape analysis for cutpoint-free programs. In SAS'05: Static Analysis Symposium, volume 3672 of LNCS, pages 284--302. Springer, 2005.
• 25: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 26: Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-40, January 2001, London, United Kingdom
• 27: Hongseok Yang , Peter W. O'Hearn, A Semantic Basis for Local Reasoning, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.402-416, April 08-12, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Theory, Verification

Keywords:
abstract interpretation, concurrent programming, shape analysis, static analysis