Re: Simultaneous destructors

Chris Jones wrote:
> Benjamin Smedberg wrote:
>> I don't understand how the extra state helps, at least if there are any
>> async messages involved:
>>
>> protocol Channel {
>>   child: dataavailable();
>>   child: datadone()
>>   parent: cancel();
>>   parent: delete();
>>
>>   state NORMAL:
>>     send dataavailable goto NORMAL;
>>     send datadone goto DYING;
>>     recv cancel goto DYING;
>>
>>   state DYING:
>>     send delete;
>> }
>>
> 
> This protocol would fail type-checking because it has a race condition 
> in the NORMAL state, datadone vs. cancel.  The protocol is stateful, and 
> datadone/cancel don't adhere to the Diamond Rule.
> 

I was remiss in not showing how the races could be avoided in this 
example.  The way to avoid them is a two-phase delete like what I 
described in an earlier post.  For this protocol, it would look like


protocol Channel {
child:
     dataavailable();
     datadone();  NOTREACHED(); //<--ignore this
parent:
     moar();
     cancel();
     delete();

state NORMAL:
     send dataavailable goto SENTDATA;
     send datadone goto DONE;
     recv cancel goto CANCELED;

state SENTDATA:
     recv moar goto NORMAL;
     recv cancel goto DEAD;

state DONE:
     recv cancel goto DEAD;

state CANCELED:
     send dataavailable goto DEAD;
     send datadone goto DEAD;

state DEAD:
     recv delete goto __deleted__;

// IPDL would generate this "state" automatically, so it can be ignored
state __deleted__:  send NOTREACHED goto __deleted__;
};


Speaking generally, this protocol allows the child to send |cancel()| 
and the parent to send |datadone()| (the parent's equivalent to cancel() 
wrt to deletion) at any time.

If the child sends cancel(), then a delete sequence is initiated, 
finished by the child sending the actual |delete()| message back to the 
parent.  The tricky part here is that if the child sends an "abrupt 
cancel", a cancel from the NORMAL state, then the child must wait for 
the parent to ack the cancel with datavailable or datadone before 
sending the actual |delete()| message.

Likewise, if the parent sends |datadone()|, a delete sequence is also 
initiated.  Like |cancel()| sent from the NORMAL state, if |datadone()| 
is sent from NORMAL, then the child must ack with |cancel()| before it 
can send |delete()|.

The substantial modification from the original protocol is the addition 
of the SENTDATA state and the "moar()" message.  This captures the 
decision a child makes between wanting more data vs. cancelling.  It 
prevents two dataavailable() messages from being sent in a row.  This 
might seem strange, but we'll need this feature when the child and 
parent are transferring network data through two shmem buffers.  The 
|moar()| message is where the child would send back to the parent a 
handle to the "free" shmem buffer (i.e., the one it's not currently 
using).  (The parent would then fill that buffer and transfer it back to 
the child using |datavailable()|).

I agree that two-phase deletion is complicated, but (i) it's the price 
to be paid for race-free deletion; (ii) two-phase deletion is a kind of 
"IPDL pattern", like "empty subprotocols", that can be documented and 
copied by other protocols.

The alternative is, as I mentioned in the previous message, allowing 
|delete()| messages to be inherently racy even in stateful protocols, 
having IPDL detect when |delete()| indeed races, and generating special 
code to handle the races.  Personally I prefer expending the effort to 
declare non-racy protocols, like the one above.

Cheers,
Chris