There is a sign-up schedule for this event that can be found
at http://www.cs.utexas.edu/department/webeven

t/utcs/events/cgi/list_events.cgi

Type of Talk: UTCS Colloquium/L

ASR

Speaker/Affiliation: Dr. Jean-Philippe Martin/Microsoft Resear

ch, Silicon Valley

Date/Time: Friday, April 16, 2010, 3:00 p.m.

Location: ACES 4.304

Host: Lorenzo Alvisi

Talk Title: D

ynamically Checking Ownership Policies in Concurrent C/C++ Programs

T

alk Abstract:

Concurrent programming errors arise when threads share dat

a incorrectly.
Programmers often avoid these errors by using synchroni

zation to enforce a
simple ownership policy: data is either owned excl

usively by a thread that
can read or write the data, or it is read ow

ned by a set of threads that can
read but not write the data. Unfortun

ately, incorrect synchronization often
fails to enforce these policie

s and memory errors in languages like C and
C++ can violate these poli

cies even when synchronization is correct.

In this paper, we p

resent a dynamic analysis for checking ownership policies
in concurren

t C and C++ programs despite memory errors. The analysis can be
used t

o find errors in commodity multi-threaded programs and to prevent
atta

cks that exploit these errors. We require programmers to write ownership
assertions that describe the sharing policies used by different parts of
the
program. These policies may change over time, as may the policie

s'' means of
enforcement, whether it be locks, barriers, thread joi

ns, etc. Our compiler
inserts checks in the program that signal an er

ror if these policies are
violated at runtime. We evaluated our tool o

n several benchmark programs.
The run-time overhead was reasonable: be

tween 0 and 49% with an average of
26%. We also found the tool easy to
use: the total number of ownership
assertions is small, and the asse

rted specification and implementation can
be debugged together by runn

ing the instrumented program and addressing the
errors that arise. Our
approach enjoys a pleasing modular soundness
property: if a thread ex

ecutes a sequence of statements on variables it
owns, the statements

are serializable within a valid execution, and thus
their effects can
be reasoned about in isolation from other threads in the
program.

Speaker Bio:

Jean-Philippe Martin is working at Microsof

t Research, Silicon Valley. He
got his PhD from the University of Tex

as at Austin and completed his
undergraduate studies at EPFL, Switzer

land. One of the themes of his
research has been to improve reliabilit

y, either by tolerating failures or
by making it easier to weed them

out early in the process.