Exclusive Access

    Contents
    1. Reasoning Guarantees
    2. Inline Separate
    3. Controlled Objects
    4. Exclusive Access to multiple regions
    5. 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.

Reasoning Guarantees

In the SCOOP model, there are two very important guarantees - Order Preservation and Exclusive Access.

Definition -- Order Preservation : The guarantee that, between any two regions, the order of separate feature calls logged by one region is the same as the order of feature applications by the other region.

Definition -- Exclusive Access (to a region) : The guarantee that no intervening features logged by other processors are executed.

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.

Inline Separate

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 show_separate_block do separate person as l_person do print (l_person.age) end end

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 l_person.

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 show_separate_block do anonymous_wrapper (person) end anonymous_wrapper (l_person: separate PERSON) do print (l_person.age) end

Controlled Objects

The Eiffel compiler introduces the concept of a controlled object to support the exclusive access guarantee.

Definition -- Controlled/uncontrolled object: An object is controlled if it is attached to a reference that has one of the following properties:
1) It is of a non-separate type.
2) It is of a separate type and it appears as a formal argument of the enclosing routine.
3) It is a local variable of an inline separate block.

Otherwise it is uncontrolled.

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:

Rule -- Controlled Target: A separate call is valid if its target is controlled.

The compiler checks this property at compile-time and throws an error if a separate call happens on an uncontrolled target.

Note: Query results with a non-separate return type are placed on the same processor as the target. This means that, if a processor controls the target, it is also safe to use these query results. The compiler tries to exploit this fact a little by treating such query results as controlled as well within a single expression. This allows to have multi-dot calls on separate target, such as sep_person.spouse.name.out.
Note that this does not yet cover all cases where controlled can be inferred, and the compiler may become smarter in the future.

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 do Result := incr.value + decr.value end balance_with_inline_separate: INTEGER do separate incrementer as incr, decrementer as decr do Result := incr.value + decr.value end end 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.

See Also: The dining philosopher example makes use of this fact. The feature {PHILOSOPHER}.eat has two separate arguments, which are guaranteed to be locked in one atomic step by the SCOOP runtime. If this were not the case, a deadlock may occur.

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.

Note: Due to this, the only way to experience a deadlock in SCOOP is when a processor is stuck in a separate query.

To summarize:

  • 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).
7f5adf71-7169-c54e-9bed-079c84aee8d3
cached: 07/21/2017 4:54:01.000 AM