diff options
author | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
---|---|---|
committer | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
commit | 092176848cbfd27b96c323cc30c54dff4c4a6872 (patch) | |
tree | 91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/2000/lusk-mccune/lusk-mccune-final/README |
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/2000/lusk-mccune/lusk-mccune-final/README')
-rw-r--r-- | books/workshops/2000/lusk-mccune/lusk-mccune-final/README | 56 |
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 + |