Module timing 

Lightweight, opt-in timing instrumentation.

Enabled by setting the CHARON_TIMINGS environment variable. Set it to 1 to get a human-readable report on stderr at the end of the run; set it to a file path to additionally append the measurements as csv lines to that file.

Scopes can be nested: we report both the total (wall) time spent in a scope and the “self” time, i.e. the time not spent inside a nested instrumented scope.

Structs

Guard

A running measurement; the timing is recorded when this is dropped.

Measure

Constants

NESTED 🔒

Time spent in nested scopes, for the currently-running scope.

Statics

MEASURES 🔒

Measurements are aggregated globally (translation is single-threaded but rustc may call us from several threads, hence the mutex).

SETTING 🔒

Whether timing is enabled at all.

Functions

enabled

report

Print the timing report on stderr, and append it to the file given in CHARON_TIMINGS if it isn’t 1.

scope

Time the given scope, if timings are enabled.

scope_lazy

Same as scope_with but only computes the suffix if timings are enabled.

scope_with

Same as scope but allows refining the name dynamically.

time

Time the given closure.