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