Proving program termination and liveness

Byron Cook

These lectures will introduce students to automatic methods available for proving that programs eventually do something good (e.g. that programs don’t hang, that programs don’t forget to release locks, etc).  Topics will include rank-function synthesis, variance analysis and refinement, fair termination, concurrency, and the support for programs with dynamically allocated data structures.

Multicore Programming Models

Vivek Sarkar

These lectures will introduce students to multicore programming models by using a subset of the X10 language as a foundational execution model.  In addition to X10, the course will survey a variety of programming models for homogeneous multicore systems --- Cilk, OpenMP, Java Concurrency Utilities, Intel Thread Building Blocks, .Net Task Parallel Library & PLINQ.  Students will be encouraged to solve simple parallel programming problems in laboratory sessions, and to participate in class discussions that compare and contrast different programming models.  The lectures will conclude with a summary of new directions in programming heterogeneous multicore systems (CUDA for GPGPU's, and Cn for ClearSpeed), and of research activities under way in the Rice Habanero Multicore Software project.

Relaxed Memory Models for Multiprocessors

Peter Sewell

Multiprocessors have become commonplace, but programming them remains very challenging. For performance reasons, they typically do not provide a sequentially consistent memory model. Instead, memory accesses can be reordered in various subtle ways, that are often not well-understood. In these lectures I will introduce relaxed memory models for multiprocessors; describe, both informally and formally, a model for Intel 64/IA-32 processors; and compare this with models for other architectures.

Concurrent Programming in Scala -- Actors and Joins

Martin Odersky and Philipp Haller

Scala is a modern, statically-typed programming language that smoothly integrates features of object-oriented and functional languages.  It contains no language support for concurrency beyond the standard thread model of the host environment.  In these lectures we show how Scala's general abstraction mechanisms can be used to implement higher-level concurrency models that are both efficient and easy to use.  First, we present the design and implementation of Scala Actors that combine thread-based and event-based programming under a unified actor abstraction.  The user experience gained so far indicates that the library makes concurrent programming in a JVM-based system much more accessible than previous techniques.  Second, we present a novel implementation of joins (or chords) based on Scala's extensible pattern matching. The implementation supports join patterns with multiple synchronous events and guards. Furthermore, we integrate joins into Scala's actor-based concurrency framework.

Parallel Computing in Fortress & Composable Atomicity: Another view

Jan-Willem Maessen

Fortress is a new language for parallel programming being developed at Sun Microsystems.  In this session I will introduce the Project Fortress and talk a bit about how to program in the language. I'll focus on advanced examples: writing parallel generator and reduction operations. These provide a thorough introduction to the language-level and library-level mechanisms for parallelism and synchronization. At the end I'll shift gears and talk a bit about the implementation techniques necessary to make a language like Fortress run on a modern machine: How work stealing is implemented, and how to best integrate transactional memory and work stealing; and how we might optimize loops when the looping constructs themselves are simply calls to library code.

One of the oft-cited advantages of Transactional Memory is that it is composable: we can take  independently-written program fragments and glue them together to form atomic actions, without having to know the internal details of how these fragments might have been implemented.  But what does this really mean?  In this session I'll present two interesting problems in designing a language with composable atomicity.  First, I'll present a semantics for a language with lightweight parallelism, and explain how we might compose parallel actions atomically.  I'll argue for a "microcosm" view of transactions, in which the world within an atomic transaction is subject to much the same rules as the world as a whole.  Second, I'll introduce the subject of semantic atomicity: given a data type with a well-defined set of operations, we can define atomicity at the level of these operations rather than looking at individual reads and writes.

Data Parallelism in Ct

Neal Glew

Parallelism is going mainstream. Many chip manufacturers are turning to multicore processor designs rather than scalar-oriented frequency increases as a way to get performance in their desktop, enterprise, and mobile processors. This endeavor is not likely to succeed long term if mainstream applications cannot be parallelized to take advantage of tens and eventually hundreds of hardware threads.  Data parallelism is one way to parallelize applications that has been particularly successful in a number of application areas including image processing, graphics, scientific computing, and finance. This tutorial will introduce the data parallelism programming model, and show a number of applications of it to these areas.  The ideas will be presented concretely in Ct, a data parallelism library for C++ developed at Intel.

Concurrent Real-time Garbage Collection for Parallel Systems

David Bacon

Performing concurrent parallel garbage collection in a real-time manner is one of the most challenging problems in concurrent algorithms, and solving it exposes numerous fundamental issues in consistency, fairness, and progress.  It also requires understanding and using a wide array of concurrent data structures, using both locks and non-blocking approaches, in combination with priority inheritance, overload handing, and real-time scheduling.  In this class I will cover the fundamental algorithmic approaches to concurrent garbage collection, and then illustrate the use of various kinds of concurrent data structures and programming techniques in the construction of a complete real-time concurrent collector.

Speculating about the Future

Suresh Jagannathan

Migrating sequential programs to effectively utilize next-generation multicore architectures is a key challenge facing application language designers, application developers, and implementors. High-level languages with complex data- and control-flow confound classical automatic parallelization techniques.  On the other hand, introducing multithreading and concurrency control explicitly into programs can impose a high conceptual burden on the programmer, and may require a substantial rewrite of the original program. We consider the design of futures, a simple annotation that introduces asynchronous concurrency, but which impose no concurrency control.  We formulate a semantics for futures that considers the code they encapsulate to be speculative.  Thus, the observable behavior of any program equipped with futures must be identical to one in which all future annotations are erased. We consider both compile-time and runtime techniques that enforce this equivalence.

Component models, their benefits and limits

Hnetynka and Plasil

Over the past years, component-based development (CBD) has become a well-understood paradigm for building not only large enterprise applications, but also other software such as middleware. A software component is a unit with (i) well-defined interfaces both those that provide services and those specifying the required ones and (ii) explicitly defined behavior. Applications are built by designing/reusing, composing, and deploying components. In this talk, we show the core concepts of CBD by first providing a historical overview of component systems which formed the CBD foundations, and secondly presenting modern component systems. We discuss advantages of software components and also point out their the limits. Practical examples and demos of component-based systems will be presented.