микроядра и FOSDEM’13

        Приветствую. Микроядра редко появляются на Хабре, но на неделе был  топик о GNU/Hurd ^[1], где вспоминали  разные микроядра и известные проекты. Было сказано много неточностей, так что я решил рассказать о том, как обстоят дела в отрасли с нашей точки зрения. Дело в том, что мы активно участвуем в развитии проектов Fiasco.OC и Genode и ведем разработки на их основе, так что нам есть о чем рассказать.

Немного истории

      Я думаю, ядро Mach достаточно известно, так что я коснусь его совсем вскользь. Разрабатывалось оно в Carnegie Mellon University в конце 80-ых — начале 90-ых, после закрытия проекта в CMU развивалось в Utah University и тогда оно, по-моему, уже называлось GNU/Mach. GNU/Mach является частью OS GNU/Hurd. Это довольно медленное микроядро, оно поддерживает только x86.
Йохен Лидтке (Jochen Liedtke ^[2]) в конце 90ых предложил новую, оптимизированную архитектуру микроядра, сначала L3, потом L4. К сожалению, в 2001 году он попал в аварию и умер. L4 это идеология и она оформлена в документах L4 eXperimental reference manual. Сейчас последняя версия X.2 rev.7 ^[3] Любой желающий может прочитать этот документ и запрограммировать «свое» микроядро архитектуры L4. Как следствие, появилось довольно много разных микроядерных проектов в 00ых.

Наиболее известные проекты.

      Проектов было много, далеко не все дожили до настоящего времени, расскажу о наиболее известных из ныне существующих
1. L4Ka::Pistachio, Karlsruhe Institute of Technology
Это команда Йохена Лидтке, они разрабатывали микроядро и окружение. В настоящее время эта команда не развивает проект L4Ka, но этот проект породил множество других.
2. Проекты NICTA Group
      NICTA Group ^[4] — Information and Communications Technology (ICT) Research Centre of Excellence. Эта организация занимается проектами в области системного программирования, распознавания образов, искусственного интеллекта, какого-то нано. В общем, самыми популярными направлениями CS, которые очень востребованы в 00ых и в будущем. При этом эта организация не просто вкладывает в ресеч-проекты, она проводит их от идеи и ресеча в университете вплоть до продуктов и продажи компании.
      Очень показательна в этом плане история развития микроядра L4Ka. Сначала был исследовательский проект NICTA::Pistachio-embedded (созданный на основе микроядра L4Ka::Pistachio из KIT), потом внутри NICTA была создана компания OKL (Open Kernel Lab), которая занималась разработкой продуктов на основе микроядра Pistachio. Потом они сделали свой продукт — микроядро OKL4 и в районе 2007 года заключили контракт с Qualcomm, с тех пор в смартфонах на чипах Qualcomm присутствует микроядро. В недавно утекших даташитах Qualcomm есть например описание апи L4 (хотя я не уверен, видел мельком). Совсем недавно компания OKL4 была продана ^[5] General Dynamics.
        L4.verified — формально верифицированное ядро на архитектуре L4. Это научная разработка NICTA Group, можно предположить, что трек у этого проекта будет как и OKL4. Основная идея этого проекта математически доказать корректность реализации ядра. Дело в том, что микроядра в отличие от монолитно-модульных монстров типа GNU/Linux маленькие, и они могут быть формально верифицированы, то есть по каждой строчке кода написана теорема, и, доказывая все теоремы, доказывается соответствие чего-то чему-то. В микроядре L4.verified доказывается соответствие реализации модели, отсутствие вечных циклов и еще некоторых вещей. Стоимость этого исследования была порядка 6 млн$, длился проект 7 лет. Объем работы — 25 человеко-лет. Это колоссальная и очень интересная работа. Его очевидное применение — война, безопасность.
seL4 это операционная система, ориентированная на безопасность, не знаю с верифицированным ли ядром или нет. На сайте NICTA можно скачать бинари.
3. MINIX3
        Это проект команды Эндрю Таненбаума. Основной упор в микроядре MINIX3 это отказоустойчивость и десктопное применение. Я мало чего знаю об этом проекте, но на прошлом FOSDEM присутствовал кто-то из разработчиков, и в России есть небольшое сообщество энтузиастов.
4. HelenOS ^[6]
Это разработка студентов Faculty of Mathematics and Physics at Charles University in Prague. Этот проект развивается довольно долго, ядро поддерживает современные аппаратные платформы. А еще в 2012 году они участвовали в GSoC. В ядре изначально были архитектурные недостатки, например ядро было не до конца микро — часть драйвера устройств все же находилась в ядре. Сейчас, насколько мне известно, этот архитектурный недостаток ликвидирован. Мне лично не нравится то, что позиционируясь как general purpose OS, они не поддерживают нормальных драйверов.
5. Проекты TU Dresden
        В Техническом Университете Дрездена есть научная группа Профессора Hermann Härtig ^[7]. Он публиковался и работал совместно с Йохеном Лидтке, и студенты под его управлением разработали много интересных проектов в области операционных систем. Старые ядра — L4/Fiasco (первое ядро L4 в TUD), VFiasco (попытка верифицировать Fiasco, 2005 год)
Современные ядра:
        Fiasco.OC ^[8] — микроядро, написанное на C++, построенное по концепции Everything Is Object. Поддерживает ARM, x86, ppc, sparc v8. Стартует на современных платформах типа панды. Мы активно участвуем в развитии этого проекта. Авторы ядра (Adam Lackorzynski и Alexander Warg) насколько мне известно пару месяцев назад ушли из TUD и организовали свой стартап по поддержке и развитию микроядер.
        NOVA ^[9] — это микрогипервизор. Его разрабатывал Udo Steinberg, сейчас он продолжает развивать этот гипервизор в Intel.
Как вы понимаете, микроядра сами по себе не функциональны, так что TUD разработало окружение для микроядер: L4Re ^[10] — L4 Runtime Environment. Это набор библиотек и прикладного ПО, которое можно запускать поверх микроядер Fiasco и Fiasco.OC. В его состав входят паравиртуализированный L4Linux, обертка для использования Linux драйверов DDEKit (такой DDEKit кстати есть и в GNU/Hurd). Это позволяет легко использовать существующие ПО и использовать микроядро в коммерческих проектах. Это очень быстрый «вход» в микроядра, что мне кажется очень важным. Негативным моментом является то, что TU Dresden крайне редко выкладывает обновления и практически отсутствует работа комьюнити. Так что мы например держим наработки и свою версию l4Linux в github.
        Genode framwork ^[11] — Проект Norman Feske и Christian Helmuth. Они выпускники TU Dresden и раньше работали над разработкой безопасной графической подсистемы и развитием микроядер. Сейчас у них свой стартап, они разрабатывают фреймверк для разных микроядерных (не только) операционных систем. У Genode в отличие от TUD регулярные релизы и roadmap, Исходники лежат в github и все желающие могут принять участие в его разработке. Мы так же развиваем этот проект, для нас интересна связка Fiasco.OC + Genode framework.
        Иными словами, микроядерные проекты из TUD вот вот переходят из состояния «экспериментальные студенческие проекты» в реальный продукт, на котором можно строить свои продукты. Так что рост сообщества и вовлеченность как раз то что сейчас нужно.

6. Singularity

Про этот проект уже писали ^[12], затрагивать не буду

FOSDEM

      В этом году мы принимали участие в FOSDEM и я рассказывал ^[13] о нашем опыте использования микроядерных ОС. Я не присутствовал на остальных сессиях, так как в первый день присутствовал на нашем devroom, а на следующий день у нас на пол дня была demo section, где мы демонстрировали прошивку для доверенного телефона на микроядре, l4linux и Genode. В devroom присутствовали проекты:
    GNU/Hurd, о нем рассказывал Samuel Thibault, самый активный как мне кажется разработчик этого проекта. Он выступал первый, и присутствовал на панельной дискуссии.
Genode labs, рассказывали о своей работе за последний год. Они портировали ^[14] Genode framework на pandaboard в 2012 году. Мне кажется это очень знаково, и крайне полезно для развития фреймверка и микроядер, так как добавляет популярности. В порте на pandaboard мы не принимали участие, хотя мы были первые, кто запустил Genode на реальном ARM based железе.
    Также присутствовали HelenOSовцы, они рассказывали о своих планах на следующий год, о том что уже поддерживается в HelenOS.
    Был Udo и рассказывал о NOVA, о том что потеря производительности у этого гипервизора ниже чем у Xen и eSXI, кроме того этот гипервизор поддерживается в Genode, то есть виртуальные машины можно запускать параллельно с прикладным ПО поверх микроядра.
    Еще были новые ребята какие-то, рассказывали о DSL, но это слабое отношение имеет к микроядрам.
Из TUD присутсвовал Bjoern Doebel ^[15], он рассказывал о своем Open Source фреймверке для репликации. Это его исследовательский проект.
    На демо секции присутствовал один молодой человек из TU Berlin. В TU Berlin есть кафедра T Lab, которая занимается RnD в области ИБ. В частности они разрабатывают доверенный телефон на паравиртуализированном L4Android для Deutsche Telecom
Доклады мне понравились, и, кстати, в следующем году организуем Microkernels and Component-based OS devroom мы.

P/S/ А еще, в прошлом году мы проводили ^[16] летнюю школу системного программирования, а сейчас ищем студентов, тех кто хочет найти себя в области Computer Science и системного программирования. Для того, чтобы попасть к нам в команду, нужно посмотреть первые три лекции (1 ^[17],2 ^[18],3 ^[19]) и выполнить из них задания. Решение нужно выложить на github и прислать мне ссылку на почту sartakov@ksyslabs.org.

P/P/S/ Если интересно, могу рассказать об основных трендах и челенджах в области системмного программирования последних лет.

P/P/P/S В этом году мы готовим новую школу, но об этом потом

Автор: sartakov

Источник ^[20]