|
|
(EC)2 2015: 8th International Workshop on Exploiting Concurrency Efficiently and Correctly
July 18, 2015
San Francisco, California
[co-located with CAV 2015]
| Time | Talk |
| 8:45 - 9:00 | Welcome from Zvonimir Rakamarić (co-chair) |
| 9:00 - 10:00 | Invited talk: Wolfram Schulte (Microsoft Research), From Software Engineering Research into Practice and Back? |
| 10:00 - 10:30 | Morning break | |
| 10:30 - 11:30 | Invited talk: Kostya Serebryany (Google), "ThreadSanitizer and Friends: How We Fight Threading (and Other) Bugs" |
| 11:30 - 12:00 | Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Dong Ahn, Ignacio Laguna, Martin Schulz, Gregory Lee, Joachim Protze and Matthias Mueller. ARCHER: Effectively Spotting Data Races in Large OpenMP Applications. |
| 12:00 - 13:30 | Lunch break |
| 13:30 - 14:30 | Invited talk: Sebastian Burckhardt (Microsoft Research), "Robust Abstractions for Replicated Shared State" |
| 14:30 - 15:00 | Igor Konnov, Helmut Veith and Josef Widder. Challenges in Model Checking of Fault-tolerant Designs in TLA+. |
| 15:00 - 15:30 | Afternoon break |
| 15:30 - 16:30 | Invited talk: Cormac Flanagan (University of California Santa Cruz), "Cooperative Concurrency for a Multicore World" |
| 16:30 - 17:00 | Kshitij Bansal, Eric Koskinen and Omer Tripp. Synthesis of Commutativity Conditions. |
| 17:00 | Close |
| 18:00 sharp | Workshop dinner at La Fusion, see below for details |
Workshop dinner
We have a dinner reservation at La Fusion, for 18:00. The restaurant is a 15 minute walk from the workshop venue. As restaurants in SF are in demand on a Saturday night, we must arrive at 18:00 sharp in order not to lose the table. If you wish to join for dinner, please let Zvonimir Rakamaric know at the start of the workshop, so that we can ensure the booking accommodates enough people.
We are very excited to have the following confirmed invited speakers for the workshop:
Sebastian Burckhardt, Microsoft Research
Robust Abstractions for Replicated Shared State
In the age of cloud-connected mobile devices, users expect
responsive, reactive, and collaborative applications. This requires
that programs can read and write shared data everywhere, at all times,
even if network connections are slow or unavailable. Replication and
eventual consistency can deliver this experience, but may require us
to deal with asynchronous update propagation and conflict resolution,
which can be tricky. It is thus imperative that we develop
abstractions that encapsulate this complexity.
In this talk, we first discuss the general principles of eventual
consistency, and how to define its many variations. Then, we describe
GSP (global sequence protocol), a simple operational consistency
model. GSP generalizes the TSO memory model, by permitting fully
asynchronous communication, and by allowing higher-level data
abstraction. Finally, we describe a robust streaming implementation of
GSP that can hide server-, client-, and connection-failures.
Biography:
Sebastian Burckhardt was born and raised in Basel, Switzerland, where
he studied Mathematics at the local University. During an exchange
year at Brandeis University, he discovered his affinity to Computer
Science and emigrated to the United States. After a few years of
industry experience at IBM, he returned to academia and earned his PhD
in Computer Science at the University of Pennsylvania. Since then, he
has worked as a researcher at Microsoft Research in Redmond. His
general research interest is the study of programming models for of
concurrent, parallel, and distributed systems. More specific interests
include consistency models, concurrency testing, self-adjusting
computation, and the concurrent revisions programming model.
Cormac Flanagan, University of California Santa Cruz
Cooperative Concurrency for a Multicore World
Multithreaded software systems effectively exploit multi-core and
multi-processor machines. Developing reliable multithreaded software,
however, is extremely difficult due to problems caused by unexpected
interference between concurrent threads. Given their non-deterministic
nature, bugs caused by unintended thread interference are difficult to
detect, reproduce, and eliminate. At the same time, their presence
can have severe consequences.
We propose a cooperative methodology for multithreaded software,
where threads use traditional synchronization idioms such as locks,
but additionally document each point of potential thread interference
with a "yield" annotation. We present static and dynamic analyses for
verifying that yields document all possible thread interference.
Experimental results show that yield annotations are more precise than
prior techniques based on atomicity or data races, and they reduce the
number of interference points one must reason about by an order of
magnitude. Moreover, code between yield annotations forms a
serializable transaction that is amenable to intuitive sequential
reasoning. Yield annotations also serve to remind the programmer of
where thread interference may occur, and they highlight all known
concurrency defects in our benchmarks.
Biography:
Cormac Flanagan is a Professor of Computer Science at the University of California, Santa Cruz (UCSC), where he leads the Software and Languages Research Group. Prior to joining UCSC, he was a Principal Research Scientist at Hewlett Packard Corporation, Compaq Computer Corporation, and Digital Equipment Corporation. He received the B.S. degree in Computer Science and Mathematics from University College Dublin, Ireland; and the M.S. and Ph.D. degrees in Computer Science from Rice University. Dr. Flanagan holds 6 U.S. patents and has published 85 journal and conference papers. He is the recipient of an Alfred P. Sloan Foundation Fellowship, a Most Influential PLDI Paper Award, Distinguished Paper awards, and an Excellence in Teaching Award. His research has been supported by the NSF, DoD, Microsoft, IBM, UC and others.
Wolfram Schulte, Microsoft Research, Tools for Software Engineers team
From Software Engineering Research into Practice and Back?
Once up on a time I was an idealistic researcher in programing languages and software engineering. I imagined: if only developers would do X - where X stands for my favorite process, tool or technique - wouldn't that result in a more efficient engineering process leading to better programs, i.e. programs that are easier to use, execute fast, reliable, secure and are resource efficient? Then I changed roles and became an engineering leader tasked to solve that very business problem that X was supposed to address. Only one constrained was added: This time do not leave anyone or anything behind: instead you also have to migrate all existing processes, tools, artifacts and developers towards X to claim success. And that turned out to be the real challenge.
In this talk I will share the most important lessons so far from my journey into building a new engineering organization that is tasked to improve Microsoft's engineering processes and tools. I will talk about what software process and artifact qualities we focused on, what we measure and how, how engineering tools and engineering services differ, when to buy or when to build, what we use for our own engineering, when internal open source works and when it doesn't, what new research questions we encountered, and where we are in our journey towards X. Not all lessons might be relevant for you, but I hope that at least one of them will resonate with you.
Biography:
Wolfram Schulte is a partner group software engineering manager in Microsoft's Developer Division, Redmond, USA, where he founded in 2012 the Tools for Software Engineers (TSE) team. TSE's
mission is to improve Microsoft's engineering velocity. TSE does so by building developer services using Cloud technologies. TSE's tools and services range from code review, via build, and test to empirical engineering and impact meanwhile every developer within Microsoft.
Before Wolfram ventured into product groups, Wolfram lead the
Research in Software Engineering (RiSE) group, at Microsoft Research (MSR). He co-authored papers and build prototypes for many tools that Microsoft ships, including Linq, CodeContracts, Task Parallel Library, IntelliTest (Pex) and SpecExplorer.
Before joining MSR in 1999, Wolfram worked at the University of Ulm (1993-1999, habilitation), at sd&m, a German software company (1992-1993), and at the Technical University Berlin (1987-1992, PhD).
Kostya Serebryany, Google
ThreadSanitizer and Friends: How We Fight Threading (and Other) Bugs
Writing correct programs and testing them is hard; when you add
threads it becomes worse. We'll talk about a collection of dynamic
testing tools, sanitizers, that simplify and automate bug
detection. The emphasis of the talk will be put on ThreadSanitizer --
a tool that detects data races in C++, Go, and Java programs. You will
learn how the tool works, what flavours of bugs it finds and how the
developers react on them. We'll also cover other Sanitizers; while
they primarily target "usual" bugs it is often the case that they
detect a harmful side-effect of an otherwise hidden threading
bug. Finally, as an oddity, we'll discuss how threads complicate a
seemingly simple task of collecting code coverage data.
Biography: Konstantin (Kostya) Serebryany is a Software
Engineer at Google. During the last ~ 8 years his team develops and
deploys dynamic testing tools, such as AddressSanitizer and
ThreadSanitizer. Prior to joining Google, Kostya spent 7 working on
compiler optimizations at Sun and Intel.
The rise of multicore CPUs, manycore GPUs, and other heterogeneous
accelerator devices, presents exciting new opportunities for building
more efficient computing systems. But with these opportunities comes
a challenge: concurrent programming is notoriously difficult, and
advances in analysis, programming and verification in the context of
concurrency are required to meet this challenge.
There has been a surge of concurrency-related research activity from
different viewpoints, such as the rethinking of programming
abstractions and memory models; standardization and formalization of
commonly used APIs and libraries; and investigating new forms of
hardware support for parallel processing. While developing tools for
verifying and debugging concurrent systems has been an important theme
in the verification community for some time, we believe that formal
verification research can go beyond checking existing code and
systems, and play a role in identifying suitable abstractions for
concurrency.
The goal of the annual (EC)2 workshop is thus to bring together
researchers from the verification and program analysis community with
experts who are involved, on the one hand, in developing multicore
architectures, programming languages, or concurrency libraries, and on
the other hand, in distributed computing and concurrency
theory. Ultimately, such a diverse environment should stimulate
incubation of ideas leading to future concurrent system design an
verification tools that are essential in the multicore era.
Program Committee:
Steering Committee:
(EC)2 2014
(EC)2 2013
(EC)2 2012
(EC)2 2011
(EC)2 2010
(EC)2 2009
(EC)2 2008
|