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

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

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

Отличием разработки MIT является проверка свойств финального кода файловой системы, а не высокоуровневой схемы. Для этого используется утилита типа proof assistant с именем Coq, которая предоставляет формальный язык для описания аспектов компьютерной системы и связей между ними. Таким образом, описываются системные объекты и поведенческие связи между ними в условиях форс-мажора.

Ценность представленных исследований кроется даже не в самой разработанной операционной системе. Предложенные методики могут использоваться в других современных ОС или при разработке новых и сделать их гораздо надёжнее.

Источник