Parallelizing Symbolic Execution

Manually invoking the workers and the load balancer

A 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 data

When 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 scripts

Coming soon. It will most likely be based on the versatile GNU parallel.

Comments