Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
Anthony PERARD writes ("Re: [PATCH v6.1 05/11] libxl_qmp: Implementation of
libxl__ev_qmp_*"):
> The current implementation already cleanup the broken state before the
> control is passed outside ev_qmp implementation. That result in the Idle
> public state. Whenever an internal function throw an error, it lets the
> main function qmp_ev_fd_callback taking care of cleanup the `broken` state
> so that when the control passes outside ev_qmp implementation the state
> is disconnected/Idle.
Ah right.
> An internal `broken` state is just an half-transition toward the
> disconnected/Idle state.
>
> I guess I could add to the internal state documentation:
>
> When an internal function return an error, it can leave ev_qmp in a
> `broken` state but only if the caller is another internal function.
> That `broken` needs to be cleaned up, e.i. transitionned to the
> `disconnected` state, before the control of ev_qmp is released
> outsides of ev_qmp implementation.
If you do this you need to describe what kinds of states are legal
`broken' states. This is probably must easily done by making the
`broken' state a proper first-class internal state (giving it an entry
in the state table), but stating, as you do above, that it is not
visible externally because it's always tidied into `disconnected'
before control passes outside ev_qmp.
Ian.
___
Xen-devel mailing list
Xen-devel@lists.xenproject.org
https://lists.xenproject.org/mailman/listinfo/xen-devel
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
On Wed, Nov 14, 2018 at 03:43:41PM +, Ian Jackson wrote:
> (I finally remembered to drop the message-id from the CC header...)
:), I kept forgeting as well.
> Anthony PERARD writes ("Re: [PATCH v6.1 05/11] libxl_qmp: Implementation of
> libxl__ev_qmp_*"):
> > > 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.
>
> I think you are saying you can leave your ev_qmp in a state like
> disconnected, but with things allocated. Let us call that state
> `broken' (in internal nomenclature).
>
> But that state `broken' does not correspond to any of your public
> states. So your API document does not match the code.
>
> You need to either change the API to document this state as a public
> Broken state, or arrange for every ev_qmp-internal function to clean
> it up appropriately before control passes outside the ev_qmp
> implementation.
The current implementation already cleanup the broken state before the
control is passed outside ev_qmp implementation. That result in the Idle
public state. Whenever an internal function throw an error, it lets the
main function qmp_ev_fd_callback taking care of cleanup the `broken` state
so that when the control passes outside ev_qmp implementation the state
is disconnected/Idle.
An internal `broken` state is just an half-transition toward the
disconnected/Idle state.
I guess I could add to the internal state documentation:
When an internal function return an error, it can leave ev_qmp in a
`broken` state but only if the caller is another internal function.
That `broken` needs to be cleaned up, e.i. transitionned to the
`disconnected` state, before the control of ev_qmp is released
outsides of ev_qmp implementation.
Thanks,
--
Anthony PERARD
___
Xen-devel mailing list
Xen-devel@lists.xenproject.org
https://lists.xenproject.org/mailman/listinfo/xen-devel
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
Ian Jackson writes ("Re: [PATCH v6.1 05/11] libxl_qmp: Implementation of
libxl__ev_qmp_*"):
> It is probably easier to introduce the new public Broken state.
If you do this you should think about what should happen if your next
layer up attempts to reuse a Broken libxl__ev_qmp for an unrelated
command. I think some of the teardown after failed domain creation
might end up doing that.
Ian.
___
Xen-devel mailing list
Xen-devel@lists.xenproject.org
https://lists.xenproject.org/mailman/listinfo/xen-devel
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
(I finally remembered to drop the message-id from the CC header...)
Anthony PERARD writes ("Re: [PATCH v6.1 05/11] libxl_qmp: Implementation of
libxl__ev_qmp_*"):
> 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.
LGTM.
> > 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
LGTM.
> > 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.
I think you are saying you can leave your ev_qmp in a state like
disconnected, but with things allocated. Let us call that state
`broken' (in internal nomenclature).
But that state `broken' does not correspond to any of your public
states. So your API document does not match the code.
You need to either change the API to document this state as a public
Broken state, or arrange for every ev_qmp-internal function to clean
it up appropriately before control passes outside the ev_qmp
implementation.
It is probably easier to introduce the new public Broken state.
As for the commentary: if you prefer not to document the `error ->
Broken' transition next to each function, you can write a general
statement in the internal design. Eg, `for any internal function
which returns an error code, the state on error return will be Broken,
unless otherwise stated'. Or something.
Thanks,
Ian.
___
Xen-devel mailing list
Xen-devel@lists.xenproject.org
https://lists.xenproject.org/mailman/listinfo/xen-devel
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
On Tue, Nov 13, 2018 at 04:10:21PM +, 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 +, 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
> >
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
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 +, 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
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
On Tue, Nov 13, 2018 at 01:14:30PM +, Ian Jackson wrote:
> Anthony PERARD writes ("[PATCH v6.1 05/11] libxl_qmp: Implementation of
> libxl__ev_qmp_*"):
> ...
>
> I think this was intended to satisfy my request for comments about
> legal states:
>
> > +/* helpers */
> > +
> > +static void qmp_ev_ensure_reading_writing(libxl__gc *gc, libxl__ev_qmp *ev)
> > +{
> > +bool enable = false;
>
> 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.
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
> > +static void qmp_ev_set_state(libxl__gc *gc, libxl__ev_qmp *ev,
> > + libxl__qmp_state new_state)
> > +{
>
> This one at least does not need a comment :-).
>
> > +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
> > +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.
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.
> > +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
State transition
connected -> waiting_reply
* -> state unchange
on error: disconnected
The state of the transmiting buffer will be changed.
> > +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
> > +static int qmp_ev_get_next_msg(libxl__egc *egc, libxl__ev_qmp *ev,
> > + libxl__json_object **o_r)
> > +/* Find a JSON object and store it in o_r.
> > + * return ERROR_NOTFOUND if no object is found.
> > + * `o_r` is allocated within `egc`.
> > + */
> > +{
>
> Missing state comment.
precondition: !disconnected
state of the receiving buffer can be changed.
> > +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
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.
Next time I'll write one BIG function, and there will be less of those
comments to write :).
Thanks,
--
Anthony PERARD
___
Xen-devel mailing list
Xen-devel@lists.xenproject.org
Re: [Xen-devel] [PATCH v6.1 05/11] libxl_qmp: Implementation of libxl__ev_qmp_*
Anthony PERARD writes ("[PATCH v6.1 05/11] libxl_qmp: Implementation of
libxl__ev_qmp_*"):
...
I think this was intended to satisfy my request for comments about
legal states:
> +/* helpers */
> +
> +static void qmp_ev_ensure_reading_writing(libxl__gc *gc, libxl__ev_qmp *ev)
> +{
> +bool enable = false;
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...
> +static void qmp_ev_set_state(libxl__gc *gc, libxl__ev_qmp *ev,
> + libxl__qmp_state new_state)
> +{
This one at least does not need a comment :-).
> +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.
> +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.
> +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.
> +static int qmp_ev_callback_readable(libxl__egc *egc,
> +libxl__ev_qmp *ev, int fd)
> +/* on error: * -> disconnected */
Precondition ? And on non-error ?
> +static int qmp_ev_get_next_msg(libxl__egc *egc, libxl__ev_qmp *ev,
> + libxl__json_object **o_r)
> +/* Find a JSON object and store it in o_r.
> + * return ERROR_NOTFOUND if no object is found.
> + * `o_r` is allocated within `egc`.
> + */
> +{
Missing state comment.
> +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.
Thanks,
Ian.
___
Xen-devel mailing list
Xen-devel@lists.xenproject.org
https://lists.xenproject.org/mailman/listinfo/xen-devel
