UTCS Faculty Candidate - Susmit Sarkar/University of Cambridge, "Discovering - and Creating - Architecture" ACES 2.302

Contact Name: 
Jenna Whitney
Date: 
Apr 3, 2012 11:00am - 12:00pm

There is a sign-up schedule for this event that can be found at

http://apps.cs.utexas.edu/talkschedules/cgi/list_events.cgi

Type o

f Talk: Faculty Recruitment

Speaker/Affiliation: Susmit Sarkar/Univers

ity of Cambridge

Talk Audience: UTCS Faculty, Graduate Students, Und

ergraduate Students and Outside Interested Parties

Date/Time: Tuesday

, April 3, 2012, 11:00 am

Location: ACES 2.302

Host: Keshav Pin

gali

Talk Title: Discovering - and Creating - Architecture

Abstra

ct:

The hardware-software interface is key to modern computer systems.

Both hardware and software designers rely on this architectural
interf

ace being well-defined (examples include the x86, ARM, and
POWER). Unfo

rtunately, such interfaces are today more fiction than
reality. In curre

nt industrial practice, these architectural
interfaces are described in

imprecise and vague terms, unsuitable for
testing against, or performin

g verification against. Inevitably,
errors keep arising, even for extre

mely careful programmers. The
situation is particularly grim for shared-m

emory concurrency, where
even experienced programmers and hardware desig

ners debate what
programmers should expect.

We can (and must) do bet

ter. In this talk I will outline a line of
recent work (POPL''09, TPHOLs

''09, CAV''10, POPL''11, PLDI''11, POPL''12,
and PLDI''12) on develo

ping precise characterizations of the
concurrency models of the x86, POW

ER and ARM architectures. We worked
with designers and implementors to es

tablish and define the
programmer-visible behaviour of these architecture

s. This work is fast
becoming the definitive characterization of the mult

iprocessor
interface, particularly as a basis for verification efforts.

I will
describe the challenges in capturing subtle implementation-depende

nt
behaviour in specifications precise enough for formal work, yet loose

enough to both allow efficient implementations and not reveal
propriet

ary details.

I then go on to describe new possibilities opened up by s

uch precise
specifications. As one example, the new C and C++ standards

have a
complex concurrency model, which has to be compiled to the very

ndifferent hardware architecture concurrency models. I will talk about
a

proof of correctness of compilation from C11/C++11 concurrency to
POWER.

More generally, my work makes possible a formalized science of
the progr

ammer-visible behaviour of architecture, informed by and
informing real-

world engineering practice, and I sketch applications
to verification of
hardware implementations and protocols and to
development of theories of
low-level concurrent programming.

Bio:
Susmit Sarkar is currentl

y an EPSRC Research Fellow at the University
of Cambridge. His fellowship
was awarded to study relaxed-memory
concurrency, and he has recently re

searched concurrency on modern
hardware such as x86, ARM, and POWER, a

nd the new concurrency model
introduced in C11/C++11. His research intere

sts are in developing and
using rigorous models of real-world systems, p

articularly
high-performance low-level code.

He holds a PhD from Car

negie Mellon University, where his dissertation
research on "A Dependent

ly-Typed Programming Language, with Applications
to Foundational Certifi

ed Code Systems" was advised by Karl Crary, and a
Bachelor of Technology
from the Indian Institute of Technology, Bombay.