?

Log in

No account? Create an account
Верифицированный лигаси-фри стек в пару рыл за 20 лет - Дважды мудак [entries|archive|friends|userinfo]
Декларативное рулит

Site Meter

[ website | Мой сайт ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Верифицированный лигаси-фри стек в пару рыл за 20 лет [дек. 2, 2017|22:11 pm]
Andy Melnikov
[Tags|, , ]

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

Итак, смотрим что можно сделать относительно реалистичного.

POSIX-говно выбросить проще простого - роль BIOS играют коммерческие гипервизоры, которые со временем верифицируются, особенно Type 1 типа Hyper-V, ESXi и Xen; роль libc - интерфейс гиперколлов. В KVM virtio, впрочем, гиперколлов нет, а паравиртуализированные устройства - это обычные PCI-устройства, просто с менее дебильным интерфейсом. Минимально нужен APIC, Baloon, PCI (configuration space etc) и сеть. Процессы, полноценный IP-стек и юзермод не нужны - пусть будет 1 поток per VM c одним "raw сокетом", на таком "node.rs for DOS" можно налепить юзермод-TCP и остальные ф-ции получать через p9-образный протокол от сервера на Linux-виртуалке, играющего роль микроядра.

Далее нам надо какой-то рантайм, который не требует реализации позикс-говна. Как ни странно, таких рантаймов 3 - это Си, С++ и rust. Си нам понадобится в хардкорных местах, в-основном же хватит Rust LibCore.

Если мы берём Rust - то есть достаточно прямолинейный вариант с RumpRun Rust. Это Rust unikernel на основе кодобазы netbsd, позволяющий запускать "полный" Rust std (даже не core). Дальше есть хардкорные (aka нерабочие) кодобазы rustboot и robigalia, из которых можно слепить "совершенно пустой юникернел" (т.е. без netbsd-кода) с памятью, APIC и PCI, и заняться портированием virtio на раст (дабы не было соблазна делать всё юникс-вэй можно взять нейтральный сюжет, рекомендованный детям дошкольного возраста - виндовые дрова). Понятно что хороший программист сделает себе позикс над любым системным апи, но это лечится административными пиздюлями aka code review. Нет сомнений, что в результате получится говно. Но зато _маленькое_ говно!

После virtio-net мы можем уже сделать дебильный недо-tcp, даже не сделав arp и демультиплексор, и тестить концептуальный клиент-сервер.

Ну а дальше задача скрестить ежа с этим недоужом. Т.е. сделать некий рантайм на расте, в пределе GHC-подобный в плане зеленых потоков, со сборкой мусора, и компилить под него из ФЯ с опциональной верификацией. А если не делать, а найдется готовый - то можно и на сях, главное чтобы был достаточно изолированный от POSIX-анахронизмов и весь из себя по-хипсторски бородатый!
СсылкаОтветить

Comments:
[User Picture]From: nponeccop
2017-12-04 06:49 pm
Про Мираж в курсе. Минимизация, лигаси-фри юникернелизация и верификация это на самом деле четыре разных направления, которыми можно заниматься и по отдельности, хотя они и выигрывают друг от друга.

> люди предпочитают пилить всякое практиш-квадратиш

за такое можно и по голове банхаммером (но у меня вместо него скрин). См. https://nponeccop.livejournal.com/575013.html пункт 3. Люди пилят всякое, селф-контейнед стеков овер 9000, в т.ч. и на расте и на хаскеле (https://github.com/faern/rips/tree/master/src, https://github.com/GaloisInc/HaNS, у эмбедщиков их море (но нужен порт с сей) https://stackoverflow.com/q/3228752/805266

С упором на верификацию тоже есть http://simonjf.com/writing/bsc-dissertation.pdf (на идрисе). Всяких sel4 даже не считаем по причине упоротости
(Ответить) (Parent) (Thread)
From: triampurum
2017-12-05 10:40 am
> пункт 3
Сам не люблю ad praktisch аргументы. "Неважно, работает ли это на практике, покажите, как это работает в теории" (М. Феллейзен). Здесь употреблено в том смысле, что ребята на верификацию даже какой-то части стэка не смотрят, экстрактить с кока с какими-то гарантиями соответствия спецификации не хотят, Fast and loose reasoning их устраивает, что жаль. Диссертацию идрисовскую читал. Живых self-contained posix-free стэков, способных рядом постоять с миражом, встречать не приходилось, но это, наверное, по причине слабого знакомства с темой.
(Ответить) (Parent) (Thread)
[User Picture]From: nponeccop
2017-12-06 07:00 am
Ну, предметно обсуждать я готов.

Там три больших вопроса:

- Зачем что-то делать и что именно делать
- Стратегия: в каком порядке делать
- Откуда накопипастить кода
(Ответить) (Parent) (Thread)
From: triampurum
2017-12-06 11:18 am
Зачем делать legacy-free стэк поверх гипервайзора, мне понятно. Зачем может захотеться верифицировать этот стэк, понятно тоже. Где взять на это ресурсов лично мне - мне непонятно. С радостью поучаствую в обсуждении вопросов из коммента выше, но, как понимаю, обсуждение без готовности вложиться в это и реализовать не укладывается в принятые здесь рамки конструктива.
(Ответить) (Parent) (Thread)
[User Picture]From: nponeccop
2017-12-06 07:00 pm
> обсуждение без готовности вложиться в это и реализовать не укладывается

Вполне укладывается. ЖЖ - это по определению площадка для обсуждений.
(Ответить) (Parent) (Thread)
[User Picture]From: nponeccop
2017-12-06 08:03 pm
Из первого вопроса остались ещё минимизация и юникернелизация:

- Зачем этот legacy-free опционально верифицированный стек дополнительно минимизировать
- Зачем в качестве одного из средств минимизации выбирать юникернелы (но там не просто юникернелы, а однопоточные юникернелы с единственным сокетом в кач-ве внешнего интерфейса)


(Ответить) (Parent) (Thread)
From: triampurum
2017-12-06 08:42 pm
> Зачем этот legacy-free опционально верифицированный стек дополнительно минимизировать

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

> Зачем в качестве одного из средств минимизации выбирать юникернелы (но там не просто юникернелы, а однопоточные юникернелы с единственным сокетом в кач-ве внешнего интерфейса)

Издалека:
Невыгодно держать on premise железяки, выгоднее отдавать это Гуглу (KVM) / Амазону (Xen). Просто по деньгам для бизнеса, за исключением некоторых специфических случаев, но и там выгоднее эти специфичные случаи огораживать у себя, а пиковые нагрузки, к примеру, держать внешними машинками.
От б-гомерзкого железа избавились, теперь у нас есть гипервайзор и, скажем, линукс поверх него.
Бесплатных завтраков все еще никто не дает, вверх мы можем отскалироваться только вот настолько, а мощности, которые нам требуются, как следует из первого пункта, достаточны для того, чтобы начать экономить на инфрастуктуре, сервера в подвале не хватает. Масштабируемся горизонтально, перед нами открывается дивный новый мир, сложность расцветает невиданными ранее красками, мы узнаем про микросервисы, software resilience и нанимаем девопса. Как у нас там наш микросервис выглядит? Ага, убунту, внутри нее докер, в докере alpine, там жвм, в нем микросервис. Живем! Думаем, как оптимизировать, смотрим, чем там занимается линуксовый шедулер в свободное время. Гоним торговцев из храма, пинним процесс к ядру (гипернити). Full blown TCP/IP стэк штука сложная, потенциально дырявая, а нам для наших микросервисов что-нибудь для общения с гарантией доставки и блекджеком есть, и хватит. Получаем, отказавшись от posix-легаси, настоящий юникс-вей - наши микросервисы делают одну вещь, возможно, даже хорошо. Нужна конкурентная модель исполнения - корутины и рядом к нашим услугам. Нужен честный параллелизм - message passing и микросервисы как толстые процессы.
(Ответить) (Parent) (Thread)
From: triampurum
2017-12-06 08:46 pm
гарантия доставки на уровне сетевого протокола, кстати, дискуссионная вещь, т.к. в наших акках здесь, например, бытует мнение, что нормально сделать гарантию доставки можно только на уровне приложения. Условно говоря, если твой актор прибит по ООМ до того, как обработать твое сообщение, то доставка его по сети тебя не радует.
(Ответить) (Parent) (Thread)
From: triampurum
2017-12-06 08:51 pm
про юникернелы не дописал, это естественный следующий шаг: когда у нас есть процесс на vCPU, а железом занимается Xen, ос нам не нужна.
(Ответить) (Parent) (Thread)
From: triampurum
2017-12-06 12:39 pm
Кстати, мимоходом попалось к третьему: https://www.opennet.ru/opennews/art.shtml?num=47691
(Ответить) (Parent) (Thread)
[User Picture]From: nponeccop
2017-12-06 06:24 pm
в духе rump kernel, но с меньшим лигаси (я надеюсь). Ну и уровень дискусси там конечно низкий :)
(Ответить) (Parent) (Thread)