1 /* PSPP - computes sample statistics.
2 Copyright (C) 2007 Free Software Foundation, Inc.
4 This program is free software; you can redistribute it and/or
5 modify it under the terms of the GNU General Public License as
6 published by the Free Software Foundation; either version 2 of the
7 License, or (at your option) any later version.
9 This program is distributed in the hope that it will be useful, but
10 WITHOUT ANY WARRANTY; without even the implied warranty of
11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
12 General Public License for more details.
14 You should have received a copy of the GNU General Public License
15 along with this program; if not, write to the Free Software
16 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
21 #include <libpspp/model-checker.h>
31 #include <libpspp/bit-vector.h>
32 #include <libpspp/compiler.h>
33 #include <libpspp/deque.h>
34 #include <libpspp/str.h>
35 #include <math/moments.h>
41 /* Initializes PATH as an empty path. */
43 mc_path_init (struct mc_path *path)
50 /* Copies the contents of OLD into NEW. */
52 mc_path_copy (struct mc_path *new, const struct mc_path *old)
54 if (old->length > new->capacity)
56 new->capacity = old->length;
58 new->ops = xnmalloc (new->capacity, sizeof *new->ops);
60 new->length = old->length;
61 memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
64 /* Adds OP to the end of PATH. */
66 mc_path_push (struct mc_path *path, int op)
68 if (path->length >= path->capacity)
69 path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
70 path->ops[path->length++] = op;
73 /* Removes and returns the operation at the end of PATH. */
75 mc_path_pop (struct mc_path *path)
77 int back = mc_path_back (path);
82 /* Returns the operation at the end of PATH. */
84 mc_path_back (const struct mc_path *path)
86 assert (path->length > 0);
87 return path->ops[path->length - 1];
92 mc_path_destroy (struct mc_path *path)
98 /* Returns the operation in position INDEX in PATH.
99 INDEX must be less than the length of PATH. */
101 mc_path_get_operation (const struct mc_path *path, size_t index)
103 assert (index < path->length);
104 return path->ops[index];
107 /* Returns the number of operations in PATH. */
109 mc_path_get_length (const struct mc_path *path)
114 /* Appends the operations in PATH to STRING, separating each one
115 with a single space. */
117 mc_path_to_string (const struct mc_path *path, struct string *string)
121 for (i = 0; i < mc_path_get_length (path); i++)
124 ds_put_char (string, ' ');
125 ds_put_format (string, "%d", mc_path_get_operation (path, i));
129 /* Search options. */
132 /* Search strategy. */
133 enum mc_strategy strategy; /* Type of strategy. */
134 int max_depth; /* Limit on depth (or INT_MAX). */
135 int hash_bits; /* Number of bits to hash (or 0). */
136 unsigned int seed; /* Random seed for MC_RANDOM
137 or MC_DROP_RANDOM. */
138 struct mc_path follow_path; /* Path for MC_PATH. */
140 /* Queue configuration. */
141 int queue_limit; /* Maximum length of queue. */
142 enum mc_queue_limit_strategy queue_limit_strategy;
143 /* How to choose state to drop
146 /* Stop conditions. */
147 int max_unique_states; /* Maximum unique states to process. */
148 int max_errors; /* Maximum errors to detect. */
149 double time_limit; /* Maximum time in seconds. */
151 /* Output configuration. */
152 int verbosity; /* 0=low, 1=normal, 2+=high. */
153 int failure_verbosity; /* If greater than verbosity,
154 verbosity of error replays. */
155 FILE *output_file; /* File to receive output. */
157 /* How to report intermediate progress. */
158 int progress_usec; /* Microseconds between reports. */
159 mc_progress_func *progress_func; /* Function to call on each report. */
165 /* Default progress function. */
167 default_progress (struct mc *mc)
169 if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
176 /* Do-nothing progress function. */
178 null_progress (struct mc *mc UNUSED)
183 /* Creates and returns a set of options initialized to the
186 mc_options_create (void)
188 struct mc_options *options = xmalloc (sizeof *options);
190 options->strategy = MC_BROAD;
191 options->max_depth = INT_MAX;
192 options->hash_bits = 20;
194 mc_path_init (&options->follow_path);
196 options->queue_limit = 10000;
197 options->queue_limit_strategy = MC_DROP_RANDOM;
199 options->max_unique_states = INT_MAX;
200 options->max_errors = 1;
201 options->time_limit = 0.0;
203 options->verbosity = 1;
204 options->failure_verbosity = 2;
205 options->output_file = stdout;
206 options->progress_usec = 250000;
207 options->progress_func = default_progress;
214 /* Returns a copy of the given OPTIONS. */
216 mc_options_clone (const struct mc_options *options)
218 return xmemdup (options, sizeof *options);
221 /* Destroys OPTIONS. */
223 mc_options_destroy (struct mc_options *options)
225 mc_path_destroy (&options->follow_path);
229 /* Returns the search strategy used for OPTIONS. The choices
232 - MC_BROAD (the default): Breadth-first search. First tries
233 all the operations with depth 1, then those with depth 2,
234 then those with depth 3, and so on.
236 This search algorithm finds the least number of operations
237 needed to trigger a given bug.
239 - MC_DEEP: Depth-first search. Searches downward in the tree
240 of states as fast as possible. Good for finding bugs that
241 require long sequences of operations to trigger.
243 - MC_RANDOM: Random-first search. Searches through the tree
244 of states in random order. The standard C library's rand
245 function selects the search path; you can control the seed
246 passed to srand using mc_options_set_seed.
248 - MC_PATH: Explicit path. Applies an explicitly specified
249 sequence of operations. */
251 mc_options_get_strategy (const struct mc_options *options)
253 return options->strategy;
256 /* Sets the search strategy used for OPTIONS to STRATEGY.
258 This function cannot be used to set MC_PATH as the search
259 strategy. Use mc_options_set_follow_path instead. */
261 mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
263 assert (strategy == MC_BROAD
264 || strategy == MC_DEEP
265 || strategy == MC_RANDOM);
266 options->strategy = strategy;
269 /* Returns OPTION's random seed used by MC_RANDOM and
272 mc_options_get_seed (const struct mc_options *options)
274 return options->seed;
277 /* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
280 mc_options_set_seed (struct mc_options *options, unsigned int seed)
282 options->seed = seed;
285 /* Returns the maximum depth to which OPTIONS's search will
286 descend. The initial states are at depth 1, states produced
287 as their mutations are at depth 2, and so on. */
289 mc_options_get_max_depth (const struct mc_options *options)
291 return options->max_depth;
294 /* Sets the maximum depth to which OPTIONS's search will descend
295 to MAX_DEPTH. The initial states are at depth 1, states
296 produced as their mutations are at depth 2, and so on. */
298 mc_options_set_max_depth (struct mc_options *options, int max_depth)
300 options->max_depth = max_depth;
303 /* Returns the base-2 log of the number of bits in OPTIONS's hash
304 table. The hash table is used for dropping states that are
305 probably duplicates: any state with a given hash value, as
306 will only be processed once. A return value of 0 indicates
307 that the model checker will not discard duplicate states based
310 The hash table is a power of 2 bits long, by default 2**20
311 bits (128 kB). Depending on how many states you expect the
312 model checker to check, how much memory you're willing to let
313 the hash table take up, and how worried you are about missing
314 states due to hash collisions, you could make it larger or
317 The "birthday paradox" points to a reasonable way to size your
318 hash table. If you expect the model checker to check about
319 2**N states, then, assuming a perfect hash, you need a hash
320 table of 2**(N+1) bits to have a 50% chance of seeing a hash
321 collision, 2**(N+2) bits to have a 25% chance, and so on. */
323 mc_options_get_hash_bits (const struct mc_options *options)
325 return options->hash_bits;
328 /* Sets the base-2 log of the number of bits in OPTIONS's hash
329 table to HASH_BITS. A HASH_BITS value of 0 requests that the
330 model checker not discard duplicate states based on their
331 hashes. (This causes the model checker to never terminate in
334 mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
336 assert (hash_bits >= 0);
337 options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
340 /* Returns the path set in OPTIONS by mc_options_set_follow_path.
341 May be used only if the search strategy is MC_PATH. */
342 const struct mc_path *
343 mc_options_get_follow_path (const struct mc_options *options)
345 assert (options->strategy == MC_PATH);
346 return &options->follow_path;
349 /* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
350 to be the explicit path specified in FOLLOW_PATH. */
352 mc_options_set_follow_path (struct mc_options *options,
353 const struct mc_path *follow_path)
355 assert (mc_path_get_length (follow_path) > 0);
356 options->strategy = MC_PATH;
357 mc_path_copy (&options->follow_path, follow_path);
360 /* Returns the maximum number of queued states in OPTIONS. The
361 default value is 10,000. The primary reason to limit the
362 number of queued states is to conserve memory, so if you can
363 afford the memory and your model needs more room in the queue,
364 you can raise the limit. Conversely, if your models are large
365 or memory is constrained, you can reduce the limit.
367 Following the execution of the model checker, you can find out
368 the maximum queue length during the run by calling
369 mc_results_get_max_queue_length. */
371 mc_options_get_queue_limit (const struct mc_options *options)
373 return options->queue_limit;
376 /* Sets the maximum number of queued states in OPTIONS to
379 mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
381 assert (queue_limit > 0);
382 options->queue_limit = queue_limit;
385 /* Returns the queue limit strategy used by OPTIONS, that is,
386 when a new state must be inserted into a full state queue is
387 full, how the state to be dropped is chosen. The choices are:
389 - MC_DROP_NEWEST: Drop the newest state; that is, do not
390 insert the new state into the queue at all.
392 - MC_DROP_OLDEST: Drop the state that has been enqueued for
395 - MC_DROP_RANDOM (the default): Drop a randomly selected state
396 from the queue. The standard C library's rand function
397 selects the state to drop; you can control the seed passed
398 to srand using mc_options_set_seed. */
399 enum mc_queue_limit_strategy
400 mc_options_get_queue_limit_strategy (const struct mc_options *options)
402 return options->queue_limit_strategy;
405 /* Sets the queue limit strategy used by OPTIONS to STRATEGY.
407 This setting has no effect unless the model being checked
408 causes the state queue to overflow (see
409 mc_options_get_queue_limit). */
411 mc_options_set_queue_limit_strategy (struct mc_options *options,
412 enum mc_queue_limit_strategy strategy)
414 assert (strategy == MC_DROP_NEWEST
415 || strategy == MC_DROP_OLDEST
416 || strategy == MC_DROP_RANDOM);
417 options->queue_limit_strategy = strategy;
420 /* Returns OPTIONS's maximum number of unique states that the
421 model checker will examine before terminating. The default is
424 mc_options_get_max_unique_states (const struct mc_options *options)
426 return options->max_unique_states;
429 /* Sets OPTIONS's maximum number of unique states that the model
430 checker will examine before terminating to
433 mc_options_set_max_unique_states (struct mc_options *options,
434 int max_unique_states)
436 options->max_unique_states = max_unique_states;
439 /* Returns the maximum number of errors that OPTIONS will allow
440 the model checker to encounter before terminating. The
443 mc_options_get_max_errors (const struct mc_options *options)
445 return options->max_errors;
448 /* Sets the maximum number of errors that OPTIONS will allow the
449 model checker to encounter before terminating to
452 mc_options_set_max_errors (struct mc_options *options, int max_errors)
454 options->max_errors = max_errors;
457 /* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
458 model checker to consume before terminating. The
459 default of 0.0 means that time consumption is unlimited. */
461 mc_options_get_time_limit (const struct mc_options *options)
463 return options->time_limit;
466 /* Sets the maximum amount of time, in seconds, that OPTIONS will
467 allow the model checker to consume before terminating to
468 TIME_LIMIT. A value of 0.0 means that time consumption is
469 unlimited; otherwise, the return value will be positive. */
471 mc_options_set_time_limit (struct mc_options *options, double time_limit)
473 assert (time_limit >= 0.0);
474 options->time_limit = time_limit;
477 /* Returns the level of verbosity for output messages specified
478 by OPTIONS. The default verbosity level is 1.
480 A verbosity level of 0 inhibits all messages except for
481 errors; a verbosity level of 1 also allows warnings; a
482 verbosity level of 2 also causes a description of each state
483 added to be output; a verbosity level of 3 also causes a
484 description of each duplicate state to be output. Verbosity
485 levels less than 0 or greater than 3 are allowed but currently
486 have no additional effect. */
488 mc_options_get_verbosity (const struct mc_options *options)
490 return options->verbosity;
493 /* Sets the level of verbosity for output messages specified
494 by OPTIONS to VERBOSITY. */
496 mc_options_set_verbosity (struct mc_options *options, int verbosity)
498 options->verbosity = verbosity;
501 /* Returns the level of verbosity for failures specified by
502 OPTIONS. The default failure verbosity level is 2.
504 The failure verbosity level has an effect only when an error
505 is reported, and only when the failure verbosity level is
506 higher than the regular verbosity level. When this is the
507 case, the model checker replays the error path at the higher
508 verbosity level specified. This has the effect of outputting
509 an explicit, human-readable description of the sequence of
510 operations that caused the error. */
512 mc_options_get_failure_verbosity (const struct mc_options *options)
514 return options->failure_verbosity;
517 /* Sets the level of verbosity for failures specified by OPTIONS
518 to FAILURE_VERBOSITY. */
520 mc_options_set_failure_verbosity (struct mc_options *options,
521 int failure_verbosity)
523 options->failure_verbosity = failure_verbosity;
526 /* Returns the output file used for messages printed by the model
527 checker specified by OPTIONS. The default is stdout. */
529 mc_options_get_output_file (const struct mc_options *options)
531 return options->output_file;
534 /* Sets the output file used for messages printed by the model
535 checker specified by OPTIONS to OUTPUT_FILE.
537 The model checker does not automatically close the specified
538 output file. If this is desired, the model checker's client
541 mc_options_set_output_file (struct mc_options *options,
544 options->output_file = output_file;
547 /* Returns the number of microseconds between calls to the
548 progress function specified by OPTIONS. The default is
549 250,000 (1/4 second). A value of 0 disables progress
552 mc_options_get_progress_usec (const struct mc_options *options)
554 return options->progress_usec;
557 /* Sets the number of microseconds between calls to the progress
558 function specified by OPTIONS to PROGRESS_USEC. A value of 0
559 disables progress reporting. */
561 mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
563 assert (progress_usec >= 0);
564 options->progress_usec = progress_usec;
567 /* Returns the function called to report progress specified by
568 OPTIONS. The function used by default prints '.' to
571 mc_options_get_progress_func (const struct mc_options *options)
573 return options->progress_func;
576 /* Sets the function called to report progress specified by
577 OPTIONS to PROGRESS_FUNC. A non-null function must be
578 specified; to disable progress reporting, set the progress
579 reporting interval to 0.
581 PROGRESS_FUNC will be called zero or more times while the
582 model checker's run is ongoing. For these calls to the
583 progress function, mc_results_get_stop_reason will return
584 MC_CONTINUING. It will also be called exactly once soon
585 before mc_run returns, in which case
586 mc_results_get_stop_reason will return a different value. */
588 mc_options_set_progress_func (struct mc_options *options,
589 mc_progress_func *progress_func)
591 assert (options->progress_func != NULL);
592 options->progress_func = progress_func;
595 /* Returns the auxiliary data set in OPTIONS by the client. The
596 default is a null pointer.
598 This auxiliary data value can be retrieved by the
599 client-specified functions in struct mc_class during a model
600 checking run using mc_get_aux. */
602 mc_options_get_aux (const struct mc_options *options)
607 /* Sets the auxiliary data in OPTIONS to AUX. */
609 mc_options_set_aux (struct mc_options *options, void *aux)
614 /* Results of a model checking run. */
617 /* Overall results. */
618 enum mc_stop_reason stop_reason; /* Why the run ended. */
619 int unique_state_count; /* Number of unique states checked. */
620 int error_count; /* Number of errors found. */
622 /* Depth statistics. */
623 int max_depth_reached; /* Max depth state examined. */
624 struct moments1 *depth_moments; /* Enables reporting mean depth. */
626 /* If error_count > 0, path to the last error reported. */
627 struct mc_path error_path;
629 /* States dropped... */
630 int duplicate_dropped_states; /* ...as duplicates. */
631 int off_path_dropped_states; /* ...as off-path (MC_PATH only). */
632 int depth_dropped_states; /* ...due to excessive depth. */
633 int queue_dropped_states; /* ...due to queue overflow. */
635 /* Queue statistics. */
636 int queued_unprocessed_states; /* Enqueued but never dequeued. */
637 int max_queue_length; /* Maximum queue length observed. */
640 struct timeval start; /* Start of model checking run. */
641 struct timeval end; /* End of model checking run. */
644 /* Creates, initializes, and returns a new set of results. */
645 static struct mc_results *
646 mc_results_create (void)
648 struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
649 results->stop_reason = MC_CONTINUING;
650 results->depth_moments = moments1_create (MOMENT_MEAN);
651 gettimeofday (&results->start, NULL);
655 /* Destroys RESULTS. */
657 mc_results_destroy (struct mc_results *results)
661 moments1_destroy (results->depth_moments);
662 mc_path_destroy (&results->error_path);
667 /* Returns RESULTS's reason that the model checking run
668 terminated. The possible reasons are:
670 - MC_CONTINUING: The run is not actually yet complete. This
671 can only be returned before mc_run has returned, e.g. when
672 the progress function set by mc_options_set_progress_func
673 examines the run's results.
675 - MC_SUCCESS: The run completed because the queue emptied.
676 The entire state space might not have been explored due to a
677 requested limit on maximum depth, hash collisions, etc.
679 - MC_MAX_UNIQUE_STATES: The run completed because as many
680 unique states have been checked as were requested (using
681 mc_options_set_max_unique_states).
683 - MC_MAX_ERROR_COUNT: The run completed because the maximum
684 requested number of errors (by default, 1 error) was
687 - MC_END_OF_PATH: The run completed because the path specified
688 with mc_options_set_follow_path was fully traversed.
690 - MC_TIMEOUT: The run completed because the time limit set
691 with mc_options_set_time_limit was exceeded.
693 - MC_INTERRUPTED: The run completed because SIGINT was caught
694 (typically, due to the user typing Ctrl+C). */
696 mc_results_get_stop_reason (const struct mc_results *results)
698 return results->stop_reason;
701 /* Returns the number of unique states checked specified by
704 mc_results_get_unique_state_count (const struct mc_results *results)
706 return results->unique_state_count;
709 /* Returns the number of errors found specified by RESULTS. */
711 mc_results_get_error_count (const struct mc_results *results)
713 return results->error_count;
716 /* Returns the maximum depth reached during the model checker run
717 represented by RESULTS. The initial states are at depth 1,
718 their child states at depth 2, and so on. */
720 mc_results_get_max_depth_reached (const struct mc_results *results)
722 return results->max_depth_reached;
725 /* Returns the mean depth reached during the model checker run
726 represented by RESULTS. */
728 mc_results_get_mean_depth_reached (const struct mc_results *results)
731 moments1_calculate (results->depth_moments, NULL, &mean, NULL, NULL, NULL);
732 return mean != SYSMIS ? mean : 0.0;
735 /* Returns the path traversed to obtain the last error
736 encountered during the model checker run represented by
737 RESULTS. Returns a null pointer if the run did not report any
739 const struct mc_path *
740 mc_results_get_error_path (const struct mc_results *results)
742 return results->error_count > 0 ? &results->error_path : NULL;
745 /* Returns the number of states dropped as duplicates (based on
746 hash value) during the model checker run represented by
749 mc_results_get_duplicate_dropped_states (const struct mc_results *results)
751 return results->duplicate_dropped_states;
754 /* Returns the number of states dropped because they were off the
755 path specified by mc_options_set_follow_path during the model
756 checker run represented by RESULTS. A nonzero value here
757 indicates a missing call to mc_include_state in the
758 client-supplied mutation function. */
760 mc_results_get_off_path_dropped_states (const struct mc_results *results)
762 return results->off_path_dropped_states;
765 /* Returns the number of states dropped because their depth
766 exceeded the maximum specified with mc_options_set_max_depth
767 during the model checker run represented by RESULTS. */
769 mc_results_get_depth_dropped_states (const struct mc_results *results)
771 return results->depth_dropped_states;
774 /* Returns the number of states dropped from the queue due to
775 queue overflow during the model checker run represented by
778 mc_results_get_queue_dropped_states (const struct mc_results *results)
780 return results->queue_dropped_states;
783 /* Returns the number of states that were checked and enqueued
784 but never dequeued and processed during the model checker run
785 represented by RESULTS. This is zero if the stop reason is
786 MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
787 states in the queue at the time that the checking run
790 mc_results_get_queued_unprocessed_states (const struct mc_results *results)
792 return results->queued_unprocessed_states;
795 /* Returns the maximum length of the queue during the model
796 checker run represented by RESULTS. If this is equal to the
797 maximum queue length, then the queue (probably) overflowed
798 during the run; otherwise, it did not overflow. */
800 mc_results_get_max_queue_length (const struct mc_results *results)
802 return results->max_queue_length;
805 /* Returns the time at which the model checker run represented by
808 mc_results_get_start (const struct mc_results *results)
810 return results->start;
813 /* Returns the time at which the model checker run represented by
814 RESULTS ended. (This function may not be called while the run
815 is still ongoing.) */
817 mc_results_get_end (const struct mc_results *results)
819 assert (results->stop_reason != MC_CONTINUING);
823 /* Returns the number of seconds obtained by subtracting time Y
826 timeval_subtract (struct timeval x, struct timeval y)
828 /* From libc.info. */
831 /* Perform the carry for the later subtraction by updating Y. */
832 if (x.tv_usec < y.tv_usec) {
833 int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
834 y.tv_usec -= 1000000 * nsec;
837 if (x.tv_usec - y.tv_usec > 1000000) {
838 int nsec = (x.tv_usec - y.tv_usec) / 1000000;
839 y.tv_usec += 1000000 * nsec;
843 /* Compute the time remaining to wait.
844 `tv_usec' is certainly positive. */
845 difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0;
846 if (x.tv_sec < y.tv_sec)
847 difference = -difference;
852 /* Returns the duration, in seconds, of the model checker run
853 represented by RESULTS. (This function may not be called
854 while the run is still ongoing.) */
856 mc_results_get_duration (const struct mc_results *results)
858 assert (results->stop_reason != MC_CONTINUING);
859 return timeval_subtract (results->end, results->start);
862 /* An active model checking run. */
865 /* Related data structures. */
866 const struct mc_class *class;
867 struct mc_options *options;
868 struct mc_results *results;
870 /* Array of 2**(options->hash_bits) bits representing states
875 struct mc_state **queue; /* Array of pointers to states. */
876 struct deque queue_deque; /* Deque. */
878 /* State currently being built by "init" or "mutate". */
879 struct mc_path path; /* Path to current state. */
880 struct string path_string; /* Buffer for path_string function. */
881 bool state_named; /* mc_name_operation called? */
882 bool state_error; /* mc_error called? */
884 /* Statistics for calling the progress function. */
885 unsigned int progress; /* Current progress value. */
886 unsigned int next_progress; /* Next value to call progress func. */
887 unsigned int prev_progress; /* Last value progress func called. */
888 struct timeval prev_progress_time; /* Last time progress func called. */
890 /* Information for handling and restoring SIGINT. */
891 bool interrupted; /* SIGINT received? */
892 bool *saved_interrupted_ptr; /* Saved value of interrupted_ptr. */
893 void (*saved_sigint) (int); /* Saved SIGINT handler. */
896 /* A state in the queue. */
899 struct mc_path path; /* Path to this state. */
900 void *data; /* Client-supplied data. */
903 /* Points to the current struct mc's "interrupted" member. */
904 static bool *interrupted_ptr = NULL;
906 static const char *path_string (struct mc *);
907 static void free_state (const struct mc *, struct mc_state *);
908 static void stop (struct mc *, enum mc_stop_reason);
909 static struct mc_state *make_state (const struct mc *, void *);
910 static size_t random_queue_index (struct mc *);
911 static void enqueue_state (struct mc *, struct mc_state *);
912 static void do_error_state (struct mc *);
913 static void next_operation (struct mc *);
914 static bool is_off_path (const struct mc *);
915 static void sigint_handler (int signum);
916 static void init_mc (struct mc *,
917 const struct mc_class *, struct mc_options *);
918 static void finish_mc (struct mc *);
920 /* Runs the model checker on the client-specified CLASS with the
921 client-specified OPTIONS. OPTIONS may be a null pointer if
922 the defaults are acceptable. Destroys OPTIONS; use
923 mc_options_clone if a copy is needed.
925 Returns the results of the model checking run, which must be
926 destroyed by the client with mc_results_destroy.
928 To pass auxiliary data to the functions in CLASS, use
929 mc_options_set_aux on OPTIONS, which may be retrieved from the
930 CLASS functions using mc_get_aux. */
932 mc_run (const struct mc_class *class, struct mc_options *options)
936 init_mc (&mc, class, options);
937 while (!deque_is_empty (&mc.queue_deque)
938 && mc.results->stop_reason == MC_CONTINUING)
940 struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
941 mc_path_copy (&mc.path, &state->path);
942 mc_path_push (&mc.path, 0);
943 class->mutate (&mc, state->data);
944 free_state (&mc, state);
946 stop (&mc, MC_INTERRUPTED);
953 /* Tests whether the current operation is one that should be
954 performed, checked, and enqueued. If so, returns true.
955 Otherwise, returns false and, unless checking is stopped,
956 advances to the next state. The caller should then advance
957 to the next operation.
959 This function should be called from the client-provided
960 "mutate" function, according to the pattern explained in the
961 big comment at the top of model-checker.h. */
963 mc_include_state (struct mc *mc)
965 if (mc->results->stop_reason != MC_CONTINUING)
967 else if (is_off_path (mc))
976 /* Tests whether HASH represents a state that has (probably)
977 already been enqueued. If not, returns false and marks HASH
978 so that it will be treated as a duplicate in the future. If
979 so, returns true and advances to the next state. The
980 caller should then advance to the next operation.
982 This function should be called from the client-provided
983 "mutate" function, according to the pattern explained in the
984 big comment at the top of model-checker.h. */
986 mc_discard_dup_state (struct mc *mc, unsigned int hash)
988 if (mc->options->hash_bits > 0)
990 hash &= (1u << mc->options->hash_bits) - 1;
991 if (TEST_BIT (mc->hash, hash))
993 if (mc->options->verbosity > 2)
994 fprintf (mc->options->output_file,
995 " [%s] discard duplicate state\n", path_string (mc));
996 mc->results->duplicate_dropped_states++;
1000 SET_BIT (mc->hash, hash);
1005 /* Names the current state NAME, which may contain
1006 printf-style format specifications. NAME should be a
1007 human-readable name for the current operation.
1009 This function should be called from the client-provided
1010 "mutate" function, according to the pattern explained in the
1011 big comment at the top of model-checker.h. */
1013 mc_name_operation (struct mc *mc, const char *name, ...)
1017 va_start (args, name);
1018 mc_vname_operation (mc, name, args);
1022 /* Names the current state NAME, which may contain
1023 printf-style format specifications, for which the
1024 corresponding arguments must be given in ARGS. NAME should be
1025 a human-readable name for the current operation.
1027 This function should be called from the client-provided
1028 "mutate" function, according to the pattern explained in the
1029 big comment at the top of model-checker.h. */
1031 mc_vname_operation (struct mc *mc, const char *name, va_list args)
1033 if (mc->state_named && mc->options->verbosity > 0)
1034 fprintf (mc->options->output_file, " [%s] warning: duplicate call "
1035 "to mc_name_operation (missing call to mc_add_state?)\n",
1037 mc->state_named = true;
1039 if (mc->options->verbosity > 1)
1041 fprintf (mc->options->output_file, " [%s] ", path_string (mc));
1042 vfprintf (mc->options->output_file, name, args);
1043 putc ('\n', mc->options->output_file);
1047 /* Reports the given error MESSAGE for the current operation.
1048 The resulting state should still be passed to mc_add_state
1049 when all relevant error messages have been issued. The state
1050 will not, however, be enqueued for later mutation of its own.
1052 By default, model checking stops after the first error
1055 This function should be called from the client-provided
1056 "mutate" function, according to the pattern explained in the
1057 big comment at the top of model-checker.h. */
1059 mc_error (struct mc *mc, const char *message, ...)
1063 if (mc->results->stop_reason != MC_CONTINUING)
1066 if (mc->options->verbosity > 1)
1067 fputs (" ", mc->options->output_file);
1068 fprintf (mc->options->output_file, "[%s] error: ",
1070 va_start (args, message);
1071 vfprintf (mc->options->output_file, message, args);
1073 putc ('\n', mc->options->output_file);
1075 mc->state_error = true;
1078 /* Enqueues DATA as the state corresponding to the current
1079 operation. The operation should have been named with a call
1080 to mc_name_operation, and it should have been checked by the
1081 caller (who should have reported any errors with mc_error).
1083 This function should be called from the client-provided
1084 "mutate" function, according to the pattern explained in the
1085 big comment at the top of model-checker.h. */
1087 mc_add_state (struct mc *mc, void *data)
1089 if (!mc->state_named && mc->options->verbosity > 0)
1090 fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
1093 if (mc->results->stop_reason != MC_CONTINUING)
1095 /* Nothing to do. */
1097 else if (mc->state_error)
1098 do_error_state (mc);
1099 else if (is_off_path (mc))
1100 mc->results->off_path_dropped_states++;
1101 else if (mc->path.length + 1 > mc->options->max_depth)
1102 mc->results->depth_dropped_states++;
1105 /* This is the common case. */
1106 mc->results->unique_state_count++;
1107 if (mc->results->unique_state_count >= mc->options->max_unique_states)
1108 stop (mc, MC_MAX_UNIQUE_STATES);
1109 enqueue_state (mc, make_state (mc, data));
1110 next_operation (mc);
1114 mc->class->destroy (mc, data);
1115 next_operation (mc);
1118 /* Returns the options that were passed to mc_run for model
1120 const struct mc_options *
1121 mc_get_options (const struct mc *mc)
1126 /* Returns the current state of the results for model checker
1127 MC. This function is appropriate for use from the progress
1128 function set by mc_options_set_progress_func.
1130 Not all of the results are meaningful before model checking
1132 const struct mc_results *
1133 mc_get_results (const struct mc *mc)
1138 /* Returns the auxiliary data set on the options passed to mc_run
1139 with mc_options_set_aux. */
1141 mc_get_aux (const struct mc *mc)
1143 return mc_options_get_aux (mc_get_options (mc));
1146 /* Expresses MC->path as a string and returns the string. */
1148 path_string (struct mc *mc)
1150 ds_clear (&mc->path_string);
1151 mc_path_to_string (&mc->path, &mc->path_string);
1152 return ds_cstr (&mc->path_string);
1155 /* Frees STATE, including client data. */
1157 free_state (const struct mc *mc, struct mc_state *state)
1159 mc->class->destroy (mc, state->data);
1160 mc_path_destroy (&state->path);
1164 /* Sets STOP_REASON as the reason that MC's processing stopped,
1165 unless MC is already stopped. */
1167 stop (struct mc *mc, enum mc_stop_reason stop_reason)
1169 if (mc->results->stop_reason == MC_CONTINUING)
1170 mc->results->stop_reason = stop_reason;
1173 /* Creates and returns a new state whose path is copied from
1174 MC->path and whose data is specified by DATA. */
1175 static struct mc_state *
1176 make_state (const struct mc *mc, void *data)
1178 struct mc_state *new = xmalloc (sizeof *new);
1179 mc_path_init (&new->path);
1180 mc_path_copy (&new->path, &mc->path);
1185 /* Returns the index in MC->queue of a random element in the
1188 random_queue_index (struct mc *mc)
1190 assert (!deque_is_empty (&mc->queue_deque));
1191 return deque_front (&mc->queue_deque,
1192 rand () % deque_count (&mc->queue_deque));
1195 /* Adds NEW to MC's state queue, dropping a state if necessary
1198 enqueue_state (struct mc *mc, struct mc_state *new)
1202 if (new->path.length > mc->results->max_depth_reached)
1203 mc->results->max_depth_reached = new->path.length;
1204 moments1_add (mc->results->depth_moments, new->path.length, 1.0);
1206 if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
1208 /* Add new state to queue. */
1209 if (deque_is_full (&mc->queue_deque))
1210 mc->queue = deque_expand (&mc->queue_deque,
1211 mc->queue, sizeof *mc->queue);
1212 switch (mc->options->strategy)
1215 idx = deque_push_back (&mc->queue_deque);
1218 idx = deque_push_front (&mc->queue_deque);
1221 if (!deque_is_empty (&mc->queue_deque))
1223 idx = random_queue_index (mc);
1224 mc->queue[deque_push_front (&mc->queue_deque)]
1228 idx = deque_push_front (&mc->queue_deque);
1231 assert (deque_is_empty (&mc->queue_deque));
1232 assert (!is_off_path (mc));
1233 idx = deque_push_back (&mc->queue_deque);
1235 >= mc_path_get_length (&mc->options->follow_path))
1236 stop (mc, MC_END_OF_PATH);
1241 if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
1242 mc->results->max_queue_length = deque_count (&mc->queue_deque);
1246 /* Queue has reached limit, so replace an existing
1248 assert (mc->options->strategy != MC_PATH);
1249 assert (!deque_is_empty (&mc->queue_deque));
1250 mc->results->queue_dropped_states++;
1251 switch (mc->options->queue_limit_strategy)
1253 case MC_DROP_NEWEST:
1254 free_state (mc, new);
1256 case MC_DROP_OLDEST:
1257 switch (mc->options->strategy)
1260 idx = deque_front (&mc->queue_deque, 0);
1263 idx = deque_back (&mc->queue_deque, 0);
1271 case MC_DROP_RANDOM:
1272 idx = random_queue_index (mc);
1277 free_state (mc, mc->queue[idx]);
1279 mc->queue[idx] = new;
1282 /* Process an error state being added to MC. */
1284 do_error_state (struct mc *mc)
1286 mc->results->error_count++;
1287 if (mc->results->error_count >= mc->options->max_errors)
1288 stop (mc, MC_MAX_ERROR_COUNT);
1290 mc_path_copy (&mc->results->error_path, &mc->path);
1292 if (mc->options->failure_verbosity > mc->options->verbosity)
1294 struct mc_options *path_options;
1296 fprintf (mc->options->output_file, "[%s] retracing error path:\n",
1298 path_options = mc_options_clone (mc->options);
1299 mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
1300 mc_options_set_failure_verbosity (path_options, 0);
1301 mc_options_set_follow_path (path_options, &mc->path);
1303 mc_results_destroy (mc_run (mc->class, path_options));
1305 putc ('\n', mc->options->output_file);
1309 /* Advances MC to start processing the operation following the
1312 next_operation (struct mc *mc)
1314 mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
1315 mc->state_error = false;
1316 mc->state_named = false;
1318 if (++mc->progress >= mc->next_progress)
1321 double elapsed, delta;
1323 if (mc->results->stop_reason == MC_CONTINUING
1324 && !mc->options->progress_func (mc))
1325 stop (mc, MC_INTERRUPTED);
1327 gettimeofday (&now, NULL);
1329 if (mc->options->time_limit > 0.0
1330 && (timeval_subtract (now, mc->results->start)
1331 > mc->options->time_limit))
1332 stop (mc, MC_TIMEOUT);
1334 elapsed = timeval_subtract (now, mc->prev_progress_time);
1337 /* Re-estimate the amount of progress to take
1338 progress_usec microseconds. */
1339 unsigned int progress = mc->progress - mc->prev_progress;
1340 double progress_sec = mc->options->progress_usec / 1000000.0;
1341 delta = progress / elapsed * progress_sec;
1345 /* No measurable time at all elapsed during that amount
1346 of progress. Try doubling the amount of progress
1348 delta = (mc->progress - mc->prev_progress) * 2;
1351 if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
1352 mc->next_progress = mc->progress + delta + 1.0;
1354 mc->next_progress = mc->progress + (mc->progress - mc->prev_progress);
1356 mc->prev_progress = mc->progress;
1357 mc->prev_progress_time = now;
1361 /* Returns true if we're tracing an explicit path but the current
1362 operation produces a state off that path, false otherwise. */
1364 is_off_path (const struct mc *mc)
1366 return (mc->options->strategy == MC_PATH
1367 && (mc_path_back (&mc->path)
1368 != mc_path_get_operation (&mc->options->follow_path,
1369 mc->path.length - 1)));
1372 /* Handler for SIGINT. */
1374 sigint_handler (int signum UNUSED)
1376 /* Just mark the model checker as interrupted. */
1377 *interrupted_ptr = true;
1380 /* Initializes MC as a model checker with the given CLASS and
1381 OPTIONS. OPTIONS may be null to use the default options. */
1383 init_mc (struct mc *mc, const struct mc_class *class,
1384 struct mc_options *options)
1386 /* Validate and adjust OPTIONS. */
1387 if (options == NULL)
1388 options = mc_options_create ();
1389 assert (options->queue_limit_strategy != MC_DROP_OLDEST
1390 || options->strategy != MC_RANDOM);
1391 if (options->strategy == MC_PATH)
1393 options->max_depth = INT_MAX;
1394 options->hash_bits = 0;
1396 if (options->progress_usec == 0)
1398 options->progress_func = null_progress;
1399 if (options->time_limit > 0.0)
1400 options->progress_usec = 250000;
1403 /* Initialize MC. */
1405 mc->options = options;
1406 mc->results = mc_results_create ();
1408 mc->hash = (mc->options->hash_bits > 0
1409 ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
1413 deque_init_null (&mc->queue_deque);
1415 mc_path_init (&mc->path);
1416 mc_path_push (&mc->path, 0);
1417 ds_init_empty (&mc->path_string);
1418 mc->state_named = false;
1419 mc->state_error = false;
1422 mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
1423 mc->prev_progress = 0;
1424 mc->prev_progress_time = mc->results->start;
1426 if (mc->options->strategy == MC_RANDOM
1427 || options->queue_limit_strategy == MC_DROP_RANDOM)
1428 srand (mc->options->seed);
1430 mc->interrupted = false;
1431 mc->saved_interrupted_ptr = interrupted_ptr;
1432 interrupted_ptr = &mc->interrupted;
1433 mc->saved_sigint = signal (SIGINT, sigint_handler);
1438 /* Complete the model checker run for MC. */
1440 finish_mc (struct mc *mc)
1442 /* Restore signal handlers. */
1443 signal (SIGINT, mc->saved_sigint);
1444 interrupted_ptr = mc->saved_interrupted_ptr;
1446 /* Mark the run complete. */
1447 stop (mc, MC_SUCCESS);
1448 gettimeofday (&mc->results->end, NULL);
1450 /* Empty the queue. */
1451 mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
1452 while (!deque_is_empty (&mc->queue_deque))
1454 struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
1455 free_state (mc, state);
1458 /* Notify the progress function of completion. */
1459 mc->options->progress_func (mc);
1462 mc_path_destroy (&mc->path);
1463 ds_destroy (&mc->path_string);