Campus Event Calendar
Event Entry
What and Who
Architecture-aware Analysis of Concurrent Software
Rajeev Alur
University of Pennsylvania
SWS Distinguished Lecture Series - Spring
Rajeev Alur is Zisman Family Professor and Graduate Group Chair in the Department of
Computer and Information Science at University of Pennsylvania. He obtained his
bachelor's degree in computer science from Indian Institute of Technology at Kanpur
in 1987, and PhD in computer science from Stanford University in 1991. Before joining
Penn in 1997, he was with Computing Science Research Center in Bell Laboratories.
His areas of research include formal modeling and analysis of reactive systems,
hybrid systems, model checking, software verification, logics and automata, and
design automation for embedded software. His awards include President of India's Gold
Medal for academic excellence (1987), US National Science Foundation's CAREER
(1997) and ITR (2001) awards, Alfred P. Sloan Faculty Fellowship (1999), ACM Fellow (2007),
IEEE Fellow (2007), and designation as a highly cited scientist by the Institute for
Scientific Information (2005). Prof. Alur has (co)chaired scientific meetings such as
CAV (Intl Conf on Computer-Aided Verification), EMSOFT (ACM Symp on Embedded Software),
HSCC (Intl Conf on Hybrid Systems: Computation and Control), and LICS (IEEE Symp
on Logic in Computer Science), and served as the chair of ACM SIGBED (Special Interest
Group on Embedded Systems).
http://www.cis.upenn.edu/~alur/
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 18 July 2008
14:00
60 Minutes
E1 5
019
Saarbrücken
Abstract
Our ability to effectively harness the computational power of multi-processor
and 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 tools
are 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 data
types 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 challenges
for 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).
and 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 tools
are 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 data
types 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 challenges
for 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).
Contact
Brigitta Hansen
0681 - 9325203
--email hidden
Video Broadcast
Yes
Kaiserslautern
49
204
passcode not visible
logged in users only
Carina Schmitt, 07/14/2008 10:50
Brigitta Hansen, 06/25/2008 13:13
Brigitta Hansen, 06/24/2008 11:55 -- Created document.
Brigitta Hansen, 06/25/2008 13:13
Brigitta Hansen, 06/24/2008 11:55 -- Created document.