Повторение одного и того же анализа сокращает время выполнения. Как этого избежать?

Я заметил, что многократное повторение одного и того же анализа резко сокращает время, необходимое для его завершения. В моем случае генерация, которая занимает 1700 мс при первом запуске, занимает всего 200 мс после нескольких повторений.

Я предполагаю, что анализатор или лежащие в его основе SAT-решатели отслеживают предыдущий анализ, и в большинстве случаев это, безусловно, к лучшему.

Но в настоящее время я хотел бы иметь более или менее постоянное время завершения. Итак, мой вопрос:

(tl;dr) Есть ли способ очистить "кэш" анализатора (кроме перезапуска анализатора)?

ИЗМЕНИТЬ

Я только что сделал несколько запусков этой моей модели, и вот что я получил:

прогон №1: 113309 переменных. 3023 первичных переменных. 298922 статей. 1964 мс.

прогон №2: 113309 переменных. 3023 первичных переменных. 298922 статей. 1081 мс.

прогон №3: 113309 переменных. 3023 первичных переменных. 298922 статей. 514 мс.

прогон №4: 113309 переменных. 3023 первичных переменных. 298922 статьи. 380 мс.

прогон №5: 113309 переменных. 3023 первичных переменных. 298922 статьи. 342 мс.

прогон №6: 113309 переменных. 3023 первичных переменных. 298922 статей. 438 мс.


alloy
person Loïc Gammaitoni    schedule 15.10.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я замечал одно и то же поведение много раз, и я никогда не был уверен, почему это происходит. Насколько я знаю, ни Alloy Analyzer, ни Kodkod не поддерживают какой-либо явный кеш (конечно, есть кеши, используемые в рамках одного перевода/выполнения, но я не думаю, что они переносятся между выполнениями).

Мое простое объяснение состоит в том, что первый «медленный» запуск происходит из-за «холодного запуска». Одним из аргументов в пользу этого является то, что если вы открываете две несвязанные модели Alloy и сначала выполняете команду из первой модели, а затем выполняете команду из второй модели, второе выполнение (по моему опыту) все равно выполняется «быстрее», чем когда одно и то же команда выполняется из холодного пуска.

person Aleksandar Milicevic    schedule 15.10.2014
comment
Я думаю, что это немного больше, чем холодный старт, потому что он продолжает улучшаться раз за разом. Я отредактировал свой вопрос, добавив производительность нескольких прогонов. - person Loïc Gammaitoni; 15.10.2014
comment
Именно такое поведение я замечал в прошлом. В вашем примере первый запуск, вероятно, будет медленным из-за холодного запуска. Все остальные прогоны похожи; в решателе SAT также присутствует некоторая недетерминированность/рандомизация, поэтому повторные прогоны одной и той же задачи редко приводят к точно такому же результату. Однако я не исключаю, что в анализаторе сплавов что-то происходит, что также влияет на общее время. Однако перевод Alloy на Kodkod и перевод Kodkod на SAT являются детерминированными. Я никогда не проводил дальнейших исследований по этому вопросу. - person Aleksandar Milicevic; 16.10.2014
comment
@LoïcGammaitoni Кроме того, не забывайте, что Alloy работает на Java. Существуют некоторые потенциальные недетерминированные факторы JVM, такие как JIT-компиляция и сборка мусора, хотя вряд ли они сами по себе являются причиной. - person afsantos; 24.10.2014