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

p :: call ( r , f , () , ()) ;
issue ( q , unlock ) ;
pop obtained rq locks |

q ::

,

σ
The statements call , issue , unlock ,and pop obtained rq locks are operations. In
a nutshell, the call (

operation asks the handler of the target r to make a call
to the feature f on target r .The unlock operation unlocks the request queue of the pro-
cessor that executes the operation. The issue (

r , f , () , ())

operation adds the unlock
operation to q 's action queue. The pop obtained rq locks operation removes the top
element from the stack of obtained request queue locks.

q , unlock )

5.3 Mechanisms
Mechanisms are the machinery for the execution of code elements. This section studies
these mechanisms.

Issuing mechanism. With the issuing mechanism, a processor p can add statements to
the action queue of a processor q .Itusesthe issue operation to get a result configura-
tion in which a processor's action queue is extended with the new statements. There are
two main cases: p adds the statements to its own action queue, i.e., p

= q ,or p adds the

statements to the action queue of a different processor, i.e., p = q . The first case is the

non-separate case and the second one is the separate case.
For the non-separate case p puts the statements to the beginning of q 's action queue,
which is the same as putting the statements on top of the call stack. This requires that p
is in possession of its own call stack lock.

Issue Operation - Non-Separate
q = p
¬ σ . locks passed ( p )
σ .

)
Γ p :: issue ( q , s w ) ; s p , σ → p :: s w ; s p , σ
For the separate case there is a difference between a normal and a callback case. In the
normal case, p adds the statements to the end of q 's action queue. This case requires
that p is in possession of q 's request queue lock. To distinguish the normal case from
the callback case, this case also requires that q does not have a lock on p .
Issue Operation - Separate
q = p
¬ σ . locks passed ( p )
σ . rq locks ( p ) . has ( q )
¬ ( σ . rq locks ( q ) . has ( p ) ∨ σ . cs locks ( q ) . has ( p ))
Γ p :: issue ( q , s w ) ; s p

cs locks ( p ) . has ( q

| q :: s q , σ → p :: s p | q :: s q ; s w , σ