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

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

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

https://research.jetbrains.org/ru/groups/plt_lab