RE: [sv-ec] Strict FIFO ordering of mailboxes try_put/try_get

Dave,

I mixed up Semaphores with Mailboxes when I posted my message, but I need to
do a little research, because semaphores and mailboxes might have the same
behavior, anyway.

With semaphores, lets assume as an example that the bucket has 2 keys
available.  A get(3) request will go into the get FIFO waiting for enough
keys.  Another get(3) request will also go into the FIFO.  But then, a
get(2) request can come in, and immediately get its keys, even though other
requests are queued up in the FIFO.  This is not a true FIFO behavior for
requesting keys.  This is the unexpected behavior I was thinking of when I
posted my agreement that users expect all get() requests to have FIFO
behavior, and are caught by surprise with SV's odd definition of a semaphore
FIFO.

Stu
~~~~~~~~~~~~~~~~~~~~~~~~~
Stuart Sutherland
Sutherland HDL, Inc.
stuart@sutherland-hdl.com
503-692-0898
 

> -----Original Message-----
> From: owner-sv-ec@server.eda.org 
> [mailto:owner-sv-ec@server.eda.org] On Behalf Of Rich, Dave
> Sent: Wednesday, February 14, 2007 12:35 AM
> Cc: sv-ec@server.eda-stds.org
> Subject: RE: [sv-ec] Strict FIFO ordering of mailboxes try_put/try_get
> 
> OK, I see there are lots of misunderstandings.
> 
> First of all, to define a bounded mailbox, you need three queues.
> 
> There is the queue that holds the data, or the contents of 
> the mailbox.
> The FIFO ordering of that queue guarantees that the first 
> piece of data
> to be placed into the mailbox by a completed put/try_put will be the
> first to be received from the mailbox by a successful get/try_get.
> Completion means the blocking put/get returns (unblocks) or the
> try_put/try_get returns true.
> 
> When the mailbox if full, there is a queue of processes suspended on a
> blocking put. That queue guarantees that a put completes in the same
> order that they are suspended. That queue and the data queue 
> give us the
> strict FIFO ordering for puts. Similarly, there is a third queue of
> processes suspended on a blocking get when the mailbox is empty.
> 
> The problem is not with multiple blocking puts/gets or multiple
> non-blocking try_puts/try_gets. The problem comes in when you start
> mixing blocking puts with non-blocking try_puts or mixing 
> blocking gets
> with non-blocking try_gets. Look at this example which is a
> simplification of a more complex example:
> 
> mailbox #(int) mb = new(.bound(1));
> int t;
> initial 
> 	begin
> 		fork
> 			mb.get(t);
> 		join_none
> 		#1 // some delay
> 		mb.put(123);
> 		void'(mb.try_get(t));
> 		assert(mb.num()==0); //this should never fail
> 	end
> 
> 
> If you accept that try_get() succeeds if and only if the size of the
> mailbox is greater than 0, then you must also accept that try_get()
> intercepts a suspended blocking get.
> 
> 
> Dave
> 
>      
> 
> > -----Original Message-----
> > From: Arturo Salz [mailto:Arturo.Salz@synopsys.com]
> > Sent: Tuesday, February 13, 2007 8:18 PM
> > To: stuart@sutherland-hdl.com; Neil.Korpusik@Sun.com; Rich, Dave
> > Cc: sv-ec@eda-stds.org
> > Subject: RE: [sv-ec] Strict FIFO ordering of mailboxes 
> try_put/try_get
> > 
> > Stu,
> > 
> > Based on your feedback and Neil's, I think I misunderstood Dave's
> point.
> > The queue maintained by the mailbox *should* be FIFO, which 
> means that
> > any previous call to get() - already in the mailboxe's 
> queue - should
> > get priority over a new call to get() - not yet in the queue. What I
> > meant to say is that we should not standardize the order in which
> > multiple try_put() calls deposit messages in the queue, that is,
> waiting
> > for the writing end of the channel need not be FIFO.
> > 
> > 	Arturo
> > 
> > -----Original Message-----
> > From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of
> > Stuart Sutherland
> > Sent: Tuesday, February 13, 2007 8:10 PM
> > To: Neil.Korpusik@Sun.com; 'Rich, Dave'
> > Cc: sv-ec@eda-stds.org
> > Subject: RE: [sv-ec] Strict FIFO ordering of mailboxes 
> try_put/try_get
> > 
> > 
> > I agree whole heartedly with Neil.  The odd behavior of a get
> bypassing
> > the
> > queue when other gets are in the queue is not at all intuitive.
> > 
> > Stu
> > ~~~~~~~~~~~~~~~~~~~~~~~~~
> > Stuart Sutherland
> > Sutherland HDL, Inc.
> > stuart@sutherland-hdl.com
> > 503-692-0898
> > 
> > 
> > > -----Original Message-----
> > > From: owner-sv-ec@server.eda.org
> > > [mailto:owner-sv-ec@server.eda.org] On Behalf Of Neil Korpusik
> > > Sent: Tuesday, February 13, 2007 3:43 PM
> > > To: Rich, Dave
> > > Cc: sv-ec@server.eda-stds.org
> > > Subject: Re: [sv-ec] Strict FIFO ordering of mailboxes
> try_put/try_get
> > >
> > > I believe that most users would expect requests to be queued up in
> the
> > > order in which they were received. It is more work for the vendors
> to
> > > support this approach, but it is what I think most users 
> would want.
> > >
> > > Neil
> > >
> > >
> > >
> > > Rich, Dave wrote On 02/13/07 08:58,:
> > > > I didn't get a response to this. I'm going to go with the
> assumption
> > > > that try_put/try_get can preempt a waiting put/get.
> > > >
> > > >
> > > >
> > > > We might want to clarify that strict FIFO order apples 
> only after
> a
> > > > successful try.
> > > >
> > > >
> > > >
> > > > Dave
> > > >
> > > >
> > > >
> > > >
> > > >
> > > >
> > > --------------------------------------------------------------
> > > ----------
> > > >
> > > > *From:* owner-sv-ec@server.eda.org
> > > [mailto:owner-sv-ec@server.eda.org]
> > > > *On Behalf Of *Rich, Dave
> > > > *Sent:* Friday, February 02, 2007 10:48 AM
> > > > *To:* sv-ec@server.eda-stds.org
> > > > *Subject:* [sv-ec] Strict FIFO ordering of mailboxes
> try_put/try_get
> > > >
> > > >
> > > >
> > > > This is related to a discussion with semaphores a few years back
> > > > http://www.eda-stds.org/sv-ec/hm/2651.html
> > > >
> > > >
> > > >
> > > > 14.3.4 says
> > > >
> > > >
> > > >
> > > > The try_put() method stores a message in the mailbox in strict
> FIFO
> > > > order. This method is meaningful
> > > >
> > > > only for bounded mailboxes. If the mailbox is not full, then the
> > > > specified message is placed in the mailbox,
> > > >
> > > > and the function returns a positive integer. If the mailbox
> > > is full, the
> > > > method returns 0.
> > > >
> > > >
> > > >
> > > >
> > > >
> > > > Is the strict ordering only with other try_put()'s or if
> > > another put()
> > > > is blocked waiting for space, must the put() be unblocked
> > > before try_put
> > > > could succeed? Same question for try_get. Must a waiting get be
> > > > unblocked before try_get could succeed?
> > > >
> > > >
> > > >
> > > > Dave
> > > >
> > > >
> > > >
> > > >
> > > >
> > > > David Rich
> > > > Verification Technologist
> > > > Design Verification & Test Division
> > > > Mentor Graphics Corporation
> > > > dave_rich@mentor.com
> > > > Office:   408 487-7206
> > > > Cell:     510 589-2625
> > > >
> > > >
> > > >
> > > >
> > > > --
> > > > This message has been scanned for viruses and
> > > > dangerous content by *MailScanner*
> > > <http://www.mailscanner.info/>*, and is
> > > > believed to be clean.
> > > > --
> > > > This message has been scanned for viruses and
> > > > dangerous content by *MailScanner*
> > > <http://www.mailscanner.info/>, and is
> > > > believed to be clean. *
> > >
> > > --
> > >
> ---------------------------------------------------------------------
> > > Neil Korpusik                                     Tel: 
> 408-720-4852
> > > Senior Staff Engineer                             Fax: 
> 408-720-4850
> > > Frontend Technologies - ASICs & Processors (FTAP)
> > > Sun Microsystems
> > > email: neil.korpusik@sun.com
> > >
> ---------------------------------------------------------------------
> > >
> > >
> > >
> > > --
> > > This message has been scanned for viruses and
> > > dangerous content by MailScanner, and is
> > > believed to be clean.
> > >
> > >
> > >
> > >
> > 
> > 
> > 
> > --
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.
> 
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> 
> 
> 



-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.