Re: FIFO-based event channel ABI design (draft B)

From: Ian Jackson <Ian.Jackson@eu.citrix.com>
To: David Vrabel <david.vrabel@citrix.com>
Cc: "xen-devel@lists.xensource.com" <xen-devel@lists.xensource.com>,
	Wei Liu <wei.liu2@citrix.com>
Subject: Re: FIFO-based event channel ABI design (draft B)
Date: Tue, 19 Feb 2013 18:39:01 +0000	[thread overview]
Message-ID: <20771.50885.702521.722255@mariner.uk.xensource.com> (raw)
In-Reply-To: <511E46FD.3010605@citrix.com>

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.