Re: [boost] Re: Threads

From: David Abrahams (abrahams_at_[hidden])
Date: 2000-08-24 17:00:35

From: "Jens Maurer" <Jens.Maurer_at_[hidden]>
>
> Greg Colvin wrote:
> > Jens Maurer:
> > > I think that striving for compile-time support for error detection
> > > is a good idea in general (that's why we're using a statically-typed
> > > language), but not very applicable to the problems with threading,
> > > which are run-time dynamic in their most intrinsic nature.
> >
> > If your problems with threads are "run-time dynamic" then
> > you are in hopeless trouble.  Code is always dynamic.  To
> > write correct code you have to be able to reason about
> > program state *statically*.
>
> The main point is whether you can explain the problem well enough
> to the compiler so that *it* can reason statically (on a meta level)
> about your program.  The answer is no.  The theory says that a
> computer cannot even decide (in general) whether your program has
> endless loops or not.  I am saying that threading is of this quality.
>
> The programmer can always reason statically, be creative and
> write a formal proof his program.  But that's the level where all
> the bugs happen: The programmer thinking wrongly about what his
> program does.

Of course that's true. On the other hand, certain library designs can make
it easier to reason about the correctness of a program; others make it
harder. For example, library components that manage the resources they
allocate are easier to reason about than ones that demand assistance from
the caller. Monitors tend to make reasoning easier by eliminating issues of
contention for the invariant of a class. I think Greg's goal is that boost
provide constructs that help the programmer to understand how and why his
program is correct. I support that goal.

Interestingly, being able to write a formal proof simply isn't good enough.
To be effective, these constructs have to allow the programmer to reason
relatively quickly and _informally_. Nobody really has the time for a formal
proof anyway ;)

-Dave