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

SCOOP relies on the Eiffel invariant mechanism. This mechanism is described in
Sec. 7.5 and Sec. 8.9.16 of the Eiffel ECMA standard [9]. On one hand, Sec. 7.5 de-
scribes the semantics of invariants: invariants must be satisfied after the execution of
every exported routine and after the execution of every creation procedure. On the other
hand, Sec. 8.9.16 describes the runtime monitoring of invariants: invariants get evalu-
ated on both start and termination of a qualified call to a routine and after every call to
a creation procedure. We had to decide whethertorelyonthesemanticsofinvariants
or on the runtime monitoring of invariants. We decided to rely on the semantics of in-
variants for two reasons. First, the runtime invariant monitoring mechanism is only one
possible implementation of the invariant semantics. Second, the runtime invariant mon-
itoring mechanism relies on the notion of unqualified calls. However, for simplicity this
work assumes feature calls to be in the canonical qualified form. The apply operation
reflects this decision: the operation evaluates the invariant whenever f is exported. Note
that the invariant can only contain non-separate target expressions. Hence, each call in
the invariant will only require p 's call stack lock.
Finally, the operation has to return the locks and it has to return the result if f is a
function. The return operation takes care of this. It comes in a variant for queries and
in a variant for commands. Both variants take the channel a and the caller processor q
in order to communicate with q . The variant for queries additionally takes the value to
be returned to q .
Before explaining the variants of the apply operation for non-fresh once routines
and attributes, the discussion continues with the operations that have not been discussed
in details so far, namely check pre and lock rqs , check post and unlock rqs ,
and return .
Check Precondition and Lock Request Queues Operation
ais fresh
Γ p :: check pre and lock rqs ( { q 1 ,..., q m }, f ) ; s p , σ →
p :: lock ( { q 1 ,..., q m } ) ;
provided f . pre exists then
eval ( a , f . pre ) ;
wait ( a )
else
nop
end ;
provided ¬ f . pre exists ∨ a . data then
nop
else
issue ( q 1 , unlock ) ;
...
issue ( q m , unlock ) ;
pop obtained rq locks ;
check pre and lock rqs ( { q 1 ,..., q m }, f )
end ;
s p , σ
The check pre and lock rqs ( {

q 1 ,..., q m }, f ) operation, executed by processor p ,

takes a processor set whose request queues must be locked on behalf of p

and it takes a feature f whose precondition must be satisfied. The operation treats the

{ q 1 ,..., q m }