Types for Correct Concurrent API Usage

摘要

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.