Re: [Xen-devel] FIFO-based event channel ABI design (draft B)

[Ian Jackson <Ian.Jackson@xxxxxxxxxxxxx>]

David Vrabel writes ("[Xen-devel] FIFO-based event channel ABI design (draft 
B)"):
> Event State Machine
> -------------------
> 
> Event channels are bound to a port in the domain using the existing
> ABI.
> 
> A bound event may be in one of three main states.
> 
> State    Abbrev.  PML Bits  Meaning
> -----    -------  --------  -------
> BOUND    B        000       The event is bound but not pending.
> PENDING  P        100       The event has been raised and not yet
> acknowledged.
> LINKED   L        101       The event is on an event queue.
> 
> Additionally, events may be UNMASKED or MASKED (M).
> 
> ![\label{events_sm}Event State Machine](event-sm.pdf)

This high-level state machine description doesn't capture the
transient states which exist when Xen and/or the guest need to update
multiple words at once.

In order to check that this protocol is correct, I think you should
draw a state diagram which includes these transient states, and verify
that the edges all operate as intended.

Ian.

_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxx
http://lists.xen.org/xen-devel