Home

Registration

Scope

Program

Format

Dates

Submission

Invited Speakers

Organizers

Previous Editions

(EC)2 2013: 6th International Workshop on Exploiting Concurrency Efficiently and Correctly

July 13-14, 2013
Saint Petersburg, Russia

[co-located with CAV 2013]

Scope

The advent of multicore CPUs has created exciting new opportunities for building more efficient computing systems, as for instance the application of GPUs for hardware acceleration. Multicore CPUs are characterized by the spatial distribution of the cores and by the inherently concurrent execution of programs. These issues introduce difficult research challenges for analysis, programming, and verification.

There has been a surge of concurrency-related research activity from different viewpoints, such as rethinking of programming abstractions and memory models; standardization and formalization of commonly used APIs and libraries; and 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, we believe that formal methods research can go beyond checking existing code and systems, and play a role in identifying suitable abstractions for concurrency. The goal of this annual workshop is thus to bring together researchers from the verification 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 multi-core era.

Program

Saturday, July 13

 9:30-10:30

  • Tutorial: Brad Bingham. Distributed Explicit State Model Checking. [slides]

 10:30-11:00

  Coffee Break

 11:00-12:30

  • Position Paper: Nikolay Shilov and Renat Idrisov. Parallel Programming as a Programming Paradigm.

  • Invited Talk: Satish Narayanasamy (University of Michigan). A Path to Achieving Sequential Correctness for Parallel Programs.

 12:30-2:00

  Lunch

 2:00-3:30

  • Position Paper: Jade Alglave. Weakness is a Virtue.

  • Invited Talk: Malay Ganai (NEC Laboratories America). Small-Scale Testing of Scalable Distributed Systems. [slides]
    Modern scalable distributed systems (SDS) are designed to provide seamless multi-homing services 24/7, and support increasing load in service requests elastically. SDS are typically deployed on cheap commodity hardware, where network/disk/node may become unresponsive quite unexpectedly. To provide services that are consistent, available, and partition-tolerant in such hostile environment is a non-trivial software engineering challenge. Implementation oversights in designing such risk-aware services often lead to system-level defects, which stay hidden even after deployment and can derail the entire system, possibly resulting in loss of revenue or customer satisfaction. Testing such systems rigorously is quite challenging, especially, due to (a) large-scale testing infrastructure cost, and (b) large coverage space. To partially address the issue, we prescribe a perturbation-based testing methodology exploiting system internal states and leveraging small-scale tests, i.e., a system of a small set of servers subjected to a small client load. Our prototype framework demonstrates the effectiveness of such methodology on several open source projects in exposing both deep system-level defects. In this talk, we provide the basic motivation, present an overview of our approach, and conclude with a demonstration.

 3:30-4:00

  Coffee Break

 4:00-5:30

  • Invited Talk: Rastislav Bodík (University of California, Berkeley). Modeling Biology with Solver-Aided Programming Languages.
    A good model of a biological cell exposes secrets of the cell's signaling mechanisms, explaining diseases and facilitating drug discovery. Modeling cells is fundamentally a programming problem --- it's programming because the model is a program that simulates the cell, and it's a problem because it is hard to write a program that reproduces all experimental observations of the cell faithfully. In this talk, I will introduce solver-aided programming languages and show how they ease modeling biology as well as make programming accessible to non-programmers. Solver-aided languages come with constructs that delegate part of the programming problem to a boolean constraint solver, which can be guided to synthesize parts of the program, localize its bugs, or act as a clairvoyant oracle. I will describe our work on synthesis of stem cell models in c. elegans and then show how our framework called Rosette can rapidly implement a solver aided language in several domains, from programming by demonstration to spatial parallel programming. Joint work with Jasmin Fisher, Ali Sinan Koksal, Nir Piterman, Evan Pu, Saurabh Srivastava, and Emina Torlak.

  • Discussion

Sunday, July 14

 9:30-10:30

  • Invited Talk: Koushik Sen (University of California, Berkeley). From Active Testing to a Domain Specific Language for Testing and Reproducing Concurrency Bugs.

 10:30-11:00

  Coffee Break

 11:00-12:30

  Joint Session with REORDER.

  • Invited Talk: Marc Shapiro (INRIA Paris-Rocquencourt). Having High Concurrency, and Correctness Too; Or How I Stopped Worrying about Eventual Consistency. [slides]

  • Invited Talk: Alexey Gotsman (IMDEA Software Institute). Understanding Eventual Consistency. [slides]

 12:30-2:00

  Lunch

 2:00-3:30

  • Position Paper: Chao Wang. Runtime Verification Methods for Concurrent Data Structures.

  • Invited Talk: Domagoj Babić (Google Research). Asynchronously Communicating Visibly Pushdown Systems. [slides]

 3:30-4:00

  Coffee Break

 4:00-5:30

  • Invited Talk: Shaz Qadeer (Microsoft Research, Redmond). Safe Asynchronous Event-Driven Programming in P. [slides]
    Asynchrony is unavoidable in a world of communicating computers, devices, and services. Unfortunately for the users of such systems, asynchronous programs that are simultaneously responsive and correct are difficult to implement because of classical challenges such as concurrency and reactivity. To address this problem, we have created P, a domain-specific language for implementing asynchronous systems. P is based on the computational model of communicating state machines. It is especially suitable for implementing protocols in low-level, event-driven software such as device drivers. P has been used to implement the USB device driver stack that shipped with Windows 8, and it is currently being used for software development in Windows and Windows Phone. This talk presents the design and implementation of the compiler, runtime, and verifier for P programs.

  • Discussion

Format

The two-day workshop will include invited talks, presentations of position papers, and discussion periods. The position papers will be distributed before-hand on the CAV memory stick and this webpage.

We seek submissions of position statements between 2 and 5 pages. There are many possible themes for a position paper, including a survey of the authors' relevant recent research, a discussion of deficiencies in current languages and tools, challenges for future verification research, and/or a vision for change.

Important Dates

Application deadline for visa invitation letters supported by CAV (non-EU citizens) Mar 20, 2013
Application deadline for visa invitation letters supported by CAV (EU citizens) Apr 10, 2013
Submission deadline Apr 21, 2013 (extended)
Notification of acceptance May 3, 2013 (extended)
Workshop Jul 13-14, 2013

Submission Instructions

Prepare a 2-5 page position paper in PDF format using any tool you like. The title and the name of the authors should appear at the top of the first page. Please submit your papers through EasyChair here. Those who do not have an EasyChair account will need to create one by visiting this URL.

There will be no formal workshop proceedings—therefore, the work will be considered "unpublished".

At least one author of each position paper is expected to register and attend to present the work.

Note: We kindly ask submission authors and potential participants to apply for a visa invitation letter as soon as possible (even if their trip plans may change later). For further details please check: http://cav2013.forsyte.at/visa/

Invited Speakers

We have an amazing lineup of invited speakers:

Organizers

Program Committee:
Ivona Brandić Vienna University of Technology
Greg Bronevetsky Lawrence Livermore National Laboratory
Rupak Majumdar Max Planck Institute for Software Systems
Madan Musuvathi Microsoft Research
Manish Parashar Rutgers University
Zvonimir Rakamarić (chair) University of Utah

Steering Committee:
Azadeh Farzan University of Toronto
Ganesh Gopalakrishnan University of Utah
Stephen Siegel University of Delaware
Helmut Veith TU Wien

Previous Editions

(EC)2 2012

(EC)2 2011

(EC)2 2010

(EC)2 2009

(EC)2 2008