~
BEGIN
stackLimit: NAT ~ 1024;
ProgramCounter: TYPE = CARD32;
SpyRep:
TYPE ~
RECORD [
missed: CARD32 ¬ 0,
startTime: BasicTime.GMT,
stopTime: BasicTime.GMT,
nAlloc: NAT,
limit: NAT,
pAlloc: POINTER TO MemUnit,
events: EventPool,
eAlloc: Event,
eLimit: NAT,
enAlloc: NAT,
mem: MemPool,
threads: Threads
];
MemPool: TYPE ~ REF MemPoolRep;
MemPoolRep:
TYPE ~
RECORD [
SEQUENCE size: NAT OF MemUnit
];
MemUnit:
TYPE ~
RECORD [
oSetNode: OSetNode,
treeRep: TreeRep
];
Threads: TYPE ~ REF ThreadsRep;
ThreadsRep:
TYPE ~
RECORD [
SEQUENCE size: NAT OF PerThreadObject
];
PerThreadObject:
TYPE ~
RECORD [
e: Event, -- the event that started the threads current wait
eventPool: NAT, -- index of first event available for use by the thread
memPool: NAT, -- index of the first MemUnit available for use by the thread
tree: Tree, -- the per-thread tree
stackBuffer: ARRAY [0..stackLimit) OF ProgramCounter,
lock: PACKED ARRAY [0..4) OF BYTE
];
OSet: TYPE = POINTER TO OSetNode; -- represents an pc-ordered collection of Tree objects
OSetNode:
TYPE =
RECORD [
left: OSet, -- smaller items
item: Tree, -- the child tree
right: OSet -- larger items
];
Tree: TYPE ~ POINTER TO TreeRep;
TreeRep:
TYPE ~
RECORD [
children: OSet ¬ NIL,
pc: ProgramCounter ¬ 0
];
EventPool: TYPE ~ REF EventPoolRep;
EventPoolRep:
TYPE ~
RECORD [
SEQUENCE size: NAT OF EventRep
];
Event: TYPE ~ POINTER TO EventRep;
EventKind: TYPE ~ {sleep, wakeup, sample, run0, run1, run2, endRun};
coded as S, W, R, X, Y, and Z in the log. endRun events don't appear.
EventRep:
TYPE ~
RECORD [
kind: EventKind,
tree: Tree,
time: CARD,
sleepusec: CARD,
wakeup: CARD,
wakeusec: CARD,
waker: Event
];