Support minimization for scenarios that contain blocking tasks

[dmitrii-artuhov]

Описание

В настоящее время минимизация сценариев не работает для сценариев, содержащих задачи, которые могут блокироваться во время выполнения (например, блокировки мьютекса и т.д.).

Решение

Варианты решения:

1. Чтобы поддержать минимизацию с блокировками надо логику удаления таски поменять:
   • Как сделано сейчас: я пробую удалить таску, и если хоть какая-та нелинеаризуемая история найдется, то помечаю таску как удаленную. Если не смог найти такую историю, то оставляю эту таску как есть.
   • Как должно быть: в процессе попытки найти новую нелинеаризумую историю я еще должен проверять, что, то, как сейчас сценарий исполняется, не приведет к дедлоку (то есть надо спросить у верификатора, можно ли применить следующую таску при перезапуксе сценария -- также как и для генерации сценариев работает). Если, все-таки, верификатор говорит, что следующую таску нельзя скедулить, то останавливаем генерацию этой истории и пробуем заново. Если все попытки найти новую историю провалились (все они либо получились линеаризуемыми, либо верификатор не разрешил довести их до конца, то мы говорим, что эту таску удалить не получилось и продолжаем минимизацию дальше)
2. Подумать как сделать верификатор, который бы мог посмотрев не сценарий сказать, есть ли у него варианты скедулинга, где в нем все таски исполнятся. Но это звучит сложно и не понятно, как такое могло бы работать (по крайней мере мне не понятно).
3. TODO... Другие варианты?