Messages in this thread | | | From | "Peter T. Breuer" <> | Subject | Re: MM deadlock [was: Re: arca-vm-8...] | Date | Tue, 12 Jan 1999 10:39:06 +0100 (MET) |
| |
Thanks for putting this clearly. It is required for any kind of formal guarantee. Let me put this bluntly - no spec, no proof.
I can upgrade a clear description to a sufficiently clear spec but I need to be educated in the terminology and filled in on the background here if I am to do that too.
(Sorry)
"A month of sundays ago Helge Hafting wrote:" > > > Some variant? I need to know what that does. What is a spinlock anyway? > > A spinlock is a technique used for "fast" protection of > critical regions on multi-cpu machines. > > It generally use a processor-specific instruction of the > test-and-set type, that is guaranteed to access memory > atomically in the case where several processors tries simultaneously. > > A processor that gets the lock continues through the critical > section which is supposed to be short for a spinlock. Processors
while (available<=0 ? 1 : available=0);
That's a typical blocking read from a semaphore. I assume it's implemented right! It's fine if indeed the test_and_set is atomic.
> that don't get the lock loop on the test-and-set instruction. > That is the "spinning" part, and the reason why the critical > region ought to be short, as any other processor(s) are busy-waiting. > > The other way of doing locking is to let processors that don't get the lock > scedule something else and just block whatever process > is waiting for a resource. This is the way disk-io queuing is > handled.
OK. Yes, the spinlock is more "classic" in terms of theory.
> Spinlocks are routinely used in cases where the critical region is so short > that scheduling overhead is a bigger loss than the > busy-waiting loss. This applies to kernels only. A spinlock
> I don't think Linus has a problem with what a semaphore should do,
No - the problem is relating that concept to the code. The fact that I can't divine the intention from the code means that it is not self-evident either, but in any case a formal guarantee of any property that is to hold of a computer requires the concept to become bound to cpu states. That abstract binding idea<->variables is what I need to have set out. Without it, I don't know if "waking" is intended to be the resource-available concept, or if "count" is.
Since he's got two fields where I have one concept, clearly one of them is an implementation detail. That's his implementation detail, and so he has to state what it's supposed to be doing!
> I believe his problem is creating one that is both > foolproof in all cases and fast enough for his liking too.
Foolproof (relative) is my business. Fast is his.
> Helge Hafting
Peter
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/
| |