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

Both the producer and the consumer access an unbounded buffer:

buffer : separate BUFFER [ INTEGER ]
−−

The data structure for exchanging objects between the producer and the
consumer.

Both the producer and the consumer need to access the buffer, in calls such as buffer . put
( x )and buffer . item . The basic SCOOP rule to ensure mutual exclusion and guarantee
the absence of data races is that any target that is declared as separate, such as buffer ,
must be an argument of an enclosing routine, which in turn guarantees that this routine
has exclusive access to the corresponding separate object for the duration of its execu-
tion. The SCOOP scheduler locks the processors handling all objects corresponding to
these controlled arguments. This rule prevents any data races on the group of controlled
objects. For example, in a call consume ( buffer ), the buffer is controlled; the call gets
exclusive access to its handler.
Condition synchronization relies on preconditions (after the require keyword) to
express wait conditions. Any precondition of the form x . some condition will make the
execution of the routine wait until the condition is true. For example, the precondition
of the consume routine ensures that the routine will wait until the buffer is not empty.

consume ( buffer : separate BUFFER [ INTEGER ])
−− Consume an item from the buffer.

require
not ( buffer . count =0)
local
consumed item : INTEGER

do

consumed item := buffer . item

end

During a feature call, the consumer processor could pass its locks to the buffer processor
if it has a lock that the buffer processor requires. This mechanism is known as lock
passing . In such a case, the consumer processor would have to wait for the passed locks
to return. For the feature call buffer . item , the buffer processor does not require any
locks from the consumer processor. Hence, the consumer processor does not have to
wait due to lock passing. However, the runtime system ensures that the result of the call
buffer . item is properly assigned to the entity consumed item using a mechanism called
wait by necessity : while the consumer processor usually does not have to wait for an
asynchronous call to finish, it will do so if it needs the result of this call.
As the buffer is unbounded, the corresponding producer routine does not need a wait
condition; mutual exclusion will be ensured as before:

produce ( buffer : separate BUFFER [ INTEGER ])
−−

Produce an item and put it into the buffer.