There is a signup schedule for this event (UT EID required).

Typ

e of Talk: UTCS Colloquium

Speaker/Affiliation: Shaz Qadeer/Micros

oft Research

Date/Time: Monday November 17 2008 2:00 p.m.

Location: TAY 3.128

Host: Allen Emerson

Talk Title: Taming

Concurrency: A Program Verification Perspective

Talk Abstract:
Co

ncurrency as a primitive for software construction
is more relevant t

oday than ever before primarily due
to the multi-core revolution. Gen

eral-purpose software
applications must find ways to exploit concurrenc

y 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 e

ra we must improve our
ability to reason about concurrency.

Ge

neralizing well-known sequential reasoning techniques to
concurrent pro

grams is fundamentally difficult because of the
possibility of interfer

ence among concurrently-executing tasks.
In this lecture I will presen

t reduction and context-bounding---
two ideas that alleviate the difficu

lty of reasoning about inter-
ference by creating a simpler view of a co

ncurrent execution
than an interleaving of thread instructions. Reduct

ion reduces
interference by making a sequence of instructions in a thre

ad
appear as a single atomic instruction; it allows the programmer
to view an execution as a sequence of large atomic instructions.
Conte

xt-bounding reduces interference by focusing on executions
with a small
number of context switches; it allows the programmer
to view an execu

tion as a sequence of large thread contexts. I will
present the theory
behind these two approaches and their realization
in a number of progr

am checkers that have been used to find bugs
-atomicity violations pro

tocol errors deadlocks and livelocks - in
real-world concurrent progr

ams.

Speaker Bio:
Shaz Qadeer is a Senior Researcher in the RiSE

(Research in
Software Engineering) group at Microsoft. His research ai

ms to
help concurrent programmers by creating methods for designing verifying and testing concurrent software. Shaz received his Ph.D.

s programmers find and reproduce Heisenbugs in con-
current programs.