Исследователи из Массачусетского технологического института (MIT) разработали файловую систему, которая обеспечивает сохранность данных при любых сбоях в работе компьютера или сервера - будь то программный или аппаратный сбой, внезапное отключение электропитания или удар молнии. Об этом сообщается на сайте института.
Как поясняет CNews, файловая система описывает метод взаимодействия операционной системы с накопителем информации и представляет собой алгоритм, модуль операционной системы. И если в работе компьютера или сервера происходит сбой, когда ОС записывает данные на жесткий диск или SSD-накопитель, данные в большинстве случаев оказываются повреждены и их нельзя прочесть. Таким образом, часы работы могут быть потрачены впустую.
- Создана универсальная программа для автоматического исправления ошибок в исходном коде программ
Для того чтобы избежать подобной ситуации, инженеры из MIT создали "первую файловую систему, математически гарантирующую сохранность данных при возникновении сбоев". Полный доклад с описанием системы они планируют представить на конференции ACM Symposium on Operating Systems Principles в октябре 2015 года.
Новая файловая система базируется на таком понятии в программировании, как формальная верификация, и использует систему управления формальными доказательствами Coq Proof Assistant с собственным языком программирования. Сама файловая система написана на этом же языке.
"Формальная верификация - это математическое описание допустимых границ работы компьютерной программы и доказательство того, что эта программа никогда не выйдет за эти границы", - поясняет сайт MIT News.
Создавая файловую систему, исследователи около 10 раз возвращались и изменяли ее спецификации, чтобы создать систему с полной защитой от сбоев. При этом около 90% всего рабочего времени было потрачено на описание компонентов вычислительной системы и логических взаимосвязей между ними.
По словам участников проекта, созданная ими файловая система работает достаточно медленно по сравнению с современными мерками, поэтому о коммерческом применении речи пока не идет. Однако примененный ими метод может быть использован в более сложных системах. В целом, отмечают исследователи, формальная верификация позволяет значительно упростить создание надежных и эффективных технологий работы с данными.
