Advanced Techniques

Static Analysis for Concurrency Cormac Flanagan
Multithreaded programs are notoriously prone to errors caused by unintended interference between concurrent threads. Atomicity is a simple yet powerful specification that guarantees the absence of such errors. Atomicity violations often indicate subtle defects in a program's synchronization structure, including some defects that would be missed by traditional approaches focused on race detection. These lectures will survey the current state-of-the-art in practical techniques and tools for leveraging atomicity in the development of reliable multithreaded software systems and will illustrate the kinds of subtle synchronization defects that have been caught with these tools.

Atomicity: Synchronization via Explicit Software Transactions Dan Grossman
These lectures will cover some basic language-design and language-implementation issues for atomicity, a hot topic in the programming-language and architecture communities. As a synchronization primitive, atomicity is easy to use but difficult to implement: atomic s executes the statement s as though no other thread has interleaved execution, but still ensures fair scheduling. Language-design issues include the interaction of this construct with exceptions, thread-creation, calls to external libraries, and other synchronization mechanisms (e.g., locks). Implementation approaches include special hardware, software-transactional-memory, restrictive thread-scheduling, and automatically managed locks. These lectures will focus on the last two techniques, but give an overview of all of them.

Software Model Checking Shaz Qadeer
The design of reliable concurrent software is particularly difficult because of nondeterministic interactions between concurrently executing threads. Software model checking is a class of techniques that aims to analyze concurrent software by systematically exploring all possible thread interleavings. The number of interleavings and consequently the number of reachable states in a concurrent program grows exponentially with the number of threads. The challenge is to develop efficient techniques for state exploration in the face of this exponential state explosion. These lectures will cover a variety of optimization techniques that have been developed to combat the state-explosion problem, such as partial-order reduction, symmetry reduction, stateless search and context-bounded search.


This page is the property of the University of Oregon