2.4.7 Resource revocation

Resources are not revoked by the \opp{} \uk{}. Instead, an UNAVAILABLE exception is raised for the resource exhausted; so that users could run whatever algorithm is needed to make more units of the resource being exhausted.

The exception trigger is the allocator being used. System allocators are provided with an Exhausted object at instantiation time for that purpose.

<Other protected members of off_Allocator. >= (<-U)
off_Exhausted *a_revocator;    //  Resource revocator.

<Other public methods of off_Allocator. >= (<-U) [D->]
// Creates an allocator.
off_Allocator(off_Exhausted *r) : a_revocator(r) {;}

The Exhausted data type is included together with the allocator code.

<Off allocator data types. >= (<-U)
<Off Exhausted resource revocation trigger. >

The Exhausted object provides a single method notify to let allocators trigger the proper action (by default, to raise an UNAVAILABLE exception).

<Off Exhausted resource revocation trigger. >= (<-U)
// Resource revocator.
//
signature off_Exhausted {
// NB: A signature always has public access.

   // Notify that resource is exhausted
   void notify(void);
};

Defines off_Exhausted (links are to index).

Allocators provide an exhausted method which relies on notify.

<Other public methods of off_Allocator. >+= (<-U) [<-D->]
// This resource is exhausted. Trigger appropriate actions. 
void exhausted(void){ if (!null(a_revocator)) a_revocator->notify(); }

Consider again the a_revocator member in Allocator. There is a single way to initialize it: passing an argument to the Allocator constructor. This will also happen with other members of Allocator subclasses.

However, sometimes it is useful to declare an Allocator and initialize it later on (eg. to reserve enough space for a member of type Allocator). We can do it by using the predefined copy operator and defining another (empty) constructor. We will be doing the same with subclasses of Allocator.

<Other public methods of off_Allocator. >+= (<-U) [<-D]
// Allows declarations of uninitialized allocators.
off_Allocator(void) {;}

It should be clear that no allocator can be used before initialized either by calling its first constructor or by copying on it an allocator already initialized.