Program Synthesis
Semantics for the Rust Language
Energy-Aware Programming Models and Architectures
Energy is increasingly a first-order concern in computer systems design. Battery life is a big constraint in mobile systems, and power/cooling costs largely dominate the cost of equipment in data centers. More fundamentally, current trends point toward a "utilization wall," in which the amount of active die area is limited by how much power can be fed to a chip.
Support for Explicit Runtime Concurrency Errors
This project posits that shared-memory multithreaded concurrency errors should be precisely detected and fail-stop at runtime in the way that segmentation faults or division-by-zero errors are today. We aim to generalize some support for concurrency exceptions throughout the system stack. Specifically, we are investigating the semantics and specification of concurrency exceptions at the language level, their implications in the compiler and runtime systems, how they should be delivered, and how they are enabled by efficient architecture support.
Interference-Free Regions
We, in collaboration with researchers at HP Labs, have developed the notion of interference-free regions for soundly reasoning about programs under memory-consistency models for which data races have undefined behavior (e.g., in C++). We have shown that if another thread has a conflicting memory access that is unsynchronized with respect to an interference-free region, then the accesses must form a data race. We have applied this idea to (1) compiler optimizations, such as redundant-read elimination (even across some synchronization operations), and (2) a dynamic data-race detection tool.
API Discovery and Advanced Code Completion
Modern programming languages and programming frameworks include enormous libraries with tens of thousands of API entry points, reducing large portions of application development to searching for and composing already written functionality. We aim to integrate advanced search and code-completion functionality, specialized to this task, into development environments. We leverage the rich type structure of modern statically typed languages to index libraries and define queries in terms of "partial expressions." Project work is being done in collaboration with Sumit Gulwani and Tom Ball at Microsoft Research.
Unit Test Generation for Object-oriented Programs
In an object-oriented program, a unit test often consists of a sequence of method calls that create and mutate objects, then use them as arguments to a method under test. It is challenging to automatically generate sequences that are legal and behaviorally diverse, that is, reaching as many different program states as possible.
Automated Techniques for Explaining Failed Tests
A Failed tests reveals a potential bug in the tested code. Developers need to understand which parts of the test are relevant to the failure before they start bug-fixing. This project investigates automated techniques to explain why a test fails. As an initial result, we presented a fully automated technique and its tool implementation, called FailureDoc, to infer explanatory documentation. FailureDoc augments the failed test with explanatory documentation in the form of code comments.
Static Deadlock Freedom
Deadlock remains a problem in concurrent programs, and we want to statically verify programs as deadlock-free. While there are effective static approaches for coarse-grained locking, fine-grained locking (e.g., where each node of a data structure is protected by its own lock) remains challenging. We propose lock capabilities as an approach to statically verifying the absence of deadlock in code for fine-grained locking. A lock capability is a static capability that permits the acquisition of a specific set of locks.
Atomic Blocks (Transactional Memory)
We have a long-standing interest in using atomic blocks (e.g., atomic { s }), where s is a statement as a synchronization primitive that is easier-to-use but harder-to-implement than conventional synchronization primitivites, such as mutual-exclusion locks. Atomic blocks are often implemented using transactional memory. Many language design and semantics isssues arise from their interaction with other language features. We have done work on design, theory, and implementation for a variety of languages, including Caml, Java, Haskell, Scheme, and x86 assembly.
Verification Games
Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. The approach is mapping a program verification problem into a game. When the game is solved, the final configuration of board elements can be mapped into a proof of correctness of the original program.
Software Reflexion Models
Many software design models,over time, becoming increasingly inconsistent with the system's source code. The reflexion model approach helps an engineer use a high-level model of a software system to show where the high-level model agrees with and differs from the source code. Our results (and Gail Murphy's dissertation!) include a use of reflexion models to aid in the understanding and experimental reengineering of the Microsoft Excel spreadsheet product.
Dependent Tests
Almost all results in software testing, and almost all software testing tools, assume that each test in a test suite will produce the same result regardless of the order in which the tests are executed. We have shown that this "test independence" assumption does not hold by identifying test suites in publicly available source where executing the tests in "isolation" (i.e., in a clean virtual machine) produces a different results from executing them one after another.
Finding Errors in Multithreaded GUI Applications
To keep a Graphical User Interface (GUI) responsive and active, a GUI application often has a main UI thread (or event dispatching thread) and spawns separate threads to handle lengthy operations in the background. Many GUI frameworks require all GUI objects to be accessed exclusively by the UI thread. If a GUI object is accessed through a non-UI thread, an invalid thread access error occurs and the whole application may abort.
Collabopt: Profile-guided Optimization for the Web
Recent advances in just-in-time compilation for JavaScript have made it possible to deploy large-scale applications using the HTML 5 platform. Unfortunately, web applications are still orders of magnitude slower than native applications. We propose collaborative optimization as a way to transparently improve performance by harnessing the "collective knowledge" about how individual web applications run.
Detecting Behavioral Anomalies
Developers change a program with an explicit and an implicit intention: to realize a particular objective and to avoid affecting other program properties. Testing and analysis help developers satisfy both intentions, but subtle bugs are still common. We earlier showed how a simple comparison of the static and dynamic call graphs from two related program versions can identify anomalies that detect some of these subtle bugs.
Speculative Analysis
Software developers primarily rely on experience and intuition to make development decisions. We believe that developers can make even better decisions if they are informed of the consequences of their choices. Speculative analysis is a family of techniques that attempt likely developer actions in the background and deliver precise information to the developers about their choices right as they are making the relevant decisions.
Synoptic: Studying Logged Behavior with Inferred Models
Computer systems are often difficult to understand and debug. A common way of gaining insight into a system's behavior is to inspect execution logs. Unfortunately, manual inspection of logs is an arduous process. We have developed a tool called Synoptic that helps developers by inferring a concise and accurate system model, in the form of a finite state machine, from execution logs. Synoptic processes the logs that most systems already produce, and it requires developers only to specify a set of regular expressions for parsing the logs. Synoptic models have been used to find new bugs, increase developer confidence in the correctness of their code, and help developers better understand their programs.
Timelapse: Back-in-time Debugging for the Web
Current web browser debuggers are inadequate for today's complex, event-driven, and nondeterministic web applications. The Timelapse project adapts "back-in-time" debugging techniques to the domain of client-side web programming. Unlike traditional breakpoint debuggers, Timelapse creates an exact recording of a web program's execution. This recording can be then played forward and backward and freely inspected at any time, using existing debugging tools.
VeriWeb: Crowdsourced Verification
VeriWeb is a web-interface for verifying Java programs with ESC/Java2. It introduces several innovative features to lower the skill barrier to formal verification and enable crowdsourced verification.
SPARTA: mobile device security
The SPARTA project (Static Program Analysis for Reliable Trusted Apps) is building a toolset to verify the security of mobile phone applications.