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

It would be fruitful to look at deadlock and starvation avoidance
proofs.  This satisfying out of FIFO order a request that can be
fulfilled in preference to others that can not be filled reminds me of
various techniques that have been proven to prevent deadlock and avoid
starvation.  The task "A" calling get(2) may already have 1 key (or may
when it is done, unblock some other task that has 1 key), and by giving
A the keys it needs, will allow it to complete (making forward
progress), and thereby release enough keys to allow the prior tasks
waiting on get(3) requests to proceed.

This seems to be a form of the multiple sleeping barbers problem. 

-----Original Message-----
From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of
Stuart Sutherland
Sent: Wednesday, February 14, 2007 10:21 AM
To: sv-ec@eda-stds.org
Subject: 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.


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