Version 1.5 of ai12s/ai12-0079-3.txt
!standard 6.1.2(0) 20-03-12 AI12-0079-3/04
!class Amendment 19-10-05
!status Amendment 1-2012 20-03-11
!status ARG Approved 11-0-3 20-03-11
!status work item 19-10-05
!status received 19-10-05
!priority High
!difficulty Hard
!subject Global-in and global-out annotations
!summary
Annotations are provided to describe the use of global objects by subprograms,
entries, tasks, and protected units, with a default specifiable at the library
unit level. A new section in the Core of the Standard defines the Global and
Global'Class aspects. In Annex H, two restrictions are defined to enforce
stricter requirements on the completeness of the global aspects, along with
some additional capabilities for the global aspects to provide more precision
regarding use of generic formal parameters and dispatching calls.
!problem
Here is the original problem statement:
Ada 2012 added many kinds of assertions to Ada in order to increase the
ability of a programmer to specify contracts for types and subprograms.
These contracts are defined to be checked at runtime, but are intended
to be potentially checked (at least in part) statically.
However, without knowledge of side effects of functions used in the
aspects, a tool has to assume the worst about any user-defined
functions. For example, that the result of a function can change even
when called with the same operands. Other assumptions could cause
incorrect programs to be accepted as correct, and if the assumptions
were used to omit "proved" aspects, to cause erroneous execution. Both of
these results are unacceptable for a feature intended to improve the
correctness of programs.
The worst-case assumptions pretty much prevent any analysis unless the
bodies of any user-defined functions used in the aspects are available.
This is troublesome, as it prevents analysis of programs as they are
constructed. If the body is not available, no analysis is possible.
Moreover, analysis depending on a body requires creating implicit body
dependencies (if the body is changed, any analysis depending on the
properties of that body would have to be performed again).
Ideally, analysis at the initial compile-time of a unit would be
possible, as it is important to detect errors as soon as possible. More
information about function side effects is needed in the specification
of subprograms in order to accomplish that goal.
---
Additional challenges addressed in this version of the AI:
Simplify the proposal, at least in the core, so few if any Global
aspects need to be specified by the typical user. Provide a way for more
advanced users to impose on themselves stricter requirements should they
so choose, but minimize the burden on programmers who want to use the
new features of Ada 202X without worrying about Global specifications.
Allow more sophisticated implementations, like the SPARK tools, to do
additional analysis without requiring the user to specify explicitly all
of the Global effects. In so far as possible, achieve compatibility
with use of Global in existing SPARK code, so that no significant change
in syntax or semantics is required for existing SPARK code to make it
Ada 202X compatible.
!proposal
(See summary.)
!wording
Add the following section:
6.1.2 The Global and Global'Class Aspects
For a subprogram, an entry, a named access-to-subprogram type, a task
unit, a protected unit, or a library package or generic library package, the
following language-defined aspect may be specified with an
aspect_specification (see 13.1.1):
Global
The syntax for the aspect_definition used to define a Global
aspect is as follows:
global_aspect_definition ::=
NULL
| Unspecified
| global_group_designator
| global_mode global_designator
| (global_aspect_element{, global_aspect_element})
| extended_global_aspect_definition -- see H.7
global_aspect_element ::=
global_mode global_set
| extended_global_aspect_element --
global_mode ::=
basic_global_mode
| extended_global_mode --
| implementation_defined_mode
basic_global_mode ::= in | in out | out
global_set ::= global_designator {, global_designator}
global_designator ::= global_group_designator | global_name
global_group_designator ::= all | synchronized
global_name ::= /object_/name | /package_/name
The Global aspect identifies the set of variables (which, for
the purposes of this clause includes all constants with some
part being immutably limited, or of a controlled type, private
type, or private extension) that are global to a callable entity
or task body, and that are read or updated as part of the execution
of the callable entity or task body. if specified for a protected
unit, it refers to all of the protected operations of the protected
unit.
Constants of any type may also be mentioned in a Global
aspect. If not specified or otherwise defined below, the aspect
defaults to the Global aspect for the enclosing library unit if
the entity is declared at library level, and to Unspecified
otherwise. If not specified for a library unit, the aspect
defaults to Global => NULL for a library unit that is declared
Pure, and to Global => Unspecified otherwise.
For a dispatching subprogram, the following language-defined aspect may
be specified with an aspect_specification (see 13.1.1):
Global'Class
The syntax for the aspect_definition used to define a Global'Class
aspect is the same as that defined above for
global_aspect_definition. This aspect identifies an upper bound on
the set of variables global to a dispatching operation that can be
read or updated as a result of a dispatching call on the operation.
If not specified, the aspect defaults to the Global aspect for the
dispatching subprogram.
Name Resolution Rules
A global_name shall resolve to statically denote an object or a
package (including a limited view of a package).
Static Semantics
A global_aspect_definition defines the Global or Global'Class aspect of
some entity. The Global aspect identifies the sets of global variables
that can be read, written, or modified as a side effect of executing the
operation(s) associated with the entity. The Global'Class aspect
associated with a dispatching operation of type T represents a
restriction on the Global aspect on a corresponding operation of any
descendant of type T.
The Global aspect for a callable entity defines the global variables
that might be referenced as part of a call on the entity, including any
assertion expressions that might be evaluated as part of the call,
including preconditions, postconditions, predicates, and type
invariants.
The Global aspect for an access-to-subprogram object (or subtype)
identifies the global variables that might be referenced when calling
via the object (or any object of that subtype) including assertion
expressions that apply.
For a predefined operator of an elementary type, or the function
representing an enumeration literal, the Global aspect is NULL. For a
predefined operator of a composite type, the Global aspect of the
operator defaults to that of the enclosing library unit (unless a Global
aspect is specified for the type -- see H.7).
The following is defined in terms of operations; the rules apply to all
of the above kinds of entities.
The global variables associated with any global_mode can be read as a
side effect of an operation. The IN OUT and OUT global_modes together
identify the set of global variables that can be updated as a side
effect of an operation. Creating an access-to-variable value that
designates an object is considered an update of the designated object,
and creating an access-to-constant value that designates an object is
considered a read of the designated object.
An implementation-defined global_mode may be specified, which limits the
use of the global objects to which it applies according to an
implementation-defined rule.
The overall set of objects associated with each global_mode includes all
objects identified for the mode in the global_aspect_definition.
A global_set identifies a global variable set as follows:
* ALL identifies the set of all global variables;
* SYNCHRONIZED identifies the set of all synchronized variables (see 9.10),
as well as variables of a composite type all of whose
non-discriminant subcomponents are synchronized;
* global_name{, global_name} identifies the union of the sets of
variables identified by the global_names in the list, for the
following forms of global_name:
+ /object_/name that identifies the specified global variable
(or constant);
+ /package_/name identifies the set of all variables declared in the
private part or body of the package, or anywhere within a private
descendant of the package.
Legality Rules
Within a global_aspect_definition, a given global_mode shall be
specified at most once. Similarly, within a global_aspect_definition, a
given entity shall be named at most once by a global_name.
If an entity (other than a library package or generic library package)
has a Global aspect other than Unspecified or IN OUT ALL, then the
execution of the associated operation(s) shall read only those variables
global to the entity that are within the global variable set associated
with the IN, IN OUT, or OUT modes, and the operation(s) shall update
only those variables global to the entity that are within the global
variable set associated with either the IN OUT or OUT global_modes. In
the absence of the No_Hidden_Indirect_Globals restriction (see H.4),
this ignores objects reached via a dereference of an access value. The
above rule includes any possible Global effects of calls occurring
during the execution of the operation, except for the following excluded
calls:
* calls to formal subprograms;
* calls associated with operations on formal subtypes;
* calls through formal objects of an access-to-subprogram type;
* calls through access-to-subprogram parameters;
* calls on operations with Global aspect Unspecified.
The possible Global effects of these excluded calls (other than those
that are Unspecified) are taken into account by the caller of the
original operation, by presuming they occur at least once during its
execution. For calls that are not excluded, the possible Global effects
of the call are those permitted by the Global aspect of the associated
entity, or by its Global'Class aspect if a dispatching call.
AARM Ramification: For a predefined equality operator of a composite
type, the possible Global effects includes those of the equality
operations invoked as part of the evaluation of the operator (which
might not be predefined and thus might have a different Global
specification than the component types).
If an implementation-defined global_mode applies to a given set of
objects, an implementation-defined rule determines what sort of
references to them are permitted.
For a subprogram that is a dispatching operation of a tagged type T,
each mode of its Global aspect shall identify a subset of the variables
identified by the corresponding mode, or by the IN OUT mode, of the
Global'Class aspect of a corresponding dispatching subprogram of any
ancestor of T, unless the aspect of that ancestor is Unspecified.
Implementation Permissions
Implementations need not require that references to a constant object
that are considered variables in the above rules, be accounted for by
the Global or Global'Class aspect, if the implementation can determine
that the constant object is immutable.
Implementations may perform additional checks on calls to operations
with an Unspecified Global aspect to ensure that they do not violate any
limitations associated with the point of call.
AARM Discussion: In this sense, Global => Unspecified is not permission
to violate the caller's Global restrictions. It is rather that the
implementor of the subprogram is presuming other means are being
used to ensure safety. Note the No_Unspecified_Globals Restriction
(H.4), which prevents the use of Unspecified with the Global aspect in a
given partition.
Implementations may extend the syntax or semantics of the Global aspect
in an implementation-defined manner.
AARM Reason: This is intended to allow preexisting usages from SPARK
2014 to remain acceptable in conforming implementations, as well as to
provide flexibility for future enhancements. Note the word “extend” in
this permission; we expect that any aspect usage that conforms with
the (other) rules of this clause will be accepted by any full Ada
implementation, regardless of any implementation-defined extensions.
NOTES
7 For an example of the use of these aspects and attributes, see the
Vector container definition in A.18.2.
----
Add after H.4 (23):
No_Unspecified_Globals
No library-level entity shall have a Global aspect of Unspecified,
either explicitly or by default. No library-level entity shall
have a Global'Class aspect of Unspecified, explicitly or by
default, if it is used as part of a dispatching call.
AARM Ramification: Global'Class need not be specified on
an operation if there are no dispatching calls to the
operation, or if all of the dispatching calls are covered
by dispatching_operation_specifiers for operations
with such calls (see H.7).
No_Hidden_Indirect_Globals
When within a context where the applicable Global aspect is neither
Unspecified nor IN OUT ALL, any execution within such a context
does neither of the following:
* Update a variable that is reachable via a sequence of zero or
more dereferences of access-to-object values from a formal
parameter of mode IN (after any OVERRIDING -- see H.7), or from
a global that is not within the applicable global variable set,
or has mode IN;
* Read a variable that is updatable via a sequence of zero or
more dereferences of access-to-object values from a global that
is not within the applicable global variable set.
AARM Ramification: The above two rules specify that any
indirect references are covered by the Global or formal
parameter modes that apply, and are not subject to
alternative paths of access (i.e. aliasing) that could
result in conflicts.
For the purposes of the above rules, if an applicable global
variable set includes a package name, and the collection of some
pool-specific access type (see 7.6.1) is implicitly declared in a
part of the declarative region of the package included within the
global variable set, then all objects allocated from that
collection are considered included within the global variable set.
The consequences of violating the No_Hidden_Indirect_Globals
restriction is implementation-defined. Any aspects or other means
for identifying such violations prior to or during execution are
implementation-defined.
AARM Discussion: We do not make violations automatically
erroneous, because if the implementation chooses to never fully
trust it, there is nothing erroneous that can happen. If an
implementation chooses to trust the restriction, and performs
some optimization as a result of the restriction, the
implementation would define such a violation as erroneous. Such
an implementation might also endeavor to detect most violations,
perhaps by providing additional aspects, thereby reducing the
situations which result in erroneous execution. Implementations
might detect some but not all violations of the restrictions.
Implementations that completely ignore the restriction should
treat the restriction as an unsupported capability of Annex H.
Add the following section:
H.7 Extensions to Global and Global'Class Aspects
In addition to the entities specified in 6.1.2, the Global aspect may be
specified for a subtype (including a formal subtype), formal package,
formal subprogram, and formal object of an anonymous
access-to-subprogram type.
The following additional syntax is provided for specifying Global and
Global'Class aspects, to more precisely describe the use of generic
formal parameters and dispatching calls within the execution of an
operation:
extended_global_aspect_definition ::=
use formal_parameter_designator
| do dispatching_operator_specifier
extended_global_aspect_element ::=
use formal_parameter_set
| do dispatching_operation_set
extended_global_mode ::=
overriding basic_global_mode
formal_parameter_designator ::=
formal_group_designator
| formal_parameter_name
formal_parameter_set ::=
formal_group_designator
| formal_parameter_name{, formal_parameter_name}
formal_group_designator ::= null | all
formal_parameter_name ::=
/formal_/subtype_mark
| /formal_subprogram_/name
| /formal_access_to_subprogram_object_/name
dispatching_operation_set ::=
dispatching_operation_specifier{, dispatching_operation_specifier}
dispatching_operation_specifier ::=
/dispatching_operation_/name (/object_/name)
Name Resolution Rules
A formal_parameter_name shall resolve to statically denote a formal
subtype, a formal subprogram, or a formal object of an anonymous
access-to-subprogram type.
The /object_/name that is associated with an OVERRIDING mode shall
resolve to statically denote a formal object, or a formal parameter of
the associated entity.
The /object_/name of a dispatching_operation_specifier shall resolve to
statically denote an object (including possibly a formal parameter) of a
tagged class-wide type T'Class; the /dispatching_operation_/name of the
dispatching_operation_specifier shall resolve to statically denote a
dispatching operation associated with T.
Static Semantics
The presence of the reserved word OVERRIDING in a global mode
indicates that the specification is overriding the mode of a formal
parameter with another mode to reflect the overall effect of an
invocation of the callable entity on the state associated with the
corresponding actual parameter.
The extended_global_aspect_definition and extended_global_aspect_element
can be used to define as part of the Global aspect the *formal parameter
set* and the *dispatching operation set* used within an operation. The
formal parameter set is identified by a set of formal parameter names
after the reserved word USE. Alternatively, the reserved word NULL may
be used to indicate none of the generic formal parameters, or ALL to
indicate all of the generic formal parameters, of any enclosing generic
unit (or visible formal package) might be used within the execution of
the operation. If there is no formal parameter set specified for an
operation declared within a generic unit, it defaults to USE ALL.
The dispatching operation set is identified by a set of
dispatching_operation_specifiers after the reserved word DO. It
indicates that the Global effects of dispatching calls that match one
of the specifiers need not be accounted for by other elements of the
Global aspect, but are instead to be accounted for by the invoker of the
operation. A dispatching call matches a
dispatching_operation_specifier if the prefix of the call statically
denotes the same operation(s) as that of the
dispatching_operation_specifier, and at least one of the objects
controlling the call is denoted by a name that statically denotes the
same object as that denoted by the /object_/name of the
dispatching_operation_specifier. In the absence of any
dispatching_operation_specifiers, all dispatching calls within the
operation are presumed to have the effects determined by the set of
Global'Class aspects that apply to the invoked dispatching operation.
The Global aspect for a subtype identifies the global variables that
might be referenced during default initialization, adjustment as part of
assignment, finalization of an object of the subtype, or conversion to
the subtype, including the evaluation of any assertion expressions that
apply. If not specified for the first subtype of a derived type, the
aspect defaults to that of the ancestor subtype; if not specified for a
nonderived first subtype the aspect defaults to that of the enclosing
library unit. If not specified for a nonfirst subtype S, the Global
aspect defaults to that of the subtype identified in the
subtype_indication defining S.
The Global'Class aspect may be specified for the first subtype of a
tagged type T, indicating an upper bound on the Global aspect of any
descendant of T. If not specified, it defaults to Unspecified.
Legality Rules
For a tagged subtype T, each mode of its Global aspect shall identify a
subset of the variables identified by the corresponding mode, or by the
in out mode, of the Global'Class aspect of the first subtype of any
ancestor of T.
If the formal parameter set is anything but ALL in the Global aspect for
an operation declared within a generic unit, then the only generic
formal subtypes that may be used, the only formal subprograms that may
be called, and the only formal objects of an anonymous
access-to-subprogram type that may be dereferenced as part of a call or
passed as the actual for an access parameter, are those included in the
formal parameter set.
Any dispatching call occurring within the operation that does not match
a dispatching_operation_specifier is checked using the Global'Class
aspect(s) applicable to the dispatching operation; if there is a match,
there is no checking against other elements of the Global aspect(s)
applicable at the point of call.
!discussion
Global annotations are critical to being able to perform any sort of modular
static analysis.
The intent is that all of the global IN, IN OUT, OUT, USE, and DO annotations
proposed can be statically checked.
This new version of this AI incorporates changes defined by AI12-0240-6
(overriding), AI12-0303-1 (mutable constants), AI12-0310-1 (package
private part), and AI12-0334-2 (subtypes and predicates).
In this new version, we have dropped the notion of a Global attribute
(i.e. X'Global) in favor of somewhat different defaults, and have
incorporated more precise forms of Global aspect elements (USE ... and
DO ...) into the High-Integrity Annex H where they need not be supported
in initial implementations of the new standard. We have also added two
restrictions in H.4, one to enable a user to disallow use of the new Unspecified
value for the Global aspect for any library-level entities, and one
to enable a user to indicate that all objects reached via access values
are covered by the formal parameter or Global aspect modes.
We allow Global specifications on packages or generic packages only if
they are library units, analogous to the same limitation of where Pure
can be specified, to establish a default for library-level entities.
More details on the new defaults are detailed below. The overall goal
is that a programmer who specifies nothing gets something reasonable.
Another goal is that existing SPARK programs use of Global should be
acceptable largely as is, except for the slight change in syntax to use
reserved words "IN" and "OUT" rather than the non-reserved "Input",
"In_Out", and "Output" currently used in the SPARK Global aspect. In
any case, a compiler could accept both the old syntax and the new
syntax, as they are unambiguously distinguishable at compile time.
The most critical new "default" in this new version is that entities not
within a declared-pure library unit, or not at library-level, have
Unspecified as their default Global aspect. This effectively implies
that the caller may assume the best, but no checking is necessarily
being performed at the point of call (though implementations are
permitted to effectively inline the call to do additional checks). We
provide a restriction of No_Unspecified_Globals in Annex H to allow a
user to disallow any library-level entities with Global => Unspecified
within a partition. Note that for non library-level entities, even if
their own Global aspect is Unspecified, they must still honor any Global
aspects of lexically enclosing entities, if these entities have an
explicit or implicit Global aspect other than Unspecified. For example,
a nested subprogram with Global => Unspecified still cannot violate the
Global aspect of its enclosing subprogram, so if the enclosing
subprogram specifies Global => SYNCHRONIZED, the nested subprogram
cannot reference a variable that is global to its enclosing subprogram
unless it is synchronized. It may reference variables local to its
enclosing subprogram with no restrictions.
The other critical new "default" is that entities declared within a
generic unit are presumed to make use of all generic formal parameters
associated with any enclosing generic unit, while not worrying about any
of the possible Global effects of that usage in their Global aspect.
These additional effects are handled at the point of instantiation,
rather than at the point of definition of the generic, much in the same
way that "purity" of an instantiation is determined by a combination of
the "purity" of the generic and the purity of the actual parameters to
the generic. In annex H, we provide ways to specify upper bounds on the
effects of generic formal parameters, and we provide an ability to limit
which generic formal parameters are actually used within an entity
defined within a generic unit (USE formal_parameter_name, ...). This
allows us to say that all entities declared at library level within a
declared-pure library unit default to Global => null, even if they are
within a generic unit, because the USE ALL is implicit for such
entities.
We have also included in Annex H an ability to specify that certain
dispatching calls might be performed as part of the execution of an entity,
allowing the invoker to more precisely deal with the possible effects
of such a call, rather than the entity itself having to fall back
on the Global'Class effects, which are likely to be very pessimistic,
if specified at all.
Some overall notes on the above:
This version of this AI was based on work done by Tuck and Claire to
reach some kind of simpler consensus position on Global. Probably the
biggest change that came from that work was the introduction of the
notion of Global => Unspecified to better match existing SPARK usage
where few if any Global specifications are required. We have coupled
that with a restriction No_Unspecified_Globals to accommodate those
users who want to impose on themselves a requirement to specify Global,
explicitly or implicitly, at least on all library-level entities.
A related change was to move concerns about use of generic formals to
the point of instantiation, so operations in a "pure" generic unit can
be (implicitly or explicitly) simply "Global => null".
The additions relative to the consensus report are relatively few. We
have held on to a way to establish an overall default, but we now limit
it to a library unit as a whole, as that is the level at which Pure can
be declared, and the default only applies to library-level elements, not
to any non library-level declarations. Non library-level entities
always default to Global => Unspecified, but we believe that that is not
a significant loss in functionality, as these nested entities must still
abide by any Global aspect of their enclosing library-level entity.
As proposed in our consensus document, we have allowed all dereferences
of access values to be ignored in the Global aspect. However in this AI
we allow the user to specify a restriction stating that in fact all such
dereferences are accounted for by Globals or parameters. We do not
specify how that claim should be enforced. Implementations have to
define how they deal with violations of the No_Hidden_Indirect_Globals
restriction; however, ignoring it completely means the capability is not
supported, and should be identified by the implementation as such.
We have eliminated the need for a Global attribute (X'Global) and moved
all functionality that depended on that into Annex H. We have ensured
that the functionality in the Annex is optional in the sense that it
only adds precision; it doesn't provide critical functionality for typical
use. Certain of the language-defined packages (such as those related
to streaming) might use these features to describe their effects
more precisely, but implementations that do not support these Annex H
features can choose how to reflect the Global effects of these
language-defined packages in a way that is appropriate to typical usage
patterns.
!example
For an example of the use of these aspects and attributes, see the
Vector container definition in A.18.2 (of draft 25 or later).
!ASIS
New functions will be needed. Details still to be determined.
!ACATS test
ACATS tests should be created to test that the new annotations are
correctly enforced.
!appendix
From: Tucker Taft
Sent: Sunday, February 9, 2020 2:18 PM
Here is a modest reformulation of the Global aspect as defined by AI12-0079-2.
The main change is to remove all access-type checking from the core, and add a
restriction called "No_Hidden_Indirect_Globals" to H.4 which a user can
specify to indicate that in fact all references via a sequence of access value
dereferences are actually covered by Global or formal parameter modes that
apply to the starting point of the sequence. Implementations must define the
consequences of violating the restriction -- such violations could be
erroneous, or they could be ignored, or the implementation could in fact
detect the violations at compile time or run time, probably by relying on
additional aspect specifications and/or run-time checks.
Comments, questions, fixes, etc. welcome. Hopefully this will be a topic at
the upcoming ARG phone meeting in March.
[This is version /01 of the AI - Editor.]
****************************************************************
From: Richard Wai
Sent: Sunday, February 9, 2020 3:38 PM
I think "No_Hidden_Indirect_Globals" is an elegant way to bring global
contracts into Ada, without being too ambitious or onerous with the
peculiarities of indirection.
However, I'm a little uncomfortable with a restriction being defined such that
the implementation may "ignore" violations.
I think it would be safer if _any_ language defined restriction that is
optionally implemented (this being first such restriction) caused any
non-supporting implementation to reject the compilation if the unsupported
restriction appears. This way the user is fully aware that the restriction is
not supported, and if they are ok with that lack of support, can remove the
restriction, or use some kind of implementation-specified override (i.e.
command-line switches). I think this agrees with higher-level Ada design
goals, specifically that a given program should not become less safe simply
by using a different (conformant) implementation. The only real trouble this
kind of requirement would cause would be a minor inconvenience at
compile-time. It seems very un Ada-like to worry about inconveniencing the
user during compilation if doing so significantly improves safety and
reliability. Implementing this requirement is almost certainly trivial.
I'd propose something like this, following paragraph to 13.12, Implementation
Permissions (after 9.2/1):
[Some language-defined restrictions (not including those defined in the
Specialized Needs Annexes), are deemed to be optionally implemented. Support
for optionally implemented language-defined restrictions may be omitted from
an implementation. If an implementation omits an optionally implemented
restriction, it shall reject any compilation containing any of the optionally
implemented restrictions that are not implemented.]
With the above general requirements of all restrictions, I feel
"No_Hidden_Indirect_Globals" should then be more explicitly "all or nothing".
If the implementation implements the restriction, then it must promise to
detect violations, either at compile time or at run-time. If the
implementation decides to not implement the restriction, then as per above,
it should reject the compilation outright.
Finally, I think No_Hidden_Indirect_Globals then should be more specific
about what runtime exception(s) could be expected if the implantation choses
to use runtime checking, as this could otherwise impact portability.
With all the above, there will be no surprises, or worse, a false sense of
security, if a user applies No_Hidden_Indirect_Globals.
****************************************************************
From: Tucker Taft
Sent: Sunday, February 9, 2020 4:36 PM
Thanks for your comments. I am a bit on the fence here. One reason to use
the restriction is to indicate that the program was written to conform to
this model, and that can be useful independent of whether the restriction
is actually enforced. To some extent assertions serve the same purpose when
the Assertion_Policy is Ignore. Perhaps we could have a way of saying that
the program obeys the restrictions, while acknowledging that they might not be
checked (equivalent of Assertion_Policy of Ignore). The presumption is that
there might be another kind of tool, other than the compiler, that helps to
enforce the restriction. This is how certain other SPARK annotations work in
general. The compiler may completely ignore them, leaving therm for the
"gnat-prove" tool to enforce.
Note that already everything in a specialized-needs annex is "optional" so it
would be a bit weird to make something doubly optional.
The fact that the consequences of violations are "implementation defined"
means that the compiler must come with documentation that indicates how the
restriction is enforced, so it becomes a quality-of-implementation issue.
I am also very reluctant to try to specify what the consequences should be at
this point, given that specifying them could add significant complexity to the
standard, and probably not exactly match what any real implementation will do
in the near term. I would rather get this restriction out there, and then at
some later point think about standardizing the consequences. My guess is that
over time tools will get better and better at detecting violations, and trying
to anticipate now what they will do or should do is a waste of energy. Having
an all or nothing situation seems like a bad approach. I would be happy to
see gradually improving support for the restriction.
****************************************************************
From: Tucker Taft
Sent: Sunday, February 9, 2020 4:42 PM
Note that this is somewhat like the situation now with the No_Exceptions
restriction, per H.4(25):
"If a pragma Restrictions(No_Exceptions) is specified, the implementation
shall document the effects of all constructs where language-defined checks
are still performed automatically (for example, an overflow check performed
by the processor)."
The documentation could say that all hell breaks loose if an exception
actually gets raised. Or it could give some more reasonable behavior.
Since we are requiring implementations to document how they support this newly
proposed restriction, a user can decide whether they find it helpful or harmful
to specify the restriction.
****************************************************************
From: Jean-Pierre Rosen
Sent: Monday, February 10, 2020 2:21 AM
> Note that already everything in a specialized-needs annex is "optional"
> so it would be a bit weird to make something doubly optional.
Not really. The annex as a whole is optional, but if you claim conformance,
then a number of things are required.
****************************************************************
From: Tucker Taft
Sent: Monday, February 10, 2020 9:53 AM
But there is also the notion of partial support of annex features, per
1.1.3(17):
"... However, it shall not provide any aspect, attribute, library unit, or
pragma having the same name as an aspect, attribute, library unit, or pragma
(respectively) specified in a Specialized Needs Annex unless the provided
construct is either as specified in the Specialized Needs Annex or is more
limited in capability than that required by the Annex. A program that attempts
to use an unsupported capability of an Annex shall either be identified by the
implementation before run time or shall raise an exception at run time. "
So "limited capability" support of an annex restriction is already fine.
****************************************************************
From: Jean-Pierre Rosen
Sent: Monday, February 10, 2020 10:11 AM
This paragraph says that if you do not claim support to an annex, but just to
the core language, you are not allowed to provide an incompatible version of
something provided in the annex.
You cannot claim conformance to an annex and "pick and choose" any feature
from the annex (which you seemed to imply by saying that "everything in a
specialized-needs annex is "optional" "). If you don't claim conformance, of
course, you can do anything you please, except being incompatible.
****************************************************************
From: Richard Wai
Sent: Monday, February 10, 2020 10:11 AM
> Thanks for your comments. I am a bit on the fence here. One reason to
> use the restriction is to indicate that the program was written to conform
> to this model, and that can be useful independent of whether the restriction
> is actually enforced. To some extent assertions serve the same purpose
> when the Assertion_Policy is Ignore.
My reasoning here was that Restriction pragmas, being configuration pragmas,
are much heavier, but also less "visible" to the programmer than the
scope-based Assertion_Policy pragma, so they aren’t really in the same
category. My concern being that one doesn't write pragma Assertion_Policy
(Check) and then have the compiler decide by itself to just say "nah, I'll
ignore it anyways". So I don't really see the comparison here, since
Assertion_Policy Ignore is just a default, but if the user specifies Check,
then the compiler cannot optionally ignore it.
> Perhaps we could have a way of saying that the program obeys the
> restrictions, while acknowledging that they might
> not be checked (equivalent of Assertion_Policy of Ignore). The
> presumption is that there might be another kind of
> tool, other than the compiler, that helps to enforce the restriction.
> This is how certain other SPARK annotations work
> in general. The compiler may completely ignore them, leaving therm
> for the "gnat-prove" tool to enforce.
This was my reasoning for implementation-specified methods of "overriding"
the lack of checking where the unimplemented restriction exists.
> Note that already everything in a specialized-needs annex is
> "optional" so it would be a bit weird to make something
> doubly optional.
Indeed, and I made note of that in the additional RM paragraph I have. My
reasoning here is not only that Special Needs Annexes are optional, but the
configuration pragmas (specifically Restriction pragmas) defined within them
are very specific to those Annexes, so users of such Restrictions are
expecting the Annex to be implemented.
****************************************************************
From: Richard Wai
Sent: Monday, February 10, 2020 10:41 AM
> But there is also the notion of partial support of annex features, per
> 1.1.3(17):
>
> "... However, it shall not provide any aspect, attribute, library
> unit, or pragma having the same name as an aspect, attribute, library
> unit, or pragma
> (respectively) specified in a Specialized Needs Annex unless the
> provided construct is either as specified in the Specialized Needs
> Annex or is more limited in capability than that required by the
> Annex. A program that attempts to use an unsupported capability of an
> Annex shall either be identified by the implementation before run time
> or shall raise an exception at run time. "
That last part of 1.1.3(17) is interestingly essentially what I was proposing.
The Annexes are optional, but if the use tries to use an unsupported
capability, the compilation fails or there is an exception at run-time. My
original suggestion being exactly that - language defined Restrictions that
are "optional" should nevertheless cause the compiler to "identify" any
(unsupported) use before run time, or else raise an exception.
In the case of SPARK, if the tools could prove the Global aspects, it seems to
me that it would satisfy the restriction, and users of SPARK should then be
justified to remove the restriction if they are using a compiler that doesn't
support that Restriction, or else use the compiler documented overrides.
****************************************************************
From: Tucker Taft
Sent: Monday, February 10, 2020 11:03 AM
I guess I would agree that if the restriction is completely ignored then it
should be rejected. But if it is even supported in a very limited way, it
serves a purpose. And in any case, expressing the intent to readers of the
program is always an important benefit to specifying such a restriction.
****************************************************************
From: Randy Brukardt
Sent: Monday, February 10, 2020 8:27 PM
...
> I think "No_Hidden_Indirect_Globals" is an elegant way to bring global
> contracts into Ada, without being too ambitious or onerous with the
> peculiarities of indirection.
I agree.
> However, I'm a little uncomfortable with a restriction being defined
> such that the implementation may "ignore" violations.
Me too. But in a different way than Richard.
Your reason for allowing "ignore the restriction" is that the compiler doesn't
take any advantage of the restriction. But the Legality Rules associated with
parallel checking are "taking advantage of the restriction".
More specifically, if one is desiring to get useful parallel usage checking,
it's required to have access types included in the Global specifications.
Such a user would use the No_Hidden_Indirect_Globals restriction (and possibly
the "No_Unspecified_Globals" restriction as well, depending on the compiler
implementation). In such a case, completely ignoring the restriction is wrong.
Even a bad (but simple) implementation (for instance, rejecting any dereference
outside of "all" or "unspecified") would be preferable to ignoring it.
I think it is OK to say that all code that violates the restriction is
erroneous (thus giving an incentive to find ways to eliminate that, but still
allowing the lazy implementer to do nothing), but to say it is "ignored" sends
the wrong message.
****************************************************************
From: Randy Brukardt
Sent: Monday, February 10, 2020 8:35 PM
...
> You cannot claim conformance to an annex and "pick and choose" any
> feature from the annex (which you seemed to imply by saying that
> "everything in a specialized-needs annex is "optional" "). If you
> don't claim conformance, of course, you can do anything you please,
> except being incompatible.
This is a very important point. Stuff in an Annex is only "optional" if one
doesn't support the Annex or if there is an explicit statement that it is
optional.
You can, for instance, claim support for Annex D and still not support
Priority_Specific_Dispatching, because D.2.1(19/2) says it doesn't have to
be supported on incompatible targets. On the other hand, claiming support for
Annex D and not supporting the EDF policy is not allowed (there's no rule
allowing that policy to be optional). [I note that since we were told that no
one has supported that policy, that therefore no compiler has ever supported
Annex D for Ada 2005 or later, despite vendor claims to the contrary. I'm
surprised that no one has ever tried to get the ARG to fix this...]
As I noted before, this restriction is integral to having useful parallelism
checking within Ada, so it seems rather important that some sort of support is
mandated. It's fine to leave the details to the implementation, however.
****************************************************************
From: Tucker Taft
Sent: Monday, February 10, 2020 10:47 PM
> ...
>
> I think it is OK to say that all code that violates the restriction is
> erroneous (thus giving an incentive to find ways to eliminate that,
> but still allowing the lazy implementer to do nothing), but to say it
> is "ignored" sends the wrong message.
Another way to do this is to say that if the parallel Conflict_Check_Policy is
anything other than No_Parallel_Conflict_Checks, then any execution in a
parallel context that violates the No_Hidden_Indirect_Globals is erroneous.
Analogous rules would apply for tasking conflict checks. We should probably
also move the Conflict_Check stuff into Annex H.
Meaningful conflict checks clearly depend on obeying
No_Hidden_Indirect_Globals.
****************************************************************
From: Tucker Taft
Sent: Thursday, February 13, 2020 7:37 PM
Here is a slight update to AI12-0079-3, incorporating suggestions from
internal AdaCore review, and from comments here. I have removed the
permission to completely ignore the No_Hidden_Indirect_Globals, without
identifying it as an unsupported capability. I also made some minor changes
to eliminate incompatibilities with SPARK's definition of what is represented
by a package name. In particular, public children are considered completely
independent of their parent and of each other, even though they do have
visibility on the private declarations in the specs of their ancestor units.
If a subprogram wants to indicate it depends on the private state of a public
child, it can name it explicitly, so I think this approach makes sense.
Finally, I moved any mention of dereferences of pool-specific access types to
Annex H. It seemed somewhat out of place in the "core" description. I also
changed it so it talks in terms of the "collection" associated with the
pool-specific access type, which focuses on the allocated objects, rather on
the way you denote them.
[This is version /02 of the AI.]
****************************************************************
From: Christoph Grein
Sent: Sunday, February 16, 2020 9:22 AM
Excuse me, but I did not follow precisely the whole discussion and I did not
really work with SPARK.
As fas as I understood, a global variable in SPARK need not really exist in
order to not violate privacy. Instead a pseudoname is used that is resolved
in the body to existing variables hidden in the body.
In this version of the AI, I read in the Name Resolution Rules that a name
shall statically denote an object or package. Isn't this a violation of
privacy?
****************************************************************
From: Tucker Taft
Sent: Sunday, February 10, 2020 10:11 AM
In SPARK there is the notion of "state abstraction" which can be declared in
the package spec and defined in the package body in terms of specific
variables. Rather than introducing the full complexity of the state
abstraction concept into Ada, we have instead permitted the use of the name
of a package to stand in for all of the hidden global state of the package.
In SPARK terms, it means the name of the package is treated like an
abstract-state identifier that maps to the full set of package-level variables
of the package private part and body (and private descendants).
****************************************************************
From: Randy Brukardt
Sent: Wednesday, February 19, 2020 10:11 PM
> Here is a slight update to AI12-0079-3, incorporating suggestions from
> internal AdaCore review, and from comments here.
...
> !proposal
>
> ** TBD. Similar to AI12-0079-1 and it's later fixups
> (AI12-0240-6 [overriding], AI12-0303-1, AI12-0310-1, and AI12-0334-2),
> but with some in the core and some in an annex.
Ahem. I don't think this will get past Editorial Review. ;-)
Probably you need to replace this with some sort of summary of the proposal.
(Perhaps move some of the text about "simplify the proposal" in the !problem
here.)
The !summary probably also needs an update (not a major change, though). If
you put enough detail in the !summary, then "(See summary.)" would be a
sufficient !proposal.
****************************************************************
From: Tucker Taft
Sent: Saturday, February 22, 2020 8:37 AM
Here is an updated !summary:
Annotations are provided to describe the use of global objects by subprograms,
entries, tasks, and protected units, with a default specifiable at the library
unit level. A new section in the Core of the Standard defines the Global and
Global'Class aspects. In Annex H two restrictions are defined to enforce
stricter requirements on the completeness of the global aspects, along with
some additional capabilities for the global aspects to provide more precision
regarding use of generic formal parameters and dispatching calls.
And as you suggest, !proposal will simply be "See !summary."
****************************************************************
From: Tucker Taft
Sent: Tuesday, March 10, 2020 1:30 PM
One minor "typo" in AI12-0079-3. In the 7th paragraph of the
!discussion it says "USE => ALL" and it should say merely "USE ALL".
I realize you all already caught that subtlety! ;-)
****************************************************************
From: Brad Moore
Sent: Wednesday, March 11, 2020 1:12 PM
The following are my editorial comments for AI12-0079-3 + one for AI12-0363-1
that were not presented during our phone meeting.
- AI12-0079-3:
Summary: 2nd sentence. "In Annex H{,}"
3rd para, Summary, penultimate sentence. "to {cause} erroneous execution."
4th para. "about function side{-}effects"
4th para. last sentence. "subprograms{, } in order to accomplish that goal."
Wording after global_name
1st para. (is also a single sentence, a long one) Can we break it up?
Otherwise, quite a mouthful to parse for the reader. Suggest bulletizing.
as in;
"The Global aspect identifies the set of variables (which, for
the purposes of this clause includes all constants with some
part being immutably limited, or of a controlled type, private
type, or private extension) global to an operation, task unit,
or protected unit, that are potentially read or updated as part
of the execution of:
- the operation; or
- the body of the task; or
- a protected operation of the protected
unit."
It feels like the next sentence (beginning with "Constants") should be a
new/separate paragraph.
1st AARM Discussion in Implementation Permissions, last sentence.
"Note the No_Unspecified_Globals Restriction
(H.4){, which prevents}[to prevent] the use of Unspecified with the Global
aspect in a given partition."
Also, I had a typo in AI12-0363-1, that I didn't mention in our phone meeting.
AARM Ramification: 1st sentence,
"a subcomponent that is specified to be atomic is considered to also specify
that {it} is independently addressable."
****************************************************************
From: Tucker Taft
Sent: Wednesday, March 11, 2020 4:36 PM
Thanks, Brad! A few comments below...
...
> - AI12-0079-3:
>
> Summary: 2nd sentence. "In Annex H{,}"
A comma after "In blah ... " seems optional...
> 3rd para, Summary, penultimate sentence. "to {cause} erroneous execution."
Agreed.
> 4th para. "about function side{-}effects"
Gary might disagree on this one. ;-)
> 4th para. last sentence. "subprograms{, } in order to accomplish that goal."
Comma also seems optional here.
> Wording after global_name
>
> 1st para. (is also a single sentence, a long one) Can we break it up?
> Otherwise, quite a mouthful to parse for the reader. Suggest
> bulletizing. as in;
>
> "The Global aspect identifies the set of variables (which, for
> the purposes of this clause includes all constants with some
> part being immutably limited, or of a controlled type, private
> type, or private extension) global to an operation, task unit,
> or protected unit, that are potentially read or updated as part
> of the execution of:
> - the operation; or
> - the body of the task; or
> - a protected operation of the protected
> unit."
Might want to refactor the sentence a bit. Having done that, the sentence
might be short enough to avoid bullet-izing. Perhaps:
The Global aspect identifies the set of variables (which, for
the purposes of this clause includes all constants with some
part being immutably limited, or of a controlled type, private
type, or private extension) that are global to a callable entity
or task body, and that are read or updated as part of the execution
of the callable entity or task body. If specified for a protected unit,
it refers to all of the protected operations of the protected unit.
> It feels like the next sentence (beginning with "Constants") should be
> a new/separate paragraph.
Agreed.
> 1st AARM Discussion in Implementation Permissions, last sentence.
>
> "Note the No_Unspecified_Globals Restriction (H.4){, which
> prevents}[to prevent] the use of Unspecified with the Global
> aspect in a given partition."
Fine.
> Also, I had a typo in AI12-0363-1, that I didn't mention in our phone
> meeting.
>
> AARM Ramification: 1st sentence,
> "a subcomponent that is specified to be atomic is considered to also
> specify that {it} is independently addressable."
Good catch.
****************************************************************
From: Gary Dismukes
Sent: Wednesday, March 11, 2020 4:54 PM
...
> > - AI12-0079-3:
> >
> > Summary: 2nd sentence. "In Annex H{,}"
>
> A comma after "In blah ... " seems optional...
FWIW, I would put a comma.
> >
> > 3rd para, Summary, penultimate sentence. "to {cause} erroneous execution."
>
> Agreed.
>
> >
> > 4th para. "about function side{-}effects"
>
> Gary might disagree on this one. ;-)
Yep, should be a space, so fine as is. :-)
> > 4th para. last sentence. "subprograms{, } in order to accomplish that
> > goal."
>
> Comma also seems optional here.
I agree, comma is optional.
****************************************************************
From: Brad Moore
Sent: Wednesday, March 11, 2020 4:56 PM
...
>> 4th para. "about function side{-}effects"
>
> Gary might disagree on this one. ;-)
I thought I was channeling my inner Gary here... :-).
But I am not entirely sure. If two or more words serve as a single adjective
before a noun, one would generally use a hyphen. Apparently the general rule
is that when compound modifiers come after a noun, they are not hyphenated:
as in;
The peanuts were chocolate covered.
The author was well known.
But these examples have a verb in-between, so it seems like a different case.
I'd be curious to hear what Gary thinks...
...
> Might want to refactor the sentence a bit. Having done that, the
> sentence might be short enough to avoid bullet-izing. Perhaps:
>
> The Global aspect identifies the set of variables (which, for
> the purposes of this clause includes all constants with some
> part being immutably limited, or of a controlled type, private
> type, or private extension) that are global to a callable entity
> or task body, and that are read or updated as part of the execution
> of the callable entity or task body. If specified for a protected unit,
> it refers to all of the protected operations of the protected unit.
That works for me.
****************************************************************
From: Gary Dismukes
Sent: Wednesday, March 11, 2020 5:40 PM
> >> 4th para. "about function side{-}effects"
> >
> > Gary might disagree on this one. ;-)
>
> I thought I was channeling my inner Gary here... :-).
>
> But I am not entirely sure. If two or more words serve as a single
> adjective before a noun, one would generally use a hyphen. Apparently
> the general rule is that when compound modifiers come after a noun,
> they are not hyphenated: as in;
>
> The peanuts were chocolate covered.
> The author was well known.
>
> But these examples have a verb in-between, so it seems like a different case.
>
> I'd be curious to hear what Gary thinks...
The noun here is "side effects" (a compound noun, but one that is normally
spelled with a space), which is modified by the adjective "function", so a
hyphen isn't appropriate here. OTOH, if it was "side-effect function", then
a hyphen would be appropriate. :-)
****************************************************************
Questions? Ask the ACAA Technical Agent