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