LINUX.ORG.RU
ФорумTalks

seL4

 ,


2

2

Осталось менее 6 часов до открытия исходников ядра seL4, вместе со всеми доказательствами.

Хотел запилить новость, но стало лень. Пишу в толксы.

Некоторые детали:

Поддерживаемые архитектуры: arm (какая-то плата KZM) и x86_32.

Что доказывали: соответствие сишного кода спецификации. Только для arm. Для самой спецификации не доказывалось ничего. Например, не доказывалось отсутствие дыр в модели безопасности. Так что говорить о том, что доказана «корректность» не совсем правильно.

Чем пожертвовали в угоду простоте доказательства: ядро не преемптивно, smp не поддерживается.

В seL4 используются некоторые интересные идеи, отличающие это ядро от других ядер 4-го поколения, вроде L4ka::Pistachio.

Например, ядро не даёт доступа к физической памяти в том смысле что невозможно узнать куда будет отображена страница. Отсюда, вся работа с железом только с использованием IOMMU.

Также ядро не показывает thread ID. Посылка сообщения осуществляется не с использованием thread ID, а с использованием т.н. endpoing capability. Вообще, capability-based access controll — это краеугольный камень модели безопасности seL4. endpoint capability — это объект, с использованием которого можно посылать и получать сообщения. Сервер ждёт сообщений на своём endpoint-е, а поток, который хочет посылать серверу сообщения должен иметь копию endpoing cap. сервера в своём capability space. Откуда клиент возьмёт endpoint сервера? Либо этот endpoint будет засунут в capability space треда его родителем при конструировании оного capability space, либо клиент получит endpoing capability в каком-то другом сообщении. Механизм IPC позволяет пересылать capabilities в сообщениях. Что делать серверу, чтобы отличать клиентов, если недоступны thread ID? Для этого введена возможность пометок endpoint-ов. Сервер, беря оригинальный enpoint, применяет к нему операцию mint указывая какое-то число. Создаётся т.н. minted endpoint capability. Которую сервер отдаёт клиенту. Далее, когда сервер будет ждать сообщений на своём оригинальном endpoint-е, а клиент пошлёт сообщение через помеченный endpoint, то сервер получит число, которым он метил endpoint в специальном регистре. Конечно, не гарантируется что все запросы с данной пометкой приходят от одного потока, т.к. клиент может копировать свои endpoint-ы и передавать кому-то ещё.

Такая модель, на мой взгляд, имеет много плюсов. Во-первых, в отличие от идентификации по номерам потоков, с одним «соединением» (endpoint-ом) могут работать разные потоки клиента, не спрашивая у сервера отдельно разрешения на подключение для каждого потока, для тех моделей, где перед отправкой сообщений нужен handshake. Также эта модель, по сравнению с моделями где для отправки сообщений нужно знать только thread ID и не нужен handshake, ограничивает возможности совершения DoS-атак.

Взамен smp на x86_32 поддерживается node-based concurrency. Физическая память делится поровну между процессорами (я буду говорить о процессорах, даже если это ядра одного) и каждое ядро ОС выполняется на своём процессоре используя свой кусок физической памяти, как будто оно работает на однопроцессорной машине. Ядра друг о друге не знают ничего и друг с другом не общаются. Единственное, позволяется указать число страниц разделяемой памяти. Ядро ОС предоставляет доступ к т.н. Boot Structure, где сообщает номер процессора (ноды) и ссылки на разделяемые страницы. Гарантируется одинаковый порядок следования разделяемых страниц на всех ядрах. Но что делать с этими разделяемыми страницами — дело userspace-кода. Доступ к оборудованию через IOMMU имеет только boot-процессор.

Я бы много чего ещё мог написать. Заинтересовавшиеся могут обратиться к reference manual-у или спрашивать свои ответы в отдельных сообщениях.

Спасибо.


Ответ на: комментарий от post-factum

Не сильно ли накладно такое IPC?

Не измерял. Наверное не сильно медленнее или быстрее любого похожего message-based IPC.

И что делать с существующим многопоточным софтом при такой concurrency?

Ну, будет работать как на однопроцессорной машине (и на ядре без преемптивности).

Я так понимаю, что ядро делалось скорее для embedded-решений, почему и доказывалось для arm. Там smp не так важно и распространено.

kike
() автор топика

Огромное спасибо! Подумаю на досуге...

multihead
()
Ответ на: комментарий от post-factum

Не сильно ли накладно такое IPC?

90% накладных расходов IPC в микроядрах идёт на обеспечение безопасности в модели Юникс.

Сабж отказался от модели безопасности Юникс.

Мне кажется здесь у микроядер два пути:

или отказаться от модели безопасности Юникс и создать свою, что упрощает моделирование ядра.

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

multihead
()

Работа в многопроцессорных системах.

Неизвестность куда будет отображены страница памяти и не давать номеров потоков это безусловный плюс к системе безопасности!

Я правильно понял:

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

Это кажется очень хорошим началом и напоминает DragonFlyBSD...

преемптивность и многопроцессорность можно допилить: сделать планировщик в пользовательском пространстве!!! Он будет запускать на выполнение процессы на множестве однопроцессорных машин и рулить общей памятью. Он и обеспечит параллелизм.

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

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

Если планировщику написать POSIX API то будем иметь Юникс.

Если планировщику сделать своё API то придётся переписывать все проги и писать эмулятор.. Но возможно тогда будет выигрыш в скорости.

Безопасность и её реализация это отдельный вопрос. Если не брать модель Юникс из-за большой цены, то надо сочинять и доказывать свою -> несовместимость API, переписывание программ... или дополнительно писать эмулятор...

multihead
()
Ответ на: комментарий от esandmann

На каждом проце/ядре запускается отдельная копия ОС/планировщика. Я о такой модели впервые в DFBSD услышал.

К стати, кроме выше перечисленных проблем с работой в многопроцессорных системах эта модель дает реально асинхронную работу ОС в целом!

multihead
()
Ответ на: комментарий от esandmann

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

Тогда в микроядро интегрируют часть функционала ФС и различий с DragonFlyBSD будет ещё меньше....

multihead
()
Ответ на: комментарий от post-factum

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

Quasar ★★★★★
()
Ответ на: комментарий от multihead

На каждом проце/ядре запускается отдельная копия ОС/планировщика. Я о такой модели впервые в DFBSD услышал.

Сомневаюсь что в DFBSD подразумевается что планировщики знают о потоках, запущенных только на их ядре.

kike
() автор топика
Ответ на: комментарий от kike

В DFBSD есть как минимум два планировщика глобальных один ядерный LWKT другой в пользовательском режиме обеспечивающий POSIX.

глобальный LWKT передаёт нити локальному планировщику ОС запущеному на конкретном проце и о них знает! То что планируется локальным планировщиком ОС на локальном проце другие не знают, это не их дело.

multihead
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.