L4 (микроядро)

Материал из Википедии — свободной энциклопедии
Это старая версия этой страницы, сохранённая IRedRat (обсуждение | вклад) в 10:49, 25 августа 2015. Она может серьёзно отличаться от текущей версии.
Перейти к навигации Перейти к поиску
У этого термина существуют и другие значения, см. L4.
L4
Скриншот программы L4
Семейство микроядер L4
Тип Микроядро
Автор Йохен Лидтке
Разработчик Йохен Лидтке
Написана на язык ассемблера
Сайт l4hq.org

L4 — микроядро второго поколения, разработанное Йохеном Лидтке (нем. Jochen Liedtke (англ.); немецкий информатик; 1953‑2001) в 1993 году[1].

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

Семейство микроядер L4

История

L1

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

L2

Основная статья: операционная система Eumel (англ.)

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

8‑битовый микроконтроллеры стали широко доступными. Требовалась операционная система, способная работать на небольших рабочих станциях в средних школах и вузах. ОС CP/M не подходила. Исследовательский центр GMD (англ. German National Research Center for Computer Science) и университет города Билефельд решили разработать новую операционную систему с нуля[4].

В 1979 году Лидтке начал разработку новой операционной системы и назвал её «Eumel» (англ.) от англ. extendable multiuser microprocessor ELAN-system. ОС «Eumel» также называлась «L2», что означает — «2‑я работа Liedtke». Новая ОС поддерживала 8-битовые процессоры Zilog Z80, была многопользовательской и многозадачной, была построена на основе микроядра, поддерживала orthogonal persistence (англ.). Поддержка «orthogonal persistence» заключалась в следующем: ОС периодически сохраняла на диск своё состояние (содержимое памяти, регистров процессора и др.); после перебоев в подаче электроэнергии ОС восстанавливалась из сохранённого состояния; программы продолжали работать так, будто бы сбоя не происходило; терялись только изменения, внесённые с момента последнего сохранения. ОС Eumel проектировалась под влиянием ОС Multics и содержала много общего с ядрами Accent (англ.) и Mach[4].

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

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

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

L3

Основная статья: микроядро L3 (англ.)

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

В 1984 году[5] Лидтке (нем. Jochen Liedtke (англ.)) перешёл на работу в исследовательский центр GMD (англ. German National Research Center for Computer Science) для создания ОС, аналогичной ОС Eumel, но работающей без эмуляции. В настоящее время GMD сходит в состав организации «Общество Фраунгофера» (нем. de:GMD-Forschungszentrum Informationstechnik (нем.)).

С 1987 года[4] Лидтке и его команда из института SET (англ. institute for system design technology), входящем в состав GMD, приступили к разработке нового микроядра, получившего название «L3» («L3» от «3‑я работа Liedtke»).

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

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

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

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

  • в школах (заменила свою предшественницу — ОС Eumel)[4];
  • фирмой «TÜV SÜD» (Германия)[источник не указан 5233 дня];
  • на примерно 3000 компьютерах, установленных в юридических фирмах Германии[5].

См. также: официальная страница, посвящённая микроядру L3, на сайте технического университета Дрездена.

L4

Во время работы над микроядром L3 Йохеном Лидтке (нем. Jochen Liedtke (англ.)) обнаружил недостатки микроядра Mach. Желая повысить производительность, Лидтке стал составлять код нового микроядра на языке ассемблера с использованием особенностей архитектуры процессоров Intel i386.

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

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

Некоторые компоненты микроядра Mach были возвращены назад — внутрь микроядра[источник не указан 5248 дней]. Это нарушало саму идею микроядер (минимальный размер, изоляция компонентов), но позволило увеличить производительность ОС.

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

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

В 1996 году Лидтке защитил диссертацию в техническом университете Берлина по теме «guarded page tables»[7] и получил степень PhD[8].

С 1996 года Лидтке работал в исследовательском центре имени Томаса Уотсона (англ. Thomas J. Watson research center — подразделении фирмы «IBM Research» (англ. IBM Research). Лидтке с коллегами продолжил исследования микроядра L4, микроядер вообще и операционной системы «Sawmill OS» в частности[9]. Из-за отсутствия коммерческого успеха у ОС IBM Workplace OS (англ.), построенной на третьей версии микроядра Mach от CMU и разрабатываемой IBM с января 1991 года по 1996 год[10], вместо понятия «микроядро L4» использовалось понятие «Lava Nucleus» или, кратко, «LN».

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

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

L4Ka::Hazelnut

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

Желая доказать возможность реализации микроядра на высокоуровневом языке, группа SAG разработала микроядро «L4Ka::Hazelnut». Работа велась в технологическом институте Карлсруэ при поддержке DFG (нем. Deutsche Forschungsgemeinschaft, англ. German research foundation)[11]. Реализация была написана на языке C++ и поддерживала процессоры архитектур IA-32 и ARM. Производительность нового микроядра оказалась приемлемой (англ. acceptable), и разработка ядер на языке ассемблера была прекращена.

L4/Fiasco

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

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

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

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

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

L4Ka::Pistachio

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В августе 2006 года Gernot Heiser (англ. Gernot Heiser) основал фирму «Open Kernel Labs» (англ.; кратко, OK Labs). Тогда Gernot Heiser занимал должность руководителя программы ERTOS (англ. embedded real time operating systems, ERTOS), организованной фирмой «NICTA»[21], и был процессором в университете UNSW. Фирма «OK Labs» создавалась для

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

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

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

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

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

Реализация L4 также использовалась в автомобильных развлекательных системам (англ. automotive infotainment systems)[26].

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

Верификация

seL4

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

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

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

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

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

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

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

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

В августе 2012 года фирмы «NICTA» (англ.), «Rockwell Collins» (англ.), «Galois Inc» (англ.), «Boeing» и университет Миннесоты в рамках программы «High-assurance cyber military systems» (HACMS)[37], организованной агентством DARPA, приступили к разработке беспилотного летательного аппарата[38]. Основное требование к разработке — обеспечение высокой надёжности аппарата. У каждой из перечисленных фирм была своя роль в программе. Фирма «NICTA» была ответственна за разработку ОС и построила её на основе микроядра «seL4». Ответственные задачи были реализованы в виде компонентов микроядра, а не ответственные — запускались под паравиртуализированной ОС Linux. Наработки программы планировалось использовать в вертолёте «Unmanned Little Bird», разработкой которого занималась фирма «Boeing». Вертолёт должен был поддерживать как управление пилотом, так и беспилотный режим.

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

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

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

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

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

«Fiasco.OC» — микроядро третьего поколения, созданное на основе микроядра «L4/Fiasco». Реализует механизм capability-based security, поддерживает многоядерные процессоры и аппаратную виртуализацию[45]. «L4 Runtime Environment» (кратко, «L4Re») — каркас, работающий поверх микроядра «Fiasco.OC» и предназначенный для создания компонентов в пространстве пользователя. «L4Re» предоставляет функционал для создания клиент-серверных приложений, реализации файловых систем, реализует популярные библиотеки, например, стандартную библиотеку языка C (libc), стандартную библиотеку языка C++ (libstdc++) и библиотеку pthreads. «L4Linux» — подсистема для запуска ОС Linux поверх микроядра «Fiasco.OC» с помощью паравиртуализации[46]. Каркас «L4Re» и микроядро «Fiasco.OC» поддерживали процессоры архитектуры x86 (IA-32 и AMD64), ARM и PowerPC (WiP). Ранее вместо пары «Fiasco.OC» - «L4Re» использовалась пара «L4/Fiasco» - «L4Env».

«NOVA» (англ. the NOVA OS virtualization architecture) — исследовательский проект, созданный с целью создания безопасного и эффективного окружения для виртуализации[47][48][49] с небольшим списком доверенного ПО (англ. trusted computing base). В состав «NOVA» входят:

  • микроядро, реализующее L4 и гипервизор первого порядка (англ. baremetal hypervisor);
  • VMM (англ. virtual-machine monitor) под названием «Vancouver» — компонент микроядра (процесс), работающий в пространстве пользователя, занимающийся обслуживанием (эмуляцией оборудования) одной виртуальной машины и лишённый привилегий. На каждую виртуальную машину запускалось по одному VMM. VMM «Vancouver» входит в состав «NUL» и может быть заменён на VMM «Seoul». VMM «Seoul»[50] создан на основе VMM «Vancouver»;
  • «NUL» (англ. NOVA user-level environment) — некоторые компоненты микроядра, работающие в пространстве пользователя (VMM «Vancouver», драйверы устройств (например, сетевой карты); partition manager; компоненты, предназначенные для управления памятью, вводом-выводом; компоненты, реализующие стеки TCP/IP, USB и др.). «NUL» может быть заменён на genode или «NRE». «NRE» (англ. NOVA runtime environment) — потомок «NUL».

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

«Xameleon» — проект по реализации ОС на микроядре L4[51]. Проект основал в 2001 году единственный разработчик Алексей Мандрыкин (род. 19 января 1973 года). Изначально ОС была построена поверх микроядра «L4/Fiasco». Позднее автор перевёл ОС на микроядро «L4Ka::Pistachio». Исходный код ОС закрыт.

Список литературы

  • Jochen Liedtke, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. Two years of experience with a μ-Kernel based OS. ACM Press. 1991
  • Liedtke, Jochen (2000-10-22). "Stub-Code Performance is Becoming Important" (PDF). In Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego, CA, October 2000. Дата обращения: 5 сентября 2006. {{cite conference}}: Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка) (о микроядре L4 и компиляторе).
  • Cheng Guanghui, Nicholas Mc Guire. L4/Fiasco/L4Linux Kickstart, Distributed & Embedded Systems Lab - Lanzhou University.
  • Elphinstone, Kevin; Heiser, Gernot (Октябрь 2014 года). "From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?". 24th ACM SIGOPS Symposium on Operating Systems Principles. Farmington, PA, USA. pp. 133‑150. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка) Эволюция архитектуры L4 и подходы к реализации.

Ссылки

Примечания

  1. ↑ 1 2 Liedtke, Jochen (Декабрь 1993 года). "Improving IPC by kernel design" (PDF). 14th ACM symposium on operating system principles. Asheville, NC, USA. pp. 175—88. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  2. ↑ Семейство микроядер L4. Обзор (англ.) // Сайт технического университета Дрездена (Германия).
  3. ↑ Язык ELAN (англ.) // Сайт технического университета Дрездена.
  4. ↑ 1 2 3 4 5 6 7 8 9 10 Liedtke, Jochen (Декабрь 1993 года). "A persistent system in real use—experiences of the first 13 years" (PDF). Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS). Asheville, NC, USA. pp. 2‑11. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  5. ↑ 1 2 In Memoriam Jochen Liedtke (1953 - 2001).
  6. ↑ 1 2 Liedtke, Jochen (Декабрь 1995 года). "On µ-Kernel construction". Proc. 15th ACM symposium on operating systems principles (SOSP). pp. 237‑250. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка); Проверьте значение |authorlink= (справка)
  7. ↑ Jochen Liedtke. Page table structures for fine-grain virtual memory. Technical report 872. German national research center for computer science (GMD). Октябрь 1994 года.
  8. ↑ 1 2 3 System architecture group. About us. People. Liedtke. Архивная копия.
  9. ↑ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000 год). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109–114. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  10. ↑ Fleisch, Brett D; Allan, Mark (23 сентября 1997 года). "Workplace Microkernel and OS: A Case Study". John Wiley & Sons, Ltd. Архивировано 24 августа 2007. Дата обращения: 25 марта 2013. {{cite journal}}: Проверьте значение даты: |date= and |archivedate= (справка); Cite journal требует |journal= (справка)
  11. ↑ Страница группы «L4Ka» // archive.org.
  12. ↑ Drops overview.
  13. ↑ Микроядро «L4Ka::Pistachio» (англ.).
  14. ↑ Команда разработчиков «L4Ka» (англ.).
  15. ↑ Микроядро «L4Ka::Pistachio». Белая книга. PDF. 1 мая 2003 года // archive.org.
  16. ↑ Gray, Charles (Апрель 2005 года). "Itanium — system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264‑278. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка)
  17. ↑ Leslie, Ben (Сентябрь 2005 года). "User-level device drivers: achieved performance". Journal of Computer Science and Technology. 20 (5): 654‑664. doi:10.1007/s11390-005-0654-4. {{cite journal}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка)
  18. ↑ van Schaik, Carl; Heiser, Gernot (Январь 2007 года). "High-performance microkernels and virtualisation on ARM and segmented architectures". 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11‑21. Дата обращения: 1 апреля 2007. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  19. ↑ Ruocco, Sergio (Октябрь 2008 года). "A real-time programmer's tour of general-purpose L4 microkernels". EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications. 2008: 1‑14. doi:10.1155/2008/234710. {{cite journal}}: Проверьте значение даты: |date= (справка); Шаблон цитирования имеет пустые неизвестные параметры: |laysource=, |laydate=, and |laysummary= (справка)Википедия:Обслуживание CS1 (не помеченный открытым DOI) (ссылка)
  20. ↑ [1].
  21. ↑ Страница программы ERTOS на сайте NICTA // archive.org.
  22. ↑ OKL4 3.0
  23. ↑ OKL4 microvisor.
  24. ↑ OK:Linux
  25. ↑ Ошибка в сносках?: Неверный тег <ref>; для сносок OKL_PR не указан текст
  26. ↑ "Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 27 марта 2012 года. {{cite press release}}: Проверьте значение даты: |date= (справка)
  27. ↑ iOS Security.
  28. ↑ Darbat project.
  29. ↑ [2].
  30. ↑ [3].
  31. ↑ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock; David; Chakravarty, Manuel M. T. (Сентябрь 2006 года). "Running the manual: an approach to high-assurance microkernel development" (PDF). ACM SIGPLAN Haskell Workshop. Portland, Oregon, USA. pp. 60‑71. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  32. ↑ 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (Октябрь 2009 года). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM symposium on operating system principles. Big Sky, MT, USA. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  33. ↑ Elkaduwe, Dhammika (Апрель 2008 года). "Kernel design for isolation and assurance of physical memory". 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка)
  34. ↑ 1 2 Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (Февраль 2014 года). "Comprehensive formal verification of an OS microkernel". ACM Transactions on Computer Systems. 32 (1): 2:1-2:70. doi:10.1145/2560537. {{cite journal}}: Проверьте значение даты: |date= (справка)
  35. ↑ "Secure operating system developed by NICTA goes open source" (Press release). NICTA. 29 июля 2014 года. {{cite press release}}: Проверьте значение даты: |date= (справка)
  36. ↑ Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. doi:10.1145/2560537.
  37. ↑ High-assurance cyber military systems (HACMS).
  38. ↑ Проект «SMACCM» // Сайт фирмы «NICTA». SMACCM — аббревиатура от англ. secure mathematically-assured composition of control models.
  39. ↑ История GNU Hurd. Портирование на другое микроядро (англ.).
  40. ↑ Hallgren, T.; Jones, M. P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). Proceedings of the tenth ACM SIGPLAN international conference on functional programming. 40 (9): 116—128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Дата обращения: 24 июня 2010.
  41. ↑ Codezero на сайте genode.org.
  42. ↑ dev.b-labs.com // archive.org.
  43. ↑ Официальный сайт проекта «Codezero».
  44. ↑ Репозиторий проекта «F9» // github.com.
  45. ↑ Peter, Michael; Schild, Henning (Март 2009 года). "Virtual Machines Jailed - Virtualization in Systems with Small Trusted Computing Bases". VTDS'09: Workshop on Virtualization Technology for Dependable Systems. Nuremberg, Germany. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка)
  46. ↑ L4Linux.
  47. ↑ 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= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  48. ↑ 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= (справка); Неизвестный параметр |booktitle= игнорируется (|book-title= предлагается) (справка)
  49. ↑ Проект «Nova». Официальный сайт.
  50. ↑ VMM «Seoul» // github.com
  51. ↑ l4os.ru. Официальный сайт проекта «Xameleon».
Источник — https://ru.wikipedia.org/ruwiki/w/index.php?title=L4_(микроядро)&oldid=72944049