Join us on:
Facebook
LinkedIn
Plaxo

T14. Detecting and preventing bugs with pluggable type-checking

Michael D. Ernst, U. of Washington

Michael D. Ernst is Associate Professor in the Computer Science and Engineering department at the University of Washington. Ernst's research aims to make software more reliable, more secure, and easier (and more fun!) to produce. His primary technical interests are in software engineering and related areas, including programming languages, type theory, security, program analysis, bug prediction, testing, and verification. Ernst's research combines strong theoretical foundations with realistic experimentation, with an eye to changing the way that software developers work. Ernst is the specification lead for Java 7's Type Annotations language extension (JSR 308). He is also a member of the expert group for JSR 305 and is the author of many tools for improving programmer productivity. For more information, see http://www.cs.washington.edu/homes/mernst/ .

Mahmood Ali, MIT CSAIL

Mahmood Ali is a graduate student at MIT. He is responsible for the JSR 308 compiler implementation, for the Checker Framework for writing pluggable type-checkers. His other research includes innovative type systems, such as for enforcing reference and object immutability.

Are you tired of null pointer exceptions, unintended side effects, mistaken equality tests, and other run-time errors that appear during testing or in the field? A pluggable type system can guarantee the absence of these errors, and many more.

A type system can help programmers to detect and prevent errors. However, the built-in type system of a programming language does not detect and prevent enough errors. It cannot express important properties such as: a reference is non-null, a data structure should not be modified, or a string has been properly sanitized.

A type system can be extended to can enforce additional properties statically, preventing whole classes of errors. Such extensions have only recently become practical: expressive, scalable, and compatible with existing languages and tools.

The use of pluggable types (that operate as an optional plug-in to the compiler) has benefits for two constituencies:

  • Programmers can detect and prevent errors in their code.

  • Type system designers can easily evaluate new type systems in the context of an industrial programming language.

The line between these constituencies is porous: a developer or architect may create a simple type system to enforce an application-specific property. Languages such as Java 7 have built-in support for expressing pluggable types.

This tutorial will explain how to both use and create pluggable type systems. Afterward, you will be ready to use pluggable types with confidence and to create type-checkers of your own.

Objectives:

This tutorial will explain how to both use and create pluggable type systems. A pluggable type system enhances the type system for a programming language, enabling the compiler to detect and prevent even more errors at compile time.

After the tutorial, participants will understand what sorts of errors are amenable to pluggable type-checking; will have experience using pluggable type-checking; and will have created a small but functional checker for a property of interest to them, in the context of Java.

Format:

Our tutorial will give attendees the theoretical background and practical knowledge to use and build scalable, robust, and expressive pluggable type systems in the context of a realistic object-oriented programming language. The tutorial will consist of a mix of activities, both to cater to different learning styles and interests and to promote alertness throughout the session. We will ask attendees to bring laptop computers — and a problem of interest to them — so that they can participate actively throughout the tutorial.

We will begin with demonstrations of existing checkers in action, both to show how the checkers support programmer needs and also to show how the framework enables the creation of effective and usable tools. The demonstrations will use real code from case studies in which pluggable type-checkers found important bugs in fielded software. We will review other results of the case studies, including strengths and weaknesses of the overall approach. During this component, attendees will also run the checkers on their own code.

A lecture component will present the theory of type qualifiers. It will also describe the parts of a pluggable type system.

We will explore the interface that the Checker Framework provides for implementing a type system. Its cleanly separates distinct tasks: type qualifiers and hierarchy; type introduction rules; type rules; and interface to the compiler. It has both declarative and procedural mechanisms for each of these tasks. In addition to presenting the interface, we will examine real code from existing checkers. There are many checkers from which to choose (see supplementary materials)

From the front of the room, we will interactively create a type checker from scratch at the keyboard. Rather than merely using a canned demo, we will also take suggestions from the audience regarding properties to check. This will make the session more interactive and relevant.

Finally, participants will to apply checkers to their own code, to begin writing their own checkers, or to refine existing ones. They will work in small groups, both to permit the presenters to spend enough time with each group and also to permit participants to learn from one another.

Audience: Researchers, Practitioners
Please email any questions to . This e-mail address is being protected from spambots. You need JavaScript enabled to view it