TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 09361

Design and Validation of Concurrent Systems

( Aug 30 – Sep 04, 2009 )


Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/09361

Organizers



Summary

While concurrency has always been central to embedded and distributed computing, it has recently received increasing interest from other fields related to software engineering such as programming languages, compilers, testing, and verification. This recent interest has been fuelled by a disruptive trend in the evolution of microprocessors - the number of independent computing cores will continue to increase with no significant increase in the speed of each individual core. This trend implies that software must become increasingly concurrent in order to exploit current and future hardware.

At the same time, we are seeing an unprecedented penetration of embedded and distributed systems into everyday human life. Embedded devices, such as cell phones and media players, are ubiquitously used for communication and entertainment, and distributed control systems in cars and airplanes are increasingly safety-critical. Today, systems and software engineers face the challenging task of developing efficient and reliable software for concurrent, embedded, distributed, and multi-core platforms.

The presence of concurrency in a system severely increases its complexity due to the possibility of unexpected interactions among concurrently-executing components. System designers are invariably forced to make trade-offs between productivity, correctness, and performance. Current practice includes "correct by-construction" design methods that yield safe implementations; these implementations are unlikely to be the most efficient. Conversely, highly flexible design methods can yield efficient distributed or multithreaded implementations; these methods are labor intensive and may require expensive post-design validation. We believe these two approaches delimit a continuous spectrum of design and validation techniques. It is important to develop techniques that provide a principled but pragmatic tradeoff between the rigidity of "correctness- by-construction" and the difficultly of post-hoc verification of arbitrary systems.

This workshop brought together academic and industrial researchers who are interested in design and validation techniques for concurrent systems. We had a broad participation reflecting the various approaches to the problem, including language design, compiler construction, program analysis, formal methods, and testing. We believe this mix of participants generated interesting and lively discussions. Concretely, we addressed the following set of inter-related questions during the seminar:

  • Specification and programming languages: How can a programmer specify correctness properties of a concurrent system? What are the right idioms for reasoning about concurrent programs? What concurrency-control mechanisms should be provided by the programming language? How do we enable programmers to write well-reasoned code that can be compiled for efficient execution on a multi-core platform? What kind of abstractions from the hardware/OS/runtime are useful and efficient?
  • Design methods: How should a programmer choose the right design approach given the constraints, such as quality-of-service and reliability, that may be imposed on a given application domain? What are common patterns of non-interference, e.g. race-freedom, atomicity, and determinism, that help programmers avoid common concurrency-related pitfalls?
  • Validation: How do we verify applications built using a given set of concurrency primitives? How do we verify implementations of algorithms realizing these primitives? How do we design efficient algorithms for verifying various forms of non-interference, and for explaining existing interference in terms understandable to the programmer? How do we test concurrent applications that may exhibit a high degree of, possibly uncontrollable, nondeterminism?

Participants
  • Mohamed-Faouzi Atig (University of Paris VII, FR) [dblp]
  • Anindya Banerjee (IMDEA Software - Madrid, ES) [dblp]
  • Imene Ben Hafaiedh (VERIMAG - Grenoble, FR)
  • Robert L. Bocchino Jr. (University of Illinois - Urbana-Champaign, US)
  • Ahmed Bouajjani (University of Paris VII, FR) [dblp]
  • Klaus Dräger (Universität des Saarlandes, DE)
  • Tayfun Elmas (Koc University - Istanbul, TR)
  • Azadeh Farzan (University of Toronto, CA) [dblp]
  • Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
  • Stephen Freund (Williams College - Williamstown, US)
  • Pierre Ganty (IMDEA Software - Madrid, ES) [dblp]
  • Ganesh L. Gopalakrishnan (University of Utah - Salt Lake City, US) [dblp]
  • Alexey Gotsman (University of Cambridge, GB) [dblp]
  • Daniel Grossman (Adobe Systems Inc. - Seattle, US) [dblp]
  • Christian Hammer (Purdue University, US) [dblp]
  • Maurice Herlihy (Brown University - Providence, US) [dblp]
  • Claude Jard (IRISA - Rennes, FR)
  • Vineet Kahlon (NEC Laboratories America, Inc. - Princeton, US)
  • Akash Lal (University of Wisconsin - Madison, US) [dblp]
  • Florence Maraninchi (VERIMAG - Univ. of Grenoble, FR) [dblp]
  • Madhavan Mukund (Chennai Mathematical Institute, IN)
  • Iulian Ober (IRIT - Toulouse, FR)
  • Gennaro Parlato (University of Illinois - Urbana-Champaign, US)
  • Madhusudan Parthasarathy (University of Illinois - Urbana-Champaign, US) [dblp]
  • Doron A. Peled (Bar-Ilan University - Ramat Gan, IL) [dblp]
  • Gustavo Petri (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
  • Shaz Qadeer (Microsoft Research - Redmond, US) [dblp]
  • Sophie Quinton (VERIMAG - Univ. of Grenoble, FR) [dblp]
  • Ganesan Ramalingam (Microsoft Research India - Bangalore, IN) [dblp]
  • Noam Rinetzky (Queen Mary University of London, GB) [dblp]
  • Koushik Sen (University of California - Berkeley, US) [dblp]
  • Vasu Singh (EPFL - Lausanne, CH)
  • Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
  • Francesco Sorrentino (University of Illinois - Urbana-Champaign, US)
  • Martin Steffen (University of Oslo, NO)
  • Serdar Tasiran (Koc University - Istanbul, TR) [dblp]
  • Frank Tip (IBM TJ Watson Research Center - Hawthorne, US) [dblp]
  • Viktor Vafeiadis (Microsoft Research UK - Cambridge, GB) [dblp]
  • Kapil Vaswani (Microsoft Research India - Bangalore, IN) [dblp]
  • Eran Yahav (IBM TJ Watson Research Center - Hawthorne, US) [dblp]
  • Lenore D. Zuck (NSF - Arlington, US) [dblp]

Classification
  • programming languages
  • compiler
  • sw-engineering
  • semantics
  • specification
  • formal methods
  • verification
  • logic

Keywords
  • concurrency
  • specification
  • programming
  • verification
  • validation
  • testing