Note, much of the Mace Model Checker (MaceMC) documentation is also relevant to the performance checker. You may also wish to look there for more information MaceMC.
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
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.
services/RandTree/RandTree.mac, and provides the Tree interface (
params.defaultfile 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
MACE_SIMULATORenvironment variable to the binary.
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.
Set the values of Q1 and Q3 to
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.
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.