Некоторое время назад я попробовал найти формальное доказательство безопасной работы с памятью, которое реализовано в Rust, но так и не смог его найти. После чего у меня сложилось впечатление, что доказательство в формальном виде и вовсе отсутствует, а вся концепция безопасного управления памятью на основе "владения и заимствования" формально не доказана и держится только на честном слове.
Я не являюсь специалистом по Rust, но после просьбы помочь разобраться этим вопросом, был переадресован искать эту очевидную информацию самостоятельно, так как "джентльменам верят на слово". Тогда как косвенным подтверждением моего предположения об отсутствии формального доказательства в общем виде, является тот факт, что отсутствует и полный список разрешающих и/или запрещающих проверок, которые реализованы в самом компиляторе языка.
Я хочу рассказать про изыскания о формальном доказательстве безопасной работы с памятью на основе владения и заимствования (независимо от языка программирования или реализации компилятора), которое основано на собственных данных и рассуждениях.
Требования для языков программирования
Если говорить не про эзотерические или учебные языки программирования, а про серьезные, которые предназначенные для разработки коммерческих приложений, то обязательным и безусловным требованием у такого языка должна быть возможность реализации любого из уже существующих алгоритмов, придуманных и реализованных ранее.
Поэтому все создатели новых языков так или иначе вынуждены реализовывать типовые алгоритмы, которые будут входить в его стандартную библиотеку. И одним из таких базовых алгоритмов является список.
Свя́зный спи́сок — базовая структура данных в информатике, состоящая из узлов, которая содержит данные и ссылки («связи») на следующий и/или предыдущий узел списка.
Односвязный список — список, каждый узел которого состоит из элемента и ссылки на следующий элемент. Самый первый элемент списка называют головой (head) односвязного списка, а последний — хвостом (tail). Последний элемент односвязного списка в качестве ссылки содержит nullr-значение.
Двусвязный список — это разновидность связного списка, при которой переход по элементам возможен в обоих направлениях (как вперёд, так и назад). В отличие от односвязного списка, в двусвязном ссылки в каждом узле указывают не только на следующий, но и на предыдущий узел в списке, благодаря чему, по двусвязному списку можно перемещаться вперёд и назад.
Реализация связного списка на любом языке программирования является обязательным и необходимым минимумом, чтобы такой язык можно было считать претендентом на роль "замены" какого либо из основных языков на текущее время (С, С++, Java и т.д.)
Проблема списков в концепции безопасной работы с памятью на основе "владения"
Если говорить про концепцию безопасной работы с памятью на основе "владения", то реализация любого вида списков будет очень нетривиальной задачей и примером этого является язык Rust, как самый очевидный образец возникающих сложностей при реализации списков Связной список на Rust в стиле С/C++ / Хабр, где используются небезопасные элементы, или LinkedList in std::collections — Rust (имеет уточнение "This is a nightly-only experimental API").
Если обращать внимание только на техническую сторону этого вопроса, то сложно не заметить некоторые затруднения в реализации этого базового алгоритма, тогда как он легко повторяется любым, даже начинающим программистом, на других языках.
И если вернуться к самому началу статьи (что нет формального доказательства безопасной работы с памятью на основе владения и заимствования), то я был вынужден разобраться в данном вопросе самостоятельно, так как формального доказательства для Rust я не нашел, но похожую проблему мне пришлось изучать в рамках собственных проектов (язык программирования NewLang и его концепция безопасной работы с памятью для С++ в виде отдельного проекта Memory safety (memsafe) single-header libraries and Clang compiler plugin for safe C++)
В результате изучения теории, поиска информации в интернете и написания кода для проверки множества гипотез, мне кажется, удалось найти формальное доказательство части концепции безопасной работы с памятью на основе "владения". Правда нашел вовсе не то, что искал, и очень боюсь, что мои выводы не понравятся популяризаторам Rust.
Реализация алгоритма "связный список" в концепции безопасного управления памятью на основе "владения"
Имеем следующую цепь рассуждений:
- Безопасное управление памятью на основе владения — это сочетание RAII с концепцией владения, когда каждое значение в памяти должно иметь только одну переменную-владельца.
- Связной список — базовая структура данных, состоящая из узлов, который имеет ссылку («связь») на следующий и/или предыдущий узел.
- В концепции владения, каждый узел списка должен быть единственным владельцем узла, на который он ссылается.
- Если узел списка оформлен в стиле ООП (структуры или классы), тогда ссылка ("связь") должна иметь тип, точно такой же как и тип самого узла, т.е. быть рекурсивной, что сложно сочетается с RAII.
- Если использовать доказательство «от противного» (лат. contradictio in contrarium), и допустить, что все же возможно реализовать связной список в концепции безопасного управления памятью на основе "владения", то для двусвязных списков ссылки на узлы должны быть более чем в одном экземпляре (вперед и назад), что противоречит изначальной концепции единственного владельца ссылки, что противоречит изначальному утверждению и опровергает проверяемую гипотезу.
Таким образом можно сделать вывод, что реализовать как алгоритм "двусвязный список" в концепции безопасного управления памятью на основе "владения" с единственным владельцем узла невозможно (а скорее всего, также односвязный и кольцевой, так как в их случае один элемент списка так же должен иметь двух владельцев).
Какие выводы?
Концепция управления памятью на основе владения и заимствования (временной передачи владения) не позволяет реализовать как минимум один базовый алгоритм без использования магических механизмов (обычных ссылок или применения небезопасного кода), из чего следует вывод, что некоторые новые концепции разработки программ могут быть не в состоянии реализовать уже существующие "базовые" алгоритмы.
Однако это не означает, что новая концепция является ущербной. В данном случае, это классическая реализация алгоритма список изначально является "не безопасной", из-за этого и становится невозможно реализовать данный алгоритм общепринятым способом, так как он не соответствует новой концепции, направленной на повышение безопасной работы с динамической памятью.
Что же касается языка Rust, то большое ему спасибо за поднятую проблему. И пусть я считаю, что его текущая реализация еще далека от совершенства, но сам язык постоянно развивается и движется в правильном направлении.
И чтобы ему помочь, хочу предложить немного доработать концепцию безопасного управления памятью в Rust с учетом описанной выше информации. А именно, не пытаться встроить не безопасные способы работы с памятью, даже несмотря на то, что они считаются "классикой", а немного доработать саму концепцию "владения и заимствования" хотя бы одним из следующих вариантов:
- Добавить в концепцию управления памятью не только владеющие (сильные) указатели, но и слабые (не владеющие) ссылки. Т.е. контролировать не просто "заимствование", т.е. переход владения, которое контролирует компилятор языка во время компиляции, но и реализовать механизм проверки валидности ссылки в рантайме.
- Немного дополнить концепцию "владения и заимствования", уточнив термин "заимствование", и трактовать его не как переход владения для сохранения постулата "единственности владельца", на допустить возможность создания копий объекта во временных переменных, время жизни которые жестко детерминировано и контролируется компилятором.
Любой из предложенных способов разрубит Гордиев узел проблем, связанных с реализацией связных списков в концепции безопасного управления памятью на основе "владения" без добавления в нее пустых указателей или небезопасного кода.
Ведь связный список, это в первую очередь интерфейс и способ взаимодействия с данными, а не внутренний алгоритм его реализации. Ну и пусть, что в концепции владения, реализация связного списка будет не очень оптимальной (например, все элементы списка нужно хранить в общем контейнере, а связи списка делать с помощью слабых указателей). Но это будет честная реализация, которая гарантирует корректную работу с динамической памятью без каких либо исключений и небезопасных блоков.
А когда потребуется скорость, то всегда остается возможность сделать UNSAFE реализацию конкретного алгоритма, но без добавления в основу языка сложных синтаксических конструкций в ущерб основной идее языка и понятности его синтаксиса.
