Comments 60
Для формального доказательства безопасного использования памяти надо сначала формально выразить "безопасное использование памяти".
А ничего, что в иммутабельных языках (эрланге, например) — двусвязный список вообще никак не построить, и это никому не мешает?
Я тоже считаю, что в этом не ничего страшного
Ну так тогда бы я предлагал не менять определение владения, а перестать пытаться накормить пятью хлебами всех — от перлистов до гошников.
Почему-то создатели именно Rust очень боятся сказать: «Тут так не принято», — в ответ на любую, самую безумную, претензию — и бросаются пытаться реализовывать, что уже приводит к куче ничем не оправданных костылей в их модели памяти.
В том же эрланге нет циклов, например. Сколько раз неофиты просили циклы? — Да не сосчитать. Добавили циклы? — Нет. Стали все без исключения кодовые базы от такого решения чище? — Несомненно.
Мне кажется, в Rust-community очень не помешал бы человек с такими же кохонес, как были у Армстронга.
Но эрланг и не претендует на то чтоб на нем писали всё от прошивок микроконтроллеров до вебстраниц. Например, если бы создатели Rust сказали "если при попытке выделения памяти оказалось что памяти нет, то мы делаем panic и точка" то в ядре линукса раста бы не было.
писали всё от прошивок микроконтроллеров до вебстраниц
Эрланг нет, а BEAM — вполне. Ну не прям микроконтроллеры, но эмбеддед — вовсю. А вебстраницы — и подавно. Интерактивные ноутбуки, просто так и для ML.
то в ядре линукса раста бы не было
И кто бы от этого проиграл?
Когда я заинтересовался эрлангом, я услышал что перемножение матриц на нем в тысячу раз медленнее чем на С, на этом мой интерес угас. В общем может на нем и пишут эмбеддед, но раст несколько более низкоуровневый язык и соответственно позволить себе сказать "вот такую штуку на нем сделать нельзя без потери производительности по сравнению с асмом/си" он не может.
И кто бы от этого проиграл?
Популярности раста среди низкоуровневых программистов это нанесло бы непоправимый урон.
С тех пор утекло много воды, эликсир давно может компилироваться напрямую в CUDA, да и перемножением матриц задачи в реальном мире не исчерпываются. Кроме того, я тоже слышал, что авторы раста не осилили написать на нём проект, ради которого он создавался (servo), но интерес не угас (хотя я лично вряд ли стану его использовать в моих задачах).
Все это никак не отменяет мой тезис. Да, задачи у всех разные, лично мне язык на котором математика настолько медленная не интересен, компиляция в cuda тут не поможет.
Аналогично и с растом - сейчас он популярен среди, скажем, программистов микроконтроллеров. Если бы создатели вели себя иначе (ограничивали возможные структуры данных и вообще перестали претендовать на замену Си) - эту часть аудитории он бы точно потерял.
ну так под BEAM циклы есть, во всяком случае то, что "неофиты" назовут циклом
https://hashrocket.com/blog/posts/elixir-for-loops-go-beyond-comprehension
Это comprehensions, вот правильная ссылка: https://www.erlang.org/doc/system/list_comprehensions.html
Они принципиально отличаются от циклов возможностью фильтровать генераторы (которые могут, в свою очередь, быть бесконечными).
Так-то и рекурсию можно циклом обозвать.
В ленивых можно
Только через хаки, ну очевидно же, иначе — chicken-egg problem. Ленивый/неленивый тут ни при чем вообще.
data DoubleList a
= LeftEnd a (DoubleList a)
| Middle a (DoubleList a) (DoubleList a)
| RightEnd a (DoubleList a)
e1 = LeftEnd 1 e2
e2 = Middle 2 e1 e3
e3 = Middle 3 e2 e4
e4 = Middle 4 e3 e5
e5 = RightEnd 5 e4Пожалуйста
Тут мы встаём на зыбкую почву понимания семантики того, что именно хотел донести автор. Денотационно здесь описана конечная последовательность узлов с соседями справа и слева, но, насколько я ничего не понимаю в хаскеле, вряд ли она операционно откомпилируется в то, что принято называть реализацией структуры данных "двусвязный список", т.е. в ячейки с двумя указателями.
Это (Middle) будет именно ячейкой с двумя указателями.
Другое дело, что он будет очень жёстко иммутабельный: у вас не получится его поменять (даже добавить узел в начало или в конец) без пересоздания вообще всей структуры. По крайней мере, именно в таком виде (я не могу сходу придумать способ это обойти иммутабельным образом, но и не могу строго доказать, что его не существует).
Предположим противно, добавили с левого края => (тут будет лемма о сущестоввании самого левого одинакового элемента, пусть это e2 для определённости).
e1 <-> e2 <-> e3 ...
... (взмжно это ничего) e0' <-> e1' <-> e2 <-> e3 ....
=> left e2 == e1 && left e2 = e1' && (e1' != e1).
Что невозможно в чистых ф-иях.
То же самое "в середине" то же самое "справа".
Лень позволяет использовать объект до его полного определения. В хаскель-тусовке это называется tying the knot, и сводится не только к двусвязным спискам, но и, например, к деревьям, где у каждого узла есть и (указатель на) родитель, и дети.
Да, я знаю, но получится ведь статическая вещь в себе — с ней уже ничего дальше сделать нельзя будет. Я имел в виду полноценный список, который можно рекурсивно определить, например.
Этот список как раз рекурсивным типом и определен ;)
Это казуистика. Под «определить список» я имею в виду: в рантайме создать такой список, а потом создать еще один, в котором этот — хвост.
x = 0:y
y = 1:xПожалуйста
Скорее всего, я просто не понимаю, как реализуется Tying the knot, хотя еще вчера думал, что понимаю. За это в любом случае — спасибо.
Реализуется указателями на thunk'и. x = 0:y означает, упрощая, что в памяти создаётся cons-cell (которая сама по себе держит два указателя), где первый (head) указатель указывает на 0, а второй (tail) — на y. Аналогично y — это cons-cell, где первый указатель указывает на 1, а второй — на x. Так как : — ленивый конструктор, то вычислять его аргументы не нужно, поэтому всё работает.
Нормально же выходные тянулись, а теперь придется вспоминать, как работает отладчик.
Спасибо, я поковыряюсь. Теперь мне снова кажется, что я всё понимаю, но без отладчика я себе уже не очень верю.
Добавить в концепцию управления памятью не только владеющие (сильные) указатели, но и слабые (не владеющие) ссылки. Т.е. контролировать не просто "заимствование", т.е. переход владения, которое контролирует компилятор языка во время компиляции, но и реализовать механизм проверки валидности ссылки в рантайме.
Это есть в стандартной библиотеке языка: владение с подсчётом ссылок, слабые ссылки (Rc, Arc, Weak). Но на этих механизмах связный список будет проигрывать реализации на C, где используются обычные указатели и не тратится время на инкремент и декремент счётчиков, в этом и состоит проблема создания связного списка в Rust - связный список имеет легкопроверяемый алгоритм, но язык, опираясь на более ограниченную концепцию владения, не позволяет его использовать. На деле, однако, связные списки не стали проблемой для Rust, т.к встречаются очень редко и замена их на обычный вектор оказывается производительнее.
Да вопрос вообще не списках.
Сперва мне было интересно выяснить источник утверждения о безопасной работе с памятью на основе концепции владения и заимствования, а выяснилось, что с её помощью нельзя написать классическую реализацию списка. Но раз списки есть, причем в классическом (не безопасном) варианте реализации, то это означает, что рекламируемый как безопасный язык изначально использует не безопасные методы разработки.
И чем тогда этот подход отличается от стандартного на C или C++, если там тоже есть все для "безопасной" работы с памятью, а все проблемы вылезают тогда, когда они не используются?
все проблемы вылезают тогда, когда они не используются.
Вопрос в дефолтах. Разница в том, что в расте проблемы нет, до тех пор пока пользователь явно не начнёт использовать unsafe.
Но основная фишка боровинга в том, что он позволяет выразить безопасный контракт. То, что внутри будет unsafe - не шибко важно. Важно, что в публичный интерфейс будет безопасным - как бы им не пользовались, проблем с памятью не будет.
Примечание: получился длинный комментарий (оценил когда написал). Кратко: не нужен вам список (ну или не нужен rust).
Итак:
Такой подход ( безопасный язык изначально использует не безопасные методы разработки ) присущ, наверное, всем топовым языкам со сборщиком мусора: сборщик сам хранит указатели на память, но счётчик при этом не инкрементирует. И освободить может эту память, хотя пользовательская программа этого сделать не может. Вот всё то же самое.
А вся разница в том, что в условном питоне тебя не пустят на уровень сборщика мусора: барахтайся в своей песочнице и будь счастлив. Плата за такую безопасность в песочнице: замедление работы или ограничение по языковым конструкциям.
Для примера: вот вы в статье прошлись по двусвязному списку и вскользь упомянули односвязный, что наверное также нельзя сделать. Однако, (по видимому!, это теоретические рассуждения!, не пробовал!) конструкциями языка односвязный список реализовать можно: только при любом действии список фактически блокируется (всё отдаётся в мутабельную ссылку), все элементы становятся мутабельными (начиная с головы, видимо игры со ссылками), потом делается требуемая операция (например, выделение/удаление/изменение 5-го элемента (или элемента с нужным идентификатором)), потом можно опять превратить всё в readonly (если требуется множественный доступ). Т.е. по любому "пуку" делаем массу действий, но зато это как-бы безопасно. Нужен ли кому-нибудь такой список? Боюсь, что нет. Но сделать как-бы можно! А вот если нужно чтобы и сделать и быстро? Тогда переходим ...
"Небезопасные" языки программирования, с другой стороны, позволяют всё сделать быстро, опуститься на уровень сборщика мусора, поделать много интересных вещей (создать свою кучу, своё управление памятью и т.д.). Но нужно очень аккуратно всё делать. Например, использовать только допустимые контейнеры - умные указатели - всё обмазывать синхронизацией. Ну или изучать матчасть (параллельное программирование и т.д.).
Везде своя засада.
Поэтому может Вам не нужны двусвязные/односвязные списки? Ну зачем они вам? Или используем те, что выданы (написаны с применением небезопасных конструкций или др.).
А вот если нужно чтобы и сделать и быстро?
Тогда пишите на JS.
А, вы имели в виду рантайм-поведение? Тогда почему (компилтайм-)блокирование, (компилтайм-)локи для вас влияют на что-то в рантайме?
Я уж не говорю о том, что более ограниченная семантика языка помогает компилятору оптимизировать код.
Ну или изучать матчасть (параллельное программирование и т.д.).
Жаль, что матчасть никто выучить не способен. Вон, из недавнего:
В загрузчике GRUB2 выявлена 21 уязвимость
Выявленные уязвимости:
CVE-2024-45774: запись за границу буфера при разборе специально оформленных JPEG-изображений.
CVE-2024-45776, CVE-2024-45777: целочисленные переполнения при чтении специально оформленных mo-файлов, приводящие к записи за пределы буфера.
CVE-2024-45778, CVE-2024-45779: целочисленные переполнения при работе с повреждённой файловой системой BFS, приводящие к переполнению буфера.
CVE-2024-45780: целочисленное переполнение при обработке специально оформленных tar-архивов, приводящее к записи за пределы буфера.
CVE-2024-45781, CVE-2025-0677: переполнения буфера при работе с повреждённой файловой системой UFS.
CVE-2024-45782, CVE-2025-1125: переполнения буфера при монтировании специально оформленного раздела HFS.
CVE-2025-0622: обращение к памяти после её освобождения при манипуляциях с модулями, может привести к выполнению кода атакующего.
CVE-2025-0624: переполнение буфера при сетевой загрузке.
CVE-2025-0678: переполнения буфера при работе с повреждённой файловой системой Squash4.
CVE-2025-0684: переполнения буфера при манипуляциях с символическими ссылками в ФС Reiserfs.
CVE-2025-0685: переполнения буфера при манипуляциях с символическими ссылками в ФС JFS.
CVE-2025-0685: переполнения буфера при манипуляциях с символическими ссылками в ФС ROMFS.
CVE-2025-0689: переполнения буфера при работе со специально модифицированным разделом UDF.
CVE-2025-0690: переполнения буфера при получении специально оформленных данных с клавиатуры.
CVE-2025-1118: обход режима изоляции Lockdown и извлечение произвольного содержимого памяти через выполнение команды dump.
CVE-2024-45775: отсутствие проверки кода ошибки при выделении памяти при разборе переданных аргументов может привести к повреждению данных IVT (Interrupt Vector Table).
CVE-2024-45783: доступ по нулевому указателю при монтировании некорректной ФС HFS+.
Всё как всегда. Всё как мы любим в сишке. И это всё в
15:30:18 деанон@деанон ~/Programming/tmp/grub (master) % cloc . | head
github.com/AlDanial/cloc v 2.00 T=0.62 s (2549.4 files/s, 737694.3 lines/s)
---------------------------------------------------------------------------------------
Language files blank comment code
---------------------------------------------------------------------------------------
C 843 42453 32782 245992
C/C++ Header 494 8234 16649 40293
Text 7 20 0 24738
за год на менее чем 300к строк кода — по промышленным меркам милипусечный проект.
Какое параллельное программирование? Массивы и их индексацию бы освоить.
И чем тогда этот подход отличается от стандартного на C или C++, если там тоже есть все для "безопасной" работы с памятью, а все проблемы вылезают тогда, когда они не используются?
Это стандартная библиотека языка, она вся состоит из небезопасного кода, так как предоставляет безопасные интерфейсы для вызова системных функций, заменяет банальные операции типа сложения на интринсики компилятора типа intrinsics::add_with_overflow, реализует аллокатор и ещё много чего, что я не понимаю. Без этой части язык не построить.
Пользовательский код уже имеет гораздо меньше блоков unsafe, и каждый из них привлекает внимание. Помню скандал с actix-web, где разработчик так любил unsafe, что его прогнали.
Не знаю как обстоит дело в C++, но подозреваю, что там наоборот, написание небезопасного кода легче, чем безопасного. То есть, когда вы говорите что в C++ нужно специально пользоваться какими-то безопасными методами обращения с памятью, то в Rust нужно специально воспользоваться НЕ-безопасными методами работы с памятью, если этого сильно захочется.
Время на инкремент и декремент счётчиков либо расходуется пренебрежимо мало, либо не расходуется вовсе (так как узким местом в современных компьютерах является сам доступ в память к узлу, а не операция инкремента). Поэтому ссылаться на неэффективность счётчика ссылок как на обоснование каких-то содержательных решений некорректно.
Другое дело, что счётчик ссылок сам по себе не является очень уж хорошим алгоритмом сбора мусора, но уж хотя бы так.
Напомню, что для инкремента/декремента счетчиков тоже требуется чтение и запись в память, что тоже не бесплатно. Более того, в условиях многопоточности эти доступы должны быть еще и atomic
Основная проблема - в многопоточном доступе. Нужно синхронизировать значение счётчика ссылок между кешами всех ядер процессора.
Худший пример, который я могу придумать - это какой-то многопоточный расчёт. Поток обращается к общему для всех потоков справочнику (который по идее, read/only), но результат забирает себе "во владение" в shared_ptr. В исходнике выглядит всё относительно безобидно,
std::shared_ptr<Item> getItemFromSharedCache(int key);
а накладные расходы на перегонку счётчика между ядрами будут сотни тактов на каждое обращение.
Это действительно плохой пример, так как std::shared_ptr не предназначен для работы в нескольких потоках из-за гонок данных:
И поэтому на C++ невозможно написать "локально безопасное" решение, и в то же время оптимальное.
Т.е. решение может быть безопасным глобально, если мы возвращаем сырые указатели, но вручную следим, чтобы время жизни справочника было больше, чем время жизни потоков расчёта.
В вашем же подходе я вижу принцип "у меня в руках молоток, а везде вокруг гвозди" - чтобы гарантированно избежать утечки памяти, вы согласны возвращать shared_ptr в таком сценарии.
std::shared_ptr не предназначен для работы в нескольких потоках
Ваше замечание немного о другом - оно справедливо, если один и тот же shared_ptr разделяется между потоками. У меня в примере у каждого потока свой экземпляр shared_ptr.
Поток обращается к общему для всех потоков справочнику (который по идее, read/only), но результат забирает себе "во владение" в shared_ptr.
Если я правильно вас понял, то у вас именно один shared_ptr на несколько потоков, а не на каждый поток по shared_ptr
Функция, которая возвращает элемент из кеша, отдаёт не ссылку на shared_ptr, а экземпляр, каждый раз новый
std::shared_ptr<Item> getItemFromSharedCache(int key);
Что внутри этой функции - другой вопрос.
Ну а разделять экземпляр shared_ptr между потоками (например, передавая его по ссылке) бессмысленно - это полностью убивает идею подсчёта ссылок и не гарантирует безопасный доступ.
Счётчик обычно является частью значения того объекта, который он защищает. Как правило, другие поля объекта всё равно используются рядом с организаций ссылок на него.
А в чём, собственно, предложение?
Добавить в концепцию управления памятью не только владеющие (сильные) указатели, но и слабые (не владеющие) ссылки
Так есть же std::rc, std::rc::Weak.
Тащить это в ядро языка rust? Встретит такое же сопротивление, как попытка перетащить std::vector и std::map из стандартной библиотеки в ядро языка C++
Вообще то std::vector и std::map, это реализации контейнеров и было бы правильнее сравнивать не с ними, а с какими нибудь типами ссылок, например, std::shared_ptr, std::weak_ptr и std::unique_ptr.
Проблема только в том, что в основе С++ лежит адресная арифметика, которая не имеет контекста в рамках компилятора и является обычными числами, а не классами. И если предложить заменить адресацию на конкретные классы ссылок, то это будет уже не С++, тогда как в Rust изначально было несколько типов указателей.
Мой посыл в том, что при желании всем этим уже можно пользоваться в rust (а платить за это производительностью). Или не пользоваться, если в каком-то частном случае можно положиться на проверку владения в compile-time.
правильнее сравнивать не с ними, а с какими нибудь типами ссылок, например, std::shared_ptr
Ну хорошо, адепты C++ также не захотят тащить shared_ptr в ядро языка, если он уже прекрасно существует в std.
И если предложить заменить адресацию на конкретные классы ссылок, то это будет уже не C++
А если в rust добавить, то по той же логике это уже будет не rust? Или в чём принципиальная разница.
Некоторое время назад я попробовал найти формальное доказательство безопасной работы с памятью, которое реализовано в Rust, но так и не смог его найти
Мне интересно, что же в итоге автор нашёл приближенное по теме? Попадались ли такие имена как Хоар, Мацакис, Юнг, Гроссман?
Много какие попадались и самое близкое по теме, что находил, вот это.
Судя по разделу Conclusion, вывод примерно такой, что, если выкинуть из Раста то, что отличает его от функционального языка, то остальное можно описать в формальной семантике :)
CPS-трансформация особенно душевно зашла.
Вы 'stacked borrow' находили? И весь rust-belt https://plv.mpi-sws.org/rustbelt/ смотрели? Я упоминаний в статье не нашел, что для подобных утверждений слишком помпезно.
Спасибо за ссылку, там действительно много информации для изучения, но с ходу непонятно, что я там должен был найти?
Ссылка, если я правильно понял, это реклама (приглашение) освоить бюджет, выделенный для написания различных работ по доказательству корректной реализации стандартной библиотеки Rust, так как она сделана с использованием не безопасных фрагментов кода, поэтому нужно как-то обосновать возможность её применения в Rust.
Что же касается статей stacked borrow и Stacked Borrows: An Aliasing Model For Rust, то они касаются попытки доказательства корректной реализации анализа в компиляторе, но не самой исходной модели. Да и сами доказательства так и не закончены и имеют некоторые некорректности и ограничения.
Stacked borrow - про корректность модели исполнения, а не конкретную реализацию. Для того, чтобы аргументировать корректность, даже неформально, сначала нужно определить предмет аргументации.
Aliasing - это основной отличительный момент семантики Rust, и поскольку утверждение про 'safety' сводится к тому, что правила владения искореняют некоторые типы ошибок, то собственно aliasing/borrowing и становится предметом (полу)формального определения и исследования.
Я сомневаюсь в том, что кто-то будет вручную доказывать правильность кода rustc. Хотя вот 'доказанный' компилятор C существует, и для rustc есть ferrocene.
Так в Раст есть общеизвестные дыры в системе типов, которые позволяют менять время жизни на произвольное. Так что никакого доказательства в принципе не может быть.
Вы про баги в компиляторе?
Вот, например, issue с 2015-го года висит. Пока не исправили. Обещают починить с новым trait solver'ом.
Неприятная история, конечно, но это именно баг в реализации, а не "дыра в системе типов".
Ничего не мешает доказать корректность абстрактной модели, в которой бага нет. Если мы в ходе доказательства найдём противоречия в этой модели — можно будет говорить о дырах в ней.
Как привести реальный компилятор в соответствие с теоретической моделью — уже отдельный вопрос.
О формальном доказательстве безопасной работы с памятью на основе «владения и заимствования»