Re: [boost] Re: Threads

From: Beman Dawes (beman_at_[hidden])
Date: 2000-08-25 10:33:04

David Abrahams wrote:

 >Maybe you and I have something different in mind. When I say "informal" I
 >don't mean "unrigorous" in any way. A formal correctness proof has been
 >shown to impracticable even for small programs without concurrency.
 >
 >I am thinking, for example, about the power of the basic/strong/no-throw
 >exception-safety distinctions, and how with those three simple concepts 
you
 >can easily reason about the exception-handling behavior of large systems. 
I
 >don't know if there is an analogue in the domain of concurrent 
programming,
 >but I think it is worth searching for.
 >
 >-Dave
 >
 >----- Original Message -----
 >From: "Bill Rutiser" <wru_at_[hidden]>
 >> Let me add a warning about informal reasoning about concurrent
 >> processes. There exist clever, efficient, synchronization schemes,
 >> proved to be correct for two processes, that fail badly for three.
 >>
 >> -- Bill Rutiser

Hoare himself addressed this issue in a 1996 paper "How did software get so 
reliable without proof?"  There's an extended abstract at 
http://users.comlab.ox.ac.uk/tony.hoare/icse18.html

Quoting the abstract, "...the techniques employed to achieve reliability 
are little different from those which have proved effective in all other 
branches of modern engineering: rigorous planning of procedures for design 
inspection and review; raised levels of machine support for design 
automation; quality assurance based on a wide range of targeted tests; 
careful structuring of the product into modules and layers; continuous 
evolution by adaptation of products already in widespread use; relaxation 
of resource constraints and deliberate over-engineering (otherwise known as 
defensive programming or belt-and-braces). Formal methods and proof play no 
greater role in largescale programming than they do in any other branch of 
modern engineering."

In other words, the same point that Dave makes: "informal" doesn't mean 
"unrigorous".

--Beman