ETH Logo
Composite of faces in the group
Concurrency Made Easy

Research

A key vehicle we use for much of our research is the SCOOP concurrency model, which aims to simplify the challenge of writing concurrent software by bringing it closer to the familiar, systematic, contract-based object-oriented development techniques that been applied successfully for many years in the sequential world. The research we undertake within the CME project refines and extends the SCOOP model along 7 major topics: model definition, performance analysis, reference implementation, theory and formal basis, proof techniques and tools, complementary verification techniques, and applications.

Below, we provide an overview of some current research activities within the team. For details about SCOOP, please take a look at this separate page.

Performance analysis

Very often concurrency is used to either improve latency or throughput of a program. For this reason, performance is often a critical property of concurrent programs, which is why we focus on measuring and improving the performance of SCOOP programs.

As a first step, we compare the performance and usability of an array of concurrent programming approaches. The basis for this study is the Cowichan problem set, which concentrate on typical parallel algorithms: matrix manipulations and array sorting, for example. Various implementations are compared for both performance metrics and usability metrics such as coding time, program size, etc.

In contrast to the above benchmarks, we are also developing a set of microbenchmarks which focus on coordination performance rather than problems that are primarily data parallel in nature. These coordination problems are then used to drive the implementation of an improved SCOOP execution model that affords more performance while still retaining the primary guarantees of the SCOOP model.

Key Publications

Theory and formal basis

Flaws in a concurrency model can have costly consequences if discovered after the model has been embedded into a programming language. It is therefore beneficial to verify the model prior to developing compiler and runtime support. To this end, we develop an executable formal specification that serves as a prototype of the model. We use it to run test programs and check whether the formal executions conform to expectation. This approach preserves the rigor of a formal model but combines it with the simplicity of a testing approach. Once the development is completed, the executable formal specification serves as an unambiguous reference, which provides a starting point for future model extensions as well as for implementing compiler and runtime support.

Key Publications

Verification techniques

Testing concurrent software is a daunting challenge; one must consider not only input data but also the relative times at which key events occur, such as lock acquisitions and accesses to shared resources, across all of the program's threads. Bugs, hence, are often difficult to reproduce, and individual components are tricky to test in isolation. Moreover, a program might exhibit potentially dangerous non-functional faults, like deadlock and starvation. When concurrent programs are annotated with contracts (as in SCOOP, or Java with JML), however, we have an additional weapon with which to fight back: the assumptions of the developer.

In one approach, we are applying metaheuristic search techniques to find program executions leading to states in which non-functional faults are more likely—according to some metric. Previous work has experimented with quite coarse-grained metrics, for example, favouring states with a higher number of blocked threads. We are experimenting with more fine-grained metrics that exploit the contracts present in code to find "interesting" regions of the state space. For example, in favouring states that come "closer" to failing certain types of preconditions, the search approaches boundaries in the state space across which program behaviours might change; possibly exposing additional non-functional faults.

In another approach—called Demonic Testing—unit testing is combined with rely-guarantee reasoning to provide deterministic unit testing for concurrent programs. Methods under test are annotated not just with standard contracts but also with rely-conditions, expressing what sort of thread interference should be tolerated; an SMT solver then constructs sequences of interfering instructions that drive the method under test to break the assumptions.

Key Publications

Model definition

Writing a multithreaded program can have a variety of very different motivations. Oftentimes, multithreading is a functional requirement: it enables applications to remain responsive to input, for example when using a graphical user interface. Furthermore, it is also an effective program structuring technique that makes it possible to handle nondeterministic events in a modular way; developers take advantage of this fact when designing reactive and event-based systems. In all these cases, multithreading is said to provide concurrency. In contrast to this, the multicore revolution has accentuated the use of multithreading for improving performance when executing programs on a multicore machine. In this case, multithreading is said to provide parallelism.

Programming models for multithreaded programming generally support either concurrency or parallelism. For example, the Actor model or Simple Concurrent Object-Oriented Programming (SCOOP) are typical concurrency models: they are optimized for coordination and event handling, and provide safety guarantees such as absence of data races. Models supporting parallelism on the other hand, for example OpenMP or Chapel, put the emphasis on providing programming abstractions for efficient shared memory computations, typically without addressing safety concerns.

While a separation of concerns such as this can be very helpful, it is evident that the two worlds of concurrency and parallelism overlap to a large degree. For example, applications designed for concurrency may have computational parts the developer would like to speed up with parallelism. On the other hand, even simple data-parallel programs may suffer from concurrency issues such as data races, atomicity violations, or deadlocks. Hence, models aimed at parallelism could benefit from inheriting some of the safety guarantees commonly ensured by concurrency models.

Key Publications

Applications: Robotics

Software plays a critical role in enabling modern robots to achieve their complex functionalities; however, the tools and techniques used to develop robotics software lag behind the state of the art in the rest of software engineering. In particular, concurrency is one of the principal roadblocks in coping with the growing complexity of new robotics applications. While advanced robotic systems typically include many components that can in principle operate concurrently â€" and should do so to meet their potential, enabling such potential concurrency requires the underlying software to support concurrent execution. Due to the limitations of traditional concurrent programming techniques, such as the standard "thread libraries" (the main concurrency mechanisms today), programmers using such tools are constantly at risk of falling into common pitfalls such as data races and deadlocks. More generally, concurrent applications are hard to design and implement correctly, to test and debug, and to maintain. As a result, most robotics applications limit themselves to an elementary use of concurrency, closing off many interesting possibilities offered by the hardware.

We expand the applications of concurrency to robotics and demonstrate how SCOOP can ease the use of concurrency in robotics and tighten the link between robot's hardware and software. In addition, we develop educational material to teach the concepts of concurrency within the context of robotics, enabling students to understand the power of concurrency beyond processors.

Key Publications

!!! Dieses Dokument stammt aus dem ETH Web-Archiv und wird nicht mehr gepflegt !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!