[DaniilVarezkin]

Реализация профилировщика - обёрки над KSolvwer, которая ведёт журнал: что и в каком порядке у солвера вызывали (push, assert, check, pop, запрос модели и так далее), сколько это заняло и чем закончилось. Журнал можно забрать через snapshot() как неизменяемый объект. Он нужен, чтобы потом ksmt-ml мог на этих данных учиться подбирать настройки солвера. Сама обёртка ничего не знает про cvc5, поэтому подойдёт к любому солверу.

• Основу написал Michael Litvinov. Черепикнул из origin/dev/litvinovmitch11/demo

Какие были доработки

• Строгий порядок событий при многопоточной работе. Порядковый номер события и его запись в журнал выполняются в одной критической секции (synchronized). Порядок номеров гарантированно совпадает с порядком записи. Отдельная сортировка в snapshot() и атомарный счётчик больше не нужны. Вызов interrupt() не захватывает блокировку, поэтому его можно выполнить из другого потока во время идущего check. Событие interrupt записывается после вызова.

• Корректное завершение сессии (close). Наблюдаемая длительность профиля фиксируется на первом завершённом close и дальше не растёт. Повторный close не переводит состояние CLOSED в CLOSE_FAILED. Неудачный close у активного профиля помечается отдельно.

• Сужена обработка ошибок записи. Сбой при формировании или записи события (Exception) не нарушает работу обёрнутого солвера. Ошибки уровня JVM (Error, например OutOfMemoryError) больше не подавляются и передаются вызывающему коду. Исключения самого солвера пробрасываются тем же объектом и фиксируются в профиле.

• Структура кода. Журнал событий с ограничением по количеству (EventLog) и счётчики утверждений (AssertionStack: глубина стека, активные и общее число утверждений) вынесены во вложенные классы. Собственных блокировок они не имеют, синхронизацию обеспечивает внешний класс. Поведение при этом не менялось.

• Привязка результатов к проверке. Обращения к model, unsatCore и reasonOfUnknown связываются с последней успешной проверкой. Эта связь сохраняется после assert, push и pop, поскольку, согласно коду KCvc5Solver, cvc5 сбрасывает результат только при следующем check.

• Тесты, измерения, документация.

  • 20 модульных тестов: базовые сценарии, многопоточность, close, обработка ошибок, вложенные задачи, привязка результатов.
  • Бенчмарк накладных расходов на реальном cvc5 (ProfilerOverheadBenchmark). По умолчанию отключён, включается переменной окружения KSMT_PROFILING_BENCHMARK=true. В последнем прогоне на очень лёгких вызовах замедление составило около 15–19%, на нагрузке с настоящим check около 1% (в пределах разброса).
  • README.md модуля с инструкцией по сборке, запуску тестов и бенчмарка.