Семантика персистентности файловой системы ext4

Существенная часть современных приложений – это взаимодействие с файлами. При работе с файловыми системами программисты часто совершают ошибки, о чём свидетельствуют многочисленные отчеты. Одна из основных причин состоит в том, что файловые системы используют алгоритмы оптимизации, которые приводят к труднопрогнозируемым поведениям программ. Поскольку ошибки, связанные с файловым вводом-выводом, сложно найти вручную, для решения этой проблемы применяют средства формальной верификации, которые позволяют автоматически проверить программу. Однако для разработки таких средств необходима формальная модель файловой системы. В данной работе я представляю формальную модель файловой системы ext4, интегрированную со слабой моделью памяти C/C++. Для её построения был разработан обобщённый фреймворк, основанный на декларативном (аксиоматическом) подходе. Затем, путём изучения документации и исходного кода, дискуссий с разработчиками и тестирования, были выделены особенности поведений программ, взаимодействующих с ext4. Наконец, формальная модель ext4 была получена как специализация фреймворка под выделенные особенности. Разработанная семантика легла в основу алгоритма проверки моделей PerSeVerE, что позволило обнаружить ошибки в популярных текстовых редакторах (emacs, vim и nano).