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.
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.