!standard 9.5.4(5/3) 14-05-30 AI05-0090-1/02 !standard 9.5.4(7/3) !standard 9.5.4(12/3) !class binding interpretation 13-10-31 !status work item 13-10-31 !status received 13-10-11 !priority High !difficulty Hard !qualifier Omission !subject Pre- and Postconditions and requeues !summary Something sensible happens with the pre- and postconditions when a requeue occurs. !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): For every [Redundant:specific or class-wide] postcondition expression P1 that applies to the named entry E1, there shall be exist a postcondition expression P2 that applies to the entry E2 of the innermost enclosing callable construct such that - P1 is fully conformant with the 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 shall imply that of the enclosing callable construct. The named entry shall not have an applicable specific or class-wide postcondition[Redundant:, enabled or not,] which includes an Old attribute_reference. If the named entry's declaration is part of 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, then the named entry shall not have a specific or class-wide postcondition[Redundant:, enabled or not] which includes a name denoting either the current instance of that type or any entity declared within that type's declaration. [Discussion: This introduces a case where replacing an anonyous task/protected type with the "equivalent" type/object declaration pair isn't equivalent - the latter version might violate this rule. If this is viewed as a problem, the obvious solution is to also ban the construct in the case of an anonymous type even though we don't really need to.] Insert a new sentence in middle of 9.5.4(7/3): 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 named entry.} 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): 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.] [Editor's note: the following isn't wording, although it ought to be.] 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. 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.] !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. 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. We can use Legality Rules or dynamic checks to ensure these things are true on a requeue. For a Legality Rule, we can use the existing conformance mechanism -- we already do that for precondition inheritance. The advantage of using Legality Rules is that they can be compatibly relaxed in the future; changing runtime rules would be inconsistent. !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. ***************************************************************