Поделиться
Создана «первая файловая система, устойчивая к сбоям любого типа»
Американские исследователи создали файловую систему, обеспечивающую 100-процентную защиту от повреждения данных при возникновении сбоев любого типа.Новая файловая система
Исследователи из Массачусетского технологического института (Massachusetts Institute of Technology, MIT) разработали файловую систему, которая обеспечивает сохранность данных при любых сбоях в работе компьютера или сервера — будь-то программный или аппаратный сбой, внезапное отключение электропитания или удар молнии (такой же, который недавно привел к безвозвратной потере данных в дата-центре Google).
Файловая система с математической гарантией
Файловая система описывает метод взаимодействия операционной системы с накопителем информации и представляет собой алгоритм, модуль операционной системы. И если в работе компьютера или сервера происходит сбой, когда ОС записывает данные на жесткий диск или SSD-накопитель, данные в большинстве случаев оказываются повреждены, и их нельзя прочесть. Таким образом, часы работы могут быть потрачены впустую.
Для того чтобы избежать подобной ситуации, инженеры из MIT создали «первую файловую систему, математически гарантирующую сохранность данных при возникновении сбоев». Полный доклад с описанием системы они планируют представить на конференции ACM Symposium on Operating Systems Principles в октябре 2015 г.
Формальная верификация
Новая файловая система базируется на таком понятии в программировании, как формальная верификация, и использует систему управления формальными доказательствами Coq Proof Assistant с собственным языком программирования. Сама файловая система написана на этом же языке.
«Формальная верификация — это математическое описание допустимых границ работы компьютерной программы и доказательство того, что эта программа никогда не выйдет за эти границы», — поясняет сайт MIT News.
Создана файловая система, устойчивая к сбоям любого типа
Coq Proof Assistant
Исследователи, используя язык программирования Coq, досконально описали все составные части вычислительной системы. Например, они дали определение тому, что такое диск и даже бит информации, рассказал доцент кафедры вычислительной техники MIT и один из авторов работы Николай Зелдович (Nickolai Zeldovich).
Описание взаимосвязей
Затем было создано формальное описание взаимосвязей между моделями поведения этих компонентов в условии возникновения сбоя. Часть работы заключается в том, что Coq Proof Assistant, в автоматизированном режиме, проверяет, что работа файловой системы соответствует установленным взаимосвязям, описанным в доказательстве.
Создавая файловую систему, исследователи около 10 раз возвращались назад и изменяли ее спецификации, чтобы создать систему с полной защитой от сбоев. При этом около 90% всего рабочего времени было потрачено на описание компонентов вычислительной системы и логических взаимосвязей между ними.
Перспективы формальной верификации
По словам участников проекта, созданная ими файловая система работает достаточно медленно по сравнению с современными мерками, поэтому о коммерческом применении речи пока не идет. Однако примененный ими метод может быть использован в более сложных системах. В целом, отмечают исследователи, формальная верификация позволяет значительно упростить создание надежных и эффективных технологий работы с данными.
Короткая ссылка
