This page contains the documentation on using MacePC for different systems. MacePC has been specifically tailored to systems built using the Mace toolkit.

MacePC is bundled with the Mace toolkit, which can be obtained through SVN: Detailed instructions for downloading and compiling Mace. It will be present within application/simulator/.

As an example, we outline the usage of MacePC on RandTree (a random tree construction protocol designed to connect nodes using an overlay tree). As described in the paper, this consists of the following phases (in that order): Event Duration Training, Performance Training, Anomaly Detection, Divergence Detection.

• Unordered List ItemRandTree is available under services/RandTree/RandTree.mac, and provides the Tree interface (services/interfaces/TreeServiceClass.mh).
• MacePC requires the setup of a simulated application to run over RandTree and control the application signals (such as find peers, initiate join, etc.). For this purpose we have services/SimApplication/SimTreeApp.mac.
• Finally, all this is tied in with MacePC with the user-specified test framework which we call Service test, performing actions such as constructing the applications and initializing the nodes. Our Service test for RandTree is available in application/simulator_common/ServiceTests.h.
• The configuration parameters for MacePC is put in a file called params.default to be used with the binary. Place the following params.default file inside a folder for testing (e.g. RandTree_macepc).

MACE_PRINT_HOSTNAME_ONLY = 1
MACE_LOG_LEVEL = 1

USE_UDP_REORDER = 0
USE_UDP_ERRORS = 0
USE_NET_ERRORS = 0
SIM_NODE_FAILURE = 0

#Largely unimportant options
USE_BEST_FIRST = 0
MACE_PORT=10201
max_num_steps=80000
search_print_mask=0
PRINT_SEARCH_PREFIX=0
USE_RANDOM_WALKS=1
USE_GUSTO=1
USE_STATE_HASHES=0
NUM_RANDOM_PATHS=40

ALLOW_RAND_MAX = 1
TRACE_TRANSITION_TIMES = 1
USE_RANDOM_SEARCH = 1

#MIN_PATH_OUTLIER_DURATION = 18637
#MAX_PATH_OUTLIER_DURATION = 250000

COMPARE_CMC = 0
RUN_CMC_MEM = 0
RUN_DIVERGENCE_MONITOR = 0

divergence_assert = 1
divergence_timeout = 30

#RandTree
#How many nodes does the tree have?
num_nodes=5
queue_size=100000
CHECKED_SERVICE=RandTree

• In order for our scripts to work, set the MACE_SIMULATOR environment variable to the binary.

export MACE_SIMULATOR=/path/to/build/application/simulator/modelchecker

This step builds the Event Duration Distributions (EDD) that describe how long each type of event-transition takes to execute. The following command generates the raw event times for RandTree.

$MACE_SIMULATOR -MAX_PATHS 50 params.default

That should've generated transition_times.log. The following command generates the actual EDDs.

mace/application/simulator_common/makeDistributions.sh transition_times.log distributions.dat

Comment out the line TRACE_TRANSITION_TIMES=1 from params.default. The following command (executed from the same directory as distributions.dat and params.default) computes the outlier bounds from sample runs.

mace/application/simulator_common/train-outliers.pl

Set the values of Q1 and Q3 to MIN_PATH_OUTLIER_DURATION and MAX_PATH_OUTLIER_DURATION respectively (and un-comment those lines). As noted in the paper, the run-time for RandTree was not expected to be more than 250ms, and hence we use 250ms as the value for upper outlier threshold.

mace/application/simulator_common/run-modelchecker.pl

The above command initiates the MacePC search technique that searches the state space for executions whose times violate the Outlier durations. After it detects such a path, it performs divergence detection to find the critical transition that triggers this violation.

The outputs of the error path is available in error.log as a visual graph. Please refer to the Mace Modelchecker documentation on the usage of the mace debugger (mdb) and usage of the scripts.

• Mace Property Parser Cannot Parse *x