JetBrains Research — наука, меняющая мир

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

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

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

Докладчик: Илья Кайсин

[1] GenMC model checker http://plv.mpi-sws.org/genmc/



Семинар пройдет онлайн 21 сентября в 17:30, ссылка Google meet: https://meet.google.com/myu-dhmz-gvu