CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2009/11/03 05:59:07 1.2
+++ ai05s/ai05-0145-2.txt 2009/12/29 05:54:24 1.3
@@ -1,6 +1,7 @@
-!standard 11.5 (00) 09-11-02 AI05-0145-2/02
-!standard 11.4.1 (10)
+!standard 13.3.2 (00) 09-12-28 AI05-0145-2/03
!class amendment 09-06-12
+!status Amendment 201Z 09-12-28
+!status ARG Approved 11-0-1 09-11-07
!status work item 09-06-12
!status received 09-06-12
!priority Medium
@@ -40,14 +41,14 @@
!proposal
Using the aspect_specification syntax, we propose to allow the
-specification of pre/postconditions for subprograms and entries.
-The aspects Pre and Post are used for this purpose. In addition, for
+specification of pre/postconditions for subprograms and entries.
+The aspects Pre and Post are used for this purpose. In addition, for
primitive subprograms of tagged types, the aspects Pre'Class and
-Post'Class are also available. These aspects are inherited by the
+Post'Class are also available. These aspects are inherited by the
corresponding primitive subprogram of types descended from the original
tagged type. When multiple preconditions apply to a subprogram, they are
"or"ed together (that is, if any of the preconditions is satisfied, the
-overall precondition is satisfied). When multiple postconditions apply
+overall precondition is satisfied). When multiple postconditions apply
to a subprogram, they are "and"ed together (that is, all of the
postconditions must be satisfied for the overall postcondition is
satisfied).
@@ -55,32 +56,6 @@
!wording
-Modify 3.9.3(1.1/2):
-
- abstract_subprogram_declaration :=
- subprogram_specification IS ABSTRACT
- [aspect_specification];
-
-Modify 6.1(2/2):
-
- subprogram_declaration ::=
- [overriding_indicator]
- subprogram_specification
- [aspect_specification]
-
-Modify 6.7(2/2):
-
- null_procedure_declaration ::=
- procedure_specification IS NULL
- [aspect_specification];
-
-Modify 9.5.2(2/2):
-
- entry_declaration ::=
- [overriding_indicator]
- ENTRY defining_identifier [(discrete_subtype_definition)] parameter_profile
- [aspect_specification];
-
Add a new section:
13.3.2 Preconditions and Postconditions
@@ -93,11 +68,11 @@
expression.*
Name Resolution
-
+
The expected type for a precondition or postcondition expression is
- the predefined type Boolean. Within a postcondition expression of a
+ the predefined type Boolean. Within a postcondition expression of a
function, the attribute Result is defined for the function, yielding
- the value returned by the function. Within a postcondition expression
+ the value returned by the function. Within a postcondition expression
of a subprogram or entry with at least one IN OUT formal parameter of a
nonlimited type, the attribute Old is defined for each such formal
parameter, yielding the value of the formal parameter at the beginning
@@ -105,29 +80,29 @@
Within the expression for a Pre'Class or Post'Class aspect for a
primitive subprogram of a tagged type T, a name that denotes a formal
- parameter of type T is converted to T'Class. Similarly, a name that
+ parameter of type T is converted to T'Class. Similarly, a name that
denotes a formal access parameter of type access-to-T is converted to
access-to-T'Class. Finally, if the subprogram is a function returning
T or access T, the Result attribute is converted to T'Class or
- access-to-T'Class, respectively. [Redundant: This ensures the
+ access-to-T'Class, respectively. [Redundant: This ensures the
expression is well-defined for a primitive subprogram of a type
descended from T.]
-
+
Legality Rules
-
+
The Pre or Post aspect shall not be specified for an abstract
subprogram. [Redundant: Only the Pre'Class and Post'Class aspects may
be specified for such a subprogram.]
Static Semantics
-
+
If a Pre'Class or Post'Class aspect is specified for a primitive
- subprogram of a tagged type T, then the associated precondition
- expression also applies to the corresponding primitive subprogram of
- each descendant of T.
-
+ subprogram of a tagged type T, then the associated expression also
+ applies to the corresponding primitive subprogram of each descendant
+ of T.
+
Dynamic Semantics
-
+
If one or more precondition expressions apply to a subprogram or
entry, and the Assertion_Policy in effect at the point of the
subprogram or entry declaration is Check, then upon a call of the
@@ -135,14 +110,14 @@
precondition check is performed. This consists of the evaluation of
the precondition expressions that apply to the subprogram or entry. If
and only if all the precondition expressions evaluate to False, then
- Ada.Assertions.Assertion_Error is raised. The order of performing the
+ Ada.Assertions.Assertion_Error is raised. The order of performing the
checks is not specified, and if any of the precondition expressions
evaluate to True, it is not specified whether the other precondition
expressions are checked. It is not specified whether any check for
elaboration of the subprogram body is performed before or after the
- precondition check. It is not specified whether in a call on a
+ precondition check. It is not specified whether in a call on a
protected operation, the check is performed before or after starting
- the protected action. For an entry call, the check is performed prior
+ the protected action. For an entry call, the check is performed prior
to checking whether the entry is open.
If one or more postcondition expressions apply to a subprogram or
@@ -151,7 +126,7 @@
from a call of the subprogram or entry, prior to copying back any
by-copy IN OUT or OUT parameters, a postcondition check is performed.
This consists of the evaluation of the postcondition expressions that
- apply to the subprogram or entry. If any of the the postcondition
+ apply to the subprogram or entry. If any of the the postcondition
expressions evaluate to False, then Ada.Assertions.Assertion_Error is
raised. The order of performing the checks is not specified, and if
one of them evaluates to False, it is not specified whether the others
@@ -160,26 +135,26 @@
before or after the postcondition check.
If a precondition or postcondition check fails, the exception is
- raised at the point of the call. [Redundant: The exception cannot
+ raised at the point of the call. [Redundant: The exception cannot
be handled inside the called subprogram.]
For a dispatching call or a call via an access-to-subprogram value,
the precondition or postcondition check performed is determined by the
- subprogram actually invoked. [Redundant: Note that for a dispatching
+ subprogram actually invoked. [Redundant: Note that for a dispatching
call, if there is a Pre'Class aspect that applies to the subprogram
named in the call, then if the precondition expression for that aspect
- evaluates to True, the precondition check for the call will succeed.
+ evaluates to True, the precondition check for the call will succeed.]
- [Redundant: If the Assertion_Policy in effect at the point of a
+ If the Assertion_Policy in effect at the point of a
subprogram or entry declaration is Ignore, then no precondition or
- postcondition check is performed on a call on that subprogram or entry.]
+ postcondition check is performed on a call on that subprogram or entry.
!discussion
-This is based on AI05-145-1. The Pre/Post aspects are specified using
-the aspect_specification syntax defined in AI05-0183-1. There is no
-message associated with the failure of a precondition or postcondition
-check: it was deemed that these annotations are intended for
+This is based on the previous alternative AI05-0145-1. The Pre/Post aspects
+are specified using the aspect_specification syntax defined in AI05-0183-1.
+There is no message associated with the failure of a precondition or
+postcondition check: it was deemed that these annotations are intended for
verification, and that for debugging purposes the Assert pragma is
sufficient.
@@ -236,5 +211,184 @@
!appendix
+From: Erhard Ploedereder
+Sent: Saturday, November 7, 2009 11:42 AM
+
+I still have 2 issues with AI-145-2.
+
+I still am bothered about the race conditions on preconditions of protected
+actions. Normally, I assume that I can use the "usual" Floyd style of
+propagating the Pre across the code of the subprogram to determine what holds at
+any given point.
+
+Here, the Pre might have been checked ages ago, when I was blocked, and need no
+longer hold when I am unblocked. The Floyd-style arguing about the code is not
+valid any more. And I do not see how I can make it valid again, short of almost
+unreasonable restrictions on the nature of Pre. See also the 2. issue. Local
+state may be very important. It is clear that references to shared global state
+in Pre will introduce general data race conditions, but that is well known and
+unavoidable short of drastic restrictions on Pre. I don't buy the argument that,
+if we cannot prevent this general problem, it is not worth to solve the specific
+problem.
+
+There are various implementation models possible:
+ a) check Pre as part of the call: has the above race condition and consequences
+ b) check after the barrier check: does not "protect" the barrier check,
+ but everything else. Satisfies Floyd.
+ c) check before the barrier check and also as part of being unblocked:
+ "protects" everything, satisfies Floyd, costs a bit more.
+
+In a safe language, I would expect b) or c), certainly not a) as currently
+proposed.
+
+----
+
+The other comment that I have is that the difference between subprograms
+operating on any (other) composite data and protected operations is striking.
+Just because "self" is not a parameter of the subprogram (but is for primitive
+ops), direct access to the local state of protected objects is unavailable,
+while access to local state of any other object is available in Pre. Such access
+is necessary, if timed logic gets involved, e.g., "must have been initialized by
+a call on xyz" presumably needs info from the local state to be an executable
+Pre.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, November 7, 2009 3:14 PM
+
+...
+> There are various implementation models possible:
+> a) check Pre as part of the call: has the above race condition and
+> consequences
+> b) check after the barrier check: does not "protect" the barrier check,
+> but everything else. Satisfies Floyd.
+> c) check before the barrier check and also as part of being unblocked:
+> "protects" everything, satisfies Floyd, costs a bit more.
+>
+> In a safe language, I would expect b) or c), certainly not a) as
+> currently proposed.
+
+Yes, I see what you mean.
+
+> ----
+>
+> The other comment that I have is that the difference between
+> subprograms operating on any (other) composite data and protected
+> operations is striking. Just because "self" is not a parameter of the
+> subprogram (but is for primitive ops), direct access to the local
+> state of protected objects is unavailable, while access to local state
+> of any other object is available in Pre. Such access is necessary, if
+> timed logic gets involved, e.g., "must have been initialized by a call
+> on xyz" presumably needs info from the local state to be an executable Pre.
+
+I don't think that's right. The type has to be private, so Pre has to refer to
+some accessor functions if it wants to depend on the innards. So protected
+types are no different, here, as far as I can see.
+
+P.S. I'm sitting right next to you as I write this. ;-)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, November 8, 2009 9:52 PM
+
+I can sympathize with the desire of checking preconditions both before and after
+any queuing, but if it makes a difference I believe that it is probably a "bad"
+precondition. How is the caller supposed to know if something *will be* true by
+the time the entry body/accept statement finally gets executed?
+
+From the entry body's point of view, any part of the conceptual Floyd-ish
+precondition that depends on the state of the object should really be part of
+the entry barrier. The only part of the precondition that should be enforced on
+the caller is the part that they have control over, namely the value of their
+parameters.
+
+It would be helpful if you could give an example where a "good"
+precondition can legitimately depend on the variable state of the protected
+object. That might be more convincing that appealing to Floyd here, since I
+don't think he was talking about concurrent data structures.
+
+As far as the specific issue of referening the local state, the
+pre/postconditions can only reference visible entities (since they are on the
+spec, and are supposed to be meaningful to the caller), but they could call
+visible protected functions. Again, though, if the protected function is
+returning a value that could change between the time the call is made and the
+entry body is executed, then it probably shouldn't be included in a
+precondition, or else there is clearly a race condition.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, December 28, 2009 11:42 PM
+
+...
+> I still am bothered about the race conditions on preconditions of
+> protected actions.
+> Normally, I assume that I can use the "usual" Floyd style of
+> propagating the Pre across the code of the subprogram to determine
+> what holds at any given point.
+
+I don't think this works in Ada, in the general case. Ada expressions can easily
+depend on functions with side-effects, on functions that modify their parameters
+(think "Random"), on global variables, on aliased objects that can be modified
+by other tasks, constants that aren't really constant, and the like. About all
+you can say for sure about an arbitrary precondition expression is that it was
+true when it was checked (at the point of the call). You most certainly cannot
+assume that it holds throughout the subprogram.
+
+Note that this has nothing whatsoever to do with protected objects; it is a
+"feature" of Ada expressions that becomes a "feature" of Assertions,
+preconditions, invariants, and anything else that you like.
+
+A fine example of that is the Claw "precondition" of object validity. For
+instance, in the following (written using our new syntax rather than the textual
+comments actually used in Claw):
+
+ procedure Move (Window : in out Root_Window_Type; Position : in Point_Type)
+ with Pre'Class => Is_Valid (Window);
+
+The problem is that the user of the Claw application can close a window
+asynchronously to the application code. So simply putting
+ if Is_Valid (Window) then
+ Move (Window, Top_Left);
+ end if;
+is insufficient to prevent Not_Valid_Error from happening. (Indeed, there is no
+way to prevent it; handling the exception is the only alternative.) [Yes, the
+state changes are synchronized to prevent dangerous race conditions related to
+the actual state change; we tried to prevent higher level race conditions, but
+that simply made responsiveness terrible and often caused deadlocks in typical
+code.]
+
+> Here, the Pre might have been checked ages ago, when I was blocked,
+> and need no longer hold when I am unblocked. The Floyd-style arguing
+> about the code is not valid any more. And I do not see how I can make
+> it valid again, short of almost unreasonable restrictions on the
+> nature of Pre.
+
+The *only* way to be able to argue *anything* about Pre *anywhere* is to put
+"almost unreasonable restrictions" on the nature of Pre. Pretty much the only
+Pre that can be guaranteed to work is one that could have been used in a
+function that has Global In/Global Out equal to null -- this is substantially
+stronger than the restrictions of a Pure function. Anything else will be at risk
+of becoming untrue because of something some other task does (even in the
+supposedly protected code).
+
+For instance, the problem with the Claw Is_Valid function is that other tasks
+have access to part of the Window object, and thus can change the state of that
+object. That problem will happen for any object that has a portion that is
+potentially shared with another task (which, of course, includes the variable
+parts of all protected objects).
+
+One hopes that there will exist tools that detect and warn about "bad"
+preconditions (and all of the other sorts of contracts that we're planning to
+add). Without that, it will be very hard to reason about anything.
+
+My primary point here is that your concerns about protected objects are just the
+tip of the iceberg. If you write "good" preconditions, there won't be any
+problem with using Floyd, but if the preconditions can change (and that is true
+for many preconditions that might be written in a real program), they're
+essentially meaningless. The blocking of the task at the barrier might make this
+problem somewhat more visible, but it is hardly worth worrying about on its own.
****************************************************************
Questions? Ask the ACAA Technical Agent