Welcome to the website for the UCLA Compilers Group supervised by Jens Palsberg. Here you'll find information about current and former students, researchers, projects and funding. Included below is a small selection of recent research projects from the group.
Declarative Fence Insertion OOPSLA'15
Previous work has shown how to insert fences that enforce sequential consistency. However, for many concurrent algorithms, sequential consistency is unnecessarily strong and can lead to high execution overhead. The reason is that, often, correctness relies on the execution order of a few specific pairs of instructions. Algorithm designers can declare those execution orders and thereby enable memory-model- independent reasoning about correctness and also ease implementation of algorithms on multiple platforms. We present a declarative approach to specify and enforce execution orders. Our fence insertion algorithm first identifies the execution orders that a given memory model enforces automatically, and then inserts fences that enforce the rest. For our benchmark experiments with the x86 and ARMv7 memory models our tool inserts fences that are competitive with those inserted by the original authors. Our tool is the first to insert fences into transactional memory algorithms and it solves the long-standing problem of how to easily port such algorithms to a novel memory model.
Automatic Atomicity Verification for Clients of Concurrent Data Structures
Mainstream programming languages offer libraries of concurrent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data structures often require stronger guarantees. We have developed an automatic and modular verification technique for clients of concurrent data structures along with a novel sufficient condition for atomicity of clients called condensability and constructed a tool called Snowflake that generates proof obligations for condensability of Java client methods.
Race directed scheduling of concurrent programs
Detection of data races in Java programs remains a difficult problem. The best static techniques produce many false positives, and also the best dynamic techniques leave room for improvement. With Racageddon we present a new technique called "Race Directed Scheduling" that for a given race candidate searches for an input and a schedule that lead to the race. The search iterates a combination of concolic execution and schedule improvement, and turns out to find useful inputs and schedules efficiently.
On the Correctness of Transactional Memory Algorithms
Transactional Memory (TM) provides programmers with a high-level and composable concurrency control abstraction. The correct execution of client programs using TM is directly dependent on the correctness of the TM algorithms. In return for the simpler programming model, designing a correct TM algorithm is an art. We have introduced a language for architecture-independent specification of synchronization algorithms that assists in the design of correct TM algorithms along with a new correctness condition, markability, and a sound program logic called synchronization object logic (SOL) that supports reasoning about the execution order and linearization orders of method calls.
Maximum stack size analysis for embedded software
Event-driven programming has gained wide acceptance, from high-performance servers to embedded systems, as an efficient method for interacting with a complex world. Unfortunately, loose coupling of event handlers obscures control flow and makes dependencies hard to detect, leading to subtle bugs. The best previous work on testing event-driven software uses event sequences that are generated randomly or by genetic algorithms. In this paper we present a new approach called "Event-based Directed Testing". Our approach combines aspects of random testing and directed testing to generate challenging event sequences for testing event-driven software. We implemented our technique into a new tool named VICE: Virgil Integrated Concolic Engine.