ParaSail concurrent interfaces

A ParaSail interface can be marked as concurrent, meaning that an object of a type produced by instantiating such a concurrent interface can be accessed concurrently by multiple parallel threads.  We use the term concurrent type for a type produced by instantiating a concurrent interface, and concurrent object for an object of a concurrent type.

Both lock-based and lock-free synchronization techniques can be used to coordinate access to a concurrent object.  In addition, operation queues are provided to hold operation requests that cannot be serviced until the concurrent object attains a desired state, as specified by the dequeue condition.  When a thread initiates an operation request, if it can't be performed immediately because the condition is False, the thread is blocked until the request gets dequeued and the associated operation is completed, or the operation request is canceled for some reason, such as a timeout.   In general, multiple operation requests may be queued simultaneously on behalf of a single thread, with the first one to be dequeued causing the automatic cancellation of the others.

With a lock-based concurrent interface, one of the operands of a procedure or function of the interface, if the operand is of the type defined by the interface, can be marked indicating it should be locked upon call. When calling the operation,  the operand's lock will be acquired automatically upon entry to the operation, and the lock will be released upon return.  Alternatively, one operand of a concurrent interface operation may be marked queued, meaning that the dequeue condition must be true before the operation will be performed, and when it is performed it will be locked automatically as well.

Within the concurrent class implementing a lock-based concurrent interface, the components of an operand marked locked or queued may be referenced directly, knowing that the access is single-threaded at that point.  If there are other (non-locked/queued) operands of the associated concurrent type, their non-concurrent components may not be referenced by the operation.  An operation with a queued operand has the further assurance that at the point when the operation starts, the dequeue condition is True.  The dequeue condition for a given operation may depend on the values of the non-concurrent parameters, plus the internal state of the (concurrent) operand marked queued.

Within the concurrent class implementing a lock-free concurrent interface, all data components must themselves be concurrent objects, since no locking is performed on entry to the operations of the class.  Typically these components will be of low-level concurrent types, such as a single memory cell that supports atomic load, atomic store, and atomic compare-and-swap (CAS), or a somewhat higher-level concurrent type that supports multi-word-compare-and-swap (MCAS).  The ParaSail standard library provides a small number of such lower-level concurrent types to support implementing lock-free concurrent interfaces.  The higher level queued operations are implemented using a lower-level race-free and lock-free concurrent type similar to a private semaphore, which can be used directly if desired.

Here is an example of a concurrent interface and corresponding concurrent class for implementing a simple bounded buffer:

concurrent interface Bounded_Buffer
  <Element_Type is Assignable<>;
   Index_Type is Integer<>> is
    function Create_Buffer(
      Max_In_Buffer : Index_Type {Max_In_Buffer > 0})
      -> Result : Bounded_Buffer;
      // Create buffer of given capacity

    procedure Put(Buffer : queued Bounded_Buffer; 
      Element : Element_Type);
      // Add element to bounded buffer; 
      // remain queued until there is room
      // in the buffer.

    function Get(Buffer : queued Bounded_Buffer)
      -> Element_Type;
      // Retrieve next element from bounded buffer;
      // remain queued until there is an element.
end interface Bounded_Buffer; 

concurrent class Bounded_Buffer
  <Element_Type is Assignable<>;
   Index_Type is Integer<>> is
    const Max_In_Buffer : Index_Type {Max_In_Buffer > 0};
    var Data : Array<Element_Type, Index_Type> := 
      Create_Array(1, Max_In_Buffer);
    var Next_Add : Index_Type 
      {Next_Add in 1..Max_In_Buffer} := 1;
    var Num_In_Buffer : Index_Type 
      {Num_In_Buffer in 0..Max_In_Buffer} := 0;
  exports
    function Create_Buffer(
      Max_In_Buffer : Index_Type {Max_In_Buffer > 0}) 
      -> Bounded_Buffer
      // Create buffer of given capacity
    is
        return (Max_In_Buffer => Max_In_Buffer);
    end function Create_Buffer;

    procedure Put(Buffer : queued Bounded_Buffer; 
      Element : Element_Type)  
      queued until 
        Buffer.Num_In_Buffer < Buffer.Max_In_Buffer 
      // Add element to bounded buffer;
      // remain queued until there is room
      // in the buffer.
    is
        Buffer.Data[Buffer.Next_Add] := Element; 
        // Advance to next element, cyclically.
        Buffer.Next_Add := 
         (Buffer.Next_Add mod Buffer.Max_In_Buffer) + 1;
        Buffer.Num_In_Buffer += 1;
    end procedure Put;

    function Get(Buffer : queued Bounded_Buffer)
      -> Element_Type
      queued until Buffer.Num_In_Buffer > 0 
      // Retrieve next element from bounded buffer;
      // remain queued until there is an element.
    is
         return Buffer.Data[
           ((Buffer.Next_Add - Buffer.Num_In_Buffer - 1)
             mod Buffer.Max_In_Buffer) + 1];
    end function Get;
end class Bounded_Buffer; 

This concurrent interface has one constructor, plus two queued operations, Put and Get.  The dequeue conditions are provided as part of the implementation of an operation with a queued operand.  Here the dequeue conditions are Buffer.Num_In_Buffer < Buffer.Max_In_Buffer for Put, and Buffer.Num_In_Buffer > 0 for Get.  These dequeue conditions ensure that when the operations are performed, they can proceed without an error.

An example of a lock-free concurrent interface will be given in a later post.