Search

Dynamic data race detectors are valuable tools for testing and validating concurrent software, but to achieve good performance they are typically implemented using sophisticated concurrent algorithms. Thus, they are ironically prone to the exact same kind of concurrency bugs they are designed to detect. To address these problems, we have developed V erified FT, a clean slate redesign of the F ast T rack race detector [19]. The V erified FT analysis provides the same precision guarantee as F ast T rack , but is simpler to implement correctly and efficiently, enabling us to mechanically verify an implementation of its core algorithm using CIVL [27]. Moreover, V erified FT provides these correctness guarantees without sacrificing any performance over current state-of-the-art (but complex and unverified) F ast T rack implementations for Java.

\begin{abstract} Multithreaded programs are notoriously prone to race conditions. Prior work on dynamic race detectors includes fast but imprecise race detectors that report false alarms, as well as slow but precise race detectors that never report false alarms. The latter typically use expensive vector clock operations that require time linear in the number of program threads. This paper exploits the insight that the full generality of vector clocks is unnecessary in most cases. That is, we can replace heavyweight vector clocks with an adaptive lightweight representation that, for almost all operations of the target program, requires only constant space and supports constant-time operations. This representation change significantly improves time and space performance, with no loss in precision. Experimental results on Java benchmarks including the Eclipse development environment show that our FastTrack race detector is an order of magnitude faster than a traditional vector-clock race detector, and roughly twice as fast as the high-performance DJIT+ algorithm. FastTrack is even comparable in speed to Eraser on our Java benchmarks, while never reporting false alarms.

Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic methods are amenable to sequential reasoning, which significantly facilitates subsequent analysis and verification. This article presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs using a synthesis of Lipton's theory of reduction and type systems for race detection. The type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We also present an algorithm for verifying atomicity via type inference. We have applied our type checker and type inference tools to a number of commonly used Java library classes and programs. These tools were able to verify the vast majority of methods in these benchmarks as atomic, indicating that atomicity is a widespread methodology for multithreaded programming. In addition, reported atomicity violations revealed some subtle errors in the synchronization disciplines of these programs.

This article presents a static race-detection analysis for multithreaded shared-memory programs, focusing on the Java programming language. The analysis is based on a type system that captures many common synchronization patterns. It supports classes with internal synchronization, classes that require client-side synchronization, and thread-local classes. In order to demonstrate the effectiveness of the type system, we have implemented it in a checker and applied it to over 40,000 lines of hand-annotated Java code. We found a number of race conditions in the standard Java libraries and other test programs. The checker required fewer than 20 additional type annotations per 1,000 lines of code. This article also describes two improvements that facilitate checking much larger programs: an algorithm for annotation inference and a user interface that clarifies warnings generated by the checker. These extensions have enabled us to use the checker for identifying race conditions in large-scale software systems with up to 500,000 lines of code.

The Java Virtual Machine executes bytecode programs that may have been sent from other, possibly untrusted, locations on the network. Since the transmitted code may be written by a malicious party or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier to check the code for type errors before it is run. As illustrated by reported attacks on Java run-time systems, the verifier is essential for system security. However, no formal specification of the bytecode verifier exists in the Java Virtual Machine Specification published by Sun. In this paper, we develop such a specification in the form of a type system for a subset of the bytecode language. The subset includes classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. We also present a type checking algorithm and prototype bytecode verifier implementation, and we conclude by discussing other applications of this work. For example, we show how to extend our formal system to check other program properties, such as the correct use of object locks.

In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then interpreted by the Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is interpreted. As illustrated by previous attacks on the Java Virtual Machine, these tests, which include type correctness, are critical for system security. In order to analyze existing bytecode verifiers and to understand the properties that should be verified, we develop a precise specification of statically-correct Java bytecode, in the form of a type system. Our focus in this paper is a subset of the bytecode language dealing with object creation and initialization. For this subset, we prove that for every Java bytecode program that satisfies our typing constraints, every object is initialized before it is used. The type system is easily combined with a previous system developed by Stata and Abadi for bytecode subroutines. Our analysis of subroutines and object initialization reveals a previously unpublished bug in the Sun JDK bytecode verifier.

Although the Java programming language has achieved widespread acceptance, one feature that seems sorely missed is the ability to use type parameters (as in Ada generics, C++ templates, and ML polymorphic functions or data types) to allow a general concept to be instantiated to one or more specific types. In this paper, we propose parameterized classes and interfaces in which the type parameter may be constrained to either implement a given interface or extend a given class. This design allows the body of a parameterized class to refer to methods on objects of the parameter type, without introducing any new type relations into the language. We show that these Java extensions may be implemented by expanding parameterized classes at class load time, without any extension or modification to existing Java bytecode, verifier or bytecode interpreter.

Precise dynamic race detectors report an error if and only if an observed program trace exhibits a data race. They must typically check for races on all memory accesses to ensure that they catch all races and generate no spurious warnings. However, a race check for a particular memory access is guaranteed to be redundant if the accessing thread has already accessed that location within the same release-free span. A release-free span is any sequence of instructions containing no lock releases or other "release-like" synchronization operations, such as wait or fork. We present a static analysis to identify redundant race checks by reasoning about memory accesses within release-free spans. In contrast to prior whole program analyses for identifying accesses that are always race-free, our redundant check analysis is span-local and can also be made method-local without any major loss in effectiveness. RedCard, our prototype implementation for the Java language, enables dynamic race detectors to reduce the number of run-time checks by close to 40% with no loss in precision. We also present a complementary shadow proxy analysis for identifying when multiple memory locations can be treated as a single location by a dynamic race detector, again with no loss in precision. Combined, our analyses reduce the number of memory accesses requiring checks by roughly 50%.

Multithreaded programs are notoriously prone to unintended interference between concurrent threads. To address this problem, we argue that yield annotations in the source code should document all thread interference, and we present a type system for verifying the absence of undocumented interference in Java programs. Under this type system, well-typed programs behave as if context switches occur only at yield annotations. Thus, well-typed programs can be understood using intuitive sequential reasoning, except where yield annotations remind the programmer to account for thread interference. Experimental results show that yield annotations describe thread interference more precisely than prior techniques based on method-level atomicity specifications. In particular, yield annotations reduce the number of interference points one must reason about by an order of magnitude. The type system is also more precise than prior methods targeting race freedom, and yield annotations highlight all known concurrency defects in our benchmarks. The type system reasons about program behavior modularly via method-level specifications. To alleviate the programmer burden of writing these specifications, we extend our system to support method specification inference, which makes our technique more practical for large code bases.

RoadRunner is a dynamic analysis framework designed to facilitate rapid prototyping and experimentation with dynamic analyses for concurrent Java programs. It provides a clean API for communicating an event stream to back-end analyses, where each event describes some operation of interest performed by the target program, such as accessing memory, synchronizing on a lock, forking a new thread, and so on. This API enables the developer to focus on the essential algorithmic issues of the dynamic analysis, rather than on orthogonal infrastructure complexities.Each back-end analysis tool is expressed as a filter over the event stream, allowing easy composition of analyses into tool chains. This tool-chain architecture permits complex analyses to be described and implemented as a sequence of more simple, modular steps, and it facilitates experimentation with different tool compositions. Moreover, the ability to insert various monitoring tools into the tool chain facilitates debugging and performance tuning.Despite RoadRunner's flexibility, careful implementation and optimization choices enable RoadRunner-based analyses to offer comparable performance to traditional, monolithic analysis prototypes, while being up to an order of magnitude smaller in code size. We have used RoadRunner to develop several dozen tools and have successfully applied them to programs as large as the Eclipse programming environment.

Atomicity is a fundamental correctness property in multithreaded programs. This paper presents an algorithm for verifying atomicity via type inference. The underlying type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We describe an implementation of this algorithm for Java and discuss its performance and usability on benchmarks totaling sixty thousand lines of code.

The race condition checker rccjava uses a formal type system to statically identify potential race conditions in concurrent Java programs, but it requires programmer-supplied type annotations. This paper describes a type inference algorithm for rccjava. Due to the interaction of parameterized classes and dependent types, this type inference problem is NP-complete. This complexity result motivates our new approach to type inference, which is via reduction to propositional satisfiability. This paper describes our type inference algorithm and its performance on programs of up to 30,000 lines of code.

The race condition checker \rcc{} statically identifies potential races in concurrent Java programs. This paper describes improvements to \rcc{} that enable it to be used on large, realistic programs. These improvements include not only extensions to the underlying analysis, but also an annotation inference algorithm and a user interface to help programmers understand warnings generated by the tool. Experience with programs containing up to 500,000 lines of code indicate that it is an effective tool for identifying races in large-scale software systems.

This paper presents a static race detection analysis for multithreaded Java programs. Our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. These patterns include classes with internal synchronization, classes thatrequire client-side synchronization, and thread-local classes. Experience checking over 40,000 lines of Java code with the type system demonstrates that it is an effective approach for eliminating races conditions. On large examples, fewer than 20 additional type annotations per 1000 lines of code were required by the type checker, and we found a number of races in the standard Java libraries and other test programs.

This paper presents a sound type system for a large subset of the Java bytecode language including classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. This work serves as the foundation for developing a formal specification of the bytecode language and the Java Virtual Machine's bytecode verifier. We also describe a prototype implementation of a type checker for our system and discuss some of the other applications of this work. For example, we show how to extend our work to examine other program properties, such as the correct use of object locks.

Commercially available compilers, particularly those used for languages like ANSI C that have extensive commercial applicability, are not well-suited to students in introductory computer science courses because they assume a level of sophistication that beginning students do not possess. To alleviate this problem at Stanford, we have developed the Thetis programming environment designed specifically for student use. The system consists of a C interpreter and associated user interface that provides students with simple and easily understood editing, debugging, and visualization capabilities. Reactions of students and instructors indicate that Thetis fulfills the goals we set out to accomplish and provides a significantly better learning environment for students in CS1/CS2.

due to the potential for subtle interactions between threads. We present a new modular verification technique to check concise specifications of large multithreaded programs. Our analysis scales to systems with large numbers of procedures and threads. We achieve thread-modular analysis by annotating each shared variable by an access predicate that summarizes the condition under which a thread may access that variable. We achieve procedure-modular analysis by annotating each procedure with a specification related to its implementation by an abstraction relation combining the notions of simulation and reduction. We have implemented our analysis in Calvin-R, a static checker for multithreaded Java programs.

In the standard Java implementation, a Java language program is compiled to Java bytecode and this bytecode is then interpreted by the Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is interpreted. As one-step towards a formal specification of the verifier, we describe a precise specification of a subset of the bytecode language dealing with object creation and initialization.