Prototyping a Concurrency Model

Many novel programming models for concurrency have been proposed in the wake of the multicore computing paradigm shift. They aim to raise the level of abstraction for expressing concurrency and synchronization in a program, and hence to help developers avoid programming errors. Because of this goal, the semantics of the models themselves becomes ever more complex, increasing the risk of design flaws. We propose a methodology for prototyping concurrency models using executable formal specifications. The prototype can be used to test and correct the model at an early stage. Once the development is completed, the executable formal specification serves as an unambiguous reference. We apply this methodology to SCOOP, an object-oriented concurrency model. Using this approach, we were able to uncover and fix three major flaws in the model.

I. Introduction

A variety of concurrency models have been introduced to improve the development of concurrent programs. Examples include the Actor model [1], Communicating Sequential Processes (CSP) [2], the Join Calculus [3], the Partitioned Global Address Space (PGAS) model [4], the tuple space model [5], and SCOOP [6]. These models introduce new programming abstractions with sophisticated semantics, raising the possibility of design flaws.