avoiding races in IPDL protocols

Sorry, this post may be very esoteric to anyone unfamiliar with IPDL
(the protocol/messaging layer we're using between processes in
electrolysis).

So we're using a contract-based scheme, in which the parent/child
specify both which types of messages can be received (and in which
directions), and state transition rules that say which messages are
allowed in a given state (and the state change that occurs, if any):
for an overview, see

    https://wiki.mozilla.org/IPDL/Getting_started

The goal here is to allow automatic detection of illegal message
traffic, so that we can take pre-emptive action (for now, killing the
child process and emitting an error message) rather than wander off
into unforeseen erroneous logic where we're receiving and trying to
process messages in states that weren't designed to handle them.  This
is basically the "contract-based channels" used in the singularity
project:

   http://research.microsoft.com/apps/pubs/?id=69431 (section 2.2)

So: I've noticed an issue with this approach that I haven't found a
good answer for yet:  what happens if/when there's a state which
allows traffic in either direction, and simultaneous messages are sent
in either direction, causing incompatible transitions?  For example,
if we have

state START:
    recv FooMsg goto FOO;
    send BarMsg goto BAR;

state FOO:
    recv Foo2Msg goto MORE_FOO;

state BAR:
    recv Bar2Msg goto MORE_BAR;

In other words, the receipt of a FOO takes one down a state transition
path that is concerned only with foo-ish things, whereas a BAR takes
one down a bar-barous path.  Once you've start down one path, receipt
of the other kind of msg wouldn't make sense, so it would be an error.

Alas, what if we're in START and a FooMsg is sent from one side just
as a BarMsg is issued from the other?  We've got a race, and it will
take us off the legal set of state transitions.   (In this case, it
would end either way with a crash, because the state FOO would barf
when it gets the "BarMsg", or BAR when it gets FooMsg).

The general computer science problem here is:  we're using a state-
transition model that assumes a series of atomic, global events and
state changes, but we're actually on a networked system with
distributed events and no global clock.  As near as I can tell, we've
got the following potential solutions within IPDL:

1) Make the programmer anticipate race conditions, and allow (and
handle) BarMsg when in state FOO.  This might, alas, requires a lot of
subtle thinking to get right (when we were hoping IPDL would make
safely writing protocols fairly trivial).

2)  make states unidirectional (only send or recv).  If any particular
state (including START) can only support messages in one direction,
than we avoid races by making the conditions for them impossible.

3) Possibly loosen #2 to allow states with bidirectional traffic, but
only if states that follow them can handle all possible race condition
messages that might occur (the IPDL compiler should be able to figure
these out).   For example, a state machine for a TCP socket could go
through the various initialization steps, which all fit into #2's
rules, then be in a CONNECTED state in which bidirectional send/recv
is allowed (with send/recv msgs just maintaining the CONNECTED state),
then a "close" msg from either direction could move it into a SHUTDOWN
state in which any stray send/recvs still in transit get ignored.

I don't have enough of an idea of the communication patterns needed by
electrolysis to know where in these options we'd fit.

As near as I can tell from their papers, the Singularity folks are
using something like #2, and they seem to have implemented a whole
operating system with it.  So perhaps things aren't so bad.  See

    http://research.microsoft.com/apps/pubs/default.aspx?id=67482

for some (alas fairly minimal) examples.

The classic way of doing things, of course, is to have each end of the
protocol be its own state machine, and have sends and recvs of
messages be separate events happening to different state machines.   I
don't know the guts or theory behind IPDL to know if autogenerating
that sort of setup is feasible.  On the plus side, our "network" is
reliable, in-order, and low latency, so we avoid a *lot* of complexity
there.

It would be great to hear any comments from folks who've got any
insight on this stuff, especially on electrolysis's likely
communication patterns.

I'm cross-posting this to dev.tech.network, but let's keep the
conversation in dev.tech.dom, because that's apparently where most
electrolysis discussions are happening.

Jason