далее, про модель выполнения.

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

система типов это атрибуты, метаинформация типов или значений данных. например ’Range, ’Length или ’Access для указателей (по сути все указатели типизированы, есть предварительная оценка корректности доступности указателей с учётом вложенных областей видимости, приватных данных пакета, дочерних пакетов).

дженерики и дочерние пакеты. по умолчанию даже стандартный Ada.Text_IO.Put полиморфный, то есть использует дженерики (полиморфизм времени выполнения). мог бы использовать и вложенные дочерние пакеты (и полиморфизм времени компиляции).

в общем, задача достаточно умного компилятора Ады выглядит так:

1. определить количество различных асинхронных задач, критических секций и разделяемых данных (protected type), объединяющих задачи.

2. используя preelaborate определить зависимости, возможно циклические между модулями (пакетами) и корректную последовательность их инициализации (elaborate)

3. поскольку единого main нет (см. хелловорд) его нужно сэмулировать. в такой сэмулированной процедуре (типа _tmain в WinAPI) последовательно будут adainit();…;adafinal() – инициализация и деинициализация рантайма; создание нужных задач в нужной последовательности и секций их синхронизации; создание и инициализация системы исключений (поверх задач); объектной системы; пулов памяти, контролируемого/неконтролируемого(ручного) выделения памяти.

4. рантаймы настраиваемы. например, если не нравится простой встроенный, ключиком –with-RTS=zfp-profile можно подключить «заглушку» Zero Footprint Profile, без стека исключений (типа паники), без сложных атрибутов, динамической диспетчеризации ’Class и прочего.

например, если стандартный GNU GNAT RTL состоит из 2х частей: GNULL платформнонезависимого и GNARL POSIX-платформноспецифичного, включает всё это богатство, и helloworld статически собранный получается на 1.2Мб (с debug, на 300 кб после strip). здесь в этот RTL входит то самое libgnat (3 Мб0, libgcc и прочее. семантически, в эти 300 кб входят полноценные исключения, задачи, protected type, атрибуты, объектная система, дженерики.

если взять примеры из wikibook под сборку gprbuild и собрать их, можно получить динамическую линковку, практически сравнимую с С (c зависимостями от libgnat.. .so/.dll)

если взять другой профиль, например drake – можно получить статические бинарники на 40 ..60 кб. за счёт того, что упрощены метаданные типов – атрибуты, упрощены исключения (паника без размотки стека), нет завязки на дженерики и проч.

то есть, если выделить модель памяти в Ада – это:

1. раздельная компиляция, по пакетам, включая вложенные дочерние и видимость, параметризованные пакеты (дженерики) и метаданные типов (атрибуты).

2. пакетам принадлежат разделяемые данные (protected type) и задачи (task). задачи могут начинать выполняться и взаимодействовать в порядке, описанном в пакетах, т.е. произвольном.

3. достаточно умный компилятор при этом определяет сколько таких задач и во что их транслировать (POSIX pthreads в GNARL, зелёные нити в GNULL в каком-то embedded profile, например ravenscar).

4. другие элементы языка : объектная система, дженерики, исключения реализованы в рантайме. который может быть разный, настраиваемый.

5. в компайлтайме можно гарантировать выполнение каких-то контрактов (SPARK и ASIS). ASIS: стандартный интерфейс к AST+ семантическому дереву. можно реализовать нечто вроде плагинов к компилятору, гарантирующих статическим анализом что некая опасная конструкция фактически не используется. SPARK: отдельный язык, верифицирующий контракты вокруг ADA-программ. Ada2012: контракты, встроенные в язык. здесь есть pragma static assert.

как пример применения SPARK на AdaCore есть пример про статически верифицируемый тетрис.

6. прагмами можно отключить «опасное» подмножество языка, если верицифируемо доказано что эта фича не используется, в реальном коде.

ещё см. например встраиваемый профиль Ravenscar (с асинхронными задачами для систем реального времени). верифицируемо доказано через SPARK максимальное время выполнения рантайма, при этом там всё ещё есть задачи/исключения в каком-то простом виде. вроде и объектная система тоже есть.

если сравнивать с моделью памяти в Rust раз (habr.com) два (github.com) три (ibm.com) растономикон управление памятью sysdev1 sysdev2, то в Rust:

0. на базовом уровне (в отличие от модели памяти C machine) тоже есть несколько потоков управления, и паника вместо исключений, чтобы прекратить их все

1. есть семантика владения/одалживания значений, предназначенная для проверки доступности областей видимости без сборки мусора.

2. см. семантику копирования/перемещения в С++ и lock-free алгоритмы. грубо говоря, не нужно оборачивать protected type критическими секциями, процессами и механизмами синхронизации процессов типа рандеву и семафоров, если гарантированно известно, что а) владелец только один в каждый момент времени б) время жизни, владение/одалживание, изменение происходит согласованно – что компилятор и пытается гарантировать. «borrow» это по сути создание ссылки на объект, ссылка «одалживается» у владельца.

3. цель и задача – избавиться от UB в поведении memory model. поэтому переменные или ссылки могут быть mut или обычными неизменяемыми. алиасинг явно запрещён для изменяемых ссылок &mut, что позволяет проводить некоторые оптимизации. лайфтаймы или времена жизни это блок кода, в течение которого ссылка должна быть доступна (’a, ’static). лайфтаймы не обязаны совпадать с «областью видимости» scope в случае замыканий, продолжений и т.п. трюков.

модель памяти в Rust

4. Модель памяти отсюда:

Память любой rust-программы состоит из набора статических (static) элементов, из некоторого количества задач (tasks), каждая из которых обладает собственным локальным стеком (stack), и из общей памяти, так называемой «кучи» (heap). Неизменяемые области общей памяти могут совместно использоваться задачами, то есть, быть разделяемыми (shared). Изменяемые области общей памяти не могут быть совместно используемыми.

Память в стеке задачи выделяется в форме слотов (slots), а в общей памяти выделяемые фрагменты обозначаются, как boxes.

4.1 Распределение памяти и время существования

static items: CTFE функции, модули и типы, несколько задач

стек задачи: активные фреймы

heap: boxes через smart pointer, могут быть managed boxes через GC и owned boxes через ссылку на него только у 1 владельца. lifetime блока зависит от lifetime указателей на блок.

4.2 Общая концепция владения

Владелец управляет lifetime вызывая конструктор/деструктор, и определяя является ли объект изменяемым. владение рекурсивно, при выходе из области видимости объект уничтожается подобно RAII. контролируется дерево владения, трейт Owned позволяет пересылать такой объект между задачами.

4.3. Частная концепция владение памятью

любая задача владеет всей памятью, к которой она имеет безопасный доступ через локальные переменные, а также через управляемые (managed), собственные (owned) и заимствованные (borrowed) указатели

4.4. Слоты памяти

стек каждой задачи содержит слоты (slots), которые являются компонентами фрейма стека и представляют собой либо параметры функции, либо временные объекты, либо локальные переменные.

Локальные переменные, которые иногда обозначают термином «элемент локального стека» (stack-local allocation), содержат собственно значение, размещённое в области памяти стека. Очевидно, что это значение является составной частью фрейма стека. Локальные переменные и параметры функций по умолчанию неизменяемы. Ключевое слово mut, явно указанное при объявлении, предоставляет возможность изменения переменных и параметров. Несмотря на то, что при размещении в стеке локальные переменные не инициализируются, их использование становится возможным только после явной инициализации, за этим строго следит компилятор.

5. дженерики

через трейты

6. объектная система

через трейты

7. исключения

есть паника. Option монады и АлгТД вместо исключений.

для сравнения, микроядро L4

в микроядре L4 есть Grant/Revoke/mmap — системные вызовы (чуть ли не единственные, из кроме IPC, которых состоит микроядро).

вся память принадлежит процессу задаче системному процессу sigma0, от этого владельца нарезается в подзадачи. полномочия capabilites при этом наследуются похоже на лайфтаймы раста.

Есть ли специальный компилятор rust для работы с ядром L4 ?

Навскидку в двойку

нет, к тому же L4 и потомки реализованы на С++. но умозрительно, модель памяти Rust хорошо ложится на модель памяти L4.

спасибо, через log(2,1000)-1~=9 лет напиши как будет готов.

SeL4 реализовано на чистом Си. Кресты обладают слишком сложной семантикой, чтобы можно было доказать отсутствие косяков в ядре.

Как-то так, да.

Nix, конечно.

Нативные ПМ арча и макоси научились в воспроизводимую сборку? Кросскомпиляцию? Хотя бы запускаться друг на друге? А Nix научился.

но может быть, его можно доказать на SPARK?

или написать на аде рантайм, который статическим анализом через ASIS (и/или, SPARK) выполняет borrow checking, и далее реализует модель памяти раста?

на аде, ога. то есть: добавить каких-то ещё атрибутов в типы (типа как ’Access и pointer.all для указателей => добавить pointer.borrowed и прочее с лайфтаймами; компилировать такое вот в особенный рантайм с особенными процессами с особенными SPARK-верифицируемыми контрактами)

надо посмотреть исходники ОС на Аде (и/или, совмещённые с си): RTEMS, MarteOS unixforum оффсайт гамезы

если на том же L4 или Haiku ядро написано на С++ и включает рантайм плюсцов, здесь по идее должно включать рантайм ады какое-то подмножество, и простые программы не должны зависеть ни от чего кроме ядра (то есть libgnat вкомпилирован в ядро MarteOS).

и/или, задавать им разные рантаймы. одно в стиле POSIX, другое в стиле L4, третье в стиле раст-рантайма.

и в итоге изобразить раст адой с особенным рантаймом/контрактами на Ада2012/SPARK верифицируемым куском кода.

И как пользователь arch-а, fedora silverblue (это которая на основе ostree построена) или osx смогут собрать продукт с помощью nix?

Typed assembler language

Coq: The world’s best macro assembler?

Coq: The world’s best macro assembler?

Ого! Я правильно понял, на Coq можно программировать на уровне ассемблера и при этом иметь верифицируемую семантику вплоть до высокого уровня? Выглядит офигенно.

Взяв и запустив на них Nix, блин.

Я вон его вообще на андроиде запустил.

На SPARK в AdaCore cделали tcp-ip-стек, вроде с доказанной корректностью.

Думаю, что для микроядра можно сделать почти то же самое, но полностью пруфануть соответствие микроядра спецификации на SPARK ПМCМ не представляется возможным, ибо там есть ансейф полюбому.

Гоню! Можно написать на спарке эмулятор целевой платформы (ВМ), сделать «микроядро» «внешним» по отношению к памяти, пруфануть коррестность.

Потом можно написать ассемблерные вставки, перенести ядро внутрь ВМ, и доказать бинарную совместимость.

Сдается мне, что это будет быстрее, чем то, что сделали в команде SeL4

Команда разработчиков SeL4 для этого написали «микроядро» на Хаскеле, а потом написали микроядро на Си и пруфанули их полную бинарную совместимость в смысле работы с памятью.

Бугуртос тебе ниже правильную ссылку дал ( http://www.ada-auth.org/standards/12rm/html/RM-C-6.html#p15 ) - в аде тоже есть примитивное ограничение гонок. Правда, оно таки слишком примитивное, и уже две ячейки атомарно средствами языка ты не сможешь изменить ни в аде, ни в расте.

книги по Ада >> pdf версия статей Gem на русском от mediascan.by

GNATCOLL.Atomic, GNATCOL.Weakref и прочее