A Formal Reference for SCOOP - Empirical Software Engineering and Verification - page 92

use of established modeling concepts from process algebra, such as the notion of chan-
nels, which is present in most calculi such as CSP [13] or the -calculus [23]. We use

the theory of abstract data types (ADT) [18] to model the elements of a program text
and to model the state of a SCOOP program.
Ostroff et al. [28] describe a structural operational semantics for SCOOP in the re-
fined version by Nienaltowski [25]. This operational semantics inspired our work, and
we have attempted to stay close to their modeling ideas where possible, so that [28]
can be viewed as a reduced version of the semantics we describe in this paper. While
[28] covers some of the most significant aspects of SCOOP, it falls short of describ-
ing a number of other critical language concepts: in their reduced model, a query rou-
tine handled by some processor p must not make calls to a processor other than p ;
lock passing, expanded objects and the import mechanism, once routines, evaluation of
(asynchronous) postconditions and invariants, and explicit processor tags are not con-
sidered. We clarify these aspects in this paper. Furthermore, [28] have pursued the goal
to check temporal logic properties of SCOOP programs using their semantics and the
SPIN model checker, but were limited to small programs by state space explosion. We
have the different goal of providing a reference document for SCOOP, and thus don't
have to sacrifice coverage of the language for keeping the specification small.

π

2.2 Approaches for Other Concurrent Programming Languages

Axum [22] is a concurrent programming language based on the actor model. In Axum,
actors are called agents. An agent is an isolated runtime component that executes in par-
allel with other agents. The agents communicate with each other by sending messages
through channels. Each channel has input ports, output ports, and a protocol. The ports
are queues of messages. The protocol is a state machine that defines how the channel
behaves. Schemas define the structure of messages. Besides message passing, Axum
also provides domains - shared state between groups of actors. Erlang [10] and Scala
[27] are further examples of actor-based programming languages.
C

ω [3] is an extension of C# that integrates elements of the Join Calculus [11].

C allows computations to be spawned off into different threads using asynchronous

methods: while for synchronous methods the caller must wait until a routine completes,
asynchronous methods return immediately while their body is scheduled for execution
in another thread. C

ω

supports so-called chords, which associate the body of a routine
with more than one method; the body is executed only if all methods have been called.
Another language is Cilk [4], which extends C with concurrency concepts. A method
marked with the cilk keyword can be asynchronously spawned with the spawn keyword.
The sync keyword requires the current method to wait for all previously spawned tasks
to complete. An inlet function within a parent method receives the result of a spawned
child method; the inlet functions of a parent method are guaranteed to execute atom-
ically. Within an inlet function, the abort keyword tells the scheduler that any other
child method spawned by the parent method can be aborted. Cilk also implements a
work stealing mechanism to achieve high performance by dividing method executions
efficiently among processors.
Ada [14] defines tasks - units that can run in parallel. A task is declared within a
procedure; it consists of a specification and an implementation. The task is activated

ω