Profiling

Analyzer performance and precision

Every regression fixture, run under every abstract domain and context policy, natively and in the browser's WebAssembly build. The numbers are measurements on one machine. They show where time and memory go, and they prove nothing about programs outside the corpus.

Cost and precision

Precision and cost by configuration

Every domain can run under different context policies. None analyses each procedure once for all its calls; entry-state analyses it once per distinct entry state; call strings with k = 1 once per calling site. Additional contexts can improve precision and increase running time. The plot compares precision and running time for every combination the snapshot measured.

One row per domain, one dot per context policy. Left: native solve time summed over the corpus. Right: the share of all checks in the corpus the configuration proves. The grey bar spans a domain's policies. A long time bar with a short precision bar indicates a large runtime increase with little precision gain.

Measurement method
  • Each fixture runs under every configuration with the CLI's other defaults (globals warrow, Int refinement to a fixpoint, flow-sensitive program globals). A fixture's own PARAM header is ignored, so every configuration analyzes the same programs.
  • Time is the CLI's own measurement around the solve (--timing), the median of runs. Process start-up, parsing and printing are not in it, so a sum over the corpus is solving alone.
  • A check counts as proved when the CLI prints PROVED for it. The denominator is every check in the corpus once, taken as the most checks any configuration reported for a fixture. A configuration the CLI rejects for a fixture, or one that runs past  s, proves nothing there.

Corpus profile

Distribution of fixture running times

Totals do not distinguish isolated slow fixtures from uniformly slow analysis. A quantile plot, as SV-COMP uses for verifiers, sorts the fixtures by running time. The curve's height at x is the run time of the x-th fastest fixture. A flat curve means uniform cost; a sharp rise at the right end means a few fixtures dominate.

Domain
Native solve time per fixture for the selected domain on a log scale, one line per context policy, each sorted on its own. The lines end where a policy's fixtures run out. A line shorter than the others lost fixtures to rejection or timeout.

Measurement method
  • The same runs and the same solve times as the configuration comparison. Times below about 0.01 ms are at the clock's resolution; the left end of the curves is programs that need almost no solving.
  • Each line is sorted separately, so the x-th point of two lines can be different fixtures. To compare one fixture across policies, use the fixture table.

Scaling

Recursion depth and entry-state contexts

Under entry-state contexts, every distinct abstract argument a recursive procedure is entered with becomes its own context. The program below recurses n levels deep. A domain that distinguishes the arguments, such as Interval, therefore creates n + 1 contexts of h. A finite domain such as Sign creates the same small number at every depth. Growing n measures how the solver scales in the number of contexts, the case that overflowed the playground's stack before the CPS build. 

fun h(i) {
  if (i == 0) { return 3; }
  r = h(i - 1);
  return r;
}
fun main() {
  x = h(n); __voblint_check(x == 3);
}
Solve time against n for every domain, native as solid lines and the WebAssembly build dashed, log–log. A straight line of slope k means time grows like nk.
Right-hand-side evaluations the solver performs, log–log. This counts work independently of the machine. If the count grows more slowly than time, each evaluation is getting more expensive.

Measurement method
  • Every domain under entry-state contexts. Each point is the median of runs of the CLI's own solve timing; peak RSS, in the tooltip, is the whole process's, from the system's time command. A domain's sweep stops at the first n whose run passes  s or fails; the reading names where.
  • Evaluations: the number of eq events in a separate traced run's JSON Lines trace, one per evaluation of an unknown's right-hand side. Tracing slows the run; the repository's tracer gate checks that a traced run gives the same answer as an untraced one.
  • WebAssembly: the playground's bundle under Node with a 512 KiB stack and no trace, timed by the analyzer around the same solve, median of runs.

Data structures

Program size and data-structure costs

The generated code keeps sets and maps as lists. A membership test scans the list, a union inserts element by element, and removing duplicates compares every pair. Each benchmark family varies one program dimension and keeps the others small. Comparing solve time with the evaluation count exposes the cost of the corresponding data structure.

Native solve time against the size n of each family's program, log–log, under Interval. A line ends at the first n whose run passed the time limit. Click a family in the scaling-family table to see the program it generates.
Family What grows Context policy Largest n Time exponent Evaluation exponent Gap

Isabelle has libraries for faster sets and maps. The Collections Framework (Lammich and Lochbihler) refines abstract sets and maps into verified balanced trees and hash tables. Light-weight Containers (Lochbihler) replaces the list-based default of code generation with such structures. Either needs only targeted replacements in the code setup and no change to the soundness proofs.

Measurement method
  • Each family is a generated VIMP program with one size parameter n. It controls variables, statements, globals, call sites, chained procedures, sequential loops, or recursion depth. Every program ends in a check the analyzer proves, so each run does the full work of a real analysis.
  • Call sites run twice. Call strings with k = 1 give every site its own context. Entry-state contexts merge identical calls into one context. Comparing the runs separates context costs from call-site costs.
  • Times are the CLI's own solve timing, the median of runs; evaluations come from a traced run, as in the recursion plot. Exponents are least-squares fits on log–log axes. Timing fits start at n = 100, where start-up no longer dominates. Evaluation fits start at n = 20 because counts are exact and tracing reaches the time limit sooner. A gap of about 1 or more means each evaluation gets roughly n times more expensive, the signature of a linear scan inside the solver's loop.
  • The family with the largest gap also gets a CPU profile, listed with the others in the CPU-profile section.

Scaling family


          
            
            Open this program in the playground
          
        

      

    

    

      

        
CPU profile

        
CPU profiles

      

      

        The timing plots measure each run; a CPU profile attributes that time to functions. A
        sampling profiler interrupts the native analyzer every millisecond and records its call
        stack. In the flame graph, each function bar sits above its caller. The bar width is the share of samples in which the function was on the stack. Wide bars
        near the top are where the time is actually spent.
      

      

        Program
        

        
        
        
        
      

      

        

        

        
Hover a bar for its samples; click to zoom in.

        

        

          Bar width represents samples with the function on the stack. Colour identifies the code's origin. Recursive calls
          of a function are merged into one bar, and its tooltip says how deep the recursion went.
        

      

      

      

        Measurement method
        
    
          
  • The sampling profiler samply
            sampled the native CLI's analysis process at 1 ms intervals until the run ended. The CLI forks this process to enforce its timeout. Function names are the OCaml symbols of the native binary, with the module prefix
            kept and the compiler's numeric suffix dropped. Attaching on macOS needs
            samply setup once; without samply, the script falls back to macOS's
            sample, which keeps only the innermost 512 frames of a stack.
    • 
          
  • A stack is complete when it reaches caml_start_program, where OCaml code
            begins. Some samples lose their callers, particularly those taken inside the garbage collector,
            which the unwinder cannot walk back out of into OCaml frames. They are grouped under
            [callers not recorded], still attributed to the right innermost functions.
            Frames below 0.2% of the samples are folded into their caller.
    • 
          
  • One run per program, on the same machine as the rest of the snapshot. Sample counts
            vary from run to run by a few percent; the shape is what is stable.
    • 
          
  • This profiles the native build. The browser build runs the same OCaml functions, but
            WebAssembly and the CPS translation change their relative cost.
    • 
        

      

    


    

      

        
Browser

        
Native and WebAssembly running times

      

      

        The playground runs the same generated OCaml, compiled to WebAssembly in
        continuation-passing style so deep solver recursion fits a worker's stack. Both builds time
        the same solve, so their ratio measures the overhead of the WebAssembly build. The first plot gives
        it for every configuration, the second fixture by fixture for the one you pick.
      

      

        

        

          Median WebAssembly / native solve time per configuration, over the runs that take at
          least 1 ms natively, log scale. The dashed line is equal time.
        

      

      

        Domain
        

        Context
        

      

      

        

        

          Each dot represents a fixture, with native time on the horizontal axis and WebAssembly time on the vertical axis. Both axes use logarithmic scales.
          Dashed lines mark equal time, twice and ten times as slow in the browser. Dots above the
          1× line are slower in the browser.
        

      

      

      

        Measurement method
        
    
          
  • The WebAssembly measurement runs the playground's bundle under Node with 40 fixtures per process, approximating worker reuse in a page session. The stack is 512 KiB, approximately Chrome's worker stack. Time is the analyzer's own measurement around the solve, without parsing or
            rendering.
    • 
          
  • Native: the CLI's own solve timing, as in the first plot. Both sides are medians of
             runs. Below about 1 ms both clocks are close to their
            resolution, so ratios use only runs above that.
    • 
          
  • Node, not a browser, runs the WebAssembly side. Chrome's engine is the same V8, but its
            worker may schedule and collect garbage differently; the playground's own timing shows
            the number for a real page.
    • 
        

      

    


    

      

        
Fixtures

        
Fixture measurements

      

      

        Every measured run, for one configuration at a time. Sort by a column to find the fixtures
        that drive the timing plots; Unknowns and Contexts come from the solver trace and explain
        most of the differences in time.
      

      

        
        
        
        
      

      

        

          
            

              Fixture
              Time (ms)
              Evaluations
              Unknowns
              Contexts
              Peak RSS (MB)
              Proved
            

          
          
        

      

    


    

      

        
Method

        
Setup and limits