[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Pspp-cvs] pspp/src data/datasheet.c libpspp/model-checker... [simpler-p
|
From: |
Ben Pfaff |
|
Subject: |
[Pspp-cvs] pspp/src data/datasheet.c libpspp/model-checker... [simpler-proc] |
|
Date: |
Wed, 18 Apr 2007 05:07:32 +0000 |
CVSROOT: /cvsroot/pspp
Module name: pspp
Branch: simpler-proc
Changes by: Ben Pfaff <blp> 07/04/18 05:07:32
Modified files:
src/data : datasheet.c
src/libpspp : model-checker.c model-checker.h
Log message:
Document the model checker.
CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/pspp/src/data/datasheet.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.6&r2=1.1.2.7
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.3&r2=1.1.2.4
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.h?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.2&r2=1.1.2.3
Patches:
Index: data/datasheet.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/data/Attic/datasheet.c,v
retrieving revision 1.1.2.6
retrieving revision 1.1.2.7
diff -u -b -r1.1.2.6 -r1.1.2.7
--- data/datasheet.c 15 Apr 2007 05:15:17 -0000 1.1.2.6
+++ data/datasheet.c 18 Apr 2007 05:07:32 -0000 1.1.2.7
@@ -1100,7 +1100,7 @@
if (params->backing_rows == 0 && params->backing_cols == 0)
{
ds = datasheet_create (NULL);
- mc_name_state (mc, "empty datasheet");
+ mc_name_operation (mc, "empty datasheet");
check_datasheet (mc, ds, NULL, 0, 0);
}
else
@@ -1132,7 +1132,7 @@
assert (reader != NULL);
ds = datasheet_create (reader);
- mc_name_state (mc, "datasheet with (%d,%d) backing",
+ mc_name_operation (mc, "datasheet with (%d,%d) backing",
params->backing_rows, params->backing_cols);
check_datasheet (mc, ds, data,
params->backing_rows, params->backing_cols);
@@ -1161,7 +1161,7 @@
union value new[MAX_COLS];
size_t i, j;
- mc_name_state (mc, "insert %zu columns at %zu", cnt, pos);
+ mc_name_operation (mc, "insert %zu columns at %zu", cnt, pos);
clone_model (ods, odata, &ds, data);
for (i = 0; i < cnt; i++)
@@ -1189,7 +1189,7 @@
struct datasheet *ds;
size_t i;
- mc_name_state (mc, "delete %zu columns at %zu", cnt, pos);
+ mc_name_operation (mc, "delete %zu columns at %zu", cnt, pos);
clone_model (ods, odata, &ds, data);
datasheet_delete_columns (ds, pos, cnt);
@@ -1209,7 +1209,7 @@
size_t i;
clone_model (ods, odata, &ds, data);
- mc_name_state (mc, "move %zu columns from %zu to %zu",
+ mc_name_operation (mc, "move %zu columns from %zu to %zu",
cnt, pos, new_pos);
datasheet_move_columns (ds, pos, new_pos, cnt);
@@ -1230,7 +1230,7 @@
size_t i, j;
clone_model (ods, odata, &ds, data);
- mc_name_state (mc, "insert %zu rows at %zu", cnt, pos);
+ mc_name_operation (mc, "insert %zu rows at %zu", cnt, pos);
for (i = 0; i < cnt; i++)
{
@@ -1259,7 +1259,7 @@
struct datasheet *ds;
clone_model (ods, odata, &ds, data);
- mc_name_state (mc, "delete %zu rows at %zu", cnt, pos);
+ mc_name_operation (mc, "delete %zu rows at %zu", cnt, pos);
datasheet_delete_rows (ds, pos, cnt);
@@ -1276,8 +1276,8 @@
struct datasheet *ds;
clone_model (ods, odata, &ds, data);
- mc_name_state (mc,
- "move %zu rows from %zu to %zu", cnt, pos, new_pos);
+ mc_name_operation (mc, "move %zu rows from %zu to %zu",
+ cnt, pos, new_pos);
datasheet_move_rows (ds, pos, new_pos, cnt);
@@ -1289,7 +1289,7 @@
}
static void
-datasheet_mc_destroy (void *ds_)
+datasheet_mc_destroy (const struct mc *mc UNUSED, void *ds_)
{
struct datasheet *ds = ds_;
datasheet_destroy (ds);
Index: libpspp/model-checker.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.c,v
retrieving revision 1.1.2.3
retrieving revision 1.1.2.4
diff -u -b -r1.1.2.3 -r1.1.2.4
--- libpspp/model-checker.c 15 Apr 2007 05:15:17 -0000 1.1.2.3
+++ libpspp/model-checker.c 18 Apr 2007 05:07:32 -0000 1.1.2.4
@@ -38,64 +38,82 @@
#include "minmax.h"
#include "xalloc.h"
+/* Initializes PATH as an empty path. */
void
mc_path_init (struct mc_path *path)
{
- path->states = NULL;
+ path->ops = NULL;
path->length = 0;
path->capacity = 0;
}
+/* Copies the contents of OLD into NEW. */
void
mc_path_copy (struct mc_path *new, const struct mc_path *old)
{
if (old->length > new->capacity)
{
- new->capacity = old->length + 1;
- free (new->states);
- new->states = xnmalloc (new->capacity, sizeof *new->states);
+ new->capacity = old->length;
+ free (new->ops);
+ new->ops = xnmalloc (new->capacity, sizeof *new->ops);
}
new->length = old->length;
- memcpy (new->states, old->states, old->length * sizeof *new->states);
+ memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
}
+/* Adds OP to the end of PATH. */
void
-mc_path_push (struct mc_path *new, int new_state)
+mc_path_push (struct mc_path *path, int op)
{
- if (new->length >= new->capacity)
- new->states = xnrealloc (new->states,
- ++new->capacity, sizeof *new->states);
- new->states[new->length++] = new_state;
+ if (path->length >= path->capacity)
+ path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
+ path->ops[path->length++] = op;
}
-void
+/* Removes and returns the operation at the end of PATH. */
+int
mc_path_pop (struct mc_path *path)
{
- assert (path->length > 0);
+ int back = mc_path_back (path);
path->length--;
+ return back;
+}
+
+/* Returns the operation at the end of PATH. */
+int
+mc_path_back (const struct mc_path *path)
+{
+ assert (path->length > 0);
+ return path->ops[path->length - 1];
}
+/* Destroys PATH. */
void
mc_path_destroy (struct mc_path *path)
{
- free (path->states);
- path->states = NULL;
+ free (path->ops);
+ path->ops = NULL;
}
+/* Returns the operation in position INDEX in PATH.
+ INDEX must be less than the length of PATH. */
int
-mc_path_get_state (const struct mc_path *path, size_t index)
+mc_path_get_operation (const struct mc_path *path, size_t index)
{
assert (index < path->length);
- return path->states[index];
+ return path->ops[index];
}
+/* Returns the number of operations in PATH. */
size_t
mc_path_get_length (const struct mc_path *path)
{
return path->length;
}
-static void
+/* Appends the operations in PATH to STRING, separating each one
+ with a single space. */
+void
mc_path_to_string (const struct mc_path *path, struct string *string)
{
size_t i;
@@ -104,36 +122,47 @@
{
if (i > 0)
ds_put_char (string, ' ');
- ds_put_format (string, "%d", mc_path_get_state (path, i));
+ ds_put_format (string, "%d", mc_path_get_operation (path, i));
}
}
/* Search options. */
struct mc_options
{
- enum mc_strategy strategy;
- int max_depth;
- int hash_bits;
- unsigned int seed;
- struct mc_path follow_path;
+ /* Search strategy. */
+ enum mc_strategy strategy; /* Type of strategy. */
+ int max_depth; /* Limit on depth (or INT_MAX). */
+ int hash_bits; /* Number of bits to hash (or 0). */
+ unsigned int seed; /* Random seed for MC_RANDOM
+ or MC_DROP_RANDOM. */
+ struct mc_path follow_path; /* Path for MC_PATH. */
- int queue_limit;
+ /* Queue configuration. */
+ int queue_limit; /* Maximum length of queue. */
enum mc_queue_limit_strategy queue_limit_strategy;
+ /* How to choose state to drop
+ from queue. */
- int max_unique_states;
- int max_errors;
- double time_limit;
-
- int verbosity;
- int failure_verbosity;
- FILE *output_file;
-
- int progress_usec;
- mc_progress_func *progress_func;
+ /* Stop conditions. */
+ int max_unique_states; /* Maximum unique states to process. */
+ int max_errors; /* Maximum errors to detect. */
+ double time_limit; /* Maximum time in seconds. */
+
+ /* Output configuration. */
+ int verbosity; /* 0=low, 1=normal, 2+=high. */
+ int failure_verbosity; /* If greater than verbosity,
+ verbosity of error replays. */
+ FILE *output_file; /* File to receive output. */
+
+ /* How to report intermediate progress. */
+ int progress_usec; /* Microseconds between reports. */
+ mc_progress_func *progress_func; /* Function to call on each report. */
+ /* Client data. */
void *aux;
};
+/* Default progress function. */
static bool
default_progress (struct mc *mc)
{
@@ -144,12 +173,15 @@
return true;
}
+/* Do-nothing progress function. */
static bool
null_progress (struct mc *mc UNUSED)
{
return true;
}
+/* Creates and returns a set of options initialized to the
+ defaults. */
struct mc_options *
mc_options_create (void)
{
@@ -179,12 +211,14 @@
return options;
}
+/* Returns a copy of the given OPTIONS. */
struct mc_options *
mc_options_clone (const struct mc_options *options)
{
return xmemdup (options, sizeof *options);
}
+/* Destroys OPTIONS. */
void
mc_options_destroy (struct mc_options *options)
{
@@ -192,12 +226,37 @@
free (options);
}
+/* Returns the search strategy used for OPTIONS. The choices
+ are:
+
+ - MC_BROAD (the default): Breadth-first search. First tries
+ all the operations with depth 1, then those with depth 2,
+ then those with depth 3, and so on.
+
+ This search algorithm finds the least number of operations
+ needed to trigger a given bug.
+
+ - MC_DEEP: Depth-first search. Searches downward in the tree
+ of states as fast as possible. Good for finding bugs that
+ require long sequences of operations to trigger.
+
+ - MC_RANDOM: Random-first search. Searches through the tree
+ of states in random order. The standard C library's rand
+ function selects the search path; you can control the seed
+ passed to srand using mc_options_set_seed.
+
+ - MC_PATH: Explicit path. Applies an explicitly specified
+ sequence of operations. */
enum mc_strategy
mc_options_get_strategy (const struct mc_options *options)
{
return options->strategy;
}
+/* Sets the search strategy used for OPTIONS to STRATEGY.
+
+ This function cannot be used to set MC_PATH as the search
+ strategy. Use mc_options_set_follow_path instead. */
void
mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
{
@@ -207,36 +266,70 @@
options->strategy = strategy;
}
+/* Returns OPTION's random seed used by MC_RANDOM and
+ MC_DROP_RANDOM. */
unsigned int
mc_options_get_seed (const struct mc_options *options)
{
return options->seed;
}
+/* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
+ to SEED. */
void
mc_options_set_seed (struct mc_options *options, unsigned int seed)
{
options->seed = seed;
}
+/* Returns the maximum depth to which OPTIONS's search will
+ descend. The initial states are at depth 1, states produced
+ as their mutations are at depth 2, and so on. */
int
mc_options_get_max_depth (const struct mc_options *options)
{
return options->max_depth;
}
+/* Sets the maximum depth to which OPTIONS's search will descend
+ to MAX_DEPTH. The initial states are at depth 1, states
+ produced as their mutations are at depth 2, and so on. */
void
mc_options_set_max_depth (struct mc_options *options, int max_depth)
{
options->max_depth = max_depth;
}
+/* Returns the base-2 log of the number of bits in OPTIONS's hash
+ table. The hash table is used for dropping states that are
+ probably duplicates: any state with a given hash value, as
+ will only be processed once. A return value of 0 indicates
+ that the model checker will not discard duplicate states based
+ on their hashes.
+
+ The hash table is a power of 2 bits long, by default 2**20
+ bits (128 kB). Depending on how many states you expect the
+ model checker to check, how much memory you're willing to let
+ the hash table take up, and how worried you are about missing
+ states due to hash collisions, you could make it larger or
+ smaller.
+
+ The "birthday paradox" points to a reasonable way to size your
+ hash table. If you expect the model checker to check about
+ 2**N states, then, assuming a perfect hash, you need a hash
+ table of 2**(N+1) bits to have a 50% chance of seeing a hash
+ collision, 2**(N+2) bits to have a 25% chance, and so on. */
int
mc_options_get_hash_bits (const struct mc_options *options)
{
return options->hash_bits;
}
+/* Sets the base-2 log of the number of bits in OPTIONS's hash
+ table to HASH_BITS. A HASH_BITS value of 0 requests that the
+ model checker not discard duplicate states based on their
+ hashes. (This causes the model checker to never terminate in
+ many cases.) */
void
mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
{
@@ -244,6 +337,8 @@
options->hash_bits = MIN (hash_bits, 31);
}
+/* Returns the path set in OPTIONS by mc_options_set_follow_path.
+ May be used only if the search strategy is MC_PATH. */
const struct mc_path *
mc_options_get_follow_path (const struct mc_options *options)
{
@@ -251,6 +346,8 @@
return &options->follow_path;
}
+/* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
+ to be the explicit path specified in FOLLOW_PATH. */
void
mc_options_set_follow_path (struct mc_options *options,
const struct mc_path *follow_path)
@@ -260,12 +357,24 @@
mc_path_copy (&options->follow_path, follow_path);
}
+/* Returns the maximum number of queued states in OPTIONS. The
+ default value is 10,000. The primary reason to limit the
+ number of queued states is to conserve memory, so if you can
+ afford the memory and your model needs more room in the queue,
+ you can raise the limit. Conversely, if your models are large
+ or memory is constrained, you can reduce the limit.
+
+ Following the execution of the model checker, you can find out
+ the maximum queue length during the run by calling
+ mc_results_get_max_queue_length. */
int
mc_options_get_queue_limit (const struct mc_options *options)
{
return options->queue_limit;
}
+/* Sets the maximum number of queued states in OPTIONS to
+ QUEUE_LIMIT. */
void
mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
{
@@ -273,12 +382,31 @@
options->queue_limit = queue_limit;
}
+/* Returns the queue limit strategy used by OPTIONS, that is,
+ when a new state must be inserted into a full state queue is
+ full, how the state to be dropped is chosen. The choices are:
+
+ - MC_DROP_NEWEST: Drop the newest state; that is, do not
+ insert the new state into the queue at all.
+
+ - MC_DROP_OLDEST: Drop the state that has been enqueued for
+ the longest.
+
+ - MC_DROP_RANDOM (the default): Drop a randomly selected state
+ from the queue. The standard C library's rand function
+ selects the state to drop; you can control the seed passed
+ to srand using mc_options_set_seed. */
enum mc_queue_limit_strategy
mc_options_get_queue_limit_strategy (const struct mc_options *options)
{
return options->queue_limit_strategy;
}
+/* Sets the queue limit strategy used by OPTIONS to STRATEGY.
+
+ This setting has no effect unless the model being checked
+ causes the state queue to overflow (see
+ mc_options_get_queue_limit). */
void
mc_options_set_queue_limit_strategy (struct mc_options *options,
enum mc_queue_limit_strategy strategy)
@@ -289,12 +417,18 @@
options->queue_limit_strategy = strategy;
}
+/* Returns OPTIONS's maximum number of unique states that the
+ model checker will examine before terminating. The default is
+ INT_MAX. */
int
mc_options_get_max_unique_states (const struct mc_options *options)
{
return options->max_unique_states;
}
+/* Sets OPTIONS's maximum number of unique states that the model
+ checker will examine before terminating to
+ MAX_UNIQUE_STATE. */
void
mc_options_set_max_unique_states (struct mc_options *options,
int max_unique_states)
@@ -302,24 +436,37 @@
options->max_unique_states = max_unique_states;
}
+/* Returns the maximum number of errors that OPTIONS will allow
+ the model checker to encounter before terminating. The
+ default is 1. */
int
mc_options_get_max_errors (const struct mc_options *options)
{
return options->max_errors;
}
+/* Sets the maximum number of errors that OPTIONS will allow the
+ model checker to encounter before terminating to
+ MAX_ERRORS. */
void
mc_options_set_max_errors (struct mc_options *options, int max_errors)
{
options->max_errors = max_errors;
}
+/* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
+ model checker to consume before terminating. The
+ default of 0.0 means that time consumption is unlimited. */
double
mc_options_get_time_limit (const struct mc_options *options)
{
return options->time_limit;
}
+/* Sets the maximum amount of time, in seconds, that OPTIONS will
+ allow the model checker to consume before terminating to
+ TIME_LIMIT. A value of 0.0 means that time consumption is
+ unlimited; otherwise, the return value will be positive. */
void
mc_options_set_time_limit (struct mc_options *options, double time_limit)
{
@@ -327,24 +474,48 @@
options->time_limit = time_limit;
}
+/* Returns the level of verbosity for output messages specified
+ by OPTIONS. The default verbosity level is 1.
+
+ A verbosity level of 0 inhibits all messages except for
+ errors; a verbosity level of 1 also allows warnings; a
+ verbosity level of 2 also causes a description of each state
+ added to be output; a verbosity level of 3 also causes a
+ description of each duplicate state to be output. Verbosity
+ levels less than 0 or greater than 3 are allowed but currently
+ have no additional effect. */
int
mc_options_get_verbosity (const struct mc_options *options)
{
return options->verbosity;
}
+/* Sets the level of verbosity for output messages specified
+ by OPTIONS to VERBOSITY. */
void
mc_options_set_verbosity (struct mc_options *options, int verbosity)
{
options->verbosity = verbosity;
}
+/* Returns the level of verbosity for failures specified by
+ OPTIONS. The default failure verbosity level is 2.
+
+ The failure verbosity level has an effect only when an error
+ is reported, and only when the failure verbosity level is
+ higher than the regular verbosity level. When this is the
+ case, the model checker replays the error path at the higher
+ verbosity level specified. This has the effect of outputting
+ an explicit, human-readable description of the sequence of
+ operations that caused the error. */
int
mc_options_get_failure_verbosity (const struct mc_options *options)
{
return options->failure_verbosity;
}
+/* Sets the level of verbosity for failures specified by OPTIONS
+ to FAILURE_VERBOSITY. */
void
mc_options_set_failure_verbosity (struct mc_options *options,
int failure_verbosity)
@@ -352,12 +523,20 @@
options->failure_verbosity = failure_verbosity;
}
+/* Returns the output file used for messages printed by the model
+ checker specified by OPTIONS. The default is stdout. */
FILE *
mc_options_get_output_file (const struct mc_options *options)
{
return options->output_file;
}
+/* Sets the output file used for messages printed by the model
+ checker specified by OPTIONS to OUTPUT_FILE.
+
+ The model checker does not automatically close the specified
+ output file. If this is desired, the model checker's client
+ must do so. */
void
mc_options_set_output_file (struct mc_options *options,
FILE *output_file)
@@ -365,12 +544,19 @@
options->output_file = output_file;
}
+/* Returns the number of microseconds between calls to the
+ progress function specified by OPTIONS. The default is
+ 250,000 (1/4 second). A value of 0 disables progress
+ reporting. */
int
mc_options_get_progress_usec (const struct mc_options *options)
{
return options->progress_usec;
}
+/* Sets the number of microseconds between calls to the progress
+ function specified by OPTIONS to PROGRESS_USEC. A value of 0
+ disables progress reporting. */
void
mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
{
@@ -378,12 +564,26 @@
options->progress_usec = progress_usec;
}
+/* Returns the function called to report progress specified by
+ OPTIONS. The function used by default prints '.' to
+ stderr. */
mc_progress_func *
mc_options_get_progress_func (const struct mc_options *options)
{
return options->progress_func;
}
+/* Sets the function called to report progress specified by
+ OPTIONS to PROGRESS_FUNC. A non-null function must be
+ specified; to disable progress reporting, set the progress
+ reporting interval to 0.
+
+ PROGRESS_FUNC will be called zero or more times while the
+ model checker's run is ongoing. For these calls to the
+ progress function, mc_results_get_stop_reason will return
+ MC_CONTINUING. It will also be called exactly once soon
+ before mc_run returns, in which case
+ mc_results_get_stop_reason will return a different value. */
void
mc_options_set_progress_func (struct mc_options *options,
mc_progress_func *progress_func)
@@ -392,56 +592,67 @@
options->progress_func = progress_func;
}
+/* Returns the auxiliary data set in OPTIONS by the client. The
+ default is a null pointer.
+
+ This auxiliary data value can be retrieved by the
+ client-specified functions in struct mc_class during a model
+ checking run using mc_get_aux. */
void *
mc_options_get_aux (const struct mc_options *options)
{
return options->aux;
}
+/* Sets the auxiliary data in OPTIONS to AUX. */
void
mc_options_set_aux (struct mc_options *options, void *aux)
{
options->aux = aux;
}
-static void
-check_options (const struct mc_options *options)
-{
- assert (options->queue_limit_strategy != MC_DROP_OLDEST
- || options->strategy != MC_RANDOM);
-}
-
+/* Results of a model checking run. */
struct mc_results
{
- enum mc_stop_reason stop_reason;
- int unique_state_count;
- int error_count;
-
- int max_depth_reached;
- struct moments1 *depth_moments;
+ /* Overall results. */
+ enum mc_stop_reason stop_reason; /* Why the run ended. */
+ int unique_state_count; /* Number of unique states checked. */
+ int error_count; /* Number of errors found. */
+
+ /* Depth statistics. */
+ int max_depth_reached; /* Max depth state examined. */
+ struct moments1 *depth_moments; /* Enables reporting mean depth. */
+ /* If error_count > 0, path to the last error reported. */
struct mc_path error_path;
- int duplicate_dropped_states;
- int off_path_dropped_states;
- int depth_dropped_states;
- int queue_dropped_states;
- int queued_unprocessed_states;
- int max_queue_length;
-
- struct timeval start;
- struct timeval end;
+ /* States dropped... */
+ int duplicate_dropped_states; /* ...as duplicates. */
+ int off_path_dropped_states; /* ...as off-path (MC_PATH only). */
+ int depth_dropped_states; /* ...due to excessive depth. */
+ int queue_dropped_states; /* ...due to queue overflow. */
+
+ /* Queue statistics. */
+ int queued_unprocessed_states; /* Enqueued but never dequeued. */
+ int max_queue_length; /* Maximum queue length observed. */
+
+ /* Timing. */
+ struct timeval start; /* Start of model checking run. */
+ struct timeval end; /* End of model checking run. */
};
+/* Creates, initializes, and returns a new set of results. */
static struct mc_results *
mc_results_create (void)
{
struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
results->stop_reason = MC_CONTINUING;
results->depth_moments = moments1_create (MOMENT_MEAN);
+ gettimeofday (&results->start, NULL);
return results;
}
+/* Destroys RESULTS. */
void
mc_results_destroy (struct mc_results *results)
{
@@ -453,30 +664,66 @@
}
}
+/* Returns RESULTS's reason that the model checking run
+ terminated. The possible reasons are:
+
+ - MC_CONTINUING: The run is not actually yet complete. This
+ can only be returned before mc_run has returned, e.g. when
+ the progress function set by mc_options_set_progress_func
+ examines the run's results.
+
+ - MC_SUCCESS: The run completed because the queue emptied.
+ The entire state space might not have been explored due to a
+ requested limit on maximum depth, hash collisions, etc.
+
+ - MC_MAX_UNIQUE_STATES: The run completed because as many
+ unique states have been checked as were requested (using
+ mc_options_set_max_unique_states).
+
+ - MC_MAX_ERROR_COUNT: The run completed because the maximum
+ requested number of errors (by default, 1 error) was
+ reached.
+
+ - MC_END_OF_PATH: The run completed because the path specified
+ with mc_options_set_follow_path was fully traversed.
+
+ - MC_TIMEOUT: The run completed because the time limit set
+ with mc_options_set_time_limit was exceeded.
+
+ - MC_INTERRUPTED: The run completed because SIGINT was caught
+ (typically, due to the user typing Ctrl+C). */
enum mc_stop_reason
mc_results_get_stop_reason (const struct mc_results *results)
{
return results->stop_reason;
}
+/* Returns the number of unique states checked specified by
+ RESULTS. */
int
mc_results_get_unique_state_count (const struct mc_results *results)
{
return results->unique_state_count;
}
+/* Returns the number of errors found specified by RESULTS. */
int
mc_results_get_error_count (const struct mc_results *results)
{
return results->error_count;
}
+/* Returns the maximum depth reached during the model checker run
+ represented by RESULTS. The initial states are at depth 1,
+ their child states at depth 2, and so on. */
int
mc_results_get_max_depth_reached (const struct mc_results *results)
{
return results->max_depth_reached;
}
+/* Returns the mean depth reached during the model checker run
+ represented by RESULTS. */
double
mc_results_get_mean_depth_reached (const struct mc_results *results)
{
@@ -485,54 +732,87 @@
return mean != SYSMIS ? mean : 0.0;
}
+/* Returns the path traversed to obtain the last error
+ encountered during the model checker run represented by
+ RESULTS. Returns a null pointer if the run did not report any
+ errors. */
const struct mc_path *
mc_results_get_error_path (const struct mc_results *results)
{
return results->error_count > 0 ? &results->error_path : NULL;
}
+/* Returns the number of states dropped as duplicates (based on
+ hash value) during the model checker run represented by
+ RESULTS. */
int
mc_results_get_duplicate_dropped_states (const struct mc_results *results)
{
return results->duplicate_dropped_states;
}
+/* Returns the number of states dropped because they were off the
+ path specified by mc_options_set_follow_path during the model
+ checker run represented by RESULTS. A nonzero value here
+ indicates a missing call to mc_include_state in the
+ client-supplied mutation function. */
int
mc_results_get_off_path_dropped_states (const struct mc_results *results)
{
return results->off_path_dropped_states;
}
+/* Returns the number of states dropped because their depth
+ exceeded the maximum specified with mc_options_set_max_depth
+ during the model checker run represented by RESULTS. */
int
mc_results_get_depth_dropped_states (const struct mc_results *results)
{
return results->depth_dropped_states;
}
+/* Returns the number of states dropped from the queue due to
+ queue overflow during the model checker run represented by
+ RESULTS. */
int
mc_results_get_queue_dropped_states (const struct mc_results *results)
{
return results->queue_dropped_states;
}
+/* Returns the number of states that were checked and enqueued
+ but never dequeued and processed during the model checker run
+ represented by RESULTS. This is zero if the stop reason is
+ MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
+ states in the queue at the time that the checking run
+ stopped. */
int
mc_results_get_queued_unprocessed_states (const struct mc_results *results)
{
return results->queued_unprocessed_states;
}
+/* Returns the maximum length of the queue during the model
+ checker run represented by RESULTS. If this is equal to the
+ maximum queue length, then the queue (probably) overflowed
+ during the run; otherwise, it did not overflow. */
int
mc_results_get_max_queue_length (const struct mc_results *results)
{
return results->max_queue_length;
}
+/* Returns the time at which the model checker run represented by
+ RESULTS started. */
struct timeval
mc_results_get_start (const struct mc_results *results)
{
return results->start;
}
+/* Returns the time at which the model checker run represented by
+ RESULTS ended. (This function may not be called while the run
+ is still ongoing.) */
struct timeval
mc_results_get_end (const struct mc_results *results)
{
@@ -540,6 +820,8 @@
return results->end;
}
+/* Returns the number of seconds obtained by subtracting time Y
+ from time X. */
static double
timeval_subtract (struct timeval x, struct timeval y)
{
@@ -566,6 +848,10 @@
return difference;
}
+
+/* Returns the duration, in seconds, of the model checker run
+ represented by RESULTS. (This function may not be called
+ while the run is still ongoing.) */
double
mc_results_get_duration (const struct mc_results *results)
{
@@ -573,59 +859,310 @@
return timeval_subtract (results->end, results->start);
}
+/* An active model checking run. */
struct mc
{
+ /* Related data structures. */
const struct mc_class *class;
struct mc_options *options;
struct mc_results *results;
+ /* Array of 2**(options->hash_bits) bits representing states
+ already visited. */
unsigned char *hash;
- struct deque state_deque;
- struct mc_state **states;
- size_t follow_path_idx;
-
- struct mc_state *state;
- struct mc_path substate_path;
- struct string substate_path_string;
- int substate;
-
- bool named_state;
- bool error_state;
-
- unsigned int progress;
- unsigned int next_progress;
- unsigned int prev_progress;
- struct timeval prev_progress_time;
-
- bool interrupted;
- bool *saved_interrupted;
- sighandler_t saved_sigint;
+ /* State queue. */
+ struct mc_state **queue; /* Array of pointers to states. */
+ struct deque queue_deque; /* Deque. */
+
+ /* State currently being built by "init" or "mutate". */
+ struct mc_path path; /* Path to current state. */
+ struct string path_string; /* Buffer for path_string function. */
+ bool state_named; /* mc_name_operation called? */
+ bool state_error; /* mc_error called? */
+
+ /* Statistics for calling the progress function. */
+ unsigned int progress; /* Current progress value. */
+ unsigned int next_progress; /* Next value to call progress func. */
+ unsigned int prev_progress; /* Last value progress func called. */
+ struct timeval prev_progress_time; /* Last time progress func called. */
+
+ /* Information for handling and restoring SIGINT. */
+ bool interrupted; /* SIGINT received? */
+ bool *saved_interrupted_ptr; /* Saved value of interrupted_ptr. */
+ sighandler_t saved_sigint; /* Saved SIGINT handler. */
};
+/* A state in the queue. */
struct mc_state
{
- struct mc_path path;
- void *data;
+ struct mc_path path; /* Path to this state. */
+ void *data; /* Client-supplied data. */
};
+/* Points to the current struct mc's "interrupted" member. */
+static bool *interrupted_ptr = NULL;
+
+static const char *path_string (struct mc *);
+static void free_state (const struct mc *, struct mc_state *);
+static void stop (struct mc *, enum mc_stop_reason);
+static struct mc_state *make_state (const struct mc *, void *);
+static size_t random_queue_index (struct mc *);
+static void enqueue_state (struct mc *, struct mc_state *);
+static void do_error_state (struct mc *);
+static void next_operation (struct mc *);
+static bool is_off_path (const struct mc *);
+static void sigint_handler (int signum);
+static void init_mc (struct mc *,
+ const struct mc_class *, struct mc_options *);
+static void finish_mc (struct mc *);
+
+/* Runs the model checker on the client-specified CLASS with the
+ client-specified OPTIONS. OPTIONS may be a null pointer if
+ the defaults are acceptable. Destroys OPTIONS; use
+ mc_options_clone if a copy is needed.
+
+ Returns the results of the model checking run, which must be
+ destroyed by the client with mc_results_destroy.
+
+ To pass auxiliary data to the functions in CLASS, use
+ mc_options_set_aux on OPTIONS, which may be retrieved from the
+ CLASS functions using mc_get_aux. */
+struct mc_results *
+mc_run (const struct mc_class *class, struct mc_options *options)
+{
+ struct mc mc;
+
+ init_mc (&mc, class, options);
+ while (!deque_is_empty (&mc.queue_deque)
+ && mc.results->stop_reason == MC_CONTINUING)
+ {
+ struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
+ mc_path_copy (&mc.path, &state->path);
+ mc_path_push (&mc.path, 0);
+ class->mutate (&mc, state->data);
+ free_state (&mc, state);
+ if (mc.interrupted)
+ stop (&mc, MC_INTERRUPTED);
+ }
+ finish_mc (&mc);
+
+ return mc.results;
+}
+
+/* Tests whether the current operation is one that should be
+ performed, checked, and enqueued. If so, returns true.
+ Otherwise, returns false and, unless checking is stopped,
+ advances to the next state. The caller should then advance
+ to the next operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+bool
+mc_include_state (struct mc *mc)
+{
+ if (mc->results->stop_reason != MC_CONTINUING)
+ return false;
+ else if (is_off_path (mc))
+ {
+ next_operation (mc);
+ return false;
+ }
+ else
+ return true;
+}
+
+/* Tests whether HASH represents a state that has (probably)
+ already been enqueued. If not, returns false and marks HASH
+ so that it will be treated as a duplicate in the future. If
+ so, returns true and advances to the next state. The
+ caller should then advance to the next operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+bool
+mc_discard_dup_state (struct mc *mc, unsigned int hash)
+{
+ if (mc->options->hash_bits > 0)
+ {
+ hash &= (1u << mc->options->hash_bits) - 1;
+ if (TEST_BIT (mc->hash, hash))
+ {
+ if (mc->options->verbosity > 2)
+ fprintf (mc->options->output_file,
+ " [%s] discard duplicate state\n", path_string (mc));
+ mc->results->duplicate_dropped_states++;
+ next_operation (mc);
+ return true;
+ }
+ SET_BIT (mc->hash, hash);
+ }
+ return false;
+}
+
+/* Names the current state NAME, which may contain
+ printf-style format specifications. NAME should be a
+ human-readable name for the current operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_name_operation (struct mc *mc, const char *name, ...)
+{
+ va_list args;
+
+ va_start (args, name);
+ mc_vname_operation (mc, name, args);
+ va_end (args);
+}
+
+/* Names the current state NAME, which may contain
+ printf-style format specifications, for which the
+ corresponding arguments must be given in ARGS. NAME should be
+ a human-readable name for the current operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_vname_operation (struct mc *mc, const char *name, va_list args)
+{
+ if (mc->state_named && mc->options->verbosity > 0)
+ fprintf (mc->options->output_file, " [%s] warning: duplicate call "
+ "to mc_name_operation (missing call to mc_add_state?)\n",
+ path_string (mc));
+ mc->state_named = true;
+
+ if (mc->options->verbosity > 1)
+ {
+ fprintf (mc->options->output_file, " [%s] ", path_string (mc));
+ vfprintf (mc->options->output_file, name, args);
+ putc ('\n', mc->options->output_file);
+ }
+}
+
+/* Reports the given error MESSAGE for the current operation.
+ The resulting state should still be passed to mc_add_state
+ when all relevant error messages have been issued. The state
+ will not, however, be enqueued for later mutation of its own.
+
+ By default, model checking stops after the first error
+ encountered.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_error (struct mc *mc, const char *message, ...)
+{
+ va_list args;
+
+ if (mc->results->stop_reason != MC_CONTINUING)
+ return;
+
+ if (mc->options->verbosity > 1)
+ fputs (" ", mc->options->output_file);
+ fprintf (mc->options->output_file, "[%s] error: ",
+ path_string (mc));
+ va_start (args, message);
+ vfprintf (mc->options->output_file, message, args);
+ va_end (args);
+ putc ('\n', mc->options->output_file);
+
+ mc->state_error = true;
+}
+
+/* Enqueues DATA as the state corresponding to the current
+ operation. The operation should have been named with a call
+ to mc_name_operation, and it should have been checked by the
+ caller (who should have reported any errors with mc_error).
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_add_state (struct mc *mc, void *data)
+{
+ if (!mc->state_named && mc->options->verbosity > 0)
+ fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
+ path_string (mc));
+
+ if (mc->results->stop_reason != MC_CONTINUING)
+ {
+ /* Nothing to do. */
+ }
+ else if (mc->state_error)
+ do_error_state (mc);
+ else if (is_off_path (mc))
+ mc->results->off_path_dropped_states++;
+ else if (mc->path.length + 1 > mc->options->max_depth)
+ mc->results->depth_dropped_states++;
+ else
+ {
+ /* This is the common case. */
+ mc->results->unique_state_count++;
+ if (mc->results->unique_state_count >= mc->options->max_unique_states)
+ stop (mc, MC_MAX_UNIQUE_STATES);
+ enqueue_state (mc, make_state (mc, data));
+ next_operation (mc);
+ return;
+ }
+
+ mc->class->destroy (mc, data);
+ next_operation (mc);
+}
+
+/* Returns the options that were passed to mc_run for model
+ checker MC. */
+const struct mc_options *
+mc_get_options (struct mc *mc)
+{
+ return mc->options;
+}
+
+/* Returns the current state of the results for model checker
+ MC. This function is appropriate for use from the progress
+ function set by mc_options_set_progress_func.
+
+ Not all of the results are meaningful before model checking
+ completes. */
+const struct mc_results *
+mc_get_results (struct mc *mc)
+{
+ return mc->results;
+}
+
+/* Returns the auxiliary data set on the options passed to mc_run
+ with mc_options_set_aux. */
+void *
+mc_get_aux (struct mc *mc)
+{
+ return mc_options_get_aux (mc_get_options (mc));
+}
+
+/* Expresses MC->path as a string and returns the string. */
static const char *
-substate_path_string (struct mc *mc)
+path_string (struct mc *mc)
{
- ds_clear (&mc->substate_path_string);
- mc_path_to_string (&mc->substate_path, &mc->substate_path_string);
- return ds_cstr (&mc->substate_path_string);
+ ds_clear (&mc->path_string);
+ mc_path_to_string (&mc->path, &mc->path_string);
+ return ds_cstr (&mc->path_string);
}
+/* Frees STATE, including client data. */
static void
-free_state (const struct mc_class *class, struct mc_state *state)
+free_state (const struct mc *mc, struct mc_state *state)
{
- if (state->data != NULL)
- class->destroy (state->data);
+ mc->class->destroy (mc, state->data);
mc_path_destroy (&state->path);
free (state);
}
+/* Sets STOP_REASON as the reason that MC's processing stopped,
+ unless MC is already stopped. */
static void
stop (struct mc *mc, enum mc_stop_reason stop_reason)
{
@@ -633,24 +1170,30 @@
mc->results->stop_reason = stop_reason;
}
+/* Creates and returns a new state whose path is copied from
+ MC->path and whose data is specified by DATA. */
static struct mc_state *
-make_child_state (const struct mc *mc, void *data)
+make_state (const struct mc *mc, void *data)
{
struct mc_state *new = xmalloc (sizeof *new);
mc_path_init (&new->path);
- mc_path_copy (&new->path, &mc->substate_path);
+ mc_path_copy (&new->path, &mc->path);
new->data = data;
return new;
}
+/* Returns the index in MC->queue of a random element in the
+ queue. */
static size_t
random_queue_index (struct mc *mc)
{
- assert (!deque_is_empty (&mc->state_deque));
- return deque_front (&mc->state_deque,
- rand () % deque_count (&mc->state_deque));
+ assert (!deque_is_empty (&mc->queue_deque));
+ return deque_front (&mc->queue_deque,
+ rand () % deque_count (&mc->queue_deque));
}
+/* Adds NEW to MC's state queue, dropping a state if necessary
+ due to overflow. */
static void
enqueue_state (struct mc *mc, struct mc_state *new)
{
@@ -660,65 +1203,64 @@
mc->results->max_depth_reached = new->path.length;
moments1_add (mc->results->depth_moments, new->path.length, 1.0);
- if (deque_count (&mc->state_deque) < mc->options->queue_limit)
+ if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
{
/* Add new state to queue. */
- if (deque_is_full (&mc->state_deque))
- mc->states = deque_expand (&mc->state_deque,
- mc->states, sizeof *mc->states);
+ if (deque_is_full (&mc->queue_deque))
+ mc->queue = deque_expand (&mc->queue_deque,
+ mc->queue, sizeof *mc->queue);
switch (mc->options->strategy)
{
case MC_BROAD:
- idx = deque_push_back (&mc->state_deque);
+ idx = deque_push_back (&mc->queue_deque);
break;
case MC_DEEP:
- idx = deque_push_front (&mc->state_deque);
+ idx = deque_push_front (&mc->queue_deque);
break;
case MC_RANDOM:
- if (!deque_is_empty (&mc->state_deque))
+ if (!deque_is_empty (&mc->queue_deque))
{
idx = random_queue_index (mc);
- mc->states[deque_push_front (&mc->state_deque)]
- = mc->states[idx];
+ mc->queue[deque_push_front (&mc->queue_deque)]
+ = mc->queue[idx];
}
else
- idx = deque_push_front (&mc->state_deque);
+ idx = deque_push_front (&mc->queue_deque);
break;
case MC_PATH:
- assert (deque_is_empty (&mc->state_deque));
- assert (mc->substate == mc_path_get_state (&mc->options->follow_path,
- mc->state->path.length));
- idx = deque_push_back (&mc->state_deque);
- if (mc->state->path.length + 1
+ assert (deque_is_empty (&mc->queue_deque));
+ assert (!is_off_path (mc));
+ idx = deque_push_back (&mc->queue_deque);
+ if (mc->path.length
>= mc_path_get_length (&mc->options->follow_path))
stop (mc, MC_END_OF_PATH);
break;
default:
NOT_REACHED ();
}
- if (deque_count (&mc->state_deque) > mc->results->max_queue_length)
- mc->results->max_queue_length = deque_count (&mc->state_deque);
+ if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
+ mc->results->max_queue_length = deque_count (&mc->queue_deque);
}
else
{
/* Queue has reached limit, so replace an existing
state. */
assert (mc->options->strategy != MC_PATH);
- assert (!deque_is_empty (&mc->state_deque));
+ assert (!deque_is_empty (&mc->queue_deque));
mc->results->queue_dropped_states++;
switch (mc->options->queue_limit_strategy)
{
case MC_DROP_NEWEST:
- free_state (mc->class, new);
+ free_state (mc, new);
return;
case MC_DROP_OLDEST:
switch (mc->options->strategy)
{
case MC_BROAD:
- idx = deque_front (&mc->state_deque, 0);
+ idx = deque_front (&mc->queue_deque, 0);
break;
case MC_DEEP:
- idx = deque_back (&mc->state_deque, 0);
+ idx = deque_back (&mc->queue_deque, 0);
break;
case MC_RANDOM:
case MC_PATH:
@@ -732,11 +1274,12 @@
default:
NOT_REACHED ();
}
- free_state (mc->class, mc->states[idx]);
+ free_state (mc, mc->queue[idx]);
}
- mc->states[idx] = new;
+ mc->queue[idx] = new;
}
+/* Process an error state being added to MC. */
static void
do_error_state (struct mc *mc)
{
@@ -744,18 +1287,18 @@
if (mc->results->error_count >= mc->options->max_errors)
stop (mc, MC_MAX_ERROR_COUNT);
- mc_path_copy (&mc->results->error_path, &mc->substate_path);
+ mc_path_copy (&mc->results->error_path, &mc->path);
if (mc->options->failure_verbosity > mc->options->verbosity)
{
struct mc_options *path_options;
fprintf (mc->options->output_file, "[%s] retracing error path:\n",
- substate_path_string (mc));
+ path_string (mc));
path_options = mc_options_clone (mc->options);
mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
mc_options_set_failure_verbosity (path_options, 0);
- mc_options_set_follow_path (path_options, &mc->substate_path);
+ mc_options_set_follow_path (path_options, &mc->path);
mc_results_destroy (mc_run (mc->class, path_options));
@@ -763,41 +1306,14 @@
}
}
-void
-mc_vname_state (struct mc *mc, const char *name, va_list args)
-{
- if (mc->named_state)
- fprintf (mc->options->output_file, " [%s] warning: duplicate call "
- "to mc_name_state (missing call to mc_add_state?)\n",
- substate_path_string (mc));
- mc->named_state = true;
-
- if (mc->options->verbosity > 1)
- {
- fprintf (mc->options->output_file, " [%s] ", substate_path_string (mc));
- vfprintf (mc->options->output_file, name, args);
- putc ('\n', mc->options->output_file);
- }
-}
-
-void
-mc_name_state (struct mc *mc, const char *name, ...)
-{
- va_list args;
-
- va_start (args, name);
- mc_vname_state (mc, name, args);
- va_end (args);
-}
-
+/* Advances MC to start processing the operation following the
+ current one. */
static void
-next_substate (struct mc *mc)
+next_operation (struct mc *mc)
{
- mc->substate++;
- mc_path_pop (&mc->substate_path);
- mc_path_push (&mc->substate_path, mc->substate);
- mc->error_state = false;
- mc->named_state = false;
+ mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
+ mc->state_error = false;
+ mc->state_named = false;
if (++mc->progress >= mc->next_progress)
{
@@ -842,117 +1358,65 @@
}
}
-bool
-mc_discard_dup_state (struct mc *mc, unsigned int hash)
-{
- if (mc->options->hash_bits > 0)
- {
- hash &= (1u << mc->options->hash_bits) - 1;
- if (TEST_BIT (mc->hash, hash))
- {
- if (mc->options->verbosity > 2)
- fprintf (mc->options->output_file,
- " [%s] discard duplicate state\n",
- substate_path_string (mc));
- mc->results->duplicate_dropped_states++;
- next_substate (mc);
- return true;
- }
- SET_BIT (mc->hash, hash);
- }
- return false;
-}
-
+/* Returns true if we're tracing an explicit path but the current
+ operation produces a state off that path, false otherwise. */
static bool
is_off_path (const struct mc *mc)
{
return (mc->options->strategy == MC_PATH
- && mc->substate != mc_path_get_state (&mc->options->follow_path,
- mc->state->path.length));
-}
-
-void
-mc_add_state (struct mc *mc, void *data)
-{
- if (!mc->named_state)
- fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
- substate_path_string (mc));
-
- if (mc->results->stop_reason != MC_CONTINUING)
- {
- /* Nothing to do. */
- }
- else if (mc->error_state)
- do_error_state (mc);
- else if (is_off_path (mc))
- mc->results->off_path_dropped_states++;
- else if (mc->state->path.length + 1 > mc->options->max_depth)
- mc->results->depth_dropped_states++;
- else
- {
- /* This is the common case. */
- mc->results->unique_state_count++;
- if (mc->results->unique_state_count >= mc->options->max_unique_states)
- stop (mc, MC_MAX_UNIQUE_STATES);
- enqueue_state (mc, make_child_state (mc, data));
- next_substate (mc);
- return;
- }
-
- mc->class->destroy (data);
- next_substate (mc);
+ && (mc_path_back (&mc->path)
+ != mc_path_get_operation (&mc->options->follow_path,
+ mc->path.length - 1)));
}
-static bool *interrupted = NULL;
-
+/* Handler for SIGINT. */
static void
sigint_handler (int signum UNUSED)
{
- *interrupted = true;
+ /* Just mark the model checker as interrupted. */
+ *interrupted_ptr = true;
}
+/* Initializes MC as a model checker with the given CLASS and
+ OPTIONS. OPTIONS may be null to use the default options. */
static void
init_mc (struct mc *mc, const struct mc_class *class,
struct mc_options *options)
{
- struct mc_state null_state = { { NULL, 0 }, NULL };
-
- mc->class = class;
-
- mc->options = options != NULL ? options : mc_options_create ();
- check_options (mc->options);
-
- if (mc->options->strategy == MC_PATH)
+ /* Validate and adjust OPTIONS. */
+ if (options == NULL)
+ options = mc_options_create ();
+ assert (options->queue_limit_strategy != MC_DROP_OLDEST
+ || options->strategy != MC_RANDOM);
+ if (options->strategy == MC_PATH)
{
- mc->options->max_depth = INT_MAX;
- mc->options->hash_bits = 0;
+ options->max_depth = INT_MAX;
+ options->hash_bits = 0;
}
-
- if (mc->options->progress_usec == 0)
+ if (options->progress_usec == 0)
{
- mc->options->progress_func = null_progress;
- if (mc->options->time_limit > 0.0)
- mc->options->progress_usec = 250000;
+ options->progress_func = null_progress;
+ if (options->time_limit > 0.0)
+ options->progress_usec = 250000;
}
+ /* Initialize MC. */
+ mc->class = class;
+ mc->options = options;
mc->results = mc_results_create ();
- gettimeofday (&mc->results->start, NULL);
-
- if (mc->options->hash_bits > 0)
- mc->hash = xcalloc (1, (1u << mc->options->hash_bits) / CHAR_BIT);
- else
- mc->hash = NULL;
- mc->states = NULL;
- deque_init_null (&mc->state_deque);
-
- mc->substate = 0;
- mc_path_init (&mc->substate_path);
- mc_path_push (&mc->substate_path, mc->substate);
- ds_init_empty (&mc->substate_path_string);
- mc->state = &null_state;
- mc->named_state = false;
- mc->error_state = false;
+ mc->hash = (mc->options->hash_bits > 0
+ ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
+ : NULL);
+
+ mc->queue = NULL;
+ deque_init_null (&mc->queue_deque);
+
+ mc_path_init (&mc->path);
+ mc_path_push (&mc->path, 0);
+ ds_init_empty (&mc->path_string);
+ mc->state_named = false;
+ mc->state_error = false;
mc->progress = 0;
mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
@@ -964,115 +1428,40 @@
srand (mc->options->seed);
mc->interrupted = false;
- mc->saved_interrupted = interrupted;
- interrupted = &mc->interrupted;
+ mc->saved_interrupted_ptr = interrupted_ptr;
+ interrupted_ptr = &mc->interrupted;
mc->saved_sigint = signal (SIGINT, sigint_handler);
class->init (mc);
}
+/* Complete the model checker run for MC. */
static void
finish_mc (struct mc *mc)
{
+ /* Restore signal handlers. */
signal (SIGINT, mc->saved_sigint);
- interrupted = mc->saved_interrupted;
+ interrupted_ptr = mc->saved_interrupted_ptr;
+ /* Mark the run complete. */
stop (mc, MC_SUCCESS);
gettimeofday (&mc->results->end, NULL);
- mc->results->queued_unprocessed_states = deque_count (&mc->state_deque);
- while (!deque_is_empty (&mc->state_deque))
+ /* Empty the queue. */
+ mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
+ while (!deque_is_empty (&mc->queue_deque))
{
- struct mc_state *state = mc->states[deque_pop_front (&mc->state_deque)];
- free_state (mc->class, state);
+ struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
+ free_state (mc, state);
}
+ /* Notify the progress function of completion. */
mc->options->progress_func (mc);
- mc_path_destroy (&mc->substate_path);
- ds_destroy (&mc->substate_path_string);
+ /* Free memory. */
+ mc_path_destroy (&mc->path);
+ ds_destroy (&mc->path_string);
free (mc->options);
- free (mc->states);
+ free (mc->queue);
free (mc->hash);
}
-
-static void
-periodic_mc (struct mc *mc)
-{
- if (mc->interrupted)
- stop (mc, MC_INTERRUPTED);
-}
-
-struct mc_results *
-mc_run (const struct mc_class *class, struct mc_options *options)
-{
- struct mc mc;
-
- init_mc (&mc, class, options);
- while (!deque_is_empty (&mc.state_deque)
- && mc.results->stop_reason == MC_CONTINUING)
- {
- mc.substate = 0;
- mc.state = mc.states[deque_pop_front (&mc.state_deque)];
- mc_path_copy (&mc.substate_path, &mc.state->path);
- mc_path_push (&mc.substate_path, mc.substate);
- class->mutate (&mc, mc.state->data);
- free_state (class, mc.state);
- periodic_mc (&mc);
- }
- finish_mc (&mc);
-
- return mc.results;
-}
-
-void
-mc_error (struct mc *mc, const char *message, ...)
-{
- va_list args;
-
- if (mc->results->stop_reason != MC_CONTINUING)
- return;
-
- if (mc->options->verbosity > 1)
- fputs (" ", mc->options->output_file);
- fprintf (mc->options->output_file, "[%s] error: ",
- substate_path_string (mc));
- va_start (args, message);
- vfprintf (mc->options->output_file, message, args);
- va_end (args);
- putc ('\n', mc->options->output_file);
-
- mc->error_state = true;
-}
-
-bool
-mc_include_state (struct mc *mc)
-{
- if (mc->results->stop_reason != MC_CONTINUING)
- return false;
- else if (is_off_path (mc))
- {
- next_substate (mc);
- return false;
- }
- else
- return true;
-}
-
-const struct mc_options *
-mc_get_options (struct mc *mc)
-{
- return mc->options;
-}
-
-const struct mc_results *
-mc_get_results (struct mc *mc)
-{
- return mc->results;
-}
-
-void *
-mc_get_aux (struct mc *mc)
-{
- return mc_options_get_aux (mc_get_options (mc));
-}
Index: libpspp/model-checker.h
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.h,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -u -b -r1.1.2.2 -r1.1.2.3
--- libpspp/model-checker.h 15 Apr 2007 05:15:17 -0000 1.1.2.2
+++ libpspp/model-checker.h 18 Apr 2007 05:07:32 -0000 1.1.2.3
@@ -16,6 +16,284 @@
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
02110-1301, USA. */
+/* Implementation-level model checker.
+
+ A model checker is a tool for software testing and
+ verification that works by exploring all the possible states
+ in a system and verifying their internal consistency. A
+ conventional model checker requires that the code in a system
+ be translated into a specification language. The model
+ checker then verifies the specification, rather than the code.
+
+ This is instead an implementation-level model checker, which
+ does not require a separate specification. Instead, the model
+ checker requires writing a second implementation of the system
+ being checked. The second implementation can usually be made
+ almost trivial in comparison to the one being checked, because
+ it's usually acceptable for its performance to be
+ comparatively poor, e.g. O(N^2) instead of O(lg N), and thus
+ to use much simpler algorithms.
+
+ For introduction to the implementation-level model checking
+ approach used here, please refer to the following papers:
+
+ Musuvathi, Park, Chou, Engler, Dill, "CMC: A Pragmatic
+ Approach to Model Checking Real Code", Proceedings of the
+ Fifth Symposium on Operating Systems Design and
+ Implementation (OSDI), Dec 2002.
+ http://sprout.stanford.edu/PAPERS/CMC-OSDI-2002/CMC-OSDI-2002.pdf
+
+ Yang, Twohey, Engler, Musuvathi, "Using Model Checking to
+ Find Serious File System Errors", Proceedings of the Sixth
+ Symposium on Operating System Design and Implementation
+ (OSDI), Dec 2004.
+ http://www.stanford.edu/~engler/osdi04-fisc.pdf
+
+ Yang, Twohey, Pfaff, Sar, Engler, "EXPLODE: A Lightweight,
+ General Approach to Finding Serious Errors in Storage
+ Systems", First Workshop on the Evaluation of Software
+ Defect Detection Tools (BUGS), June 2005.
+ http://www.stanford.edu/~blp/papers/explode.pdf
+
+ Use of a model checker is appropriate when the system being
+ checked is difficult to test using handwritten tests. This
+ can be the case, for example, when the system has a
+ complicated internal state that is difficult to reason about
+ over a long series of operations.
+
+ The implementation model checker works by putting a set of one
+ of more initial states in a queue (and checking them for
+ consistency). Then the model checker removes a state from the
+ queue and applies all possible operations of interest to it
+ ("mutates" it), obtaining a set of zero or more child states
+ (and checking each of them for consistency). Each of these
+ states is itself added to the queue. The model checker
+ continues dequeuing states and mutating and checking them
+ until the queue is empty.
+
+ In pseudo-code, the process looks like this:
+
+ Q = { initial states }
+ while Q is not empty:
+ S = dequeue(Q)
+ for each operation applicable to S do:
+ T = operation(S)
+ check(T)
+ enqueue(Q, T)
+
+ In many cases this process will never terminate, because every
+ state has one or more child states. For some systems this is
+ unavoidable, but in others we can make the process finite by
+ pursuing a few stratagems:
+
+ 1. Limit the maximum size of the system; for example, limit
+ the number of rows and columns in the implmentation of a
+ table being checked. The client of the model checker is
+ responsible for implementing such limits.
+
+ 2. Avoid checking a single state more than one time. This
+ model checker provides assistance for this function by
+ allowing the client to provide a hash of the system state.
+ States with identical hashes will only be checked once
+ during a single run.
+
+ When a system cannot be made finite, or when a finite system
+ is too large to check in a practical amount of time, the model
+ checker provides multiple ways to limit the checking run:
+ based on maximum depth, maximum unique states checked, maximum
+ errors found (by default, 1), or maximum time used for
+ checking.
+
+ The client of the model checker must provide three functions
+ via function pointers embedded into a "struct mc_class":
+
+ 1. void init (struct mc *mc);
+
+ This function is called once at the beginning of a
+ checking run. It checks one or more initial states and
+ adds them to the model checker's queue. (If it does not
+ add any states to the queue, then there is nothing to
+ check.)
+
+ Here's an outline for writing the init function:
+
+ void
+ init_foo (struct mc *mc)
+ {
+ struct foo *foo;
+
+ mc_name_operation (mc, "initial state");
+ foo = generate_initial_foo ();
+ if (!state_is_consistent (foo))
+ mc_error (mc, "inconsistent state");
+ mc_add_state (mc, foo);
+ }
+
+ 2. void mutate (struct mc *mc, const void *data);
+
+ This function is called when a dequeued state is ready to
+ be mutated. For each operation that can be applied to
+ the client-specified DATA, it applies that operation to a
+ clone of the DATA, checks that the clone is consistent,
+ and adds the clone to the model checker's queue.
+
+ Here's an outline for writing the mutate function:
+
+ void
+ mutate_foo (struct mc *mc, void *state_)
+ {
+ struct foo *state = state_;
+
+ for (...each operation...)
+ if (mc_include_state (mc))
+ {
+ struct foo *clone;
+
+ mc_name_operation (mc, "do operation %s", ...);
+ clone = clone_foo (state);
+ do_operation (clone);
+ if (!mc_discard_dup_state (mc, hash_foo (clone)))
+ {
+ if (!state_is_consistent (clone))
+ mc_error (mc, "inconsistent state");
+ mc_add_state (mc, clone);
+ }
+ else
+ destroy_foo (clone);
+ }
+ }
+
+ Notes on the above outline:
+
+ - The call to mc_include_state allows currently
+ uninteresting operations to be skipped. It is not
+ essential.
+
+ - The call to mc_name_operation should give the current
+ operation a human-readable name. The name may
+ include printf-style format specifications.
+
+ When an error occurs, the model checker (by default)
+ replays the sequence of operations performed to reach
+ the error, printing the name of the operation at each
+ step, which is often sufficient information in itself
+ to debug the error.
+
+ At higher levels of verbosity, the name is printed
+ for each operation.
+
+ - Operations should be performed on a copy of the data
+ provided. The data provided should not be destroyed
+ or modified.
+
+ - The call to mc_discard_dup_state is needed to discard
+ (probably) duplicate states. It is otherwise
+ optional.
+
+ To reduce the probability of collisions, use a
+ high-quality hash function. MD4 is a reasonable
+ choice: it is fast but high-quality. In one test,
+ switching to MD4 from MD5 increased overall speed of
+ model checking by 8% and actually reduced (!) the
+ number of collisions.
+
+ The hash value needs to include enough of the state
+ to ensure that interesting states are not excluded,
+ but it need not include the entire state. For
+ example, in many cases, the structure of complex data
+ (metadata) is often much more important than the
+ contents (data), so it may be reasonable to hash only
+ the metadata.
+
+ mc_discard_dup_state may be called before or after
+ checking for consistency, but calling it first avoids
+ wasting time checking duplicate states for
+ consistency, which again can be a significant
+ performance boost.
+
+ - The mc_error function reports errors. It may be
+ called as many times as desired to report each kind
+ of inconsistency in a state.
+
+ - The mc_add_state function adds the new state to the
+ queue. It should be called regardless of whether an
+ error was reported, to indicate to the model checker
+ that state processing has finished.
+
+ - The mutation function should be deterministic, to
+ make it possible to reliably reproduce errors.
+
+ 3. void destroy (struct mc *mc, void *data);
+
+ This function is called to discard the client-specified
+ DATA associated with a state.
+
+ Numerous options are available for configuring the model
+ checker. The most important of these are:
+
+ - Search algorithm:
+
+ * Breadth-first search (the default): First try all the
+ operations with depth 1, then those with depth 2, then
+ those with depth 3, and so on.
+
+ This search algorithm finds the least number of
+ operations needed to trigger a given bug.
+
+ * Depth-first search: Searches downward in the tree of
+ states as fast as possible. Good for finding bugs that
+ require long sequences of operations to trigger.
+
+ * Random-first search: Searches through the tree of
+ states in random order.
+
+ * Explicit path: Applies an explicitly specified sequence
+ of operations.
+
+ - Verbosity: By default, messages are printed only when an
+ error is encountered, but you can cause the checker to
+ print a message on every state transition. This is most
+ useful when the errors in your code cause segfaults or
+ some other kind of sudden termination.
+
+ - Treatment of errors: By default, when an error is
+ encountered, the model checker recursively invokes itself
+ with an increased verbosity level and configured to follow
+ only the error path. As long as the mutation function is
+ deterministic, this quickly and concisely replays the
+ error and describes the path followed to reach it in an
+ easily human-readable manner.
+
+ - Limits:
+
+ * Maximum depth: You can limit the depth of the operations
+ performed. Most often useful with depth-first search.
+ By default, depth is unlimited.
+
+ * Maximum queue length: You can limit the number of states
+ kept in the queue at any given time. The main reason to
+ do so is to limit memory consumption. The default
+ limit is 10,000 states. Several strategies are
+ available for choosing which state to drop when the
+ queue overflows.
+
+ - Stop conditions: based on maximum unique states checked,
+ maximum errors found (by default, 1), or maximum time used
+ for checking.
+
+ - Progress: by default, the checker prints a '.' on stderr
+ every .25 seconds, but you can substitute another progress
+ function or disable progress printing.
+
+ This model checker does not (yet) include two features
+ described in the papers cited above: utility scoring
+ heuristics to guide the search strategy and "choice points" to
+ explore failure cases. The former feature is less interesting
+ for this model checker, because the data structures we are
+ thus far using it to model are much smaller than those
+ discussed in the paper. The latter feature we should
+ implement at some point. */
+
#ifndef LIBPSPP_MODEL_CHECKER_H
#define LIBPSPP_MODEL_CHECKER_H 1
@@ -26,6 +304,7 @@
#include <libpspp/compiler.h>
+/* An active model checking run. */
struct mc;
/* Provided by each client of the model checker. */
@@ -33,25 +312,56 @@
{
void (*init) (struct mc *);
void (*mutate) (struct mc *, const void *);
- void (*destroy) (void *);
+ void (*destroy) (const struct mc *, void *);
};
+/* Results of a model checking run. */
+struct mc_results;
+
+/* Configuration for running the model checker. */
+struct mc_options;
+
+/* Primary external interface to model checker. */
+struct mc_results *mc_run (const struct mc_class *, struct mc_options *);
+
+/* Functions for use from client-supplied "init" and "mutate"
+ functions. */
+bool mc_include_state (struct mc *);
+bool mc_discard_dup_state (struct mc *, unsigned int hash);
+void mc_name_operation (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3);
+void mc_vname_operation (struct mc *, const char *, va_list)
+ PRINTF_FORMAT (2, 0);
+void mc_error (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3);
+void mc_add_state (struct mc *, void *data);
+
+/* Functions for use from client-supplied "init", "mutate", and
+ "destroy" functions. */
+const struct mc_options *mc_get_options (struct mc *);
+const struct mc_results *mc_get_results (struct mc *);
+void *mc_get_aux (struct mc *);
+
+/* A path of operations through a model to arrive at some
+ particular state. */
struct mc_path
{
- int *states;
- size_t length;
- size_t capacity;
+ int *ops; /* Sequence of operations. */
+ size_t length; /* Number of operations. */
+ size_t capacity; /* Number of operations for which room is allocated. */
};
void mc_path_init (struct mc_path *);
void mc_path_copy (struct mc_path *, const struct mc_path *);
void mc_path_push (struct mc_path *, int new_state);
-void mc_path_pop (struct mc_path *);
+int mc_path_pop (struct mc_path *);
+int mc_path_back (const struct mc_path *);
void mc_path_destroy (struct mc_path *);
-int mc_path_get_state (const struct mc_path *, size_t index);
+int mc_path_get_operation (const struct mc_path *, size_t index);
size_t mc_path_get_length (const struct mc_path *);
+struct string;
+void mc_path_to_string (const struct mc_path *, struct string *);
+
struct mc_options *mc_options_create (void);
struct mc_options *mc_options_clone (const struct mc_options *);
void mc_options_destroy (struct mc_options *);
@@ -67,7 +377,6 @@
enum mc_strategy mc_options_get_strategy (const struct mc_options *);
void mc_options_set_strategy (struct mc_options *, enum mc_strategy);
-const struct mc_path *mc_options_get_follow_path (const struct mc_options *);
unsigned int mc_options_get_seed (const struct mc_options *);
void mc_options_set_seed (struct mc_options *, unsigned int seed);
int mc_options_get_max_depth (const struct mc_options *);
@@ -75,13 +384,16 @@
int mc_options_get_hash_bits (const struct mc_options *);
void mc_options_set_hash_bits (struct mc_options *, int hash_bits);
+const struct mc_path *mc_options_get_follow_path (const struct mc_options *);
void mc_options_set_follow_path (struct mc_options *, const struct mc_path *);
+/* Strategy for dropped states from the queue when it
+ overflows. */
enum mc_queue_limit_strategy
{
- MC_DROP_NEWEST,
- MC_DROP_OLDEST,
- MC_DROP_RANDOM
+ MC_DROP_NEWEST, /* Don't enqueue the new state at all. */
+ MC_DROP_OLDEST, /* Drop the oldest state in the queue. */
+ MC_DROP_RANDOM /* Drop a random state from the queue. */
};
int mc_options_get_queue_limit (const struct mc_options *);
@@ -116,19 +428,18 @@
void *mc_options_get_aux (const struct mc_options *);
void mc_options_set_aux (struct mc_options *, void *aux);
+/* Reason that a model checking run terminated. */
enum mc_stop_reason
{
- MC_CONTINUING,
- MC_SUCCESS,
- MC_MAX_UNIQUE_STATES,
- MC_MAX_ERROR_COUNT,
- MC_END_OF_PATH,
- MC_TIMEOUT,
- MC_INTERRUPTED
+ MC_CONTINUING, /* Run has not yet terminated. */
+ MC_SUCCESS, /* Queue emptied (ran out of states). */
+ MC_MAX_UNIQUE_STATES, /* Did requested number of unique states. */
+ MC_MAX_ERROR_COUNT, /* Too many errors. */
+ MC_END_OF_PATH, /* Processed requested path (MC_PATH only). */
+ MC_TIMEOUT, /* Timeout. */
+ MC_INTERRUPTED /* Received SIGINT (Ctrl+C). */
};
-struct mc_results;
-
void mc_results_destroy (struct mc_results *);
enum mc_stop_reason mc_results_get_stop_reason (const struct mc_results *);
@@ -151,17 +462,4 @@
struct timeval mc_results_get_end (const struct mc_results *);
double mc_results_get_duration (const struct mc_results *);
-struct mc_results *mc_run (const struct mc_class *, struct mc_options *);
-
-bool mc_include_state (struct mc *);
-bool mc_discard_dup_state (struct mc *, unsigned int hash);
-void mc_name_state (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3);
-void mc_vname_state (struct mc *, const char *, va_list) PRINTF_FORMAT (2, 0);
-void mc_error (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3);
-void mc_add_state (struct mc *, void *data);
-
-const struct mc_options *mc_get_options (struct mc *);
-const struct mc_results *mc_get_results (struct mc *);
-void *mc_get_aux (struct mc *);
-
#endif /* libpspp/model-checker.h */
| [Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Pspp-cvs] pspp/src data/datasheet.c libpspp/model-checker... [simpler-proc],
Ben Pfaff <=