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

p and now p is calling back processor q . The separate callback is only possible if p has
alockon q .However, p does not necessarily have this lock because the lock might be
in possession of the processor that locked q in the first place. Request queue locks and
call stack locks allow us to clarify the situation. Thus we propose a new lock model
with request queue locks and call stack locks.
The lock model used in Nienaltowski's work [25] is an abstraction of the new lock
model. The abstraction works under the assumption that no processor passes its locks.
Under this assumption each processor keeps its call stack lock. In this abstraction, the
request queue lock on a processor p is called the lock on p . As long as the call stack
lock on a processor p is in possession of p , a request queue lock on p in possession of a
processor q means that processor p will be executing new feature requests in the request
queue exclusively on behalf of q . This means that a request queue lock grants exclusive
access to all the objects handled by p . Transferring this insight to the abstraction, a lock
on processor p denotes exclusive access to the objects handled by p .
The formalization defines the ADT PROC for processors. A processor has an identifier
stored in the query id .
The constructor make returns a new processor with a fresh identifier. The fresh iden-
tifier is defined through the query new id .
make : PROC
axioms
make . id = new id
The ADT PROC is very simple. It neither takes care of the mapping from processors
to the handled objects nor does it take care of the locks. These aspects are taken care of
by the ADT for regions.
Mapping of processors to objects and locking. This section introduces the ADT REG
for regions. This ADT declares a query procs that keeps track of all the processors in the
system. The query handled objs defines a set of handled objects for each processor in
procs . Finally, the query last added proc denotes the last processor that has been added
to procs .
procs : REG → SET [ PROC ]
handled objs : REG → PROC SET [ OBJ ]
k . handled objs ( p ) require
k . procs . has ( p )
last added proc : REG PROC
k . last added proc require
¬ k . procs . is empty
Next to the queries that are concerned with the mapping from processors to objects,
there are a number of queries that deal with locking. The feature rq locked states
whether the request queue of a processor in procs is locked or not. Similarly, the feature
cs locked states whether the call stack is locked.