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

required request queue locks and another set with required call stack locks. The set of
required call stack locks is composed of p that will lead to a non-separate call and all the
processors that will lead to separate callbacks. The set of required request queue locks
is composed of the processors that will lead to separate calls. The operation defines two
sets for these two categories: g required cs locks and g required rq locks .
Each processor initially has its own call stack lock as its obtained call stack lock.
This call stack never gets unlocked. This means that other call stack locks cannot be
obtained; they must be retrieved through lock passing. The condition of the inference
rule expresses this: σ . . The operation can be

assured that p did not pass its own call stack lock because otherwise p would be waiting.
The remaining required call stack locks are the ones for the processors that will lead to
separate callbacks. Note that the lock passing conditions are not sufficient to guarantee
that the call stack locks for separate callbacks are always available.
As for the request queue locks, the operation calculates g missing rq locks as the required
request queue locks minus the already owned request queue locks. The already owned
request queue locks are the previously obtained request queue locks and the retrieved
request queue locks. In the synchronization step, the operation must obtain the differ-
ence. If this is not possible because some of the missing request queue locks are not
available, then the operation must wait. The check pre and lock rqs operation takes
care of this; it takes g missing rq locks and the feature f . Once the execution succeeds, p
has the request queue locks of g missing rq locks and the precondition of f holds.
The apply operation can be assured that each processor g , whose obtained request
queue lock the operation got in the synchronization step, must be in possession of its
call stack lock. If g was not in possession of its call stack lock, it must have passed
its locks. This means that g is executing a feature call and still waiting for the locks to
return. In order to execute the feature call, there must have been a lock on g 's request
queue lock so that its action queue can contain the feature call. The request queue must
still be locked because g is still executing the feature call. Hence, it would not have been
possible to obtain g 's request queue lock. The only exception is the bootstrap processor.
However this processor only plays a role in the system setup and it never passes its own
call stack lock.
Once the operation got all the required locks, it can execute the body. For once func-
tions it must update the once status whenever it writes to the result entity as part of
an assignment instruction or as part of a creation instruction. For this purpose it adds
a read operation and a set not fresh operation after each assignment instruction or
creation instruction. For each assignment instruction or creation instruction it has to use
a fresh channel.
After the execution of the body, the operation has to evaluate the postcondition and it
has to make sure that the locked request queues get unlocked at the right time. These two
steps are performed by another operation check post and unlock rqs that takes the
missing request queue locks g missing rq locks and the feature f . This operation evaluates
the postcondition either synchronously or asynchronously. After the evaluation of the
postcondition, the operation enqueues an unlock operation to each request queue in
g missing rq locks .

∀ x ∈ g required cs locks : cs locks ( p ) . has ( x )