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
andnodes.substitute()
)writing inputs to files (
nodeio.write_smtlib_for_checking
)pickling (
nodes.__getstate__
andnodes.__setstate__
)