[talks] Wed. Dec 12th: Shaz Qadeer: "Taming Concurrency: A Program Verification Perspective"

David Walker dpw at CS.Princeton.EDU
Fri Dec 7 13:39:42 EST 2007


December 12th (next Wednesday) Shaz Qadeer from Microsoft research is 
visiting Princeton.  He is an expert in analysis of concurrent programs 
and will be giving a distinguished lecture entitled "Taming Concurrency: 
A Program Verification Perspective".  If you would like to meet with him 
(faculty or students), please pick a timeslot on Wednesday and put 
yourself on his schedule by editing this file:

~dpw/qadeer

His abstract and bio are list below.

Thanks,
Dave

**********************************************************
* Taming Concurrency: A Program Verification Perspective *
*                     Shaz Qadeer                        *
*                 Microsoft Research                     *
**********************************************************

Concurrency, as a basic primitive for software construction, is more 
relevant
today than ever before, primarily due to the multi-core revolution.
General-purpose software applications must find ways to exploit concurrency
explicitly in order to take advantage of multiple cores. However, 
experience
has shown that explicitly parallel programs are difficult to get right. To
deliver compelling software products in the multi-core era, we must improve
our ability to reason about concurrency.

Generalizing well-known sequential reasoning techniques to concurrent 
programs
is fundamentally difficult because of the possibility of interference among
concurrently-executing tasks. In this lecture, I will present reduction and
context-bounding, two ideas that alleviate the difficulty of reasoning 
about
interference by creating a simpler view of a concurrent execution than an
interleaving of thread instructions. Reduction reduces interference by 
making
a sequence of instructions in a thread appear as a single atomic 
instruction;
it allows the programmer to view an execution as a sequence of large atomic
instructions. Context-bounding reduces interference by focusing on 
executions
with a small number of context switches; it allows the programmer to 
view an
execution as a sequence of large thread contexts. I will present the theory
behind these two approaches and their realization in a number of program
verification tools I have developed over the years.

Bio: Shaz Qadeer is a researcher in the Software Reliability Research group
at Microsoft Research. The goal of his research is to develop tools for
improving the productivity of programmers. He has worked on many program
verification tools, spanning the range from run-time verification to model
checking to static analysis, with an emphasis on tools for concurrent
programs. Shaz received his Ph.D. at UC Berkeley and worked at Compaq
Systems Research Center before joining Microsoft Research.



More information about the talks mailing list