Создана «первая файловая система, устойчивая к сбоям любого типа»

20 марта 2008

smart

Новая файловая совокупность

Исследователи из Массачусетского технологического университета (Massachusetts Institute of Technology, MIT) создали файловую совокупность, которая снабжает сохранность данных при любых сбоях в работе компьютера либо сервера — будь-то программный либо аппаратный сбой, неожиданное отключение электропитания либо удар молнии (такой же, что сравнительно не так давно стал причиной безвозвратной утрата данных в дата-центре Гугл).

Файловая совокупность с математической гарантией

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

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

Формальная верификация

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

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

Создана «первая файловая система, устойчивая к сбоям любого типа»
Создана файловая совокупность, устойчивая к сбоям любого типа

Coq Proof Assistant

Исследователи, применяя язык программирования Coq, досконально обрисовали все составные части вычислительной совокупности. К примеру, они дали определение тому, что такое диск а также бит информации, поведал доцент кафедры вычислительной техники MIT и один из авторов работы Николай Зелдович (Nickolai Zeldovich).

Описание связей

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

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

Возможности формальной верификации

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