Projects

Ataysn

Timing analysis of TCP servers for surviving denial-of-service attacks.

Denial-of-service attacks are becoming more frequent and sophisticated. Researchers have proposed a variety of defenses but can we validate a server implementation in a systematic manner? Atasyn focuses on a particular attack, SYN flooding, where an attacker sends many TCP-connection requests to a victim's machine. It automatically transforms a TCP-server implementation into a timed automaton, and it transforms an attacker model, given by the output of a packet generator, into another timed automaton.

Avrora

Scalable sensor network simulation with precise timing.

Avrora is a set of simulation and analysis tools for programs written for the AVR microcontroller produced by Atmel and the Mica2 sensor nodes. Avrora contains a flexible framework for simulating and analyzing assembly programs, providing a clean Java API and infrastructure for experimentation, profiling, and analysis.

Concurrent Data Structures

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.

Java Tree Builder

A frontend for The Java Compiler Compiler.

JTB is a syntax tree builder to be used with the Java Compiler Compiler (JavaCC) parser generator. It takes a plain JavaCC grammar file as input and automatically generates a set of syntax tree classes, visitor interfaces, and a Java CC grammar.

Parry

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.

Racageddon

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.

RALF

A framework for end-to-end evaluation of register allocators.

RALF is a framework for end-to-end evaluation of register allocators. Built on top of gcc, RALF enables evaluation and comparison of register allocators in the setting of an industrial-strength compiler. RALF supports modular plug-and-play of register allocators without modifying the compiler implementation at all. RALF provides any plugged-in register allocator with an intermediate program representation that is independent of the data structures of the framework. In return, the register allocator provides RALF with a set of register allocation directives.

Register Alloc by Puzzle Solving

A new model for register allocation.

This project consists in developing a new model for register allocation that has fast compilation time, produces code of good quality, is able to address the many irregularities found in common computer architectures and is intuitive enough to be easily understood. We have shown that register allocation can be viewed as solving a collection of puzzles. We model the register file as a puzzle board and the program variables as puzzle pieces; pre-coloring and register aliasing fit in naturally.

Sherlock

Scalable Deadlock Detection for Concurrent Programs

We present a new technique to find real deadlocks in concurrent programs. For 4.5 million lines of Java, our technique found almost twice as many real deadlocks as four previous techniques combined. Among those, 33 deadlocks that happened after more than one million computation steps, including 27 new deadlocks. We first use a known technique to find 1275 deadlock candidates and then we determine that 146 of them are real deadlocks. Our technique combines previous work on concolic execution with a new constraint-based approach that iteratively drives an execution towards a deadlock candidate.

Transactional Memory Algorithms

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.

Vice

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.

Virgil

Objects on the head of a pin.

Virgil is a light-weight object-oriented programming language that is designed for building software for resource-constrained embedded systems at the lowest level. Microcontroller programmers can now develop complete software systems, including hardware drivers and OS services, in one language, without the need to resort to unsafe libraries or native code. Virgil also provides a whole-program compiler system that applies novel global optimization techniques to produce efficient machine code that runs directly on the hardware, without the need of a virtual machine or a language runtime system.

Miscellaneous

Our bitbucket organization houses various projects in progress as well as the source for this site. Check there for new and nascent software.