Re: A CSP model for Java threads

[Bryan Scattergood <bryan@xxxxxxxx>]

Oyyvind,

> I sit here, in industry, without any FDR or FDR2 and read your very
> interesting letters, pushing state of the art of Java CSP ahead.
> Thanks for sharing these things!

Indeed. It is reasssuring that mechanical checks can catch these
problems, if a little depressing to see just how hard this stuff can
be to get 'right'.

> There is a problem in getting this technology over to industry:
> FDR is too expensive! 

The price of FDR is comparable to that of other commercial tools.
We've priced similar products, such as C++ validators, and FDR is is
reasonably priced in comparison. I very much doubt that the 'virtually
free' alternatives come with telephone and email support, or scale to
problems with >10^8 states.

How many basic architectural errors does FDR have to catch in order to
cover the licence cost?

> I want to learn from this as well! I know FSP is virtually free:
> http://www-dse.doc.ic.ac.uk/concurrency/
> 
> o  Could FSP and LTSA have done the job for you, or is it 
>    only a "toy" compared to FDR2?

I can't comment on the performance of other tools, but the checks in
Jeremy's CSP are trivial by FDR standards. Taking the 30 July version,
our (obsolete) SparcStation1 performed all the checks in less than 50
seconds. Our fastest took slightly over 1 second.

> FDR doesn't even run on MS-Windows!

Yet.

When we started development of FDR, Windows 3.1 was the dominant
version and was, frankly, incapable of supporting FDR's virtual-memory
requirements. Even with NT4, our experience suggests that FDR will run
better under FreeBSD/Linux/Solaris86 than under Windows on the same
hardware.

However, we do have plans for an NT version in the medium-term.

   Bryan