Легковесные формальные методы для верификации примитивов синхронизации

Мало кто не слышал про такие проекты, как seL4 или CompCert, потратившие невероятное количество сил на формальную верификацию микроядра операционной системы и компилятора языка Cи соответственно.

Результаты этих проектов поражают воображение. Ещё недавно было страшно помыслить о верификации столь сложных программных систем. Но формальные методы не появились из воздуха, а существовали довольно давно. В том числе легковесные, к которым можно отнести модел-чекинг.

Сегодня мы хотели бы поделиться ссылкой на страницу, на которой Расс Кокс (Russ Cox) собрал всю историческую информацию про верификацию примитивов синхронизации в ядре Plan 9.

Применение Spin/Promela помогло найти реальные проблемы в реализации рандеву, что использовалась в системе, ну и, конечно, исправить ее.

Обратите внимание, насколько просты модели на этом языке. При помощи Spin/Promela можно верифицировать сетевые протоколы, примитивы синхронизации и параллельные алгоритмы.

Инструмент за долгие годы существования стал стабильным и быстрым, его отлично документировали. Почему бы не попробовать его в своих задачах?

#lilerature