Manually invoking the workers and the load balancerA Cloud9 distributed system is composed of a load balancer and one or more workers. Each of them runs as a separate process. The processes communicate through network sockets and can be co-located on the same machine, and thus benefit from the multi-core parallelism, or be spread across a cluster. Starting the load balancer$ setarch $(arch) -R -L $CLOUD9_ROOT/src/cloud9/Release+Asserts/bin/c9-lb --address=<local address> --port=<local port> If no address or port is specified, the load balancer listens by default to localhost:1337 Starting the workers$ setarch $(arch) -R -L $CLOUD9_ROOT/src/cloud9/Release+Asserts/bin/c9-worker --output-dir=<worker dir> \ --c9-local-host=<local address> --c9-local-port=<local port> \ --c9-lb-host=<lb address> --c9-lb-port=<lb port> If no local address or port is specified, the worker listens by default to localhost:1234 Example: For running Cloud9 locally on a 48-core machine, one could use the following script to instantiate 48 workers: for I in $(seq 1 48); do setarch $(arch) -R -L $CLOUD9_ROOT/src/cloud9/Release+Asserts/bin/c9-worker \ --output-dir=worker-output-$(printf "%02d" $I) \ --c9-local-port=$((19000+I)) \ [... other KLEE/Cloud9 parameters ...] & sleep 1 done Analyzing the dataWhen managing the workers manually, the user is responsible with making sure that each worker writes its results in a separate directory on the host machine. The data must be collected and aggregated manually from all the machines involved in the experiment. Note: Export the GLOG_logtostderr=1 environment variable if you wish the application logs to be written at standard error, instead of files in /tmp. Find more details here.Invoking workers remotely using SSH-based scriptsComing soon. It will most likely be based on the versatile GNU parallel. |