This file gives instructions for installing and running the prototype implementation of the view abstraction checker. Please mail me at gavin.lowe@cs.ox.ac.uk if you have difficulties. Installation ------------ These instructions assume you already have scala, java and FDR4 installed. 1. Unpack util.zip somewhere convenient; this will give the ox.gavin package. 2. Update the makefile so that the first few lines give the locations of the ox.gavin package (the directory containing ox), the base of the FDR installation (directory including lib), and the base of the Scala installation (directory containing lib). 3. "make" should now compile all the files. Please contact me if this doesn't work. Scripts ------- The script should include annotations, defining the families of components and the servers. For example -- @VA component process = FreeNode -- @VA component alphabet = alphaNode -- @VA component identity type = NodeID -- @VA component process = Thread -- @VA component alphabet = alphaThread -- @VA component identity type = ThreadID -- @VA servers = ServerSet This defines a family of components FreeNode, with alphabets given by alphaNode, and indexed by NodeID. The types should be FreeNode :: (NodeIDType) -> Proc alphaNode :: (NodeIDType) -> {Event} where NodeIDType is the type that includes NodeID (plus maybe distinguished values). Likewise, the above defines a family of components Thread, with alphabets given by alphaThread, and indexed by ThreadID. Finally, the servers are defined by ServerSet, or type ServerSet :: <(Proc, {Event})> each pair in the sequence representing one server and its alphabet. Usage ----- Example: scala -cp .:/users/gavinl/Scala/Util:/users/gavinl/bin/FDR4/fdr/lib/fdr.jar ViewAbstraction.VA CSP/TreiberStack.csp --shape 1 2 --shape 2 1 --shape 3 0 The classpath must include the location of the ox.gavin package, and the FDR jar file. This example will run on the file CSP/TreiberStack.csp. It will use abstraction set (Node:1, Thread:2) U (Node:2, Thread:1) U (Node:3, Thread:0). Optional command-line arguments: * --shape n1 n2 ... nk: includes a shape (F1:n1, ..., Fk:nk) in the abstraction set, where the families of components are F1, ..., Fk, listed in that order in the annotations of the input file. * -k k: set the abstraction set to be all views of size k; this abbreviates a sequence of --shape arguments. * --checkDeadlock: include a check for deadlock freedom. * --significancePath f1 f2 ... fk: include a chain indicating significant components, as described in Section 8 of the paper; to be including when checking for deadlock freedom. * --bound b: limit the search to a depth of b. * --profile t: run profiling, sampling every t ms, and giving tree output. * --profileFlat t: run profiling, sampling every t ms, and giving flat output. Other programs -------------- Experiment.scala corresponds to the experiments reported in the paper. It will be necessary to edit the "classpath" variable in this file for it to run. Instrumentation.java performs memory profiling. Read the instructions in the file (but the framework this uses is a pig to get to work).