Re: [boost] Re: Design and documentation of Boost.Threads

From: Kevin S. Van Horn (kevin.vanhorn_at_[hidden])
Date: 2001-11-14 15:21:48

On Wed, 14 Nov 2001 terekhov_at_[hidden] wrote:

> > there is a precise technical meaning of "fairness" in the literature
> > on correctness proofs for concurrent programs.
>
> How about posting a URL?

It's been nearly thirteen years (grad school) since I was actively involved
in the area of correctness proofs for concurrent programs, and I have only done
the odd informal correctness proof since then, so I'll admit I'm a bit out of
date on the current literature.  You might want to look at Chandy and Misra's
book, _Parallel Program Design: A Foundation_.  Or you might want to visit
Leslie Lamport's home page
http://research.microsoft.com/users/lamport/pubs/pubs.html; he wrote a lot of
the important papers in the field.  In particular, you might want to take a
look at his paper "'Sometime' is sometimes 'not never'," which is available in
PDF on that web page.  You might also go to www.citeseer.com
and search on "fairness" or "temporal logic."

> Are you saying that if A gets the mutex 100000000000000
> times for every time B gets it, it would still be "fair"?

Yes.  Lack of starvation is generally considered a property one might try to
prove holds for a program.  How frequently a thread gets access to shared
resources, if important, is usually considered a performance issue, which
is much less amenable to formal proof.  (However, the notion of "bounded
fairness" is one that may be of practical interest and amenable to proof; that
is, one shows a bound on how many times a thread can be passed up for a
resource before it finally gets its turn.)  BTW, let me repeat a comment I
made earlier on correctness proofs for concurrent algorithms: I do not view
such proofs as a panacea, but as an important and necessary tool in rooting
out bugs in concurrent algorithms, which are very hard to adequately test.

> hmm. You wrote:
>
> "Note that mutexes that use FIFO scheduling are fair"
>
> Why do you think so?

Because if threads acquire the mutex in the same (or even approximately the
same) order as that in which the request it, then no thread can be starved.

> b) in POSIX, mutexes do not hand-off lock ownership
> to a selected waitor on unlock.

You have me at a disadvantage here; as I don't have $180 to spare for a copy
of the POSIX standard, I have been unable to find out these fine details, and
have instead had to rely on secondary sources whose authors are completely
oblivious to these issues.  Some things I had read seemed to indicate to me,
however, that POSIX mutexes were strong mutexes.

Whatever the POSIX standard guarantees, it is easy to implement fair or strong
mutexes at the OS level.  If you want a fair but weak mutex, for example, but
want to reduce context switches, you could use a priority scheme that gives
high priority to running threads, combined with aging to cause a thread's
priority to slowly increase as it waits.

> c) I have yet to see a mutex which would guarantee
> starvation-free access to its "queue" of waitors.

I'm not sure what you mean here.  For a uniprocessor this is trivial.  Are you
talking about spinlocks protecting the wait queue structure for a mutex in a
SMP operating system?  I've never heard of such a starvation problem occurring
in practice (i.e., a CPU getting stuck forever in the busy wait trying to
acquire the spinlock); I would expect that, in practice, spinlocks are
starvation-free because the locks are held for only a short period of time and
a spinning CPU will do its test-and-set (or equivalent) long before the CPU
that just released the spinlock is going to try to reacquire it.  (I can see a
potential for problems if you have many CPUs continually contending for the
spinlock, though.  If such a situation occurs, though, you have other problems
-- your system is spending too much time in the kernel locking and unlocking
spinlocks instead of doing useful work!)