Re: avoiding races in IPDL protocols

Benjamin Smedberg wrote:
> On 7/15/09 2:16 AM, Jason Duell wrote:
> 
>> 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).
> 
> Yeah, that defeats the point of having a protocol state system.
> 

Not really.  It's a question of error handling --- no races would have
been tolerated in any case.  The question is whether races are dynamic
errors (boo!), static errors of the C++ implementation (meh), or static
errors of the IPDL spec (yay!).

>> 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.
> 
> In any case I think IPDL ought to statically verify that there are no
> illegal race conditions between async messages, like #3.
> 

I certainly agree.  The question is when or at what level this is
checked.  The original plan, static analysis of C++ code to build models
for checking, is obviously inferior to good language features that avoid
this issue altogether.

Cheers,
Chris