Performance Report 2025

[wadoon]

We notice a decline in the performance of KeY starting in 2020-2021ish.

I conducted a test phalanx by sampling the performance of KeY with weekly sampling. Scripts can be found here: https://github.com/wadoon/key-performance

In short, the result shows that we have three performance regressions:

First Regression

MRs/PRs:

• 2021-06-16T14:01:04.201Z
  492e3ea
  Renovating the Jml Parser

• 2021-06-17T19:36:58.741Z
  f5279ab
  Better exception message in JML parser

**Conclusion: ** We thought that the KeY parser has a bad performance. The JML parser appears freshly on the performance tableau. No much changes between ANTLR3 and ANTLR4 happened.

Second Regression

MRs/PRs:

1. 2022-11-11T13:51:05.697Z
   fda933f
   Translating DL contracts to JML

2. 2022-11-11T18:26:16.251Z
   349bcd8
   Disable proof_references symbolic_execution

3. 2022-11-12T13:14:18.756Z
   a697b43
   Stop the message about java_profile.jfr

4. 2022-11-12T16:52:23.420Z
   523f6ca
   Suppress logback message before configuration

5. 2022-11-13T14:38:38.919Z
   cdfbea6
   Tooltip for the exloration status label

6. 2022-11-13T17:54:35.951Z
   e392db7
   New shell script to separate allowed_fail tests on Jenkins

7. 2022-11-17T17:48:51.673Z
   debeefb
   Remove highlighting artifacts in SequentView with Unicode symbols enabled"),

Conclusion: No obvious failure.

Third regression

MRs/PRs

1. 2023-01-17T16:35:07.012Z
   baeeb8e
   "Move subprojects to top level"

2. 2023-01-20T10:06:21.809Z
   5c86f2c
   Update Checkstyle configuration to latest Checkstyle version

3. 2023-01-20T13:26:19.916Z
   f4c6937
   Reducing the binary filesize by only including the necessary example files

4. 2023-01-22T07:54:05.246Z
   131d42d
   Redux additions

5. 2023-01-22T18:50:03.177Z
   d630da9
   Run the Javac compiler on loading

6. 2023-01-23T16:58:16.585Z
   a906c34
   Fix for Bug in rule application for floating point comparsion #1723 (Rebase after Spotless)"

**Conclusion: ** I would guess on item 5.