- 19.12 (released) ...
- Reasoning Guarantees
- Inline Separate
- Controlled Objects
- Exclusive Access to multiple regions
- Waiting for regions
The topic of exclusive access was already briefly touched in Separate Calls. In this chapter, we'll have a deeper look at the exclusive access guarantees given in SCOOP, and what it means in practice.
In the SCOOP model, there are two very important guarantees - Order Preservation and Exclusive Access.
The first guarantee is always valid. A SCOOP processor is never allowed to reorder two feature calls when both have been logged by the same region. However, the order preservation guarantee only holds between two processors - it is not valid in a global context. For example, when a region A first logs a command to C, and then another region B logs a command to C, you generally don't know which feature will be applied first. And also the other way around: You have no guarantee on the order of feature application when A logs both an (asynchronous) separate call to B and C.
Exclusive access on the other hand is only valid in certain contexts. When an object is controlled, SCOOP guarantees exclusive access to the region that contains the object. We'll define the term controlled a bit later, but you've already seen an example in Separate Calls: A separate object which is passed as an argument.
These two basic guarantees in the SCOOP model are important to reach one of the main goals: The ability to reason about a program should be preserved in a concurrent program. SCOOP guarantees that a controlled object behaves just like in a sequential program, meaning that Pre- and Postconditions will remain valid in between feature calls because no other processor can interfere.
Passing a separate object as an argument is not the only way to gain exclusive access in SCOOP. While in theory the mechanism would be sufficient, experience has shown that it's often bulky and not very elegant to write a new routine whenever one wants to call a feature on a separate target.
Therefore SCOOP introduces the Inline Separate block to make things a bit easier.
person: separate PERSON
separate person as l_person do
The separate block evaluates the expression on the left hand side of the
as keyword, assigns it to the new read-only local variable
l_person on the right hand side,
and does whatever is necessary to provide exclusive access to the region that handles
You can think of the inline separate block as syntactic sugar that creates a new wrapper routine (although inline separate still lets you access local variables of the enclosing routine):
person: separate PERSON
anonymous_wrapper (l_person: separate PERSON)
The Eiffel compiler introduces the concept of a controlled object to support the exclusive access guarantee.
An object is always controlled with respect to the processor handling
Current, and the meaning is that the current processor has Exclusive Access to the region that holds the object. In particular, this means that no other processor can access or modify a controlled object.
In chapter Separate Calls we've already mentioned that SCOOP places a restriction on separate calls. A separate call is allowed if the target appears as a formal argument of the enclosing routine. While this rule is correct, it does not cover all of the cases. With the above definition however, we can both simplify and extend the previous Separate Argument rule:
The compiler checks this property at compile-time and throws an error if a separate call happens on an uncontrolled target.
Exclusive Access to multiple regions
It is possible to gain exclusive access to multiple regions simultaneously. This can either be done by passing multiple arguments to a region, or with an inline separate block.
balance_with_arguments (incr: separate INCREMENTER; decr: separate DECREMENTER): INTEGER
Result := incr.value + decr.value
separate incrementer as incr, decrementer as decr do
Result := incr.value + decr.value
incrementer: separate INCREMENTER
decrementer: separate DECREMENTER
Exclusive access to the arguments is granted atomically in this case. This ensures that no deadlock can occur when two regions want to gain access to the same regions, provided that they both use the "multiple-arguments-mechanism" of SCOOP and don't lock regions one after the other by hand.
Waiting for regions
You may wonder how the exclusive access guarantee is implemented in SCOOP. A simple solution would be to have a lock for every region, and to gain exclusive access, one has to acquire the lock. Before the 15.01 release, this was indeed how it was implemented. However, the implementation proved to be flawed because it caused a lot of synchronization and waiting.
In EiffelStudio 15.01 this has changed. When a processor needs exclusive access to another one, it opens a new queue to log calls. There can be multiple open queues to a processor, but the processor will always work on only one queue.
This has an important effect in practice: Gaining exclusive access to a region is always non-blocking. Note that this is also true for exclusive access to multiple regions. Previously it may have been necessary to wait for another processor to relinquish the lock, but now a processor can just proceed with logging calls, which will eventually be executed by the supplier processor.
You may start to wonder now where waiting happens, as it isn't possible to both have a guarantee for exclusive access and fully non-blocking behaviour. Well, it happens during synchronous calls. When a client gains exclusive access and starts logging calls, the supplier may not care about it yet because it is busy with something else. However, as soon as a synchronous call is logged, the client needs to wait for the result. During that time, the supplier will finish its other tasks and eventually start to execute the calls logged by the suspended client, at which point it will wake up again.
- Gaining exclusive access, also to multiple regions, is always non-blocking.
- An asynchronous call is also non-blocking.
- Only a call to a query may be blocking, and thus a place where a processor can be stuck (e.g. in case of deadlock or starvation).