Defining access to global data

Global-in and global-out annotations (AI12-0079-3) (see RM 6.1.2) allow the programmer to specify what global data a subprogram uses, in a manner that is similar to that by which subprogram parameters are specified. Specifying the "side effects" (i.e. effects other than via a parameter) of a subprogram makes it easier for static analysis tools to reason, and (especially when there are no side-effects) can be useful to the human reader as well. For example:

This should be fairly familiar to SPARK users. Since we are extending the language proper, we can use the reserved words in, out and in out rather than the SPARK 2014 terms Input, Output and In_Out. Note though that, unlike SPARK 2014, there is no inner => after each mode.

The Global'Class aspect can be specified for a dispatching subprogram, giving an upper bound on the set of global variables that any subprogram dispatched to may access.

For each mode there can be a list of global variables (comma-separated if more than one), the reserved word all for all global variables, or the reserved word synchronized for all synchronized variables (i.e. tasks, protected objects and atomic objects, the implication being that accesses to them are thread-safe). (Meaning of Global when there is no mode (AI12-0375) tweaks the syntax to use semicolons to separate the list of variables for each mode as in the examples above).

The intention is that although advanced users may impose stricter requirement on themselves, the typical user should have to specify few, if any, global aspects. Thus the global aspect for a library unit usually defaults to "Unspecified", i.e. read and write of an unspecified set of global variables (sounds a bit like Rumsfeld's "known unknowns"!), although to null for Pure library units, i.e. no read or write of any global variable. For other entities, the global aspect defaults to that of the enclosing library unit.

Besides covering any global variables accessed by the body of the subprogram, the global aspect should also cover those accessed by any preconditions, postconditions, predicates and type invariants. Global variables accessed by other subprograms that the subprogram calls should normally also be identified, though if the other subprogram is passed in as an access-to-subprogram parameter then it is up to the caller of the original subprogram to take account of the effects of whatever subprogram it passes in. If an access-to-variable value is created then presumably the variable that it designates is going to be written, and if an access-to-constant value is created then presumably the constant that it designates is going to be read, so these accesses should be identified too. Generic formal parameters do not need to be included in the global aspect, as the globals used by the actual parameters of an instantiation are automatically added to the globals used by each entity declared by the instance. However, the core language does not check accesses to objects reached via dereferences of access values (the expectation being that such checks are provided by implementation-defined mechanisms).

Optional Annex H, for High Integrity Systems, adds restriction No_Unspecified_Globals, disallowing the Global and Global'Class for a library-level entity from being set or defaulting to Unspecified, thereby forcing the specification of Global. It also adds the restriction No_Hidden_Indirect_Globals, requiring that any accesses to objects reached via dereferences of access values are identified. For example:

package P is
   type G is private;
   type Ref (Data : access T) is null record;
   Glob : G;
   ...
   function F (C : aliased in out Container;
                       Pos : Cursor) return Ref
      with Global => in Glob;
   ...
private
   type G is record
      Info : access T;
   end record;
end P;

package body P is
   ...
   function F (C : aliased in out Container;
                       Pos : Cursor) return Ref is
   begin
      return Ref'(Data => Glob.Info);
        -- Error!
        -- The above returns a writable reference to
        -- Glob.Info.all, but Glob is of mode in, and
        -- Glob.Info.all is reachable from Glob.
   end F;
   ...
end P;

Optional Annex H allows the global aspect to be specified for subtypes and certain generic formal parameters.

Optional Annex H also provides an extension for dealing with “handles”, for example the File_Type of Text_IO or the Generator of Discrete_Random. Hence, in:

the File parameter is of mode in as the parameter itself isn't modified, yet the state associated with the file is modified. This can now be indicated using an overriding global mode, thus:

Fixups for Global annotations (AI12-0380 ) provides finer grain control regarding the use of generic formal parameters and dispatching calls, in optional Annex H. See the preceding section, 2.3, “Defining Nonblocking” for details.

Control over dispatching calls can be very useful in cases such as stream attributes. For example:

type T is tagged private
   with Input => Stream_Input;
procedure Fill (X : out T'Class;
              Str : aliased in out Ada.Streams.Root_Stream_Type'Class)
   with Global => in Debug,
           Dispatching => (T'Input (X), Display (X), Read (Str));
.. -- That was the spec of Fill; the body is below
procedure Fill (X : out T'Class;
              Str : aliased in out Ada.Streams.Root_Stream_Type'Class) is
begin
   X := T'Input (Str'Access);
   if Debug then
      Display (X);
   end if;
end Fill;

Without the Dispatching aspect, Fill would have to allow blocking and be assumed to write to all global objects. With it in place, the compiler can examine the type of X and Str to determine the actual operations invoked to determine the blocking state and global objects accessed by a specific call on Fill.

Contracts for container operations (AI12-0112 ) then uses the global annotations mechanism to specify the Global aspect for the predefined Containers.

Default Global aspect for language-defined units (AI12-0302 ) then uses the global annotations mechanism to specify the Global aspect for the remainder of Ada's own units (that is, child units of packages Ada, System and Interfaces).

For most language-defined packages (that are not Pure) an explicit value of "in out synchronized" (i.e. read and write of the set of global variables that are tasks, protected objects, or atomic objects) is added.

But where some unknown, unsynchronised variable holds state (such as Current_Input or Current_Output for Text_IO) then only "in out all" can be stated. This would mean that two concurrent subprogram calls using either Current_Input or Current_Output would be considered to conflict.

2.4 Defining access to global data