Version 1.2 of ai12s/ai12-0374-1.txt

!standard 9.5(24/5) 20-04-29 AI12-0374-1/02
!standard 9.5(27/5)
!standard 9.5(36/5)
!standard 9.5(47/5)
!standard 9.5(49/5)
!standard 9.5(65/5)
!standard 9.5(68/5)
!standard 13.1.1(18.1/4)
!class Amendment 20-03-22
!status work item 20-03-22
!status received 20-03-22
!priority Medium
!difficulty Medium
!subject Fixes for Nonblocking

(1) Generic units that are declared Nonblocking use the "and" of all of the formal parameters as their nonblocking expression.

(2) Subprograms that make dispatching calls may define their Nonblocking aspects in terms of their own references and calls on potentially blocking operations, combined with the Nonblocking aspects of the particular dispatching operations they invoke on particular class-wide parameters or globals.

(3) The Nonblocking aspect may be specified for nonfirst subtypes, and referenced via the corresponding attribute. If not specified, the aspects are inherited from the subtype on which the subtype is based.

The Nonblocking aspect of a subprogram must account for any potentially blocking operations involved in evaluating assertion expressions (including preconditions, postconditions, predicates, and type invariants) that would apply to a call on that subprogram.

The Nonblocking aspect for a private type or a private extension must account for evaluation of assertion expressions that might occur as part of default initialization, finalization, adjustment if nonlimited, and conversion/membership in the case of a private extension.

(1) AI12-0079-3 has redesigned Global to be more automatic for generic declarations. Something similar should be done for Nonblocking for generic units.

(2) Stream attributes internally make dispatching calls on the stream read/write routines, which can be user written. In general for a subprogram that internally makes dispatching calls, we probably need a way to specify its Nonblocking aspect in terms of the Nonblocking aspects of the dispatching calls performed on a given classwide object, in combination with the nonblocking of the subprogram as a whole.

(3) A predicate expression can potentially block. However, there is currently no way to indicate that the predicate of a type has blocking behavior. This means that a nonblocking type used in a supposedly nonblocking subprogram can in fact block if the predicate blocks.

As part of a call on a subprogram, we might need to evaluate various assertion expressions in the form of preconditions, predicates, postconditions, and/or type invariants, and these might invoke a potentially blocking operation.

For a generic unit G, if the aspect Nonblocking is statically true for G (by inheritance or specification), then the nonblocking expression for G is the and of the nonblocking attribute for each formal parameter of G.

AARM Reason: This means that an instance of this generic will be nonblocking only if all of the formal parameters are nonblocking (see below). This is the most usable definition. If one wants a generic whose instantiations will always be nonblocking, Nonblocking can be specified on the formal parameters.

For a prefix X denoting an object of a class-wide type T'Class, the following attribute is defined:

X'Nonblocking(dispatching_operation_list)

X'Nonblocking(list) represents the AND of the Nonblocking aspect of the tagged type T1 identified by the tag of X, and the Nonblocking aspects of the dispatching operations of T1 corresponding to the specified dispatching operations of T (or all dispatching operations of T if the list is the reserved word ALL). If a /dispatching_/selector_name within the list denotes multiple dispatching operations of T, the Nonblocking aspects of all of the corresponding dispatching operations of T1 are ANDed together.

For a program unit, task entry, formal package, formal subprogram, formal object of an anonymous access-to-subprogram type, enumeration literal, and for a {sub}type (including a formal {sub}type), the following language-defined operational aspect is defined:

Unless directly specified, for a formal {sub}type, formal package, or formal subprogram, the Nonblocking aspect is that of the actual {sub}type, package, or subprogram.

Denotes whether default initialization, finalization, assignment, predefined operators, and (in the case of access-to-subprogram subtypes) a subprogram designated by a value of {sub}type S are considered nonblocking; the type of this attribute is the predefined type Boolean. S'Nonblocking represents the nonblocking expression of S; evaluation of S'Nonblocking evaluates that expression.

Denotes whether the {sub}type of X is considered nonblocking; the type of this attribute is the predefined type Boolean. X'Nonblocking represents the nonblocking expression of X; evaluation of X'Nonblocking evaluates that expression. [S'Nonblocking represents the nonblocking expression of S; evaluation of S'Nonblocking evaluates that expression.]

For a subtype for which aspect Nonblocking is True, any predicate expression that applies to the subtype shall only contain constructs that are allowed immediately within a nonblocking program unit.

Aspect Nonblocking shall be specified for {the first subtype of} a derived type only if it fully conforms to the nonblocking expression of the ancestor {sub}type or if it is specified to have the Boolean literal True. {Aspect Nonblocking shall be specified for a nonfirst subtype S only if it fully conforms to the nonblocking expression of the subtype identified in the subtype_indication defining S or if it is specified to have the Boolean literal True.}

for checking in P, default initialization, finalization, [or] assignment{, or conversion to} [of] a [composite] formal {sub}type F is considered to call subprograms that have the nonblocking aspect of F'Nonblocking, and this is checked for conformance against that of P as described above. [These operations of an elementary formal type are considered nonblocking, and thus require no checks.]

If an aspect of a derived type {(or its first subtype)} is inherited from an ancestor {(sub)}type and has the boolean value True, the inherited value shall not be overridden to have the value False for the derived type {(or its first subtype)}, unless otherwise specified in this International Standard. {If an aspect of a nonfirst subtype is inherited from the subtype in the subtype_indication that defines it, and has the value True, the inherited value shall not be overridden to have the value False for the nonfirst subtype, unless otherwise specified in this International Standard.}

(1) We make the setting of a generic unit to be Nonblocking (implicitly or explicitly) to be the trigger for the special rules. This provides the maximum functionality, as even a nonblocking generic can be instantiated with actuals that are blocking (in that case, the instance will allow blocking; that can be detected by declaring the instance nonblocking if that is required).

It does mean that making a generic so that any instance is always nonblocking is more difficult: each formal that has a nonblocking aspect will have to be declared with a Nonblocking aspect. This seems to be a rare case, however, we want the usual case to be easy.

If the generic unit allows blocking (implicitly or explicitly), the nonblocking of the formals do not matter. This is the default for library units, as any other setting would be very incompatible.

This definition has the pleasant effect of by default allowing the use of the formal entities within the generic unit regardless of their nonblocking state. The assume-the-worst rules only come into play when the default nonblocking expression is replaced by a more restrictive expression.

(2) For a subprogram that internally performs dispatching calls on an object of whose tag is determined at the call site, it is essentially impossible to describe the Nonblocking behavior independently of that caller-determined tag. Therefore, we propose to allow a subprogram to indicate what dispatching operations it performs on a given object known to the caller, and then have the caller determine what are the implications with respect to Nonblocking.

(3) In this AI we define 'Nonblocking as attributes on subtypes rather than types, and we allow specifying the corresponding aspects. The alternative of forcing the type Nonblocking aspect specifications to cover all possible subtypes that might ever be declared seemed quite limiting, as far as interesting predicates. It seems clear that some predicates may want to use a blocking operation. [Editor's note: This seems much less clear than it does for Global!! A blocking predicate is pretty weird.] Forcing the type declaration to worry about this seems painful.

function Seize return Boolean with Nonblocking => False, Global => synchronized in out Lock is begin Lock.Seize; -- Entry call. return True; end Seize;

function Release return Boolean with Nonblocking => False, Global => synchronized in out Lock is begin Lock.Release; -- Entry call. return True; end Release;

type Wild is range 0 .. 255 with Nonblocking, Global => null, Dynamic_Predicate => (if Wild > 200 then Seize else Release); -- Illegal by this AI.

procedure P with Nonblocking, Global => null is Local : Wild := 255; -- Seizes the global lock. Prior to this AI, -- would be legal since scalar -- types didn't block nor access globals. begin Local := 0; -- Releases the global lock. Also was legal. end P;

The alternative approach of enforcing the nonblocking rules when a predicate is evaluated doesn't work for generic formal types, where the details of any predicate that might apply are unknown.