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

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

!standard 6.1.1(35.1/4)          16-11-09 AI12-0193-1/03
!standard 9.5.2(24)
!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
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
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.
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.
[Editor's note: It's a little weird that the term "rendezvous", which is defined in the following paragraph, is used in this one. I didn't see a simple fix.]
!discussion
9.5.4(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.4(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:
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 handled_sequence_of_statements of an accept_statement, 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.
!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.

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

Questions? Ask the ACAA Technical Agent