Re: Asynchronous Transfer of Control

[dewar@merv.cs.nyu.edu (Robert Dewar)]

James Squire worries about me noting that abort completion points are
still important if annex D is implemented, when Tuck said they are not.

In fact these statements are not inconsistent, even though they appear
to be. What Tuck was saying is that if you are worried about the immediacy
of abort, then the issue of abort completion points is not important,
since it is annex D that describes the latency of aborts.

What I was saying is that if you are concerned with the exact set of
events that can occur, in terms of reasoning formally about state, then
abort completion points are important.
What an abort completion point promises is that if a task is aborted, then
it is NEVER the case that a statement after this point is executed, even
if the latency guaranteed in annex D would permit such an execution sequence.

It is quite possible to construct a test where this reasoning makes a
difference to the invariants of the program state after the abort has
taken place.