Re: Simultaneous destructors

Chris Jones wrote:
> Benjamin Smedberg wrote:
>> Or to put it another way, is the following protocol is also
>> race-free and allows multiple dataavailable() calls in a row?
>>
>> protocol Channel {
>> child:
>>     dataavailable();
>>     datadone();
>>     oncanceled()
>> parent:
>>     cancel();
>>     delete();
>>
>> state NORMAL:
>>     send dataavailable goto NORMAL;
>>     send datadone goto DONE;
>>     recv cancel goto CANCELED;
>>
>> state DONE:
>>     recv cancel goto DONE;
>>     recv delete goto __deleted__;
>>
>> state CANCELED:
>>     send dataavailable goto CANCELED;
>>     send datadone goto CANCELED;
>>     send oncanceled goto DONE;
>> };
>>
> 
> No, this is a racy protocol.  BTW, I should have mentioned in the last 
> message that you can run these protocols through IPDL to check whether 
> they pass the race detector.  (I have a script called "ipdlc" that 
> basically does |exec python $srcdir/ipdl.py $*|).
> 
> The reason this protocol is racy is exactly because it specifies that 
> the parent can send an indefinite number of dataavailable() messages in 
> a row.  The child can send cancel() at any time during that indefinitely 
> long sequence of datavailable() messages, and if it does, 
> dataavailable() will arrive at the child in a state where it's not allowed.
> 

Sorry, this isn't quite right.  The protocol is indeed racy per IPDL's 
rules, but the reason it's racy is that it allows the parent's and 
child's states to get out of sync for more than one "transition".  I 
don't see any cases in which a message would arrive in a state where 
it's not allowed.

This to me looks like another reasonable proposal for making it easier 
to write race-free destructors (i.e. by loosening IPDL's 
race-free-protocol rules).  I need to think more carefully about the 
implications of modifying the particular check that makes this protocol 
fail the race detector, though.  The basic problem is that this protocol 
as written would allow the parent's and child's states to get out sync 
for an indefinite number of messages, which doesn't seem desirable in 
general.

Cheers,
Chris