Information Technology Reference
In-Depth Information
A Formal Reference for SCOOP
Benjamin Morandi, Sebastian Nanz, and Bertrand Meyer
Chair of Software Engineering, ETH Zurich, Switzerland
firstname.lastname@inf.ethz.ch
Abstract.
Operational semantics is a flexible but rigorous means to describe
the meaning of programming languages. Small semantics are often preferred,
for example to facilitate model checking. However, omitting too many details in
a semantics limits results to a core language only, leaving a wide gap towards
real implementations. In this paper we present a comprehensive semantics of
the concurrent programming model SCOOP (Simple Concurrent Object-Oriented
Programming). The semantics has been found detailed enough to guide an imple-
mentation of the SCOOP compiler and runtime system, and to detect and correct a
variety of errors and ambiguities in the original informal specification and proto-
type implementation. In our formal specification, we use abstract data types with
preconditions and axioms to describe the state, and introduce a number of special
operations to model the runtime system with our inference rules. This approach
makes our large formal specification manageable, providing a first step towards
reference documents for specifying concurrent object-oriented languages based
on operational semantics.
1
Introduction
Concurrent programming has become an important part of mainstream software devel-
opment, caused by the widespread use of multicore processors. The notorious difficulty
of writing concurrent programs correctly has on the other hand spawned work into novel
language abstractions to express concurrency and synchronization. One such language
is SCOOP [21,25], an object-oriented programming model for concurrency based on
the idea of contracts.
The main idea of SCOOP is to simplify the writing of correct concurrent programs
for developers, who can use familiar concepts from object-oriented programming but
are protected by the model from common concurrency errors such as data races. This
is achieved by a runtime system that automatically takes care of operations such as
obtaining and releasing of necessary locks, without the need for explicit program state-
ments. While being based on conceptually simple ideas, the semantics of the language
concepts and runtime system turns out to be very complex.
The question is therefore how the semantics can be properly documented. The initial
version of SCOOP has been defined in [21], where all the main concepts are outlined
but implementation aspects are neglected for the most part. A first prototype implemen-
tation was then introduced in [25], where the semantics was described only informally,
with the exception of a formalization of the type system. In this paper we provide a full
Search WWH ::
Custom Search