Zero cost

Rust без аллокатора: `fff` снизил пиковое потребление памяти через `mmap`

Во время тестирования fff обнаружилось, что при создании большого Vec<u64> процесс потребляет заметно больше оперативной памяти, чем требуется для индекса.

Причиной оказался аллокатор, который мог резервировать лишнюю память при работе с крупными буферами.

Теперь на Unix-системах fff выделяет память напрямую через mmap:

* рассчитывает точный объём памяти
* округляет его до размера системной страницы
* создаёт приватное анонимное отображение
* работает с данными через *mut u64
* освобождает память вызовом munmap

На остальных платформах по-прежнему используется обычный Vec<u64>.

В результате fff запрашивает у ядра ровно столько страниц, сколько необходимо для хранения и обработки индекса.

🦀 Как доказать, что Rust-код работает правильно: Amazon рассказывает о Verus

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

Разработчик описывает прямо в исходниках:

* requires - условия перед выполнением функции.
* ensures — свойства результата.
* Инварианты циклов и вспомогательные доказательства.

Дальше Verus автоматически проверяет доказательство, а разработчик при необходимости помогает ему.

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

Нужно добавить второе требование: если вернулся `None`, искомого элемента действительно нет в массиве.

Amazon уже использует Verus для проверки ключевых примитивов Nitro Isolation Engine, отвечающего за изоляцию виртуальных машин. Инструмент также позволяет доказывать свойства конкурентного кода и безопасность поддерживаемых конструкций unsafe.

Гарантии относятся к заданной спецификации и принятым допущениям: полнота самих требований остаётся ответственностью разработчика.

📖 https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

#Rust #Разработка #FormalVerification

🦀 Qt открывает Rust полноценный путь к кроссплатформенному UI

Qt представила Qt Bridge for Rust = слой, который позволяет писать логику приложения на Rust и напрямую подключать её к Qt Quick/QML без ручного FFI и C++-кода в проекте.

Что это даёт:

- Rust для application logic;
- QML для интерфейса;
- hardware acceleration;
- Linux, macOS и Windows;
- безопасный Rust API;
- интеграцию через привычные struct, traits и attribute macros.

Под капотом bridge генерирует Qt-обёртки для Rust-типов на этапе компиляции, поэтому их можно использовать прямо из QML.

Сейчас Rust Bridge находится в public beta. Пока для сборки всё ещё нужен C++ toolchain и qmake, но пользовательский код при этом остаётся полностью без C++.

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

Статья: https://www.qt.io/blog/rust-ui-framework-via-bridging-technology