blob: 49a036e83ded8397559439166149c5644994d56a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
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
|
