[Pl-seminar] [Fwd: EventNotification] TALK: Atomicity Analysis for Multithreaded Programs

[Mitchell Wand]

------- start of forwarded message (RFC 934 encapsulation) -------
Return-Path: <apache at www.lcs.mit.edu>
Delivered-To: wand at ccs.neu.edu
From: EventNotification <events at lcs.mit.edu>
To: ai-seminar at ai.mit.edu
Subject: TALK: Atomicity Analysis for Multithreaded Programs
Date: Fri, 14 Mar 2003 09:07:31 -0500 (EST)


Atomicity Analysis for Multithreaded Programs
Speaker: Shaz Qadeer
Speaker Affiliation: Microsoft Research
Host: Martin Rinard
Host Affiliation: Massachusetts Institute of Technology

Date: 03-20-2003
Time: 11:00 AM - 12:30 PM
Refreshments: 10:45 AM
Location: NE43-6th Floor Lounge

Abstract:
Ensuring the correctness of multithreaded programs is difficult, due to
the potential for unexpected and nondeterministic interactions between
threads.  In the past, researchers have addressed this problem by
devising tools for detecting race conditions, a situation where two
threads simultaneously access the same data variable, and at least one
of the accesses is a write. However, verifying the absence of such
simultaneous-access race conditions is neither necessary nor sufficient
to ensure the absence of errors due to unexpected thread interactions.

We propose that a stronger non-interference property, namely atomicity,
is required. If a method is atomic then clients can assume that the
method executes ``in one step'', which significantly simplifies both
formal and informal reasoning about the client's correctness.  We will
present a type and effect system for specifying and verifying the
atomicity of methods in multithreaded Java programs.

We have implemented this type system for atomicity and used it to check
a variety of standard Java classes.  The checker uncovered subtle
atomicity violations in classes such as java.lang.String and
java.lang.StringBuffer that cause crashes under certain thread
interleavings.  These errors are not due to race conditions, and would
be missed by a race condition checker.

This talk is based on joint work with Cormac Flanagan of Compaq Systems
Research Center.

Bio: 
Shaz Qadeer is a member of the Software Productivity Tools group at
Microsoft Research.  Before joining Microsoft Research, he was a member
of the research staff at the Compaq Systems Research Center from 1999 to 
2002.  Shaz received his Ph.D. from the EECS Department of the
University of California at Berkeley in 1999.  His current research is
focused on tools for detecting errors in concurrent software systems.
To build these tools, he is investigating combinations of techniques
such as compositional reasoning, model checking, automated theorem
proving, and run-time verification.

Relevant URL(S): 
For more information please contact: Shireen Yadollahpour, 617.253.9620, shireen at cag.lcs.mit.edu
------- end -------