ddSMT provides option
--profile, which uses
collect profiling data.
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
Reading profiling data¶
cProfile data as
.profile.prof (for the main
.profile-<pid>.prof for the subprocesses).
ddSMT renders this data using
These images usually give a pretty good intuition about the performance profile.
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
which makes the actual call to the command under test.
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 (
writing inputs to files (