Re: Experience with JCSP/CTJ/FDR

[Dyke Stiles <dyke.stiles@xxxxxxxxxxx>]

Greetings -

With respect to designing fairly significant systems with CSP:
Last Fall the final project for my CSP class (Roscoe's text, Gerald's
CTJ, FDR) was a message routing system. Each node had two sources and
two destinations; the sources could send messages to any destination
on any other node, and acks were required before additional messages
could be sent. All messages and acks had to be multiplexed over
a single pair of channels - one in each direction - connecting the
nodes. Each node wound up having about 20 processes (many of the
3 line variety).

The students were required to design and check (with FDR) the 
CSP versions before implementing the CTJ version. The individual
node (composite) process was checked against specs and to be deadlock
and livelock free. We could verify two-node systems on fairly small
workstations, but the three-node systems (about 60 processes) ran
out of virtual memory space after running up something like 3,300,000
states (we hope to reconfigure one of our servers and take another 
shot at this one soon...or reduce the CSP to simpler equivalents...)

Best part: two out of four groups had NO trouble getting the 3-node CTJ
versions - all 60 processes - up and running. Quote: "The Java was 
very easy once we finished with CSP design."  A third group got the
2-node CTJ version running, and the fourth group made a valiant
try (too little effort too late on the last two groups, I think).

If we can get students from square zero (as far as concurrency goes) to
verified 60-process running implementations in 14 weeks, something must 
be right with CSP... (project was last 4-5 weeks - done incrementally)

Dyke.


-- 
======================================================================
Dyke Stiles            >>>>>> new address!!>>> dyke.stiles@xxxxxxxxxxx
Professor and Chair, Graduate Committee
Department of Electrical and Computer Engineering
4120 Old Main Hill
Utah State University
Logan UT 84322-4120
Voice: +1-435-797-2840                          FAX:   +1-435-797-3054
Work:                http://www.engineering.usu.edu/ece/research/rtpc/
Play:  http://www.engineering.usu.edu/ece/research/rtpc/utah/utah.html
======================================================================