Kevin Bierhoff. API Protocol Compliance in Object-Oriented Software. PhD thesis. Technical Report CMU-ISR-09-108, Carnegie Mellon University, School of Computer Science, April 2009.
While the disseration provides the most comprehensive description of my thesis work, many of my other publications are directly related to it, notably my ECOOP '09, SAVCBS '08, OOPSLA '07, SAVCBS '06, and ESEC/FSE '05 papers. I authored or co-authored several other conference papers at OOPSLA '08, EC '07, and at OOPSLA '06, as well as additional workshop papers on a variety of topics, which I encourage you to check out as well.
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.
LNCS volume 5653, Springer-Verlag, Berlin, July 2009. Available through SpringerLink.
Zip of the specified Java standard library APIs.
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. Available in the ACM
Digital Library.
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. Available in the ACM
Digital Library.
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. Available in the ACM Digital Library.
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. Available in the ACM
Digital Library.
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. Available in the ACM
Digital Library.
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.
Taekgoo Kim, Kevin Bierhoff, Jonathan Aldrich, and Sungwon Kang. Typestate Protocol Specification in JML. In 8th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS '09) at ESEC/FSE 2009, Amsterdam, The Netherlands, August 25, 2009, pages 11-18. ACM Press, New York, August 2009. Available in the ACM Digital Library.
Abstract. The Java Modeling Language (JML) is a language for specifying the behavior of Java source code. However, it can describe the protocols of Java classes and interfaces only implicitly. Typestate protocol specification is a more direct, lightweight and abstract way of documenting usage protocols for object-oriented programs. In this paper, we propose a technique for incorporating the typestate concept into JML for specifying protocols of Java classes and interfaces, based on our previous research on typestate protocol specifications. This paper presents a set of formal translation rules for encoding typestate protocol specifications into pre/post-condition specifications. It shows how typestate protocol specifications can be mixed with pre/post-condition specifications and how violations of code contracts in inheritance can be handled. Finally, our proposed technique is demonstrated within the Java/JML environment to show its effectiveness.
Kevin Bierhoff and Jonathan Aldrich. Permissions
to Specify the Composite Design
Pattern. In 7th International Workshop on
Specification and Verification of Component-Based Systems (SAVCBS '08)
at FSE-16,
Atlanta, GA, USA, November 9-10, 2008. Slides
on the workshop website.
Abstract. The
Composite design pattern is a well-known implementation of whole-part
relationships with trees of Composite objects. This paper
presents a permission-based specification of the Composite pattern that
allows nodes in an object hierarchy to depend on invariants over their
children while permitting clients to add new children to any node in
the hierarchy at any time. Permissions can capture the circular
dependencies between nodes and their children that arise in this
context. The paper also discusses verifying a Composite
implementation and known limitations of the presented specification.
Kevin Bierhoff and Chris Hawblitzel. Checking the Hardware-Software Interface in Spec#. In Proceedings of the 4th Workshop on Programming Languages and Operating Systems (PLOS '07) at SOSP '07, Stevenson, WA, USA, October 18, 2007. Available in the ACM Digital Library. Slides on the workshop website.
Abstract. Research operating systems are often written in type-safe, high-level languages. These languages perform automatic static and dynamic checks to give basic assurances about run-time behavior. Yet such operating systems still rely on unsafe, low-level code to communicate with hardware, with little or no automated checking of the correctness of the hardware-software interaction. This paper describes experience using the Spec# language and Boogie verifier to statically specify and statically verify the safety of a driver's interaction with a network interface, including the safety of DMA.
Kevin Bierhoff, Mark Grechanik, and Edy S. Liongosari. Architectural Mismatch in Service-Oriented Architectures. In Proceedings of the International Workshop on Systems Development in SOA Environments (SDSOA '07) at ICSE-29, Minneapolis, MN, USA, May 21, 2007, pp. 114-119. IEEE Computer Society, Los Alamitos, CA, USA, May 2007. Available in the IEEE Digital Library.
Abstract. Architectural mismatch results from implicit and conflicting assumptions that designers of components make about the environments in which these components should operate. While architectural mismatch was extensively studied in monolithic and distributed applications, it has not been applied to Service-Oriented Architectures (SOAs). A major contribution of this paper is the analysis of how architectural mismatch affects SOAs. We study how implicit and conflicting assumptions that designers make about web services and their compositions affect the quality of resulting SOA-based systems. We support our analysis with empirical data that we collected from a large-scale SOA-based project within Accenture and other smaller projects.
Kevin Bierhoff. Iterator
Specification with Typestates. In Proceedings of the
5th
International
Workshop on Specification and Verification of
Component-Based Systems (SAVCBS '06) at FSE-14, Portland, OR, USA,
November 10-11, 2006, pages 79-82. ACM Press, New York, November
2006. Available
in the ACM Digital Library. Slides
on the workshop website.
Abstract. Java iterators are notoriously hard to specify. This paper applies a general typestate specification technique that supports several forms of aliasing to the iterator problem. The presented specification conservatively captures iterator protocols and consistency rules. Two limitations of the specification are discussed.
Kevin Bierhoff, Edy S. Liongosari, and Kishore S. Swaminathan. Incremental Development of a Domain-Specific Language That Supports Multiple Application Styles. In 6th OOPSLA Workshop on Domain-Specific Modeling (DSM '06) at OOPSLA '06, Portland, OR, USA, October 22, 2006, pages 79-86.
Abstract. Domain-Specific Languages (DSLs) are typically built top-down by domain experts for a class of applications (rather than a specific application) that are anticipated in a domain. This paper investigates taking the opposite route: Building a DSL incrementally based on a series of example applications in a domain. The investigated domain of CRUD applications (create, retrieve, update, delete) imposes challenges including independence from application styles and platforms. The major advantages of an incremental approach are that the language is available for use much sooner, there is less upfront cost and the language and domain boundaries are defined organically. Our initial experiments suggest that this could be a viable approach provided certain careful design decisions are made upfront.
Andi Bejleri, Jonathan Aldrich, and Kevin Bierhoff. Ego:
Controlling the Power of Simplicity. In 2006
International
Workshop on Foundations and Developments of Object-Oriented Languages
(FOOL/WOOD '06) at POPL '06,
Charleston, SC, USA, January 14, 2006.
The proof of soundness and additional material can be found in the
companion Technical Report CMU-ISRI-04-142.
Abstract. The Self programming language provides powerful dynamic features, allowing programmers to add and remove methods from objects and to change the inheritance hierarchy at run time. These facilities are useful for modeling objects that behave in different ways at different points in the object’s lifecycle. Unstructured use of these techniques, however, can result in arbitrary changes to the interface of the object, and thus is incompatible with static type checking. This paper proposes a structural type system for tracking changes to the interface of an object as methods are added and removed, and inheritance is changed at run time. The type system tracks the linearity of object and method references in order to ensure that objects whose interfaces change are not aliased. We show how our type system can express and enforce interesting protocol specifications. We then define a formal model of the language and type system, and prove that the type system is sound. Thus, our system is a foundation for languages that combine much of the power of dynamic languages like Self with the benefits of static typechecking.
Kevin Bierhoff. Checking API Protocol Compliance in Java.
Research competition abstract in Companion
Proceedings of
the 23rd ACM Conference on
Object-Oriented Programming, Systems, Languages, and Applications
(OOPSLA '08), Nashville, TN, USA, October
19-23, 2008, pages 915-916. ACM Press, New York, October
2008. Available
in the ACM Digital Library.
Kevin Bierhoff and Jonathan Aldrich. PLURAL:
Checking Protocol Compliance under Aliasing. In Companion
Proceedings of the 30th International
Conference on Software Engineering (ICSE-30), Leipzig,
Germany, May 10-18, 2008, pages 971-972. ACM Press, New York, May
2008. Available
in the ACM Digital Library.
Abstract. Enforcing
compliance to API usage protocols is notoriously
hard due to possible aliasing of objects through multiple
references. In previous work we proposed a sound, modular
approach to checking protocol compliance based on typestates
that offers a great deal of flexibility in aliasing. In
our approach, API protocols are defined based on typestates.
Every reference is associated with a permission,
and reasoning
about permissions is appropriately conservative for the
“degree” of possible aliasing admitted by a permission.
This paper describes Plural, a tool to automatically enforce
typestate-based protocols using permissions in Java.
API developers can specify protocols with simple annotations
on methods and method parameters. A static flow
analysis tracks permissions in code that uses specified APIs
and issues warnings for possible protocol violations.
Kevin Bierhoff and Jonathan Aldrich. Modular
Typestate Verification of Aliased Objects. Technical
Report
CMU-ISRI-07-105,
March 2007.
Abstract. A number of type systems have used typestates to specify and statically verify protocol compliance. Aliasing is a major challenge for these systems. This paper proposes a modular type system for a core object-oriented language that leverages linear logic for verifying compliance to more expressive protocol specifications than previously supported. The system improves reasoning about aliased objects by associating references with access permissions that systematically capture what aliases know about and can do to objects. Permissions grant full, shared, or read-only access to a certain part of object state and allow aliasing both on the stack and in the heap. The system supports dynamic state tests, arbitrary callbacks, and open recursion. The system's expressiveness is illustrated with examples from the Java I/O library.
Kevin Bierhoff, Jonathan Aldrich, and Sangjin Han. A Language-based Approach to Specification
and
Enforcement of Architectural Protocols.
Technical Report CMU-ISRI-07-121,
April 2006 (reissued in December
2007). A draft of
this report with identical content has been available on this
website since April 2006.
Abstract.
Software architecture research has proposed using protocols for
specifying the interactions between
components through ports. Enforcing these protocols in an
implementation is difficult. This
paper proposes an approach to statically reason about protocol
conformance of an implementation.
It leverages the architectural guarantees of the ArchJava programming
language. The approach
allows modular reasoning about implementations with callbacks,
recursive calls, and multiple instances
of component types. It uses a dataflow analysis to check method
implementations and uses
model checking techniques to reason modularly about component
composition. The approach is
limited to static architectures but can handle multiple instances for
component types and arbitrary
nesting of components.
Andi Bejleri, Jonathan Aldrich, and Kevin Bierhoff. A
Type
Checked Prototype-based Model with Linearity. Technical
Report CMU-ISRI-04-142,
December 2004.
Abstract. Dynamic
inheritance, originating in the Self programming language, is
the ability of an object to change the code that it inherits at run
time. This ability is useful for modeling objects that behave in
different ways at different points in the object's lifecycle.
Unstructured dynamic inheritance, however, allows arbitrary changes to
the interface of the object, and thus is incompatible with statically
typechecked languages such as C++, C\# and Java.
This paper provides a more structured facility for
dynamic inheritance, where a type system tracks the changes in an
object's interface that occur as the inheritance hierarchy is
changed. We define a formal model of a language and type system with
dynamic inheritance, and prove that the type system is sound in that
it prevents run-time type errors. The type system tracks the
linearity of objects and methods in order to ensure that objects whose
interfaces change are not aliased.
Kevin Bierhoff and Jonathan Aldrich. Cooperative Permissions for Reasoning About Aliased Objects.