!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 1-2012 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) @dinsa If the requeue target has parameters, then its (prefixed) profile shall be subtype conformant with the profile of the innermost enclosing callable construct. @dinss Given a requeue_statement where the innermost enclosing callable construct is for an entry @i, for every specific or class-wide postcondition expression @i that applies to @i, there shall exist a postcondition expression @i that applies to the requeue target @i such that @xbullet<@i is fully conformant with the expression produced by replacing each reference in @i to a formal parameter of @i with a reference to the corresponding formal paramter of @i; and> @xbullet is enabled, then @i is also enabled.> 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 @fa of a named task type or the @fa 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) @drepl The execution of a @fa proceeds by first evaluating the @i@fa, including the @fa identifying the target task or protected object and the @fa identifying the entry within an entry family, if any. The @fa or @fa enclosing the @fa is then completed, finalized, and left (see 7.6.1). @dby The execution of a @fa proceeds by first evaluating the @i@fa, including the @fa identifying the target task or protected object and the @fa 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 @fa or @fa enclosing the @fa is then completed, finalized, and left (see 7.6.1). !corrigendum 9.5.4(12/3) @drepl If the requeue target named in the @fa has formal parameters, then during the execution of the @fa or @fa 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 @fa; any parameter passing is implicit. @dby If the requeue target named in the @fa has formal parameters, then during the execution of the @fa or @fa 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 @fa; 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. ***************************************************************