Thu Nov 8, 2007, 4:15-5:30, 3400 Boelter Hall

Architecture-aware Analysis of Concurrent Software

Rajeev Alur
University of Pennsylvania

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.

About the speaker:  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), 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).

Host: Rupak Majumdar