Version 1.12 of ai12s/ai12-0090-1.txt

Unformatted version of ai12s/ai12-0090-1.txt version 1.12
Other versions for file ai12s/ai12-0090-1.txt

!standard 9.5.4(5/3)          15-01-19 AI12-0090-1/06
!standard 9.5.4(7/3)
!standard 9.5.4(12/3)
!class binding interpretation 13-10-31
!status Corrigendum 2015 14-11-12
!status WG9 Approved 15-06-26
!status ARG Approved 7-0-0 14-10-18
!status work item 13-10-31
!status received 13-10-11
!priority High
!difficulty Hard
!qualifier Omission
!subject Pre- and Postconditions and requeues
!summary
The preconditions of a target entry are evaluated before a call is requeued. The postconditions of a target entry have to be the same as those on the current entry.
!question
Interactions between pre/post-condition checking (for entries) and requeues appear to have some peculiar consequences.
Suppose entries E1 and E2 have pre- and post-conditions, a call to E1 requeues to E2, and E2 returns normally.
Is E2's precondition ever checked? (A requeue isn't a call!) Is E1's postcondition ever checked?
Is the answer to either of these questions a problem that needs to be fixed? (Yes.)
!recommendation
(See Summary.)
!wording
Add after 9.5.4(5/3) [Legality Rules]:
Given a requeue_statement where the innermost enclosing callable construct is for an entry E1, for every [Redundant:specific or class-wide] postcondition expression P1 that applies to E1, there shall exist a postcondition expression P2 that applies to the requeue target E2 such that
- P1 is fully conformant with the expression produced by
replacing each reference in P2 to a formal parameter of E2 with a reference to the corresponding formal paramter of E1; and
- if P1 is enabled, then P2 is also enabled.
AARM Note: Roughly speaking, the postcondition of the requeue target is required to imply that of the enclosing callable construct.
The requeue target shall not have an applicable specific or class-wide postcondition which includes an Old attribute_reference.
If the requeue target is declared immediately within the task_definition of a named task type or the protected_definition of a named protected type, and if the requeue statement occurs within the body of that type, and if the requeue is an external requeue, then the requeue target shall not have a specific or class-wide postcondition which includes a name denoting either the current instance of that type or any entity declared within the declaration of that type.
Insert a new sentence in middle of 9.5.4(7/3) [Dynamic Semantics]:
The execution of a requeue_statement proceeds by first evaluating the procedure_or_entry_name [Redundant:, including the prefix identifying the target task or protected object and the expression identifying the entry within an entry family, if any]. {Precondition checks are then performed as for a call to the requeue target entry or subprogram.} The entry_body or accept_statement enclosing the requeue_statement is then completed[Redundant:, finalized, and left (see 7.6.1)].
Modify 9.5.4(12/3) [also in Dynamic Semantics]:
If the requeue target named in the requeue_statement has formal parameters, then during the execution of the accept_statement or entry_body corresponding to the new entry {and during the checking of any preconditions of the new entry}, the formal parameters denote the same objects as did the corresponding formal parameters of the callable construct completed by the requeue. [Redundant:In any case, no parameters are specified in a requeue_statement; any parameter passing is implicit.]
!discussion
Let's assume that E1 and E2 are as defined in the question.
Entering any callable entity without evaluating its precondition is trouble, as the body may assume that the precondition is true. (This is assuming that the Assertion_Policy is Check, of course.) We need to ensure that E2's precondition holds before its body executes, whether or not a requeue is a call.
Thus, we require that a requeue check the enabled preconditions of the entry E2 before the call is requeued.
One expects the postcondition of E2 will be evaluated, but this is problematical if that postcondition includes 'Old references that were never evaluated on the original call. Moreover, the postcondition of E1 will never be evaluated. That means that any promises that the postcondition of E1 makes could very well be false.
Thus, we require that the postconditions of E1 and E2 be the same (fully conform). For external requeues, we further require that they don't contain any references to parts of the object (such as a task discriminant) which might have different values in the different task or protected objects. [The objects necessarily are different objects of the same type; otherwise the full conformance check would have failed (if the types are different), it's an immediate deadlock (if it's the same task object), or it's an immediate bounded error that probably raises Program_Error (if it's the same protected object). Thus the rule only needs to apply to types and not to single objects.] We allow such references if this is an internal call, as such references necessarily are to the same object and thus have the same value.
We do not attempt to prevent uses in postconditions of things like (instances of) Ada.Task_Attributes or Ada.Task_Identification.Current_Task even though those might yield different results depending on the identity of the task which evaluates the postcondition expression. That's because these can be used in any function called from the postcondition, including functions declared outside of the task. As such, we can't really prohibit such things, and doing a partial job doesn't seem very helpful. Additionally, Current_Task and the associated task attributes aren't even well-defined in a protected entry body, so they aren't useful in postconditions of protected entries. So we don't think the problematic uses will appear very often, and mixing them with requeues will be rarer still.
We considered the effect on Type Invariants. We eventually concluded that the primary use of type invariants is for the writer of the body, so a promise to the caller is less important. In addition, type invariants already have a number of other holes, so adding one more unlikely way to escape a check doesn't change the utility of the feature much. Whereas we believe the checking of postconditions cannot be evaded, thus we expect programmers to trust them and do not want to introduce any way to have enabled postconditions to be unchecked.
!corrigendum 9.5.4(5/3)
Insert after the paragraph:
If the requeue target has parameters, then its (prefixed) profile shall be subtype conformant with the profile of the innermost enclosing callable construct.
the new paragraphs:
Given a requeue_statement where the innermost enclosing callable construct is for an entry E1, for every specific or class-wide postcondition expression P1 that applies to E1, there shall exist a postcondition expression P2 that applies to the requeue target E2 such that
The requeue target shall not have an applicable specific or class-wide postcondition which includes an Old attribute_reference.
If the requeue target is declared immediately within the task_definition of a named task type or the protected_definition of a named protected type, and if the requeue statement occurs within the body of that type, and if the requeue is an external requeue, then the requeue target shall not have a specific or class-wide postcondition which includes a name denoting either the current instance of that type or any entity declared within the declaration of that type.
!corrigendum 9.5.4(7/3)
Replace the paragraph:
The execution of a requeue_statement proceeds by first evaluating the procedure_or_entry_name, including the prefix identifying the target task or protected object and the expression identifying the entry within an entry family, if any. The entry_body or accept_statement enclosing the requeue_statement is then completed, finalized, and left (see 7.6.1).
by:
The execution of a requeue_statement proceeds by first evaluating the procedure_or_entry_name, including the prefix identifying the target task or protected object and the expression identifying the entry within an entry family, if any. Precondition checks are then performed as for a call to the requeue target entry or subprogram. The entry_body or accept_statement enclosing the requeue_statement is then completed, finalized, and left (see 7.6.1).
!corrigendum 9.5.4(12/3)
Replace the paragraph:
If the requeue target named in the requeue_statement has formal parameters, then during the execution of the accept_statement or entry_body corresponding to the new entry, the formal parameters denote the same objects as did the corresponding formal parameters of the callable construct completed by the requeue. In any case, no parameters are specified in a requeue_statement; any parameter passing is implicit.
by:
If the requeue target named in the requeue_statement has formal parameters, then during the execution of the accept_statement or entry_body corresponding to the new entry and during the checking of any preconditions of the new entry, the formal parameters denote the same objects as did the corresponding formal parameters of the callable construct completed by the requeue. In any case, no parameters are specified in a requeue_statement; any parameter passing is implicit.
!ASIS
No changes needed.
!ACATS test
An ACATS C-Test is needed to check that the handling of overlong encodings is correct.
!appendix

From: Steve Baird
Sent: Friday, October 11, 2013  7:53 PM

One reasonably substantive question followed by two corner case nits.

[Editor's note: Each question is handled separately.]

1) In internal discussions at AdaCore, it was noted that the
    interactions between pre/post-condition checking (for entries)
    and requeues appear to have some peculiar consequences.

    Suppose entries E1 and E2 have pre- and post-conditions,
    a call to E1 requeues to E2, and E2 returns normally.

    Is E2's precondition ever checked? (note that a requeue isn't a call)
    Is E1's postcondition ever checked?

    Is the answer to either of these questions a problem that
    needs to be fixed?

    [I don't think uses of 'Old in either of the two post-conditions
    add any problems, but it seems like a case to bear in mind
    when considering possible language changes in this area.]

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

From: Jean-Pierre Rosen
Sent: Monday, October 14, 2013  4:55 AM

I tend to think that the pre/post conditions should match between initial and
requeued entry, the same way as profiles must match, because the user shouldn't
even know that the service is provided through requeue. Matching conditions
could be (TBD) either the same, or weaker preconditions / stronger
post-conditions.

I understand that in practice, this means introducing a new conformance kind,
but it may be useful in other cases as well...

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

From: Tucker Taft
Sent: Monday, October 14, 2013  9:19 AM

I agree, though weaker/stronger is not something the compiler should be expected
to determine, so these will require run-time checks or a very simple static
rule.  To keep things static, a simple rule would be no precondition or a
matching precondition on the target of the requeue (vaguely reminiscent of no
parameters or matching parameters). Similarly, the entry doing the requeue would
be required do have no postcondition or a postcondition that matched that of the
target entry.

> I understand that in practice, this means introducing a new
> conformance kind, but it may be useful in other cases as well...

E.g. a renaming-as-body could have used a similar rule.

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

From: Bob Duff
Sent: Monday, October 14, 2013  10:07 AM

> I agree, though weaker/stronger is not something the compiler should
> be expected to determine, so these will require run-time checks or a
> very simple static rule.  To keep things static, a simple rule would
> be no precondition or a matching precondition on the target of the
> requeue (vaguely reminiscent of no parameters or matching parameters).
> Similarly, the entry doing the requeue would be required do have no
> postcondition or a postcondition that matched that of the target entry.

I don't get it.  If E1 changes the state of the world, and then requeues to E2,
how can E2 be expected to have the same precondition? And if E1 has Post =>
F(X), then callers expect F(X) to be True upon return, but you're allowing E2 to
have no postcondition, so there's no run-time check that F(X) is True.

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

From: Tucker Taft
Sent: Monday, October 14, 2013  10:32 AM

Sorry, I was both confused and confusing.  If E1 requeues on E2, then E1 must
check E2's precondition prior to the requeue, and E2 must have the same
postcondition as E1, or E1 must have no postcondition at all.

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

From: Randy Brukardt
Sent: Monday, October 14, 2013  8:24 PM

> > I understand that in practice, this means introducing a new
> > conformance kind, but it may be useful in other cases as well...
>
> E.g. a renaming-as-body could have used a similar rule.

I don't see any new conformance kind here, or any new use of a similar rule.
We already use expression conformance in the renames-as-body case (6.1.1(17/3)),
and it's part of the homograph check in the requires overriding case
(6.1.1(13/3) and (16/3)). I would expect that we'd use expression conformance in
the same way if we wanted to enforce a similar rule. If we did find some reason
that the existing expression conformance was too limiting, I'm sure we'd change
it in such a way that it applied to all conformance (as we did for quantified
expressions).

The point being, we already do this in some cases, it certainly would make sense
to do it in more cases if that is necessary for those cases to make sense.

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

From: Steve Baird
Sent: Tuesday, October 15, 2013  11:06 AM

> I would expect that we'd use
> expression conformance in the same way if we wanted to enforce a
> similar rule. If we did find some reason that the existing expression
> conformance was too limiting, I'm sure we'd change it in such a way
> that it applied to all conformance (as we did for quantified expressions).

I think that requiring full conformance of postcondition expressions wouldn't
handle 'Old correctly (at least given the current definition of full
conformance).

Let's say the postcondition for both entries is
     X = X'Old + 1

Say E1 increments X and then requeues on E2; E2 increments X again, performs its
postcondition check (which passes), and returns normally.

The original caller is surprised to find that X has grown by 2, not 1.

One way to look at it is that the two uses of X'Old are names denoting two
different (implicitly declared) constants.

If we choose to view it that way, then it might make sense to (as you mentioned)
change the definition of expression conformance to handle this case.

I think this would be a compatible change because 'Old attribute references are
only allowed in postconditions and there are currently no language rules for
which the full conformance (or lack thereof) of a postcondition expression with
some other expression matters.

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

From: Jean-Pierre Rosen
Sent: Tuesday, October 15, 2013  11:33 AM

Do you mean that you are willing to accept that behaviour? I certainly wouldn't;
I'd prefer to completely remove postconditions on entries - better have no
contract than a contract you can't trust.

How to achieve correct behaviour is another matter. I can only think of either
passing all 'Old to the second entry, or evaluating the postcondition of the
first entry after the one of the second entry. Both seem unpleasant...

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

From: Tucker Taft
Sent: Tuesday, October 15, 2013  11:36 AM

> I think that requiring full conformance of postcondition expressions
> wouldn't handle 'Old correctly (at least given the current definition
> of full conformance).
>
> Let's say the postcondition for both entries is
>      X = X'Old + 1
>
> Say E1 increments X and then requeues on E2; E2 increments X again,
> performs its postcondition check (which passes), and returns normally.
>
> The original caller is surprised to find that X has grown by 2, not 1.

Ugh!

>
> One way to look at it is that the two uses of X'Old are names denoting
> two different (implicitly declared) constants.
>
> If we choose to view it that way, then it might make sense to (as you
> mentioned) change the definition of expression conformance to handle
> this case.

Interesting way to look at it.  But what happens if you requeue on yourself?

I suspect we will want to disallow requeue from an entry that uses 'Old in a
postcondition.

> I think this would be a compatible change because 'Old attribute
> references are only allowed in postconditions and there are currently
> no language rules for which the full conformance (or lack thereof) of
> a postcondition expression with some other expression matters.

I think we should just say that X'Old doesn't conform, even with itself.

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

From: Steve Baird
Sent: Tuesday, October 15, 2013  11:54 AM

> I suspect we will want to disallow requeue from an entry that uses
> 'Old in a postcondition.

Sounds right to me.

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

From: Randy Brukardt
Sent: Monday, June 23, 2014  6:44 PM

Here are some comments from me on Steve's AI12-0090-1/02. Steve and I both
hoped that he's be able to deal with some or all of these before the deadline,
but that wasn't possible. So I'm sending these to the group to put them on
the record for when we discuss the AI this weekend.

               Randy.

---------

In the !wording section:

  Section 7.3.2 (Type Invariants) describes the criteria for determining
  whether type invariant checks associated with a given type T
  are performed upon successful return from a given subprogram subprogram
Dept. of redundancy dept.--------------------------------------^
  or entry. Such a subprogram or entry is said to be a boundary subprogram
  for the type T. The entry corresponding to the enclosing callable
  construct shall not be a boundary subprogram for any type T.

[Discussion: Keep it simple; we could try for some rules like with postconditions
saying that the same type invariant checks must be performed by the entry of the
enclosing callable entity and by the requeue target, but that seems unnecessarily
complicated.]

This isn't wording! You have to insert something into 7.3.2 to define "type
invariant boundary callable entity". (An entry is not a subprogram, so defining
it to be some sort of subprogram isn't going to fly.) And then you have to have
a rule in 9.5.4 somewhere using that definition.

Also, I think there needs to be a discussion of this problem in the !discussion
section. (In particular, how it could arise as described in the minutes.)

---

I'd also like some discussion of the problem that led to the last new paragraph
in 9.5.4(5/3). I have no idea why that's needed, and while I'm sure it's
important, we need to put why on the record somewhere.

---

I don't see how "named entry E1" (in the new text 9.5.4(5/3)) works if the
requeue is on a procedure implemented by an entry. This is *not* an entry. I
also think you need to work in "target" somehow. Because this doesn't say
what's naming the entry E1. All of the other nearby paragraphs say either
"target" or "requeue target". Maybe you could solve both issues by saying
"named target E1" so that it doesn't actually mention entry. (Otherwise,
"entry or subprogram" would needed.) (I'm assuming you want to say "named"
so that the rule applies nominally -- "named" here meaning about the same as
"statically denoted" and not at run-time (which of course would be impossible
because you don't know the preconditions of the actual entity if this is
dispatching call through an interface).

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

From: Steve Baird
Sent: Wednesday, June 25, 2014  1:35 PM

> Steve and I both
> hoped that he's be able to deal with some or all of these before the 
> deadline, but that wasn't possible.

Better late than never. I got a little bit of extra time due to a flight delay
 - at least I found out about it before going to the airport.

Typo: "paramter".

>> Section 7.3.2 (Type Invariants) describes the criteria for determining
>>   whether type invariant checks associated with a given type T
>>   are performed upon successful return from a given subprogram
>>   or entry. Such a subprogram or entry is said to be a boundary subprogram
>>   for the type T.
>
> This isn't wording! You have to insert something into 7.3.2 to define 
> "type invariant boundary callable entity". (An entry is not a 
> subprogram, so defining it to be some sort of subprogram isn't going 
> to fly.) And then you have to have a rule in 9.5.4 somewhere using that definition.

I was trying to confine the changes to 9.5.4, but we could certainly take the
approach you describe if folks feel that is more appropriate.
I agree that it would be cleaner if 7.3.2 defined the term that we want.

> I'd also like some discussion of the problem that led to the last new 
> paragraph in 9.5.4(5/3).

Suppose we have a task or protected type T with an entry E and two objects,
X1 and X2, of that type. Suppose further that we requeue from X1.E to X2.E. If
the postcondition for E refers to the current instance of the type (or
something declared therein). Then the postconditions for X1.E and for X2.E are
not the same (in particular, the postcondition for X2.E does not imply the
postcondition for X1.E, which is the high-level goal of these postcondition
rules). Consider, for example, a postcondition expression involving T'Identity
or E'Count.

There may be a similar issues now that I think of it, with postconditions that
reference Task_Identification.Current_Task. Ugh.

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

Questions? Ask the ACAA Technical Agent