Challenge 4 – Protected objects, tasks and race conditions

This package defines tasks to track friendly and enemy ships, based on a protected type defining a short list of nearby ships. A flag is set when the combat zone becomes crowded, in order to switch to a different combat mode.

Have a look at the following code and see if you can spot the errors. Once you think you’ve got them all, click on the “Go CodePeer” button to see how well you matched up to CodePeer’s comprehensive and rapid analysis of the same code.

Error line 76: “warning: unprotected access of Saturated_Combat_Zone via radar.track_ship’Task_Type_Body”

Here’s how CodePeer helps you coming to this conclusion: CodePeer is warning that global variable Saturated_Combat_Zone is accessed through task type Track_Ship without proper locking, which makes it possible to have a race condition when more than one task attempts to write to this global variable. Indeed, Add_Ship is called twice in Track_Ship on two different protected objects, Friends and Foes, which makes it possible that a first task of type Track_Ship calls it on Friends and a second task calls it on Foes, hence the race condition.

Error line 98: “warning: unprotected access of Saturated_Combat_Zone via radar.track_ship’Task_Type_Body”

Here’s how CodePeer helps you coming to this conclusion: This warning is similar to the one on line 76. Putting both warnings together, this also reveals a possible race condition between accesses to Saturated_Combat_Zone in Add_Ship and Remove_Ship.

Error line 100: “medium: range check might fail: requires (Num_Untracked_Ships – 1) >= 0”

Here’s how CodePeer helps you coming to this conclusion: CodePeer detects that Num_Untracked_Ship might be assigned a negative value at this point, which would violate the constraint that Num_Untracked_Ship is a Natural. Looking just 3 lines above, we see indeed that Num_Untracked_Ship might be null at this point, so that the subtraction on line 100 returns -1. The error is that the statements on lines 97 and 100 are in the wrong order.

Error line 115: “medium: validity check: Index might be uninitialized”

Here’s how CodePeer helps you coming to this conclusion: Index is not initialized on line 105, so it remains uninitialized if the loop terminates without finding a bigger ship, which would occur for example if no ships are currently tracked.

package Radar is

   type Friend_Or_Foe is (Friend, Foe, Unknown);
   type Class_Of_Ship is
     (Not_A_Ship, Coastal_Patrol, Fast_Attack_Craft, Corvette, Frigate,
      Destroyer, Cruiser, Pocket_Battleship, Battlecruiser, Helicopter_Carrier,
      Battleship, Dreadnought, Aircraft_Carrier, Supercarrier);
   type Kilometer is new Natural;

   --  Every ship detected by the radar is assigned a unique identifier that
   --  allows tracking it until it espaces the radar's scope.
   type Ship is record
      Quality   : Friend_Or_Foe := Unknown;
      Category  : Class_Of_Ship := Not_A_Ship;
      Distance  : Kilometer     := 0;
      Unique_ID : Natural       := 0;
   end record;

   function "=" (X, Y : Ship) return Boolean;

   type Ship_Array is array (Positive range <>) of Ship;

   --  Detect when too many ships are sailing in the combat zone, which makes
   --  it very likely to be hit by enemy fire or friendly fire. This triggers
   --  a different combat mode where the ship principally attempts to escape
   --  the crowded zone.
   Saturated_Combat_Zone : Boolean := False;

   --  Track ships closer than this distance
   Short_Distance : constant Kilometer := 20;

   --  Short list of nearest ships that should be dealt with higher priority,
   --  whether it is to engage combat for enemies or to agree on maneuvers
   --  for friends.
   protected type Short_List (Max_Tracked_Ships : Positive) is
      --  Add a ship when entering the short range
      procedure Add_Ship (E : Ship);
      --  Remove a ship when leaving the short range
      procedure Remove_Ship (E : Ship);
      --  Return the biggest ship in the short range
      function Biggest_Ship return Ship;
   private
      Num_Tracked_Ships   : Natural := 0;
      Num_Untracked_Ships : Natural := 0;
      --  Only tracked ships are included in Ships
      Ships               : Ship_Array (1 .. Max_Tracked_Ships);
   end Short_List;

   Friends : Short_List (50);  --  50 friendly ships tracked for maneuvers
   Foes    : Short_List (18);  --  18 enemy ships tracked (# of weapon systems)

   --  Track a ship entering and leaving the short range
   task type Track_Ship is
      entry New_Ship (E : Ship);
      entry Update_Position (Distance : Kilometer);
   end Track_Ship;

end Radar;

package body Radar is

   function "=" (X, Y : Ship) return Boolean is
   begin
      return X.Unique_ID = Y.Unique_ID;
   end "=";

   protected body Short_List is

      procedure Add_Ship (E : Ship) is
      begin
         if Num_Tracked_Ships < Max_Tracked_Ships then
            Ships (Num_Tracked_Ships) := E;
            Num_Tracked_Ships         := Num_Tracked_Ships + 1;
         else
            Num_Untracked_Ships       := Num_Untracked_Ships + 1;
            Saturated_Combat_Zone     := True;
         end if;
      end Add_Ship;

      procedure Remove_Ship (E : Ship) is
      begin
         for J in Ships'First .. Num_Tracked_Ships loop
            if Ships (J) = E then
               --  Ship E was found. First remove it.
               for K in J + 1 .. Num_Tracked_Ships loop
                  Ships (K - 1) := Ships (K);
               end loop;
               --  Then update the number of tracked ships and return.
               Num_Tracked_Ships := Num_Tracked_Ships - 1;
               return;
            end if;
         end loop;

         --  Ship E was not found, so it is an untracked ship.
         --  Update the number of untracked ships and possibly leave the mode
         --  where combat zone is saturated.
         if Num_Untracked_Ships = 0 then
            Saturated_Combat_Zone := False;
         end if;
         Num_Untracked_Ships := Num_Untracked_Ships - 1;
      end Remove_Ship;

      function Biggest_Ship return Ship is
         Current : Class_Of_Ship := Not_A_Ship;
         Index   : Integer;
      begin
         for J in Ships'First .. Num_Tracked_Ships loop
            if Current < Ships (J).Category then
               --  Found a bigger ship. Update Current and Index.
               Current := Ships (J).Category;
               Index   := J;
            end if;
         end loop;

         return Ships (Index);
      end Biggest_Ship;

   end Short_List;

   task body Track_Ship is
      Current : Ship;
   begin
      --  Define the ship being tracked.
      accept New_Ship (E : Ship)
      do
         Current := E;
      end New_Ship;

      loop
         --  Following a movement of the ship entering or leaving the short
         --  range, add or remove it from the corresponding short list.
         accept Update_Position (Distance : Kilometer)
         do
            Current.Distance := Distance;
            if Distance < Short_Distance then
               case Current.Quality is
                  when Friend =>
                     Friends.Add_Ship (Current);
                  when Foe =>
                     Foes.Add_Ship (Current);
                  when Unknown =>
                     null;
               end case;
            else
               case Current.Quality is
                  when Friend =>
                     Friends.Remove_Ship (Current);
                  when Foe =>
                     Foes.Remove_Ship (Current);
                  when Unknown =>
                     null;
               end case;
            end if;
         end;
      end loop;
   end Track_Ship;

end Radar;