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
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.