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

From: Neil Korpusik <Neil.Korpusik_at_.....>
Date: Wed Feb 14 2007 - 11:15:34 PST
Mac,

The situation that you are describing only applies to the semaphore
construct. The mailbox doesn't maintain a set of keys.

Your discussion of deadlock avoidance is a user issue and doesn't
need to be addressed by the LRM. There are many ways to use a
semaphore, some of which are trickier than others. Users need to
be very careful when varying the number of keys used by various
threads.

Neil



Michael (Mac) McNamara wrote On 02/14/07 10:53,:
> 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.
>>
>>
>>
>>
> 
> 
> 
> 

-- 
---------------------------------------------------------------------
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.
Received on Wed Feb 14 11:16:08 2007

This archive was generated by hypermail 2.1.8 : Wed Feb 14 2007 - 11:16:14 PST