[Colloq] Thesise Defense - Aaron Turn - Understanding and Expressing Scalable Currency
Jessica Biron
bironje at ccs.neu.edu
Fri Feb 15 08:20:38 EST 2013
Speaker: Aaron Turon
Date: Friday, February 22nd at 2:30pm
Location: 366 WVH
Title: Understanding and expressing scalable concurrency
Abstract:
The Holy Grail of parallel programming is to provide good
speedup while hiding or avoiding the pitfalls of
concurrency. But some level in the tower of abstraction must
face facts: parallel processors execute code concurrently,
and the interplay between concurrent code, synchronization,
and the memory subsystem is a major determiner of
performance. Effective parallel programming must ultimately
be supported by scalable concurrent algorithms---algorithms
that tolerate (or even embrace) concurrency for the sake of
scaling with available parallelism. This dissertation makes
several contributions to the understanding and expression of
such algorithms:
* It shows how to understand scalable algorithms in terms of
local protocols governing each part of their hidden
state. These protocols are visual artifacts that can be
used to informally explain an algorithm at a whiteboard.
But they also play a formal role in a new logic for
verifying concurrent algorithms, enabling correctness
proofs that are local in space, time, and thread
execution. Correctness is stated in terms of refinement:
clients of an algorithm can reason as if they were using
the much simpler specification code it refines.
* It shows how to express synchronization in a declarative
but scalable way, based on a new library providing "join
patterns". By declarative, we mean that the programmer
needs only to write down the constraints of a
synchronization problem, and the library will
automatically derive a correct solution. By scalable, we
mean that the derived solutions deliver robust performance
with increasing processor count and problem complexity.
For common synchronization problems, join patterns perform
as well as specialized algorithms from the literature.
* It shows how to express scalable algorithms through
"reagents", a new monadic abstraction. With reagents,
algorithms no longer need to be constructed from "whole
cloth," i.e. by using system-level primitives directly.
Instead, they are built using a mixture of shared-state
and message-passing combinators. Concurrency experts
benefit, because they can write libraries at a higher
level, with more reuse, without sacrificing scalability.
Their clients benefit, because composition empowers them
to extend and tailor a library without knowing the details
of its underlying algorithms.
Committee:
Mitchell Wand (advisor)
Amal Ahmed
Olin Shivers
Doug Lea (external)
Claudio Russo (external)
Jessica Biron
Administrative Assistant – Office of the Dean and CCIS Development
College of Computer and Information Science
Northeastern University
202 West Village H
617-373-5204
bironje at ccs.neu.edu
http://www.ccs.neu.edu/
More information about the Colloq
mailing list