This thesis represents an attempt to improve the state of the art in our ability to understand and check object protocols, with a particular emphasis on concurrent programs. Object protocols are the patterns of use imposed on clients of APIs in object-oriented programs. We show through an empirical study of open-source object-oriented programs that object protocols are quite common. We then present "Sync-or-Swim," a methodology and suite of accompanying tools for checking at compile-time that object protocols are used and implemented correctly. This methodology is based upon the existing access permissions method of alias control, which is here extended to be sound in the face of shared-memory concurrency. The analysis is formalized as a type system for an object-oriented calculus, and then proven to be free from false-negatives using a proof of type safety. The type system is extended with parametric polymorphism, or "generics," in order to increase its ability to check commonly occurring patterns. An implementation of the approach, a static analysis for programs written in the Java programming language, is presented. This implementation was used to perform a series of case studies whose goal was to evaluate the ease of use, expressiveness and ability to verify commonly occurring patterns. These case studies are presented. Next, an approach and an associated tool for inferring access permission annotations is presented. This inference tool can reduce the burden of using our protocol-checking approach by automatically inferring the required typing annotations. This inference is built upon a system of probabilistic constraints, which allows the easy encoding of heuristics. Finally, an optimization of software transactional memory runtimes is presented. This optimization is enabled by the typing annotations required to use the concurrent protocol checker and can remove some of the overhead typically associated with transactional memory systems. As a result of the work presented in this thesis, it is possible to guarantee the absence of certain API usage errors even in concurrent programs, and to do so with a low burden on programmers. By adhering to such an approach, programmers can produce more reliable software.

253 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu