В MIT объявили о создании файловой системы, которая сохранит данные даже при ударе молнии

В MIT объявили о создании файловой системы, которая сохранит данные даже при ударе молнии

Как поясняет CNews, файловая система описывает метод взаимодействия операционной системы с накопителем информации и представляет собой алгоритм, модуль операционной системы. И если в работе компьютера или сервера происходит сбой, когда ОС записывает данные на жесткий диск или SSD-накопитель, данные в большинстве случаев оказываются повреждены и их нельзя прочесть. Таким образом, часы работы могут быть потрачены впустую.

Для того чтобы избежать подобной ситуации, инженеры из MIT создали "первую файловую систему, математически гарантирующую сохранность данных при возникновении сбоев". Полный доклад с описанием системы они планируют представить на конференции ACM Symposium on Operating Systems Principles в октябре 2015 года.

Новая файловая система базируется на таком понятии в программировании, как формальная верификация, и использует систему управления формальными доказательствами Coq Proof Assistant с собственным языком программирования. Сама файловая система написана на этом же языке.

"Формальная верификация - это математическое описание допустимых границ работы компьютерной программы и доказательство того, что эта программа никогда не выйдет за эти границы", - поясняет сайт MIT News.

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

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

Источник:
NEWSru.com