EC2 on Wednesday, July 21st

09:00‑10:00 Session 7
Location: IF G.07A
09:00 Bill Gropp (UIUC)
Invited talk: Challenges in Using the Message Passing Interface in Multicore and Heterogeneous Systems

The Message Passing Interface (MPI) has become the dominant parallel programming model in technical computing, in part because of its attention to performance issues and scalability. However, MPI was always intended to be part of an overall solution strategy, complementing other programming approaches. With the emergence of both multi- and many-core systems and heterogenous systems (such as clusters with GPGPUs), MPI must interoperate with a increasing variety of programming models. MPI is also evolving; with active efforts to define support for fault tolerance and new interfaces for one-sided operations, as well as support for hybrid programming models. This talk will provide background on why support for interaction with other models is important for MPI users and what some of the challenges are in interoperating with those models.

10:30‑11:30 Session 8
Location: IF G.07A
10:30 Alan Humphrey, Christopher Derrick, Beth Tibbitts, Anh Vo, Sarvani Vakkalanka, Ganesh Gopalakrishnan, Bronis de Supinski, Martin Schulz and Greg Bronevetsky
Verification for Portability, Scalability, and Grokkability

This paper will describe progress in Dynamic reduction algorithms (including verification for portability), Distributed dynamic verification (how to run MPI verification on 1000 cores), and how to make verification understandable (by plugging in our verifier into the Eclipse Parallel Tools Platform).

10:50 Rajesh Karmani and P Madhusudan
A Contract Language for Race-Freedom

We propose an annotation framework of thread contracts, called Accord, in order to reason that a parallel program has no data-races, and build accompanying verification and testing tools. Accord annotations allow programmers to declaratively specify the fine-grained parts of memory that a thread may read or write into, and the locks that protect them, and hence can be used to establish race-freedom. We show that this can be achieved using automatic constraint-solvers based on SMT solvers. We also show how to compile Accord thread contracts to runtime assertions that check the contracts dynamically during testing. Furthermore, we explore static verification of annotation correctness for concurrent programs, using a new and surprising reduction to verifying assertions in sequential programs; the latter can be tackled using sequential contract-verification tools. Using a large class of data-parallel programs that share memory in intricate ways, we show that natural and simple contracts suffice to argue race-freedom, and that the task of showing that the annotations imply race-freedom and the task of showing the annotations are respected by the program, can be handled by existing SMT solvers (Z3) and sequential verification tools (Boogie, with specifications in Spec#).

11:10 Ariel Cohen, Kedar Namjoshi, Yaniv Sa'ar, Lenore Zuck and Katya Kisyova
Model Checking in Bits and Pieces

The central thesis explored in this paper is that parallel model checking is easily achieved through compositional methods.

11:30‑12:00 Session 9
Location: IF G.07A
11:30 Concurrency Education
14:00‑15:00 Session 10
Location: IF G.07A
14:00 Miriam Leeser (Northeastern University)
Invited talk: GPU programming: bugs, pitfalls and the importance of correctness in biomedical and scientific applications

GPUs are being used to accelerate many biomedical and scientific applications. My research group is accelerating applications including: i) lung tumor tracking to better pinpoint the tumor in radiation therapy and ii) in vivo imaging of tumors in live animals. In these and many other applications, high confidence in the correctness of the result is essential. At the same time, a GPU program is by its nature massively parallel, launching hundreds or thousands of threads simultaneously. Such programs are extremely difficult to debug. Symbolic methods are essential for reasoning about the concurrency inherent in these programs and their many different possible behaviors due to interleaving, memory interfacing and barrier synchronization. In this talk, I will discuss the applications we are working on, common coding errors in GPU programs, and why we believe that formal methods will help both finding bugs and giving users an increased confidence of the correctness of their GPU programs.

15:30‑16:30 Session 11
Location: IF G.07A
15:30 Marius Bozga and Emmanuel Sifakis
Issues on Memory Management for Component-Based Models

Memory management has a great influence on systems performance. To exploit parallelism provided by new multicore platforms, appropriate memory models are needed. In the component-based programming paradigm, a private memory model is usually assumed. Each component acts as a black box with a well defined interface, through which it exchanges messages with its environment. Message passing communication can introduce a big overhead when deploying component-based systems on shared memory architectures, like multicores. This work proposes an automated transformation of I/O systems described using the BIP component-based framework, to equivalent Shared-Memory BIP (SM-BIP) systems. The transformation consists on replacing costful message passing by shared memory communication. The potential gains are both reduced execution times and easy configuration of memory usage. Moreover, the transformation allows us to investigate the deep relation between memory usage, underlaying platform and maximum parallelism that can be obtained for a given BIP application.

15:50 Vasu Singh
Memory Model Relaxations to Boost TM Performance

Transactional memory (TM) is a promising paradigm for concurrent programming in the multi-core era. While the mutual interaction between transactions has been formalized using correctness notions like serializability and opacity, the interaction between transactions and non-transactional operations is formalized using a notion of strong atomicity. Recently, we formalized a notion of correctness parametrized by a memory model. Our formalization has led to an interesting insight: it turns out for relaxed memory models as compared to sequential consistency, opacity can be achieved with more efficient TM implementations.

16:10 Guodong Li and Ganesh Gopalakrishnan
PUG: A symbolic verification and test generation tool for GPU programs

GPUs are going to fuel the many-core revolution by supporting wide-word SIMD parallelism. All systems from future HPC systems to hand-held systems will (or are) employing GPUs. We present a tool Prover of User GPU programs (PUG) that is based on SMT techniques and employs innovative complexity reduction methods for concurrency encoding and handling loops. PUG can verify GPU kernel instances for the absence of data races and also verifies embedded assertions. Current work on PUG will allow test input generation. PUG has verified many of the kernels on the Nvidia SDK, handling thousands of lines of code. Our presentation will detail the algorithms employed in PUG, results, and future prospects.

16:30‑17:00 Session 12
Location: IF G.07A
16:30 Q-and-A session with all the speakers