skip to main content
research-article
Open Access

Verifying safety properties of concurrent heap-manipulating programs

Published:24 May 2008Publication History
Skip Abstract Section

Abstract

We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are more precise than existing techniques. The framework also provides a precise shape-analysis algorithm for concurrent programs. In contrast to most existing verification techniques, we do not put a bound on the number of allocated objects. The framework produces interesting results even when analyzing programs with an unbounded number of threads. The framework is applied to successfully verify the following properties of a concurrent program:

—Concurrent manipulation of linked-list based ADT preserves the ADT datatype invariant.

—The program does not perform inconsistent updates due to interference.

—The program does not reach a deadlock.

—The program does not produce runtime errors due to illegal thread interactions.

We also found bugs in erroneous programs violating such properties. A prototype of our framework has been implemented and applied to small, but interesting, example programs.

References

  1. Abdulla, P. A., Annichini, A., Bensalem, S., Bouajjani, A., Habermehl, P., and Lakhnech, Y. 1999. Verification of infinite-state systems by combining abstraction and reachability analysis. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99). Springer-Verlag, Berlin, Germany, 146--159. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. Amit, D., Rinetzky, N., Reps, T., Sagiv, M., and Yahav, E. 2007. Comparison under abstraction for verifying linearizability. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Atig, M. F., Bouajjani, A., and Qadeer, S. 2009. Context-bounded analysis for concurrent programs with dynamic creation of threads. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 5505. Springer-Verlag, Berlin, Germany, 107--123. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Balaban, I., Pnueli, A., and Zuck, L. D. 2005. Shape analysis by predicate abstraction. In Proceedings of the Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3385. Springer-Verlag, Berlin, Germany, 164--180. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. 2001. Automatic predicate abstraction of C programs. In Proceedings of the Conference on Programming Languages Design and Implementation. ACM, New York, 203--213. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Bensalem, S., Ganesh, V., Lakhnech, Y., Muñoz, C., Owre, S., Ruess, H., Rushby, J., Rusu, V., Saïdi, H., Shankar, N., Singerman, E., and Tiwari, A. 2000. An overview of SAL. In Proceedings of the 5th NASA Langley Formal Methods Workshop (LFM'00), NASA, Hampton, VA, 187--196.Google ScholarGoogle Scholar
  7. Bensalem, S., Lakhnech, Y., and Owre, S. 1998. Invest: A tool for the verification of invariants. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98). Springer-Verlag, Berlin, Germany, 505--510. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Berdine, J., Calcagno, C., Cook, B., Distefano, D., OHearn, P. W., Wies, T., and Yang, H. 2007. Shape analysis for composite data structures. In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 178--192. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Berdine, J., Calcagno, C., and OHearn, P. W. 2005. Symbolic execution with separation logic. In Proceedings of the Programming Languages and Systems. Lecture Notes in Computer Science, vol. 3780. Springer-Verlag, Berlin, Germany, 52--68. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., and Sagiv, M. 2008. Thread quantification for concurrent shape analysis. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV'08). Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 399--413. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Bogudlov, I., Lev-Ami, T., Reps, T. W., and Sagiv, M. 2007. Revamping TVLA: Making parametric shape analysis competitive. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 221--225. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Bornat, R., Calcagno, C., O'Hearn, P., and Parkinson, M. 2005. Permission accounting in separation logic. SIGPLAN Not. 40, 1, 259--270. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Boyapati, C., Lee, R., and Rinard, M. 2002. Ownership types for safe programming: preventing data races and deadlocks. In Proceedings of the 17th ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA'02). ACM, New York, 211--230. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Boyapati, C. and Rinard, M. 2001. A parameterized type system for race-free java programs. In Proceedings of the 16th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'01). ACM, New York, 56--69. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. Buhr, P. A., Fortier, M., and Coffin, M. H. 1995. Monitor classification. ACM Comput. Surv. 27, 1, 63--107. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Calcagno, C., Distefano, D., O'Hearn, P., and Yang, H. 2009. Compositional shape analysis by means of bi-abduction. In Proceedings of the 36th Annual ACM Symposium on Principles of Programming Languages (POPL'09). ACM, New York, 289--300. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Cardelli, L. and Gordon, A. D. 1998. Mobile ambients. In Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS'98). Lecture Notes in Computer Science, vol. 1378. Springer-Verlag, Berlin, Germany, 140--155. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Cenciarelli, P., Knapp, A., Reus, B., and Wirsing, M. 1999. An event-based structural operational semantis of multi-threaded Java. In Formal Syntax and Semantics of Java. Springer-Verlag, Berlin, Germany, 157--200. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Chase, D., Wegman, M., and Zadeck, F. 1990. Analysis of pointers and structures. In Proceedings of the Conference on Programming Languages Design and Implemntation. ACM, New York, 296--310. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Choi, J., Loginov, A., and Sarkar, V. 2001. Static datarace analysis for multithreaded object-oriented programs. IBM Research Report 22146, IBM Research.Google ScholarGoogle Scholar
  21. Clarke, E., Grumberg, O., and Long, D. 1994. Model checking and abstraction. Trans. Prog. Lang. and Syst. 16, 5, 1512--1542. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Clarke, E., Grumberg, O., and Peled, D. 1999a. Model Checking. MIT Press, Cambridge, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Clarke, E., Talupur, M., and H. V. 2008. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 33--47. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Clarke, E., Talupur, M., and Veith, H. 2006. Environment abstraction for parameterized verification. In Proceedings of the Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3855. Springer-Verlag, Berlin, Germany, 126--141. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. Clarke, E. M., Grumberg, O., and Jha, S. 1997. Verifying parameterized networks. Trans. Prog. Lang. Syst. 19, 5, 726--750. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. Clarke, E. M., Grumberg, O., and Peled, D. A. 1999b. Model Checking. MIT Press, Cambridge, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., and Quesada, J. F. 2002. Maude: specification and programming in rewriting logic. Theoret. Comput. Sci. 285, 2, 187--243. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Cook, B., Kroening, D., and Sharygina, N. 2005. Symbolic model checking for asynchronous boolean programs. In Proceedings of the Symposium on Model Checking Software (SPIN'05). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 75--90. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Corbett, J. C. 2000. Using shape analysis to reduce finite-state models of concurrent java programs. ACM Trans. Softw. Eng. Methodol. 9, 1, 51--93. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 238--252. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 269--282. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. Das, M., Lerner, S., and Seigle, M. 2002. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02). ACM, New York, 57--68. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the 11th International Conference on Computer-Aided Verification. Springer-Verlag, Berlin, Germany. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. Demartini, C., Iosif, R., and Sisto, R. 1999a. A deadlock detection tool for concurrent Java programs. Softw. Pract. Exper. 29, 7, 577--603. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. Demartini, C., Iosif, R., and Sisto, R. 1999b. dSPIN: A dynamic extension of SPIN. In Proceedings of the 5th and 6th International SPIN Wokshops on Theoretical and Practical Aspects of SPIN Model Checking. Springer-Verlag, Berlin, Germany, 261--276. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. Distefano, D., O'Hearn, P. W., and Yang, H. 2006. A local shape analysis based on separation logic. In Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06). Lecture Notes in Computer Science, vol. 3920. Springer-Verlag, New York, 287--302. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. Emerson, E. A. and Sistla, A. P. 1993. Symmetry and model checking. In Proceedings of the International Conference in Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 697. Springer-Verlag, Berlin, Germany, 463--478. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. Engler, D. and Ashcraft, K. 2003. Racerx: Effective, static detection of race conditions and deadlocks. In Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP'03). ACM, New York, 237--252. Google ScholarGoogle ScholarDigital LibraryDigital Library
  39. Farzan, A., Chen, F., Meseguer, J., and Rosu, G. 2004. Formal analysis of java programs in javafan. In Proceedings of the International Conference in Computer-Aided Verification (CAV'04). Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 501--505.Google ScholarGoogle Scholar
  40. Fink, S., Yahav, E., Dor, N., Ramalingam, G., and Geay, E. 2006. Effective typestate verification in the presence of aliasing. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA'06). ACM, New York, 133--144. Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. Flanagan, C. and Abadi, M. 1999. Types for safe locking. In Proceedings of the 8th European Symposium on Programming Languages and Systems (ESOP'99). Springer-Verlag, Berlin, Germany, 91--108. Google ScholarGoogle ScholarDigital LibraryDigital Library
  42. Flanagan, C. and Freund, S. N. 2000. Type-based race detection for java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00). ACM, New York, 219--232. Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. Flanagan, C. and Freund, S. N. 2004. Type inference against races. In Proceedings of the 11th Annual International Symposium on Static Analysis (SAS'04). Lecture Notes in Computer Science, vol. 3148. Springer-Verlag, Berlin, Germany, 116--132.Google ScholarGoogle Scholar
  44. Flanagan, C., Freund, S. N., and Qadeer, S. 2002. Thread-modular verification for shared-memory programs. In Proceedings of the 11th European Symposium on Programming (ESOP'02). Lecture Notes in Computer Science, vol. 2305. Springer-Verlag, Berlin, Germany, 262--277. Google ScholarGoogle ScholarDigital LibraryDigital Library
  45. Flanagan, C., Freund, S. N., and Yi, J. 2008. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08). ACM, New York, 293--303. Google ScholarGoogle ScholarDigital LibraryDigital Library
  46. Flanagan, C. and Godefroid, P. 2005. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05). ACM, New York, 110--121. Google ScholarGoogle ScholarDigital LibraryDigital Library
  47. Ganai, M. K. and Gupta, A. 2008. Efficient modeling of concurrent systems in BMC. In Proceedings of the Symposium on Model Checking Software (SPIN'08). Lecture Notes in Computer Science, vol. 5156. Springer-Verlag, Berlin, Germany, 114--133. Google ScholarGoogle ScholarDigital LibraryDigital Library
  48. Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, Berlin, Germany. Google ScholarGoogle ScholarDigital LibraryDigital Library
  49. Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., and Lea, D. 2006. Java Concurrency in Practice. Addison-Wesley, Reading, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  50. Gopan, D., Reps, T., and Sagiv, M. 2005. A framework for numeric analysis of array operations. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL'05). ACM, New York, 338--350. Google ScholarGoogle ScholarDigital LibraryDigital Library
  51. Gosling, J., Joy, B., and Steele, G. 1997. The Java Language Specification. The Java Series. Addison-Wesley, Reading, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  52. Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., and Sagiv, M. 2007a. Local reasoning for storable locks and threads. In Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS'07). Lecture Notes in Computer Science, vol. 4807. Springer-Verlag, Berlin, Germany, 19--37. Google ScholarGoogle ScholarDigital LibraryDigital Library
  53. Gotsman, A., Berdine, J., Cook, B., and Sagiv, M. 2007b. Thread-modular shape analysis. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'07). ACM, New York, 266--277. Google ScholarGoogle ScholarDigital LibraryDigital Library
  54. Gotsman, A., Cook, B., Parkinson, M., and Vafeiadis, V. 2009. Proving that non-blocking algorithms don't block. In Proceedings of the 36th Annual ACM Symposium on Principles of Programming Languages (POPL'09). ACM, New York, 16--28. Google ScholarGoogle ScholarDigital LibraryDigital Library
  55. Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. Lecture Notes in Computer Science, vol. 1254, Springer-Verlag, Berlin, Germany, 72--83. Google ScholarGoogle ScholarDigital LibraryDigital Library
  56. Gueta, G., Flanagan, C., Yahav, E., and Sagiv, M. 2006. A semantics for reducing nondeterminism in concurrent programs and its applications. Technical Report TA-CS-2006-052, School of Computer Science, Tel-Aviv, Univ. Tel-Aviv, Israel. (Avialable at “http://www.cs.tau.ac.il/~msagiv/skipping.ps”.)Google ScholarGoogle Scholar
  57. Gueta, G., Flanagan, C., Yahav, E., and Sagiv, M. 2007. Cartesian partial order reduction. In Proceedings of the 14th Workshop on Model Checking Software (SPIN'07). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany. Google ScholarGoogle ScholarDigital LibraryDigital Library
  58. Havelund, K. and Pressburger, T. 2000. Model checking Java programs using Java pathfinder. Int. J. Softw. Tools Tech. Transf. 2, 4, 366--381.Google ScholarGoogle ScholarCross RefCross Ref
  59. Henzinger, T. A., Jhala, R., and Majumdar, R. 2004. Race checking by context inference. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04). ACM, New York, 1--13. Google ScholarGoogle ScholarDigital LibraryDigital Library
  60. Herlihy, M. 1991. Wait-free synchronization. ACM Trans. Programming Languages and Systems 13, 1, 124--149. Google ScholarGoogle ScholarDigital LibraryDigital Library
  61. Herlihy, M. and Shavit, N. 2008. The Art of Multiprocessor Programming. Morgan-Kaufmann, San Francisco, CA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  62. Herlihy, M. P. and Wing, J. M. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3, 463--492. Google ScholarGoogle ScholarDigital LibraryDigital Library
  63. Holzmann, G. J. 1995. Proving properties of concurrent systems with SPIN. In Proceedings of the 6th International Conference on Concurrency Theory (CONCUR'95). Lecture Notes in Computer Science, vol. 962. Springer-Verlag, Berlin, Germany, 453--455. Google ScholarGoogle ScholarDigital LibraryDigital Library
  64. IBM. 1983. IBM System/370 Extended Architecture, Principles of Operation. Publication No. SA22-7085.Google ScholarGoogle Scholar
  65. Immerman, N. 1998. Descriptive Complexity. Texts in Computer Science. Springer-Verlag, Berlin, Germany.Google ScholarGoogle Scholar
  66. Ishtiaq, S. S. and O'Hearn, P. W. 2001. Bi as an assertion language for mutable data structures. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL'01). ACM, New York, 14--26. Google ScholarGoogle ScholarDigital LibraryDigital Library
  67. Jeannet, B., Loginov, A., Reps, T. W., and Sagiv, S. 2004. A relational approach to interprocedural shape analysis. In Proceedings of the 11th International Symposium on Static Analysis, (SAS'04). Lecture Notes in Computer Science, vol. 3148. Springer-Verlag, Berlin, Germany, 246--264.Google ScholarGoogle Scholar
  68. Jones, N. and Muchnick, S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, NJ, Chapter 4, 102--131.Google ScholarGoogle Scholar
  69. Jones, N. and Muchnick, S. 1982. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Proceedings of the Symposium on the Principles of Programming Languages. ACM, New York, 66--74. Google ScholarGoogle ScholarDigital LibraryDigital Library
  70. Lahiri, S. and Qadeer, S. 2008. Back to the future: Revisiting precise program verification using SMT solvers. In Proceedings of the 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08). ACM, New York, 171--182. Google ScholarGoogle ScholarDigital LibraryDigital Library
  71. Lahiri, S. K., Qadeer, S., and Rakamari, Z. 2009. Static and precise detection of concurrency errors in systems code using SMT solvers. In Proceedings of the Symposium on Computer Aided Verification (CAV'09). Lecture Notes in Computer Science, vol. 5643. Springer-Verlag, Berlin, Germany, 509--524. Google ScholarGoogle ScholarDigital LibraryDigital Library
  72. Lal, A. and Reps, T. 2008. Reducing concurrent analysis under a context bound to sequential analysis. In Proceedings of the Symposium on Computer Aided Verification. Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 37--51. Google ScholarGoogle ScholarDigital LibraryDigital Library
  73. Lea, D. 1997. Concurrent Programming in Java. Addison-Wesley, Reading, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  74. Leino, K. R. and Müller, P. 2009. A basis for verifying multi-threaded programs. In Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP'09). Springer-Verlag, Berlin, Germany, 378--393. Google ScholarGoogle ScholarDigital LibraryDigital Library
  75. Lev-Ami, T., and Sagiv, M. 2000. TVLA: A framework for Kleene based static analysis. In Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 1824. Springer-Verlag, Berlin, Germany, 280--301. Google ScholarGoogle ScholarDigital LibraryDigital Library
  76. Lindholm, T., and Yellin, F. 1997. The Java Virtual Machine Specification. The Java Series. Addison-Wesley, Reading, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  77. Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., and Berdine, J. 2008. Heap decomposition for concurrent shape analysis. In Proceedings of the 15th International Symposium on Static Analysis (SAS'08). Lecture Notes in Computer Science, vol. 5079. Springer-Verlag, Berlin, Germany, 363--377. Google ScholarGoogle ScholarDigital LibraryDigital Library
  78. Manevich, R., Yahav, E., Ramalingam, G., and Sagiv, S. 2005. Predicate abstraction and canonical abstraction for singly-linked lists. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'05). Lecture Notes in Computer Science, vol. 3385. Springer-Verlag, Berlin, Germany, 181--198. Google ScholarGoogle ScholarDigital LibraryDigital Library
  79. Michael, M. and Scott, M. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the 15th Annual ACM Symposium on Principles of Distributed Computing (PODC '96). ACM, New York, 267--275. Google ScholarGoogle ScholarDigital LibraryDigital Library
  80. Michael, M. M. 2004. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parall. Distrib. Syst. 15, 6, 491--504. Google ScholarGoogle ScholarDigital LibraryDigital Library
  81. Moller, A. and Schwartzbach, M. I. 2001. The pointer assertion logic engine. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01). ACM, New York, 221--231. Google ScholarGoogle ScholarDigital LibraryDigital Library
  82. Moore, J. S. and Porter, G. 2002. The apprentice challenge. ACM Trans. Prog. Lang. Syst. 24, 3, 193--216. Google ScholarGoogle ScholarDigital LibraryDigital Library
  83. Naik, M., Aiken, A., and Whaley, J. 2006. Effective static race detection for java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06). ACM, New York, 308--319. Google ScholarGoogle ScholarDigital LibraryDigital Library
  84. Netzer, R., and Miller, B. 1992. What are race conditions? Some issues and formalizations. ACM Lett. Prog. Lang. Syst. 1, 1, 74--88. Google ScholarGoogle ScholarDigital LibraryDigital Library
  85. Nielson, F., Nielson, H. R., and Sagiv, M. 2000. A kleene analysis of mobile ambients. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP'00). Springer-Verlag, Berlin, Germany, 305--319. Google ScholarGoogle ScholarDigital LibraryDigital Library
  86. O'Hearn, P. W. 2007. Resources, concurrency, and local reasoning. Theoret. Comput. Sci. 375, 1-3, 271--307. (Prelim version appeared in CONCUR'04, Lecture Notes in Computer Science, vol. 3170, Springer-Verlag, Berlin, Germany, 49--67.) Google ScholarGoogle ScholarDigital LibraryDigital Library
  87. Pnueli, A., Xu, J., and Zuck, L. D. 2002. Liveness with (0, 1, infty)-counter abstraction. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02). Springer-Verlag, Berlin, Germany, 107--122. Google ScholarGoogle ScholarDigital LibraryDigital Library
  88. Prakash, S., Lee, Y., and Johnson, T. 1991. A non-blocking algorithm for shared queues using Compare-and-Swap. In Proceedings of the International Conference on Parallel Processing. CRC Press, 68--75.Google ScholarGoogle Scholar
  89. Pratikakis, P., Foster, J., and Hicks, M. 2006. Locksmith: Context-sensitive correlation analysis for race detection. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI'06). ACM, New York, 320--331. Google ScholarGoogle ScholarDigital LibraryDigital Library
  90. Qadeer, S. and Rehof, J. 2005. Context-bounded model checking of concurrent software. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3440. Springer-Verlag, Berlin, Germany, 93--107. Google ScholarGoogle ScholarDigital LibraryDigital Library
  91. Reps, T., Sagiv, M., and Loginov, A. 2003. Finite differencing of logical formulas for static analysis. In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 2618. Springer-Verlag, Berlin, Germany. Google ScholarGoogle ScholarDigital LibraryDigital Library
  92. Reps, T. W., Sagiv, M., and Wilhelm, R. 2004. Static program analysis via 3-valued logic. In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 401--404.Google ScholarGoogle Scholar
  93. Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA. 55. Google ScholarGoogle ScholarDigital LibraryDigital Library
  94. Rinetskey, N. and Sagiv, M. 2001. Interprocedural shape analysis for recursive programs. In Proceedings of the International Conference on Compiler Construction, Lecture Notes in Computer Science, vol. 2027. Springer-Verlag, Berlin, Germany, 133--149. Google ScholarGoogle ScholarDigital LibraryDigital Library
  95. Rinetzky, N. 2008. Interprocedural and modular local heap shape analysis. Ph.D. dissertation, Tel-Aviv Univ. Tel-Aviv Isreal.Google ScholarGoogle Scholar
  96. Sagiv, M., Reps, T., and Wilhelm, R. 1998. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst. 20, 1, 1--50. Google ScholarGoogle ScholarDigital LibraryDigital Library
  97. Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst. 24, 3, 217--298. Google ScholarGoogle ScholarDigital LibraryDigital Library
  98. Saidi, H. 2000. Model checking guided abstraction and analysis. In Proceedings of the 7th International Symposium on Static Analysis (SAS'00). Springer-Verlag, Berlin, Germany, 377--396. Google ScholarGoogle ScholarDigital LibraryDigital Library
  99. Shaham, R., Yahav, E., Kolodner, E. K., and Sagiv, M. 2003. Establishing local temporal heap safety properties with applications to compile-time memory management. In Proceedings of the 10th International Static Analysis Symposium (SAS'03). Lecture Notes in Computer Science, vol. 2694. Springer-Verlag, Berlin, Germany. Google ScholarGoogle ScholarDigital LibraryDigital Library
  100. Silberschatz, A. and Galvin, P. B. 1994. Operating Systems Concepts, 4 Ed. Addison-Wesley, Reading, MA. Google ScholarGoogle ScholarDigital LibraryDigital Library
  101. Sterling, N. 1993. Warlock—A static data race analysis tool. In USENIX Technical Conference Proceedings. ACM, New York, 97--106.Google ScholarGoogle Scholar
  102. Stoller, S. 2000. Model-checking multi-threaded distributed Java programs. In Proceedings of the 7th International SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 1885. Springer-Verlag, Berlin, Germany, 224--244. Google ScholarGoogle ScholarDigital LibraryDigital Library
  103. Stone, J. M. 1990. A simple and correct shared-queue algorithm using compare-and-swap. In Proceedings of the Conference on Supercomputing (Supercomputing'90). IEEE Computer Society Press, Los Alamitos, CA, 495--504. Google ScholarGoogle ScholarDigital LibraryDigital Library
  104. Stone, J. M. 1992. A non-blocking Compare-and-Swap algorithm for a shared circular queue. In Proceedings of the Parallel and Distributed Computing in Engineering Systems. Elsevier Science Publishers, Amsterdam, The Netherlands, 147--152.Google ScholarGoogle Scholar
  105. Strom, R. and Yemini, S. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng. 12, 1, 157--171. Google ScholarGoogle ScholarDigital LibraryDigital Library
  106. Strom, R. E. 1983. Mechanisms for compile-time enforcement of security. In Proceedings of the 10th ACM Symposium on Principles of Programming Languages (POPL'83). ACM, New York, 276--284. Google ScholarGoogle ScholarDigital LibraryDigital Library
  107. Vafeiadis, V. 2008. Modular fine-grained concurrency verification. Ph.D. dissertation, University of Cambridge, Computer Laboratory. Also available as technical report UCAM-CL-TR-726.Google ScholarGoogle Scholar
  108. Vafeiadis, V. 2009. Shape-value abstraction for verifying linearizability. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 5403. Springer-Verlag, Berlin, Germany, 335--348. Google ScholarGoogle ScholarDigital LibraryDigital Library
  109. Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., and Co, P. 1999. Soot - A java optimization framework. In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collabrative Research. IBM, 125--135. Google ScholarGoogle ScholarDigital LibraryDigital Library
  110. Valmari, A. 1991. Stubborn sets for reduced state space generation. In Proceedings of the Conference on Advances in Petri Nets 1990. Lecture Notes in Computer Science, vol. 483. Springer-Verlag, Berlin, Germany, 491--515. Google ScholarGoogle ScholarDigital LibraryDigital Library
  111. Vechev, M., and Yahav, E. 2008. Deriving linearizable fine-grained concurrent objects. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'08). ACM, New York, 125--135. Google ScholarGoogle ScholarDigital LibraryDigital Library
  112. Vechev, M., Yahav, E., Bacon, D. F., and Rinetzky, N. 2007. CGCExplorer: A semi-automated search procedure for provably correct concurrent collectors. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'07). ACM, New York, 456--467. Google ScholarGoogle ScholarDigital LibraryDigital Library
  113. Vechev, M., Yahav, E., and Yorsh, G. 2009. Experience with model checking linearizability. In Proceedings of the 16th International SPIN Workshop on Model Checking Software. Springer-Verlag, Berlin, Germany, 261--278. Google ScholarGoogle ScholarDigital LibraryDigital Library
  114. Vermeulen, A. 1997. Java deadlock: The woes of multithreaded design. Dr. Dobb's J. Softw. Tools 22, 9, 52, 54--56, 88, 89.Google ScholarGoogle Scholar
  115. Wing, J. M. and Gong, C. 1990. A library of concurrent objects and their proofs of correctness. Tech. rep. CMU--CS--90--151, CMU.Google ScholarGoogle Scholar
  116. Yahav, E. 2000. 3VMC user's manual. Available at http://www.math.tau.ac.il/~yahave.Google ScholarGoogle Scholar
  117. Yahav, E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 27--40. Google ScholarGoogle ScholarDigital LibraryDigital Library
  118. Yahav, E. and Ramalingam, G. 2004. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, New York, 25--34. Google ScholarGoogle ScholarDigital LibraryDigital Library
  119. Yahav, E., and Sagiv, M. 2003. Automatically verifying concurrent queue algorithms. Electronic Notes in Theoretical Computer Science, vol. 89. Elsevier, Amsterdam, The Netherlands.Google ScholarGoogle Scholar
  120. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., and O'Hearn, P. 2008. Scalable shape analysis for systems code. In Proceedings of the Conference on Aided Verification. Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 385--398. Google ScholarGoogle ScholarDigital LibraryDigital Library
  121. Zee, K., Kuncak, V., and Rinard, M. 2008. Full functional verification of linked data structures. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08). ACM, New York, 349--361. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Verifying safety properties of concurrent heap-manipulating programs

                          Recommendations

                          Comments

                          Login options

                          Check if you have access through your login credentials or your institution to get full access on this article.

                          Sign in

                          Full Access

                          • Published in

                            cover image ACM Transactions on Programming Languages and Systems
                            ACM Transactions on Programming Languages and Systems  Volume 32, Issue 5
                            May 2010
                            168 pages
                            ISSN:0164-0925
                            EISSN:1558-4593
                            DOI:10.1145/1745312
                            Issue’s Table of Contents

                            Copyright © 2008 ACM

                            Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                            Publisher

                            Association for Computing Machinery

                            New York, NY, United States

                            Publication History

                            • Accepted: 1 October 2009
                            • Published: 24 May 2008
                            • Revised: 1 October 2007
                            • Received: 1 September 2007
                            Published in toplas Volume 32, Issue 5

                            Permissions

                            Request permissions about this article.

                            Request Permissions

                            Check for updates

                            Qualifiers

                            • research-article
                            • Research
                            • Refereed

                          PDF Format

                          View or Download as a PDF file.

                          PDF

                          eReader

                          View online with eReader.

                          eReader