The Chemistry of Concurrent and Distributed Programming II
May 11-13, 2015
NETYS'15
Agadir, Morocco
Context and goal
Modern computer systems rely crucially on concurrency and distribution to meet increasing high performance requirements. The rise of new technologies such as multi-core processors and could-computing have pushed concurrent and distributed programming to the mainstream. However, the development of concurrent and distributed systems that are both performant and consistent is a huge challenge, both from the conceptual and practical viewpoints. Researchers and practitioners in the fields of databases, cloud computing, parallel programming, concurrency, programming languages, and verification have independently tackled this challenge focusing on unique problems arising in their respective domains. We believe that there is significant potential for synergy by bringing together researchers from these diverse areas to build upon insights and techniques from each other. The main goal of this workshop is to provide an opportunity for such a synergy and to foster collaboration between the participants. Participation in
the workshop is by invitation only. The workshop is a follow up of
The Chemistry of Concurrent and Distributed Programming
held in Mysore (India) in February 2011.
Topics of interest:
A central theme of the workshop will be the issue of correctness in the development of performant concurrent and distributed systems. In this workshop, we would like to explore the different correctness notions that are used in this context and to understand the relationship between them. We would like to investigate methods for specifying, verifying, and testing systems against these notions. Here are some suggested topics that are of interest to this workshop:
- Correctness criteria: What forms of consistency notions are appropriate for the different class of concurrent and distributed applications? What abstractions do these correctness criteria offer to the applications? What kinds of correctness properties do applications typically require?
- Specification: How do the applications specify the required correctness properties?
- Systems: To what degree can these properties be guaranteed by the platform (programming language, libraries, and runtime system)? What are the performance tradeoffs when one moves the responsibility for correctness between the platform and application?
- Modularity: Can we build concurrent/distributed systems for which correctness can be established in a modular manner?
- Verification: How do we build automatic verification and testing tools that determine if applications ensure the desired specification?
- Synthesis: Can program synthesis aid in achieving correct-by-construction applications?
Organizers
Dates and venue
The workshop will take place in May 11-13 (11, 12, and 13 morning), and will be organised in Agadir, Morocco. Agadir is a major city in southwest morocco, on Atlantic ocean's cost. It has an international airport, and it is directly connected with airports in most of the european countries. Agadir is also reachable via Casablanca, which is one of the main north-african hubs.
Location
The workshop will be held at Royal Atlas.
Is is co-located with the NETYS'15 conference,
and the associated METIS'15 spring school.
Registration
Participants to the workshop must register to Metis
(see
http://netys.net/registration/).
If they are also attending Netys, they should register to Metis+Netys.
Accomodation
See
http://netys.net/accommodation/
Program
Monday May 11
09:00 - 09:15 Opening of CCDP’15
09:15 - 10:15 Session 1:
- Marko Vukolić, XFT: Decoupling Machine from Network Faults
- Cezara Dragoi, Psync: a partially synchronous language for fault-tolerant distributed algorithms
10:15 - 11:00 Break
11:00 - 12:30 Session 2:
- Javier Esparza, Verifying Population Protocols
- Aiswarya Cyriac, Split-width technique for the verification of Communicating Recursive Programs
- Rupak Majumdar, Asynchronous Programs: From Theory to Tools
12:30 - 14:15 Lunch
14:15 - 15:15 Session 3:
- Ahmed Rezine, Ordered Counter Abstraction
- Azadeh Farzan, Proof Spaces for Unbounded Parallelism
15:15 - 16:00 Break
16:00 - 17:30 Session 4:
- Shaz Qadeer, Automated and modular refinement reasoning for concurrent programs
- David Pichardie, Formal verification of concurrent algorithms for verified compilation
- Mohammed Faouzi Atig, The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO
Tuesday May 12
09:15 - 10:15 Session 5:
- Constantin Enea, Tractable Refinement Checking for Concurrent Objects
- Ali Sezgin, Correctness for Concurrent Data Structures
10:15 - 11:00 Break
11:00 - 12:30 Session 6:
- Michael Emmi, Monitoring Refinement via Symbolic Reasoning
- Jad Hamza, On Reducing Linearizability to State Reachability
- Christoph Kirsch, Concurrent Data Structures: Fast but Relaxed versus Strict but Slow Semantics
12:30 - 14:15 Lunch
14:15 - 15:15 Session 7:
- Andreas Podelski, Automated Program Verification
- Madan Musuvathi, The silently shifting semicolon
15:15 - 16:00 Break
16:00 - 17:30 Session 8:
- Rodrigo Rodrigues, Strongly versus weakly consistent replication: in search of the right balance
- Sebastian Burckhardt, Global Sequence Protocol: A Robust Abstraction for Replicated Shared State
- Marc Shapiro, Decomposing consistency
Wednesday May 13
09:15 - 10:15 Session 9:
- Claude Jard, Concurrency and real-time models: the example of back-in-time Petri nets
- Carole Delporte, Adaptive register allocation with a linear number of registers and its proof in TLA+
10:15 - 11:00 Break
11:00 - 12:00 Session 10:
- Roland Meyer, Pointer Race Freedom
- Michel Raynal, Hybrid implementation of concurrent objects and abortable objects
12:30 - 14:00 Lunch
List of confirmed participants
| Parosh Aziz Abdulla |
Uppsala |
| Mohamed Faouzi Atig |
Uppsala |
| Ahmed Bouajjani |
Paris Diderot |
| Sebastian Burckhardt |
MSR Redmond |
| Aiswarya Cyriac |
Uppsala |
| Carole Delporte-Gallet |
Paris Diderot |
| Cezara Dragoi |
Inria, ENS Paris |
| Michael Emmi |
Imdea |
|
Constantin Enea
|
Paris Diderot
|
|
Javier Esparza
|
TU Munich
|
|
Azadeh Farzan
|
Toronto
|
| Hugues Fauconnier |
Paris Diderot |
|
Rachid Guerraoui
|
EPFL
|
|
Jad Hamza
|
Paris Diderot
|
|
Claude Jard
|
Nantes
|
|
Christoph Kirsch
|
Salzburg
|
|
Rupak Majumdar
|
MPI Soft Syst
|
|
Roland Meyer
|
Kaiserslautern
|
|
Madan Musuvathi
|
MSR Redmond
|
|
David Pichardie
|
ENS Rennes
|
|
Andreas Podelski
|
Freiburg
|
|
Shaz Qadeer
|
MSR Redmond
|
|
Michel Raynal
|
Rennes
|
|
Ahmed Rezine
|
Linkoeping
|
|
Rodrigo Rodrigues
|
Lisbon
|
| Ali Sezgin |
Cambridge |
| Marc Shapiro |
Inria, Paris UPMC |
|
Marko Vukolić
|
IBM Zurich
|