Module concuerror_options

Concuerror's options module.

Description

Concuerror's options module

The _option() functions listed on this page all correspond to valid configuration options.

For general documentation go to the Overview page.

Table of Contents

Help

You can also access documentation about options using the help option. You can get more help with concuerror --help help. In the future even more help might be added.

If you invoke Concuerror without an argument, --help is assumed as an argument.

Options

  1. All options have a long name.
  2. Some options also have a short name.
  3. Options marked with an asterisk * are considered experimental and may be brittle and disappear in future versions.

Arguments

The type of each options' argument is listed at the option's specification below. When specifying integer() or boolean() options in the command line you can omit true or 1 as values.

Module Attributes

You can use the following attributes in the module specified by --module to pass options to Concuerror:
-concuerror_options(Options)
A list of Options that can be overriden by other options.
-concuerror_options_forced(Options)
error (exit status: 1)
A list of Options that override any other options.

This information is also available via concuerror --help attributes

Keywords

Each option is associated with one or more keywords. These can be used with help to find related options.

If you invoke help without an argument, you will only see options with the keyword basic. To see all options use --help all.

Multiple Arguments

Some options can be specified multiple times, each time with a different argument. For those that don't the last value is kept (this makes invocation via command line easier). Concuerror reports any overrides.

Standard Error Printout

By default, Concuerror prints diagnostic messages in the standard error stream. Such messages are also printed at the bottom of the Report File after the analysis is completed. You can find explanation of the classification of these messages in the verbosity option.

By default, Concuerror also prints progress information in the standard error stream. You can find what is the meaning of each field by running concuerror --help progress.

The printout can be reduced or disabled (see verbosity option). Diagnostic messages are always printed in the Report File.

Report File

By default, Concuerror prints analysis findings in a report file.

This file contains:

  1. A header line containing the version used and starting time.
  2. A list of all the options used in the particular run.
  3. Zero or more Error Reports about erroneous interleavings.
  4. Diagnostic messages (see Standard Error Printout).
  5. Summary about the analysis, including

Error Reports

An error report corresponds to an interleaving that lead to errors and contains at least the following sections:

If the program produce any output, this is also included.

By default, Concuerror reports the following errors: If the show_races option is used, the pairs of racing events that justify the exploration of new interleavings are also shown. These are shown for all interleavings, not only the ones with errors.

Data Types

bound()

bound() = infinity | non_neg_integer()

If you want to pass infinity as option from the command-line, use -1.

dpor()

dpor() = none | optimal | persistent | source

See dpor_option/0 for the meaning of values.

option_spec()

abstract datatype: option_spec()

This is used internally to specify option components and is irrelevant for a user of Concuerror.

options()

options() = proplists:proplist()

Concuerror's configuration options are given as a proplist(). See the list of functions in this module for valid configuration options.

scheduling()

scheduling() = oldest | newest | round_robin

See scheduling_option/0 for the meaning of values.

scheduling_bound_type()

scheduling_bound_type() = bpor | delay | none | ubpor

See scheduling_bound_option/0 for the meaning of values.

Function Index

after_timeout_option/0Threshold for treating timeouts as infinity.
assertions_only_option/0Report only abnormal exits due to ?asserts
assume_racing_option/0Do not crash if race info is missing.
depth_bound_option/0Maximum number of events.
disable_sleep_sets_option/0Disable sleep sets.
dpor_option/0DPOR technique.
exclude_module_option/0* Modules that should not be instrumented.
file_option/0Load specified file (.beam or .erl).
first_process_errors_only_option/0Report only errors that involve the first process.
graph_option/0Produce a DOT graph in the specified file.
help_option/0Display help (use -h h for more help).
ignore_error_option/0Error categories that should be ignored.
instant_delivery_option/0Make messages and signals arrive instantly.
interleaving_bound_option/0Maximum number of interleavings.
keep_going_option/0Keep running after an error is found.
module_option/0Module containing the test function.
no_output_option/0Do not produce an analysis report.
non_racing_system_option/0No races due to 'system' messages.
observers_option/0Synonym for --use_receive_patterns
optimal_option/0Synonym for --dpor optimal (true) | source (false)
output_option/0Filename to use for the analysis report.
pa_option/0Add directory to Erlang's code path (front).
parse_cl/1Converts command-line arguments to a proplist using getopt.
print_depth_option/0Print depth for log/graph.
pz_option/0Add directory to Erlang's code path (rear).
quiet_option/0Synonym for --verbosity 0
scheduling_bound_option/0Scheduling bound value.
scheduling_bound_type_option/0* Schedule bounding technique.
scheduling_option/0Scheduling order.
show_races_option/0Show races in log/graph.
strict_scheduling_option/0Force preemptions when scheduling.
symbolic_names_option/0Use symbolic process names.
test_option/0Name of test function.
timeout_option/0How long to wait for an event (>= 500ms).
treat_as_normal_option/0Exit reason treated as normal (i.e., not reported as an error).
use_receive_patterns_option/0Use receive patterns for racing sends.
verbosity_option/0Verbosity level (0-7).
version_option/0Display version information.

Function Details

after_timeout_option/0

after_timeout_option() -> option_spec()

Threshold for treating timeouts as infinity

Assume that after clauses with timeouts higher or equal to the specified value cannot be triggered. Concuerror treats all lower values as triggerable

assertions_only_option/0

assertions_only_option() -> option_spec()

Report only abnormal exits due to ?asserts

Only processes that exit with a reason of form {{assert*, _}, _} are considered errors. Such exit reasons are generated e.g. by the macros defined in the stdlib/include/assert.hrl header file.

assume_racing_option/0

assume_racing_option() -> option_spec()

Do not crash if race info is missing

Concuerror has a list of operation pairs that are known to be non-racing. If there is no info about whether a specific pair of built-in operations may race, assume that they do indeed race. If this option is set to false, Concuerror will exit instead. Useful only for detecting missing racing info.

depth_bound_option/0

depth_bound_option() -> option_spec()

Maximum number of events

The maximum number of events allowed in an interleaving. Concuerror will stop exploring an interleaving that has events beyond this limit.

disable_sleep_sets_option/0

disable_sleep_sets_option() -> option_spec()

Disable sleep sets

This option is only available with --dpor none.

dpor_option/0

dpor_option() -> option_spec()

DPOR technique

Specifies which Dynamic Partial Order Reduction technique will be used. The available options are: - none: Disable DPOR. Not recommended. - optimal: Using source sets and wakeup trees. - source: Using source sets only. Use this if the rate of exploration is too slow. Use optimal if a lot of interleavings are reported as sleep-set blocked. - persistent: Using persistent sets. Not recommended.

exclude_module_option/0

exclude_module_option() -> option_spec()

* Modules that should not be instrumented

Experimental. Concuerror needs to instrument all code in a test to be able to reset the state after each exploration. You can use this option to exclude a module from instrumentation, but you must ensure that any state is reset correctly, or Concuerror will complain that operations have unexpected results.

file_option/0

file_option() -> option_spec()

Load specified file (.beam or .erl)

Explicitly load the specified file(s) (.beam or .erl). Source (.erl) files should not require any command line compile options. Use a .beam file (preferably compiled with +debug_info) if special compilation is needed.

It is recommended to rely on Erlang's load path rather than using this option.

first_process_errors_only_option/0

first_process_errors_only_option() -> option_spec()

Report only errors that involve the first process

All errors involving only children processes will be ignored.

graph_option/0

graph_option() -> option_spec()

Produce a DOT graph in the specified file

The DOT graph can be converted to an image with e.g. dot -Tsvg -o graph.svg graph

help_option/0

help_option() -> option_spec()

Display help (use -h h for more help)

Without an argument, prints info for basic options.

With all as argument, prints info for all options.

With attributes as argument, prints info about passing options using module attributes.

With progress as argument, prints info about what the items in the progress info mean.

With an option name as argument, prints more help for that option.

Options have keywords associated with them (shown in their help). With a keyword as argument, prints a list of all the options that are associated with the keyword.

If a boolean or integer argument is omitted, true or 1 is the implied value.

ignore_error_option/0

ignore_error_option() -> option_spec()

Error categories that should be ignored

Concuerror will not report errors of the specified kind: - abnormal_exit: processes exiting with any abnormal reason; check -h treat_as_normal and -h assertions_only for more refined control - abnormal_halt: processes executing erlang:halt/1,2 with status /= 0 - deadlock: processes waiting at a receive statement - depth_bound: reaching the depth bound; check -h depth_bound

instant_delivery_option/0

instant_delivery_option() -> option_spec()

Make messages and signals arrive instantly

Assume that messages and signals are delivered immediately. Setting this to false enables "true" Erlang message-passing semantics, in which message delivery is distinct from sending.

interleaving_bound_option/0

interleaving_bound_option() -> option_spec()

Maximum number of interleavings

The maximum number of interleavings that will be explored. Concuerror will stop exploration beyond this limit.

keep_going_option/0

keep_going_option() -> option_spec()

Keep running after an error is found

Concuerror stops by default when the first error is found. Enable this option to keep looking for more errors.

It is usually recommended to modify the test, or use the --ignore_error / --treat_as_normal options, instead of this one.

module_option/0

module_option() -> option_spec()

Module containing the test function

Concuerror begins exploration from a test function located in the module specified by this option.

There is no need to specify modules used in the test if they are in Erlang's code path. Otherwise use --file, --pa or --pz.

no_output_option/0

no_output_option() -> option_spec()

Do not produce an analysis report

Concuerror will not produce an analysis report.

non_racing_system_option/0

non_racing_system_option() -> option_spec()

No races due to 'system' messages

Assume that any messages sent to the specified (by registered name) system process are not racing with each-other. Useful for reducing the number of interleavings when processes have calls to e.g. io:format/1,2 or similar.

observers_option/0

observers_option() -> option_spec()

Synonym for --use_receive_patterns

See also: use_receive_patterns_option/0.

optimal_option/0

optimal_option() -> option_spec()

Synonym for --dpor optimal (true) | source (false)

See also: dpor_option/0.

output_option/0

output_option() -> option_spec()

Filename to use for the analysis report

This is where Concuerror writes the results of the analysis.

pa_option/0

pa_option() -> option_spec()

Add directory to Erlang's code path (front)

Works exactly like erl -pa.

parse_cl/1

parse_cl(CommandLineArgs::[string()]) -> {run, options()} | {return, concuerror:analysis_result()}

Converts command-line arguments to a proplist using getopt

This function also augments the interface of getopt, allowing

print_depth_option/0

print_depth_option() -> option_spec()

Print depth for log/graph

Specifies the max depth for any terms printed in the log (behaves just as the additional argument of ~W and ~P argument of io:format/3). If you want more info about a particular piece of data in an interleaving, consider using erlang:display/1 and checking the standard output section in the error reports of the analysis report instead.

pz_option/0

pz_option() -> option_spec()

Add directory to Erlang's code path (rear)

Works exactly like erl -pz.

quiet_option/0

quiet_option() -> option_spec()

Synonym for --verbosity 0

Do not write anything to standard error.

See also: verbosity_option/0.

scheduling_bound_option/0

scheduling_bound_option() -> option_spec()

Scheduling bound value

The maximum number of times the rule specified in --scheduling_bound_type can be violated.

scheduling_bound_type_option/0

scheduling_bound_type_option() -> option_spec()

* Schedule bounding technique

Enables scheduling rules that prevent interleavings from being explored. The available options are: - none: no bounding - bpor: how many times per interleaving the scheduler is allowed to preempt a process. * Not compatible with Optimal DPOR. - delay: how many times per interleaving the scheduler is allowed to skip the process chosen by default in order to schedule others. - ubpor: same as bpor but without conservative backtrack points. * Experimental, unsound, not compatible with Optimal DPOR.

scheduling_option/0

scheduling_option() -> option_spec()

Scheduling order

How Concuerror picks the next process to run. The available options are oldest, newest and round_robin, with the expected semantics.

show_races_option/0

show_races_option() -> option_spec()

Show races in log/graph

Determines whether information about pairs of racing instructions will be included in the logs of erroneous interleavings and the graph.

strict_scheduling_option/0

strict_scheduling_option() -> option_spec()

Force preemptions when scheduling

Whether Concuerror should enforce the scheduling strategy strictly or let a process run until blocked before reconsidering the scheduling policy.

symbolic_names_option/0

symbolic_names_option() -> option_spec()

Use symbolic process names

Replace PIDs with symbolic names in outputs. The format used is: <[symbolic name]/[last registered name]> where [symbolic name] is:

- P, for the first process and - [parent symbolic name].[ordinal], for any other process, where [ordinal] shows the order of spawning (e.g. <P.2> is the second process spawned by <P>). The [last registered name] part is shown only if applicable.

test_option/0

test_option() -> option_spec()

Name of test function

This must be a 0-arity function located in the module specified by --module. Concuerror will start the test by spawning a process that calls this function.

timeout_option/0

timeout_option() -> option_spec()

How long to wait for an event (>= 500ms)

How many ms to wait before assuming that a process is stuck in an infinite loop between two operations with side-effects. Setting this to infinity will make Concuerror wait indefinitely. Otherwise must be >= 500.

treat_as_normal_option/0

treat_as_normal_option() -> option_spec()

Exit reason treated as normal (i.e., not reported as an error)

A process that exits with the specified atom as reason, or with a reason that is a tuple with the specified atom as a first element, will not be reported as exiting abnormally. Useful e.g. when analyzing supervisors (shutdown is usually a normal exit reason in this case).

use_receive_patterns_option/0

use_receive_patterns_option() -> option_spec()

Use receive patterns for racing sends

If true, Concuerror will only consider two message deliveries as racing when the first message is really received and the patterns used could also match the second message.

verbosity_option/0

verbosity_option() -> option_spec()

Verbosity level (0-7)

The value of verbosity determines what is shown on standard error. Messages up to info are always also shown in the output file. The available levels are the following:

0 (quiet) Nothing is printed (equivalent to --quiet) 1 (error) Critical, resulting in early termination 2 (warn) Non-critical, notifying about weak support for a feature or the use of an option that alters the output 3 (tip) Notifying of a suggested refactoring or option to make testing more efficient 4 (info) Normal operation messages, can be ignored 5 (time) Timing messages 6 (debug) Used only during debugging 7 (trace) Everything else

version_option/0

version_option() -> option_spec()

Display version information


Generated by EDoc