Pluralism: API Protocol Compliance
in Object-Oriented Software

Kevin Bierhoff, Carnegie Mellon University, http://www.cs.cmu.edu/~kbierhof/

Academic advisor: Jonathan Aldrich

Graduate category, first place at OOPSLA 2008

Overview

A number of type systems have been proposed for enforcing API protocols—such as reading only from open files—statically at compile-time. But studies of Java standard library APIs show that existing type-based approaches are inadequate for capturing common protocols and therefore unable to enforce them. My work on Pluralism proposes a novel abstraction, access permissions, which allow succinctly capturing and soundly enforcing common object-oriented API protocols due to their ability to capture assumptions about aliasing. Based on access permissions, I built an automated protocol checking tool, Plural, for conventional Java code. Case studies show that open-source software can be checked with few false positives and that Plural adds precision to an existing state-of-the-art protocol checker.

Problem and Motivation

Software development today heavily relies on reusable APIs (Application Programming Interfaces) that provide services such as access to relational databases. Many of these APIs define usage protocols that API clients must follow in order to allow the API implementation to work correctly. Protocols, loosely speaking, restrict the order in which an API can perform the operations it provides.

The Java Database Connectivity (JDBC) API will serve as a running example. JDBC is part of the Java standard library and defines a set of interfaces that are widely used in Java programs to access relational databases using SQL commands. In particular, JDBC includes the interfaces “Connection” and “ResultSet”, which roughly have the following—informally documented—protocol. A Connection object can only execute SQL queries when “open”. Running an SQL query will return a ResultSet object for inspecting the query result. Its protocol is shown in Figure 1. The “next” operation can be used to iterate over the result’s rows (tuples). This operation will return true if the result set was advanced to a valid row and false if the end of the result was reached. Column values can be retrieved from valid rows (e.g., using getInt), but attempts to retrieve column values in the “end” state violate the protocol for ResultSet. Furthermore, a result set can only be used until the connection it was created on is closed.

Figure 1: Simplified JDBC ResultSet protocol as hierarchical state machine.

Protocols are often unavoidable, for instance when APIs depend on stateful resources, or at least desirable, for example in the interest of efficient implementation. But the fact that protocols have to be followed also creates challenges including the following:

1. Using an unfamiliar API may require painful “trial-and-error” attempts at writing sample programs until a sequence of operations exercising the API is found that seemingly works. Depending on their quality, available API documentation and source code may help or hurt in this quest, and an API implementation may or may not produce useful runtime error messages when protocols are violated at.

2. It may be hard to ensure that even small changes to existing code do not violate API protocols, greatly complicating software maintenance tasks.

3. Protocols also complicate the implementation of APIs because protocol violations can lead to unsafe states which a malicious attacker may be able exploit.

In short, protocols represent a significant barrier to software re-use, a key mechanism for building the ever-larger systems we have come to rely upon.

The goal of my work on Pluralism is to help overcome this barrier by aiding developers in understanding APIs, by giving them assurance that API protocols are followed, and by helping API developers implement dependable APIs. Assurance here means soundness, i.e., finding all possible protocol violations. In order to be applicable to large codebases and to support developers while they write or maintain code (rather than with after-the-fact checks), protocol checking should be automated (instead of relying on manual proofs) and modular (consider a piece of code separately from the rest of the program).

Ensuring API protocol compliance statically at compile-time is an in general undecideable problem. It is complicated by object aliasing (objects being referenced and possibly updated from multiple places)—the hallmark feature of imperative languages like C and Java. In particular, aliasing makes it very hard to keep a sound modular analysis precise (report few false positives), because the analysis may have to constantly make conservative assumptions in order to take interference through possible aliases into account. My work, like most previous work, assumes that threads are correctly synchronized, but aliasing still permits interference during every method call (because the callee could have access to the same objects as the caller). To avoid this problem, previous modular protocol checkers have imposed strong restrictions on how the program is allowed to alias objects (Bierhoff & Aldrich, 2007).

But my studies of APIs in the Java standard library show, somewhat surprisingly, that aliasing-related challenges go deeper (Bierhoff et al, 2009): API objects often depend on each other, which can be seen as aliasing inherent in the API. An example is the mentioned dependency of JDBC ResultSet objects on “their” connection to remain open. Notice that multiple result sets can depend on the same connection (Figure 2): we can think of the result sets as aliasing the common connection object. Similar dependencies can be found in several other Java standard library APIs (Bierhoff et al, 2009) including the Collections API. Previous automated modular protocol checkers are to my knowledge unable to express such object dependencies sufficiently, making them inadequate for enforcing practical protocols such as for JDBC. I will refer to this challenging pattern as “dependent objects”.

Figure 2: Dependent objects in JDBC: multiple result sets depend on a single connection to remain open.

My work on Pluralism (Permissions Let Us Reason about ALiasing In a Static Manner) proposes the use of a novel abstraction, access permissions, for both expressing and enforcing API protocols. Access permissions afford a great deal of flexibility in aliasing objects. As it turns out, this flexibility enables encoding the dependencies between objects found in several commonly used APIs. My tool Plural statically checks compliance to API protocols by tracking access permissions through Java code with annotation burden that is comparable to conventional typing information.

Background and Related Work

A plethora of approaches for expressing and statically enforcing API protocols have been proposed in the literature. Some, like Plural, are based on typestates (Strom & Yemini, 1986), such as Vault and Fugue (DeLine & Fähndrich, 2001, 2004), but other formalisms have been used as well. Many of these systems are designed to be modular; others are designed or at least implemented as whole-program analyses. Modular approaches are often proven sound and shown to work on well-known examples such as file access. But implementations and empirical studies are rare (Vault and Fugue being notable exceptions). Existing modular systems have in common that their support for aliasing is limited, hence their inability to express dependent objects.

In contrast, whole-program protocol analyses (most recently, approaches based on “Tracematches”) are typically implemented and empirically evaluated, often on a sizeable number of open-source programs. Many are intended to be, but with few exceptions not proven, sound. Tracematches, a protocol specification technique underlying several recent whole-program protocol checkers such as Bodden et al (2008), is the only existing mechanism that I am aware of that can express the dependent objects pattern.

In addition, automated program verification tools such as the Jave Modeling Language (JML), Spec#, or JStar can be used for checking protocols. But these approaches typically incur much higher overhead for developers due to the use of theorem provers. Sound modular checking of JML and Spec# specifications is based on ownership, which only allows one object (the “owner”) to depend on another one. By contrast, multiple result sets can depend on a single connection in JDBC. JStar and other approaches based on separation logic capture explicit sharing, but this is unsatisfying for JDBC: the shared connection would have to be passed around explicitly between its conceptually independent result sets. Furthermore, automated reasoning about separation logic is still a largely open problem.

Approach and Uniqueness

Protocols in Pluralism are defined with hierarchical state machines such as the one visualized in Figure 1. Ultimately, a tool like Plural needs to determine, for every program point, the current state of API objects in scope, which has been called their current typestate (Strom & Yemini, 1986). Using hierarchical instead of flat state machines improves the succinctness of protocol specifications in many cases (Bierhoff & Aldrich, 2005).

Pluralism is enabled by access permissions. Access permissions encode common patterns for aliasing objects, enabling sound and modular verification of program behavior in the presence of aliasing. Access permissions are tokens associated with object references that govern access to the referenced object. The key insight of permissions is that we do not care how many aliases there are to a given reference or where in the program they reside. We just need to know whether aliases exist and what they may do to the referenced object. Therefore, instead of tracking exactly which program references may alias a given object—which is hard to do modularly and precisely in general—access permissions summarize possible effects of all aliases from the perspective of the current reference. Compared to previous work on protocol enforcement, two insights went into the design of access permissions:

1. Aliases to a given reference pose no threat in single-threaded programs as long as they do not modify an object’s state. Thus, we can reason about permissions that guarantee the absence of modifications through other aliases roughly as if there were no other aliases. (This idea is also exploited in ownership-based approaches.) Accordingly, all other references will be associated with permissions granting read-only access to the object. The following table summarizes the different kinds of permissions, what access they grant to the current reference, and what assumptions can be made about other permissions

Permission kind	This reference can…	Other references can…	Other permissions for the same object permitted
Unique	Modify	not have any access	None
Full	modify	read-only	Pure
Share	modify	modify	Share, Pure
Immutable	read-only	read-only	Immutable, Pure
Pure	read-only	Modify	Full, Share, Immutable, Pure

2. Permissions can guarantee that an object remains in a given state, called the “state guarantee”. For instance, this allows encoding the dependency of result sets on a (guaranteed) “open” connection. State guarantees can also be exploited to keep access to orthogonal parts of an object’s state separate.

Permissions can be split when aliases are introduced. For example, we can split a Unique permission into a Full and a Pure permission to introduce a read-only alias. Using fractions (Boyland, 2003) we can also merge previously split permissions when aliases disappear (e.g., when a method returns). The key to soundness is to make sure that permissions are split in such a way that two permissions for the same object never make contradictory assumptions. For example, a Unique permission must not be split into two Full permissions, as both assume that no other Full permission exists.

Permissions hence enable what was previously impossible: fully modular and nonetheless sound static reasoning about the possibly-changing typestate of aliased objects. This allows assuring protocol compliance like a typechecker: we can check partial programs (such as unfinished code or a library) and do not have to re-check an entire program after every change to it. Roughly, soundness guarantees the absence of protocol violations at runtime if the entire program passes the typechecker.

But I did not stop with a system that works on paper. I wanted to demonstrate that permissions can be a useful addition to a programming environment for a conventional programming language. Therefore, Nels Beckman and I developed a tool, Plural, that can automatically check Java programs for protocol compliance as part of Eclipse’s Java development environment. (Plural is available open-source at http://code.google.com/p/pluralism/.) Plural defines a set of Java annotations that API designers can use to declare API protocols based on permissions directly in API source files (Figure 3). For instance, the ResultSet method close (Figure 3) requires a Full permission in any state and returns it in the “closed” state.

public interface ResultSet {

@Full(guarantee = "open")

@TrueIndicates("unread")

@FalseIndicates("end")

boolean next();

@Full(guarantee = "valid", ensures = "read")

int getInt(int column);

@Pure(guarantee = "read")

boolean wasNull();

@Full(ensures = "closed")

void close(); ... }

Figure 3: Simplified JDBC ResultSet protocol specification with Plural.

Plural can then check API client programs against the declared protocols. Plural checks individual methods in a fully automated fashion using a dataflow analysis that tracks permissions through the code and infers loop invariants as well. A key challenge is inferring permission splits and merges, which Plural achieves by collecting constraints over the permissions needed for calling methods and ensuring that these constraints remain consistent (Bierhoff, 2009). The annotations for declaring API protocols can also be placed on method parameters. This allows Plural to be modular because its analysis “trusts” annotations on called methods and checks their bodies separately.

I specified protocols for a number of sizeable APIs from the Java standard library and used Plural to check these protocols in open-source codebases with promising precision, especially when objects are long-lived or otherwise aliased, while keeping the annotation overhead to the extent of conventional typing information. As such, my work on Pluralism attempts to combine the advantages of modular and whole-program protocol analyses without incurring the overhead (or automation challenges) of program verification tools.

Results and Contributions

Contributions of this work include the following:

· The novel abstraction of access permissions and here in particular “full” and “pure” permissions as well as state guarantees.

· A formalization of a linear dependent type system based on access permissions, a fragment of which I proved sound for single-threaded programs (Bierhoff & Aldrich, 2007). (Beckman et al, 2008, prove that access permissions are sound in concurrent programs as well.)

· A prototype tool (Plural) demonstrating that access permissions can be automatically tracked in conventional Java code based on annotations that have the “size and feel” of conventional typing annotations. What I mean here is that method parameters are annotated with the permission needed for it, such as @Full for a parameter with a “full” permission.

· Protocol specifications for parts of the Java standard library APIs for Collections, JDBC, regular expressions, and exceptions using Plural annotations (Bierhoff et al, 2009). Specifying these APIs required about 2 annotations per method and is relatively straightforward because of their extensive informal documentation (which is many times longer than the annotations I provided).

· The identification of three challenging API protocol patterns (Bierhoff et al, 2009) including “dependent objects” (discussed throughout). With permissions, these dependencies could be specified using state guarantees and “immutable” permissions, while previous automated modular approaches are too restrictive to even specify such dependencies.

· Plural was used to check for compliance to these API protocols in two open-source code bases, Apache Beehive and PMD:

o The considered 2KLOC in Beehive use all of the specified APIs and I added about 1 annotation per method to check compliance to them. Plural exposed two “issues” (albeit no bugs) and produces 5 false positives (Bierhoff et al, 2009).

o The use of Plural in PMD allows comparing Plural to a state-of-the-art protocol analysis based on Tracematches (Bodden et al, 2008). Bodden used Tracematches to check that Java collections (lists and sets) are not modified while iterated, commonly referred to as “concurrent modification” (CM). CM is an example of dependent objects because many iterators can depend on a single collection. I used Plural to check CM in about 9KLOC of PMD, for which Bodden’s analysis flags 51 false positives. Plural can rule out these false positives (7 of them conditional on unchecked code or other warnings) after adding about 0.5 annotations per method to PMD. Plural flags 46 false positives of its own, which are partially due to the fact that Bodden’s analysis did not check Java maps for CM (only sets and lists), while Plural did (Bierhoff, 2009). I believe that many of these false positives could be removed with improved tooling.

These results suggest that Pluralism gives sufficient flexibility for specifying real APIs and that it can be used to assist developers in their tasks. The overhead of providing annotations is at the level of conventional Java type information while enabling analysis precision that promises not to overwhelm developers with false positives. Reasoning about objects from different APIs is largely orthogonal, providing a graceful path for introducing the tool into an existing codebase. Finally, considering their relatively small overhead, annotations on APIs can be realistically provided by the API designers and would increase the precision with which these APIs are defined. Therefore, I believe that Pluralism is a significant step towards practical adoption of automatic API protocol enforcement techniques.

References

N. E. Beckman, K. Bierhoff, and J. Aldrich. Verifying Correct Usage of Atomic Blocks and Typestate. In ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, Nashville, TN, USA, pages 227-244. ACM Press, New York, October 2008.

K. Bierhoff. API Protocol Compliance in Object-Oriented Software. Ph.D. thesis, Carnegie Mellon University School of Computer Science. Technical Report CMU-ISR-09-108, 2009.

K. Bierhoff and J. Aldrich. Lightweight Object Specification with Typestates. In Joint European Software Engineering Conference and ACM Symposium on the Foundations of Software Engineering, Lisbon, Portugal, pp. 217-226. ACM Press, New York, September 2005.

K. Bierhoff and J. Aldrich. Modular Typestate Checking of Aliased Objects. In ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, Montreal, Canada, pages 301-320. ACM Press, New York, October 2007.

K. Bierhoff, N. E. Beckman, and J. Aldrich. Practical API Protocol Checking with Access Permissions. In European Conference on Object-Oriented Programming, Genova, Italy. Springer, to appear, July 2009.

R. DeLine & M. Fähndrich. Enforcing high-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation, pages 59–69. ACM Press, New York, 2001.

R. DeLine & M. Fähndrich. Typestates for objects. In European Conference on Object-Oriented Programming, pages 465–490. Springer, 2004.

E. Bodden, P. Lam, and L. Hendren. Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In ACM Symposium on the Foundations of Software Engineering, pages 36–47. ACM Press, New York, November 2008.

R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12:157–171, 1986.