Применимость инcтрумента Spin к верификации протоколов когерентности памяти

Широкое использование методов поиска ошибок в устройствах, которые реализуют протоколы когерентности памяти, основанных на моделировании со случайными воздействиями, не обеспечивает 100%-ной полноты верификации. Некоторые ошибки могут проявиться лишь при возникновении длинных последовательностей событий, таких как кэш-промахи и прием сообщений различными частями системы. Поскольку число таких последовательностей является комбинаторным, вероятность их возникновения во время моделирования со случайными воздействиями резко уменьшается при увеличении их длины.