-- C940A03.A
--
--                             Grant of Unlimited Rights
--
--     Under contracts F33600-87-D-0337, F33600-84-D-0280, MDA903-79-C-0687,
--     F08630-91-C-0015, and DCA100-97-D-0025, the U.S. Government obtained 
--     unlimited rights in the software and documentation contained herein.
--     Unlimited rights are defined in DFAR 252.227-7013(a)(19).  By making 
--     this public release, the Government intends to confer upon all 
--     recipients unlimited rights  equal to those held by the Government.  
--     These rights include rights to use, duplicate, release or disclose the 
--     released technical data and computer software in whole or in part, in 
--     any manner and for any purpose whatsoever, and to have or permit others 
--     to do so.
--
--                                    DISCLAIMER
--
--     ALL MATERIALS OR INFORMATION HEREIN RELEASED, MADE AVAILABLE OR
--     DISCLOSED ARE AS IS.  THE GOVERNMENT MAKES NO EXPRESS OR IMPLIED 
--     WARRANTY AS TO ANY MATTER WHATSOEVER, INCLUDING THE CONDITIONS OF THE
--     SOFTWARE, DOCUMENTATION OR OTHER INFORMATION RELEASED, MADE AVAILABLE 
--     OR DISCLOSED, OR THE OWNERSHIP, MERCHANTABILITY, OR FITNESS FOR A
--     PARTICULAR PURPOSE OF SAID MATERIAL.
--*
--
-- OBJECTIVE:
--      Check that a protected object provides coordinated access to
--      shared data.  Check that it can implement a semaphore-like construct
--      controlling access to shared data through procedure parameters to
--      allow a specific maximum number of tasks to run and exclude all
--      others.
--
-- TEST DESCRIPTION:
--      Declare a resource descriptor tagged type.  Extend the type and
--      use the extended type in a protected data structure.
--      Implement a counting semaphore type that can be initialized to a 
--      specific number of available resources.  Declare an entry for 
--      requesting a specific resource and an procedure for releasing the 
--      same resource it.  Declare an object of this (protected) type, 
--      initialized to two resources.  Declare and start three tasks each 
--      of which asks for a resource.  Verify that only two resources are 
--      granted and that the last task in is queued.
--
--      This test models a multi-user operating system that allows a limited
--      number of logins.  Users requesting login are modeled by tasks.
--
--
-- TEST FILES:
--      This test depends on the following foundation code:
--
--         F940A00
--
--
-- CHANGE HISTORY:
--      06 Dec 94   SAIC    ACVC 2.0
--      13 Nov 95   SAIC    Fixed bugs for ACVC 2.0.1
--
--!

package C940A03_0 is
      --Resource_Pkg

  -- General type declarations that will be extended to model available
  -- logins

  type Resource_ID_Type is range 0..10;
  type Resource_Type is tagged record 
    Id : Resource_ID_Type := 0;
  end record;

end C940A03_0;
  --Resource_Pkg

--======================================--
-- no body for C940A3_0
--======================================--

with F940A00;     -- Interlock_Foundation
with C940A03_0;   -- Resource_Pkg;

package C940A03_1 is
     -- Semaphores

  -- Models a counting semaphore that will allow up to a specific 
  -- number of logins
  -- Users (tasks) request a login slot by calling the Request_Login
  -- entry and logout by calling the Release_Login procedure

  Max_Logins : constant Integer := 2;
  

  type Key_Type is range 0..100;
                                      -- When a user requests a login, an
                                      -- identifying key will be returned
  Init_Key : constant Key_Type := 0;

  type Login_Record_Type is new C940A03_0.Resource_Type with record
    Key  : Key_Type := Init_Key;
  end record;


  protected type Login_Semaphore_Type (Resources_Available : Integer :=1) is

    entry     Request_Login   (Resource_Key : in out Login_Record_Type);
    procedure Release_Login;
    function  Available return Integer;  -- how many logins are available?
  private
    Logins_Avail : Integer  := Resources_Available;
    Next_Key     : Key_Type := Init_Key;

  end Login_Semaphore_Type;

  Login_Semaphore      : Login_Semaphore_Type (Max_Logins);

  --====== machinery for the test, not the model =====--
  TC_Control_Message : F940A00.Interlock_Type;    
  function TC_Key_Val (Login_Rec : Login_Record_Type) return Integer;


end C940A03_1;
 -- Semaphores;

--=========================================================--

package body C940A03_1 is
          -- Semaphores is

  protected body Login_Semaphore_Type is

    entry Request_Login (Resource_Key : in out Login_Record_Type)
                                             when Logins_Avail > 0 is
    begin
      Next_Key := Next_Key + 1;        -- login process returns a key
      Resource_Key.Key := Next_Key;     -- to the requesting user
      Logins_Avail := Logins_Avail - 1;
    end Request_Login;

    procedure Release_Login is
    begin
      Logins_Avail := Logins_Avail + 1;
    end Release_Login;

    function Available return Integer is
      begin
        return Logins_Avail;
      end Available;

  end Login_Semaphore_Type;

  function TC_Key_Val (Login_Rec : Login_Record_Type) return Integer is
    begin
      return Integer (Login_Rec.Key);
    end TC_Key_Val;

end C940A03_1;
 -- Semaphores;

--=========================================================--

with C940A03_0;    -- Resource_Pkg,
with C940A03_1;    -- Semaphores;

package C940A03_2 is
     -- Task_Pkg

  package Semaphores renames C940A03_1;

  task type User_Task_Type is

     entry Login  (user_id : C940A03_0.Resource_Id_Type);
                      -- instructs the task to ask for a login
     entry Logout;    -- instructs the task to release the login
     --=======================--
     -- this entry is used to get information to verify test operation
     entry Get_Status (User_Record : out Semaphores.Login_Record_Type);

  end User_Task_Type;

end C940A03_2;
 -- Task_Pkg

--=========================================================--

with Report;
with C940A03_0;   -- Resource_Pkg,
with C940A03_1;   -- Semaphores,
with F940A00;     -- Interlock_Foundation;
    
package body C940A03_2 is
          -- Task_Pkg 

  -- This task models a user requesting a login from the system
  -- For control of this test, we can ask the task to login, logout, or
  -- give us the current user record (containing login information)

  task body User_Task_Type is
    Rec  : Semaphores.Login_Record_Type;
  begin
    loop
      select
        accept Login (user_id : C940A03_0.Resource_Id_Type) do
          Rec.Id := user_id;
        end Login;

        Semaphores.Login_Semaphore.Request_Login (Rec);
                      -- request a resource; if resource is not available, 
                      -- task will be queued to wait

        --== following is test control machinery ==--
        F940A00.Counter.Increment;
        Semaphores.TC_Control_Message.Post;   
               -- after resource is obtained, post message

      or
        accept Logout do  
          Semaphores.Login_Semaphore.Release_Login;
                      -- release the resource
          --== test control machinery ==--
          F940A00.Counter.Decrement;
        end Logout;
        exit;

      or
        accept Get_Status (User_Record : out Semaphores.Login_Record_Type) do
          User_Record := Rec;
        end Get_Status;

      end select;  
    end loop;

  exception
    when others => Report.Failed ("Exception raised in model user task");
  end User_Task_Type;

end C940A03_2;
 -- Task_Pkg

--=========================================================--

with Report;
with ImpDef;
with C940A03_1;   -- Semaphores, 
with C940A03_2;   -- Task_Pkg,
with F940A00;     -- Interlock_Foundation;

procedure C940A03 is

  package Semaphores renames C940A03_1;
  package Users      renames C940A03_2;  

  Task1, Task2, Task3 : Users.User_Task_Type;
  User_Rec            : Semaphores.Login_Record_Type;

begin      -- Tasks start here

  Report.Test ("C940A03", "Check that a protected object can coordinate " &
                          "shared data access using procedure parameters");

  if F940A00.Counter.Number /=0 then
    Report.Failed ("Wrong initial conditions");
  end if;
                                 
  Task1.Login (1);               -- request resource; request should be granted
  Semaphores.TC_Control_Message.Consume;  
                                 -- ensure that task obtains resource by
                                 -- waiting for task to post message

                                 -- Task 1 waiting for call to Logout
                                 -- Others still available
  Task1.Get_Status (User_Rec);
  if (F940A00.Counter.Number /= 1)
  or (Semaphores.Login_Semaphore.Available /=1)
  or (Semaphores.TC_Key_Val (User_Rec) /= 1) then
    Report.Failed ("Resource not assigned to task 1");
  end if;
 
  Task2.Login (2);               -- Request for resource should be granted  
  Semaphores.TC_Control_Message.Consume;  
                                 -- ensure that task obtains resource by
                                 -- waiting for task to post message
 
  Task2.Get_Status (User_Rec);
  if (F940A00.Counter.Number /= 2)
  or (Semaphores.Login_Semaphore.Available /=0)
  or (Semaphores.TC_Key_Val (User_Rec) /= 2) then
    Report.Failed ("Resource not assigned to task 2");
  end if;
 

  Task3.Login (3);               -- request for resource should be denied
                                 -- and task queued


                                 -- Tasks 1 and 2 holds resources
                                 -- and are waiting for a call to Logout
                                 -- Task 3 is queued

  if (F940A00.Counter.Number /= 2)
  or (Semaphores.Login_Semaphore.Available /=0) then
    Report.Failed ("Resource incorrectly assigned to task 3");
  end if;

  Task1.Logout;                  -- released resource should be given to
                                 -- queued task
  Semaphores.TC_Control_Message.Consume;  
                                 -- wait for confirming message from task

                                 -- Task 1 holds no resources
                                 --   and is terminated (or will soon)
                                 -- Tasks 2 and 3 hold resources
                                 --   and are waiting for a call to Logout

  Task3.Get_Status (User_Rec);
  if (F940A00.Counter.Number /= 2)
                      or (Semaphores.Login_Semaphore.Available /=0)
                      or (Semaphores.TC_Key_Val (User_Rec) /= 3) then
    Report.Failed ("Resource not properly released/assigned to task 3");
  end if;

  Task2.Logout;                  -- no outstanding request for released
                                 -- resource
                                 -- Tasks 1 and 2 hold no resources
                                 -- Task 3 holds a resource
                                 --   and is waiting for a call to Logout

  if (F940A00.Counter.Number /= 1)
                        or (Semaphores.Login_Semaphore.Available /=1) then
    Report.Failed ("Resource not properly released from task 2");
  end if;

  Task3.Logout;

                                 -- all resources have been returned
                                 -- all tasks have terminated or will soon

  if (F940A00.Counter.Number /=0)
                          or (Semaphores.Login_Semaphore.Available /=2) then
    Report.Failed ("Resource not properly released from task 3");
  end if;

  -- Ensure all tasks have terminated before calling Result
  while not (Task1'terminated and     
             Task2'terminated and
             Task3'terminated)     loop
    delay ImpDef.Minimum_Task_Switch;   
  end loop;

  Report.Result;

end C940A03;