Profiling

VerCors can generate a profile in the pprof format. This only works on unix-like systems, and works best on linux. The file profile.pprof.gz is generated in the current directory when passing the flag --profile:

$ vercors --profile some/example.java
(...)
$ ls profile.pprof.gz
profile.pprof.gz

It's safe to stop vercors with control-C (SIGINT), and the profile will contain all samples up to that point, with the exception of childSys and childUser (explained below).

It can be viewed with e.g. the pprof tool, e.g.:

$ pprof -http=:1234 profile.pprof.gz

Samples

The profile contains several different samples, listed under "Sample":

• wall: The amount of real time a task took (as though you looked at a clock on the wall). Under parallelism this measurement does not aggregate nicely
• (...)User: The amount of time spent on the CPU. Under parallelism the time is summed up, i.e. it can go considerably faster that wall time.
• (...)Sys: The amount of time spent in the kernel, as requested by the process. Indicative of file i/o etc.
• child(...): Measures the time spent in child processes. For VerCors this is strictly the SMT backend, usually z3. It is only populated once an entire child process has completed, hence in practice the entire z3 time is accounted under "Verification" without further specifying.
• self(...): Measures the time spent in our own process, excluding any child processes
• agg(...): aggregate of child and self usage.
• agg: all child and self usage, both system time and user time, all summed.

Measuring for publication

Use aggUser as a stable measurement for the amount of computation VerCors has done: it represents the total amount of computation time VerCors has used.

Diagnosing slow proof goals

View > Flame Graph is most useful for this. You can use selfUser to diagnose cases where silicon itself (without z3) is slow. wall is most useful when including z3, since unfortunately childUser cannot track the individual usage by verifier or goal.

The width of bars in the flame graph represent the amount of time spent on them. Click on a bar to zoom into it horizontally, click on bars above the focused bar to zoom out again.

In silicon we try to compute a hierarchy, trying to obtain in order:

• The entity being verified (method, function, predicate)
• Then the statement being executed
• Then the assertion being in- or exhaled
• Then the branch conditions under which we are dealing with the assertion

We also include some "comment" records, indicated with /* and */.