[e-lang] Non-local Exits vs Defensive Consistency - David Hopwood

[Mark Miller]

This is the first of a series of messages discussing how various
non-local exit constructs in E and Joe-E make it hard-to-impossible
for the programmer to write defensively consistent code.

Because I "jumped the gun" -- starting a private discussion of the
following preview message sent by David Hopwood -- the messages on the
resulting thread were also sent around privately. However, everyone
who's posted on this thread has given me permission to repost to
e-lang, so that the discussion can continue here.

In reposting these messages, I will give them all the subject line
"Non-local Exits vs Defensive Consistency" appended with the original
author.


---------- Forwarded message ----------
From: David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
Date: Jan 24, 2007 5:32 PM
Subject: Re: Speculative Concurrency for E?
To: Mark Miller <erights at gmail.com>


Mark Miller wrote:
> Hi David,
>
> I remain curious about your thoughts on speculative concurrency for E.

I got a bit distracted over Christmas and new year, but I intend to post
the notes I have over the next week or so. Here is a summary.


====
Transactional Event Loop Concurrency

This is a summary of a series of articles proposing to add support for
lightweight
transactions to E, Oz-E, and other security-oriented event-loop
languages. (I wrote
it originally as a single article, but it got ridiculously long.)

Here are the arguments I will make:

Non-local exits, with the semantics used in most languages including E, make it
unreasonably difficult to ensure defensive consistency or correctness.

MarkM's thesis discusses this problem, but in my opinion the fixes
suggested there
are not likely to work well enough to allow sufficient confidence in
the defensive
consistency of large bodies of code, or are too inefficient to be practical.

What is needed to make defensively consistent programming tractable in
the presence
of non-local exits, is that "only calls that exit normally have significant
side-effects". I will call this the Very Strong Exit Guarantee (since it is
stronger than what the C++ community calls the "Strong Exception Guarantee").

It is possible, and efficiently implementable, for an event-loop
language to ensure
the Very Strong Exit Guarantee automatically (except for calls to the operating
system or an external library, where this guarantee cannot be supported by the
OS or library itself). No effort is required from the application
programmer, and
no application program errors can cause the guarantee to be violated.

In an event-loop language, the effect of the Very Strong Exit Guarantee is that
each turn becomes a lightweight (Atomic, Consistent, serializably Isolated)
transaction. Transactions are nestable within a turn, and allow any significant
effect (including pending message sends to other vats) to be rolled back to the
start of the transaction. Code does not need to be written to do
anything special
to cooperate with transactions.

It is, however, necessary to use a *pure* event-loop model for this to work.
E currently has some synchronous I/O facilities, which would have to be reviewed
and possibly removed.

There has to be an "escape hatch" to allow effects that should not be considered
significant (i.e. should not be rolled back), such as debugging
output. It is not
sufficient to limit this to a fixed set of functions. I discuss how to
ensure that
these effects can be easily reviewed to check that they don't pose a
security risk,
and don't violate a programmer's mental model of what effects are significant.

The changes needed to exception and escape semantics will be described
in detail.
The proposed semantics is based on Prolog-style backtracking, so it is not a
fundamentally new idea (indeed, it is mentioned as a possible behaviour for
exceptions in a paper from 1975!) It is completely compatible with distribution
among non-mutually-reliant machines; the backtracking is only local to a vat.

The ability to roll back side effects makes it possible to support
safe, consistent
termination of uncooperative code. This can be used to improve resistance to DoS
attacks (although there are still unsolved problems in that area).

In addition to transactions, we get an increase in language
expressiveness slightly
greater than adding "don't know" nondeterministic choice (the
relational model from
CTM Chapter 9, a.k.a. 'amb'), if the language did not already support it.

Despite the increase in expressiveness, the resulting language is
easier to reason
about.

This need to use catch blocks to clean up after exceptions is greatly reduced.
Although this is usually not a large amount of code, less code is
certainly better,
and programs become a little simpler and easier to both read and write (even if
defensive consistency were not an issue).

Removal of synchronous I/O from the E libraries is obviously an
incompatible change.
While the changes to exceptions and escapes are also technically incompatible, I
believe almost all existing E code that does not use synchronous I/O
is likely to
behave correctly (and a few latent bugs may be fixed). I propose a convention to
be used to replace code that relied on non-local exit from a call with visible
effects.

The main disadvantage is greater memory usage during a turn. I discuss how this
might require some algorithms to be written differently.

For free (and without the overhead of full checkpointing), we get some nice
debugging facilities such as reverse execution to the start of a turn. This also
gives us the ability to reexecute the turn with tracing and other possibly
expensive debugging features switched on, as though we could predict in advance
that an exception is going to be thrown.

Depending on the implementation, we can also get other goodies such as
cheap support
for soft real-time concurrent GC, and soft real-time concurrent checkpointing.

Implementation will be discussed in detail. Essentially it amounts to
implementing
backtracking search, for which efficient techniques are known from existing
languages, especially Prolog. The run-time overhead of a suggested
implementation
using "undo trails" is similar to that of write barriers used for concurrent GC
(I estimate no more than 20% for typical imperative programs, and less
for mostly
functional programs). This is an order of magnitude better than other published
approaches to implementing transactions used for Software Transactional Memory
(albeit that the latter allows a more general kind of transaction). By taking
advantage of restrictions imposed by event-loop concurrency, the implementation
can be much simpler than any STM implementation.

Finally, I throw out some more speculative ideas for language features, such as
"vat metaprograms" and "first-class checkpoints", which are not part of this
proposal but might be complementary to it.

--
David Hopwood