В октябре на симпозиуме по операционным системам, проводимом aссоциацией вычислительной техники Association for Computing Machinery, специалисты Массачусетского технологического института собираются представить файловую систему, гарантирующую отсутствие потерь данных при сбоях, которые могут быть вызваны отказами питания, программными и аппаратными ошибками и т. п.

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

Ввиду сложности задачи формальной верификации обычно ее проводят для высокоуровневой упрощенной схемы программы. Но исследователи из МТИ, по их словам, выполнили верификацию реального кода файловой системы, воспользовавшись инструментом доказательства теорем Coq, который позволяет на формальном языке описать элементы компьютерной системы и взаимоотношения между ними.

Авторам, по их словам, пришлось на языке Coq описывать, что такое бит, накопитель и т. п., а затем задавать связи между различными компонентами файловой системы в условиях сбоя. После этого было проведено доказательство того, что система будет работать согласно спецификациям, а затем написан сам код. Coq позволил в автоматизированном режиме удостовериться в том, что созданная система соответствовала логическим отношениям, описанным в доказательстве.

Исследователи сообщили, что в процессе реализации системы пришлось многократно переработать ее спецификации, однако 90% усилий ушло все же на составление формализованных определений компонентов. Авторы признают, что получившаяся файловая система работает по современным меркам довольно медленно, и выражают уверенность в том, что примененные ими методы могут быть положены в основу формальной верификации более сложных систем.