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

[Ian Jackson <ian.jackson@xxxxxxxxxx>]

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:
> > This one is probably an asisstant for transitioning between states so
> > the pre- and post-conditions may not be pure.  Whatever it is should
> > be documented...
> 
> It's hard to document the state transition of a function that doesn't
> care of the current state when the function is called, and will attempt
> to figure out the current state to find out if a function `writable`
> needs to be called later.

Then write that down rather than just saying nothing!


I think it might be useful to paste in again a thing I wrote on the
15th of October:

  Again, I asked for more internal documentation about the legal states
  etc.  I will have to read it in detail again I'm afraid after that is
  done.

  The reason I ask for this is that this is a complicated and
  substantial pile of code.  It's not sensible for anyone to try to hold
  it in their head at once - we will make mistakes.  And it should be
  possbile to modify it without reading all of it.

  So, it should be possible for anyone to:

   * Look only at the summary internal architecture state machine
     comments and so on, and confirm to themselves that this is a
     sensible design and that all the possible states are represented
     and that the interlocking states of the detailed variables are
     both sufficient, and of manageable complexity.

   * Read any small fragment of code and see that transforms legal
     states into other legal states, by reference to the above.

  Right now this is not really possible.  I look at things like this:

I want someone who reads one of these functions to be able to see that
it is correct, without having to go and look at its call sites to
understand what it needs to promise.  And of course from my own point
of view, I won't want to reverse engineer the intention from the code.
It's OK if it is obvious but in this case I think it is usually
un-obvious.

These kind of explicitly coded state machines are indeed tiresome,
compared to synchronous code where the state is encoded in the program
counter (ie, the progress through the single function).  It more easy
to make mistakes where a variable is not set or has the wrong value,
because (compared to a synchronous function) the sequencing is
obscured.

Unfortunately we do not have a workable coroutines system, and
multithreading is even worse for writing bugs.  (Nontrivial
multithreaded programs are almost always full of race bugs.)  So we
are left with doing it this way, and we have to mitigate the risk of
bugs a different way: in this case, by writing down more explicitly in
comments things that could be easily inferred from reading the code if
the code were a single function.


One way to test to see if you have succeeded is as follows: can you
prove that each function is correct, in isolation, without having to
read the body of any other function ?  You are only allowed to rely on
the struct definition, and the formal state definitions, and the doc
comments for your function and everything you call.

That is obviously not possible if there is nothing saying what state
the function is supposed to leave things in.  Nor is it possible to
show that the function is correct unless either it tolerates any (even
impure) input state, or there is a comment saying what input states
it is supposed to deal with.


> Are all those comments good enough? Also sometime the internal state
> isn't fully changed in one go, and the transition could happen in
> several functions (I think). Do we needs states like disconnecting,
> connectinging, ... ? with a comment that say that the value of the
> internal variables can be one of before or after the state transition.

This is what I meant by `impure' states below.  I don't think you want
to write them in your state table, but you can describe them in
comments as `connected, but with rx_fd not Active' or some such.
`But' and `but maybe' are good phrasings for this.


> 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.

> > > +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.)

> > > +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.

?

> > > +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.

> > > +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


> > > +static int qmp_ev_parse_error_messages(libxl__egc *egc,
> > > +                                       libxl__ev_qmp *ev,
> > > +                                       const libxl__json_object *resp)
> > > +{
> > 
> > This doesn't touch the state I think.  Should perhaps be mentioned in
> > a comment.
> 
> The only thing that this function use is set by a user (of
> libxl__ev_qmp): ev->domid. But I guess that comment would do:
> 
>   no state change

Yes.


> Next time I'll write one BIG function, and there will be less of those
> comments to write :).

Hah.


Thanks,
Ian.

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