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

Application Operation - Non-Once Routine or Fresh Once Routine
f ∈ ROUTINE ∧ f . is once → σ . is fresh ( p , f )
σ . handler ( r 0 )= p
¬ σ . locks passed ( p )

⎨
⎩

σ . set once func not fresh ( p , f , void ) if f ∈ FUNCTION ∧ f . is once
σ . set once proc not fresh ( p , f )

de f
= σ if f ∈ PROCEDURE ∧ f . is once

σ otherwise

de f
= σ . pass locks ( q , p , l ) . push env with feature ( p , f , r 0 , ( r 1 ,..., r n ))
g required locks

σ

de f
= { }∪

{ x ∈ PROC |∃ i ∈{ 1 ,..., n }, g , c :

p

Γ f . formals ( i ) : ( ! , g , c ) ∧ c . is ref ∧ x = σ . handler ( r i ) }

g required cs locks de f =

{ x ∈ g required locks | x = p ∨ ( x = p ∧ ( σ . rq locks ( x ) . has ( p ) ∨ σ . cs locks ( x ) . has ( p ))) }
g required rq locks de f = g required locks \ g required cs locks

g missing rq locks de f = { x ∈ g required rq locks |¬ σ . rq locks ( p ) . has ( x ) }

∀ x ∈ g required cs locks : σ . cs locks ( p ) . has ( x )
a inv is f resh ∧ a is f resh
Γ p :: apply ( a , r 0 , f , ( r 1 ,..., r n ) , q , l ) ; s p , σ →
p :: check pre and lock rqs ( g missing rq locks , f ) ;
provided f ∈ FUNCTION ∧ f . is once then
f . body
[ result : = y ; read ( Result , a r ) ; set not fresh ( f , a r . data ) where a r is f resh /

]
[ create result . y ; read ( Result , a r ) ; set not fresh ( f , a r . data ) where a r is f resh /
create result . y ]

result : = y

else
f . body
end ;
check post and unlock rqs ( g missing rq locks , f ) ;
provided f . class type . inv exists ∧ f . exported then
eval ( a inv , f . class type . inv )

; wait ( a inv )

else
nop
end ;
provided f ∈ FUNCTION then
read ( Result , a ) ; return ( a , a . data , q )
else
return ( a , q )
end ;
s p , σ
In the next step, the operation synchronizes. For each target expressions in the body
of f , the operation can get the controlling entity. Each of these controlling entities is
mapped to an object and each of these objects is handled by a processor. For each
of these processors the operation must either get a request queue lock or a call stack
lock. There are three types of calls: non-separate calls, separate calls, and separate call-
back. Non-separate calls and separate callbacks require a call stack lock. Separate calls
require a request queue lock. This leads to two sets of required locks: one set with