Enforcing object protocols by combining static and runtime analysis

ABSTRACT

In this paper, we consider object protocols that constrain interactions between objects in a program. Several such protocols have been proposed in the literature. For many APIs (such as JDOM, JDBC), API designers constrain how API clients interact with API objects. In practice, API clients violate such constraints, as evidenced by postings in discussion forums for these APIs. Thus, it is important that API designers specify constraints using appropriate object protocols and enforce them. The goal of an object protocol is expressed as a protocol invariant. Fundamental properties such as ownership can be expressed as protocol invariants. We present a language, PROLANG, to specify object protocols along with their protocol invariants, and a tool, INVCOP++, to check if a program satisfies a protocol invariant. INVCOP++ separates the problem of checking if a protocol satisfies its protocol invariant (called protocol correctness), from the problem of checking if a program conforms to a protocol (called program conformance). The former is solved using static analysis, and the latter using runtime analysis. Due to this separation (1) errors made in protocol design are detected at a higher level of abstraction, independent of the program's source code, and (2) performance of conformance checking is improved as protocol correctness has been verified statically. We present theoretical guarantees about the way we combine static and runtime analysis, and empirical evidence that our tool INVCOP++ finds usage errors in widely used APIs. We also show that statically checking protocol correctness greatly optimizes the overhead of checking program conformance, thus enabling API clients to test whether their programs use the API as intended by the API designer.

REFERENCES

• 1: AspectJ -- http://www.eclipse.org/aspectj/.
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 3: M. Barnett, R. DeLine, M. Fähndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. JOT, 3(6):27--56, 2004.
• 4: M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 04: Construction and Analysis of Safe, Secure and Interoperable Smart devices, LNCS 3362. Springer Verlag, 2004.
• 5: M. Barnett and D. A. Naumann. Friends need a bit more: Maintaining invariants over shared state. In MPC, pages 54--84. Springer-Verlag, 2004.
• 6: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-223, January 15-17, 2003, New Orleans, Louisiana, USA
• 7: Feng Chen , Grigore Roşu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 8: Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 9: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 10: http://www.servlets.com/archive/servlet/ReadMsg?msgId=539019&listName=jdom-interest.
• 11: http://bugs.mysql.com/bug.php?id=2054.
• 12: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 13: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 14: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 15: Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146254]
• 16: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 17: Martin Fowler, Analysis patterns: reusable objects models, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 18: M. Gopinathan and S. Rajamani. Runtime monitoring of object invariants with guarantee. In RV '08: Runtime Verification, LNCS 5289. Springer, 2008.
• 19: Richard Helm , Ian M. Holland , Dipayan Gangopadhyay, Contracts: specifying behavioral compositions in object-oriented systems, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.169-180, September 1990, Ottawa, Canada
• 20: Ciera Jaspan , Jonathan Aldrich, Checking framework plugins, Companion to the 22nd ACM SIGPLAN conference on Object oriented programming systems and applications companion, October 21-25, 2007, Montreal, Quebec, Canada [doi>10.1145/1297846.1297892]
• 21: http://archives.postgresql.org/pgsql-jdbc/2003--10/msg00062.php.
• 22: http://java.sun.com/products/jdbc/download.html#corespec40.
• 23: JDOM -- http://www.jdom.org.
• 24: JDOM FAQ -- http://www.jdom.org/docs/faq.html#a0390.
• 25: G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. V. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. In ECOOP, pages 220--242, 1997.
• 26: G. Leavens and Y. Cheon. Design by contract with jml, 2003.
• 27: http://people.csa.iisc.ernet.in/gmadhu/oopsla.
• 28: MySQL -- http://www.mysql.com.
• 29: http://java.sun.com/javase/6/docs/platform/serialization/spec/security.html#4271.
• 30: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools

General Terms:
Design, Languages, Reliability, Verification

Keywords:
aspect oriented programming, invariants, program verification