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

The remaining queries specify the owners of the locks. For this, the formalization
distinguishes between obtained and retrieved locks. Obtained locks are locks that got
acquired by a processor. Retrieved locks are locks that got passed from another processor.
The query obtained rq locks returns a stack of obtained processor sets for a proces-
sor. A stack of sets models the way processors acquire locks: they go through a nested
series of feature applications and each feature application requires a set of locks before
the feature can be executed. For each feature application the executing processor adds
a new set on top of its stack. As soon as the feature application finished, the processor
removes the top set from its stack. The query obtained cs lock returns the acquired call
stack lock of a processor. Initially each processor starts with a lock on its own call stack
and this call stack lock never changes. Thus this query is only declared for reasons of
completeness. If a processor appears in a set of request queue locks, then the processor
denotes its request queue lock. If a processor appears in a set of call stack locks, then
the processor denotes its call stack lock.
A processor can pass its locks to another processor. There are several queries to
formalize this aspect. The features retrieved rq locks and retrieved cs locks return the
retrieved locks of a processor. Both of these queries return a stack of sets. The stack
keeps track of the set of retrieved locks for each feature application. These two stacks
grow and shrink in parallel to the stack obtained rq locks . Once a processor passed its
locks, it cannot use them anymore until the locks are revoked. The query locks passed
returns whether a processor passed some or all of its locks or not.
The following discussion first goes through the list of commands that add processors
and commands that change the association of processors to objects. It then proceeds
with the commands that handle locks. The command add proc updates the regions with
a new processor. Note that the processor must have been created beforehand. The ax-
ioms state that the new processor will be included in procs and that it will be stored in
last added proc . The axioms also state how the new processor is initialized. The new
processor's request queue is unlocked and its call stack is locked. Apart from the initial
lock on the call stack there are no obtained or retrieved locks and hence the processor
did not pass its locks.

add proc : REG → PROC REG
k . add proc ( p ) require
¬ k . procs . has ( p )
axioms
k . add proc ( p ) . procs . has ( p )
k . add proc ( p ) . last added proc = p
k . add proc ( p ) . handled objs ( p ) . is empty
¬ k . add proc ( p ) . rq locked ( p )

k )

k . add proc ( p ) . obtained rq locks ( p ) . is empty
k . add proc ( p ) . obtained cs lock ( p )= p
k . add proc ( p ) . retrieved rq locks ( p ) . is empty
k . add proc ( p ) . retrieved cs locks ( p ) . is empty
¬ k . add proc ( p ) . locks passed ( p )

. add proc ( p ) . cs locked ( p

The command add obj takes a processor p in procs and an object o that is not handled
by a processor in procs yet. It returns the updated regions in which o is handled by p .