Gem #81: GNAT Semaphores

by Pat Rogers —AdaCore

Let's get started…


A number of semaphore definitions exist, although the general concept remains as introduced by Dijkstra in 1968. We assume the reader has some familiarity with semaphores and their semantics, and so we will not cover them here. Many books are available for those requiring additional information. See especially Principles of Concurrent and Distributed Programming by M. Ben-Ari.

The GNAT.Semaphores package defines two semaphore abstractions, both in terms of protected types. We use protected types, rather than defining abstract data types based on operating-system facilities, for the sake of portability. A simple wrapper around the facilities of an operating system or RTOS would be reasonable, but the resulting interface (and implementation, of course) would not have the portability required of the general-purpose GNAT hierarchy.

The first abstraction defines a "counting" semaphore, in which an integer count is maintained by the operations, such that the acquire operation only executes (and thus returns, allowing the caller to continue) when the count is greater than zero. Counting semaphores are convenient for expressing condition synchronization in terms of the availability of some number of resources. For example, with a circular bounded buffer, a semaphore's count can represent the number of available buffer slots. Callers must wait for the buffer to be non-full when attempting to insert a new item, and the blocking call to acquire the semaphore will achieve that effect directly.

The declaration for the counting semaphore is as follows. Note that we have removed the in-line comments for the sake of brevity, but will cover their content.

   protected type Counting_Semaphore
      (Initial_Value : Natural;
      Ceiling : System.Priority)
   is
      pragma Priority (Ceiling);

      entry Seize;
      procedure Release;

   private
      Count : Natural := Initial_Value;
   end Counting_Semaphore;

The second type implements "binary" semaphores. This kind of semaphore is less flexible than the counting semaphore, in that no notion of a count is maintained. The abstraction is simply that of a flag indicating whether or not the semaphore is available. (If the value of a counting semaphore varied between zero and one, the effect would be the same.)

   protected type Binary_Semaphore
     (Initially_Available : Boolean;
      Ceiling : System.Priority)
   is
      pragma Priority (Ceiling);

      entry Seize;
      procedure Release;

   private
      Available : Boolean := Initially_Available;
   end Binary_Semaphore;

In both cases, the provided operations consist of an entry "Seize" to acquire the semaphore with mutually exclusive access, and a protected procedure "Release" to release it. The Seize operation must be an entry for the sake of the barrier expressing the required condition synchronization. Releasing the semaphore has no such requirement, so it need not be an entry.

Both types are visibly defined as protected types so that users can make conditional and timed calls when appropriate. This capability addresses one of the portability problems with semaphores. Although the basic "acquire" and "release" operations will always be provided (by whatever name), there is no "standard" interface for other forms of interaction. Language-defined constructs provide some of those kinds of interactions, and do so portably.

Both types require discriminants. The counting semaphore type uses a discriminant to specify the initial nonnegative value of the count. The binary semaphore type uses a Boolean discriminant to specify whether the semaphore should be initially available. For example, a binary semaphore would be initially available when used to express mutual exclusion, but might not be initially available when used to express condition synchronization.

In addition, both types use another discriminant to specify the ceiling priority for objects of the type. The discriminant is then passed as the argument to pragma Priority. If the Real-Time Systems Annex is in force this part is essential; otherwise it has no effect. Note that a default value cannot be provided for the Ceiling discriminant because that would require a default for the other discriminant, too. The best we can do is to define a convenient value to be used in declarations of individual objects when the Real-Time Annex is not in force, so the following constant is provided in GNAT.Semaphores:

   Default_Ceiling : constant System.Priority := System.Default_Priority;

However, subtypes can be used to enhance convenience, readability and robustness. The earlier Gem (#70) provided an example:

   subtype Mutual_Exclusion is Binary_Semaphore
     (Initially_Available => True,
      Ceiling             => Default_Ceiling);

The subtype ensures that corresponding objects are initially available, but also conveniently supplies the Ceiling discriminant value (assuming the Real-Time Annex is not in force) and gives the reader an indication of the intended use.

As you can see, the declarations of protected types can be very expressive. The discriminants are the part you might not have considered using, although that is by no means an unusual approach. The protected bodies of both types are trivial and will not be shown here. You can see them in the GNAT hierarchy, along with the implementations of all the other GNAT hierarchy packages.


About the Author

Pat Rogers has been a computing professional since 1975, primarily working on microprocessor-based real-time applications in Ada, C, C++ and other languages, including high-fidelity flight simulators and Supervisory Control and Data Acquisition (SCADA) systems controlling hazardous materials. Having first learned Ada in 1980, he was director of the Ada9X Laboratory for the U.S. Air Force’s Joint Advanced Strike Technology Program, Principle Investigator in distributed systems and fault tolerance research projects using Ada for the U.S. Air Force and Army, and Associate Director for Research at the NASA Software Engineering Research Center. He has B.S. and M.S. degrees in computer systems design and computer science from the University of Houston and a Ph.D. in computer science from the University of York, England. As a member of the Senior Technical Staff at AdaCore, he specializes in supporting real-time/embedded systems developers, creates and provides training courses, and is project leader and a developer of the GNATbench Eclipse plug-in for Ada. He also has a 3rd Dan black belt in Tae Kwon Do and is founder of the AdaCore club “The Wicked Uncles”.