Хайзер, Гернот

Материал из Циклопедии
Перейти к навигации Перейти к поиску

Гернот Хайзер

англ. Gernot Heiser
Файл:GH 29 crop.jpg
Гернот Хайзер выступает на выставке исследований UNSW CSE 25 октября 2022 года


Дата рождения
1957




Род деятельности
учёный в области информатики





Награды и премии

Член Леопольдины (2023)
Член Королевского общества Нового Южного Уэльса (2022)
Зал славы ACM SIGOPS (2019)
Член Австралийской академии технологических наук и инженерии (2016)
Член IEEE (2016)
Член ACM (2014)

Сайт

gernot-heiser.org

Ге́рнот Ха́йзер (англ. Gernot Heiser; [Нет даты!]) — немецко-австралийский учёный в области информатики. Известен исследованиями и коммерциализацией операционных систем, в частности разработкой микроядра seL4.

Биография[править]

Хайзер получил абитур в 1976 году в гимназии Маркгрефлер в Мюлльхайме. Окончил Фрайбургский университет (бакалавр), Университет Брока (магистр) и Швейцарскую высшую техническую школу Цюриха (доктор философии).

В 1991 году Хайзер присоединился к Школе компьютерных наук и инженерии Университета Нового Южного Уэльса (UNSW Sydney) в качестве преподавателя. В 2002 году получил звание профессора. Является профессором (Scientia Professor) и заведующим кафедрой операционных систем имени Джона Лайонса в UNSW Sydney, где руководит исследовательской группой Trustworthy Systems (TS).

В 2002 году он стал одним из первых руководителей программ в созданной исследовательской организации NICTA, возглавив программу Embedded, Real-Time and Operating Systems (ERTOS). После реорганизации в 2011 году ERTOS стала Исследовательской группой программных систем (SSRG) под его руководством. Когда NICTA была поглощена CSIRO в 2016 году, Хайзер отошёл от управления группой, получившей название Trustworthy Systems (TS). В 2021 году CSIRO отказалась от TS, после чего Хайзер вернул группу в UNSW и вновь возглавил её.

С апреля 2020 года Хайзер является председателем-основателем фонда seL4 Foundation. Был основателем, техническим директором и директором компании Open Kernel Labs.

Исследования[править]

Исследования Хайзера сосредоточены на микроядрах, системах на их основе и виртуальных машинах, с акцентом на производительность и надёжность.

Его группа разработала Mungi, операционную систему с единым адресным пространством[1] для кластеров 64-битных компьютеров, а также реализации микроядра L4 с быстрым межпроцессным взаимодействием[2]. Его команда Gelato@UNSW была одним из основателей Gelato Federation и занималась производительностью и масштабируемостью Linux на Itanium. Они установили теоретические и практические пределы производительности передачи сообщений при межпроцессном взаимодействии (IPC) на Itanium[3].

После перехода в NICTA в 2002 году его исследования сместились в сторону встраиваемых систем с целью повышения безопасности и надёжности с использованием микроядерных технологий[4]. Это привело к разработке нового микроядра seL4 и его формальной верификации, которая стала первым полным доказательством функциональной корректности ядра операционной системы общего назначения[5].

Работа Хайзера над виртуализацией была мотивирована необходимостью обеспечения полноценной среды ОС на его микроядрах. Проект Wombat развивал подход проекта L4Linux в Дрездене, представляя собой мультиархитектурный паравиртуализированный Linux для оборудования x86, ARM и MIPS. Позже Wombat стал основой для гипервизора OKL4 его компании Open Kernel Labs (OK Labs). Стремление снизить инженерные затраты на паравиртуализацию привело к разработке подхода soft layering для автоматизированной паравиртуализации, продемонстрированного на оборудовании x86 и Itanium[6]. Его работа над виртуальным неоднородным доступом к памяти (vNUMA) продемонстрировала гипервизор, представляющий распределённую систему как мультипроцессор с общей памятью, что может служить моделью для многоядерных чипов[7].

Драйверы устройств — ещё одно направление его работы. Он продемонстрировал драйверы пользовательского режима с накладными расходами производительности менее 10 %[8], подход к разработке, устраняющий большинство типичных ошибок драйверов на этапе проектирования[9], драйверы, созданные на основе тестовых стендов устройств[10], и возможность автоматической генерации драйверов из формальных спецификаций[11]. Он также проводил исследования по управлению энергопотреблением на уровне операционной системы[12].

После ухода из OK Labs в 2010 году Хайзер сосредоточился на seL4 и системах высокой степени надёжности на её основе. Среди достижений — полный анализ наихудшего времени выполнения (WCET) для seL4, который стал первым подобным анализом для ОС в защищённом режиме[13][14]. Его работа по расширению функциональности seL4 для поддержки систем смешанной критичности (MCS) привела к тому, что время стало первоклассным ресурсом в системе мандатного управления доступом seL4[15].

Исследуя микроархитектурные временные каналы, в 2015 году он продемонстрировал первую практическую атаку по стороннему каналу времени между ядрами[16]. Это привело к работе по систематическому предотвращению утечек через временные каналы и предложению механизмов для достижения этой цели, названных time protection[17].

Ранее он также работал над моделированием полупроводниковых приборов, где впервые применил многомерное моделирование для оптимизации кремниевых солнечных элементов[18].

Награды и премии[править]

  • Член Леопольдины (2023)
  • Член Королевского общества Нового Южного Уэльса (2022)
  • Выдающийся спикер ACM (2021)[19]
  • Зал славы ACM SIGOPS (2019) за статью «seL4: Formal Verification of an OS Kernel»[20][5]
  • Член Австралийской академии технологических наук и инженерии (2016)[21]
  • Член IEEE (2016)[22]
  • Исследователь года в области ИКТ по версии Австралийского компьютерного общества (2015)[23]
  • Член ACM (2014)[24]
  • Профессор (Scientia Professor) Университета Нового Южного Уэльса
  • Герой инноваций Центра передовых инженерных разработок Уоррена при Сиднейском университете (2010)
  • Учёный года Нового Южного Уэльса в категории «Инженерия, математика и компьютерные науки» (2009)
  • Лучшая статья на 22-м симпозиуме ACM SIGOPS по принципам операционных систем (2009)
  • Лучшая статья на 13-й Азиатско-Тихоокеанской конференции по архитектуре компьютерных систем IEEE (2008)
  • Лучшая студенческая статья на ежегодной технической конференции USENIX (2005)

Примечания[править]

  1. ↑ (1998) «The Mungi Single-Address-Space Operating System». Software: Practice and Experience 28 (9): 901–928. DOI:<901::AID-SPE181>3.0.CO;2-7 10.1002/(SICI)1097-024X(19980725)28:9<901::AID-SPE181>3.0.CO;2-7.
  2. ↑ (1997-05) "Achieved IPC performance (still the foundation for extensibility)".: 28–31, Cape Cod, Massachusetts, United States: IEEE. 
  3. ↑ (2005-04) "Itanium: a system implementor's tale".. 
  4. ↑ (2007-07) «Towards trustworthy computing systems: Taking microkernels to the next level». ACM Operating Systems Review 41 (4): 3–11. DOI:10.1145/1278901.1278904.
  5. ↑ 5,0 5,1 (2009-10) "seL4: Formal verification of an OS kernel".. 
  6. ↑ (2008-08) "Pre-virtualization: Soft layering for virtual machines".. 
  7. ↑ (2009-06) "vNUMA: A virtual shared-memory multiprocessor".. 
  8. ↑ Leslie, Ben (2005-09). «User-level device drivers: Achieved performance». Journal of Computer Science and Technology 20 (5): 654–664. DOI:10.1007/s11390-005-0654-4.
  9. ↑ (2009-04) "Dingo: Taming device drivers".. 
  10. ↑ (2011-03) "Improved device driver reliability through hardware verification reuse".. 
  11. ↑ (2009-10) "Automatic device driver synthesis with Termite".. 
  12. ↑ (2009-04) "Koala: A platform for OS-level power management".. 
  13. ↑ (2013-04) "Sequoll: a framework for model checking binaries".. 
  14. ↑ (2016-04) "Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis".. 
  15. ↑ (2018-04) "Scheduling-Context Capabilities: A Principled, Light-Weight OS Mechanism for Managing Time".. 
  16. ↑ (2015-05) "Last-Level Cache Side-Channel Attacks are Practical".. 
  17. ↑ (2019-03) "Time Protection: the Missing OS Abstraction".. 
  18. ↑ (1995) «Limiting loss mechanisms in 23-percent efficient silicon solar cells». Journal of Applied Physics 77 (7): 3491–3504. DOI:10.1063/1.358643.
  19. ↑ ACM Distinguished Speakers list. Проверено 27 июля 2026.
  20. ↑ ACM SIGOPS Hall of Fame Award. Проверено 27 июля 2026.
  21. ↑ ATSE Fellow. Проверено 27 июля 2026.
  22. ↑ Fellow of the IEEE. Проверено 27 июля 2026.
  23. ↑ ACS ICT Researcher of the Year 2015. Проверено 27 июля 2026.
  24. ↑ ACM Fellows 2014. Проверено 27 июля 2026.

Ссылки[править]

Рувики

Одним из источников, использованных при создании данной статьи, является статья из википроекта «Рувики» («ruwiki.ru») под названием «Хайзер, Гернот», расположенная по адресу:

—https://ru.ruwiki.ru/wiki/Хайзер,_Гернот

Материал указанной статьи полностью или частично использован в Циклопедии по лицензии CC-BY-SA 4.0 и более поздних версий.

Всем участникам Рувики предлагается прочитать материал «Почему Циклопедия?».

Источник — http://cyclowiki.org/w/index.php?title=Хайзер,_Гернот&oldid=2706777