Eran Yahav
ABSTRACT
We provide a parametric framework for verifying safety properties of concurrent Java programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to error-detection algorithms that are more precise than existing techniques. The framework also provides the most precise shape-analysis algorithm for concurrent programs. In contrast to existing verification techniques, we do not put a bound on the number of allocated objects. The framework even produces interesting results when analyzing Java 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 [19]. •The program does not perform inconsistent updates due to interference. •The program does not reach a deadlock. •The program does not produce run-time errors due to illegal thread interactions. We also find bugs in erroneous versions of such implementations. A prototype of our framework has been implemented.
- 1.J. Aldrich, C. Chambers, E. Sirer, and S. Eggers. Static analyses for eliminating unnecessary synchronization from Java programs. In A. Cortesi and G. Fil~, editors, Static Analysis, volume 1694 of Lecture Notes in Computer Science, pages 19-38. Springer, 1999.]] Google Scholar
Digital Library
- 2.R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, Sept. 1992.]] Google ScholarDigital Library
- 3.R. E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. Technical Report CS-92-160, Carnegie Mellon University, School of Computer Science, July 1992.]] Google ScholarDigital Library
- 4.L. Cardelli and A.D.Gordon. Mobile ambients. In Proc. FoSSaCS'98, vol. 1378 of LNCS, pages 140-155. Springer, 1998.]] Google Scholar
- 5.D. Chase, M. VVegman, and F. Zadeck. Analysis of pointers and structures. In SIGPLAN Conf. on Prog. Lang. Design and lmpl., pages 296-310, New York, NY, 1990. ACM Press.]] Google ScholarDigital Library
- 6.E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512-1542, Sept. 1994.]] Google ScholarDigital Library
- 7.E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.]] Google ScholarDigital Library
- 8.E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks. A CM Transactions on Programming Languages and Systems, 19(5):726-750, Sept. 1997.]] Google ScholarDigital Library
- 9.J. Corbett. Using shape analysis to reduce finite-state models of concurrent java programs. Oct. 1998.]]Google Scholar
- 10.J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, R. Shawn, and L. Hongjun. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd Int. Conf. on Soft. Eng. (ICSE), June 2000.]] Google ScholarDigital Library
- 11.P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Symp. on Princ. of Prog. Lang., pages 238-252, New York, NY, 1977. ACM Press.]] Google ScholarDigital Library
- 12.P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Symp. on Princ. of Prog. Lang., pages 269-282, New York, NY, 1979. ACM Press.]] Google ScholarDigital Library
- 13.C. Demartini, R. Iosif, and R. Sisto. A deadlock detection tool for concurrent Java programs. Software: Practice and Experience, 29(7):577-603, June 1999.]] Google ScholarDigital Library
- 14.C. Demartini, R. Iosif, and R. Sisto. dSPIN : A dynamic extension of SPIN, Sept. 1999.]]Google Scholar
- 15.E. Emerson and A. P. Sistla. Symmetry and model checking. In C. Courcoubetis, editor, Proc. of The Fifth Workshop on Computer-Aided Verificaton, June/July 1993.]] Google ScholarDigital Library
- 16.C. Flanagan and S. Freund. Type-based race detection for java. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation, June 2000.]] Google ScholarDigital Library
- 17.J. Gosling, B. Joy, and G. Steele. The Java Language Specification. The Java Series. Addison-VVesley, 1997.]] Google ScholarDigital Library
- 18.K. Havelund and T. Pressburger. Model checking Java programs using Java pathfinder. Int. Journal on Software Tools for Technology Transfer (STTT), 2(4), Apr. 2000.]]Google Scholar
- 19.C. Hoare. Recursive data structures. Int. J. of Comp. and Inf. Sci., 4(2):105-132, 1975.]]Google ScholarCross Ref
- 20.G. J. Holzmann. Proving properties of concurrent systems with SPIN. In Proc. of the 6th Int. Conf. on Concurrency Theory (CONCUR '95), volume 962 of LNCS, pages 453-455, Berlin, GER, Aug. 1995. Springer.]] Google ScholarDigital Library
- 21.G. J. Holzmann and D. Peled. An improvement in formal verification. In Proc. Formal Description Techniques, FORTEg,, pages 197-211, Berne, Switzerland, Oct. 1994. Chapman Hall.]] Google Scholar
- 22.A. Knapp, P. Cenciarelli, B. Reus, and M. Wirsing. An event-based structural operational semantics of multi-threaded java, 1998.]]Google Scholar
- 23.D. Lea. Concurrent Programming in Java. Addison-Wesley, Reading, Massachusetts, 1997.]] Google ScholarDigital Library
- 24.T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In SAS'00, Static Analysis Symposium. Springer, 2000. Available at http://www.math.tan.ac.il/~tla.]]Google ScholarDigital Library
- 25.T. Lindholm and F. Yellin. The Java Virtual Machine Specification. The Java Series. Addison-VVesley, Reading, MA, USA, Jan. 1997.]] Google ScholarDigital Library
- 26.S. Masticola and B. Ryder. Non-concurrency analysis. ACM SIGPLAN Notices, 28(7):129-138, July 1993.]] Google ScholarDigital Library
- 27.M. Michael and M. Scott. 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), pages 267-275, New York, USA, May 1996. ACM.]] Google ScholarDigital Library
- 28.G. Naumovich and G. Avrunin. A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In Proceedings of the ACM SIGSOFT 6th International Symposium on the Foundations of Software Engineering (FSE-98), volume 23, 6 of Software Engineering Notes, pages 24-34, New York, Nov. 3-5 1998. ACM Press.]] Google ScholarDigital Library
- 29.G. Naumovich, G. Avrunin, and L. Clarke. Data flow analysis for checking properties of concurrent Java programs. In Proc. of the 1999 Int. Conf. on Soft. Eng., pages 399-410. IEEE Computer Society Press / ACM Press, 1999.]] Google ScholarDigital Library
- 30.R. Netzer and B. Miller. What are race conditions? some issues and formalizations. ACM Letters on Programming Languages and Systems, 1(1):74-88, Mar. 1992.]] Google ScholarDigital Library
- 31.F. Nielson, H. R. Nielson, and M. Sagiv. A Kleene analysis of mobile ambients. In Proceedings of ESOP '2000, 2000.]] Google ScholarDigital Library
- 32.N. Rinetskey. Interprocedural shape analysis for recursive programs. Master's thesis, Technion, Israel, 2000. Available at http://www.cs.technion.ac.il/maon/.]]Google Scholar
- 33.R. Rugina and M. Rinard. Pointer analysis for multithreaded programs. In Proceedings of the ACM SIGPLAN '99 Conference on Programming Language Design and Implementation, pages 77-90, Atlanta, Georgia, May 1-4, 1999.]] Google ScholarDigital Library
- 34.M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Syrup. on Princ. of Prog. Lang., 1999.]] Google ScholarDigital Library
- 35.H. Saidi. Model checking guided abstraction and analysis. In Proceedings of the 7th International Static Analysis Symposium (SAS '00), 2000.]] Google ScholarDigital Library
- 36.A. Silberschatz and P. B. Galvin. Operating Systems Concepts. Addison-Wesley, Reading, 4 edition, 1994.]] Google ScholarDigital Library
- 37.S. Stoller. Model-checking multi-threaded distributed Java programs. In Proc. of the 7th International SPIN Workshop on Model Checking of Software, volume 1885 of Lecture Notes in Computer Science, pages 224-244. Springer-Verlag, Aug. 2000.]] Google ScholarDigital Library
- 38.C. Ungureanu and S. Jagannathan. Concurrency analysis for java. In Proceedings of the 7th International Static Analysis Symposium (5.45 '00), 2000.]] Google ScholarDigital Library
- 39.A. Vermeulen. Java deadlock: The woes of multithreaded design. Dr. Dobb's Journal of Software Tools, 22(9):52, 54-56, 88, 89, Sept. 1997.]]Google Scholar
- 40.E. Yahav. 3VMC user's manual, 2000. Available at http://www.math.tan.ac.il/~yahave.]]Google Scholar
Index Terms
- Verifying safety properties of concurrent Java programs using 3-valued logic
Recommendations
Verifying safety properties of concurrent Java programs using 3-valued logic
We provide a parametric framework for verifying safety properties of concurrent Java programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to error-detection algorithms that are more ...
Verifying safety properties of concurrent heap-manipulating programs
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 ...
Verifying concurrent programs: tutorial talk
FMCAD '11: Proceedings of the International Conference on Formal Methods in Computer-Aided DesignThe proliferation of multi-core hardware has led to widespread use of concurrent programs. However, these programs are notoriously difficult to get right and to debug for developers. Even for automated verification, it is a big challenge to reason about ...
Comments