Обновить

Комментарии 34

Кстти еще существует такая штука как unsafe{}. Она отключает всю безопасность и позволяет управлять памятью как тебе угодно. 

Это не вполне корректное утверждение.unsafe{} ничего не отключает а скорей наоборот включает внутри области возможность работать с небезопасными операциями: разыменование сырого указателя, вызов небезопасных функций, модификация статической переменной, доступ к полям union. Безопасность работает так же как и прежде, просто внутри области видимости программист берет на себя отвественность за возможное возникновение неопределенного поведения для вышеуказанных операций.

Спасибо за уточнение

"Безопасность работает так же как и прежде" - как безопасность может работать как и прежде, если можно свободно обращаться по любым указателям без никаких проверок, а доступ к полям union это самый настоящий reinterpret_cast? Поясните пожалуйста.

"Безопасность работает так же как и прежде" - как безопасность может работать как и прежде, если можно свободно обращаться по любым указателям без никаких проверок, а доступ к полям union это самый настоящий reinterpret_cast? Поясните пожалуйста.

Я имел ввиду что никакие существующие правила и проверки не отключаются а работают также как и прежде и unsafe к примеру не позволяет брать несколько мутабельных ссылок, но разумеется работа с сырыми указателями в области unsafe может привести к UB.

std::string_view get_name() {
    std::string s = "John";
    return s;  // неявное преобразование string -> string_view
}
int main() {
    auto name = get_name();
    std::cout << name;  // UB, крэш или мусор
}

И

// Rust - не скомпилируется
fn get_name() -> &str {
    let s = String::from("John");
    &s  // error: cannot return reference to local variable
}

https://stackoverflow.com/questions/63166194/implicitly-convert-string-to-string-view

Жесть вообще

но при этом если заменить string_view на string& код ровно по такой же причине не скомпилируется ( или выкинет warning который лего сделать ошибкой)

Можно и посложнее пример придумать, где просто не заметишь. Вопрос то принципиальный

https://godbolt.org/z/xxb549TEM у меня так вышло суть в том что лайф тайм внутри функции, кончится когда скобочка закончилась поэтому и будет уб, чтобы лайфтайм был определен он должен быть в зоне видимости, тоесть чтобы не было уб надо передать в функцию что пишем и куда пишем, или в функции создаётся что-то и пишется туда куда указано, дело в том что string_view создаёт еффективное представление на строку (ну чтобы не было копирования данных пишут что еффективно) и при выходе при создании внутри функции, лайфтайм строки! кончится и поэтому там будет пусто вобщем, поэтому надо позаботиться о том чтобы строка! была в области видимости как я понял

Вам там в комментариях много полезного написали, но кажется не в коня корм.

Ага, много слов и никакой конкретики по заданным вопросам. Так же как и ваш комментарий.

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

А вот в этом комментарии и нижележащей ветке вам привели ссылки на доказательства корректности модели памяти Rust. Но не доказательства корректности её реализации в компиляторе.

Может быть вы тогда обратите внимание и на ответы к упомянутым вами комментариям?

Конечно. Например я обратил внимание, что вы даже не перешли по ссылке оппонента. В ней 11-я статья от 2020 года описывает то, что вам нужно. А вы привели две статьи 2018 года, конечно в них всё было в зачаточном состоянии.

Конечно, я не туда посмотрел или не так понял.

Может быть тогда вы напишите ту самую правильную ссылку с описанием доказательства математической корректности модели управления памятью или на худой конец список проверок и/или ограничений, которые сделаны в компиляторе Rust для её реализации?

И вы еще раз подтвердили, что не переходите по ссылкам. Еще раз дублирую:

11-я статья от 2020 года описывает то, что вам нужно

Вы издеваетесь? Мне хочется найти

описанием доказательства математической корректности модели управления памятью или на худой конец список проверок и/или ограничений, которые сделаны в компиляторе Rust для её реализации

А вы мне опять подсовываете частный случай оптимизации при доступе к памяти:

We give formal proofs (mechanized in Coq) showing that this rules out enough programs to enable optimizations that reorder memory accesses around unknown code and function calls, based solely on intraprocedural reasoning.

Прямо над вашей цитатой написано следующее:

In this work, we propose Stacked Borrows, an operational semantics for memory accesses in Rust. Stacked Borrows defines an aliasing discipline and declares programs violating it to have undefined behavior, meaning the compiler does not have to consider such programs when performing optimizations.

А под ней:

We also implemented this operational model in an interpreter for Rust and ran large parts of the Rust standard library test suite in the interpreter to validate that the model permits enough real-world unsafe Rust code.

А в самой статье описана реализация интерпретатора Miri, который проверяет код std на соответствие модели Stacked Borrows:

We implemented Stacked Borrows in Miri to be able to test existing bodies of unsafe Rust code and make sure the model we propose is not completely in contradiction with how real Rust code gets written. Moreover, this also served to test a large body of safe code (including code that relies on non-lexical lifetimes), empirically verifying that Stacked Borrows is indeed a dynamic version of the borrow checker and accepts strictly more code than its static counterpart.

Так что либо вы сами издеваетесь, либо мы по разному понимаем термин Aliasing Model.

P.S. Чисто ради интереса, минусы тоже вы лепите?

Причем тут Aliasing Model и цитаты из вашей ссылки?

Я задаю вопросы про базовую концепцию Rust, основанную на единственности владельца, а вы мне приводите работы по натяжению совы на глобус доказательству её частичной корректности в некоторых случаях.

Это не проблема Раста, это проблема самой концепции единственного владельца. У неё есть ограничения в виде невозможно выразить не ориентированные и циклические графы.

Ну штош, зато в 95 процентах случаем она работает и улучшает жизнь.

А если прикинуть немного, то для циклических структур не уверен, что вообще возможно формальное доказательство корректности. По циклам же можно бесконечно скакать.

По правде, это не "проблема", а "ограничение" данной концепции. Так будет правильнее, чтобы не создавать негативную коннотацию при использовании штампа "проблема".

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

По хорошему, и это тоже не стоит называть "проблемой". Просто нужно иметь ввиду, что у каждого языка программирвания есть ограничения и не стараться использовать PHP или JavaScript во встраиваемых решениях для микроконтроллеров или, как в данном случае, просто нужно помнить, что в Раст статическая проверка "владения и заимствования" не работает для циклических графов. Только рантайм, аналогичный реализованному в С++ :-)

Ссылка на диссертацию в которой рассматриваются две модели:

RustBelt is a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. The model is designed to verify the safety of a number of intricate APIs from the Rust standard library, despite the fact that the implementations of these APIs use unsafe language features.

Доказательство корректной реализации небезопасными методами некоторых функций стандартной библиотеки Rust, и

Stacked Borrows is a proposed extension of the Rust specification, which enables the compiler to use the strong aliasing information in Rust’s types to better analyze and optimize the code it is compiling. The adequacy of this specification is evaluated not only formally, but also by running real Rust code in an instrumented version of Rust’s Miri interpreter that implements the Stacked Borrows semantics.

Рассмотрение частного случая оптимизации компилятора при доступе к памяти.

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

Еще ни разу не видел ни одной статьи, которая рассказывает, как ссылочная модель Раста строит иерархии объектов в хипе. Как предотвращаются утечки памяти и дедлоки, как гарантируется иммутабельность шареных объектов. Я тут попытался реализовать на Расте вот этот бенчмарк DOM-структур данных, и пока застрял на невозможности иметь одновременно объект с единственным владельцем, на который можно ссылаться weak-указателями из других объектов. Кроме того для двухпроходной операции копирования с сохранением топологии графа мне нужен map(оригинальный объект->копия). И указатели в этой мапе должны потом присваиваться типизированным указателям - Weak<RefCell<Card>> и Weak<RefCell<dyn CardItem>> . Хотя я даже не уверен, что мне нужны именно эти указатели. Не мобли бы вы подсказать, как в Расте реализуются структуры данных в хипе. Не обязательно в комментарии. Это могло бы стать хорошей темой для отдельной статьи.

И правда интересная идея для статьи, но пока что я сам не смотрел как реализуется иерархия объектов в куче. В ближайшее время поищу и постараюсь ответить

концепция BVH(Bounding_volume_hierarchy) ищите в инете описания, но если найдёте про аабб - представляйте флай обжект тоесть коробку в которой данные, на вашем сленге Trait<T> чото такое или Box или просто структура с метаданными или та структура которая определяет связь или выборку

можно реализовать как дерево индексов, но у вас нету рейкаста, возможно надо будет подумать как выбирать иерархии или боксы

тоесть у вас владельцы в последовательности, в DOM индексация для ускорения(тут как раз не владельцы а указатели)

в теории ссылочная модель раста такая же как в С++, вам просто нужна последовательность и алгоритм по которому вы сортируете обьекты из последовательности(критерий при вставке из последовательности, чтобы дерево было еффективно)

Скрытый текст
struct Object3D
{
  glm::vec3 position;
  glm::vec3 prevpos;
  glm::vec3 velocity;
  float spped;
  glm::vec3 size;   // cube
  glm::vec3 radius; // sphere
  bool isSphere;
  bool collided = false; // visualisation
  bool stayObj = false;
  glm::vec3 NormalWall; //(1, 0, 0)
  std::string name;
};//типо флай обджекта наверно данные для рендера в другом месте

...
struct BVHNode
{
    AABB box;
    BVHNode *left = nullptr;
    BVHNode *right = nullptr;
    std::vector<Object3D *> objects; // листовой узел
    bool isLeaf() const { return !objects.empty(); }
    ~BVHNode()
    {
        delete left;
        delete right;
    }
};

BVHNode *buildBVH(std::vector<Object3D *> &objs, int depth = 0);
...
BVHNode *bvhRoot;
std::vector<Object3D> objects;//реальные обьекты
...
    glm::vec3 v = glm::vec3{0, 0, 0};
    createOneBigCubeCoords(objects, v);//спрятана генерация обьектов просто

    std::vector<Object3D *> objPtrs;//я себе это как индексация представляю
    for (auto &o : objects)
        objPtrs.push_back(&o);
    bvhRoot = buildBVH(objPtrs);//будет обход по механизму дерева уже всё тех же обьектов
...
но это дерево пока еще для коллизий, в теории так же можно сделать и для рендера

утечек не было покачто

Насколько знаю, никак, модель ссылок работает с иерархической областью видимости (scope). Когда используются графы или циклические зависимостм, применяют индексы и указатели. Остальное гарантируется системой типов. Если захотите неправильно их использовать, у вас это получиться.

Кстати еще существует такая штука как unsafe{}. Она отключает всю безопасность

Не отключает.

и позволяет управлять памятью как тебе угодно.

Не позволяет.

Rust имеет LLVM компилятор, то есть исходники на rust превращаются в промежуточный MIR который мы можем поглядеть точно также как и выше посмотрели ассемблер

Вы перепутали LLVM IR и MIR.

В общем, на мой взгляд система заслуживает внимания но это определенно не панацея.

Есть ощущение что перед выводом пропущен огромный кусок текста из которого сделан этот вывод

Rust не замена плюсам, скорее аналог. У каждого свои плюсы.

Замена.

Также хотел бы попросить о обратной связи. Я не сильно опытен в написании статей, так что это важно.

Не очень понятно зачем на хабре перепечатка первой главы растбука который уже есть на русском.

Часть про описание ассемблера может написать любая ЛЛМ.

Так что не очень понятно в чем ценность. Написать на хабре что плюсы точно-точно живы? Увы нет, они мертвы.

Статья понравилась, разбор на низком уровне смысла того, о чём люди спорят, не вникая в подробности и не читая asm, лучше всего такие споры разрешает. Хочется видеть больше разборов, как реализуется безопасность чего-то и какой ценой, какие бывают другие варианты сделать то же.

Однако поправил бы, что unsafe не снимает все проверки безопасности. Код внутри блока unsafe компилируется по почти всем тем же правилам, разрешается очень немногое дополнительно: адресная арифметика, разыменование сырых указателей, небезопасная работа с union, ffi, потоконебезопасность, послабления на mut&, передачу аргументов с гонкой данных и ещё там пара штуковин. Есть явный исчерпывающий список, что становится можно, это не всё подряд.

Как-то тема borrow checker так и осталась нетронутой. Думал щас про SAT или хотя бы расскраску памяти как в Asan/Lsan расскажут .

Надо бы, мне самому как через пару дней перечитал статью она показалось незаконченной. Думаю сильнее раскрыть эту тему

Зарегистрируйтесь на Хабре, чтобы оставить комментарий

Публикации