public void terminated(Pipe pipe_) 
    {
        //  Drop the reference to the deallocated pipe.
        assert (pipe == pipe_ || terminating_pipes.contains (pipe_));
        
        if (pipe == pipe_)
            // If this is our current pipe, remove it
            pipe = null;
        else
            // Remove the pipe from the detached pipes set
            terminating_pipes.remove (pipe_);
        
        //  If we are waiting for pending messages to be sent, at this point
        //  we are sure that there will be no more messages and we can proceed
        //  with termination safely.
        if (pending && pipe == null && terminating_pipes.size () == 0)
            proceed_with_term ();
    }