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

The check post and unlock rqs operation also takes a processor set q m }

and a feature f . The processor set is the same as for the check pre and lock rqs op-
eration, i.e., the set of processors whose request queues got locked in the synchroniza-
tion step. The operation first determines whether the postcondition should be evaluated
synchronously or asynchronously. Then the operation starts the evaluation. Finally, the
operation enqueues an unlock operation to each request queue in

{ q 1 ,...,

{ q 1 ,..., q m } .

Clarification 5 (Asynchronous postcondition evaluation). The postcondition can be
evaluated asynchronously if every feature call in the postcondition only requires a re-
quest queue lock that was obtained in the synchronization step and if the postcondition
does not involve lock passing. If the postcondition has a feature call that requires a lock
different from the obtained request queue locks, then p cannot delegate its obtained
request queue lock and then continue because the required lock would be required in
another feature execution context as well. Hence the postcondition must be evaluated
synchronously in this case. If the postcondition involves lock passing, then one of p 's
lock might be necessary for the evaluation of the postcondition. Hence, p must pass
its locks and cannot proceed until the postcondition is evaluated and the passed locks
returned. Once again, the postcondition must be evaluated synchronously. In Nienal-
towski's description of SCOOP [25] a postcondition can be evaluated asynchronously
if the current processor is not involved in the postcondition evaluation. This rule permits
configurations in which the evaluating processor does not have the necessary locks for
the evaluation.

If the postcondition can be evaluated asynchronously, then the operation can take one of
the processors in . This set does not contain processor p because processor

p never obtains its own request queue lock. Each processor in this set is exclusively
available in the current execution context and can thus be used to evaluate the postcon-
dition asynchronously. The check post and unlock rqs operation defines g 0 to be
the evaluating processor according to the rule just presented. It also defines

{ q 1 ,..., q m }

{ g 1 ,..., g j }

to be the set minus the request queue lock of g 0 .If p is the evaluating

processor, then this set is the same as

{ q 1 ,..., q m }

. As a result of these definitions, the
postcondition can be evaluated asynchronously if g 0

{ q 1 ,..., q m }

= p . Otherwise, the postcondition

must be evaluated synchronously.
In the synchronous case, processor p evaluates the postcondition, enqueues unlock
operations to each request queue in

{ ,..., }

, and then removes the corresponding
locks from its stack of obtained request queue locks. The unlock operations will not
proceed until the locks have been removed from p 's stack of obtained request queue
locks. In the asynchronous case, processor p must delegate the postcondition evalua-
tion to processor g 0 . For this purpose, p enqueues an execute delegated operation
to g 0 . The workload involves the postcondition evaluation along with the subsequent
issuing of unlock operations to all processor in

q 1 q m

. Processor g 0 unlocks its
own request queue after the delegated execution. The evaluation of the postcondition
on g 0 requires the environment that defines the values of the entities in the postcondi-
tion. Furthermore, the evaluation requires the request queue locks

{ g 1 ,..., g j }

.These
locks are sufficient because the postcondition only gets evaluated asynchronously if the
evaluation only requires these locks. To satisfy these two requirements, p gives its top

{ q 1 ,..., q m }