ETH Logo

Master's Thesis (Claudio Corrodi)

Summary

Modelling and Verifying an Object-Oriented Concurrency Model in GROOVE
Master's Thesis, October 2014 — April 2015
Author: Claudio Corrodi
Supervisor: Chris Poskitt
External Co-Supervisor: Alexander Heußner (University of Bamberg)

Resulting Publications

Project Proposal

Background

With the rise of multi-core and distributed architectures, demand is increasing for high-level programming interfaces that alleviate the notorious difficulty of writing efficient and portable parallel code. Two recent, contrasting developments include Grand Central Dispatch (GCD) and SCOOP. The former is a library present in Apple’s operating systems (with ports existing for FreeBSD, Linux, and Windows), whereas the latter is a concurrency model for the object-oriented programming language Eiffel. Both provide concurrency at a higher level of abstraction than threads, through mechanisms for asynchronously dispatching “units” (or “blocks”) of code – together with various dependencies between them. Concurrent programs expressed in such models can often exhibit complex, perplexing, and surprising behaviour, and there is a pressing need for tools and methods that facilitate their verification and analysis. In the case of GCD, a formal model has been proposed and a translation to Petri nets prototyped; in the case of SCOOP, a comprehensive operational semantics has been formalised in Maude – but the model is too complex for many of the automatic analyses that the tool supports. For these and other kinds of asynchronous systems, a formalisation is needed that is natural, quick to prototype, supported by rigorous theory, and supported by a tool that can perform analyses of interest on the models.

Scope of the Work

This project proposes to investigate, as such a formalism, the use of a graph-based abstract semantics – a visual, powerful, and rigorous modelling technique based on (algebraic) graph grammars. By this, we mean a semantics in which program states are abstracted to graphs, and computational steps to applications of graph rewrite rules (akin to those of Chomsky string grammars, but lifted to graphs). Such a formalism – while unconventional – appears to be a natural choice for prototyping systems as complex as SCOOP, e.g. with objects, processors, and tasks all represented by nodes, and queues, locks, and handlers by edges. Furthermore, it benefits from a well-developed theoretical foundation and support from a number of tools. The most notable of the latter is GROOVE, which is able to perform (bounded) model checking directly on graph grammars and programs, is equipped with state-pruning strategies that directly exploit the graph-based representation (e.g. symmetry reduction based on graph isomorphism), and has had its maturity demonstrated through several encouraging case studies (e.g. modelling Java type graphs).

This project, in particular, aims to develop automatic translations of SCOOP programs to inputs for the GROOVE model checker to verify, visualise, and analyse. To achieve this, a core (but expressive) subset of the SCOOP language will be formalised, in GROOVE, as a system of graph grammar rules. Then, an automatic translation of (this subset of) SCOOP programs to GROOVE inputs will be developed, and thoroughly evaluated on case studies. Both the formalisation and translation will be constructed as “parametrically” as possible, in order to allow an analogous future treatment of GCD and similar such asynchronous systems.