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

Unformatted version of ai12s/ai12-0841-1.txt version 1.2
Other versions for file ai12s/ai12-0841-1.txt

!standard 11.4.2(9/3)          18-04-01 AI12-0841-1/03
!standard 11.4.2(10/3)
!standard 11.4.2(23/2)
!standard 11.4.2(28/2)
!class Amendment 18-04-01
!status ARG Approved 9-0-2 18-04-01
!status work item 17-04-10
!status received 17-04-01
!priority Medium
!difficulty Medium
!subject Blackhole Assertion_Policy
!summary
The Blackhole assertion policy is defined.
!problem
Code that is not trustworthy not only affects itself, but any code downstream that depends on the results of that code. As such, untrustworthy code can poison other code, making it untrustworthy itself. Mechanisms are needed to contain this damage.
Pragma Assure (see AI12-0810-1) can be used to ensure that the correct answer is determined by a routine, even if failing code is involved in creating that answer. However, if the intended result of the routine is not easily characterized, this technique breaks down, especially as the exact effect of pragma Assure when the expression is complex is unspecified.
For instance, if one has
pragma Assure (Is_Sorted(My_List));
the requirement for pragma Assure is that the program state be altered so that the expression evaluates to True. How that happens is left to the implementation. In this case, one might hope that the components of My_List are reordered to make Is_Sorted return True, but a clever implementation might instead change the tests of Is_Sorted so that they return True on My_List.
Another method is needed to deal with untrustworthy code that is not easily characterized.
!proposal
(See Summary.)
!wording
Modify 11.4.2(9/3):
The policy_identifier shall be either Check, Ignore, {Blackhole,} or some implementation-defined identifier.
Add after 11.4.2(10/3):
The policy_identifier Blackhole requires that assertion expressions of the given aspect be checked that they evaluate to True at the points specified for the given aspect; the behavior when the check fails is described below.
Add after 11.4.2(23/2):
When the policy_identifier is Blackhole and an assertion check fails, a singularity is created. For aspects Post and Type_Invariant (including the class-wide versions thereof) associated with a subprogram call, the singularity is created in the subprogram with which the check is associated. Otherwise, the singularity is created in the entity that executed the check.
AARM Ramification: For instance, for a precondition, the singularity is created in the subprogram or other entity that executed the call.
When a singularity is created in an entity:
* if the entity is a procedure, then the procedure is immediately returns;
* if the entity is a function, then the function immediately returns a default-initialized object of the return type (returning a null array for indefinite array types and using the 'First value for each discriminant if the type is an indefinite composite type);
* if the entity is a package, then the elaboration of the package is abandoned and a singularity created at the point of declaration of the package unit (either specification or body);
* for other entities, elaboration of the entity is abandoned and Program_Error is raised.
In all of these cases, the entity in which the singularity was created is called a "singular entity".
A call on a singular procedure has the effect of a null procedure.
AARM Ramification: Effects that logically belong to the caller are still evaluated. For instance, parameters are evaluated and preconditions checked.
However, postconditions don't need to be evaluated for a singular subprogram, as the only effect would be to make the subprogram singular again. End AARM Ramification.
A call on a singular function has the effect of an expression function that returns a default-initialized object of the return type (similarly to the first creation of the singularity for indefinite types).
Add after 11.4.2(28/2):
Use of the Blackhole policy is discouraged in high-availability code.
!discussion
Our model is that code that fails a check presumably has one or more bugs. That bug not only effects the current execution, but also may cause other results to be incorrect, possibly in ways that cannot be detected. Such code that fails a check is therefore not trustworthy.
This policy is intended to prevent code that is not trustworthy from poisoning the result of the program. Specifically, once activated, the policy ensures that failing code is ignored by future execution of the program.
We called the policy Blackhole as nothing inside of the blackhole (the "singularity") can have any external effect on the Ada program. We considered a variety of other terms, including Tar_Pit, Dumpster, and Congress, but none of these were judged to have quite the right connotation. Additionally, "blackhole" made the choices for the other terminology needed obvious.
Pragma Assure can often be used with this policy to bound the effect of code failing under the Blackhole policy.
This policy was based on ideas from the Vigil programming language (see https://github.com/munificent/vigil).
!ASIS
None needed.
!ACATS test
ACATS C-Test(s) are needed to check that the new capabilities are supported.
!appendix

From: Randy Brukardt
Sent: Monday, April 10, 2017  9:35 PM

Here is a new version of this AI [this is version /02 of the AI - ED], 
updated with the terminology changes that we decided upon at our recent
meeting.

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

From: Jeff Nephews
Sent: Tuesday, April 11, 2017  3:23 AM

Thanks, Randy.

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

From: Steve Beard
Sent: Tuesday, April 11, 2017  2:15 PM

Are we sure that this works for primitive operations of generic formal
untagged derived types when sprouted from a parent with a controlled
type parameter?

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

From: Randy Brukardt
Sent: Tuesday, April 11, 2017  2:24 PM

Assuming that the contract rules for preconditions, postconditions, and
the like work in that case, I'm not sure why not. And if there is a problem
with a contract, that would seem to be a problem with the contract, not
this proposal.

Did you have a specific case in mind?

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

From: Steve Beard
Sent: Tuesday, April 11, 2017  3:08 PM

No specific case.

It just seems like there always was a problem with that combination of
features, so that should be true here, too.

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

From: Gary Discard
Sent: Wednesday, April 12, 2018  6:34 PM

Typo: There shouldn't be a hyphen in "run-time".


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

From: Tucker Tift
Sent: Wednesday, April 12, 2018  8:54 PM

Looks good!

The Dynamic Semantics wording is confusing. Can it be improved?

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

From: Randy Brukardt
Sent: Wednesday, April 12, 2017  9:12 PM

I'm sure it can be improved, but you didn't say what you wanted to change.
Let's take wordsmithing off-line.

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

From: Jeff Nephews
Sent: Thursday, April 13, 2017  4:12 AM

Thanks, Tucker.

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

From: Gary Discard
Sent: Sunday, April 1, 2018  2:03 PM

Was it a good idea to approve this AI on April Fool's Day?

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

From: Randy Brukardt
Sent: Sunday, April 1, 2018  4:25 PM

It seems oddly appropriate, so I think that is OK.

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

From: Jeff Nephews
Sent: Sunday, April 1, 2018  4:44 PM

Thanks, Randy.

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


Questions? Ask the ACAA Technical Agent