Skip to main content
2009-2010 Colloquium Series: Dr. Rajeev Alur

CSE 2009-2010 Colloquium Series


Title: Architecture-aware Analysis of Concurrent Software

Dr. Rajeev Alur

University of Pennsylvania

Date: February 5th, 2010

Time: 11:00am

Location: 3105 Egr (CSE conference room)

Host: Sandeep Kulkarni


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.


Dr. Alur's Web site