Re: Simultaneous destructors

Benjamin Smedberg wrote:
> On 11/11/09 10:26 AM, Benjamin Smedberg wrote:
> 
>> I slightly prefer the divergent-path approach rather than the discard
>> approach, for one main reason: it means that we don't have to implement
>> special handling for actors which have already been "destructed" but are
>> still receiving messages.
>>
>> I don't think my opinion is strong enough to *insist* on the divergent-path
>> approach, though. If we do go with the discard-bad-messages approach, I'd
>> like a very solid approach torwards zombie actor IDs.
>>
>> In any case, I'm also concerned with getting a theoretically sound approach
>> implemented for plugin destructor races for 1.9.3.
> 
> I discovered another edge-case that needs consideration: when you pass an
> actor as a parameter, it must be in a state that does not race with destruction.
> 

This is a great point, I thought about this a while back.  It's 
checkable (a finite-state problem modulo RPC stacks), but there are two 
issues (i) we need more powerful machinery, in the form of the SPIN 
model checker; and (ii) the way we've been passing actors around so far, 
Msg(fooActor), will result in a 100% false-positive rate because 
|fooActor| syntax means "fooActor may be in any state."  We need to 
start passing actors as |fooActor:STATE| before cross-protocol checks 
would be useful.  (That feature is slightly broken in IPDL right now, 
but easy to fix.)

Cheers,
Chris