Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*

[Anthony PERARD <anthony.perard@xxxxxxxxxx>]

On Tue, Nov 13, 2018 at 04:10:21PM +0000, Ian Jackson wrote:
> Anthony PERARD writes ("Re: [PATCH v6.1 05/11] libxl_qmp: Implementation of 
> libxl__ev_qmp_*"):
> > On Tue, Nov 13, 2018 at 01:14:30PM +0000, Ian Jackson wrote:
> > But now I realise that `disconnected` would be an illigal state.
> > 
> > What about:
> > 
> >   Precondition: !disconnected
> >   ensure that qmp_ev_callback_writable is been called when needed
> 
> That sounds good, but I think you probably want something more like:
> 
>    On entry: connected/..., but with [the ev_fd] maybe Idle
>    On return: the same state, but with [the ev_fd] Active iff needed
> 
> ?  Or whatever else is true.

Here is a simpler comment that is true:
  !disconnected -> same state

Even if in this function ev_fd is modified, it needs to be Active on
entry, and stay Active on return. But just saying that qmp_state needs
to be different than disconnected is enough.

> > > > +static int qmp_ev_prepare_cmd(libxl__gc *gc,
> > > > +                              libxl__ev_qmp *ev,
> > > > +                              const char *cmd,
> > > > +                              const libxl__json_object *args)
> > > > +{
> > > > +    char *buf = NULL;
> > > 
> > > Missing state comment.
> > 
> > Maybe:
> > 
> >   Precondition: connecting/connected
> 
> Does it change the state to a new one ?  Are the old and new states
> pure states as described in the state table, or are they
> half-transitioned ?  (More on this below.)

They are half-transitioned, here is a new comments:

    on entry: connecting/connected but with `msg` free
    on return: same state but with `msg` set

> > > > +static void qmp_ev_fd_callback(libxl__egc *egc, libxl__ev_fd *ev_fd,
> > > > +                               int fd, short events, short revents)
> > > > +{
> > > 
> > > Missing state comment, although I think the precondition can be easily
> > > inferred from the state of ev_fd and the postcondition varies, but
> > > would still be nice to discuss it.
> > 
> > This function is the main loop function, so almost everything happen in
> > this function. It should not be called directly. So I'm not sure what
> > kind of comment would be usefull here.
> 
> The purpose of the state comments is not just to allow verification
> that call sites are legal.  It is also to allow verification that the
> contents of the function is appropriate.
>
> > Maybe:
> >   Preconditions:
> >     `ev_fd` is Active
> >     this means that `ev` isn't disconnected
> >   Any allowed internal state transition can happen.
> >   A user callback may be called, when that happen, the function should
> >   return.
> 
> You could also write something more discursive.  Maybe
> 
>     On entry, ev_fd is (of course) Active.  The ev_qmp may be in any
>     state where this is permitted.  qmp_ev_fd_callback will do the
>     work necessary to make progress, depending on the current state,
>     and make the appropriate state transitions and callbacks.
> 
> ?

That sounds fine. Thanks.

> > > > +static int qmp_ev_callback_writable(libxl__gc *gc,
> > > > +                                    libxl__ev_qmp *ev, int fd)
> > > > +    /* connected -> waiting_reply
> > > > +     * the state isn't change otherwise. */
> > > > +{
> > > 
> > > I don't know what `otherwise' means.  Maybe you mean all other states
> > > are legal and remain unchanged ?  But that does not seem to be
> > > likely.  Presumably disconnected is ruled out, at least.
> > 
> > If for some random reason this function is called with the state
> > disconnected, it would just return. Unless the state is disconnecting
> > and tx_buf haven't been cleared yet.
> > 
> > `Otherwise` would be the `otherwise` of haskell, or the `default` of a
> > switch case in C.
> > 
> > So a different comment could be:
> >   Precondition:
> >     !disconnected
> 
> You are contradicting yourself.  You are both stating that this
> function may be called in state disconnected, and that it may not.
> 
> But assuming that what you write here in your proposed comment is
> true, ...
> 
> >   State transition
> >     connected -> waiting_reply
> >     * -> state unchange
> >     on error: disconnected
> >   The state of the transmiting buffer will be changed.
> 
> ... this looks good.

Do I need to say here and everywhere else that on error the new state
isn't really disconnected, and that the ev_qmp needs to be cleaned?
On one hand, saying that the new state is disconnected means that the
ev_qmp functions that only deal with !disconnected, but on the other,
the caller still need to call _dispose.

> > > > +static int qmp_ev_callback_readable(libxl__egc *egc,
> > > > +                                    libxl__ev_qmp *ev, int fd)
> > > > +    /* on error: * -> disconnected */
> > > 
> > > Precondition ?  And on non-error ?
> > 
> > Here is a more complete comment:
> >   Precondition:
> >     !disconnected
> >   State transition:
> >     Only the state of the receiving buffer is change on success
> >     on error: disconnected
> 
> That's good.  I would have been happy with:
> 
>      !disconnected -> same state (with rx buffer updated)
>      on error -> disconnected

I'll go with that, that looks better and easier to read.

Thanks,

-- 
Anthony PERARD

_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/xen-devel