Version 1.3 of ai12s/ai12-0256-1.txt

Unformatted version of ai12s/ai12-0256-1.txt version 1.3
Other versions for file ai12s/ai12-0256-1.txt

!standard H.4.1(0)          18-07-06 AI12-0256-1/02
!standard 13.1.1(18.7/5)
!class Amendment 18-01-31
!status Amendment 1-2012 18-07-06
!status ARG Approved 10-0-0 18-06-23
!status work item 18-01-31
!status received 18-01-21
!priority Very_Low
!difficulty Easy
!subject Aspect No_Controlled_Parts
!summary
Aspect No_Controlled_Parts is added to Ada.
!problem
In high-integrity, embedded applications, it is usually necessary to prove that the program will not run into stack overflow or other problems. It is often required to prove these properties at the machine code level with a special tool. The use of dynamic finalization greatly complicates such analysis as it depends on implicit dynamic dispatching. Thus many such applications ban finalization.
On the other hand, it is desirable, and becoming accepted, to use tagged types and dynamic dispatching even in high-integrity applications. Static analysis tools for stack usage can usually deal with the dynamic dispatching (even if it introduces some over-estimation), but a harder problem is that dynamic dispatching requires class-wide subtypes.
In general, class-wide subtypes are compiled such that any possible future extension will work. That includes, of course, extensions that include controlled components. This brings in finalization overhead, even if none of the current types use any finalization.
It would be desirable to be able to declare that a type and any descendants will not use any finalization, so this overhead can be eliminated (and thus, eliminated from analysis).
!proposal
(See Summary.)
!wording
[Editor's note: I'm not sure where this goes in the Standard. It seems related to H.4, High-Integrity Restrictions, and it IS a restriction, but only on a single type and its descendants. So I've put it there pending discussion.
H.4.1 Aspect No_Controlled_Parts
Static Semantics
For a type, the following type-related, operational aspect may be specified:
No_Controlled_Parts
The type of this aspect is Boolean. If True, requires that the type and any descendants do not have any controlled parts. If specified, the value of the expression shall be static. If not specified, the value of this aspect is considered False.
The No_Controlled_Parts aspect is nonoverridable (see 13.1.1).
Legality Rules
If No_Controlled_Parts is True for a type, no component of the type shall have a controlled part nor shall the type itself be controlled. In addition to the places where Legality Rules normally apply (see 12.3), this rule also applies in the private part of an instance of a generic unit.
When enforcing the above rule within a generic body, a generic formal private type and a generic formal derived type of a composite type are considered to have a controlled part.
AARM Reason: This is a typical generic assume-the-worst rule.
Modify 13.1.1(18.7/5) to include aspect No_Controlled_Parts.
!discussion
We could have extended this aspect to allow it to be given on generic formal types. If specified True there, then only types with this aspect specified True would match. This would allow declaring types with the aspect in a generic body which have components of generic formal private types. However, most such types can be declared in the private part of the generic (where assume-the-best is used and a recheck is made if necessary). So this was considered overkill.
---
The only Ada 2012 way to eliminate finalization is to use pragma Restrictions (No_Dependence => Ada.Finalization); However, this requires the entire program (including the runtime) to avoid using finalization. This means that features like storage pools and the bounded indefinite container(s) [see AI12-0254-1] cannot be used in such programs, even if they are designed with trivial finalization. (Most compilers can eliminate finalization overhead from objects with trivial finalization.)
The proposed aspect allows eliminating overhead specifically from class-wide type hierarchies while still allowing controlled types to appear in the runtime and elsewhere.
!corrigendum 13.1.1(18.6/5)
!comment This was the original paragraph number, AI12-0211-1 changed it.
!comment We have to use the original number here so that a conflict is
!comment properly detected.
@drepl The Default_Iterator, Iterator_Element, Implicit_Dereference, Constant_Indexing, Variable_Indexing, and Max_Entry_Queue_Length aspects are nonoverridable. @dby The Default_Iterator, Iterator_Element, Implicit_Dereference, Constant_Indexing, Variable_Indexing, Max_Entry_Queue_Length, and No_Controlled_Parts aspects are nonoverridable.
!corrigendum H.4.1(0)
Insert new clause:
Static Semantics
For a type, the following type-related, operational aspect may be specified:
No_Controlled_Parts
The type of this aspect is Boolean. If True, requires that the type and any descendants do not have any controlled parts. If specified, the value of the expression shall be static. If not specified, the value of this aspect is considered False.
The No_Controlled_Parts aspect is nonoverridable (see 13.1.1).
Legality Rules
If No_Controlled_Parts is True for a type, no component of the type shall have a controlled part nor shall the type itself be controlled. In addition to the places where Legality Rules normally apply (see 12.3), this rule also applies in the private part of an instance of a generic unit.
When enforcing the above rule within a generic body, a generic formal private type and a generic formal derived type of a composite type are considered to have a controlled part.
!ASIS
[Not sure. Not sure how aspects are handled - Editor.]
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix

This AI was split from AI12-0254-1. The original request for this aspect
can be found in the !appendix of that AI, in a message dated Sunday, January
21, 2018, 9:48 AM.

****************************************************************

From: Bob Duff
Sent: Sunday, April 15, 2018  4:54 PM

[He's replying to an off-hand remark on a Letter Ballot - Editor.]

> I donít see any of them as important, and the ones I havenít voted for 
> at all as possibly even being harmful, but hereís my 5 most useful.

...

> ______  AI12-0256-1/01   2018-01-31 --  Aspect No_Controlled_Subcomponents

Why do you consider that one harmful?  There's the usual (every new feature
causes implementation cost, and cost to define it in the RM, and adds
complexity to the language).  Anything else?


****************************************************************

From: Jeff Cousins
Sent: Monday, April 16, 2018  2:12 AM

I should have said apart from that one (which I'm neutral about).

****************************************************************

Questions? Ask the ACAA Technical Agent