Семейство микроядер L4 - L4 microkernel family - Wikipedia
L4 это семья во втором поколении микроядра, обычно используется для реализации Unix-подобный операционные системы, но также используется во множестве других систем.
L4, как и его предшественник L3 микроядро, был создан Немецкий специалист в области информатики Йохен Лидтке в ответ на низкую производительность более ранних операционных систем на базе микроядра. Лидтке считал, что система, разработанная с самого начала для обеспечения высокой производительности, а не для других целей, может создать микроядро для практического использования. Его оригинальная реализация, написанная вручную Intel i386 -специфический язык ассемблера code в 1993 году вызвал большой интерес в компьютерной индустрии.[нужна цитата ] С момента своего появления L4 был разработан для независимость от платформы а также в улучшении безопасность, изоляция и надежность.
Были различные повторные реализации исходного двоичного интерфейса ядра L4 (ABI ) и его преемников, в том числе L4Ka :: Фисташка (Uni Karlsruhe ), L4 / MIPS (UNSW ), Фиаско (TU Dresden ). По этой причине название L4 был обобщен и больше не относится только к исходной реализации Лидтке. Теперь это относится ко всему микроядро семья, включая L4 ядро интерфейс и разные его версии.
L4 широко распространен. Один вариант, OKL4 от Открытые лаборатории ядра, поставлено на миллиарды мобильных устройств.[1][2]
Парадигма дизайна
Уточнение общей идеи микроядро, Liedtke состояния:
Концепция допускается внутри микроядра только в том случае, если ее перемещение за пределы ядра, то есть разрешение конкурирующих реализаций, помешает реализации требуемых функций системы.[3]
В этом духе микроядро L4 предоставляет несколько основных механизмов: адресные пространства (абстрагирование таблиц страниц и обеспечение защиты памяти), потоки и планирование (абстрагирование исполнения и обеспечение временной защиты), и межпроцессного взаимодействия (для контролируемой коммуникации через границы изоляции).
Операционная система, основанная на микроядре, таком как L4, предоставляет услуги в качестве серверов в пространство пользователя который монолитные ядра подобно Linux или микроядра старшего поколения включают внутренне. Например, чтобы реализовать безопасный Unix-подобный системы, серверы должны обеспечивать управление правами, что Мах включены в ядро.
История
Низкая производительность микроядер первого поколения, таких как Мах, побудил ряд разработчиков пересмотреть всю концепцию микроядра в середине 1990-х годов. Асинхронная буферизация в ядре процесс коммуникации Концепция, использованная в Mach, оказалась одной из основных причин его плохой работы. Это побудило разработчиков операционных систем на базе Mach переместить некоторые критичные по времени компоненты, такие как файловые системы или драйверы, обратно внутрь ядра.[нужна цитата ] Хотя это несколько улучшило проблемы с производительностью, это явно нарушает концепцию минимальности настоящего микроядра (и упускает их основные преимущества).
Детальный анализ узкого места Маха показал, что, среди прочего, его рабочий набор слишком большой: код IPC выражает плохую пространственную локальность; то есть это приводит к слишком большому количеству тайник промахи, большинство из которых находятся в ядре.[3] Этот анализ привел к выводу о том, что эффективное микроядро должно быть достаточно маленьким, чтобы большая часть критически важного для производительности кода помещалась в кэш (первого уровня) (предпочтительно небольшую часть указанного кеша).
L3
Йохен Лидтке намеревался доказать, что хорошо разработанный более тонкий МПК Layer с особым вниманием к производительности и машинному (в отличие от платформенно-независимого) дизайну может привести к значительному повышению производительности в реальном мире. Вместо сложной системы IPC Маха его микроядро L3 просто передавало сообщение без дополнительных накладных расходов. Определение и реализация необходимых политик безопасности считались обязанностями пространство пользователя серверы. Роль ядра заключалась только в обеспечении необходимого механизма, позволяющего серверам пользовательского уровня применять политики. L3, разработанный в 1988 году, зарекомендовал себя как безопасный и надежный Операционная система, много лет используется, например, TÜV SÜD[нужна цитата ].
L4
После некоторого опыта использования L3 Лидтке пришел к выводу, что несколько других концепций Маха также неуместны. Еще больше упростив концепции микроядра, он разработал первое ядро L4, которое в первую очередь проектировалось с учетом высокой производительности. Чтобы выжать каждый бит производительности, все ядро было написано на язык ассемблера, а его IPC был в 20 раз быстрее, чем у Маха.[4] Такое резкое повышение производительности - редкое явление для операционных систем, и работа Лидтке привела к появлению новых реализаций L4 и работы над системами на основе L4 в ряде университетов и исследовательских институтов, включая IBM, где Лидтке начала работать в 1996 году, Технический университет Дрездена и UNSW. В IBM Исследовательский центр Томаса Дж. Уотсона Лидтке и его коллеги продолжили исследования систем на базе L4 и микроядра в целом, особенно ОС Sawmill.[5]
L4Ka :: Фундук
В 1999 году Лидтке возглавил группу системной архитектуры в Университет Карлсруэ, где продолжил исследования в области микроядерных систем. В качестве доказательства концепции того, что высокопроизводительное микроядро также может быть построено на языке более высокого уровня, группа разработала L4Ka :: Фундук, версия ядра C ++, работающая на машинах на базе IA-32 и ARM. Эта попытка увенчалась успехом - производительность оставалась приемлемой - и с его выпуском версии ядер на чистом языке ассемблера были фактически прекращены.
L4 / Фиаско
Параллельно с разработкой L4Ka :: Hazelnut в 1998 г. группа операционных систем TUD: OS of the TU Dresden (Дрезденский технологический университет) приступили к разработке своей собственной реализации на C ++ интерфейса ядра L4, получившей название L4 / Fiasco. В отличие от L4Ka :: Hazelnut, который вообще не допускает параллелизма в ядре, и его преемника L4Ka :: Pistachio, который разрешает прерывания в ядре только в определенных точках приоритетного прерывания, L4 / Фиаско был полностью вытеснен (за исключением чрезвычайно коротких атомарных операций) для достижения низкого задержка прерывания. Это было сочтено необходимым, потому что L4 / Fiasco используется в качестве основы DROPS,[6] а жесткий режим реального времени совместимая операционная система, также разработанная TU Dresden. Однако сложность полностью вытесняемой конструкции побудила более поздние версии Fiasco вернуться к традиционному подходу L4 к запуску ядра с отключенными прерываниями, за исключением ограниченного числа точек вытеснения.
Независимость от платформы
L4Ka :: Фисташка
Вплоть до выпуска L4Ka :: Pistachio и более новых версий Fiasco все микроядра L4 были неотъемлемо привязаны к базовой архитектуре ЦП. Следующим большим сдвигом в разработке L4 стала разработка платформенно-независимого API, который все еще сохранял высокие характеристики производительности, несмотря на более высокий уровень переносимости. Хотя базовые концепции ядра остались прежними, новый API предоставил много значительных изменений по сравнению с предыдущими версиями L4, включая лучшую поддержку многопроцессорных систем, более слабые связи между потоками и адресными пространствами и введение управления потоками на уровне пользователя. блоки (UTCB) и виртуальные регистры. После выпуска нового L4 API (Версия X.2, также известная как Версия 4) в начале 2001 года, Группа системной архитектуры Университета Карлсруэ реализовала новое ядро, L4Ka :: Фисташка, полностью с нуля, теперь с упором как на высокую производительность, так и на портативность. Он был выпущен под лицензия BSD с двумя пунктами.
Более новые версии Fiasco
Микроядро L4 / Fiasco также значительно улучшилось за эти годы. Теперь он поддерживает несколько аппаратных платформ от x86 до AMD64 до нескольких платформ ARM. Примечательно, что версия Fiasco (Fiasco-UX) может работать как приложение уровня пользователя поверх Linux.
L4 / Fiasco реализует несколько расширений API L4v2. IPC исключения позволяет ядру отправлять исключения ЦП приложениям-обработчикам на уровне пользователя. С помощью чужие нити можно выполнять точный контроль над системными вызовами. Добавлены UTCB в стиле X.2. Кроме того, Fiasco содержит механизмы для управления правами связи, а также потреблением ресурсов на уровне ядра. На вершине Fiasco разработан набор базовых сервисов пользовательского уровня (называемых L4Env), которые, среди прочего, используются для паравиртуализации текущей версии Linux (4.19 по состоянию на май 2019 года) (называемой L4Linux ).
Университет Нового Южного Уэльса и NICTA
Разработка также проходила на Университет Нового Южного Уэльса (UNSW), где разработчики реализовали L4 на нескольких 64-битных платформах. Их работа привела к L4 / MIPS и L4 / Альфа, в результате чего оригинальная версия Лидтке была ретроспективно названа L4 / x86. Как и оригинальные ядра Liedtke, ядра UNSW (написанные на смеси ассемблера и C) были непереносимыми, и каждое реализовывалось с нуля. С выпуском очень портативного L4Ka :: Pistachio группа UNSW отказалась от собственных ядер в пользу создания хорошо настроенных портов L4Ka :: Pistachio, включая самую быструю из когда-либо зарегистрированных реализаций передачи сообщений (36 циклов на Itanium архитектура).[7] Группа также продемонстрировала, что драйверы устройств пользовательского уровня могут работать так же хорошо, как и драйверы ядра.[8] и разработал Вомбат, очень портативная версия Linux на L4, который работает на процессорах x86, ARM и MIPS. На XScale процессоры, Вомбат демонстрирует затраты на переключение контекста, которые до 50 раз ниже, чем в родном Linux.[9]
Позже группа UNSW в своем новом доме в НИКТА, разветвил L4Ka :: Pistachio в новую версию L4 под названием NICTA :: L4-встроенный. Как следует из названия, это было нацелено на использование в коммерческих встроенных системах, и, следовательно, компромиссы реализации благоприятствовали небольшому объему памяти и были направлены на снижение сложности. API был изменен так, чтобы почти все системные вызовы оставались достаточно короткими, чтобы им не требовались точки прерывания для обеспечения высокой скорости отклика в реальном времени.[10]
Коммерческое развертывание
В ноябре 2005 г. НИКТА объявил[11] который Qualcomm развертывал версию L4 NICTA на своих Модем мобильной станции чипсеты. Это привело к использованию L4 в мобильный телефон телефоны в продаже с конца 2006 года. В августе 2006 года руководитель ERTOS и профессор UNSW Гернот Хайзер создал компанию под названием Открытые лаборатории ядра (OK Labs) для поддержки коммерческих пользователей L4 и дальнейшего развития L4 для коммерческого использования под торговой маркой OKL4, в тесном сотрудничестве с NICTA. OKL4 Version 2.1, выпущенный в апреле 2008 г., был первым общедоступный версия L4, в которой безопасность на основе возможностей. OKL4 3.0, выпущенный в октябре 2008 года, был последней версией OKL4 с открытым исходным кодом. Более поздние версии имеют закрытый исходный код и основаны на переписывании для поддержки собственного варианта гипервизора, называемого OKL4 Microvisor. OK Labs также распространяла паравиртуализированный Linux под названием OK: Linux, потомок Wombat, а также паравиртуализированные версии SymbianOS и Android. OK Labs также приобрела права на seL4 от NICTA.
В начале 2012 года поставки OKL4 превысили 1,5 миллиарда,[2] в основном на чипах беспроводных модемов Qualcomm. Другие варианты развертывания включают автомобильная информационно-развлекательная система системы.[12]
Apple серии A процессоры, начиная с A7 содержать безопасный анклав сопроцессор работает под управлением операционной системы L4[13]на основе встроенного ядра L4, разработанного в НИКТА в 2006 году.[14]Это означает, что L4 теперь поставляется на всех устройствах iOS, общий объем поставок которых оценивается в 310 миллионов на 2015 год.[15]
Высокая надежность: seL4
В 2006 г. НИКТА группа начала с нуля проектирование микроядро третьего поколения, называемый seL4, с целью создания основы для высокозащищенных и надежных систем, подходящих для удовлетворения требований безопасности, таких как Общие критерии и дальше. С самого начала разработка была направлена на формальная проверка ядра. Чтобы упростить выполнение иногда противоречивых требований к производительности и проверке, команда использовала средний программный процесс, начиная с исполняемая спецификация написано в Haskell.[16]seL4 использует управление доступом на основе возможностей для формального рассуждения о доступности объекта.
Формальное доказательство функциональной корректности было завершено в 2009 году.[17]Доказательство обеспечивает гарантию того, что реализация ядра соответствует его спецификации, и подразумевает, что оно не содержит ошибок реализации, таких как взаимоблокировки, живые замки, переполнение буфера, арифметические исключения или использование неинициализированных переменных. seL4 считается первым в истории ядром операционной системы общего назначения, которое было проверено.[17]
seL4 использует новый подход к управлению ресурсами ядра,[18] экспорт управления ресурсами ядра на уровень пользователя и подчиняет их тому же основанный на возможностях контроль доступа как пользовательских ресурсов. Эта модель, которую также приняли на вооружение Баррель, упрощает рассуждения о свойствах изоляции и послужил средством для последующих доказательств того, что seL4 обеспечивает соблюдение основных свойств безопасности, таких как целостность и конфиденциальность.[19] Команда NICTA также подтвердила правильность перевода с C на исполняемый машинный код, взяв компилятор вне надежная вычислительная база из seL4. Это означает, что для исполняемого файла ядра сохраняются доказательства высокого уровня безопасности. seL4 также является первым опубликованным ядром ОС защищенного режима с полным и надежным время исполнения наихудшего случая (WCET) анализ, необходимое условие для его использования в сложных системы реального времени.[19]
29 июля 2014 г. НИКТА и Системы General Dynamics C4 объявил, что seL4 с непрерывными доказательствами теперь выпущен под лицензии с открытым исходным кодом.[20]Исходный код ядра и доказательства находятся под GPLv2, а большинство библиотек и инструментов находятся под лицензией BSD с двумя пунктами.
Исследователи заявляют, что стоимость формальной проверки программного обеспечения ниже, чем стоимость разработки традиционного «высоконадежного» программного обеспечения, несмотря на то, что дает гораздо более надежные результаты.[21] В частности, стоимость одного строка кода во время разработки seL4 оценивался примерно в 400 долларов США, в сравнении с 1000 долларов США для традиционных систем высокой надежности.[22]
Под DARPA Программа High-Assurance Cyber Military Systems (HACMS), NICTA вместе с партнерами по проекту Роквелл Коллинз, Galois Inc, Университет Миннесоты и Боинг разработал беспилотный летательный аппарат с высоким уровнем надежности на базе seL4, наряду с другими инструментами и программным обеспечением для обеспечения гарантий, с запланированной передачей технологий на опционально пилотируемый автономный Беспилотная птичка вертолет, разрабатываемый компанией Boeing. Окончательная демонстрация технологии HACMS состоялась в Стерлинге, штат Вирджиния, в апреле 2017 года.[23] DARPA также профинансировало несколько Инновационные исследования малого бизнеса (SBIR) контракты, связанные с seL4 в рамках программы, начатой Dr. Джон Лаанчбери. Малые предприятия, получившие SBIR, связанные с seL4, включали: DornerWorks, Techshot, Wearable Inc, Real Time Innovations и Critical Technologies.[24]
Прочие исследования и разработки
Osker, ОС, написанная на Haskell, ориентированный на спецификацию L4; хотя в этом проекте основное внимание уделялось использованию функциональное программирование язык для разработки ОС, а не исследования микроядра как такового.[25]
CodeZero - это микроядро L4, предназначенное для встраиваемых систем с акцентом на виртуализацию и реализацию собственных сервисов ОС. Существует GPL -лицензионная версия,[26] и версия, которая была перелицензирована разработчиками как закрытая и разветвленная в 2010 году.[27]
Микроядро F9,[28] реализация L4 под лицензией BSD, посвященная ARM Cortex-M процессоры для глубоко встраиваемых устройств с защитой памяти.
Архитектура виртуализации ОС NOVA - это исследовательский проект с упором на создание безопасной и эффективной среды виртуализации.[29][30]с небольшой надежной вычислительной базой. NOVA состоит из микрогипервизора, пользовательского уровня монитор виртуальной машины, и непривилегированную компонентную многосерверную пользовательскую среду, работающую поверх нее, которая называется NUL. NOVA работает на многоядерных системах на базе x86.
WrmOS[31] это операционная система реального времени, основанная на микроядре L4. Имеет собственные реализации ядра, стандартных библиотек и сетевого стека, поддерживающие архитектуры SPARC, ARM, x86 и x86_64. Есть паравиртуализированное ядро Linux (w4linux[32]) работает поверх WrmOS.
Рекомендации
- ^ «Продукты гипервизора - General Dynamics Mission Systems». gdmissionsystems.com. В архиве с оригинала 15 ноября 2017 г.. Получено 26 апреля 2018.
- ^ а б «Программное обеспечение Open Kernel Labs превзошло рубеж в 1,5 миллиарда отгрузок мобильных устройств» (Пресс-релиз). Открытые лаборатории ядра. 19 января 2012 г. Архивировано с оригинал 11 февраля 2012 г.
- ^ а б Лидтке, Йохен (Декабрь 1995 г.). «О конструкции µ-ядра». Proc. 15-й симпозиум ACM по принципам операционных систем (SOSP). С. 237–250. В архиве с оригинала 25 октября 2015 года.
- ^ Лидтке, Йохен (Декабрь 1993 г.). «Улучшение IPC за счет дизайна ядра». 14-й симпозиум ACM по принципам операционных систем. Эшвилл, Северная Каролина, США. С. 175–88.
- ^ Гефло, Ален; Джегер, Трент; Пак, Юнхо; Лидтке, Йохен; Эльфинстон, Кевин; Улиг, Фолькмар; Тидсуэлл, Джонатон; Деллер, Люк; Рейтер, Ларс (2000). «Многосерверный подход Лесопилки». ACM SIGOPS Европейский семинар. Колдинг, Дания. С. 109–114.
- ^ «Архивная копия». В архиве из оригинала 2011-08-07. Получено 2011-08-10.CS1 maint: заархивированная копия как заголовок (связь)
- ^ Грей, Чарльз; Чепмен, Мэтью; Чабб, Питер; Мосбергер-Танг, Дэвид; Хайзер, Гернот (Апрель 2005 г.). "Itanium - сказка разработчика систем". Ежегодная техническая конференция USENIX. Аннахайм, Калифорния, США. С. 264–278. В архиве из оригинала от 17.02.2007.
- ^ Лесли, Бен; Чабб, Питер; Фитцрой-Дейл, Николас; Гётц, Стефан; Грей, Чарльз; Макферсон, Люк; Поттс, Дэниел; Шен, Ютинг; Эльфинстон, Кевин; Хайзер, Гернот (Сентябрь 2005 г.). «Драйверы устройств пользовательского уровня: достигнутая производительность». Журнал компьютерных наук и технологий. 20 (5): 654–664. CiteSeerX 10.1.1.59.6766. Дои:10.1007 / s11390-005-0654-4. S2CID 1121537.
- ^ ван Шайк, Карл; Хайзер, Гернот (Январь 2007 г.). «Высокопроизводительные микроядра и виртуализация на ARM и сегментированных архитектурах». 1-й международный семинар по микроядрам для встраиваемых систем. Сидней, Австралия: НИКТА. С. 11–21. В архиве из оригинала на 2015-03-01. Получено 2015-10-25.
- ^ Руокко, Серджио (октябрь 2008 г.). "Путешествие программиста в реальном времени по микроядрам L4 общего назначения". Журнал EURASIP по встроенным системам. 2008: 1–14. Дои:10.1155/2008/234710. S2CID 7430332.
- ^ «Микроядро NICTA L4 будет использоваться в некоторых решениях на базе набора микросхем QUALCOMM» (Пресс-релиз). НИКТА. 24 ноября 2005 г. Архивировано с оригинал 25 августа 2006 г.
- ^ "Виртуализация автомобилей Open Kernel Labs выбрана Bosch для информационно-развлекательных систем" (Пресс-релиз). Открытые лаборатории ядра. 27 марта 2012 г. Архивировано с оригинал 2 июля 2012 г.
- ^ «Безопасность iOS, iOS 12.3» (PDF). Apple Inc., май 2019 г.
- ^ Мандт, Тарьей; Сольник, Мэтью; Ван, Дэвид (31 июля 2016 г.). «Демистификация процессора Secure Enclave» (PDF). BlackHat США. Лас-Вегас, Невада, США. В архиве (PDF) с оригинала 21 октября 2016 г.
- ^ Элмер-ДеВитт, Филип (28 октября 2014 г.). «Прогноз: Apple поставит 310 миллионов устройств iOS в 2015 году». Удача. В архиве из оригинала 27 сентября 2015 г.. Получено 25 октября, 2015.
- ^ Деррин, Филип; Эльфинстон, Кевин; Кляйн, Гервин; Петух; Дэйвид; Чакраварти, Мануэль М. Т. (сентябрь 2006 г.). «Выполнение руководства: подход к разработке высоконадежного микроядра». ACM SIGPLAN Мастерская Haskell. Портланд, штат Орегон. С. 60–71.
- ^ а б Кляйн, Гервин; Эльфинстон, Кевин; Хайзер, Гернот; Андроник, июнь; Петух, Дэвид; Деррин, Филип; Элькадуве, Дхаммика; Энгельгардт, Кай; Колански, Рафаль; Норриш, Майкл; Сьюэлл, Томас; Туч, Харви; Уинвуд, Саймон (октябрь 2009 г.). "seL4: Формальная проверка ядра ОС" (PDF). 22-й симпозиум ACM по принципам операционных систем. Big Sky, MT, США. В архиве (PDF) из оригинала 28.07.2011.
- ^ Элькадуве, Дхаммика; Деррин, Филип; Эльфинстон, Кевин (апрель 2008 г.). Дизайн ядра для изоляции и обеспечения физической памяти. 1-й семинар по изоляции и интеграции во встроенных системах. Глазго, Великобритания. Дои:10.1145/1435458. Получено 2020-02-22.
- ^ а б Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хайзер, Гернот (февраль 2014 г.). «Комплексная формальная проверка микроядра ОС». ACM-транзакции в компьютерных системах. 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140. Дои:10.1145/2560537. S2CID 4474342.
- ^ «Безопасная операционная система, разработанная NICTA, имеет открытый исходный код» (Пресс-релиз). НИКТА. 29 июля 2014 г. В архиве с оригинала 15 марта 2016 г.
- ^ Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хайзер, Гернот (2014). «Комплексная формальная проверка микроядра ОС» (PDF). ACM-транзакции в компьютерных системах. 32: 64. CiteSeerX 10.1.1.431.9140. Дои:10.1145/2560537. S2CID 4474342. В архиве (PDF) из оригинала от 03.08.2014.
- ^ seL4 бесплатно - что это значит для вас? на YouTube
- ^ «DARPA выбирает Rockwell Collins для применения технологии кибербезопасности на новых платформах» (Пресс-релиз). Роквелл Коллинз. 24 апреля 2017 года. В архиве с оригинала от 11 мая 2017 года.
- ^ "Спонсор агентства DARPA доктор Джон Лаанчбери". SBIRSource. 2017. В архиве из оригинала от 29 сентября 2017 г.. Получено 16 мая, 2017.
- ^ Hallgren, T .; Jones, M.P .; Лесли, Р .; Толмач, А. (2005). «Принципиальный подход к построению операционных систем на Haskell» (PDF). Материалы Десятой Международной конференции ACM SIGPLAN по функциональному программированию. 40 (9): 116–128. Дои:10.1145/1090189.1086380. ISSN 0362-1340. В архиве (PDF) из оригинала от 15.06.2010. Получено 2010-06-24.
- ^ "jserv / codezero: Codezero Microkernel". В архиве из оригинала 2015-08-15. Получено 2020-10-20.
- ^ «Архивная копия». Архивировано из оригинал 11 января 2016 г.. Получено 25 января, 2016.CS1 maint: заархивированная копия как заголовок (связь)
- ^ "Микроядро F9". Получено 2020-10-20.
- ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). "NOVA: Архитектура безопасной виртуализации на основе микрогипервизора". EuroSys '10: Материалы 5-й Европейской конференции по компьютерным системам. Париж, Франция.
- ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). «На пути к масштабируемой многопроцессорной среде на уровне пользователя». IIDS'10: Семинар по изоляции и интеграции для надежных систем. Париж, Франция.
- ^ "WrmOS". Получено 2020-10-20.
- ^ "w4linux - это паравиртуализированное ядро Linux, работающее поверх WrmOS". Получено 2020-10-20.
дальнейшее чтение
- Йохен Лидтке, Ульрих Бартлинг, Уве Бейер, Дитмар Генрихс, Рудольф Руланд, Дьюла Салай. Два года опыта работы с ОС на основе μ-ядра, ACM Press 1991
- Лидтке, Йохен; Хэберлен, Андреас; Пак, Юнхо; Рейтер, Ларс; Улиг, Фолькмар (2000-10-22). «Производительность заглушки становится важной». В материалах 1-го семинара по промышленному опыту с системным программным обеспечением (WIESS), Сан-Диего, Калифорния, октябрь 2000 г.. Архивировано из оригинал (PDF) на 2006-09-05. Получено 2006-09-05. (на ядре L4 и компиляторе)
- Ченг Гуанхуи, Николас МакГвайр. L4 / Fiasco / L4Linux Кикстарт, Лаборатория распределенных и встроенных систем - Университет Ланьчжоу
- Эльфинстон, Кевин; Хайзер, Гернот (Ноябрь 2013). «От L3 к seL4: что мы узнали за 20 лет использования микроядер L4?». 24-й симпозиум ACM SIGOPS по принципам операционных систем. Фармингтон, Пенсильвания, США. С. 133–150. Эволюция подходов к проектированию и реализации L4
внешняя ссылка
- Официальный веб-сайт, L4Hq: штаб-квартира L4, сайт сообщества для проектов L4
- Семейство микроядер L4: Обзор реализаций L4, документации и проектов
- Официальный TUD: OS Wiki
- L4Ka: Реализации L4Ka :: Pistachio и L4Ka :: Hazelnut
- UNSW: Реализации для DEC Alpha и Архитектура MIPS
- OKL4: Коммерческая версия L4 от Открытые лаборатории ядра
- NICTA L4: Обзор исследований и публикации
- Группа надежных систем в CSIRO's Data61: Дом бывшей группы NICTA, которая разработала seL4
- Платформа операционной системы Genode: Потомок сообщества L4
- seL4: Очень безопасная и надежная система