1 files changed, 56 insertions, 0 deletions
diff --git a/books/workshops/2000/lusk-mccune/lusk-mccune-final/README b/books/workshops/2000/lusk-mccune/lusk-mccune-final/README
new file mode 100644
index 0000000..49a036e
--- /dev/null
+++ b/books/workshops/2000/lusk-mccune/lusk-mccune-final/README
@@ -0,0 +1,56 @@
+ACL2 for Parallel Systems Software
+
+This directory contains version sim19 of our multiprocess
+simulator.  It is described in a short paper (paper.ps).
+
+This represents the early stages of a work in progress.
+The simulator doesn't have all the functions we write
+about in the paper, it is not well debugged, and it is
+slow.  The guard proofs are very slow.  But it's s start :-)
+
+Bill McCune  mccune@mcs.anl.gov
+Rusty Lusk   lusk@mcs.anl.gov
+
+September 1, 2000
+
+======================================================
+
+Paper:
+
+paper.tex
+paper.ps
+
+======================================================
+
+Books:
+
+util             some utilities
+gensym-e         generate new symbols
+base             basic types such as hostname, process-id, file descriptor
+expr             expressions for the programming language
+pstate           process state
+cstate           connection state
+lstate           listening state
+mstate           multiprocess state
+stepproc0        step functions for for exec, fork, rsh
+stepproc1        step functions for send, receive, select, and ordinary stmts
+setup            support for stepproc2
+stepproc2        step functions for setup-listener, accept, connect
+stepprocess      bring together all step functions
+compile          preprocessor for our programs
+simulator        the simulator
+
+======================================================
+
+Example Multiprocess Programs:
+
+trace            pass a message around a ring
+fence            a barrier operation
+
+======================================================
+
+Bill McCune  mccune@mcs.anl.gov
+Rusty Lusk   lusk@mcs.anl.gov
+
+September 1, 2000
+