Design and Validation of Concurrent Systems

Motivation

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 seminar aims to bring together academic and industrial researchers who are interested in design and validation techniques for concurrent systems. We intend to have a broad participation reflecting the various approaches to the problem, including language design, compiler construction, program analysis, formal methods, and testing. To focus the discussions, we will also include participants from application areas (embedded reactive systems, robotics, middleware, operating systems, and virtual machines) who have strong interests in verification. We hope this mix of participants will generate interesting and heated discussions, and will inspire researchers to come up with long-term and practical solutions for the design and verification of concurrent systems. Concretely, we hope to address 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?