Rajeev Alur

(University of Pennsylvania)

Architecture-aware Analysis of Concurrent Software

(Vortrag im Rahmen der "Distinguished Lecture Series Spring 2008" des Max Planck Instituts für Software-Systeme)

Our ability to effectively harness the computational power of multi-processorand multi-core architectures is predicated upon advances in programming languages and tools for developing concurrent software. Recent years have seen intensive research in methods for verifying concurrent software resulting in powerful tools for finding concurrency-related bugs. Almost all of such toolsare based on the assumption that the instructions of the same thread are executed according to the program order. This model is called the interleaving model in the verification community, and the sequential consistency model in the computer architecture literature. While this is a commonly accepted language-level memory model, modern multi-processors relax sequential consistency in different ways for performance reasons resulting in weaker models. The goal of our research is to develop tools for analyzing system-level concurrent software along with such details of the underlying architecture. A first step in our research has resulted in a tool called CheckFence. CheckFence analyzes C code for concurrent datatypes with respect to an axiomatic specification of a memory model. Using a satisfiability solver, for a given client test program, CheckFence searches for discrepancy between operation-level sequential consistency semantics for the data type and concurrent executions feasible with respect to the specified model. We have analyzed a number of benchmarks successfully using CheckFence. Our analysis has revealed a number of potential bugs, and the memory ordering fences needed to fix the bugs. We conclude by discussing research opportunities and challengesfor analysis tools that can bridge the gap between the programmers' desire for simplicity of concurrency abstractions and architects' ability to expose hardware parallelism.
This talk is based on joint work with Sebastian Burckhardt (Microsoft Research) and Milo Martin (Penn).

Zeit:	Freitag, 18. Juli 2008, 14:00 Uhr
Ort:	Saarbrücken, Gebäude MPI-SWS, Raum 019
Hinweis:	Der Vortrag wird live an die TU Kaiserslautern Gebäude 49 Raum 204-206 übertragen.