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;