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

In both cases, p has to wait for the locks to come back. Thus it does not hurt to pass
all the locks in both cases. In contrast to Nienaltowski's [25] description of SCOOP, p
only passes the locks that it really has. In particular, p does not pass its own request
queue lock in situations where p does not possess this lock, such as when the processor
that called p possesses p 's request queue lock.

In the cases where the operation passes the locks, l is ( σ . rq locks ( p ) , σ . cs locks ( p )) .

In all other cases there is no lock passing and thus l . The operation just

determines which locks to pass. The actual lock passing action will be executed by q .
Similarly, the actual lock revocation action will be executed by q .
For command calls, lock passing is the only reason to wait. In this case, the operation
creates a fresh channel a to wait for a notification from q . The notification arrives when
q is ready to return the locks. For query calls, the operation has to wait for the result.
The operation uses the given channel a to wait for the result. This has the advantage that
once the result arrives, it will be substituted after the call operation, i.e. in the result
operation of the eval operation.
Call Operation - Command
q de f

=( {}, {} )

= σ . handler ( r 0 )

⎨
⎩

if
q = p ∧∃ i ∈{ 1 ,..., n } :

Γ e i : t ∧ controlled ( t ) ∧ Γ f . formals ( i ) : ( ! , g , c ) ∧ c . is ref

then
( σ . rq locks ( p ) , σ . cs locks ( p ))

if
q = p ∧ ( σ . rq locks ( q ) . has ( p ) ∨ σ . cs locks ( q ) . has ( p ))
then
( σ . rq locks ( p ) , σ . cs locks ( p ))
otherwise
( {}, {} )
ais fresh

l de f =

Γ p :: call ( r 0 , f , ( r 1 ,..., r n ) , ( e 1 ,..., e n )) ; s p , σ →
p :: issue ( q , apply ( a , r 0 , f , ( r 1 ,..., r n ) , p , l ))

;
provided l =( {}, {} ) then wait ( a ) else nop end ;
s p , σ

Call Operation - Query
q de f = σ . handler ( r 0 )

⎨

if
q

= p ∧∃ i ∈{ 1 ,..., n } : Γ e i : t ∧ controlled ( t ) ∧ Γ f . formals ( i ) : ( ! , g , c ) ∧ c . is ref

then
( σ .

rq locks ( p ) , σ . cs locks ( p ))

if
q = p ∧ ( σ . rq locks ( q ) . has ( p ) ∨ σ . cs locks ( q ) . has ( p ))
then
( σ . rq locks ( p ) , σ . cs locks ( p ))
otherwise
( {}, {} )
Γ p :: call ( a , r 0 , f , ( r 1 ,..., r n ) , ( e 1 ,..., e n )) ; s p , σ →
p :: issue ( q , apply ( a , r 0 , f , ( r 1 ,..., r n ) , p , l )) ; wait ( a ) ; s p , σ

l de f

=

⎩