Если компьютер вдруг дал сбой в процессе записи информации или пропало электричество, файловая система дискового накопителя также может повредиться.

Это означает, что рабочие и персональные файлы могут уже не открыться, а программы могут перестать корректно работать. Решить эту проблему смогли исследователи из Массачусетского технологического института (MИТ).

В ходе октябрьской конференции ACM Symposium on Operating Systems Principles они покажут первую файловую систему FSCQ, которая математически гарантирует, что данные не потеряются даже в процессе непредвиденных сбоев ОС. Хотя предложенная файловая система является медленной по сравнению с современными аналогами, специалисты планируют улучшить ее производительность в будущем.

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

Отличием разработки MИТ является то, что с помощью специальной утилиты с именем Coq компьютер может описать системные объекты и поведенческие связи между ними в условиях форс-мажора. Это гарантирует, что при сбое компьютер не запишет файл в ненужное место или забудет обнулить удаленный. Проведенные тесты показывают, что файловая система FSCQ способна корректно восстановить данные в случае непредвиденных ситуаций.