!standard 6.1.1(26/4) 16-12-21 AI12-0193-1/04 !standard 7.3.2(20/3) !standard 9.5.2(24) !standard 9.5.2(25) !class binding interpretation 16-06-06 !status Amendment 1-2012 16-11-09 !status ARG Approved 9-0-1 16-10-08 !status work item 16-06-06 !status received 16-01-29 !priority Low !difficulty Medium !qualifier Omission !subject Postcondition failure for a task entry !summary An exception raised by a postcondition check for an entry is raised inside of the accept statement as well as at the call site. !question 6.1.1(35.1/4) says in part: "For a call to a task entry, the postcondition check is performed before the end of the rendezvous; ..." What happens if this check fails? Obviously, Assertion_Error is raised at the point of the check. Where is the exception propagated? 9.5.2(24) says: "When an exception is propagated from the handled_sequence_of_statements of an accept_statement, the same exception is also raised by the execution of the corresponding entry_call_statement." Clearly, a postcondition check is not in the handled_sequence_of_statement. Indeed, formally, it's checked at the call site (an entry_call_statement in this case) - the wording is "upon successful return". So, from that, the exception should be raised at the call site, but not in the accept statement. However, the "before the end of the rendezvous" wording implies that the check is inside of the accept statement, so it would be weird if it wasn't raised there. Is it propagated to the accept statement? (Yes.) !recommendation (See Summary.) !wording Add after 6.1.1(26/4): AARM Ramification: In the case of an accept statement, the constant is declared inside of the rendezvous. It is considered part of the initialization of the postcondition check, which is part of the rendezvous by definition (see 9.5.2). Replace 7.3.2(20/3): The check is performed on each such part of type T. with The check is performed on each such part of type T. In the case of a call to a protected operation, the check is performed before the end of the protected action. In the case of a call to a task entry, the check is performed before the end of the rendezvous. Replace 9.5.2(24): For the execution of an accept_statement, the entry_index, if any, is first evaluated and converted to the entry index subtype; this index value identifies which entry of the family is to be accepted. Further execution of the accept_statement is then blocked until a caller of the corresponding entry is selected (see 9.5.3), whereupon the handled_sequence_of_statements, if any, of the accept_statement is executed, with the formal parameters associated with the corresponding actual parameters of the selected entry call. Upon completion of the handled_sequence_of_statements, the accept_statement completes and is left. When an exception is propagated from the handled_sequence_of_statements of an accept_statement, the same exception is also raised by the execution of the corresponding entry_call_statement. with The interaction between a task that calls an entry and an accepting task is called a @i. For the execution of an accept_statement, the entry_index, if any, is first evaluated and converted to the entry index subtype; this index value identifies which entry of the family is to be accepted. Further execution of the accept_statement is then blocked until a caller of the corresponding entry is selected (see 9.5.3), whereupon the handled_sequence_of_statements, if any, of the accept_statement is executed, with the formal parameters associated with the corresponding actual parameters of the selected entry call. Execution of the rendezvous consists of the execution of the handled_sequence_of_statements, performance of any postcondition or type invariant checks associated with the entry, and any initialization or finalization associated with these checks, as described in 6.1.1 and 7.3.2. After execution of the rendezvous, the accept_statement completes and is left. The two tasks then proceed independently. When an exception is propagated from the execution of a rendezvous, the same exception is also raised by the execution of the corresponding entry_call_statement. AARM Ramification: Execution of the rendezvous does not include any checks associated with parameter copy back or any post-call subtype predicate check for a parameter which is passed by reference. These checks are performed by the caller after the execution of the rendezvous. Delete 9.5.2(25). [It's included above.] !discussion 9.5.2(24) is the entire definition of rendezvous. There doesn't seem to be any possibility in the above wording of anything happening after the handled_sequence_of_statements but before the accept statement is left. On the other hand, 6.1.1(35.1/4) as modified by AI12-0032 says: For a call to a task entry, the postcondition check is performed before the end of the rendezvous; It's clear that the intent in 6.1.1 is that postcondition checks are done as part of the rendezvous. We have to resolve this conflict somehow. The most sensible thing to do is to expand the definition of rendezvous to include these additional operations. !corrigendum 7.3.2(20/3) @drepl The check is performed on each such part of type @i. @dby The check is performed on each such part of type @i. In the case of a call to a protected operation, the check is performed before the end of the protected action. In the case of a call to a task entry, the check is performed before the end of the rendezvous. !corrigendum 9.5.2(24) @drepl For the execution of an @fa, the @fa, if any, is first evaluated and converted to the entry index subtype; this index value identifies which entry of the family is to be accepted. Further execution of the @fa is then blocked until a caller of the corresponding entry is selected (see 9.5.3), whereupon the @fa, if any, of the @fa is executed, with the formal parameters associated with the corresponding actual parameters of the selected entry call. Upon completion of the @fa, the @fa completes and is left. When an exception is propagated from the @fa of an @fa, the same exception is also raised by the execution of the corresponding @fa. @dby The interaction between a task that calls an entry and an accepting task is called a @i. For the execution of an @fa, the @fa, if any, is first evaluated and converted to the entry index subtype; this index value identifies which entry of the family is to be accepted. Further execution of the @fa is then blocked until a caller of the corresponding entry is selected (see 9.5.3), whereupon the @fa, if any, of the @fa is executed, with the formal parameters associated with the corresponding actual parameters of the selected entry call. Execution of the rendezvous consists of the execution of the @fa, performance of any postcondition or type invariant checks associated with the entry, and any initialization or finalization associated with these checks, as described in 6.1.1 and 7.3.2. After execution of the rendezvous, the @fa completes and is left. The two tasks then proceed independently. When an exception is propagated from the @fa of an @fa, the same exception is also raised by the execution of the corresponding @fa. !corrigendum 9.5.2(25) @ddel The above interaction between a calling task and an accepting task is called a @i. [After a rendezvous, the two tasks continue their execution independently.] !ASIS No ASIS effect. !ACATS test An ACATS C-Test should be created. !appendix From: Randy Brukardt Sent: Friday, January 29, 2016 9:09 PM 6.1.1(35.1/4) says in part: "For a call to a task entry, the postcondition check is performed before the end of the rendezvous; ..." What happens if this check fails? Obviously, Assertion_Error is raised at the point of the check. But then what? Is the exception propagated to the caller as well? (Or, if the check is at the call site, is it propagated to the accept statement as well?) 9.5.2(24) says: "When an exception is propagated from the handled_sequence_of_statements of an accept_statement, the same exception is also raised by the execution of the corresponding entry_call_statement." Clearly, a postcondition check is not in the handled_sequence_of_statement. Indeed, formally, it's checked at the call site (an entry_call_statement in this case) - the wording is "upon successful return". So, from that, the exception should be raised at the call site, but not in the accept statement. But wait: the "end of the rendezvous" wording (plus practical considerations) says that it is evaluated inside of the accept statement (but surely not as part of the handled_sequence_of_statements -- those have already been left in order for us to have "successful return". I have to think that the intent is that the exception is raised in both places (as one would expect for an exception raised "before the end of the rendezvous"). But the actual wording seems to provide no way to deal with exceptions that are raised after the completion of the sequence of statements but before leaving the accept statement. Something seems wrong here. P.S. Ain't it great to try to write test objectives for this text? One asks questions that never would get asked otherwise. Bob must be thrilled. :-) **************************************************************** From: Tucker Taft Sent: Friday, January 29, 2016 9:41 PM I agree that the exception should be raised in both caller and acceptor, and there is no way to handle it inside the accept statement itself. Nothing seems wrong with that... **************************************************************** From: Erhard Ploedereder Sent: Saturday, January 30, 2016 5:59 AM I am all in favor of the "is raised in both places" position. **************************************************************** From: Tullio Vardanega Sent: Saturday, January 30, 2016 7:40 AM Indeed, that is what one would expect. **************************************************************** From: Stephen Michell Sent: Saturday, January 30, 2016 8:04 AM Indeed. **************************************************************** From: Jean-Pierre Rosen Sent: Saturday, January 30, 2016 8:17 AM +1 Nothing else would be consistent. It's just a matter of how to express it. **************************************************************** From: Randy Brukardt Sent: Wednesday, November 9, 2016 8:46 PM I had asked about this in the AI, but we didn't discuss it in Pittsburgh, just approving the AI. In context, one of the wording changes for this AI is: For the execution of an accept_statement, the entry_index, if any, is first evaluated and converted to the entry index subtype; this index value identifies which entry of the family is to be accepted. Further execution of the accept_statement is then blocked until a caller of the corresponding entry is selected (see 9.5.3), whereupon the handled_sequence_of_statements, if any, of the accept_statement is executed, with the formal parameters associated with the corresponding actual parameters of the selected entry call. Execution of the rendezvous consists of the execution of the handled_sequence_of_statements, performance of any postcondition or type invariant checks associated with the entry, and any finalization associated with these checks, as described in 6.1.1 and 7.3.2. After execution of the rendezvous, the accept_statement completes and is left. When an exception is propagated from the execution of a rendezvous, the same exception is also raised by the execution of the corresponding entry_call_statement. The above interaction between a calling task and an accepting task is called a *rendezvous*. [After a rendezvous, the two tasks continue their execution independently.] Note that the first paragraph uses the term "rendezvous", while the second one (unchanged by this AI) actually contains the definition. The proposed change doesn't really make any sense. Either we have to leave "rendezvous" out of the first paragraph, or we have to move the definitional text about the rendezvous before the text that describes the details. The former doesn't work, and the latter is hard to do sensibly. A first try would be to put something like before the current text: The interaction between a task that calls an entry and an accepting task is called a *rendezvous*. But then I don't know what to do with the "after a rendezvous" sentence. And I'm doing Steve's homework for him again, and I'm quite tired of doing that. Thoughts?? **************************************************************** From: Randy Brukardt Sent: Wednesday, November 9, 2016 8:56 PM Also associated with this AI: We changed the new part of the wording to: Execution of the rendezvous consists of the execution of the handled_sequence_of_statements, performance of any postcondition or type invariant checks associated with the entry, and any finalization associated with these checks, as described in 6.1.1 and 7.3.2. because we hated Steve's bringing up 'Old here. The problem is that neither his original wording or the new wording seems to take into account the *initialization* of the implicitly declared 'Old objects. 6.1.1(26/4) says that happens "at the beginning of the accept_statement", which doesn't appear to be part of the rendezvous (based on the above wording - the handled_sequence_of_statements is *inside* of the accept_statement, which is why we're mentioning the finalization in the first place). It's bizarre to initialize and finalize objects in different places, so that doesn't seem to make sense. One would expect that the failure to initialize a 'Old constant would propagate the exception to both places, just like the failure to finalize such a constant would. I'm pretty sure that neither the wording in 6.1.1(26/4) nor that of 9.5.2(24) has that effect. This one doesn't appear finished. Sigh. **************************************************************** From: Tullio Vardanega Sent: Thursday, November 10, 2016 12:23 PM Why don't you add the "after a rendevous" sentence to the one you propose putting before the current text? The interaction between a task that calls an entry and an accepting task is called a *rendezvous*. At the end of that interaction, the two tasks continue their execution independently. In that manner you would first explain the "outside" of the concept and then move on to explain the "inside" of it. **************************************************************** From: Randy Brukardt Sent: Thursday, November 10, 2016 12:52 PM I suppose that would work. I thought that put the unimportant stuff first, but maybe that can't be helped. I'm kinda waiting for Tucker's opinion, since he usually has the solution to all wording problems. :-) **************************************************************** From: Gary Dismukes Sent: Thursday, November 10, 2016 1:07 PM > I suppose that would work. I thought that put the unimportant stuff > first, but maybe that can't be helped. Tullio's suggestion sounds reasonable to me (I had been thinking along the same lines when I saw his message). > I'm kinda waiting for Tucker's opinion, since he usually has the > solution to all wording problems. :-) Tuck is on vacation in Patagonia for the next couple of weeks, so his responsiveness on e-mail may be a bit reduced. ;-) **************************************************************** From: Randy Brukardt Sent: Thursday, November 10, 2016 2:09 PM Ah, yes, I forgot about that. Having talked to him yesterday makes one think that he's around, but of course things change. **************************************************************** From: Tucker Taft Sent: Friday, November 11, 2016 6:09 AM I like tullio's suggestion. **************************************************************** From: Erhard Ploedereder Sent: Saturday, November 12, 2016 3:16 PM I agree with moving it up, but have a mod to suggest ... Let the difition stand by itself. Move the execution sementics, i.e. drop the 2. sentence here and pick up the theme where it is talked about anyway. In the text below, look for the place that starts like this modification: > After execution of the rendezvous, the accept_statement completes and > is left. append: The two tasks then proceed independently. **************************************************************** From: Randy Brukardt Sent: Wednesday, December 21, 2016 10:20 PM > I'm pretty sure that neither the wording in 6.1.1(26/4) nor that of > 9.5.2(24) has that effect. > > This one doesn't appear finished. Sigh. No one ever commented on this, so I'm answering myself for the record. I've concluded now that this actually is a ramification of the new wording. My reasoning is that the declaration of 'Old constants is part of the postcondition check (the check wouldn't work without them). As such, I've answered my question by adding a ramification after 6.1.1(26/4): AARM Ramification: In the case of an accept statement, the constant is declared inside of the rendezvous. It is considered part of the postcondition check, which is part of the rendezvous by definition (see 9.5.2). As this is just an AARM note (and the other change is just editorial, since it is just shuffling around existing text), it isn't necessary to reopen the AI. Yea. **************************************************************** From: Randy Brukardt Sent: Wednesday, December 21, 2016 10:52 PM ... > I've concluded now that this actually is a ramification of > the new wording. And now I've changed my mind. The explicit mention of finalization in the new wording seems to indicate that is special somehow. It would be weird to mention finalization without including the matching initialization somehow. I just did that explicitly in the 9.5.2 wording: ... performance of any postcondition or type invariant checks associated with the entry, and any {initialization or} finalization associated with these checks ... I think the original intent was that this wording implied some sort of order, but that's not really necessary (6.1.1 and 7.3.2 give that), so we can just add two words and declare victory. I've also adjusted the new AARM note accordingly: AARM Ramification: In the case of an accept statement, the constant is declared inside of the rendezvous. It is considered part of the initialization of the postcondition check, which is part of the rendezvous by definition (see 9.5.2). This is still within the range of an Editorial Review change (barely), so we don't need to reopen or have a vote. If someone wants a formal Letter Ballot, however, just ask (always an option for an approved AI) and I'll set one up. **************************************************************** From: Tucker Taft Sent: Wednesday, December 21, 2016 10:52 PM > ... > AARM Ramification: In the case of an accept statement, the constant is > declared inside of the rendezvous. It is considered part of the > postcondition check, which is part of the rendezvous by definition > (see 9.5.2). Your suggestion seems fine to me. ****************************************************************