Re: New Book: CONCURRENCY

[Denis A Nicole <dan@xxxxxxxxxxxxxxx>]

On Wed, 21 Apr 1999, Bryan Scattergood wrote:

> 
> On Wed, 21 Apr 1999, Denis A Nicole wrote:
> > > On Tue, 20 Apr 1999, Oyvind Teig wrote:
> > > WHY CAN'T I INPUT IN OCCAM?
> > > It MUST be better to model check and code in the same language, eh?
> > 
> > That's not uncontroversial.  I think so, but others would have you design,
> > prove and (maybe) check in an unexecutable specification language and
> > then refine (with automated checking of the refinement) into an
> > implementation language.
> 
> Okay, I'll bite. We don't have a version of FDR which accepts occam as
> input because of the size of the state-space. On current PCs we
> regularly check systems with around 10^8 states. Throwing time, disk
> and memory at the problem might get you another order of magnitude.
> That still isn't enough to explicitly check a system with one INT32,
> let alone a real-world system.

I agree, you don't model-check a whole program.  

> You can simply ignore the state, and the paper I presented at Como in
> 1994 discussed doing just that. Unfortunately that throws away so much
> that we never went beyond a prototype implementation.

It seems to me that the program validation tool we are reaching for
integrates several technologies: 

	1. User input, to indicate which state can be discarded in
	"program slicing" 

	2. User input of "intended" assertions about the program.  At its
	crudest, say, loop invariants, but expressed as programming
	language constructs.

	3. Automatic proof of "regular" and unbounded parts of the
	behaviour, based on 1 and 2.

	4. Model checking of irregular parts.

> I'll agree that ideally you would be able to check your final
> implementation, but that is rarely possible with the current state of
> the art. In the meantime, the best we can do is to check some
> abstraction of the system. The aim of specification languages is to
> make it easier to produce suitable abstractions, whether during the
> design phase or after implementation.

The specification languages do at least three things:

	1. Provide a more regular semantics than most programming
	languages, so reducing the technical complexity of proofs.

	2. Provide mathematical structures (say sets, bags) that encourage
	suitable levels of abstraction.

	3. Provide a common notation for assertions and for abstract
	program designs. 

Unfortunately they also:

	1. Generate a syntactic and semantic gap between abstract designs
	and implementations.

	2. Most importantly, intimidate programmers without a mathematical
	background. I believe that "real" computer scientists completely
	fail to understand the limitations of ordinary programmers writing
	ordinary mission-critical applications in, say, Visual BASIC. 
	Programming needs to be like car driving; a mass activity with
	socially acceptable loss of life.  It's already a mass activity;
	how do we reduce the carnage?


Denis A Nicole                      WWW:   http://www.hpcc.ecs.soton.ac.uk/~dan 
High Performance Computing Centre   Email: dan@xxxxxxxxxxxxxxx                  
University of Southampton           Phone: +44 1703 592703                      
UK.                                 Fax:   +44 1703 593903