Ravenscar-compliant bounded buffer

[Maciej Sobczak <see.my.homepage@gmail.com>]

In one of my previous posts I have criticized example 12 from the
Ravenscar document.
It makes sense to criticize constructively, I think. :-)

-- bounded_buffer.ads
package Bounded_Buffer is

   type Buffer_Type is limited private;

   procedure Put (Buffer : in out Buffer_Type; Item : in Integer);
   procedure Get (Buffer : in out Buffer_Type; Item : out Integer);

private

   protected type Binary_Semaphore (Initial_State : Boolean) is
      entry Acquire;
      procedure Release;
   private
      Available : Boolean := Initial_State;
   end Binary_Semaphore;

   type Buffer_Type is limited record
      Storage : Integer;
      Available_For_Reading : Binary_Semaphore (Initial_State =>
False);
      Available_For_Writing : Binary_Semaphore (Initial_State =>
True);
   end record;

end Bounded_Buffer;

-- bounded_buffer.adb
package body Bounded_Buffer is

   procedure Put (Buffer : in out Buffer_Type; Item : in Integer) is
   begin
      Buffer.Available_For_Writing.Acquire;
      Buffer.Storage := Item;
      Buffer.Available_For_Reading.Release;
   end Put;

   procedure Get (Buffer : in out Buffer_Type; Item : out Integer) is
   begin
      Buffer.Available_For_Reading.Acquire;
      Item := Buffer.Storage;
      Buffer.Available_For_Writing.Release;
   end Get;

   protected body Binary_Semaphore is

      entry Acquire when Available is
      begin
         Available := False;
      end Acquire;

      procedure Release is
      begin
         Available := True;
      end Release;

   end Binary_Semaphore;

end Bounded_Buffer;

-- test.adb
with Ada.Text_IO;
with Bounded_Buffer;

procedure Test is

   Buffer : Bounded_Buffer.Buffer_Type;

   task Writer;
   task body Writer is
   begin
      for I in 1 .. 50 loop
         Bounded_Buffer.Put (Buffer, I);
      end loop;

      Bounded_Buffer.Put (Buffer, 0);
   end Writer;

   task Reader;
   task body Reader is
      I : Integer;
   begin
      loop
         Bounded_Buffer.Get (Buffer, I);
         exit when I = 0;
         Ada.Text_IO.Put (Integer'Image (I));
         Ada.Text_IO.New_Line;
      end loop;
   end Reader;

begin
   null;
end Test;


I would like to ask you to comment/criticize on the above.
(The test.adb driver is provided just to sanity-check the rest.)

Note that in this example the shared data (Storage component of the
Buffer object) is accessed directly from concurrent subprograms.
Protecting this access is not necessary on the basis that binary
semaphores provide necessary exclusion and signalling (ordering). With
buffer of capacity > 1 the storage array and top/bottom indices would
be encapsulated by another protected object.

--
Maciej Sobczak
http://www.msobczak.com/