L4 (микроядро): различия между версиями

L4
L4
	; Семейство микроядер L4
Тип	Микроядро
Автор	Йохен Лидтке
Разработчик	Йохен Лидтке
Написана на	язык ассемблера
Сайт	l4hq.org

Интерактивная навигация по истории

[отпатрулированная версия]

← Предыдущая правка

Содержимое удалено Содержимое добавлено

ВизуальныйВики-текст

Линейный

Текущая версия от 07:33, 26 января 2024

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

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

История

L1

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

L2

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

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

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

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

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

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

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

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

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

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

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

L4

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

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

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

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

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

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

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

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

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

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

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

Желая доказать возможность реализации микроядра на высокоуровневом языке, группа SAG разработала микроядро «L4Ka::Hazelnut». Работа велась в технологическом институте Карлсруэ при поддержке DFG^[11]. Реализация была написана на языке 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»^[12] — ОС «жёсткого» реального времени (когда крайне важно, чтобы на событие реагировали в строго установленные сроки), также разработанной в техническом университете Дрездена.

Ввиду усложнения архитектуры микроядра в поздних версиях ОС «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»^[13]^[14]. Код составлялся с нуля на языке C++, использовался опыт проекта L4Ka::Hazelnut. Внимание уделялось высокой производительности и переносимости.

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

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

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

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

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

Исключение IPC позволило ядру передавать обработку исключений процессора в пространство пользователя.
Добавление Alien thread^[англ.] (потока, выполняемого одним ядром процессора от имени процесса, запущенного на другом ядре процессора) позволило реализовать детальное управление системными вызовами.
Добавление 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)^[16].

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

Она разработала компоненты для паравиртуализации ядер 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 системные вызовы были сделаны настолько «короткими», что не требовали точек вытесняющей многозадачности и позволяли реализовать ОС реального времени^[19].

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

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

В августе 2006 года Г. Хейсер^[англ.] основал фирму Open Kernel Labs. Тогда Хейсер занимал должность руководителя программы 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]. Большинство из этих устройств содержало микросхемы, реализующие беспроводные модемы и было выпущено фирмой «Qualcomm».

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

ОС, построенная на основе реализации L4, исполнялась процессором secure enclave, входящим в состав размещённой на кристалле электронной схемы 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]. Существование доказательства гарантировало соответствие реализации и спецификации, подтверждало отсутствие в реализации некоторых ошибок (например, отсутствие взаимных блокировок, livelocks, переполнений буферов, арифметических исключений и случаев использования неинициализированных переменных). Микроядро seL4 было первым микроядром, предназначенным для ОС общего назначения и прошедшим верификацию^[32].

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

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

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

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

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

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

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

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

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

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

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

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

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

Fiasco.OC — микроядро третьего поколения, созданное на основе микроядра «L4/Fiasco». Реализует механизм Capability-based security^[англ.], поддерживает многоядерные процессоры и аппаратную виртуализацию^[46].

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» с помощью паравиртуализации^[47]. Ранее вместо пары «Fiasco.OC» — L4Re использовалась пара «L4/Fiasco» — L4Env.

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

микроядро, реализующее L4 и гипервизор первого порядка (англ. baremetal hypervisor);
VMM Vancouver — компонент микроядра (процесс), работающий в пространстве пользователя, занимающийся обслуживанием (эмуляцией оборудования) одной виртуальной машины и лишённый привилегий. На каждую виртуальную машину запускалось по одному VMM. VMM Vancouver входит в состав NUL и может быть заменён на VMM Seoul. VMM Seoul^[51] создан на основе 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^[52]. Проект основал в 2001 году единственный разработчик Алексей Мандрыкин (род. 19 января 1973 года). Изначально ОС была построена поверх микроядра «L4/Fiasco». Позднее автор перевёл ОС на микроядро «L4Ka::Pistachio». Исходный код ОС закрыт.

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

Примечания

↑ ¹ ² Liedtke, Jochen (Декабрь 1993 года). "Improving IPC by kernel design" (PDF). 14th ACM symposium on operating system principles. Asheville, NC, USA. pp. 175—88. Архивировано (PDF) 4 марта 2016. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 4 марта 2016 года.
↑ Семейство микроядер L4. Обзор Архивная копия от 14 мая 2015 на Wayback Machine (англ.) // Сайт технического университета Дрездена (Германия).
↑ Язык ELAN Архивная копия от 12 мая 2015 на Wayback Machine (англ.) // Сайт технического университета Дрездена.
↑ ¹ ² ³ ⁴ ⁵ ⁶ ⁷ ⁸ ⁹ ¹⁰ 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. Архивировано (PDF) 10 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 10 июля 2015 года.
↑ ¹ ² In Memoriam Jochen Liedtke (1953—2001) Архивная копия от 5 марта 2012 на Wayback Machine.
↑ ¹ ² Liedtke, Jochen (Декабрь 1995 года). "On µ-Kernel construction". Proc. 15th ACM symposium on operating systems principles (SOSP). pp. 237‑250. Архивировано из оригинала 18 марта 2009. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 18 марта 2009 года.
↑ ¹ ² ³ System architecture group. About us. People. Liedtke. Архивная копия.
↑ Jochen Liedtke. Page table structures for fine-grain virtual memory Архивная копия от 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 год). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109—114. {{cite conference}}: Проверьте значение даты: |date= (справка)
↑ Fleisch, Brett D; Allan, Mark. Workplace Microkernel and OS: A Case Study (неопр.). — John Wiley & Sons, Ltd.. Архивировано 24 августа 2007 года.
↑ Страница группы «L4Ka» // archive.org.
↑ Drops overview Архивная копия от 7 августа 2011 на Wayback Machine.
↑ Микроядро «L4Ka::Pistachio» Архивная копия от 9 января 2007 на Wayback Machine (англ.).
↑ Команда разработчиков «L4Ka» Архивная копия от 22 января 2007 на Wayback Machine (англ.).
↑ The L4Ka::Pistachio Microkernel. (англ.) Белая книга. PDF. 1 мая 2003 года // archive.org.
↑ Gray, Charles (Апрель 2005 года). "Itanium — system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264‑278. Архивировано 17 февраля 2007. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |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; Heiser, Gernot. User-level device drivers: achieved performance (неопр.) // Journal of Computer Science and Technology. — Т. 20, № 5. — С. 654‑664. — doi:10.1007/s11390-005-0654-4.
↑ 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. Архивировано 26 апреля 2007. Дата обращения: 1 апреля 2007. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 26 апреля 2007 года.
↑ Ruocco, Sergio. 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 : journal. — 2008. — October (vol. 2008). — P. 1‑14. — doi:10.1155/2008/234710. (недоступная ссылка)
↑ [1] Архивная копия от 25 августа 2006 на Wayback Machine.
↑ Страница программы ERTOS на сайте NICTA // archive.org.
↑ OKL4 3.0 (неопр.). Дата обращения: 21 мая 2011. Архивировано из оригинала 16 мая 2011 года.
↑ OKL4 microvisor Архивная копия от 13 марта 2014 на Wayback Machine.
↑ OK:Linux (неопр.). Дата обращения: 8 июля 2015. Архивировано из оригинала 10 апреля 2015 года.
↑ "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 2012-01-19. Архивировано из оригинала 11 февраля 2012. Дата обращения: 10 ноября 2015.
↑ "Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 2012-03-27. Архивировано из оригинала 2 июля 2012.
↑ iOS Security (неопр.). Дата обращения: 28 сентября 2017. Архивировано 23 сентября 2014 года.
↑ Darbat project Архивная копия от 19 декабря 2013 на Wayback Machine.
↑ [2] Архивная копия от 15 июля 2015 на Wayback Machine.
↑ [3] Архивная копия от 3 мая 2022 на Wayback Machine.
↑ 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. Архивировано (PDF) 3 марта 2016. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 3 марта 2016 года.
↑ ¹ ² 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. Архивировано (PDF) 28 июля 2011. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 28 июля 2011 года.
↑ 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. Архивировано из оригинала 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:10.1145/2560537.
↑ "Secure operating system developed by NICTA goes open source" (Press release). NICTA. 2014-07-29. Архивировано из оригинала 10 августа 2014. Дата обращения: 8 июля 2015.
↑ 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. — 2014. — Vol. 32. — P. 64. — doi:10.1145/2560537. Архивировано 3 августа 2014 года.
↑ High-assurance cyber military systems Архивировано 8 августа 2014 года. (HACMS).
↑ Проект SMACCM Архивная копия от 10 июля 2015 на Wayback Machine // Сайт фирмы NICTA^[англ.]. SMACCM — аббревиатура от англ. secure mathematically-assured composition of control models.
↑ Дронов нового поколения взломать невозможно Архивная копия от 18 ноября 2015 на Wayback Machine // Журнал «Популярная механика». 12 ноября 2015 года.
↑ История GNU Hurd. Портирование на другое микроядро Архивная копия от 8 марта 2017 на Wayback Machine (англ.).
↑ Hallgren, T.; Jones, M. P.; Leslie, R.; Tolmach, A. A principled approach to operating system construction in Haskell (англ.) // Proceedings of the tenth ACM SIGPLAN international conference on functional programming : journal. — 2005. — Vol. 40, no. 9. — P. 116—128. — ISSN 0362-1340. — doi:10.1145/1090189.1086380. Архивировано 15 июня 2010 года.
↑ Codezero Архивная копия от 9 июля 2015 на Wayback Machine на сайте genode.org.
↑ dev.b-labs.com // archive.org.
↑ Официальный сайт проекта Codezero Архивная копия от 9 июля 2015 на Wayback Machine.
↑ Репозиторий проекта F9 Архивная копия от 5 марта 2017 на Wayback Machine // github.com.
↑ 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= (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка)
↑ L4Linux Архивная копия от 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= (справка)
↑ Проект Nova Архивная копия от 24 июня 2015 на Wayback Machine. Официальный сайт.
↑ VMM Seoul Архивная копия от 11 июня 2018 на Wayback Machine // github.com
↑ l4os.ru Архивная копия от 9 февраля 2011 на Wayback Machine. Официальный сайт проекта Xameleon.

Литература

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. Дата обращения: 5 сентября 2006. {{cite conference}}: Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка) Архивная копия от 5 сентября 2006 на Wayback Machine (о микроядре 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= (справка) Архивная копия от 12 августа 2014 на Wayback Machine Эволюция архитектуры L4 и подходы к реализации.

Ссылки

L4Hq: L4 headquarters, сайт сообщества о реализациях L4.
Семейство микроядер L4. Обзор реализаций L4, документации и проектов.
Официальная вики проекта TUD:OS.
L4Ka. Реализации L4 «L4Ka::Pistachio» и «L4Ka::Hazelnut».
UNSW. Реализация L4 для процессоров DEC Alpha и процессоров архитектуры MIPS.
OKL4. Коммерческая реализация L4 от фирмы «Open Kernel Labs».
Реализация L4 от фирмы «NICTA». Обзоры исследований и публикации.
Genode Operating System Framework. Каркас для построения операционных систем, разработка сообщества L4.
Официальная страница, посвящённая ядру L3
Микроядро L4 как основа ядра ОС

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

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

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

[Liedtke_iwooos93-4] ¹ ² ³ ⁴ ⁵ ⁶ ⁷ ⁸ ⁹ ¹⁰ 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. Архивировано (PDF) 10 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 10 июля 2015 года.

[liedtke_mem-5] ¹ ² In Memoriam Jochen Liedtke (1953—2001) Архивная копия от 5 марта 2012 на Wayback Machine.

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

[liedtke_mem_2-7] ¹ ² ³ System architecture group. About us. People. Liedtke. Архивная копия.

[8] Jochen Liedtke. Page table structures for fine-grain virtual memory Архивная копия от 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 год). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109—114. {{cite conference}}: Проверьте значение даты: |date= (справка)

[WorkplaceMicrokernelandOS-10] Fleisch, Brett D; Allan, Mark. Workplace Microkernel and OS: A Case Study (неопр.). — John Wiley & Sons, Ltd.. Архивировано 24 августа 2007 года.

[11] Страница группы «L4Ka» // archive.org.

[12] Drops overview Архивная копия от 7 августа 2011 на Wayback Machine.

[13] Микроядро «L4Ka::Pistachio» Архивная копия от 9 января 2007 на Wayback Machine (англ.).

[14] Команда разработчиков «L4Ka» Архивная копия от 22 января 2007 на Wayback Machine (англ.).

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

[Gray_CCMH_05-16] Gray, Charles (Апрель 2005 года). "Itanium — system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264‑278. Архивировано 17 февраля 2007. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка); Неизвестный параметр |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; Heiser, Gernot. User-level device drivers: achieved performance (неопр.) // Journal of Computer Science and Technology. — Т. 20, № 5. — С. 654‑664. — doi:10.1007/s11390-005-0654-4.

[vanSchaik_Heiser_07-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. Архивировано 26 апреля 2007. Дата обращения: 1 апреля 2007. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 26 апреля 2007 года.

[Ruocco_08-19] Ruocco, Sergio. 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 : journal. — 2008. — October (vol. 2008). — P. 1‑14. — doi:10.1155/2008/234710. (недоступная ссылка)

[20] [1] Архивная копия от 25 августа 2006 на Wayback Machine.

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

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

[23] OKL4 microvisor Архивная копия от 13 марта 2014 на Wayback Machine.

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

[OKL_PR-25] "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 2012-01-19. Архивировано из оригинала 11 февраля 2012. Дата обращения: 10 ноября 2015.

[OKL_PR_auto-26] "Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 2012-03-27. Архивировано из оригинала 2 июля 2012.

[27] OS Security (неопр.). Дата обращения: 28 сентября 2017. Архивировано 23 сентября 2014 года.

[28] Darbat project Архивная копия от 19 декабря 2013 на Wayback Machine.

[29] [2] Архивная копия от 15 июля 2015 на Wayback Machine.

[30] [3] Архивная копия от 3 мая 2022 на Wayback Machine.

[Derrin_EKCC_06-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. Архивировано (PDF) 3 марта 2016. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 3 марта 2016 года.

[Klein_EHACDEEKNSTW_09-32] ¹ ² 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. Архивировано (PDF) 28 июля 2011. Дата обращения: 8 июля 2015. {{cite conference}}: Проверьте значение даты: |date= (справка) Источник (неопр.). Дата обращения: 8 июля 2015. Архивировано 28 июля 2011 года.

[Elkaduwe_DE_08-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. Архивировано из оригинала 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:10.1145/2560537.

[seL4_OSS-35] "Secure operating system developed by NICTA goes open source" (Press release). NICTA. 2014-07-29. Архивировано из оригинала 10 августа 2014. Дата обращения: 8 июля 2015.

[36] 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. — 2014. — Vol. 32. — P. 64. — doi:10.1145/2560537. Архивировано 3 августа 2014 года.

[37] High-assurance cyber military systems Архивировано 8 августа 2014 года. (HACMS).

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

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

[40] История GNU Hurd. Портирование на другое микроядро Архивная копия от 8 марта 2017 на Wayback Machine (англ.).

[41] Hallgren, T.; Jones, M. P.; Leslie, R.; Tolmach, A. A principled approach to operating system construction in Haskell (англ.) // Proceedings of the tenth ACM SIGPLAN international conference on functional programming : journal. — 2005. — Vol. 40, no. 9. — P. 116—128. — ISSN 0362-1340. — doi:10.1145/1090189.1086380. Архивировано 15 июня 2010 года.

[42] Codezero Архивная копия от 9 июля 2015 на Wayback Machine на сайте genode.org.

[43] v.b-labs.com // archive.org.

[44] Официальный сайт проекта Codezero Архивная копия от 9 июля 2015 на Wayback Machine.

[45] Репозиторий проекта F9 Архивная копия от 5 марта 2017 на Wayback Machine // github.com.

[Peter_Schild_VTDS_09-46] 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= (справка); Неизвестный параметр |coauthors= игнорируется (|author= предлагается) (справка)

[47] L4Linux Архивная копия от 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] Проект Nova Архивная копия от 24 июня 2015 на Wayback Machine. Официальный сайт.

[51] VMM Seoul Архивная копия от 11 июня 2018 на Wayback Machine // github.com

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

[40]

[41]

[42]

[43]

[44]

[45]

[46]

[47]

[48]

[49]

[50]

[51]

[52]

L4 (микроядро): различия между версиями

Текущая версия от 07:33, 26 января 2024

Содержание

История

L1

L2

L3

L4

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

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

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

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

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

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

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

Верификация

seL4

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

Примечания

Литература

Ссылки

Навигация

@@ Строка 1: / Строка 1: @@
+{{Значения|L4}}
-{{избыточная викификация}}
-{{Закончить перевод|en}}{{Значения|L4}}
+{{Закончить перевод|en}}
 {{Infobox software
 | name                    = L4
@@ Строка 27: / Строка 27: @@
 }}
-'''L4''' — [[микроядро]] [[Микроядро#Поколения|второго поколения]], разработанное [[Лидтке, Йохен|Йохеном Лидтке]] в [[1993 год]]у<ref name="Liedtke_93" />.
+'''L4''' — [[микроядро]] [[Микроядро#Поколения|второго поколения]], разработанное [[Лидтке, Йохен|Йохеном Лидтке]] в [[1993 год]]у<ref name="Liedtke_93" />.
-Архитектура микроядра L4 оказалась успешной. Было создано множество реализаций [[Двоичный интерфейс приложений|ABI]] и [[API]] микроядра L4. Все реализации стали называть семейством микроядер L4. Реализация Лидтке неофициально была названа «L4/x86»<ref name="dresden_overview">[https://os.inf.tu-dresden.de/L4/overview.html Семейство микроядер L4. Обзор]{{ref-en}} // Сайт [[Дрезденский технический университет|технического университета Дрездена]] ([[Германия]]).</ref>.
+Архитектура микроядра L4 оказалась успешной. Было создано множество реализаций [[Двоичный интерфейс приложений|ABI]] и [[API]] микроядра L4. Все реализации стали называть семейством микроядер L4. Реализация Лидтке неофициально была названа «L4/x86»<ref name="dresden_overview">[https://os.inf.tu-dresden.de/L4/overview.html Семейство микроядер L4. Обзор] {{Wayback|url=https://os.inf.tu-dresden.de/L4/overview.html |date=20150514022153 }}{{ref-en}} // Сайт [[Дрезденский технический университет|технического университета Дрездена]] ([[Германия]]).</ref>.
-[[Файл:L4 family tree.png|thumb|400px|Семейство микроядер L4]]
 == История ==
 === L1 ===
+В [[1977 год]]у Йохен Лидтке защитил дипломный проект по математике в [[Билефельдский университет|университете города Билефельд]] (Германия). В рамках проекта Лидтке написал [[компилятор]] для языка [[ELAN]] ([[:en:ELAN (programming language)|англ.]]). Язык ELAN создан в [[1974 год]]у на основе языка [[Алгол 68]] для обучения программированию<ref name="dresden_elan">[https://os.inf.tu-dresden.de/L4/l3elan.html Язык ELAN] {{Wayback|url=https://os.inf.tu-dresden.de/L4/l3elan.html |date=20150512154234 }}{{ref-en}} // Сайт [[Дрезденский технический университет|технического университета Дрездена]].</ref>. Лидтке назвал свою работу «L1»: буква «L» — первая буква фамилии автора ([[Лидтке, Йохен|'''L'''iedtke]]); цифра «1» — порядковый номер работы.
-В [[1977 год]]у Йохен Лидтке защитил дипломный проект по математике в [[Билефельдский университет|университете города Билефельд]] (Германия). В рамках проекта Лидтке написал [[компилятор]] для языка [[ELAN]] ([[:en:ELAN (programming language)|англ.]]). Язык ELAN создан в [[1974 год]]у на основе языка [[Алгол 68]] для обучения программированию<ref name="dresden_elan">[https://os.inf.tu-dresden.de/L4/l3elan.html Язык ELAN]{{ref-en}} // Сайт [[Дрезденский технический университет|технического университета Дрездена]].</ref>. Лидтке назвал свою работу «L1»: буква «L» — первая буква фамилии автора ([[Лидтке, Йохен|'''L'''iedtke]]); цифра «1» — порядковый номер работы.
 === L2 ===
 {{Основная статья|:en:Eumel|l1=операционная система Eumel{{ref-en}}}}
-В 1977 году Лидтке получил диплом математика, остался в университете города Билефельд и приступил к созданию [[Среда выполнения|среды выполнения]] для языка ELAN.
+В 1977 году Лидтке получил диплом математика, остался в университете города Билефельд и приступил к созданию [[Среда выполнения|среды выполнения]] для языка ELAN.
-‑битные [[микроконтроллер]]ы стали широко доступными. Требовалась операционная система, способная работать на небольших рабочих станциях в средних школах и вузах. [[CP/M]] не подходила. Исследовательский центр GMD ({{lang-en|German National Research Center for Computer Science}}) и университет города Билефельд решил разработать новую OC с нуля<ref name="Liedtke_iwooos93" />.
+‑битные [[микроконтроллер]]ы стали широко доступными. Требовалась операционная система, способная работать на небольших рабочих станциях в средних школах и вузах. [[CP/M]] не подходила. Национальный исследовательский центр компьютерных наук и технологий Германии GMD и университет города Билефельд решил разработать новую операционную систему с нуля<ref name="Liedtke_iwooos93" />.
-В [[1979 год]]у Йохен Лидтке начал разработку новой операционной системы и назвал её «[[Eumel]]» ([[:en:Eumel|англ.]]) от {{lang-en|'''e'''xtendable multi'''u'''ser '''m'''icroprocessor '''EL'''AN-system}}. Операционная система «Eumel» также называлась «L2», что означает «'''2'''‑я работа '''L'''iedtke». Новая ОС поддерживала 8-битовые процессоры [[Zilog Z80]], была [[Многопользовательская система|многопользовательской]] и [[Многозадачность|многозадачной]], была построена на основе [[Микроядро|микроядра]], поддерживала {{Не переведено|:en:Persistence (computer science)|Orthogonal persistence|orthogonal persistence}}. Поддержка orthogonal persistence заключалась в следующем: ОС периодически сохраняла на диск своё состояние (содержимое [[Оперативная память|памяти]], [[Регистр процессора|регистров процессора]] и др.); после перебоев в подаче [[Электроэнергия|электроэнергии]] ОС восстанавливалась из сохранённого состояния; программы продолжали работать так, будто бы сбоя не происходило; терялись только изменения, внесённые с момента последнего сохранения. ОС Eumel проектировалась под влиянием ОС [[Multics]] и содержала много общего с [[Ядро операционной системы|ядрами]] {{Не переведено|:en:Accent (programming language)|Accent (язык программирования)|Accent}} и [[Mach]]<ref name="Liedtke_iwooos93" />.
+В [[1979 год]]у Йохен Лидтке начал разработку новой операционной системы и назвал её «[[Eumel]]» ([[:en:Eumel|англ.]]) от {{lang-en|'''e'''xtendable multi'''u'''ser '''m'''icroprocessor '''EL'''AN-system}}. Операционная система «Eumel» также называлась «L2», что означает «'''2'''‑я работа '''L'''iedtke». Новая ОС поддерживала 8-битовые [[процессор]]ы [[Zilog Z80]], была [[Многопользовательская система|многопользовательской]] и [[Многозадачность|многозадачной]], была построена на основе [[Микроядро|микроядра]], поддерживала {{Не переведено|Orthogonal persistence|orthogonal persistence|en|Persistence (computer science)}}. Поддержка orthogonal persistence заключалась в следующем: ОС периодически сохраняла на диск своё состояние (содержимое [[Оперативная память|памяти]], [[Регистр процессора|регистров процессора]] и др.); после перебоев в подаче [[Электроэнергия|электроэнергии]] ОС восстанавливалась из сохранённого состояния; программы продолжали работать так, будто бы сбоя не происходило; терялись только изменения, внесённые с момента последнего сохранения. ОС Eumel проектировалась под влиянием ОС [[Multics]] и содержала много общего с [[Ядро операционной системы|ядрами]] {{Не переведено|Accent (язык программирования)|Accent|en|Accent (programming language)}} и [[Mach]]<ref name="Liedtke_iwooos93" />.
-Позднее ОС Eumel была портирована на процессоры [[Zilog Z8000]], [[Motorola 68000]] и [[Intel 8086]]. Эти процессоры были 8‑ и 16‑битовыми, не содержали [[Блок управления памятью|MMU]] и не поддерживали механизма защиты памяти. ОС Eumel эмулировала виртуальную машину, имеющую 32‑битовую адресацию и MMU<ref name="Liedtke_iwooos93">{{cite conference
+Позднее ОС Eumel была [[Портирование программного обеспечения|портирована]] на процессоры [[Zilog Z8000]], [[Motorola 68000]] и [[Intel 8086]]. Эти процессоры были 8‑ и 16‑битовыми, не содержали [[Блок управления памятью|MMU]] и не поддерживали механизма [[Защита памяти|защиты памяти]]. ОС Eumel эмулировала [[Виртуальная машина|виртуальную машину]], имеющую 32‑битовую адресацию и MMU<ref name="Liedtke_iwooos93">{{cite conference
  | first = Jochen
  | last = Liedtke
  | authorlink = Jochen Liedtke
  | title = A persistent system in real use—experiences of the first 13 years
- | booktitle = Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS)
+ | book-title = Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS)
  | pages = 2‑11
  | publisher =
- |date = Декабрь [[1993 год]]а
+ | date = Декабрь [[1993 год]]а
  | location = [[Эшвилл (Северная Каролина)|Asheville]], [[Северная Каролина|NC]], [[США|USA]]
- | url = https://os.itec.kit.edu/downloads/publ_1993_liedtke_persistent-system-in-real-use.pdf<!-- (платный доступ) http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=324932&tag=1 -->
+ | url = https://os.itec.kit.edu/downloads/publ_1993_liedtke_persistent-system-in-real-use.pdf
  | accessdate =
  | id =
+ | archive-date = 2015-07-10
-}}</ref>. Несмотря на использование эмуляции, к одной рабочей станции с ОС Eumel можно было подключить до пяти [[Компьютерный терминал|терминалов]]<ref name="Liedtke_iwooos93" />.
+ | archive-url = https://web.archive.org/web/20150710001522/https://os.itec.kit.edu/downloads/publ_1993_liedtke_persistent-system-in-real-use.pdf
+ | url-status = live
+ }} {{Cite web |url=https://os.itec.kit.edu/downloads/publ_1993_liedtke_persistent-system-in-real-use.pdf |title=Источник |access-date=2015-07-08 |archive-date=2015-07-10 |archive-url=https://web.archive.org/web/20150710001522/https://os.itec.kit.edu/downloads/publ_1993_liedtke_persistent-system-in-real-use.pdf |url-status=unfit }}</ref>. Несмотря на использование эмуляции, к одной рабочей станции с ОС Eumel можно было подключить до пяти [[Компьютерный терминал|терминалов]]<ref name="Liedtke_iwooos93" />.
-Поначалу писать программы для ОС Eumel можно было только на языке ELAN. Позднее были добавлены компиляторы для языков {{Не переведено|:en:Compiler Description Language|CDL}}, [[Паскаль (язык программирования)|Pascal]], [[Бейсик|Basic]] и {{Не переведено|:en:DYNAMO (programming language)|DYNAMO (язык программирования)|DYNAMO}}, но массово они не применялись<ref name="Liedtke_iwooos93" />.
+Поначалу писать программы для ОС Eumel можно было только на языке ELAN. Позднее были добавлены компиляторы для языков {{Не переведено|CDL||en|Compiler Description Language}}, [[Паскаль (язык программирования)|Pascal]], [[Бейсик|Basic]] и {{Не переведено|DYNAMO (язык программирования)|DYNAMO|en|DYNAMO (programming language)}}, но массово они не применялись<ref name="Liedtke_iwooos93" />.
-С [[1980 год]]а началось применение ОС Eumel сначала для обучения программированию и обработки текста, а затем и в коммерческих целях. Так, в середине 1980‑х годов ОС Eumel работала уже на более чем 2000 компьютеров в юридических и других фирмах<ref name="Liedtke_iwooos93" />.
+С [[1980 год]]а началось применение ОС Eumel сначала для обучения программированию и обработки текста, а затем — и в коммерческих целях. Так, в середине 1980‑х годов ОС Eumel работала уже на более чем 2000 компьютеров в юридических и других фирмах<ref name="Liedtke_iwooos93" />.
 === L3 ===
 {{Основная статья|:en:L3 microkernel|l1=микроядро L3{{ref-en}}}}
 С появлением процессоров, поддерживающих [[Виртуальная память|виртуальную память]] (за счёт MMU) и механизмы для её защиты, пропала необходимость эмуляции виртуальной машины.
-В [[1984 год]]у<ref name="liedtke_mem" /> Йохен Лидтке перешёл на работу в исследовательский центр GMD ({{lang-en|German National Research Center for Computer Science}}) для создания ОС, аналогичной ОС Eumel, но работающей без эмуляции. В настоящее время GMD входит в состав организации «[[Общество Фраунгофера]]».
+В [[1984 год]]у<ref name="liedtke_mem" /> Йохен Лидтке перешёл на работу в исследовательский центр GMD для создания ОС, аналогичной ОС Eumel, но работающей без эмуляции. В настоящее время GMD входит в состав организации «[[Общество Фраунгофера]]».
-С [[1987 год]]а<ref name="Liedtke_iwooos93" /> Йохен Лидтке и его команда из института [[Institute for system design techology|SET]], входящем в состав GMD, приступили к разработке нового микроядра, получившего название «L3» («L3» от «'''3'''‑я работа '''L'''iedtke»).
+С [[1987 год]]а<ref name="Liedtke_iwooos93" /> Йохен Лидтке и его команда из института [[Institute for system design techology|SET]], входящем в состав GMD, приступили к разработке нового микроядра, получившего название «L3» («L3» от «'''3'''‑я работа '''L'''iedtke»).
-Йохен Лидтке хотел проверить, возможно ли добиться высокой производительности компонента [[Межпроцессное взаимодействие|IPC]], если выбрать для ядра подходящую архитектуру и в реализации использовать особенности аппаратной платформы. Реализация механизма IPC оказалась удачной (по сравнению со сложной реализацией IPC в микроядре Mach). Позднее был реализован механизм изоляции областей памяти [[Процесс (информатика)|процессов]], работающих в [[Пространство пользователя|пространстве пользователя]].
+Йохен Лидтке хотел проверить, возможно ли добиться высокой производительности компонента [[Межпроцессное взаимодействие|IPC]], если выбрать для ядра подходящую архитектуру и в реализации использовать особенности [[архитектура компьютера|архитектуры]]. Реализация механизма IPC оказалась удачной (по сравнению со сложной реализацией IPC в микроядре Mach). Позднее был реализован механизм изоляции областей памяти [[Процесс (информатика)|процессов]], работающих в [[Пространство пользователя|пространстве пользователя]].
-В [[1988 год]]у разработка была завершена и была выпущена одноимённая операционная система. Микроядро L3 было написано на [[Язык ассемблера|языке ассемблера]], задействовало особенности процессоров архитектуры [[Intel]] [[x86]], не поддерживало другие платформы, по производительности обогнало микроядро Mach. ОС L3 была совместима с ОС Eumel: программы, созданные для ОС Eumel, работали под управлением ОС L3, но не наоборот<ref name="Liedtke_iwooos93" />.
+В [[1988 год]]у разработка была завершена и была выпущена одноимённая операционная система. Микроядро L3 было написано на [[Язык ассемблера|языке ассемблера]], задействовало особенности процессоров архитектуры [[Intel]] [[x86]], не поддерживало другие платформы, по производительности обогнало микроядро Mach. ОС L3 была совместима с ОС Eumel: программы, созданные для ОС Eumel, работали под управлением ОС L3, но не наоборот<ref name="Liedtke_iwooos93" />.
 Компоненты микроядра L3:
@@ Строка 86: / Строка 85: @@
 * компонент, реализующий механизм обеспечения безопасности, называемый {{lang-en|secure domains}} («tasks», «clans» и «chiefs»).
-С [[1989 год]]а<ref name="Liedtke_iwooos93" /> ОС стала применяться:
+С [[1989 год]]а<ref name="Liedtke_iwooos93" /> ОС стала применяться:
-* в школах (заменила свою предшественницу — ОС Eumel)<ref name="Liedtke_iwooos93" />;
+* в школах (заменила свою предшественницу — ОС Eumel)<ref name="Liedtke_iwooos93" />;<!--
-* фирмой «[[TÜV SÜD]]» (Германия){{Нет АИ|6|9|2010}};
+* фирмой «[[TÜV SÜD]]» (Германия){{Нет АИ|6|9|2010}};-->
-* на примерно 3000 компьютерах, установленных в юридических фирмах Германии<ref name="liedtke_mem">[http://os.ibds.kit.edu/downloads/in-memoriam-jochen-liedtke_en.pdf In Memoriam Jochen Liedtke (1953—2001)].</ref>.
+* на примерно 3000 компьютерах, установленных в юридических фирмах Германии<ref name="liedtke_mem">[http://os.ibds.kit.edu/downloads/in-memoriam-jochen-liedtke_en.pdf In Memoriam Jochen Liedtke (1953—2001)] {{Wayback|url=http://os.ibds.kit.edu/downloads/in-memoriam-jochen-liedtke_en.pdf |date=20120305193522 }}.</ref>.
 === L4 ===
 Во время работы над микроядром L3 Йохен Лидтке обнаружил недостатки микроядра Mach. Желая повысить производительность, Лидтке стал составлять код нового микроядра на языке ассемблера с использованием особенностей архитектуры процессоров [[Intel 80386|Intel i386]]. Новое микроядро получило название «L4» (от «'''4'''‑я работа '''L'''iedtke»).
-В 1993 году реализация микроядра L4 была закончена. Компонент IPC оказался в {{nobr|20 раз}} быстрее IPC из микроядра Mach<ref name="Liedtke_93">{{cite conference
+В 1993 году реализация микроядра L4 была закончена. Компонент IPC оказался в {{nobr|20 раз}} быстрее IPC из микроядра Mach<ref name="Liedtke_93">{{cite conference
  | first = Jochen
  | last = Liedtke
  | authorlink = Jochen Liedtke
  | title = Improving IPC by kernel design
- | booktitle = 14th [[Ассоциация вычислительной техники|ACM]] [[:en:Symposium on Operating Systems Principles|symposium on operating system principles]]
+ | book-title = 14th [[Ассоциация вычислительной техники|ACM]] [[:en:Symposium on Operating Systems Principles|symposium on operating system principles]]
  | pages = 175–88
  | publisher =
  | date = Декабрь [[1993 год]]а
  | location = [[Эшвилл (Северная Каролина)|Asheville]], [[Северная Каролина|NC]], [[США|USA]]
- | url = http://www.read.seas.harvard.edu/~kohler/class/aosref/liedtke93improving.pdf<!-- (платный доступ) http://portal.acm.org/citation.cfm?id=168619.168633&coll=portal&dl=ACM&type=series&idx=168619&part=Proceedings&WantType=Proceedings&title=ACM%20Symposium%20on%20Operating%20Systems%20Principles&CFID=18793560&CFTOKEN=54028606 -->
+ | url = http://www.read.seas.harvard.edu/~kohler/class/aosref/liedtke93improving.pdf
  | accessdate =
  | id =
+ | archive-date = 2016-03-04
-}}</ref>.
+ | archive-url = https://web.archive.org/web/20160304202636/http://www.read.seas.harvard.edu/~kohler/class/aosref/liedtke93improving.pdf
+ | url-status = live
+ }} {{Cite web |url=http://www.read.seas.harvard.edu/~kohler/class/aosref/liedtke93improving.pdf |title=Источник |access-date=2015-07-08 |archive-date=2016-03-04 |archive-url=https://web.archive.org/web/20160304202636/http://www.read.seas.harvard.edu/~kohler/class/aosref/liedtke93improving.pdf |url-status=unfit }}</ref>.
-ОС, построенные на [[Микроядро#Поколения|микроядрах первого поколения]] (в частности, на микроядре Mach), отличались низкой производительностью. Из-за этого в середине [[1990-е годы|1990-х годов]] разработчики стали пересматривать концепцию микроядерной архитектуры. В частности, плохую производительность микроядра Mach объясняли переносом компонента, ответственного за IPC, в пространство пользователя.
+ОС, построенные на [[Микроядро#Поколения|микроядрах первого поколения]] (в частности, на микроядре Mach), отличались низкой производительностью. Из-за этого в середине [[1990-е годы|1990-х годов]] разработчики стали пересматривать концепцию микроядерной архитектуры. В частности, плохую производительность микроядра Mach объясняли переносом компонента, ответственного за IPC, в пространство пользователя.<!--
-Некоторые компоненты микроядра Mach были возвращены назад — внутрь микроядра{{Нет АИ|22|8|2010}}. Это нарушало саму идею микроядер (минимальный размер, изоляция компонентов), но позволило увеличить производительность ОС.
+Некоторые компоненты микроядра Mach были возвращены назад — внутрь микроядра{{Нет АИ|22|8|2010}}. Это нарушало саму идею микроядер (минимальный размер, изоляция компонентов), но позволило увеличить производительность ОС.-->
-Исследователи искали причины низкой производительности микроядра Mach и тщательно анализировали компоненты, важные для обеспечения хорошей производительности. Анализ показал, что ядро выделяло процессам слишком большой [[Working Set|working set]] (много памяти), в результате чего при обращении ядра к памяти постоянно происходили [[Кэш‑промах|кэш‑промахи]]<ref name="Lie95">{{cite conference
+Исследователи искали причины низкой производительности микроядра Mach и тщательно анализировали компоненты, важные для обеспечения хорошей производительности. Анализ показал, что ядро выделяло процессам слишком большой [[Working Set|working set]] (много памяти), в результате чего при обращении ядра к памяти постоянно происходили [[Кэш процессора|кэш]]‑промахи ({{lang-en|cache misses}})<ref name="Lie95">{{cite conference
- | first = Jochen
+ |first        = Jochen
- | last = Liedtke
+ |last         = Liedtke
- | authorlink = Jochen Liedtke
+ |authorlink   = Jochen Liedtke
- | title = On µ-Kernel construction
+ |title        = On µ-Kernel construction
- | booktitle = Proc. 15th [[Ассоциация вычислительной техники|ACM]] [[Symposium on Operating Systems Principles|symposium on operating systems principles]] (SOSP)
+ |book-title   = Proc. 15th [[Ассоциация вычислительной техники|ACM]] [[Symposium on Operating Systems Principles|symposium on operating systems principles]] (SOSP)
- | pages = 237‑250
+ |pages        = 237‑250
- | date = Декабрь [[1995 год]]а
+ |date         = Декабрь [[1995 год]]а
- | url = http://i30www.ira.uka.de/research/publications/papers/index.php?lid=en&docid=642
+ |url          = http://i30www.ira.uka.de/research/publications/papers/index.php?lid=en&docid=642
+ |access-date  = 2015-07-08
-}}</ref>. Анализ позволил сформулировать новое правило для разработчиков микроядер — микроядро должно проектироваться так, чтобы компоненты, важные для обеспечения высокой производительности, помещались в [[кэш процессора]] (желательно, первого уровня ({{lang-en|level 1}}, L1) и желательно, чтобы в кеше ещё осталось немного места).
+ |archive-date = 2009-03-18
+ |archive-url  = https://web.archive.org/web/20090318005943/http://i30www.ira.uka.de/research/publications/papers/index.php?lid=en&docid=642
+ |url-status   = dead
+}} {{Cite web |url=http://i30www.ira.uka.de/research/publications/papers/index.php?lid=en&docid=642 |title=Источник |access-date=2015-07-08 |archive-date=2009-03-18 |archive-url=https://web.archive.org/web/20090318005943/http://i30www.ira.uka.de/research/publications/papers/index.php?lid=en&docid=642 |url-status=unfit }}</ref>. Анализ позволил сформулировать новое правило для разработчиков микроядер — микроядро должно проектироваться так, чтобы компоненты, важные для обеспечения высокой производительности, помещались в [[кэш процессора]] (желательно, первого уровня ({{lang-en|level 1}}, L1) и желательно, чтобы в кеше ещё осталось немного места).
 Из-за резкого скачка в производительности компонента IPC существующие ОС оказались неспособны обработать возросший поток сообщений IPC. Несколько университетов (например, [[Дрезденский технический университет|технический университет Дрездена]], [[университет Нового Южного Уэльса]]), институтов и организаций (например, [[IBM]]) начали создавать реализации L4 и строить на их основе новые ОС.
-В [[1996 год]]у Лидтке защитил диссертацию в [[Берлинский технический университет|техническом университете Берлина]] по теме «guarded [[:en:Page table|page tables]]»<ref>Jochen Liedtke. [http://citeseer.ist.psu.edu/liedtke94page.html Page table structures for fine-grain virtual memory]. Technical report 872. German national research center for computer science (GMD). Октябрь [[1994 год]]а.</ref> и получил степень [[Доктор философии|PhD]]<ref name="liedtke_mem_2" />.
+В [[1996 год]]у Лидтке защитил диссертацию на степень [[PhD]]<ref name="liedtke_mem_2" /> в [[Берлинский технический университет|техническом университете Берлина]] по теме «защищённые таблицы страниц»<ref>Jochen Liedtke. [http://citeseer.ist.psu.edu/liedtke94page.html Page table structures for fine-grain virtual memory] {{Wayback|url=http://citeseer.ist.psu.edu/liedtke94page.html |date=20071112043202 }}. Technical report 872. German national research center for computer science (GMD). Октябрь [[1994 год]]а.</ref>.
-С 1996 года в {{Не переведено|:en:Thomas J. Watson Research Center|Исследовательский центр имени Томаса Уотсона|исследовательском центре имени Томаса Уотсона}} Лидтке с коллегами продолжил исследования микроядра L4, микроядер вообще и операционной системы «[[Sawmill OS]]» в частности<ref name="Gefflaut_JPLEUTDR_00">{{cite conference
+С 1996 года в {{Не переведено|Исследовательский центр имени Томаса Уотсона|исследовательском центре имени Томаса Уотсона|en|Thomas J. Watson Research Center}} Лидтке с коллегами продолжил исследования микроядра L4, микроядер вообще и операционной системы «[[Sawmill OS]]» в частности<ref name="Gefflaut_JPLEUTDR_00">{{cite conference
  | first1 = Alain
  | last1 = Gefflaut
@@ Строка 151: / Строка 156: @@
  | url = http://dl.acm.org/citation.cfm?id=566726.566751
  | title = The Sawmill multiserver approach
- | booktitle = [[Ассоциация вычислительной техники|ACM]] SIGOPS European Workshop
+ | book-title = [[Ассоциация вычислительной техники|ACM]] SIGOPS European Workshop
- | pages = 109-114
+ | pages = 109—114
  | date = [[2000 год]]
  | location = [[Коллинг|Kolding]], [[Дания|Denmark]]
-}}</ref>. Из-за отсутствия коммерческого успеха у ОС «{{Не переведено 5|IBM Workspace OS}}», построенной на третьей версии микроядра Mach от [[Университет Карнеги — Меллон|CMU]] и разрабатываемой фирмой IBM с января 1991 года по 1996 год<ref name="WorkplaceMicrokernelandOS">{{cite journal
+}}</ref>. Из-за отсутствия коммерческого успеха у ОС «{{Не переведено 5|IBM Workspace OS}}», построенной на третьей версии микроядра Mach от [[Университет Карнеги — Меллон|CMU]] и разрабатываемой фирмой IBM с января 1991 года по 1996 год<ref name="WorkplaceMicrokernelandOS">{{статья
- |url         = http://www.cs.ucr.edu/~brett/PAPERS/SPE97/REVISED/techreport.ps
+|ссылка=http://www.cs.ucr.edu/~brett/PAPERS/SPE97/REVISED/techreport.ps
- |archiveurl  = https://web.archive.org/web/20070824050732/http://www.cs.ucr.edu/~brett/PAPERS/SPE97/REVISED/techreport.ps
+|archiveurl=https://web.archive.org/web/20070824050732/http://www.cs.ucr.edu/~brett/PAPERS/SPE97/REVISED/techreport.ps
- |archivedate = 2007-08-24
+|archivedate=2007-08-24
- |accessdate  = March 25, 2013
+|accessdate=2013-03-25
- |title       = Workplace Microkernel and OS: A Case Study
+|заглавие=Workplace Microkernel and OS: A Case Study
+|издательство=John Wiley & Sons, Ltd.
- |first1      = Brett D
+|язык=und
- |last1       = Fleisch
+|автор=Fleisch, Brett D; Allan, Mark}}</ref>, вместо понятия «микроядро L4» использовалось понятие «Lava Nucleus» или, кратко, «LN».
- |first2      = Mark
- |last2       = Allan
- |date        = [[23 сентября]] [[1997 год]]а
- |publisher   = John Wiley & Sons, Ltd.
- |deadurl     = yes
-}}</ref>, вместо понятия «микроядро L4» использовалось понятие «Lava Nucleus» или, кратко, «LN».
 Со временем код микроядра L4 был избавлен от привязки к платформе, были улучшены механизмы обеспечения безопасности и изоляции.
-В [[1999 год]]у Лидтке стал работать профессором по операционным системам в [[Технологический институт Карлсруэ|технологическом институте Карлсруэ]] (Германия)<ref name="liedtke_mem_2" />.
+В [[1999 год]]у Лидтке стал работать профессором по операционным системам в [[Технологический институт Карлсруэ|технологическом институте Карлсруэ]] (Германия)<ref name="liedtke_mem_2" />.
 === Микроядро L4Ka::Hazelnut ===
+В 1999 году Йохен Лидтке был принят в состав группы «Systems Architecture Group» ({{anchor|SAG}}SAG), работающей в технологическом институте Карлсруэ (Германия), и продолжил исследования микроядерных ОС. Группа SAG также известна как группа «L4Ka».
-В 1999 году Йохен Лидтке был принят в состав группы «Systems Architecture Group» ({{anchor|SAG}}SAG), работающей в технологическом институте Карлсруэ (Германия), и продолжил исследования микроядерных ОС. Группа SAG также известна как группа «L4Ka».
 Желая доказать возможность реализации микроядра на [[Высокоуровневый язык программирования|высокоуровневом языке]], группа [[#SAG|SAG]] разработала микроядро «L4Ka::Hazelnut». Работа велась в технологическом институте Карлсруэ при поддержке [[Немецкое научно-исследовательское общество|DFG]]<ref>[https://web.archive.org/web/20010419064321/http://www.l4ka.org/ Страница группы «L4Ka»] // [[archive.org]].</ref>. Реализация была написана на языке [[C++]] и поддерживала процессоры архитектур [[IA-32]] и [[ARM (архитектура)|ARM]]. Производительность нового микроядра оказалась приемлемой, и разработка ядер на языке ассемблера была прекращена.
 === Микроядро L4/Fiasco ===
+В [[1998 год]]у группа Operating Systems Group, входящая в состав технического университета Дрездена, начала разработку собственной реализации микроядра L4, получившую название «L4/Fiasco». Разработка велась на языке C++ параллельно с разработкой микроядра «L4Ka::Hazelnut».
-В [[1998 год]]у группа Operating Systems Group, входящая в состав технического университета Дрездена, начала разработку собственной реализации микроядра L4, получившую название «L4/Fiasco». Разработка велась на языке C++ параллельно с разработкой микроядра «L4Ka::Hazelnut».
 В то время микроядро L4Ka::Hazelnut не поддерживало concurrency в пространстве ядра, а микроядро «L4Ka::Pistachio» поддерживало [[Прерывание|прерывания]] в пространстве ядра только в особых точках preemption. Разработчики микроядра «L4/Fiasco» реализовали полную [[Вытесняющая многозадачность|вытесняющую многозадачность]] (за исключением некоторых атомарных операций). Это усложнило архитектуру ядра, но снизило задержки при прерываниях, что важно для операционной системы реального времени.
-Микроядро «L4/Fiasco» использовалось в ОС «DROPS»<ref>[http://os.inf.tu-dresden.de/drops/overview.html Drops overview].</ref> — [[Система реального времени#Система жёсткого реального времени|ОС «жёсткого» реального времени]] ({{lang-en|[[:en:Real-time computing|hard real-time]]}}), также разработанной в техническом университете Дрездена.
+Микроядро «L4/Fiasco» использовалось в ОС «DROPS»<ref>[http://os.inf.tu-dresden.de/drops/overview.html Drops overview] {{Wayback|url=http://os.inf.tu-dresden.de/drops/overview.html |date=20110807170107 }}.</ref> — [[Система реального времени#Система жёсткого реального времени|ОС «жёсткого» реального времени]] (когда крайне важно, чтобы на событие реагировали в строго установленные сроки), также разработанной в техническом университете Дрездена.
 Ввиду усложнения архитектуры микроядра в поздних версиях ОС «Fiasco» разработчики вернулись к традиционному подходу — запуску ядра с выключенными прерываниями (за исключением нескольких точек preemption).
@@ Строка 193: / Строка 191: @@
 === Микроядро L4Ka::Pistachio ===
 Реализации микроядра L4, созданные до выпуска микроядра L4Ka::Pistachio и поздних версий микроядра «Fiasco», использовали особенности архитектуры компьютера (были «привязаны» к архитектуре процессора). Был разработан API, не зависимый от архитектуры. Несмотря на добавление [[:en:Software portability|переносимости]], API обеспечивал высокую производительность. Идеи, лежащие в основе микроядерной архитектуры, не изменились.
-В начале [[2001 год]]а новое L4 API было опубликовано, сильно отличалось от L4 API предыдущей версии, получило номер версии 4 («version 4», также известно как «version X.2») и отличалось:
+В начале [[2001 год]]а новое L4 API было опубликовано, сильно отличалось от L4 API предыдущей версии, получило номер версии 4 («version 4», также известно как «version X.2») и отличалось:
-* лучшей поддержкой многопроцессорных систем;
+* лучшей поддержкой [[Многопроцессорность|многопроцессорных]] систем;
 * «looser ties» между [[Поток выполнения|потоками]] и адресным пространством;
 * добавлением к потокам, работающим в пространстве пользователя, блоков UTCBs ({{lang-en|user-level thread control blocks}});
 * добавлением виртуальных [[Регистр процессора|регистров]].
-После выпуска новой версии API группа SAG приступила к созданию нового микроядра, получившего название «L4Ka::Pistachio»<ref>[http://l4ka.org/projects/pistachio Микроядро «L4Ka::Pistachio»]{{ref-en}}.</ref><ref>[http://l4ka.org/team Команда разработчиков «L4Ka»]{{ref-en}}.</ref>. Код составлялся с нуля на языке C++, использовался опыт проекта L4Ka::Hazelnut. Внимание уделялось высокой производительности и переносимости.
+После выпуска новой версии API группа SAG приступила к созданию нового микроядра, получившего название «L4Ka::Pistachio»<ref>[http://l4ka.org/projects/pistachio Микроядро «L4Ka::Pistachio»] {{Wayback|url=http://l4ka.org/projects/pistachio |date=20070109053214 }}{{ref-en}}.</ref><ref>[http://l4ka.org/team Команда разработчиков «L4Ka»] {{Wayback|url=http://l4ka.org/team |date=20070122040136 }}{{ref-en}}.</ref>. Код составлялся с нуля на языке C++, использовался опыт проекта L4Ka::Hazelnut. Внимание уделялось высокой производительности и переносимости.
-[[10 июня]] 2001 года доктор Йохен Лидтке погиб<ref name="liedtke_mem_2">[http://i30www.ira.uka.de/aboutus/people/liedtke/inmemoriam.php System architecture group. About us. People. Liedtke]. [https://web.archive.org/web/20020610075139/http://i30www.ira.uka.de/aboutus/people/liedtke/inmemoriam.php Архивная копия].</ref> в автокатастрофе. После этого скорость развития проекта заметно снизилась.
+[[10 июня]] 2001 года доктор Йохен Лидтке погиб<ref name="liedtke_mem_2">[http://i30www.ira.uka.de/aboutus/people/liedtke/inmemoriam.php System architecture group. About us. People. Liedtke]. [https://web.archive.org/web/20020610075139/http://i30www.ira.uka.de/aboutus/people/liedtke/inmemoriam.php Архивная копия].</ref> в автокатастрофе. После этого скорость развития проекта заметно снизилась.
-В [[2003 год]]у<ref>[https://web.archive.org/web/20031002084129/http://l4ka.org/projects/pistachio/pistachio-whitepaper.pdf The L4Ka::Pistachio Microkernel].{{ref-en}} [[Белая книга]]. [[Portable Document Format|PDF]]. [[1 мая]] [[2003 год]]а // [[archive.org]].</ref> работа была завершена благодаря усилиям студентов Лидтке: Volkmar Uhlig, Uwe Dannowski и Espen Skoglund. Исходный код был выпущен под лицензией [[Лицензия BSD|2‑clause BSD]].
+В [[2003 год]]у<ref>[https://web.archive.org/web/20031002084129/http://l4ka.org/projects/pistachio/pistachio-whitepaper.pdf The L4Ka::Pistachio Microkernel].{{ref-en}} [[Белая книга]]. [[Portable Document Format|PDF]]. [[1 мая]] [[2003 год]]а // [[archive.org]].</ref> работа была завершена благодаря усилиям студентов Лидтке: Volkmar Uhlig, Uwe Dannowski и Espen Skoglund. Исходный код был выпущен под лицензией [[Лицензия BSD|2‑clause BSD]].
 === Новые версии Fiasco ===
+Параллельно продолжалось развитие микроядра L4/Fiasco. Была добавлена поддержка нескольких аппаратных платформ ([[x86]], [[x86-64|AMD64]], [[ARM (архитектура)|ARM]]). Примечательно, что версия Fiasco, названная «FiascoUX», могла работать в пространстве пользователя под управлением ОС [[Ядро Linux|Linux]].
-Параллельно продолжалось развитие микроядра L4/Fiasco. Была добавлена поддержка нескольких аппаратных платформ (x86, [[x86-64|AMD64]], ARM). Примечательно, что версия Fiasco, названная «FiascoUX», могла работать в пространстве пользователя под управлением ОС [[Ядро Linux|Linux]].
 Разработчики микроядра L4/Fiasco реализовали несколько расширений к L4v2 API.
-* Исключение IPC позволило ядру передавать [[Обработка исключений|обработку исключений]] процессора в пространство пользователя.
+* Исключение [[Межпроцессное взаимодействие|IPC]] позволило ядру передавать [[Обработка исключений|обработку исключений]] процессора в пространство пользователя.
-* Добавление {{Не переведено|:en:Alien threat|Alien threat|alien threat}}(потока, выполняемого одним ядром процессора от имени процесса, запущенного на другом ядре процессора) позволило реализовать детальное управление [[Системный вызов|системными вызовами]].
+* Добавление {{iw|Alien thread}} (потока, выполняемого одним ядром процессора от имени процесса, запущенного на другом ядре процессора) позволило реализовать детальное управление [[Системный вызов|системными вызовами]].
 * Добавление UTCB (таких же, как в L4 API версии X.2).
 Кроме того, микроядро «Fiasco» предоставляло механизмы управления правами коммуникации. Такие же механизмы существовали для управления потребляемыми ядром ресурсами.
@@ Строка 221: / Строка 217: @@
 === Университет Нового Южного Уэльса и фирма NICTA ===
 {{anchor|UNSW}}Разработчики из [[Университет Нового Южного Уэльса|университета Нового Южного Уэльса]] создали микроядра L4/MIPS и L4/Alpha — реализации L4 для 64‑битовых процессоров серий [[MIPS (архитектура)|MIPS]] и [[DEC Alpha]]. Оригинальное микроядро L4 поддерживало только процессоры архитектуры x86 и неофициально стало называться «L4/x86». Реализации были написаны с нуля на языке [[Си (язык программирования)|C]] и языке ассемблера, не были переносимы. После выпуска независимого от платформы микроядра L4Ka::Pistachio группа UNSW прекратила разработку своих микроядер, занялась портированием микроядра L4Ka::Pistachio. Реализация механизма передачи сообщений оказалась быстрее других реализаций (36 тактов на процессорах архитектуры [[Itanium]])<ref name=Gray_CCMH_05>{{cite conference
  | first = Charles
@@ Строка 227: / Строка 222: @@
  | coauthors = Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; [[Gernot Heiser|Heiser, Gernot]]
  | title = Itanium — system implementor's tale
- | booktitle = [[USENIX]] [[Ежегодная техническая конференция USENIX|Annual Technical Conference]]
+ | book-title = [[USENIX]] [[Ежегодная техническая конференция USENIX|Annual Technical Conference]]
  | pages = 264‑278
  | date = Апрель 2005 года
  | location = [[Анахайм (Калифорния)|Annaheim]], [[Калифорния|CA]], [[США|USA]]
  | url = http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html
+ | access-date = 2015-07-08
-}}</ref>.
+ | archive-date = 2007-02-17
+ | archive-url = https://web.archive.org/web/20070217224750/http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html
+ | url-status = live
+ }} {{Cite web |url=http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html |title=Источник |access-date=2015-07-08 |archive-date=2007-02-17 |archive-url=https://web.archive.org/web/20070217224750/http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html |url-status=unfit }}</ref>.
-Группа UNSW показала, что [[драйвер]], работающий в пространстве пользователя, может исполняться также, как и драйвер, работающий в пространстве ядра<ref name=Leslie_CFGGMPSEH_05>{{cite journal
+Группа UNSW показала, что [[драйвер]], работающий в пространстве пользователя, может исполняться так же, как и драйвер, работающий в пространстве ядра<ref name=Leslie_CFGGMPSEH_05>{{статья
+|заглавие=User-level device drivers: achieved performance
- | last = Leslie
+|издание=Journal of Computer Science and Technology
- | first = Ben
+|том=20
- | coauthors = Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; [[:en:Gernot Heiser|Heiser, Gernot]]
+|номер=5
- | date = Сентябрь [[2005 год]]а
+|страницы=654‑664
- | title = User-level device drivers: achieved performance
+|doi=10.1007/s11390-005-0654-4
- | journal = Journal of Computer Science and Technology
+|язык=und
- | volume = 20
+|автор=Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; [[:en:Gernot Heiser|Heiser, Gernot]]}}</ref>.
- | issue = 5
- | pages = 654‑664
- | doi = 10.1007/s11390-005-0654-4
-}}</ref>.
 Она разработала компоненты для паравиртуализации ядер Linux. Компоненты работали поверх микроядра L4. Результат был назван «{{Не переведено 5|Wombat OS}}». Wombat OS могла работать на процессорах архитектур x86, ARM и MIPS. На процессорах [[Intel XScale]] ОС Wombat OS выполняла переключение контекста в 30 раз медленнее, чем [[Монолитное ядро|монолитное]] ядро Linux<ref name=vanSchaik_Heiser_07>{{cite conference
- | first = Carl
+ |first        = Carl
- | last = van Schaik
+ |last         = van Schaik
- | author2 = Heiser, Gernot
+ |author2      = Heiser, Gernot
- | authorlink2 = Gernot Heiser
+ |authorlink2  = Gernot Heiser
- | title = High-performance microkernels and virtualisation on ARM and segmented architectures
+ |title        = High-performance microkernels and virtualisation on ARM and segmented architectures
- | booktitle = 1st International Workshop on Microkernels for Embedded Systems
+ |book-title   = 1st International Workshop on Microkernels for Embedded Systems
- | pages = 11‑21
+ |pages        = 11‑21
- | publisher = [[:en:NICTA|NICTA]]
+ |publisher    = [[:en:NICTA|NICTA]]
- | date = Январь 2007 года
+ |date         = Январь 2007 года
- | location = [[Сидней|Sydney]], [[Австралия|Australia]]
+ |location     = [[Сидней|Sydney]], [[Австралия|Australia]]
- | url = http://ertos.nicta.com.au/publications
+ |url          = http://ertos.nicta.com.au/publications
- | accessdate = 2007-04-01
+ |accessdate   = 2007-04-01
- | id =
+ |id           =
+ |archive-date = 2007-04-26
-}}</ref>.
+ |archive-url  = https://web.archive.org/web/20070426092901/http://ertos.nicta.com.au/publications
+ |url-status   = live
+}} {{Cite web |url=http://ertos.nicta.com.au/publications |title=Источник |access-date=2015-07-08 |archive-date=2007-04-26 |archive-url=https://web.archive.org/web/20070426092901/http://ertos.nicta.com.au/publications |url-status=unfit }}</ref>.
-Затем группа UNSW перешла в фирму NICTA, создала ответвление микроядра L4Ka::Pistachio и назвала его «NICTA::L4-embedded». Новое микроядро писалось для коммерческих [[Встраиваемая система|встраиваемых систем]], требовало мало памяти и реализовывало упрощённый API L4. С упрощённым API системные вызовы были сделаны настолько «короткими», что не требовали точек вытесняющей многозадачности и позволяли реализовать [[Операционная система реального времени|ОС реального времени]]<ref name=Ruocco_08>{{cite journal
+Затем группа UNSW перешла в фирму NICTA, создала ответвление микроядра L4Ka::Pistachio и назвала его «NICTA::L4-embedded». Новое микроядро писалось для коммерческих [[Встраиваемая система|встраиваемых систем]], требовало мало памяти и реализовывало упрощённый API L4. С упрощённым API системные вызовы были сделаны настолько «короткими», что не требовали точек вытесняющей многозадачности и позволяли реализовать [[Операционная система реального времени|ОС реального времени]]<ref name=Ruocco_08>{{статья
+|заглавие=A real-time programmer's tour of general-purpose L4 microkernels
- | first = Sergio
+|издание=EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications
- | last = Ruocco
+|doi=10.1155/2008/234710
- | title =   A real-time programmer's tour of general-purpose L4 microkernels
+|ссылка=http://www.hindawi.com/getarticle.aspx?doi=10.1155/2008/234710
- | journal = EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications
- | doi = 10.1155/2008/234710
+|том=2008
+|страницы=1‑14
- | date = Октябрь 2008 года
+|язык=en
- | url=http://www.hindawi.com/getarticle.aspx?doi=10.1155/2008/234710
+|тип=journal
- | volume = 2008
+|автор=Ruocco, Sergio
- | issue =
+|месяц=10
- | id =
+|год=2008
- | language =
+}}{{Недоступная ссылка|date=Апрель 2020 |bot=InternetArchiveBot }}</ref>.
- | format =
- | accessdate =
- | laysummary =
- | laysource =
- | laydate =
- | quote =
- | pages = 1‑14
-}}</ref>.
 === Коммерческое применение ===
+Фирма [[Qualcomm]] запускала реализацию микроядра L4, разработанную фирмой «{{Не переведено 5|NICTA}}», на наборе микросхем, называемом «Mobile Station Modem» (MSM). Об этом в ноябре [[2005 год]]а сообщили<ref>[http://www.nicta.com.au/director/mediacentre/media_releases_2005.cfm?viewArticle=true&item_id=2563&startrow=1] {{Wayback|url=http://www.nicta.com.au/director/mediacentre/media_releases_2005.cfm?viewArticle=true&item_id=2563&startrow=1 |date=20060825225104 }}.</ref> представители фирмы «NICTA», а в конце [[2006 год]]а наборы микросхем MSM поступили в продажу. Так реализация микроядра L4 оказалась в [[Сотовый телефон|сотовых телефонах]].
+В августе 2006 года {{Не переведено|Хейсер, Гернот|Г. Хейсер|en|Gernot Heiser}} основал фирму Open Kernel Labs. Тогда Хейсер занимал должность руководителя программы ERTOS, организованной фирмой NICTA<ref>[https://web.archive.org/web/20040402073335/http://nicta.com.au/ertos.html Страница] программы ERTOS на сайте NICTA // [[archive.org]].</ref>, и был профессором в университете UNSW. Фирма «OK Labs» создавалась для
-Фирма [[Qualcomm]] запускала реализацию микроядра L4, разработанную фирмой «{{Не переведено 5|NICTA}}», на наборе микросхем, называемом «Mobile Station Modem» (MSM). Об этом в ноябре [[2005 год]]а сообщили<ref>[http://www.nicta.com.au/director/mediacentre/media_releases_2005.cfm?viewArticle=true&item_id=2563&startrow=1].</ref> представители фирмы «NICTA», а в конце [[2006 год]]а наборы микросхем MSM поступили в продажу. Так реализация микроядра L4 оказалась в [[Сотовый телефон|сотовых телефонах]].
-В августе 2006 года {{Не переведено|:en:Gernot Heiser|Хейсер, Гернот|Г. Хейсер}} основал фирму Open Kernel Labs. Тогда Хейсер занимал должность руководителя программы ERTOS, организованной фирмой NICTA<ref>[https://web.archive.org/web/20040402073335/http://nicta.com.au/ertos.html Страница] программы ERTOS на сайте NICTA // [[archive.org]].</ref>, и был профессором в университете UNSW. Фирма «OK Labs» создавалась для
 * оказания [[Техническая поддержка|технической поддержки]] коммерческим пользователям L4;
 * продолжения разработки L4 совместно с фирмой «NICTA» для продолжения коммерческого использования реализации L4, но уже под [[бренд]]ом «OKL4».
-В апреле [[2008 год]]а была выпущена версия 2.1 микроядра «OKL4» — первая [[Стадии разработки программного обеспечения#Общая доступность|общедоступная]] реализация L4, имеющая [[:en:Capability-based security|capability-based security]]. В октябре 2008 года вышла версия 3.0<ref>[http://wiki.ok-labs.com/ OKL4 3.0]</ref> — последняя версия «OKL4» с [[Открытое программное обеспечение|открытым]] [[Исходный код|исходным кодом]]. Исходный код следующих версий был закрыт. Прослойка микроядра, обеспечивающая работу [[гипервизор]]а, была переписана с целью добавления поддержки native гипервизора, называемого «OKL4 microvisor»<ref>[http://www.ok-labs.com/products/okl4-microvisor OKL4 microvisor].</ref>.
+В апреле [[2008 год]]а была выпущена версия 2.1 микроядра «OKL4» — первая [[Стадии разработки программного обеспечения#Общая доступность|общедоступная]] реализация L4, имеющая [[:en:Capability-based security|capability-based security]]. В октябре 2008 года вышла версия 3.0<ref>{{Cite web |url=http://wiki.ok-labs.com/ |title=OKL4 3.0 |accessdate=2011-05-21 |archiveurl=https://web.archive.org/web/20110516140001/http://wiki.ok-labs.com/ |archivedate=2011-05-16 |url-status=dead }}</ref> — последняя версия «OKL4» с [[Открытое программное обеспечение|открытым]] [[Исходный код|исходным кодом]]. Исходный код следующих версий был закрыт. Прослойка микроядра, обеспечивающая работу [[гипервизор]]а, была переписана с целью добавления поддержки native гипервизора, называемого «OKL4 microvisor»<ref>[http://www.ok-labs.com/products/okl4-microvisor OKL4 microvisor] {{Wayback|url=http://www.ok-labs.com/products/okl4-microvisor |date=20140313081519 }}.</ref>.
-Фирма «OK Labs» распространяла паравиртуализированную ({{lang-en|para-virtualized}}) [[Операционная система|ОС]] [[Linux]], называемую «OK:Linux»<ref>[http://www.ok-labs.com/products/ok-linux OK:Linux]</ref>. «OK:Linux» была потомком ОС «[[:en:Wombat OS|Wombat OS]]»{{ref-en}}. Также фирма «OK Labs» распространяла паравиртуализированные версии [[Операционная система|операционных систем]] [[Symbian]] и Android.
+Фирма «OK Labs» распространяла паравиртуализированную ({{lang-en|para-virtualized}}) [[Операционная система|ОС]] [[Linux]], называемую «OK:Linux»<ref>{{Cite web |url=http://www.ok-labs.com/products/ok-linux |title=OK:Linux |accessdate=2015-07-08 |archiveurl=https://web.archive.org/web/20150410080456/http://www.ok-labs.com/products/ok-linux |archivedate=2015-04-10 |url-status=dead }}</ref>. «OK:Linux» была потомком ОС «[[:en:Wombat OS|Wombat OS]]»{{ref-en}}. Также фирма «OK Labs» распространяла паравиртуализированные версии [[Операционная система|операционных систем]] [[Symbian]] и Android.
 Фирма «OK Labs» приобрела у фирмы «NICTA» права на микроядро «seL4».
-В начале [[2012 год]]а было продано более 1.5 миллиарда устройств, оснащённых реализацией микроядра L4<ref name=OKL_PR>{{cite press release
+В начале [[2012 год]]а было продано '''более 1,5 миллиарда устройств''', оснащённых реализацией микроядра L4<ref name=OKL_PR>{{cite press release
  |title        = Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments
  |url          = http://www.ok-labs.com/releases/release/ok-labs-software-surpasses-milestone-of-1.5-billion-mobile-device-shipments
  |archive-url  = https://web.archive.org/web/20120211210405/http://www.ok-labs.com/releases/release/ok-labs-software-surpasses-milestone-of-1.5-billion-mobile-device-shipments
  |archive-date = 2012-02-11
- |dead-url     = yes
+ |url-status     = dead
- |date         = January 19, 2012
+ |date         = 2012-01-19
  |publisher    = [[Open Kernel Labs]]
+ |accessdate   = 2015-11-10
-}}</ref>. Большинство из этих устройств содержали микросхемы, реализующие [[Беспроводной модем|беспроводные модемы]] ({{lang-en|wireless modem}}) и выпущенные фирмой «Qualcomm».
+ }}</ref>. Большинство из этих устройств содержало микросхемы, реализующие [[Беспроводной модем|беспроводные модемы]] и было выпущено фирмой «[[Qualcomm]]».
 Реализация L4 также использовалась в автомобильных развлекательных системах<ref name="OKL_PR_auto">{{cite press release
- | title = Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems
+ |title       = Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems
- | url = http://www.ok-labs.com/releases/release/ok-labs-automotive-virtualization-selected-by-bosch-forinfotainment-systems
+ |url         = http://www.ok-labs.com/releases/release/ok-labs-automotive-virtualization-selected-by-bosch-forinfotainment-systems
- | date = [[27 марта]] [[2012 год]]а
+ |date        = 2012-03-27
- | publisher = [[:en:Open Kernel Labs|Open Kernel Labs]]
+ |publisher   = [[:en:Open Kernel Labs|Open Kernel Labs]]
+ |url-status    = dead
+ |archiveurl  = https://web.archive.org/web/20120702191648/http://www.ok-labs.com/releases/release/ok-labs-automotive-virtualization-selected-by-bosch-forinfotainment-systems
+ |archivedate = 2012-07-02
 }}</ref>.
-ОС, построенная на основе реализации L4, исполнялась процессором secure enclave, входящим в состав размещённой на кристалле электронной схемы [[Apple A7]]<ref>{{cite web|title=iOS Security|url=https://images.apple.com/privacy/docs/iOS_Security_Guide_Sept_2014.pdf}}</ref>. Эта же реализация L4 использовалась в проекте «Darbat» фирмы NICTA<ref>[http://www.ertos.nicta.com.au/software/darbat/ Darbat project].</ref>. Устройства, содержащие Apple A7, поставлялись с ОС [[iOS]]. По состоянию на 2015 год количество устройств с ОС iOS составляло примерно 310 миллионов<ref>[http://fortune.com/2014/10/28/forecast-apple-will-ship-310-million-ios-devices-in-2015/].</ref>.
+ОС, построенная на основе реализации L4, исполнялась процессором secure enclave, входящим в состав размещённой на кристалле электронной схемы [[Apple A7]]<ref>{{cite web|title=iOS Security|url=https://images.apple.com/privacy/docs/iOS_Security_Guide_Sept_2014.pdf|access-date=2017-09-28|archive-date=2014-09-23|archive-url=https://web.archive.org/web/20140923062211/http://images.apple.com/privacy/docs/iOS_Security_Guide_Sept_2014.pdf|url-status=live}}</ref>. Эта же реализация L4 использовалась в проекте «Darbat» фирмы NICTA<ref>[http://www.ertos.nicta.com.au/software/darbat/ Darbat project] {{Wayback|url=http://www.ertos.nicta.com.au/software/darbat/ |date=20131219064814 }}.</ref>. Устройства, содержащие Apple A7, поставлялись с ОС [[iOS]]. По состоянию на 2015 год количество устройств с ОС iOS составляло примерно 310 миллионов<ref>[http://fortune.com/2014/10/28/forecast-apple-will-ship-310-million-ios-devices-in-2015/] {{Wayback|url=http://fortune.com/2014/10/28/forecast-apple-will-ship-310-million-ios-devices-in-2015/ |date=20150715000100 }}.</ref>.
 === Верификация ===
 === seL4 ===
+В [[2006 год]]у началась разработка [[Микроядро#Третье поколение|микроядра третьего поколения]], получившего название «seL4»<ref>[http://seL4.systems] {{Wayback|url=http://sel4.systems/ |date=20220503040446 }}.</ref>. Разработка началась с нуля группой программистов из фирмы «NICTA». Цель: создание основы для построения безопасных и надёжных систем, способных удовлетворить современным требованиям безопасности, записанным, например, в документе «Общие критерии оценки защищённости информационных технологий». С самого начала код микроядра писался так, чтобы была возможность его верификации (проверки корректности). Верификация выполнялась с помощью языка [[Haskell]]: на языке Haskell записывались требования к микроядру (спецификация); объекты микроядра представлялись в виде объектов Haskell; работа с оборудованием эмулировалась<ref name=Derrin_EKCC_06>{{cite conference
-В [[2006 год]]у началась разработка [[Микроядро#Третье поколение|микроядра третьего поколения]], получившего название «seL4»<ref>[http://seL4.systems].</ref>. Разработка началась с нуля группой программистов из фирмы «NICTA». Цель: создание основы для построения безопасных и надёжных систем, способных удовлетворить современным требованиям безопасности, записанным, например, в документе «Общие критерии оценки защищённости информационных технологий». С самого начала код микроядра писался так, чтобы была возможность его верификации (проверки корректности). Верификация выполнялась с помощью языка [[Haskell]]: на языке Haskell записывались требования к микроядру (спецификация); объекты микроядра представлялись в виде объектов Haskell; работа с оборудованием эмулировалась<ref name=Derrin_EKCC_06>{{cite conference
  | first = Philip
  | last = Derrin
@@ Строка 330: / Строка 324: @@
  | author6 = Chakravarty, Manuel M. T.
  | title = Running the manual: an approach to high-assurance microkernel development
- | booktitle = ACM SIGPLAN Haskell Workshop
+ | book-title = ACM SIGPLAN Haskell Workshop
  | date = Сентябрь [[2006 год]]а
  | pages = 60‑71
  | location = [[Портленд (Орегон)|Portland]], [[Орегон|Oregon]], [[США|USA]]
- | url = https://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf <!-- (платный доступ) http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956 -->
+ | url = https://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf
+ | access-date = 2015-07-08
-}}</ref>. Чтобы иметь возможность получения информации о доступности объекта путём выполнения формального рассуждения, в seL4 использовался контроль доступа, основанный на capability-based security.
+ | archive-date = 2016-03-03
+ | archive-url = https://web.archive.org/web/20160303184034/https://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf
+ | url-status = live
+ }} {{Cite web |url=https://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf |title=Источник |access-date=2015-07-08 |archive-date=2016-03-03 |archive-url=https://web.archive.org/web/20160303184034/https://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf |url-status=unfit }}</ref>. Чтобы иметь возможность получения информации о доступности объекта путём выполнения формального рассуждения, в seL4 использовался контроль доступа, основанный на capability-based security.
-В [[2009 год]]у было завершено доказательство корректности кода микроядра seL4<ref Name="Klein_EHACDEEKNSTW_09">
+В [[2009 год]]у было завершено доказательство корректности кода микроядра seL4<ref Name="Klein_EHACDEEKNSTW_09">{{cite conference
-{{ cite conference
  | first1 = Gerwin
  | last1 = Klein
@@ Строка 367: / Строка 364: @@
  | last13 = Winwood
  | title = seL4: Formal verification of an OS kernel
- | booktitle = 22nd [[Ассоциация вычислительной техники|ACM]] [[:en:Symposium on Operating Systems Principles|symposium on operating system principles]]
+ | book-title = 22nd [[Ассоциация вычислительной техники|ACM]] [[:en:Symposium on Operating Systems Principles|symposium on operating system principles]]
  | pages =
  | date = Октябрь [[2009 год]]а
  | location = [[Big Sky, Montana|Big Sky]], [[Монтана|MT]], [[США|USA]]
  | doi =
  | url = http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
+ | access-date = 2015-07-08
-}}</ref>. Существование доказательства гарантировало соответствие реализации и спецификации, подтверждало отсутствие в реализации некоторых ошибок (например, отсутствие [[Взаимная блокировка|взаимных блокировок]], livelocks, [[Переполнение буфера|переполнений буферов]], арифметических исключений и случаев использования неинициализированных переменных). Микроядро seL4 было первым микроядром, предназначенным для ОС общего назначения и прошедшим верификацию<ref Name="Klein_EHACDEEKNSTW_09" />.
+ | archive-date = 2011-07-28
+ | archive-url = https://web.archive.org/web/20110728022610/http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
+ | url-status = live
+ }} {{Cite web |url=http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf |title=Источник |access-date=2015-07-08 |archive-date=2011-07-28 |archive-url=https://web.archive.org/web/20110728022610/http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf |url-status=unfit }}</ref>. Существование доказательства гарантировало соответствие реализации и спецификации, подтверждало отсутствие в реализации некоторых ошибок (например, отсутствие [[Взаимная блокировка|взаимных блокировок]], livelocks, [[Переполнение буфера|переполнений буферов]], арифметических исключений и случаев использования неинициализированных переменных). Микроядро seL4 было первым микроядром, предназначенным для ОС общего назначения и прошедшим верификацию<ref Name="Klein_EHACDEEKNSTW_09" />.
-В микроядре seL4 было реализовано нестандартное управление ресурсами ядра<ref Name="Elkaduwe_DE_08">
+В микроядре seL4 было реализовано нестандартное управление ресурсами ядра<ref Name="Elkaduwe_DE_08">{{cite conference
+ |first        = Dhammika
-{{ cite conference
+ |last         = Elkaduwe
- | first = Dhammika
+ |coauthors    = Derrin, Philip; Elphinstone, Kevin
- | last = Elkaduwe
+ |title        = Kernel design for isolation and assurance of physical memory
- | coauthors = Derrin, Philip; Elphinstone, Kevin
- | title = Kernel design for isolation and assurance of physical memory
+ |book-title   = 1st Workshop on Isolation and Integration in Embedded Systems
+ |date         = Апрель [[2008 год]]а
- | booktitle = 1st Workshop on Isolation and Integration in Embedded Systems
+ |location     = [[Глазго|Glasgow]], [[Великобритания|UK]]
- | date = Апрель [[2008 год]]а
+ |doi          = 10.1145/1435458
- | location = [[Глазго|Glasgow]], [[Великобритания|UK]]
+ |url          = http://ertos.nicta.com.au/publications/papers/Elkaduwe_DE_08.abstract
- | doi = 10.1145/1435458
+ |accessdate   = 2015-07-08
- | url = http://ertos.nicta.com.au/publications/papers/Elkaduwe_DE_08.abstract
+ |archive-date = 2010-04-24
-}}</ref>:
+ |archive-url  = https://web.archive.org/web/20100424035229/http://ertos.nicta.com.au/publications/papers/Elkaduwe_DE_08.abstract
+ |url-status   = dead
+}} {{Cite web |url=http://ertos.nicta.com.au/publications/papers/Elkaduwe_DE_08.abstract |title=Источник |access-date=2015-07-08 |archive-date=2010-04-24 |archive-url=https://web.archive.org/web/20100424035229/http://ertos.nicta.com.au/publications/papers/Elkaduwe_DE_08.abstract |url-status=dead }}</ref>:
 * управлением ресурсами ядра занимался компонент, работающий в пространстве пользователя;
 * механизм capability-based security использовался не только для контроля доступа к ресурсам пространства пользователя, но и для контроля доступа к ресурсам ядра.
-Нечто похожее было реализовано в экспериментальной ОС [[Barrelfish]]. Благодаря такому подходу к управлению ресурсами ядра появилась возможность выполнения рассуждения о изолированности свойств, а в дальнейшем было выполнено доказательство того, что микроядро seL4 обеспечивает целостность и конфиденциальность свойств<ref name="Klein_AEMSKH_14">{{cite journal
+Нечто похожее было реализовано в экспериментальной ОС [[Barrelfish]]. Благодаря такому подходу к управлению ресурсами ядра появилась возможность выполнения рассуждения о изолированности свойств, а в дальнейшем было выполнено доказательство того, что микроядро seL4 обеспечивает целостность и конфиденциальность свойств<ref name="Klein_AEMSKH_14">{{статья
+|заглавие=Comprehensive formal verification of an OS microkernel
- | last1 = Klein
+|издание=[[Ассоциация вычислительной техники|ACM]] Transactions on Computer Systems
- | first1 = Gerwin
+|том=32
- | last2 = Andronick
+|номер=1
- | first2 = June
+|страницы=2:1—2:70
- | last3 = Elphinstone
+|doi=10.1145/2560537
- | first3 = Kevin
+|язык=en
- | last4 = Murray
+|тип=journal
- | first4 = Toby
+|автор=Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot}}</ref>. Доказательство было выполнено для исходного кода.
- | last5 = Sewell
- | first5 = Thomas
- | last6 = Kolanski
- | first6 = Rafal
- | last7 = Heiser
- | first7 = Gernot
- | date = Февраль [[2014 год]]а
- | title = Comprehensive formal verification of an OS microkernel
- | journal = [[Ассоциация вычислительной техники|ACM]] Transactions on Computer Systems
- | volume = 32
- | issue = 1
- | pages = 2:1-2:70
- | doi = 10.1145/2560537
-}}</ref>. Доказательство было выполнено для исходного кода.
 Команда исследователей из фирмы NICTA доказала корректность трансляции текста с языка C на машинный код. Это позволило исключить компилятор из списка доверенного ПО и считать доказательство, выполненное для исходного кода микроядра, справедливым и для исполняемого файла микроядра.
@@ Строка 417: / Строка 408: @@
 Микроядро seL4 стало первым ядром, поддерживающим [[защищённый режим]], для которого анализ worst-case execution-time был выполнен полностью, а результаты этого анализа были опубликованы. Результаты анализа необходимы для использования микроядра в ОС жёсткого реального времени<ref name="Klein_AEMSKH_14" />.
-[[29 июля]] [[2014 год]]а фирмы NICTA и {{нп3|General Dynamics C4 Systems|General Dynamics C4 Systems|en|General Dynamics C4 Systems}} объявили о выпуске микроядра seL4 (включая все доказательства их корректности) под открытыми лицензиями<ref name=seL4_OSS>{{cite press release
+[[29 июля]] [[2014 год]]а фирмы NICTA и {{нп3|General Dynamics C4 Systems|General Dynamics C4 Systems|en|General Dynamics C4 Systems}} объявили о выпуске микроядра seL4 (включая все доказательства их корректности) под открытыми лицензиями<ref name=seL4_OSS>{{cite press release
  | title = Secure operating system developed by NICTA goes open source
  | url = http://www.nicta.com.au/media/current_releases2/secure_operating_system_developed_by_nicta_goes_open_source
- | date = [[29 июля]] [[2014 год]]а
+ | date = 2014-07-29
  | publisher = [[:en:NICTA|NICTA]]
+ | url-status = dead
-}}</ref>. Исходный код микроядра и доказательства поставлялись под лицензией GPL v2. Большинство библиотек и инструментов поставлялись под лицензией 2-clause BSD.
+ | accessdate = 2015-07-08
+ | archivedate = 2014-08-10
+ | archiveurl = https://web.archive.org/web/20140810035351/http://www.nicta.com.au/media/current_releases2/secure_operating_system_developed_by_nicta_goes_open_source
+ }}</ref>. Исходный код микроядра и доказательства поставлялись под лицензией GPL v2. Большинство библиотек и инструментов поставлялись под лицензией 2-clause BSD.
-Интересно заявление исследователей<ref>{{cite journal
+Интересно заявление исследователей<ref>{{статья
+|заглавие=Comprehensive formal verification of an OS microkernel
-| last1 = Klein
+|ссылка=http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf
-| first1 = Gerwin
+|издание=[[Ассоциация вычислительной техники|ACM]] Transactions on Computer Systems
-| last2 = Andronick
+|том=32
-| first2 = June
+|страницы=64
-| last3 = Elphinstone
+|doi=10.1145/2560537
-| first3 = Kevin
+|язык=en
-| last4 = Murray
+|тип=journal
-| first4 = Toby
+|автор=Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot
-| last5 = Sewell
+|год=2014
-| first5 = Thomas
+|archivedate=2014-08-03
-| last6 = Kolanski
+|archiveurl=https://web.archive.org/web/20140803122308/http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf
-| first6 = Rafal
-| last7 = Heiser
-| first7 = Gernot
-| year = 2014
-| title = Comprehensive formal verification of an OS microkernel
-| url = http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf
-| format = PDF
-| journal = [[Ассоциация вычислительной техники|ACM]] Transactions on Computer Systems
-| volume = 32
-| issue =
-| page = 64
-| doi = 10.1145/2560537
 }}</ref> о том, что стоимость выполнения верификации ПО ниже стоимости традиционного исследования ПО несмотря на то, что при верификации можно получить намного больше заслуживающей доверие информации.
-В августе 2012 года фирмы NICTA, {{нп3|Rockwell Collins|Rockwell Collins|en|Rockwell Collins}}, [[Galois Inc]], [[Boeing]] и [[Миннесотский университет|университет Миннесоты]] в рамках программы «High-assurance cyber military systems»<ref>[http://www.darpa.mil/Our_Work/I2O/Programs/High-Assurance_Cyber_Military_Systems_(HACMS).aspx High-assurance cyber military systems] {{webarchive|url=https://web.archive.org/web/20140808063932/http://www.darpa.mil/Our_Work/I2O/Programs/High-Assurance_Cyber_Military_Systems_%28HACMS%29.aspx |date=2014-08-08 }} (HACMS).</ref>, организованной агентством [[Агентство по перспективным оборонным научно-исследовательским разработкам США|DARPA]], приступили к разработке беспилотного летательного аппарата<ref>[http://ssrg.nicta.com.au/projects/TS/SMACCM/ Проект SMACCM] // Сайт фирмы {{нп3|NICTA|NICTA|en|NICTA}}. SMACCM — [[аббревиатура]] от {{lang-en|secure mathematically-assured composition of control models}}.</ref>. Основное требование к разработке — обеспечение высокой надёжности аппарата. У каждой из перечисленных фирм была своя роль в программе. Фирма NICTA была ответственна за разработку ОС и построила её на основе микроядра seL4. Ответственные задачи были реализованы в виде компонентов микроядра, а не ответственные — запускались под паравиртуализированной ОС Linux. Наработки программы планировалось использовать в вертолёте «NICTA Unmanned Little Bird», разработкой которого занималась фирма Boeing. Вертолёт должен был поддерживать как управление пилотом, так и беспилотный режим. В ноябре 2015 года было сообщено об успешной реализации<ref>[http://www.popmech.ru/technologies/231500-dronov-novogo-pokoleniya-vzlomat-nevozmozhno/ Дронов нового поколения взломать невозможно] // Журнал «[[Популярная механика]]». 12 ноября 2015 года.</ref>.
+В августе 2012 года фирмы NICTA, {{нп3|Rockwell Collins|Rockwell Collins|en|Rockwell Collins}}, [[Galois Inc]], [[Boeing]] и [[Миннесотский университет|университет Миннесоты]] в рамках программы по разработке высоконадежных военных кибер-систем<ref>[http://www.darpa.mil/Our_Work/I2O/Programs/High-Assurance_Cyber_Military_Systems_(HACMS).aspx High-assurance cyber military systems] {{webarchive|url=https://web.archive.org/web/20140808063932/http://www.darpa.mil/Our_Work/I2O/Programs/High-Assurance_Cyber_Military_Systems_%28HACMS%29.aspx |date=2014-08-08 }} (HACMS).</ref>, организованной агентством [[Агентство по перспективным оборонным научно-исследовательским разработкам США|DARPA]], приступили к разработке беспилотного летательного аппарата<ref>[http://ssrg.nicta.com.au/projects/TS/SMACCM/ Проект SMACCM] {{Wayback|url=http://ssrg.nicta.com.au/projects/TS/SMACCM/ |date=20150710072430 }} // Сайт фирмы {{нп3|NICTA|NICTA|en|NICTA}}. SMACCM — [[аббревиатура]] от {{lang-en|secure mathematically-assured composition of control models}}.</ref>. Основное требование к разработке — обеспечение высокой надёжности аппарата. У каждой из перечисленных фирм была своя роль в программе. Фирма NICTA была ответственна за разработку ОС и построила её на основе микроядра seL4. Ответственные задачи были реализованы в виде компонентов микроядра, а не ответственные — запускались под паравиртуализированной ОС Linux. Наработки программы планировалось использовать в вертолёте «NICTA Unmanned Little Bird», разработкой которого занималась фирма Boeing. Вертолёт должен был поддерживать как управление пилотом, так и беспилотный режим. В ноябре 2015 года было сообщено об успешной реализации<ref>[http://www.popmech.ru/technologies/231500-dronov-novogo-pokoleniya-vzlomat-nevozmozhno/ Дронов нового поколения взломать невозможно] {{Wayback|url=http://www.popmech.ru/technologies/231500-dronov-novogo-pokoleniya-vzlomat-nevozmozhno/ |date=20151118041113 }} // Журнал «[[Популярная механика]]». 12 ноября 2015 года.</ref>.
 == Другие исследования и разработки ==
+'''Hurd/L4'''. В ноябре [[2000 год]]а для обсуждения идеи [[Портирование программного обеспечения|портирования]] ядра «[[GNU Hurd]]» на микроядро L4 был создан список рассылки «l4-hurd». Портирование осуществлялось в течение 2002‑2004 годов, результат получил название «Hurd/L4». Реализация «Hurd/L4» не была окончена. В 2005 году проект был остановлен<ref>[https://www.gnu.org/software/hurd/history/port_to_another_microkernel.html История GNU Hurd. Портирование на другое микроядро] {{Wayback|url=https://www.gnu.org/software/hurd/history/port_to_another_microkernel.html |date=20170308144918 }}{{ref-en}}.</ref>.
+'''Osker''' — операционная система, реализующая L4 и написанная на языке Haskell в [[2005 год]]у. Цель проекта: проверка возможности реализации ОС на функциональном языке (а не исследовании микроядра)<ref>{{статья
-'''Hurd/L4'''. В ноябре [[2000 год]]а для обсуждения идеи [[Портирование программного обеспечения|портирования]] ядра «[[GNU Hurd]]» на микроядро L4 был создан список рассылки «l4-hurd». Портирование осуществлялось в течение 2002‑2004 годов, результат получил название «Hurd/L4». Реализация «Hurd/L4» не была окончена. В 2005 году проект был остановлен<ref>[https://www.gnu.org/software/hurd/history/port_to_another_microkernel.html История GNU Hurd. Портирование на другое микроядро]{{ref-en}}.</ref>.
+|заглавие=A principled approach to operating system construction in Haskell
+|ссылка=http://web.cecs.pdx.edu/~apt/icfp05.pdf
-'''[[Osker]]''' — операционная система, реализующая L4 и написанная на языке Haskell в [[2005 год]]у. Цель проекта: проверка возможности реализации ОС на функциональном языке (а не исследовании микроядра)<ref>{{Cite journal
+|издание=Proceedings of the tenth ACM SIGPLAN international conference on functional programming
- | title = A principled approach to operating system construction in Haskell
+|страницы=116—128
- | url = http://web.cecs.pdx.edu/~apt/icfp05.pdf
+|issn=0362-1340
- | year = 2005
+|doi=10.1145/1090189.1086380
- | journal = Proceedings of the tenth ACM SIGPLAN international conference on functional programming
+|accessdate=2010-06-24
- | pages = 116–128
+|том=40
- | last1 = Hallgren
+|цитата=<!--None-->
- | first1 = T.
+|номер=9
- | last2 = Jones
+|язык=en
- | first2 = M. P.
+|тип=journal
- | last3 = Leslie
+|автор=Hallgren, T.; Jones, M. P.; Leslie, R.; Tolmach, A.
- | first3 = R.
+|год=2005
- | last4 = Tolmach
+|archivedate=2010-06-15
- | first4 = A.
+|archiveurl=https://web.archive.org/web/20100615164444/http://web.cecs.pdx.edu/~apt/icfp05.pdf
- | issn = 0362-1340
- | doi=10.1145/1090189.1086380
- | accessdate = 2010-06-24
- | volume = 40
- | postscript = <!--None-->
- | issue = 9
 }}</ref>.
-'''[[Codezero]]''' — реализация микроядра L4 для встраиваемых систем, ставшая общедоступной летом [[2009 год]]а<ref>[http://genode.org/documentation/platforms/codezero Codezero] на сайте genode.org.</ref>. Создана разработчиками британской фирмы «B Labs» с нуля. Код составлялся на языке C. Реализация поддерживает процессоры архитектуры [[ARM (архитектура)|ARM]], реализует [[Гипервизор#Автономный гипервизор (Тип 1,X)|гипервизор первого порядка]], поддерживает виртуализацию ОС Linux и Android<ref>[https://web.archive.org/web/20120924211055/http://dev.b-labs.com/ dev.b-labs.com] // [[archive.org]].</ref><ref>[http://www.l4dev.org/ Официальный сайт проекта Codezero].</ref>. Несмотря на заявление о поставке кода под лицензией GPL v3, скачать код с официального сайта нельзя.
+'''Codezero''' — реализация микроядра L4 для встраиваемых систем, ставшая общедоступной летом [[2009 год]]а<ref>[http://genode.org/documentation/platforms/codezero Codezero] {{Wayback|url=http://genode.org/documentation/platforms/codezero |date=20150709081430 }} на сайте genode.org.</ref>. Создана разработчиками британской фирмы «B Labs» с нуля. Код составлялся на языке C. Реализация поддерживает процессоры архитектуры [[ARM (архитектура)|ARM]], реализует [[Гипервизор#Автономный гипервизор (Тип 1,X)|гипервизор первого порядка]], поддерживает виртуализацию ОС Linux и Android<ref>[https://web.archive.org/web/20120924211055/http://dev.b-labs.com/ dev.b-labs.com] // [[archive.org]].</ref><ref>[http://www.l4dev.org/ Официальный сайт проекта Codezero] {{Wayback|url=http://www.l4dev.org/ |date=20150709095438 }}.</ref>. Несмотря на заявление о поставке кода под лицензией GPL v3, скачать код с официального сайта нельзя.
-'''F9''' — реализация микроядра L4, ставшая общедоступной в июле [[2013 год]]а<ref>[https://github.com/f9micro Репозиторий проекта F9] // [[github|github.com]].</ref>. Написана с нуля на языке C. Предназначена для встраиваемых систем. Поддерживает серии процессоров [[ARM (архитектура)#ARM Cortex-M)|Cortex-M]] архитектуры ARM. Код поставляется под лицензией BSD.
+'''F9''' — реализация микроядра L4, ставшая общедоступной в июле [[2013 год]]а<ref>[https://github.com/f9micro Репозиторий проекта F9] {{Wayback|url=https://github.com/f9micro |date=20170305090216 }} // [[github|github.com]].</ref>. Написана с нуля на языке C. Предназначена для встраиваемых систем. Поддерживает серии процессоров [[ARM (архитектура)#ARM Cortex-M)|Cortex-M]] архитектуры ARM. Код поставляется под лицензией BSD.
 '''Fiasco.OC''' — [[Микроядро#Поколения|микроядро третьего поколения]], созданное на основе микроядра «L4/Fiasco». Реализует механизм {{нп3|Capability-based security|Capability-based security|en|Capability-based security}}, поддерживает многоядерные процессоры и [[Аппаратная виртуализация|аппаратную виртуализацию]]<ref name=Peter_Schild_VTDS_09>{{cite conference
@@ Строка 489: / Строка 469: @@
  | coauthors = Lackorzynski, Adam; Warg, Alexander
  | title = Virtual Machines Jailed - Virtualization in Systems with Small Trusted Computing Bases
- | booktitle = VTDS'09: Workshop on Virtualization Technology for Dependable Systems
+ | book-title = VTDS'09: Workshop on Virtualization Technology for Dependable Systems
  | date = Март [[2009 год]]а
  | location = [[Нюрнберг|Nuremberg]], [[Германия|Germany]]
@@ Строка 499: / Строка 479: @@
 Каркас L4Re и микроядро «Fiasco.OC» поддерживали процессоры архитектур x86 (IA-32 и AMD64), ARM и [[PowerPC]] (WiP).
-'''L4Linux''' — подсистема для запуска ОС Linux поверх микроядра «Fiasco.OC» с помощью паравиртуализации<ref>[http://os.inf.tu-dresden.de/L4/LinuxOnL4 L4Linux].</ref>. Ранее вместо пары «Fiasco.OC» — L4Re использовалась пара «L4/Fiasco» — L4Env.
+'''L4Linux''' — подсистема для запуска ОС Linux поверх микроядра «Fiasco.OC» с помощью паравиртуализации<ref>[http://os.inf.tu-dresden.de/L4/LinuxOnL4 L4Linux] {{Wayback|url=http://os.inf.tu-dresden.de/L4/LinuxOnL4 |date=20150707011210 }}.</ref>. Ранее вместо пары «Fiasco.OC» — L4Re использовалась пара «L4/Fiasco» — L4Env.
 '''NOVA''' ({{lang-en|the '''N'''OVA '''O'''S '''v'''irtualization '''a'''rchitecture}}) — исследовательский проект, созданный с целью создания безопасного и эффективного окружения для виртуализации<ref name=Steinberg_Kauer_EuroSys_2010>{{cite conference
@@ Строка 507: / Строка 487: @@
  | last2  = Bernhard
  | title  = NOVA: A Microhypervisor-Based Secure Virtualization Architecture
- | booktitle = EuroSys '10: Proceedings of the 5th European Conference on Computer Systems
+ | book-title = EuroSys '10: Proceedings of the 5th European Conference on Computer Systems
  | date = Апрель [[2010 год]]а
  | location = [[Париж|Paris]], [[Франция|France]]
@@ Строка 516: / Строка 496: @@
  | last2  = Bernhard
  | title  = Towards a Scalable Multiprocessor User-level Environment
- | booktitle = IIDS'10: Workshop on Isolation and Integration for Dependable Systems
+ | book-title = IIDS'10: Workshop on Isolation and Integration for Dependable Systems
  | date = Апрель [[2010 год]]а
  | location = [[Париж|Paris]], [[Франция|France]]
-}}</ref><ref>[http://hypervisor.org/ Проект Nova]. Официальный сайт.</ref> с небольшим списком доверенного ПО ({{lang-en|trusted computing base}}). В состав NOVA входят:
+}}</ref><ref>[http://hypervisor.org/ Проект Nova] {{Wayback|url=http://hypervisor.org/ |date=20150624052907 }}. Официальный сайт.</ref> с небольшим списком доверенного ПО ({{lang-en|trusted computing base}}). В состав NOVA входят:
 :* микроядро, реализующее L4 и гипервизор первого порядка ({{lang-en|baremetal hypervisor}});
-:* VMM Vancouver — компонент микроядра (процесс), работающий в пространстве пользователя, занимающийся обслуживанием (эмуляцией оборудования) одной виртуальной машины и лишённый привилегий. На каждую виртуальную машину запускалось по одному VMM. VMM Vancouver входит в состав NUL и может быть заменён на VMM Seoul. VMM Seoul<ref>[https://github.com/TUD-OS/seoul VMM Seoul] // [[github|github.com]]</ref> создан на основе VMM Vancouver;
+:* VMM Vancouver — компонент микроядра (процесс), работающий в пространстве пользователя, занимающийся обслуживанием (эмуляцией оборудования) одной виртуальной машины и лишённый привилегий. На каждую виртуальную машину запускалось по одному VMM. VMM Vancouver входит в состав NUL и может быть заменён на VMM Seoul. VMM Seoul<ref>[https://github.com/TUD-OS/seoul VMM Seoul] {{Wayback|url=https://github.com/TUD-OS/seoul |date=20180611031852 }} // [[github|github.com]]</ref> создан на основе VMM Vancouver;
 :* NUL ({{lang-en|'''N'''OVA '''u'''ser-'''l'''evel environment}}) — некоторые компоненты микроядра, работающие в пространстве пользователя (VMM Vancouver, драйверы устройств (например, сетевой карты); partition manager; компоненты, предназначенные для управления памятью, вводом-выводом; компоненты, реализующие стеки [[TCP/IP]], [[USB]] и др.). NUL может быть заменён на genode или NRE. NRE ({{lang-en|'''N'''OVA '''r'''untime '''e'''nvironment}}) — потомок NUL.
 Проект NOVA поддерживал многоядерные процессоры архитектуры x86. Для запуска под управлением микрогипервизора (гипервизора, построенного на микроядре) NOVA гостевая ОС должна поддерживать [[Аппаратная виртуализация#VT-x|Intel VT-x]] или [[Аппаратная виртуализация#AMD virtualization (AMD-V)|AMD-V]]. Исходный код поставлялся под лицензией GPL v2.
-'''[[Xameleon]]''' — ОС на микроядре L4<ref>[http://l4os.ru/ l4os.ru]. Официальный сайт проекта Xameleon.</ref>. Проект основал в [[2001 год]]у единственный разработчик [[Мандрыкин, Алексей|Алексей Мандрыкин]] (род. [[19 января]] [[1973 год]]а). Изначально ОС была построена поверх микроядра «[[#Микроядро L4/Fiasco|L4/Fiasco]]». Позднее автор перевёл ОС на микроядро «[[#Микроядро L4Ka::Pistachio|L4Ka::Pistachio]]». Исходный код ОС закрыт.
+'''Xameleon''' — ОС на микроядре L4<ref>[http://l4os.ru/ l4os.ru] {{Wayback|url=http://l4os.ru/ |date=20110209031410 }}. Официальный сайт проекта Xameleon.</ref>. Проект основал в [[2001 год]]у единственный разработчик [[Мандрыкин, Алексей|Алексей Мандрыкин]] (род. [[19 января]] [[1973 год]]а). Изначально ОС была построена поверх микроядра «[[#Микроядро L4/Fiasco|L4/Fiasco]]». Позднее автор перевёл ОС на микроядро «[[#Микроядро L4Ka::Pistachio|L4Ka::Pistachio]]». Исходный код ОС закрыт.
+'''WrmOS''' — операционная система реального времени (РТОС) с открытым исходным кодом, основанная на микроядре L4. [https://wrmlab.org/projects/wrmos WrmOS] имеет собственную реализацию ядра, стандартных библиотек и сетевого стэка. Поддержаны следующие процессорные архитектуры — SPARC, ARM, x86, x86_64. Ядро WrmOS базируется на документе [https://web.archive.org/web/20150226070705/http://l4hq.org/docs/manuals/l4-x2-r6.pdf L4 Kernel Reference Manual Version X.2]. Существует паравиртуализированное ядро Linux ([https://wrmlab.org/projects/w4linux w4linux]) работающее поверх WrmOS.
-== Список литературы ==
+== Примечания ==
+{{примечания|2}}
+== Литература ==
 * [[:en:Jochen Liedtke|Jochen Liedtke]], Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. ''[http://portal.acm.org/citation.cfm?id=122124&dl=ACM&coll=&CFID=15151515&CFTOKEN=6184618 Two years of experience with a μ-Kernel based OS]''. [[Ассоциация вычислительной техники|ACM]] Press. 1991
 * {{Cite conference
- | first = Jochen
+ |first       = Jochen
- | last = Liedtke
+ |last        = Liedtke
- | authorlink = Jochen Liedtke
+ |authorlink  = Jochen Liedtke
- | coauthors = Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar
+ |coauthors   = Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar
- | date = 2000-10-22
+ |date        = 2000-10-22
- | title = Stub-Code Performance is Becoming Important
+ |title       = Stub-Code Performance is Becoming Important
- | booktitle = In Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), [[Сан-Диего|San Diego]], [[Калифорния|CA]], October [[2000 год|2000]]
+ |book-title   = In Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), [[Сан-Диего|San Diego]], [[Калифорния|CA]], October [[2000 год|2000]]
- | url = http://l4ka.org/publications/
+ |url         = http://l4ka.org/publications/
- | format = PDF
+ |format      = PDF
- | accessdate = 2006-09-05
+ |accessdate  = 2006-09-05
+ |archiveurl  = https://web.archive.org/web/20060905181634/http://www.l4ka.org/publications/
-}} (о микроядре L4 и компиляторе).
+ |archivedate = 2006-09-05
+}} {{Wayback|url=http://l4ka.org/publications/ |date=20060905181634 }} (о микроядре L4 и компиляторе).
 * Cheng Guanghui, Nicholas Mc Guire. ''[https://web.archive.org/web/20120327161621/http://dslab.lzu.edu.cn:8080/docs/publications/l4_kickstart.pdf L4/Fiasco/L4Linux Kickstart]'', Distributed & Embedded Systems Lab — [[Университет Ланьчжоу|Lanzhou University]].
 * {{Cite conference
@@ Строка 551: / Строка 537: @@
  | date = Октябрь [[2014 год]]а
  | title = From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?
- | booktitle = 24th [[Ассоциация вычислительной техники|ACM]] SIGOPS Symposium on Operating Systems Principles
+ | book-title = 24th [[Ассоциация вычислительной техники|ACM]] SIGOPS Symposium on Operating Systems Principles
  | location = [[:en:Farmington, Pennsylvania|Farmington]], [[Пенсильвания|PA]], [[США|USA]]
  | pages = 133‑150
  | url = http://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml
-}} Эволюция архитектуры L4 и подходы к реализации.
+ }} {{Wayback|url=http://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml |date=20140812065831 }} Эволюция архитектуры L4 и подходы к реализации.
 == Ссылки ==
+* [https://web.archive.org/web/20140830054545/http://www.l4hq.org/ L4Hq]: L4 headquarters, сайт сообщества о реализациях L4.
-* [http://www.l4hq.org/ L4Hq]: L4 headquarters, сайт сообщества о реализациях L4.
 * [http://os.inf.tu-dresden.de/L4/ Семейство микроядер L4]. Обзор реализаций L4, документации и проектов.
 * [http://wiki.tudos.org/ Официальная вики проекта TUD:OS].
 * [http://www.l4ka.org L4Ka]. Реализации L4 «L4Ka::Pistachio» и «L4Ka::Hazelnut».
 * [http://www.cse.unsw.edu.au/~disy/L4/ UNSW]. Реализация L4 для процессоров [[DEC Alpha]] и процессоров архитектуры [[MIPS (архитектура)|MIPS]].
-* [http://okl4.org/ OKL4]. Коммерческая реализация L4 от фирмы «[http://www.ok-labs.com/ Open Kernel Labs]».
+* [https://web.archive.org/web/20080820043831/http://okl4.org/ OKL4]. Коммерческая реализация L4 от фирмы «[https://web.archive.org/web/20070303102514/http://ok-labs.com/ Open Kernel Labs]».
-* [http://ertos.nicta.com.au/research/l4/ Реализация L4 от фирмы «NICTA»]. Обзоры исследований и публикации.
+* [https://web.archive.org/web/20140717185304/http://www.ertos.nicta.com.au/research/l4/ Реализация L4 от фирмы «NICTA»]. Обзоры исследований и публикации.
 * {{anchor|genode}}[http://genode.org/about/index Genode Operating System Framework]. Каркас для построения операционных систем, разработка сообщества L4.
 * [https://os.inf.tu-dresden.de/L4/l3.html Официальная страница, посвящённая ядру L3]
+* [https://web.archive.org/web/20190814094647/http://ru2.halfos.ru/core/articles/core003.html Микроядро L4 как основа ядра ОС]
-== Примечания ==
-{{примечания}}
 [[Категория:Микроядра]]

L4
Семейство микроядер L4
Тип	Микроядро
Автор	Йохен Лидтке
Разработчик	Йохен Лидтке
Написана на	язык ассемблера
Сайт	l4hq.org

L4 (микроядро): различия между версиями

Текущая версия от 07:33, 26 января 2024

История

L1

L2

L3

L4

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

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

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

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

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

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

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

Верификация

seL4

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

Примечания

Литература

Ссылки

Навигация

Поиск