[Haskell-cafe] Re: Channel9 Interview: Software Composability and theFu ture of Languages

[Benjamin Franksen]

Chris Kuklewicz wrote:
> Aside on utterly useful proofs: When you write concurrent programs you
> want an API with strong and useful guarantees so you can avoid deadlocks
> and starvation and conflicting data read/writes.  Designing an using such
> an API is a reasoning exercise identical to creating proofs.  Some systems
> makes this possible and even easy (such as using STM).

I have to -- partly -- disagree with your last statement. It is possible
that I missed something important but as I see it, STM has by construction
the disadvantage that absence of starvation is quite hard (if not
impossible) to prove. A memory transaction must be re-started from the
beginning if it finds (when trying to commit) another task has modified one
of the TVars it depends on. This might mean that a long transaction may in
fact /never/ commit if it gets interrupted often enough by short
transactions which modify one of the TVars the longer transaction depends
upon.

IIRC this problem is mentioned in the original STM paper only in passing
("Starvation is surely a possibility" or some such comment). I would be
very interested to hear if there has been any investigation of the
consequences with regard to proving progress guarantees for programs that
use STM.

My current take on this is that there might be possibilities avoid this kind
of starvation by appropriate scheduling. One idea is to assign time slices
dynamically, e.g. to double it whenever a task must do a rollback instead
of a commit (due to externally modified TVars), and to reset the time slice
to the default on (successful) commit or exception. Another possibility is
to introduce dynamic task priorities and to increase priority on each
unsuccessful commit. (Unfortunately I have no proof that such measures
would remove the danger of starvation, they merely seem plausible avenues
for further research. I also don't know whether the current GHC runtime
system already implements such heuristics.)

Cheers
Ben