Developer Guide

Performance Profiling

ddSMT provides option --profile, which uses cProfile to collect profiling data. Since cProfile has no support for parallelism, ddSMT collects separate profiles for every process and combines them accordingly: it generates one profile for the main process, and one combined profile for all subprocesses.

Reading profiling data

ddSMT dumps cProfile data as .profile.prof (for the main process) (and .profile-<pid>.prof for the subprocesses). ddSMT renders this data using gprof2dot and dot into .png images profile.png and profile-workers.png. These images usually give a pretty good intuition about the performance profile.

Note

Strategy ddmin sometimes does not delegate work to worker processes, but decides to run in sequential mode. If this is the case, the main profile will contain work that you might expect to actually have been delegated.

The “solver side” mostly consists of the checker.check() function, which makes the actual call to the command under test. Calls to subprocess.communicate() and select.poll() are usually responsible for the largest chunk of the run time spent on the “ddSMT side”.

The “ddSMT side” is pretty much everything else. The most expensive parts are usually

• applying a simplification (mutator_utils.apply_simp and nodes.substitute())

• writing inputs to files (nodeio.write_smtlib_for_checking)

• pickling (nodes.__getstate__ and nodes.__setstate__)