kevin bierhoff

Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierhoff.  A Type System for Borrowing Permissions.  In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12), Philadelphia, PA, USA, pages 557-570.  ACM Press, New York, January 2012.

Abstract.  In object-oriented programming, unique permissions to object references are useful for checking correctness properties such as consistency of typestate and noninterference of concurrency. To be usable, unique permissions must be borrowed--for example, one must be able to read a unique reference out of a field, use it for something, and put it back. While one can null out the field and later reassign it, this paradigm is ungainly and requires unnecessary writes, potentially hurting cache performance. Therefore, in practice borrowing must occur in the type system, without requiring memory updates. Previous systems support borrowing with external alias analysis and/or explicit programmer management of fractional permissions. While these approaches are powerful, they are also awkward and difficult for programmers to understand. We present an integrated language and type system with unique, immutable, and shared permissions, together with new local permissions that say that a reference may not be stored to the heap. Our system also includes change permissions such as unique>>unique and unique>>none that describe how permissions flow in and out of method formal parameters. Together, these features support common patterns of borrowing, including borrowing multiple local permissions from a unique reference and recovering the unique reference when the local permissions go out of scope, without any explicit management of fractions in the source language. All accounting of fractional permissions is done by the type system "under the hood". We present the syntax and static and dynamic semantics of a formal core language and state soundness results. We also illustrate the utility and practicality of our design by using it to express several realistic examples.

Kevin Bierhoff.  Automated Program Verification Made SYMPLAR: SYMbolic Permissions for Lightweight Automated Reasoning.  In Proceedings of the 10th SIGPLAN Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward! '11), Portland, OR, USA, 2009, October 22-27, 2011, pages 19-32.  ACM, New York, October 2009.

Abstract.  Research in automated program verification against specifications written in first-order logic has come a long way. Ever-faster Satisfiability Modulo Theories (SMT) solvers [Barrett et al. 2010] promise to verify program instructions quickly against specifications. Unfortunately, aliasing still prevents automated program verification tools from easily and soundly verifying interesting programs. This paper introduces the use of symbolic permissions as the basis for sound automated program verification. Symbolic permissions provide a simple alias control mechanism with expressiveness similar to the well-known fractional permissions [Boyland 2003]. The paper shows that symbolic permissions can be enforced with a linear refinement typechecking procedure. Once permissions are checked, aliasing can essentially be ignored for the purposes of program verification, which allows taking full advantage of SMT solvers for doing the heavy verification lifting. The paper shows that a verification tool based on symbolic permissions can easily verify a design pattern with inherent aliasing challenges.

Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich.  Practical API Protocol Checking with Access Permissions.  In Sophia Drossopoulou (Ed.), 23rd European Conference on Object-Oriented Programming (ECOOP '09), Genova, Italy, July 6-10, 2009, pages 195-219.  Lecture Notes in Computer Science (LNCS) volume 5653, Springer-Verlag, Berlin, July 2009.
A previous version of this paper appeared as Technical Report CMU-ISR-09-101.

Abstract.  Reusable APIs often define usage protocols. We previously developed a sound modular type system that checks compliance with typestate-based protocols while affording a great deal of aliasing flexibility. We also developed Plural, a prototype tool that embodies our approach as an automated static analysis and includes several extensions we found useful in practice. This paper evaluates our approach along the following dimensions: (1) We report on experience in specifying relevant usage rules for a large Java standard API with our approach. We also specify several other Java APIs and identify recurring patterns. (2) We summarize two case studies in verifying third-party open-source code bases with few false positives using our tool. We discuss how tool shortcomings can be addressed either with code refactorings or extensions to the tool itself. These results indicate that our approach can be used to specify and enforce real API protocols in practice.

Nels E. Beckman, Kevin Bierhoff, and Jonathan Aldrich.  Verifying Correct Usage of Atomic Blocks and Typestate.  In Proceedings of the 23rd ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '08), Nashville, TN, USA, October 19-23, 2008, pages 227-244.  ACM Press, New York, October 2008.

Abstract.  The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software.  However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic.  In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly.  Using access permissions, which describe how objects are aliased and modified, our system statically prevents race conditions and enforces typestate properties in concurrent programs. We have implemented a prototype static analysis for the Java language based on our system and have used it to verify several realistic examples.

Kevin Bierhoff and Jonathan Aldrich.  Modular Typestate Checking of Aliased Objects.  In Proceedings of the 22nd ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '07), Montreal, Canada, October 21-25, 2007, pages 301-320.  ACM Press, New York, October 2007.
The proof of soundness and additional material can be found in the companion Technical Report CMU-ISRI-07-105.

Abstract.  Objects often define usage protocols that clients must follow in order for these objects to work properly. Aliasing makes it notoriously difficult to check whether clients and implementations are compliant with such protocols. Accordingly, existing approaches either operate globally or severely restrict aliasing.
We have developed a sound modular protocol checking approach, based on typestates, that allows a great deal of flexibility in aliasing while guaranteeing the absence of protocol violations at runtime. The main technical contribution is a novel abstraction, access permissions, that combines typestate and object aliasing information. In our methodology, developers express their protocol design intent through annotations based on access permissions. Our checking approach then tracks permissions through method implementations. For each object reference the checker keeps track of the degree of possible aliasing and is appropriately conservative in reasoning about that reference. This helps developers account for object manipulations that may occur through aliases. The checking approach handles inheritance in a novel way, giving subclasses more flexibility in method overriding. Case studies on Java iterators and streams provide evidence that access permissions can model realistic protocols, and protocol checking based on access permissions can be used to reason precisely about the protocols that arise in practice.

Christopher Scaffidi, Kevin Bierhoff, Eric Chang, Mikhael Felker, Herman Ng, and Chun Jin.  RedOpal: Product-Features Scoring from Reviews.  In Proceedings of the 8th ACM Conference on Electronic Commerce (EC '07), San Diego, CA, USA, June 11-15, 2007, pages 182-191.  ACM Press, New York, June 2007.

Abstract.  Online shoppers are generally highly task-driven: they have a certain goal in mind, and they are looking for a product with features that are consistent with that goal. Unfortunately, finding a product with specific features is extremely time-consuming using the search functionality provided by existing web sites. In this paper, we present a new search system called Red Opal that enables users to locate products rapidly based on features. Our fully automatic system examines prior customer reviews, identifies product features, and scores each product on each feature. Red Opal uses these scores to determine which products to show when a user specifies a desired product feature. We evaluate our system on four dimensions: precision of feature extraction, efficiency of feature extraction, precision of product scores, and estimated time savings to customers. On each dimension, Red Opal performs better than a comparison system.

George Fairbanks, Kevin Bierhoff, and Desmond D'Souza.  Software Architecture at a Large Financial Firm.  In Companion Proceedings of the 21st ACM SIGPLAN/SIGSOFT International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '06), Portland, OR, USA, October 22-26, 2006, pages 815-823. ACM Press, New York, October 2006.

Abstract.  System builders have historically used informal software architecture models to understand options, make choices, and communicate with others. Research into software architecture over the past fifteen years has indicated that more precise architecture models may be beneficial. At a large financial firm, we applied precise software architecture techniques on four software projects and this experience has revealed a number of practical issues. We made the following observations across the projects: 1) Architecture models can be used to bridge gaps between business requirements and technology, 2) A small collection of techniques and a detail knob are practical and useful in a variety of projects, 3) Architecture modeling techniques amplify the skills of the architects, 4) A model of domain concepts and relationships is helpful when building architecture models, and 5) It is difficult to know when to stop adding detail to your architecture model. We believe that these observations motivate future research and can help practitioners make software architecture more effective in practice.

Kevin Bierhoff and Jonathan Aldrich.  Lightweight Object Specification with Typestates.  In Proceedings of the Joint 10th European Software Engineering Conference (ESEC) and the 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-13), Lisbon, Portugal, September 7-9, 2005, pp. 217-226. ACM Press, New York, September 2005.

Abstract.  Previous work has proven typestates to be useful for modeling protocols in object-oriented languages. We build on this work by addressing substitutability of subtypes as well as improving precision and conciseness of specifications. We propose a specification technique for objects based on abstract states that incorporates state refinement, method refinement, and orthogonal state dimensions. Union and intersection types form the underlying semantics of method specifications. The approach guarantees substitutability and behavioral subtyping. We designed a dynamic analysis to check existing object-oriented software for protocol conformance and validated our approach by specifying two standard Java libraries. We provide preliminary evidence for the usefulness of our approach.