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

The callback case occurs if q has a lock on p . In this situation, p could issue a statement
s w on q andthenwaitfor q to complete. On the other side, processor q could already be
waiting for p to complete. Processor q would be waiting for p to finish and p would be
waiting for q to finish. However, since s w would be at the end of q 's action queue and q
would be waiting there cannot be any progress. This type of deadlock can be prevented
by adding s w not to the of q 's action queue but to the beginning. This will make sure
that q can execute the statement right away and hence p can continue. This in return
will enable q to continue. As a prerequisite, p must possess q 's call stack lock.

Issue Operation - Separate Callback
q = p
¬ σ . locks passed ( p )
σ . cs locks ( p ) . has ( q )
σ . rq locks ( q ) . has ( p ) ∨ σ . cs locks ( q ) . has ( p )
Γ p :: issue ( q , s w )

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

Delegated execution mechanism. This section discusses how a processor q can del-
egate the execution of statements to a different processor p . This mechanism is useful
for the evaluation of asynchronous postconditions. Processor q must make sure that the
statements make sense in the context of processor p . The names that occur in these
statements must be defined in the top environment of p and p must have the necessary
locks to execute the statements. Statements that fulfill the following conditions can be
delegated:

- All names that occur in the statements are defined in q 's top environment.
- Their execution only requires the top set of q 's stack of obtained request queue
locks.

These conditions exclude statements that involve non-separate calls or separate call-
backs because such calls require a call stack lock. If these conditions are met, q can
transfer its top environment and the top of its obtained request queue locks to p .Given
this context, p can then execute the delegated statements instead of q .
The execute delegated

( , , { ,..., } )

operation sets up a new context on
p with an environment x and obtained request queue locks

s w x q 1 q m

{ ,..., }

.Tosetup
the new context, the operation uses a combination of the commands push env and
delegate obtained rq locks . The command delegate obtained rq locks requires that the
request queue locks

q 1 q m

are not in possession of another processor anymore. It
also requires that the request queues of

{ q 1 ,..., q m }

are locked. Once the context is set
up, processor p executes the statements s w and then gets rid of the context, using the
leave delegated operation.
To delegate the execution of the statements s w , processor q must make sure that its
top environment x is set up correctly and it must make sure that the top set of its obtained
request queue locks contains all locks

{ q 1 ,..., q m }

that are necessary for the execution
of s w . Processor q must then issue a execute delegated (

{ q 1 ,..., q m }

s w , x , { q 1 ,..., q m } ) operation

to processor p . Processor q must then remove from its stack of obtained

request queue locks so that the delegate obtained rq locks operation can take place.

{ q 1 ,..., q m }