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

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

!standard C.7.1(4/3)          19-02-26 AI12-0316-1/02
!standard D.2.6(9/5)
!standard D.2.6(29/2)
!standard D.5.1(4)
!standard D.5.1(5)
!standard D.5.1(9)
!standard D.11(3/5)
!standard D.11(9)
!standard D.14(5/2)
!standard D.14(17/2)
!class Amendment 19-02-22
!status Hold 11-0-0 19-02-26
!status work item 19-02-22
!status received 19-02-007
!priority Low
!difficulty Easy
!subject Preconditions for checking Task_Ids
!summary
Preconditions, rather than wording, are used to check Task_Ids in various Annex D subprograms.
!problem
Ada 2020 is attempting to use preconditions and postconditions as much as possible. The following rule appears in a number of places in Annex D:
For all the operations defined in <<some package>>, Tasking_Error is raised if the task identified by T has terminated. Program_Error is raised if the value of T is Null_Task_Id.
This would be better described by a precondition.
!proposal
Add function Valid_Task to Ada.Task_Identification, and then use that in preconditions in Annex D.
!wording
Split C.7.1(4/3) before "private", and add between the existing paragraphs:
function Valid_Task (T : in Task_Id) return Boolean is (if T = Null_Task_Id then raise Program_Error elsif Is_Terminated(T) then raise Tasking_Error);
Add: with Pre => Ada.Task_Identification.Valid_Task (T); to Set_Deadline, Get_Deadline, Set_Relative_Deadline, Get_Relative_Deadline, Get_Last_Release_Time in D.2.6(9/5); to Set_Priority in D.5.1(4); to Get_Priority in D.5.1(5); to Hold, Continue, and Is_Held in D.11(3/5); and to Clock in D.14(5/2).
Replace in AARM D.5.1(12.a) "the above rule saying" with "the precondition".
Delete D.2.6(29/2), D.5.1(9), D.11(8).
Modify D.14(17/2):
The function Clock returns the current execution time of the task identified by T[; Tasking_Error is raised if that task has terminated; Program_Error is raised if the value of T is Task_Identification.Null_Task_Id].
!discussion
!ASIS
[Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.]
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix

From: Randy Brukardt
Sent: Thursday, February  7, 2019  11:42 PM

AI12-0230-1 completely replaces the existing definition of package 
Ada.Dispatching.EDF.

It also has the following paragraph:

  For all the operations defined in Dispatching.EDF, Tasking_Error is
  raised if the task identified by T has terminated. Program_Error is
  raised if the value of T is Null_Task_Id.

(which is pretty much the only unchanged paragraph, but I digress).

This seems to be a (and backwards, IMHO, you have to test null before
termination) way to write:

   Pre => (if T = Ada.Task_Identification.Null_Task_Id then raise Program_Error
           elsif Ada.Task_Identification.Terminated(T) then raise Tasking_Error);

Would the real-time folks freak out like they did when we replaced all of their
pragmas with aspects if we put these on each subprogram (there are 5, I think)?

Or if these are too large, declaring an expression function:

     function Valid_Task (T : in Ada.Task_Identification.Task_Id) return Boolean is
        (if T = Ada.Task_Identification.Null_Task_Id then raise Program_Error
           elsif Ada.Task_Identification.Terminated(T) then raise Tasking_Error);

in the package and then putting

   Pre => Valid_Task (T);

on each subprogram??

Since we're changing this package and the subclause it lives in anyway, we 
probably ought to bring it up to current standards for new packages (and that 
means no English-language preconditions).

Note that manay of the packages in Annex D have a similar rule; we're not 
going to change them all now, but ultimately that would be a good idea.

Thoughts? Brickbats?

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

From: Arnaud Charlet
Sent: Friday, February  8, 2019   3:22 AM

I guess this makes sense from a language point of view.

From a pragmatic point of view this will have zero impact on users since this
package (Ada.Dispatching.EDF) isn't supported by any Ada compiler.

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

From: Tucker Taft
Sent: Friday, February  8, 2019  10:25 AM

Your suggestion seems fine.  I would create Valid_Task only if it is needed 
several times (e.g. 4 or more times).  I would think Valid_Task might want to
be defined in Task_Identification, if we define it.

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

From: Tullio Vardanega
Sent: Friday, February  8, 2019  10:44 AM

As one of the "real-time folks", I am with Tuck in liking your suggestion, 
including his advice to create Valid_Task only if it warrants factoring 
enough instances.
On the whole, using the Pre aspect fits the case and also makes sense 
pedagogically.

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

From: Randy Brukardt
Sent: Friday, February  8, 2019  4:25 PM

> Your suggestion seems fine.  I would create Valid_Task only if it is 
> needed several times (e.g. 4 or more times).

There are 5 uses in EDF alone. Many other packages in Annex D have the same 
rule (pretty much every one that takes a Task_Id as a parameter).

> I would think Valid_Task might want to be defined in 
> Task_Identification, if we define it.

That sounds like a good idea, I was trying to figure out how to generalize 
that since it is clearly not limited to EDF. (Specifically, Execution_Time 
has one such routine; Asynchronous_Task_Control has three such routines; 
and Dynamic_Priorities has three such routines.)

I'll write up an AI for this for the March meeting (past the deadline for 
Monday's meeting).

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

From: Steve Baird
Sent: Friday, February  8, 2019  5:43 PM

> There are 5 uses in EDF alone. Many other packages in Annex D have the 
> same rule (pretty much every one that takes a Task_Id as a parameter).

This amount of repetition suggests that it would be better to define a subtype 
with a predicate (and a Predicate_Failure aspect) and then use that subtype as 
needed.

The problem with that approach is that conceivably there could be a 
compatibility issue. Changing the subtype of a parameter or a function result 
can affect subtype conformance, whereas adding a precondition or 
postcondition won't.

If it weren't for this issue, I would certainly argue for a subtype. And I 
would ignore compatibility issues if we were only talking about EDF because, 
as Arno pointed out, EDF isn't supported by any Ada compiler. But, as Randy 
pointed out, this issue comes up elsewhere and we probably should address the 
problem uniformly.

For compatibility reasons, we certainly would not want to consider changing 
the subtype of the Task_Id parameter mentioned in the 
access-to-protected-procedure type Ada.Task_Termination.Termination_Handler.

Interestingly, invoking Asynchronous_Task_Control.Is_Held with a null task id 
appears to be erroneous (as opposed to raising an exception).

These are examples of the cases that would need to be looked at.

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

From: Randy Brukardt
Sent: Friday, February  8, 2019  5:43 PM

...
> Interestingly, invoking Asynchronous_Task_Control.Is_Held with a null 
> task id appears to be erroneous (as opposed to raising an exception).

D.11(8) seems to apply to Is_Held as well as Hold and Continue, so I don't 
know why you say that.

One could ask if we really want it to do so (typically, with boolean 
functions you just want to return False for nonsense parameters rather than 
raising an exception), but in any case I would not be looking to change any 
semantics in this AI.

> These are examples of the cases that would need to be looked at.
> 
> Thoughts?

I think Tucker's suggestion is best, because these are existing subprograms.
I don't think these are likely to be used in 'Access or one of the other 11 
places that subtype conformance is required (according to the index), but it 
seems possible enough that I'd avoid the predicate. I'd only use a subtype 
predicate on a new subprogram/package, since there isn't enough benefit to 
writing these as contracts to take any incompatibility whatsoever.

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

From: Steve Baird
Sent: Friday, February  8, 2019  6:18 PM

My mistake - I was misremembering the error condition in
D.11(9) as something more like
    "does not specify an existing task"
.

And I agree with you on the larger point of avoiding incompatibilities when 
we are talking about existing code.

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

From: Randy Brukardt
Sent: Tuesday, February 26, 2019  6:55 PM

We voted to Hold this today, so I'm making this comment mainly so it is in the 
e-mail whenever we take it up again.

It strikes me that J-P's late comment about the semantics of Is_Terminated 
provides a solution to this conundrum. Specifically, he noted that calling 
Is_Terminated with an argument of Null_Task_Id raises Program_Error (see 
C.7.1(15/5)). Therefore, it isn't necessary to explicitly handle the 
Program_Error case in the precondition, and it isn't necessary to write a 
subprogram in that case, either. The precondition can just be:

   when Pre => (if Ada.Task_Identification.Is_Terminated (T) 
                then raise Tasking_Error);

which probably is short enough to just replicate for the 10 uses.

I note in passing that passing a Task_Id whose task doesn't exist to 
Is_Terminated is erroneous, meaning that the separate Erroneous Execution 
rules in Annex D aren't strictly necessary either (probably still a good 
reminder, so I wouldn't recommend removing them).

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

Questions? Ask the ACAA Technical Agent