On Monday, October 29, 2001, at 11:00 am, David Chase wrote:
[...]
> At a recent C-- workshop, I think the consensus (among us,
> various academics, and someone who had worked on Plan 9) was
> that you wanted to make the hardware interrupts Go Away.  There
> are two approaches -- polling (compiler/verifier inserted) and
> service threads, which can also be combined.  It also helps to
> use wait-free (Herlihy-style) data structures based on
> compare-and-swap so that you can actually accomplish
> something in your interrupt handler.  (So, at the very bottom
> there is asynchrony, and it is tricky to reason about, but
> that is the end of it).
[...]
>> Some would argue that it is better to be able to reason about 
>> your program
>> than try to test it exhaustively. And having a simpler cleaner 
>> underlying
>> model of computation facilitates reasoning. It is harder to 
>> reason about
>> programs that are both concurrent and sequential.
>
> This is all absolutely true -- however, it is also absolutely
> true that I am a fallible typist, and a fallible proofreader
> (as the the repeated word example demonstrates all too too well).
> Testing is absolutely necessary simply to test for transcription
> errors, and there is also the possibility of a "thinko" (meaning,
> I start with the wrong assumptions) in my design and proof.
> There is, in any multi-person task, the existence of
> communication errors between different people; I may not state
> an "obvious" assumption that turns out not to be so obvious,
> etc, etc.  Testing is good for smoking out all of these things,
> and once there is smoke, you then go looking for fire.

The (often implicit) reason people want to do formal proofs that 
programs meet their specifications is that the specifications 
are usually simpler than the implementations.  The "simpler" is 
usually implied to be some combination of "shorter" and/or 
"easier to understand/believe/map to reality".  When this 
condition is true, then a formal proof is a *very* nice thing to 
have.  Testing is nice to have too, especially if a failure 
during testing can automatically be mapped back to the 
corresponding false assumption in the specification.

[...]
> The central trick here (and a good one) is the use of single-assignment
> synchronized variables.

That sounds a *lot* like functional programming, especially in a 
functional language that supports lazy evaluation.

> So, what happens if you combine that sort of programming with
> something like OO Squeak?  I imagine producers-consumers being
> done with an endless linked list, where the consumer waits on
> the next list element, which will contain one chunk of data, and
> an initially empty next-list-element field.  At the low level,
> what's going on is each "unknown" variable has a full-empty
> indicator, and (because all blocked computations are wakened
> at the same time) a thread can register its interest in data
> by pushing itself onto a stack, where the head of the stack
> is perhaps the full-empty indicator, using a compare-and-swap,
> which is as fast as a simple synchronization-acquire in Java
> (then the thread has to put itself to sleep, which requires
> a bit more work and synchronization, urk).

Here's a possible solution.  Within the Herlihy style wait-free 
framework, have the "go to sleep and wake up when" activity be 
able to prevent the current thread from going to sleep if the 
condition is true at the time.  The "potential excess work" that 
is typical in such algorithms would be to ignore the attempt to 
resume an already running thread (if it hasn't reached some 
other potential stopping point in the interim).