Персистентная семантика файловой системы ext4 и верификация в ней

При работе с файлами возможны слабые поведения: ядро, файловая система и железо влияют на порядок операций и их атомарность. По сравнению аналогичными эффектами в памяти, при работе с диском добавляется вопрос персистентности -- в каком состоянии останутся файлы после внезапного прерывания питания или kernel panic. Отсутствие исчерпывающей документации усложняет понимание особенностей файловых систем. В результате программисты допускают ошибки, ведущие к потере данных. Первым шагом к решению этой проблемы является формализация файловых систем. В докладе мы рассмотрим Linux ext4 и её формальную модель, интегрированную с моделью памяти C/С 11. Кроме того, обсудим адаптацию алгоритма проверки моделей GenMC[1] для верификации программ, работающих с файлами. В конце будут приведены примеры ошибок, которые удалось найти с помощью адаптированного GenMC в текстовых редакторах, таких как vim и nano. Докладчик: Илья Кайсин