FreeBSD Manual Pages
RUMUR(1) General Commands Manual RUMUR(1) NAME rumur - Yet another explicit state model checker SYNOPSIS rumur options --output FILE [FILE] DESCRIPTION Rumur is a reimplementation of the model checker CMurphi with improved performance and a slightly different feature set. OPTIONS --bound STEPS Set a limit for state space exploration. The verifier will stop checking beyond this depth. A bound of 0, the default, indicates unlimited exploration. That is, the verifier will not stop checking until it has expanded all seen states. --colour [auto | off | on] Enable or disable the use of ANSI colour codes in the verifier's output. The default is auto, to auto-detect based on whether the verifier's stdout is a TTY. --counterexample-trace [diff | full | off] Set how counterexample traces are printed when an error is found during checking. diff, the default, prints each state showing only the differences from the previous state. full shows the en- tire contents of each state. off disables counterexample trace printing altogether. --deadlock-detection [off | stuck | stuttering] Enable or disable deadlock detection. Rumur has the ability to generate a verifier that notices when there is no valid transi- tion out of a state and raise an error in this scenario. The possible modes for this check are: • off No deadlock checks are performed. • stuck A deadlock is reached when arriving at a state from which there are no enabled transitions, and an er- ror is signaled in this case. • stuttering A deadlock is reached in the same circum- stances as for the stuck option or additionally if there are enabled transitions but these all result in an identical state. For CMurphi users, this is the sce- nario that CMurphi considers to be a deadlock. This defaults to stuttering. However, whether such a deadlock actually represents a problem depends on the properties of the system you are modelling. Hence you may want to change deadlock detection. --debug or -d Enable debugging options in the generated verifier. This in- cludes enabling runtime assertions. This will also output debug- ging messages while generating the verifier. --help Display this information. --max-errors COUNT Number of errors the verifier should report before considering them fatal. By default this is 1, that is exit as soon as an er- ror is encountered. However, you may wish to set a higher value to get multiple error traces from a single run. --monopolise Assume that the machine the generated verifier will run on is the current host and that it will be the only process running. This flag causes the verifier to upfront allocate a seen set that will eventually occupy all of memory. That is, it is the same as passing --set-expand-threshold 100 and --set-capacity with the total amount of physical memory available on the cur- rent machine. --output FILE or -o FILE Set path to write the generated C verifier's code to. --output-format [machine-readable | human-readable] Change the format in which the verifier displays its output. By default, it uses human-readable which results in progress output and then a final summary of the result. Using machine-readable generates output in an XML format suitable for consumption by a following tool in an I/O pipeline. --pack-state [on | off] Set whether auxiliary state data is compressed in the generated verifier. Compression (on, the default) saves memory at the ex- pense of runtime. That is, by default the verifier will try to minimise memory usage. If your model is small enough to comfort- ably fit in available memory, you may want to set this to off to accelerate the checking process. --pointer-bits [auto | BITS] Number of relevant (non-zero) bits in a pointer on the target platform on which the verifier will be compiled. This option can be used to tune pointer compression, which can save memory when checking larger models. With the default, auto, 5-level paging is assumed for x86-64, meaning pointers can be compressed and stored in 56 bits. Other platforms currently have no auto-detec- tion, and will store pointers uncompressed at their full width. If you know a certain number of high bits of pointers on your target platform are always zero, you can teach Rumur this infor- mation with this option. For example, if you are compiling on an x86-64 platform that you know is using 4-level paging you can pass --pointer-bits 48 to tell Rumur that the upper 16 bits of a pointer will always be zero. --quiet or -q Don't output any messages while generating the verifier. --reorder-fields [on | off] Control whether access to state variables and record fields is optimised by reordering them. By default this is on, causing the order of a model's state variables and fields within record types to be optimised to more likely result in naturally aligned memory accesses, which are assumed to be faster. You should never normally have cause to turn this off, but this feature was buggy when first implemented so this option is provided for de- bugging purposes. --sandbox [on | off] Control whether the generated verifier uses your operating sys- tem's sandboxing facilities to limit its own operations. The verifier does not intentionally perform any malicious or danger- ous operations, but at the end of the day it is a generated pro- gram that you are going to execute. To safeguard against a bug in the code generator, it is recommended to constrain the opera- tions the verifier is allowed to perform if you are using a model you did not write yourself. By default this is off. --scalarset-schedules [on | off] Enable or disable tracking of the permutation of scalarset val- ues for more comprehensible counterexample traces. The permuting of scalarset values that is performed during symmetry reduction leads to paths in the state space where a single scalarset iden- tity does not have the same value throughout the trace. When this option is on (the default), Rumur tracks these permutations and takes them into account when printing scalarset values or reconstructing counterexample traces. The result is more intu- itive and easily understandable traces. Turning this off may gain runtime performance on models that use scalarsets. However counterexample traces will likely be confusing in this configu- ration, as scalarset variables will appear to have their values change arbitrarily. --set-capacity SIZE or -s SIZE The size of the initial set to allocate for storing seen states. This is given in bytes and is interpreted to mean the desired size of the set when it is completely full. That is, the initial allocation performed will be for a number of "state slots" that, when all occupied, will consume this much memory. Default value for this 8MB. --set-expand-threshold PERCENT or -e PERCENT Expand the state set when its occupancy exceeds this percentage. Default is 75, valid values are 1 - 100. Setting a value of 100 will result in the set only expanding when completely full. This may sound ideal, but will actually result in a much longer run- time. --symmetry-reduction [off | heuristic | exhaustive] Enable or disable symmetry reduction. Symmetry reduction is an optimisation that decreases the state space that must be searched by deriving a canonical representation of each state. While two states may not be directly equal, if their canonical representations are the same only one of them need be expanded. To take advantage of this optimisation you must be using named scalarset types. The available options are: • off Do not use symmetry reduction. All scalarsets will be treated as if they were range types. • heuristic Use a symmetry reduction algorithm based on sorting the state data. This is not guaranteed to find a single, canonical representation for each equivalent state, but it is fast and performs reasonably well em- pirically. Using this option, you may explore more states than you need to, with the advantage that you will process each individual state much faster than with exhaustive. This is the default. • exhaustive Use a symmetry reduction algorithm based on exhaustive permutation of the state data. This is guar- anteed to find a single, canonical representation for each equivalent state, but is typically very slow. Use this if you want to minimise memory usage at the ex- pense of runtime. --threads COUNT or -t COUNT Specify the number of threads the verifier should use. If you do not specify this parameter or pass 0, the number of threads will be chosen based on the available hardware threads on the plat- form on which you generate the model. --trace CATEGORY Enable tracing of specific events while checking. This option is for debugging Rumur itself, and lets you generate a verifier that writes events to stderr. Available event categories are: • handle_reads Reads from variable handles • handle_writes Writes to variable handles • memory_usage Summary of memory allocation during check- ing • queue Events relating to the pending state queue • set Events relating to the seen state set • symmetry_reduction Events related to the symmetry re- duction optimisation • all Enable all of the above More than one of these can be enabled at once by passing the --trace argument multiple times. Note that enabling tracing will significantly slow the verifier and is only intended for debug- ging purposes. --value-type TYPE Change the C type used to represent scalar values in the gener- ated verifier. Valid values are auto and the C fixed-width types, int8_t, uint8_t, int16_t, uint16_t, int32_t, uint32_t, int64_t, and uint64_t. The type you select is mapped to its fast equivalent (e.g. int_fast8_t) and then used in the verifier. The default is auto that selects the narrowest type that can contain all the scalar types in use in your model. It is possible that your model does some arithmetic that temporarily exceeds the bound of any declared type in your model, in which case you will need to use this option to select a wider type. However, this is not a common case. --verbose or -v Output informational messages while generating the verifier. --version Display version information and exit. SMT OPTIONS If you have a Satisfiability Modulo Theories (SMT) solver installed, Rumur can use it to optimise your model while generating a verifier. This functionality is not enabled by default, but you can use the fol- lowing options to configure Rumur to find and use your SMT solver. Some examples of solver configuration: # for Z3 with a 5 second timeout rumur --smt-path z3 --smt-arg=-smt2 --smt-arg=-in --smt-arg=-t:5000 ... # for CVC4 with a 5 second timeout rumur --smt-path cvc4 --smt-prelude "(set-logic AUFLIA)" --smt-arg=--lang=smt2 --smt-arg=--rewrite-divk --smt-arg=--tlimit=5000 ... For other solvers, consult their manpages or documentation to determine what command line parameters they accept. Then use the options de- scribed below to instruct Rumur how to use them. Note that Rumur can only use a single SMT solver and specifying the --smt-path option mul- tiple times will only retain the last path given. --smt-arg ARG A command line argument to pass to the SMT solver. This option can be given multiple times and arguments are passed in the or- der listed. E.g. if you specify --smt-arg=--tlimit --smt-arg=5000 the solver will be called with the command line arguments --tlimit 5000. --smt-bitvectors [off | on] Select whether simple types (enums, ranges, and scalarsets) are translated to bitvectors or unbounded integers when passed to the solver. By default, unbounded integers are used (--smt-bitvectors off). If you turn this option on, 64-bit vec- tors are used instead. Whether integers, bitvectors, or both are supported will depend on your solver as well as the SMT logic you are using. --smt-budget MILLISECONDS Total time allotted for running the SMT solver. That is, the time the solver will be allowed to run for over multiple execu- tions. This defaults to 30000, 30 seconds. So if the solver runs for 10 seconds the first time it is called, then 5 seconds the second time it is called, then 20 seconds the third time it is called, it will not be called again. Note that Rumur trusts the SMT solver to limit itself to a reasonable timeout per run, so its final run can exceed the budget. You may want to use the --smt-arg option to pass the SMT solver a timeout limit if it supports one. --smt-path PATH Command or path to the SMT solver. This will use your environ- ment's PATH variable, so if the solver is in one of your system directories you can simply provide the name of its binary. Note that this option has no effect unless you also pass --smt-sim- plification on. --smt-prelude TEXT Text to emit when communicating with the solver prior to sending the actual problem itself. You can use this to set a solver logic or other options. This option can be given multiple times and each argument will be passed to the solver on a separate line. --smt-simplification [off | on] Disable or enable using the SMT solver to simplify the input model. By default, this is automatic, in that it is turned on if you use any of the other SMT options or off if you do not use them. AUTHOR All comments, questions and complaints should be directed to Matthew Fernandez <matthew.fernandez@gmail.com>. LICENSE This is free and unencumbered software released into the public domain. Anyone is free to copy, modify, publish, use, compile, sell, or dis- tribute this software, either in source code form or as a compiled bi- nary, for any purpose, commercial or non-commercial, and by any means. In jurisdictions that recognize copyright laws, the author or authors of this software dedicate any and all copyright interest in the soft- ware to the public domain. We make this dedication for the benefit of the public at large and to the detriment of our heirs and successors. We intend this dedication to be an overt act of relinquishment in per- petuity of all present and future rights to this software under copy- right law. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MER- CHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. For more information, please refer to <http://unlicense.org> RUMUR(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SMT OPTIONS | AUTHOR | LICENSE
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=rumur&sektion=1&manpath=FreeBSD+Ports+14.3.quarterly>