Version 1.6 of ai12s/ai12-0193-1.txt

Unformatted version of ai12s/ai12-0193-1.txt version 1.6
Other versions for file ai12s/ai12-0193-1.txt

!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<rendezvous>.
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)
Replace the paragraph:
The check is performed on each such part of type T.
by:
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.
!corrigendum 9.5.2(24)
Replace the paragraph:
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.
by:
The interaction between a task that calls an entry and an accepting task is called a rendezvous.
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 handled_sequence_of_statements of an accept_statement, the same exception is also raised by the execution of the corresponding entry_call_statement.
!corrigendum 9.5.2(25)
Delete the paragraph:
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.]
!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.
<Grumble>

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.

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

Questions? Ask the ACAA Technical Agent