Update the USERMANUAL with info about how to do rule profiling in the LLVM backend

[radumereuta]

This could be useful for profiling the Plutus semantics
@ChristianoBraga and @gtrepta can you have a look into this?

[ChristianoBraga]

Profiling your K semantics

General instructions

(This is this post, by @dwightguth, with minor changes in prose and formatting.)

1. The first thing to be aware of is in order to get meaningful data, you need to build the semantics and all of its dependencies with optimizations enabled but without the frame pointer elimination optimization. For example, for EVM, this means rebuilding GMP, MPFR, JEMalloc, Crypto++, SECP256K1, etc with the following exports.

export CFLAGS="-g -O2 -fno-omit-frame-pointer"; export CXXFLAGS="-g -O2 -fno-omit-frame-pointer"

2. You can skip this step, but if you do, any samples within these libraries will not have correct stack trace information, which means you will likely not get a meaningful set of data that will tell you where the majority of time is really being spent. Don't worry about rebuilding literally every single dependency though. Just focus on the ones that you expect to take a non-negligible amount of runtime. You will be able to tell if you haven't done enough later, and you can go back and rebuild more.
   Once this is done, you then build K with optimizations and debug info enabled, like so:

mvn package -Dproject.build.type="RelWithDebInfo"

3. Next, you build the semantics with optimizations and debug info enabled (i.e., kompile -O3 -ccopt -g )

4. Once all this is done, you should be ready to profile your application. Essentially, you should run whatever test suite you usually run, but with perf record -g -- prefixed to the front. For example, for KEVM it's the following command.

perf record -g -- make test-conformance

For best data, don't run this step in parallel.

4. Finally, you want to filter out just the samples that landed within the llvm backend and view the report. For this, you need to know the name of the binary that was generated by your build system. Normally it is interpreter, but e.g. if you are building the web3 client for kevm, it would be kevm-client. You will want to run perf report -g -c $binary_name. If all goes well, you should see a breakdown of where CPU time has been spent executing the application. You will know that sufficient time was spent rebuilding dependencies with the correct flags when the total time reported by the main method is close to 100%. If it's not close to 100%, this is probably because a decent amount of self time was reported in stack traces that were not built with frame pointers enabled, meaning that perf was unable to walk the stack. You will have to go back, rebuild the appropriate libraries, and then record your trace again.

5. Your ultimate goal is to identify the hotspots that take the most time, and make them execute faster. Entries like step and step_1234 like functions refer to the cost of matching. An entry like side_condition_1234 is a side condition and apply_rule_1234 is constructing the rhs of a rule. You can convert from this rule ordinal to a location using the llvm-kompile-compute-loc script in the bin folder of the llvm backend repo. For example,

llvm-kompile-compute-loc 5868 evm-semantics/.build/defn/llvm/driver-kompiled

spits out the following text.

Line: 18529
/home/dwightguth/evm-semantics/./.build/defn/llvm/driver.k:493:10

This is the line of definition.kore that the axiom appears on as well as the original location of the rule in the K semantics. You can use this information to figure out which rules and functions are causing the most time and optimize them to be more efficient.

Makefile target examples

(Uses @gtrepta implementations of the instructions above in KPlutus Makefile.)

In the KPlutus project, two targets were defined to help profiling Untyped Plutus Core language semantics: k-deps-profiling, to build K's dependencies, and build-llvm-profiling that builds the llvm backend with proper settings.

k-deps-profiling target

Essentially, with respect to profiling, this target removes the frame pointer elimination optimization (-fno-omit-frame-pointer) and prevents the use of Release or RelWithDebInfo while building the backend (K_BUILD_TYPE := FastBuild). Otherwise link time optimization (LTO) would be enabled and there would not be possible to tell the linker to disable frame pointer elimination. This target also prevents the compilation of the haskell backend, and sets debuging and optimization flags. Then it triggers making K's dependencies (such as the blockchain plugin) with k-deps. (The need for -fno-omit-frame-pointer here is realted with step 2 above.)

k-deps-profiling: K_MVN_ARGS += -Dhaskell.backend.skip=true                                                                                                                
k-deps-profiling: K_BUILD_TYPE := FastBuild                                                                                                                                
k-deps-profiling: export CMAKE_CXX_FLAGS='-O2 -DNDEBUG -fno-omit-frame-pointer'                                                                                            
k-deps-profiling: k-deps                                                                                                                                                   

build-llvm-profiling target

Again, we should set flags for the build process, again removing the frame pointer elimination optimization but setting the proper optimization level. Finally, it trigger the generation of the LLVM backend with these flags. Note that both targets require removing the frame pointer elimination optimization. Here for the backend itself and in k-deps-profiling for the libraries that the backend uses.

build-llvm-profiling: KOMPILE_OPTS += -O3 -ccopt -fno-omit-frame-pointer                                                                                                   
build-llvm-profiling: $(KPLUTUS_LIB)/$(llvm_kompiled)                                                                                                                      

[ehildenb]

Thank you :) It looks very nice.

[radumereuta]

@ChristianoBraga can you also make a PR and update https://github.com/runtimeverification/k/blob/master/USER_MANUAL.md
with this info?

[radumereuta]

Should be close to this section: https://github.com/runtimeverification/k/blob/master/USER_MANUAL.md#debugging

[Baltoli]

Can this issue be closed now that the information is in the USER_MANUAL? https://github.com/runtimeverification/k/blob/master/USER_MANUAL.md#profiling-your-k-semantics