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

usable if they are not passed. This information can be retrieved with a call to the auxil-
iary query locks passed .
The facade provides auxiliary commands for locking request queues, removing ob-
tained request queue locks, unlocking request queues, delegating obtained request queue
locks, passing locks, and revoking locks.

5 Formalization of Execution

This section formalizes the execution of a SCOOP program. It explains the general
approach, defines the starting point of the execution, and explains the rules that drive the
execution. The rules are divided into rules for mechanisms and rules for code elements.

5.1 General Approach
The formalization is based on structural operational semantics [29], combined with
parts of the terminology from Ostroff et al. [28]. The idea behind a structural operational
semantics is to define the behavior of a program in terms of its parts, i.e., the syntactical
elements of the program. Such a semantics is intuitive because it talks directly about
elements in the code. It is a very powerful semantics because it allows us to apply
structural induction as a proof technique.

Computations. A computation models the execution of a SCOOP program. It is a
sequence of configurations, where each non-initial configuration is derived from a pre-
vious configuration through a transition. Each configuration defines a state and a list
of statements for each processor. Each transition is described by an inference rule that
maps one configuration to another. The transition from one configuration to the next
models an atomic step of one processor. The concurrent execution of a SCOOP pro-
gram is modeled by the interleaved transitions taken by different processors.
Example 4 (Modeling of parallel execution). Suppose there are two processors p and
q . Processor p executes the following sequence of statements: s p , 1 ; s p , 2 . In parallel, pro-
cessor q executes the following sequence of statements: s q , 1 . This execution is mod-
eled by any of the following simplified computations: s p , 1 ; s p , 2 ; s q , 1 or s p , 1 ; s q , 1 ; s p , 2 or
s q , 1 ; s p , 1 ; s p , 2 .

Configurations. A configuration models a snapshot in the execution of a SCOOP pro-
gram. A configuration consists of a state and a set of processors, each with a queue
of statements. The state is an instance of STATE .A schedule models the processors
and the associated queues, called action queues . Each processor must execute the state-
ments in its action queue in a FIFO order. The beginning of the action queue contains
the statements for the features that are being executed at the moment. The order of these
statements models the way the call stack orders feature executions. The tail of the action
queue is the request queue of the processor. A call stack lock is the right to add a feature
request to the beginning of the action queue and a request queue lock is the right to add
a feature request to the end of the action queue. The notation for a configuration with
processors p 1 ,..., p n , respective action queues s 1 ,..., s n ,andstate σ is:

p 1 :: s 1 | ... | p n :: s n , σ