Interested Article - L4 (микроядро)

L4 — микроядро второго поколения , разработанное Йохеном Лидтке в 1993 году .

Архитектура микроядра L4 оказалась успешной. Было создано множество реализаций ABI и API микроядра L4. Все реализации стали называть семейством микроядер L4. Реализация Лидтке неофициально была названа «L4/x86» .

История

L1

В 1977 году Йохен Лидтке защитил дипломный проект по математике в университете города Билефельд (Германия). В рамках проекта Лидтке написал компилятор для языка ( ). Язык ELAN создан в 1974 году на основе языка Алгол 68 для обучения программированию . Лидтке назвал свою работу «L1»: буква «L» — первая буква фамилии автора ( L iedtke ); цифра «1» — порядковый номер работы.

L2

В 1977 году Лидтке получил диплом математика, остался в университете города Билефельд и приступил к созданию среды выполнения для языка ELAN.

8‑битные микроконтроллеры стали широко доступными. Требовалась операционная система, способная работать на небольших рабочих станциях в средних школах и вузах. CP/M не подходила. Национальный исследовательский центр компьютерных наук и технологий Германии GMD и университет города Билефельд решил разработать новую операционную систему с нуля .

В 1979 году Йохен Лидтке начал разработку новой операционной системы и назвал её « » ( ) от англ. e xtendable multi u ser m icroprocessor EL AN-system . Операционная система «Eumel» также называлась «L2», что означает « 2 ‑я работа L iedtke». Новая ОС поддерживала 8-битовые процессоры Zilog Z80 , была многопользовательской и многозадачной , была построена на основе микроядра , поддерживала . Поддержка orthogonal persistence заключалась в следующем: ОС периодически сохраняла на диск своё состояние (содержимое памяти , регистров процессора и др.); после перебоев в подаче электроэнергии ОС восстанавливалась из сохранённого состояния; программы продолжали работать так, будто бы сбоя не происходило; терялись только изменения, внесённые с момента последнего сохранения. ОС Eumel проектировалась под влиянием ОС Multics и содержала много общего с ядрами и Mach .

Позднее ОС Eumel была портирована на процессоры Zilog Z8000 , Motorola 68000 и Intel 8086 . Эти процессоры были 8‑ и 16‑битовыми, не содержали MMU и не поддерживали механизма защиты памяти . ОС Eumel эмулировала виртуальную машину , имеющую 32‑битовую адресацию и MMU . Несмотря на использование эмуляции, к одной рабочей станции с ОС Eumel можно было подключить до пяти терминалов .

Поначалу писать программы для ОС Eumel можно было только на языке ELAN. Позднее были добавлены компиляторы для языков , Pascal , Basic и , но массово они не применялись .

С 1980 года началось применение ОС Eumel сначала для обучения программированию и обработки текста, а затем — и в коммерческих целях. Так, в середине 1980‑х годов ОС Eumel работала уже на более чем 2000 компьютеров в юридических и других фирмах .

L3

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

В 1984 году Йохен Лидтке перешёл на работу в исследовательский центр GMD для создания ОС, аналогичной ОС Eumel, но работающей без эмуляции. В настоящее время GMD входит в состав организации « Общество Фраунгофера ».

С 1987 года Йохен Лидтке и его команда из института , входящем в состав GMD, приступили к разработке нового микроядра, получившего название «L3» («L3» от « 3 ‑я работа L iedtke»).

Йохен Лидтке хотел проверить, возможно ли добиться высокой производительности компонента IPC , если выбрать для ядра подходящую архитектуру и в реализации использовать особенности архитектуры . Реализация механизма IPC оказалась удачной (по сравнению со сложной реализацией IPC в микроядре Mach). Позднее был реализован механизм изоляции областей памяти процессов , работающих в пространстве пользователя .

В 1988 году разработка была завершена и была выпущена одноимённая операционная система. Микроядро L3 было написано на языке ассемблера , задействовало особенности процессоров архитектуры Intel x86 , не поддерживало другие платформы, по производительности обогнало микроядро Mach. ОС L3 была совместима с ОС Eumel: программы, созданные для ОС Eumel, работали под управлением ОС L3, но не наоборот .

Компоненты микроядра L3:

компонент IPC (реализовывал механизм для синхронного обмена сообщениями );
компонент, обеспечивающий работу со страницами памяти и работающий в пространстве пользователя ;
компонент, реализующий механизм обеспечения безопасности, называемый англ. secure domains («tasks», «clans» и «chiefs»).

С 1989 года ОС стала применяться:

в школах (заменила свою предшественницу — ОС Eumel) ;
на примерно 3000 компьютерах, установленных в юридических фирмах Германии .

L4

Во время работы над микроядром L3 Йохен Лидтке обнаружил недостатки микроядра Mach. Желая повысить производительность, Лидтке стал составлять код нового микроядра на языке ассемблера с использованием особенностей архитектуры процессоров Intel i386 . Новое микроядро получило название «L4» (от « 4 ‑я работа L iedtke»).

В 1993 году реализация микроядра L4 была закончена. Компонент IPC оказался в 20 раз быстрее IPC из микроядра Mach .

ОС, построенные на микроядрах первого поколения (в частности, на микроядре Mach), отличались низкой производительностью. Из-за этого в середине 1990-х годов разработчики стали пересматривать концепцию микроядерной архитектуры. В частности, плохую производительность микроядра Mach объясняли переносом компонента, ответственного за IPC, в пространство пользователя.

Исследователи искали причины низкой производительности микроядра Mach и тщательно анализировали компоненты, важные для обеспечения хорошей производительности. Анализ показал, что ядро выделяло процессам слишком большой working set (много памяти), в результате чего при обращении ядра к памяти постоянно происходили кэш ‑промахи ( англ. cache misses ) . Анализ позволил сформулировать новое правило для разработчиков микроядер — микроядро должно проектироваться так, чтобы компоненты, важные для обеспечения высокой производительности, помещались в кэш процессора (желательно, первого уровня ( англ. level 1 , L1) и желательно, чтобы в кеше ещё осталось немного места).

Из-за резкого скачка в производительности компонента IPC существующие ОС оказались неспособны обработать возросший поток сообщений IPC. Несколько университетов (например, технический университет Дрездена , университет Нового Южного Уэльса ), институтов и организаций (например, IBM ) начали создавать реализации L4 и строить на их основе новые ОС.

В 1996 году Лидтке защитил диссертацию на степень PhD в техническом университете Берлина по теме «защищённые таблицы страниц» .

С 1996 года в Лидтке с коллегами продолжил исследования микроядра L4, микроядер вообще и операционной системы « » в частности . Из-за отсутствия коммерческого успеха у ОС « », построенной на третьей версии микроядра Mach от CMU и разрабатываемой фирмой IBM с января 1991 года по 1996 год , вместо понятия «микроядро L4» использовалось понятие «Lava Nucleus» или, кратко, «LN».

Со временем код микроядра L4 был избавлен от привязки к платформе, были улучшены механизмы обеспечения безопасности и изоляции.

В 1999 году Лидтке стал работать профессором по операционным системам в технологическом институте Карлсруэ (Германия) .

Микроядро L4Ka::Hazelnut

В 1999 году Йохен Лидтке был принят в состав группы «Systems Architecture Group» ( SAG), работающей в технологическом институте Карлсруэ (Германия), и продолжил исследования микроядерных ОС. Группа SAG также известна как группа «L4Ka».

Желая доказать возможность реализации микроядра на высокоуровневом языке , группа разработала микроядро «L4Ka::Hazelnut». Работа велась в технологическом институте Карлсруэ при поддержке DFG . Реализация была написана на языке C++ и поддерживала процессоры архитектур IA-32 и ARM . Производительность нового микроядра оказалась приемлемой, и разработка ядер на языке ассемблера была прекращена.

Микроядро L4/Fiasco

В 1998 году группа Operating Systems Group, входящая в состав технического университета Дрездена, начала разработку собственной реализации микроядра L4, получившую название «L4/Fiasco». Разработка велась на языке C++ параллельно с разработкой микроядра «L4Ka::Hazelnut».

В то время микроядро L4Ka::Hazelnut не поддерживало concurrency в пространстве ядра, а микроядро «L4Ka::Pistachio» поддерживало прерывания в пространстве ядра только в особых точках preemption. Разработчики микроядра «L4/Fiasco» реализовали полную вытесняющую многозадачность (за исключением некоторых атомарных операций). Это усложнило архитектуру ядра, но снизило задержки при прерываниях, что важно для операционной системы реального времени.

Микроядро «L4/Fiasco» использовалось в ОС «DROPS» — ОС «жёсткого» реального времени (когда крайне важно, чтобы на событие реагировали в строго установленные сроки), также разработанной в техническом университете Дрездена.

Ввиду усложнения архитектуры микроядра в поздних версиях ОС «Fiasco» разработчики вернулись к традиционному подходу — запуску ядра с выключенными прерываниями (за исключением нескольких точек preemption).

Независимость от платформ

Микроядро L4Ka::Pistachio

Реализации микроядра L4, созданные до выпуска микроядра L4Ka::Pistachio и поздних версий микроядра «Fiasco», использовали особенности архитектуры компьютера (были «привязаны» к архитектуре процессора). Был разработан API, не зависимый от архитектуры. Несмотря на добавление , API обеспечивал высокую производительность. Идеи, лежащие в основе микроядерной архитектуры, не изменились.

В начале 2001 года новое L4 API было опубликовано, сильно отличалось от L4 API предыдущей версии, получило номер версии 4 («version 4», также известно как «version X.2») и отличалось:

лучшей поддержкой многопроцессорных систем;
«looser ties» между потоками и адресным пространством;
добавлением к потокам, работающим в пространстве пользователя, блоков UTCBs ( англ. user-level thread control blocks );
добавлением виртуальных регистров .

После выпуска новой версии API группа SAG приступила к созданию нового микроядра, получившего название «L4Ka::Pistachio» . Код составлялся с нуля на языке C++, использовался опыт проекта L4Ka::Hazelnut. Внимание уделялось высокой производительности и переносимости.

10 июня 2001 года доктор Йохен Лидтке погиб в автокатастрофе. После этого скорость развития проекта заметно снизилась.

В 2003 году работа была завершена благодаря усилиям студентов Лидтке: Volkmar Uhlig, Uwe Dannowski и Espen Skoglund. Исходный код был выпущен под лицензией 2‑clause BSD .

Новые версии Fiasco

Параллельно продолжалось развитие микроядра L4/Fiasco. Была добавлена поддержка нескольких аппаратных платформ ( x86 , AMD64 , ARM ). Примечательно, что версия Fiasco, названная «FiascoUX», могла работать в пространстве пользователя под управлением ОС Linux .

Разработчики микроядра L4/Fiasco реализовали несколько расширений к L4v2 API.

Исключение IPC позволило ядру передавать обработку исключений процессора в пространство пользователя.
Добавление (потока, выполняемого одним ядром процессора от имени процесса, запущенного на другом ядре процессора) позволило реализовать детальное управление системными вызовами .
Добавление UTCB (таких же, как в L4 API версии X.2).

Кроме того, микроядро «Fiasco» предоставляло механизмы управления правами коммуникации. Такие же механизмы существовали для управления потребляемыми ядром ресурсами.

Был разработан «L4Env» — набор компонентов, работающих поверх микроядра «Fiasco» в пространстве пользователя. «L4Env» использовался в «L4Linux» — реализации паравиртуализации (виртуализации ABI) для ядер Linux версий 2.6.x.

Университет Нового Южного Уэльса и фирма NICTA

Разработчики из университета Нового Южного Уэльса создали микроядра L4/MIPS и L4/Alpha — реализации L4 для 64‑битовых процессоров серий MIPS и DEC Alpha . Оригинальное микроядро L4 поддерживало только процессоры архитектуры x86 и неофициально стало называться «L4/x86». Реализации были написаны с нуля на языке C и языке ассемблера, не были переносимы. После выпуска независимого от платформы микроядра L4Ka::Pistachio группа UNSW прекратила разработку своих микроядер, занялась портированием микроядра L4Ka::Pistachio. Реализация механизма передачи сообщений оказалась быстрее других реализаций (36 тактов на процессорах архитектуры Itanium ) .

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

Она разработала компоненты для паравиртуализации ядер Linux. Компоненты работали поверх микроядра L4. Результат был назван « ». Wombat OS могла работать на процессорах архитектур x86, ARM и MIPS. На процессорах Intel XScale ОС Wombat OS выполняла переключение контекста в 30 раз медленнее, чем монолитное ядро Linux .

Затем группа UNSW перешла в фирму NICTA, создала ответвление микроядра L4Ka::Pistachio и назвала его «NICTA::L4-embedded». Новое микроядро писалось для коммерческих встраиваемых систем , требовало мало памяти и реализовывало упрощённый API L4. С упрощённым API системные вызовы были сделаны настолько «короткими», что не требовали точек вытесняющей многозадачности и позволяли реализовать ОС реального времени .

Коммерческое применение

Фирма Qualcomm запускала реализацию микроядра L4, разработанную фирмой « », на наборе микросхем, называемом «Mobile Station Modem» (MSM). Об этом в ноябре 2005 года сообщили представители фирмы «NICTA», а в конце 2006 года наборы микросхем MSM поступили в продажу. Так реализация микроядра L4 оказалась в сотовых телефонах .

В августе 2006 года основал фирму Open Kernel Labs. Тогда Хейсер занимал должность руководителя программы ERTOS, организованной фирмой NICTA , и был профессором в университете UNSW. Фирма «OK Labs» создавалась для

оказания технической поддержки коммерческим пользователям L4;
продолжения разработки L4 совместно с фирмой «NICTA» для продолжения коммерческого использования реализации L4, но уже под брендом «OKL4».

В апреле 2008 года была выпущена версия 2.1 микроядра «OKL4» — первая общедоступная реализация L4, имеющая . В октябре 2008 года вышла версия 3.0 — последняя версия «OKL4» с открытым исходным кодом . Исходный код следующих версий был закрыт. Прослойка микроядра, обеспечивающая работу гипервизора , была переписана с целью добавления поддержки native гипервизора, называемого «OKL4 microvisor» .

Фирма «OK Labs» распространяла паравиртуализированную ( англ. para-virtualized ) ОС Linux , называемую «OK:Linux» . «OK:Linux» была потомком ОС « » (англ.) . Также фирма «OK Labs» распространяла паравиртуализированные версии операционных систем Symbian и Android.

Фирма «OK Labs» приобрела у фирмы «NICTA» права на микроядро «seL4».

В начале 2012 года было продано более 1,5 миллиарда устройств , оснащённых реализацией микроядра L4 . Большинство из этих устройств содержало микросхемы, реализующие беспроводные модемы и было выпущено фирмой « Qualcomm ».

Реализация L4 также использовалась в автомобильных развлекательных системах .

ОС, построенная на основе реализации L4, исполнялась процессором secure enclave, входящим в состав размещённой на кристалле электронной схемы Apple A7 . Эта же реализация L4 использовалась в проекте «Darbat» фирмы NICTA . Устройства, содержащие Apple A7, поставлялись с ОС iOS . По состоянию на 2015 год количество устройств с ОС iOS составляло примерно 310 миллионов .

Верификация

seL4

В 2006 году началась разработка микроядра третьего поколения , получившего название «seL4» . Разработка началась с нуля группой программистов из фирмы «NICTA». Цель: создание основы для построения безопасных и надёжных систем, способных удовлетворить современным требованиям безопасности, записанным, например, в документе «Общие критерии оценки защищённости информационных технологий». С самого начала код микроядра писался так, чтобы была возможность его верификации (проверки корректности). Верификация выполнялась с помощью языка Haskell : на языке Haskell записывались требования к микроядру (спецификация); объекты микроядра представлялись в виде объектов Haskell; работа с оборудованием эмулировалась . Чтобы иметь возможность получения информации о доступности объекта путём выполнения формального рассуждения, в seL4 использовался контроль доступа, основанный на capability-based security.

В 2009 году было завершено доказательство корректности кода микроядра seL4 . Существование доказательства гарантировало соответствие реализации и спецификации, подтверждало отсутствие в реализации некоторых ошибок (например, отсутствие взаимных блокировок , livelocks, переполнений буферов , арифметических исключений и случаев использования неинициализированных переменных). Микроядро seL4 было первым микроядром, предназначенным для ОС общего назначения и прошедшим верификацию .

В микроядре seL4 было реализовано нестандартное управление ресурсами ядра :

управлением ресурсами ядра занимался компонент, работающий в пространстве пользователя;
механизм capability-based security использовался не только для контроля доступа к ресурсам пространства пользователя, но и для контроля доступа к ресурсам ядра.

Нечто похожее было реализовано в экспериментальной ОС Barrelfish . Благодаря такому подходу к управлению ресурсами ядра появилась возможность выполнения рассуждения о изолированности свойств, а в дальнейшем было выполнено доказательство того, что микроядро seL4 обеспечивает целостность и конфиденциальность свойств . Доказательство было выполнено для исходного кода.

Команда исследователей из фирмы NICTA доказала корректность трансляции текста с языка C на машинный код. Это позволило исключить компилятор из списка доверенного ПО и считать доказательство, выполненное для исходного кода микроядра, справедливым и для исполняемого файла микроядра.

Микроядро seL4 стало первым ядром, поддерживающим защищённый режим , для которого анализ worst-case execution-time был выполнен полностью, а результаты этого анализа были опубликованы. Результаты анализа необходимы для использования микроядра в ОС жёсткого реального времени .

29 июля 2014 года фирмы NICTA и (англ.) ( объявили о выпуске микроядра seL4 (включая все доказательства их корректности) под открытыми лицензиями . Исходный код микроядра и доказательства поставлялись под лицензией GPL v2. Большинство библиотек и инструментов поставлялись под лицензией 2-clause BSD.

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

В августе 2012 года фирмы NICTA, (англ.) ( , , Boeing и университет Миннесоты в рамках программы по разработке высоконадежных военных кибер-систем , организованной агентством DARPA , приступили к разработке беспилотного летательного аппарата . Основное требование к разработке — обеспечение высокой надёжности аппарата. У каждой из перечисленных фирм была своя роль в программе. Фирма NICTA была ответственна за разработку ОС и построила её на основе микроядра seL4. Ответственные задачи были реализованы в виде компонентов микроядра, а не ответственные — запускались под паравиртуализированной ОС Linux. Наработки программы планировалось использовать в вертолёте «NICTA Unmanned Little Bird», разработкой которого занималась фирма Boeing. Вертолёт должен был поддерживать как управление пилотом, так и беспилотный режим. В ноябре 2015 года было сообщено об успешной реализации .

Другие исследования и разработки

Hurd/L4 . В ноябре 2000 года для обсуждения идеи портирования ядра « GNU Hurd » на микроядро L4 был создан список рассылки «l4-hurd». Портирование осуществлялось в течение 2002‑2004 годов, результат получил название «Hurd/L4». Реализация «Hurd/L4» не была окончена. В 2005 году проект был остановлен .

Osker — операционная система, реализующая L4 и написанная на языке Haskell в 2005 году . Цель проекта: проверка возможности реализации ОС на функциональном языке (а не исследовании микроядра) .

Codezero — реализация микроядра L4 для встраиваемых систем, ставшая общедоступной летом 2009 года . Создана разработчиками британской фирмы «B Labs» с нуля. Код составлялся на языке C. Реализация поддерживает процессоры архитектуры ARM , реализует гипервизор первого порядка , поддерживает виртуализацию ОС Linux и Android . Несмотря на заявление о поставке кода под лицензией GPL v3, скачать код с официального сайта нельзя.

F9 — реализация микроядра L4, ставшая общедоступной в июле 2013 года . Написана с нуля на языке C. Предназначена для встраиваемых систем. Поддерживает серии процессоров Cortex-M архитектуры ARM. Код поставляется под лицензией BSD.

Fiasco.OC — микроядро третьего поколения , созданное на основе микроядра «L4/Fiasco». Реализует механизм (англ.) ( , поддерживает многоядерные процессоры и аппаратную виртуализацию .

L4 Runtime Environment (кратко, L4Re) — каркас, работающий поверх микроядра «Fiasco.OC» и предназначенный для создания компонентов в пространстве пользователя. L4Re предоставляет функционал для создания клиент-серверных приложений, реализации файловых систем, реализует популярные библиотеки, например, стандартную библиотеку языка C («libc»), стандартную библиотеку языка C++ («libstdc++») и библиотеку pthreads .

Каркас L4Re и микроядро «Fiasco.OC» поддерживали процессоры архитектур x86 (IA-32 и AMD64), ARM и PowerPC (WiP).

L4Linux — подсистема для запуска ОС Linux поверх микроядра «Fiasco.OC» с помощью паравиртуализации . Ранее вместо пары «Fiasco.OC» — L4Re использовалась пара «L4/Fiasco» — L4Env.

NOVA ( англ. the N OVA O S v irtualization a rchitecture ) — исследовательский проект, созданный с целью создания безопасного и эффективного окружения для виртуализации с небольшим списком доверенного ПО ( англ. trusted computing base ). В состав NOVA входят:

микроядро, реализующее L4 и гипервизор первого порядка ( англ. baremetal hypervisor );
VMM Vancouver — компонент микроядра (процесс), работающий в пространстве пользователя, занимающийся обслуживанием (эмуляцией оборудования) одной виртуальной машины и лишённый привилегий. На каждую виртуальную машину запускалось по одному VMM. VMM Vancouver входит в состав NUL и может быть заменён на VMM Seoul. VMM Seoul создан на основе VMM Vancouver;
NUL ( англ. N OVA u ser- l evel environment ) — некоторые компоненты микроядра, работающие в пространстве пользователя (VMM Vancouver, драйверы устройств (например, сетевой карты); partition manager; компоненты, предназначенные для управления памятью, вводом-выводом; компоненты, реализующие стеки TCP/IP , USB и др.). NUL может быть заменён на genode или NRE. NRE ( англ. N OVA r untime e nvironment ) — потомок NUL.

Проект NOVA поддерживал многоядерные процессоры архитектуры x86. Для запуска под управлением микрогипервизора (гипервизора, построенного на микроядре) NOVA гостевая ОС должна поддерживать Intel VT-x или AMD-V . Исходный код поставлялся под лицензией GPL v2.

Xameleon — ОС на микроядре L4 . Проект основал в 2001 году единственный разработчик (род. 19 января 1973 года ). Изначально ОС была построена поверх микроядра « ». Позднее автор перевёл ОС на микроядро « ». Исходный код ОС закрыт.

WrmOS — операционная система реального времени (РТОС) с открытым исходным кодом, основанная на микроядре L4. имеет собственную реализацию ядра, стандартных библиотек и сетевого стэка. Поддержаны следующие процессорные архитектуры — SPARC, ARM, x86, x86_64. Ядро WrmOS базируется на документе . Существует паравиртуализированное ядро Linux ( ) работающее поверх WrmOS.

Примечания

↑ Liedtke, Jochen (Декабрь 1993 года ). (PDF) . 14th ACM . Asheville , NC , USA . pp. 175—88. (PDF) из оригинала 4 марта 2016 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 4 марта 2016 года.
от 14 мая 2015 на Wayback Machine (англ.) // Сайт технического университета Дрездена ( Германия ).
от 12 мая 2015 на Wayback Machine (англ.) // Сайт технического университета Дрездена .
↑ Liedtke, Jochen (Декабрь 1993 года ). (PDF) . Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS) . Asheville , NC , USA . pp. 2‑11. (PDF) из оригинала 10 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 10 июля 2015 года.
↑ от 5 марта 2012 на Wayback Machine .
↑ Liedtke, Jochen (Декабрь 1995 года ). . Proc. 15th ACM (SOSP) . pp. 237‑250. Архивировано из 18 марта 2009 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 18 марта 2009 года.
↑ . .
Jochen Liedtke. от 12 ноября 2007 на Wayback Machine . Technical report 872. German national research center for computer science (GMD). Октябрь 1994 года .
Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars ( 2000 год ). . ACM SIGOPS European Workshop . Kolding , Denmark . pp. 109—114. {{ cite conference }} : Проверьте значение даты: |date= ( справка )
Fleisch, Brett D; Allan, Mark. (неопр.) . — John Wiley & Sons, Ltd.. 24 августа 2007 года.
// archive.org .
от 7 августа 2011 на Wayback Machine .
от 9 января 2007 на Wayback Machine (англ.) .
от 22 января 2007 на Wayback Machine (англ.) .
. (англ.) Белая книга . PDF . 1 мая 2003 года // archive.org .
Gray, Charles (Апрель 2005 года). . USENIX Annual Technical Conference . Annaheim , CA , USA . pp. 264‑278. из оригинала 17 февраля 2007 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) ; no-break space character в |title= на позиции 8 ( справка ) ; Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка ) . Дата обращения: 8 июля 2015. Архивировано 17 февраля 2007 года.
Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; . User-level device drivers: achieved performance (неопр.) // Journal of Computer Science and Technology. — Т. 20 , № 5 . — С. 654‑664 . — doi : .
van Schaik, Carl; (Январь 2007 года). . 1st International Workshop on Microkernels for Embedded Systems . Sydney , Australia : . pp. 11‑21. из оригинала 26 апреля 2007 . Дата обращения: 1 апреля 2007 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 26 апреля 2007 года.
Ruocco, Sergio. (англ.) // EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications : journal. — 2008. — October ( vol. 2008 ). — P. 1‑14 . — doi : . (недоступная ссылка)
от 25 августа 2006 на Wayback Machine .
программы ERTOS на сайте NICTA // archive.org .
. Дата обращения: 21 мая 2011. Архивировано из 16 мая 2011 года.
от 13 марта 2014 на Wayback Machine .
. Дата обращения: 8 июля 2015. Архивировано из 10 апреля 2015 года.
(Press release). . 2012-01-19. Архивировано из 11 февраля 2012 . Дата обращения: 10 ноября 2015 .
(Press release). . 2012-03-27. Архивировано из 2 июля 2012 .
. Дата обращения: 28 сентября 2017. 23 сентября 2014 года.
от 19 декабря 2013 на Wayback Machine .
от 15 июля 2015 на Wayback Machine .
от 3 мая 2022 на Wayback Machine .
Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock; David; Chakravarty, Manuel M. T. (Сентябрь 2006 года ). (PDF) . ACM SIGPLAN Haskell Workshop . Portland , Oregon , USA . pp. 60‑71. (PDF) из оригинала 3 марта 2016 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 3 марта 2016 года.
↑ Klein, Gerwin; Elphinstone, Kevin; ; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (Октябрь 2009 года ). (PDF) . 22nd ACM . , MT , USA . (PDF) из оригинала 28 июля 2011 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 28 июля 2011 года.
Elkaduwe, Dhammika (Апрель 2008 года ). . 1st Workshop on Isolation and Integration in Embedded Systems . Glasgow , UK . doi : . Архивировано из 24 апреля 2010 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) ; Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка ) . Дата обращения: 8 июля 2015. Архивировано из 24 апреля 2010 года.
↑ Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Comprehensive formal verification of an OS microkernel (англ.) // ACM Transactions on Computer Systems : journal. — Vol. 32 , no. 1 . — P. 2:1—2:70 . — doi : .
(Press release). . 2014-07-29. Архивировано из 10 августа 2014 . Дата обращения: 8 июля 2015 .
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. (англ.) // ACM Transactions on Computer Systems : journal. — 2014. — Vol. 32 . — P. 64 . — doi : . 3 августа 2014 года.
8 августа 2014 года. (HACMS).
от 10 июля 2015 на Wayback Machine // Сайт фирмы (англ.) ( . SMACCM — аббревиатура от англ. secure mathematically-assured composition of control models .
от 18 ноября 2015 на Wayback Machine // Журнал « Популярная механика ». 12 ноября 2015 года.
от 8 марта 2017 на Wayback Machine (англ.) .
Hallgren, T.; Jones, M. P.; Leslie, R.; Tolmach, A. (англ.) // Proceedings of the tenth ACM SIGPLAN international conference on functional programming : journal. — 2005. — Vol. 40 , no. 9 . — P. 116—128 . — ISSN . — doi : . 15 июня 2010 года.
от 9 июля 2015 на Wayback Machine на сайте genode.org.
// archive.org .
от 9 июля 2015 на Wayback Machine .
от 5 марта 2017 на Wayback Machine // github.com .
Peter, Michael; Schild, Henning (Март 2009 года ). . VTDS'09: Workshop on Virtualization Technology for Dependable Systems . Nuremberg , Germany . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) ; Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка )
от 7 июля 2015 на Wayback Machine .
Steinberg, Udo; Bernhard, Kauer (Апрель 2010 года ). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems . Paris , France . {{ cite conference }} : Проверьте значение даты: |date= ( справка )
Steinberg, Udo; Bernhard, Kauer (Апрель 2010 года ). "Towards a Scalable Multiprocessor User-level Environment". IIDS'10: Workshop on Isolation and Integration for Dependable Systems . Paris , France . {{ cite conference }} : Проверьте значение даты: |date= ( справка )
от 24 июня 2015 на Wayback Machine . Официальный сайт.
от 11 июня 2018 на Wayback Machine // github.com
от 9 февраля 2011 на Wayback Machine . Официальный сайт проекта Xameleon.

Литература

, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. . ACM Press. 1991
Liedtke, Jochen (2000-10-22). (PDF) . In Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego , CA , October 2000 . из оригинала 5 сентября 2006 . Дата обращения: 5 сентября 2006 . {{ cite conference }} : Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка ) от 5 сентября 2006 на Wayback Machine (о микроядре L4 и компиляторе).
Cheng Guanghui, Nicholas Mc Guire. , Distributed & Embedded Systems Lab — Lanzhou University .
Elphinstone, Kevin; (Октябрь 2014 года ). . 24th ACM SIGOPS Symposium on Operating Systems Principles . , PA , USA . pp. 133‑150. {{ cite conference }} : Проверьте значение даты: |date= ( справка ) от 12 августа 2014 на Wayback Machine Эволюция архитектуры L4 и подходы к реализации.

Ссылки

: L4 headquarters, сайт сообщества о реализациях L4.
. Обзор реализаций L4, документации и проектов.
.
. Реализации L4 «L4Ka::Pistachio» и «L4Ka::Hazelnut».
. Реализация L4 для процессоров DEC Alpha и процессоров архитектуры MIPS .
. Коммерческая реализация L4 от фирмы « ».
. Обзоры исследований и публикации.
. Каркас для построения операционных систем, разработка сообщества L4.

[Liedtke_93-1] Liedtke, Jochen (Декабрь 1993 года ). (PDF) . 14th ACM . Asheville , NC , USA . pp. 175—88. (PDF) из оригинала 4 марта 2016 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 4 марта 2016 года.

[dresden_overview-2] от 14 мая 2015 на Wayback Machine (англ.) // Сайт технического университета Дрездена ( Германия ).

[dresden_elan-3] от 12 мая 2015 на Wayback Machine (англ.) // Сайт технического университета Дрездена .

[Liedtke_iwooos93-4] Liedtke, Jochen (Декабрь 1993 года ). (PDF) . Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS) . Asheville , NC , USA . pp. 2‑11. (PDF) из оригинала 10 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 10 июля 2015 года.

[liedtke_mem-5] от 5 марта 2012 на Wayback Machine .

[Lie95-6] Liedtke, Jochen (Декабрь 1995 года ). . Proc. 15th ACM (SOSP) . pp. 237‑250. Архивировано из 18 марта 2009 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 18 марта 2009 года.

[liedtke_mem_2-7] . .

[8] Jochen Liedtke. от 12 ноября 2007 на Wayback Machine . Technical report 872. German national research center for computer science (GMD). Октябрь 1994 года .

[Gefflaut_JPLEUTDR_00-9] Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars ( 2000 год ). . ACM SIGOPS European Workshop . Kolding , Denmark . pp. 109—114. {{ cite conference }} : Проверьте значение даты: |date= ( справка )

[WorkplaceMicrokernelandOS-10] Fleisch, Brett D; Allan, Mark. (неопр.) . — John Wiley & Sons, Ltd.. 24 августа 2007 года.

[11] // archive.org .

[12] от 7 августа 2011 на Wayback Machine .

[13] от 9 января 2007 на Wayback Machine (англ.) .

[14] от 22 января 2007 на Wayback Machine (англ.) .

[15] . (англ.) Белая книга . PDF . 1 мая 2003 года // archive.org .

[Gray_CCMH_05-16] Gray, Charles (Апрель 2005 года). . USENIX Annual Technical Conference . Annaheim , CA , USA . pp. 264‑278. из оригинала 17 февраля 2007 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) ; no-break space character в |title= на позиции 8 ( справка ) ; Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка ) . Дата обращения: 8 июля 2015. Архивировано 17 февраля 2007 года.

[Leslie_CFGGMPSEH_05-17] Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; . User-level device drivers: achieved performance (неопр.) // Journal of Computer Science and Technology. — Т. 20 , № 5 . — С. 654‑664 . — doi : .

[vanSchaik_Heiser_07-18] van Schaik, Carl; (Январь 2007 года). . 1st International Workshop on Microkernels for Embedded Systems . Sydney , Australia : . pp. 11‑21. из оригинала 26 апреля 2007 . Дата обращения: 1 апреля 2007 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 26 апреля 2007 года.

[Ruocco_08-19] Ruocco, Sergio. (англ.) // EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications : journal. — 2008. — October ( vol. 2008 ). — P. 1‑14 . — doi : . (недоступная ссылка)

[20] от 25 августа 2006 на Wayback Machine .

[21] программы ERTOS на сайте NICTA // archive.org .

[22] . Дата обращения: 21 мая 2011. Архивировано из 16 мая 2011 года.

[23] от 13 марта 2014 на Wayback Machine .

[24] . Дата обращения: 8 июля 2015. Архивировано из 10 апреля 2015 года.

[OKL_PR-25] (Press release). . 2012-01-19. Архивировано из 11 февраля 2012 . Дата обращения: 10 ноября 2015 .

[OKL_PR_auto-26] (Press release). . 2012-03-27. Архивировано из 2 июля 2012 .

[27] . Дата обращения: 28 сентября 2017. 23 сентября 2014 года.

[28] от 19 декабря 2013 на Wayback Machine .

[29] от 15 июля 2015 на Wayback Machine .

[30] от 3 мая 2022 на Wayback Machine .

[Derrin_EKCC_06-31] Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock; David; Chakravarty, Manuel M. T. (Сентябрь 2006 года ). (PDF) . ACM SIGPLAN Haskell Workshop . Portland , Oregon , USA . pp. 60‑71. (PDF) из оригинала 3 марта 2016 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 3 марта 2016 года.

[Klein_EHACDEEKNSTW_09-32] Klein, Gerwin; Elphinstone, Kevin; ; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (Октябрь 2009 года ). (PDF) . 22nd ACM . , MT , USA . (PDF) из оригинала 28 июля 2011 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) . Дата обращения: 8 июля 2015. Архивировано 28 июля 2011 года.

[Elkaduwe_DE_08-33] Elkaduwe, Dhammika (Апрель 2008 года ). . 1st Workshop on Isolation and Integration in Embedded Systems . Glasgow , UK . doi : . Архивировано из 24 апреля 2010 . Дата обращения: 8 июля 2015 . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) ; Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка ) . Дата обращения: 8 июля 2015. Архивировано из 24 апреля 2010 года.

[Klein_AEMSKH_14-34] Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Comprehensive formal verification of an OS microkernel (англ.) // ACM Transactions on Computer Systems : journal. — Vol. 32 , no. 1 . — P. 2:1—2:70 . — doi : .

[seL4_OSS-35] (Press release). . 2014-07-29. Архивировано из 10 августа 2014 . Дата обращения: 8 июля 2015 .

[36] Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. (англ.) // ACM Transactions on Computer Systems : journal. — 2014. — Vol. 32 . — P. 64 . — doi : . 3 августа 2014 года.

[37] 8 августа 2014 года. (HACMS).

[38] от 10 июля 2015 на Wayback Machine // Сайт фирмы (англ.) ( . SMACCM — аббревиатура от англ. secure mathematically-assured composition of control models .

[39] от 18 ноября 2015 на Wayback Machine // Журнал « Популярная механика ». 12 ноября 2015 года.

[40] от 8 марта 2017 на Wayback Machine (англ.) .

[41] Hallgren, T.; Jones, M. P.; Leslie, R.; Tolmach, A. (англ.) // Proceedings of the tenth ACM SIGPLAN international conference on functional programming : journal. — 2005. — Vol. 40 , no. 9 . — P. 116—128 . — ISSN . — doi : . 15 июня 2010 года.

[42] от 9 июля 2015 на Wayback Machine на сайте genode.org.

[43] // archive.org .

[44] от 9 июля 2015 на Wayback Machine .

[45] от 5 марта 2017 на Wayback Machine // github.com .

[Peter_Schild_VTDS_09-46] Peter, Michael; Schild, Henning (Март 2009 года ). . VTDS'09: Workshop on Virtualization Technology for Dependable Systems . Nuremberg , Germany . {{ cite conference }} : Проверьте значение даты: |date= ( справка ) ; Неизвестный параметр |coauthors= игнорируется ( |author= предлагается) ( справка )

[47] от 7 июля 2015 на Wayback Machine .

[Steinberg_Kauer_EuroSys_2010-48] Steinberg, Udo; Bernhard, Kauer (Апрель 2010 года ). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems . Paris , France . {{ cite conference }} : Проверьте значение даты: |date= ( справка )

[Steinberg_Kauer_IIDS_2010-49] Steinberg, Udo; Bernhard, Kauer (Апрель 2010 года ). "Towards a Scalable Multiprocessor User-level Environment". IIDS'10: Workshop on Isolation and Integration for Dependable Systems . Paris , France . {{ cite conference }} : Проверьте значение даты: |date= ( справка )

[50] от 24 июня 2015 на Wayback Machine . Официальный сайт.

[51] от 11 июня 2018 на Wayback Machine // github.com

[52] от 9 февраля 2011 на Wayback Machine . Официальный сайт проекта Xameleon.