CVS difference for ai12s/ai12-0064-2.txt

Differences between 1.15 and version 1.16
Log of other versions for file ai12s/ai12-0064-2.txt

--- ai12s/ai12-0064-2.txt	2017/04/21 05:43:52	1.15
+++ ai12s/ai12-0064-2.txt	2017/09/06 01:58:29	1.16
@@ -1,4 +1,4 @@
-!standard 9.5(17/3)                                 17-02-15    AI12-0064-2/10
+!standard 9.5(17/3)                                 17-09-015    AI12-0064-2/11
 !standard 9.5.1(8)
 !standard 9.5.1(9)
 !standard 9.5.1(10)
@@ -37,8 +37,53 @@
 
 !proposal
 
-[Summary of changes for June 2017 meeting:
+Add the aspect Nonblocking and the attribute Nonblocking to Ada. These allow
+specifying and querying the blocking status of a subprogram. If a subprogram
+is declared to be nonblocking, the Ada compiler will verify that it does not
+execute any potentially blocking operations (other than deadlocking
+operations).
+
+[Summary of changes for October 2017 meeting:
+
+Added some proposal wording, and put in the missing !wording.
+
+Changed "blocking restriction expression" to "nonblocking expression" as
+requested.
+
+Changed "nonblocking-static" expressions to only allow combining with
+"and" and "and then", as requested. Note that I didn't change the wording
+for the "poor man's inference" (as Tucker called it), as I couldn't find
+any simplification. I considered replacing "and" and "and then" with
+"boolean operator or short-circuit form" (which have to be only "and" or
+"and then" in this context), but this is longer and doesn't seem to add
+any readability/understandability. In any case, we have to allow conforming
+to parts of an expression, and that seems to need some description of the
+parts in question. (If we just said "conform to some part of the expression",
+that would seem to leave a lot to the imagination, or to figuring out the
+details of the rules.) [This wording can be near around line 620 in this AI;
+I'm not giving exact numbers as editing changes the line numbers frequently.]
+
+Changed the "assume-the-best" and "assume-the-worst" rules to apply to
+stand-alone generic specifications and generic bodies as well. Since
+calls to subprograms that allow blocking can occur in the elaboration
+code of generic packages and in the bodies of generic subprograms, we
+need to know when and how to make these checks as well. [This wording can
+be found at approximately lines 600-620 in this AI.]
+
+Minor: The nonblocking expression of a predefined operator of a composite
+type was "determined by" the expression of the type; I changed it to say
+it is "the same as" the expression of the type since that more clearly
+expresses the intent. (Else someone will ask "determined how"?).
+
+Note: We didn't discuss the Open Issue found near line 740; we need to decide
+how many Nonblocking aspects will be added to the Standard. I personally think
+we should write them all as aspects, since Global will have to be written that
+way, having both pragmas and aspects is ugly, and as such no Program Unit
+pragma Nonblocking is needed.]
 
+[Summary of changes for June 2017 meeting: (Note: I kept this for the benefit
+of people who were not at the Vienna meeting.)
+
 Applied the minor wording changes requested during meeting #56 (Pittsburgh).
 
 Added definition of nonblocking-static expressions, to reply to a comment from
@@ -93,7 +138,7 @@
 of generic units. Outside of any generic, it is required to be static so that
 we can enforce Legality Rules based on an unambiguous value. In order to
 follow the model of preconditions, the expression is given a name, the
-"blocking restriction expression". I changed as many uses as possible to use
+"nonblocking expression". I changed as many uses as possible to use
 this name; it makes more sense than talking about the "value of the
 Nonblocking aspect" when that might be a complex expression. (When Tucker
 reviewed the AI, he asked me to remove most of the remaining uses of "value",
@@ -119,6 +164,8 @@
 
 ---
 
+!wording
+
 [Editor's note: Individual rule changes scattered throughout the Standard
 follow this primary definition.]
 
@@ -129,25 +176,17 @@
    An expression is *nonblocking-static* if it is one of the following:
       * a static expression;
       * a Nonblocking attribute reference;
-      * a call to a predefined boolean logical operator and, or, xor, or not,
+      * a call to a predefined boolean logical operator /and/
         where each operand is nonblocking-static;
-      * a call to a predefined equality or ordering operator, where one operand
-        is a Nonblocking attribute reference, and the other is a static
-        expression;
-      * a short-circuit control form where both operands are
-        nonblocking-static;
-      * an if_expression where each condition is a static expression and
-        each dependent_expression is nonblocking-static;
-      * a case_expression where the selecting_expression is static and
-        each dependent_expression is nonblocking-static; or
+      * an /and then/ short-circuit control form where both operands
+        are nonblocking-static;
       * a parenthesized nonblocking-static expression. 
 
    [Editor's note: This wording is intended to parallel the definition of
-    predicate-static expression (from 3.2.4(15-22/3)). The membership
-    case doesn't make any sense here (T'Nonblocking in Boolean???).
-    The equality/ordering operators aren't very useful, but it seems strange
-    to leave them out. Conditional expressions have a different rule than
-    predicate-static.]
+    predicate-static expression (from 3.2.4(15-22/3)). However, we only
+    allow combining expressions with "and" or "and then", as this is the
+    only useful case. (Other combinations mismatch with the underlying
+    Legality Rules.)]
 
       AARM Reason: We define the term "nonblocking-static expression" so that
       nonblocking attribute references can be used to define the value of
@@ -162,12 +201,12 @@
    Nonblocking
 
        This aspect specifies the blocking restriction for the entity; it shall
-       be specified by an expression, called a *blocking restriction
-       expression*. If directly specified, the aspect_definition shall be a
+       be specified by an expression, called a *nonblocking expression*. If
+       directly specified, the aspect_definition shall be a
        nonblocking-static expression. The expected type for the expression is
        the predefined type Boolean. [Redundant: The aspect_definition can be
-       omitted from the specification of this aspect; in that case the blocking
-       restriction expression for the entity is the enumeration literal True.]
+       omitted from the specification of this aspect; in that case the
+       nonblocking expression for the entity is the enumeration literal True.]
 
          AARM Proof: 13.1.1 allows omitting the aspect expression for
          any aspect with type Boolean; we take advantage of that here.
@@ -179,9 +218,9 @@
 
          [Editor's 2nd note: One difference with preconditions is the we
          specify that the type is Boolean, not "any boolean type". We did
-         this because we have matching attributes, and having attributes
-         with a different type than the aspect is weird, while attributes
-         with "any boolean type" is weirder. ]
+         this because we have defined nonblocking attributes, and having
+         attributes with a different type than the aspect is weird, while
+         attributes with "any boolean type" is weirder. ]
 
        The Nonblocking aspect may be specified for all entities for
        which it is defined, except for protected operations and
@@ -193,7 +232,7 @@
        13.1(9.4/5) does not apply to aspect Nonblocking. This is the
        "unless otherwise specified" of that rule.]
 
-       When the blocking restriction expression is static for an entity,
+       When the nonblocking expression is static for an entity,
        the expression is evaluated to produce a static value for the aspect.
        When aspect Nonblocking is statically False for an entity, the entity
        might contain a potentially blocking operation; such an entity *allows
@@ -214,21 +253,21 @@
          that Program_Error is raised in a deadlock situation.
 
        For a generic instantiation and entities declared within such an
-       instance, the aspect is determined by the blocking restriction
+       instance, the aspect is determined by the nonblocking
        expression for the corresponding entity of the generic unit, with
        any Nonblocking attributes of the generic formal parameter replaced
        by the appropriate expression of the corresponding actual parameters.
        If the aspect is directly specified for an instance, the specified
-       expression shall be static and have the same value as the blocking
-       restriction expression of the instance (after replacement).
+       expression shall be static and have the same value as the nonblocking
+       expression of the instance (after replacement).
 
          AARM Reason: We want to allow confirming aspects for instances,
          but nothing else. The Legality Rules of the generic body were
-         checked assuming the blocking restriction expression of the
+         checked assuming the nonblocking expression of the
          generic unit, and if that is changed, the instance body might
          make calls that allow blocking in subprograms that are nonblocking.
 
-         AARM Ramification: If the blocking restriction expression of the
+         AARM Ramification: If the nonblocking expression of the
          instance is not static (if the instance is itself inside of a
          generic unit), then the Nonblocking aspect cannot be specified
          for the instance.
@@ -251,7 +290,7 @@
        to know that the instance is nonblocking without having to look up the
        definition of the generic unit and repeat any substitutions.]
 
-       For a (protected or task) entry, the blocking restriction expression is
+       For a (protected or task) entry, the nonblocking expression is
        the Boolean literal False.
 
          AARM Reason: An entry can be renamed as a procedure, so the value
@@ -263,10 +302,10 @@
          individual rules for these cases, but there were already many
          of them, and this solution avoids the need for extra rules.
 
-       For a predefined operator of an elementary type the blocking restriction
+       For a predefined operator of an elementary type the nonblocking 
        expression is the Boolean literal True. For a predefined operator of a
-       composite type, the blocking restriction expression of the operator is
-       determined by the blocking restriction expression for the type.
+       composite type, the nonblocking expression of the operator is
+       the same as the nonblocking expression for the type.
 
           AARM Reason: Predefined operators of elementary types can never
           include any potentially blocking operations, so we want them to
@@ -282,8 +321,8 @@
           to handle private types completed by elementary types, we need to
           have this rule apply to the operators, not the types.
 
-          AARM Ramification: It's not possible to specify the blocking
-          restriction expression of a predefined operator; if an operator
+          AARM Ramification: It's not possible to specify the nonblocking
+          expression of a predefined operator; if an operator
           is declared in order to do that, it is no longer predefined.
 
        [Redundant: For a full type declaration that has a partial view, the
@@ -303,21 +342,21 @@
           actual parameters of the instance is only necessary when the aspect
           is explicitly specified for the formal type.
 
-       Unless directly specified, for a derived type the blocking restriction
+       Unless directly specified, for a derived type the nonblocking 
        expression is that of the parent type.
 
           AARM Discussion: The expressions that can be specified for a derived
           type are limited by a Legality Rule, see below.
 
        Unless directly specified, for any other program unit, type, or formal
-       object, the blocking restriction expression of the entity is determined
-       by the blocking restriction expression for the innermost program unit
+       object, the nonblocking expression of the entity is determined
+       by the nonblocking expression for the innermost program unit
        enclosing the entity.
 
           [Editor's note: Formal objects are here since objects don't have
           the aspect in general, only in this specific case.]
 
-       If not specified for a library unit, the blocking restriction expression
+       If not specified for a library unit, the nonblocking expression
        is the Boolean literal True if the library unit is declared pure and is
        not a generic unit, and the Boolean literal False otherwise.
 
@@ -337,7 +376,7 @@
          use in aspect specifications, we don't want any evaluation, as it
          would happen at some freezing point.
 
-       S'Nonblocking represents the blocking restriction expression of S;
+       S'Nonblocking represents the nonblocking expression of S;
        evaluation of S'Nonblocking evaluates that expression.
 
        [Editor's note: All of these attributes are not allowed to be used
@@ -353,7 +392,7 @@
        Denotes whether package P is considered nonblocking; the type
        of this attribute is the predefined type Boolean.
 
-       P'Nonblocking represents the blocking restriction expression of P;
+       P'Nonblocking represents the nonblocking expression of P;
        evaluation of P'Nonblocking evaluates that expression.
 
    For a prefix S that denotes a subtype (including formal subtypes):
@@ -364,7 +403,7 @@
        type S are considered nonblocking; the type of this attribute is the
        predefined type Boolean.
 
-       S'Nonblocking represents the blocking restriction expression of S;
+       S'Nonblocking represents the nonblocking expression of S;
        evaluation of S'Nonblocking evaluates that expression.
 
    [Editor's note: The following is moved from 9.5.1, including the AARM notes
@@ -481,7 +520,7 @@
       blocking in the full view.
 
    Aspect Nonblocking shall be specified for a derived type only if it
-   fully conforms to the blocking restriction expression of the ancestor type
+   fully conforms to the nonblocking expression of the ancestor type
    or if it is specified to have the Boolean literal True.
 
       AARM Reason: Boolean-valued aspects have a similar rule (see 13.1.1),
@@ -520,8 +559,12 @@
    allows blocking.
 
       AARM Ramification: This applies to both record and array "=".
+
+      This check occurs when the equality operator is declared, so this rule
+      effectively makes the type illegal if the rule is violated.
+      End AARM Ramification.
 
-   In a generic instantiation (after replacement in the blocking restriction
+   In a generic instantiation (after replacement in the nonblocking 
    expressions by values of the actuals as described previously):
 
       * the actual subprogram corresponding to a nonblocking formal
@@ -558,6 +601,7 @@
       the body of an expression function might make a prohibited call.
 
     A program unit P declared inside of a generic unit but not in a generic body
+    or that is a generic specification not declared in a generic unit
     is considered nonblocking for the purposes of checking the restrictions on a
     nonblocking unit only if the value of its Nonblocking aspect is statically
     True. For the purposes of checks in P, a call to a subprogram is considered
@@ -570,16 +614,16 @@
       so that a generic specification declared inside of a generic body uses
       the following "assume-the-worst" rule.
 
-    A program unit P declared inside of a generic body is considered nonblocking
-    for the purposes of checking the restrictions on a nonblocking unit unless
-    the value of its Nonblocking aspect is statically False. For the purposes of
-    checks in P, a call to a subprogram is considered to allow blocking
-    unless:
+    A program unit P declared inside of a generic body or that is a generic body
+    is considered nonblocking for the purposes of checking the restrictions on a
+    nonblocking unit unless the value of its Nonblocking aspect is statically
+    False. For the purposes of checks in P, a call to a subprogram is considered
+    to allow blocking unless:
        * the value of its Nonblocking aspect is statically True, or
-       * its blocking restriction expression (that is, Nonblocking aspect)
-         conforms exactly to that of P, or conforms to some part of the blocking
-         restriction expression of P that is combined with the remainder of the
-         blocking restriction expression of P by one or more "and" or "and then"
+       * its nonblocking expression (that is, Nonblocking aspect)
+         conforms exactly to that of P, or conforms to some part of the
+         nonblocking expression of P that is combined with the remainder of the
+         nonblocking expression of P by one or more "and" or "and then"
          operations.
 
       AARM Ramification: That is, if the aspect of the program unit is specified
@@ -710,8 +754,8 @@
     package Ada.Command_Line
        with Preelaborate, Nonblocking is
 
-An alternative to make John happy would be to define a Nonblocking library
-unit pragma to use as an alternative to the aspect for library units:
+An alternative that would make John happy would be to define a Nonblocking
+library unit pragma to use as an alternative to the aspect for library units:
 
     package Ada.Command_Line is
        pragma Preelaborate(Command_Line);
@@ -720,14 +764,16 @@
 We didn't do this pending a full ARG discussion, since it would add even more
 wording to an already large AI, and many of us have a strong preference for
 aspects in all cases. It also would not extend well to other kinds of
-contracts (global, exceptions, etc.) where more is needed than just an on-off
-value.
+contracts (global, exceptions, etc.) where more is needed than just a
+present/absent value.
 
 (John was the major holdout in the past. Has he moderated his view with
 experience? Or has he retired yet? ;-)
 End Open issue.]
+
+[Lengthy Editor's note:
 
-[Editor's note: We intend that language-defined subprograms are nonblocking
+We intend that language-defined subprograms are nonblocking
 unless this Standard says otherwise. Specifically, 9.5.1(18) said (before we
 deleted it above):
 

Questions? Ask the ACAA Technical Agent