(EC)2 2015: 8th International Workshop on Exploiting Concurrency Efficiently and Correctly
July 18, 2015
|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.|
|18:00 sharp||Workshop dinner at La Fusion, see below for details|
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:
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.
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.
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).
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.
|Pavol Cerny||University of Colorado Boulder|
|Alastair F. Donaldson (co-chair)||Imperial College London|
|Michael Emmi||IMDEA Software Institute|
|Akash Lal||Microsoft Research|
|Zvonimir Rakamarić (co-chair)||University of Utah|
|Azadeh Farzan||University of Toronto|
|Ganesh Gopalakrishnan||University of Utah|
|Stephen Siegel||University of Delaware|
|Helmut Veith||TU Wien|