alar
C СЯУ l4 WTF
it turned out that by carefully handcrafting the fast path, we can achieve highly-competitive IPC latencies [Blackham and Heiser, 2012]. Specifically this means manually re-ordering statements, making use of (verified) invariants that the compiler is unable to determine by static analysis
Люди руками переписывали сишный код в другой сишный код, на основании знаний того, какие машинные команды получатся в итоге и с какой скоростью будут выполняться.

По-моему, проще обучить Изабель понимать асм ARMv6
valerius
Darwin l4 n900 На Nokia N900 портировано ядро Darwin (которое, в свою очередь, основано на микроядре Mach). habrahabr.ru Вот бы еще запустить Maemo на основе L4Linux (но там некоторые драйвера проприетарные, а нужно перекомпилить их, чтобы заработали в userspace). А так, люди говорили, что у N900 SoC такой же, как у Beagle board (на которой уже запускали L4/Fiasco+L4Re+L4Linux)
alexst
l4 Samsung ARM Вот запустил u-boot на Samsung Galaxy Tab 2 (P5100).

Пока что chainload вместо ядра.
Что могу сказать про девайс и uboot
В девайсе omap4. У нас уже есть портированный uboot на Galaxy Nexus. (https://www.youtube.com/watch?v=tcrNbwwPBkI) Причем, поскольку для Galaxy Nexus есть утилита для прошивки по usb, даже когда стерт бутлодер xloader из emmc (то есть, брикнуть его нельзя) — там uboot грузится сразу, вместо самсунговского бутлодера. Посмотрю — возможно, получится утилиту от Galaxy Nexus адаптировать под этот планшет

В uboot недавно появилась поддержка файловой системы EXT4, и теперь он не виснет при чтении андроидовских ФС. Теперь можно кастомные ядра/скрипты класть в папку во внутреннем хранилище.

Кстати, я перенес на последнюю версию uboot патчи для андроидовского mkbootimg формата — можно залить uboot вместо recovery, например, и использовать ванильные немодифицированные прошивки.

Что неудобно — в uboot для omap нет DFU, и в uboot вообще нет fastboot. Есть только в версиях от ti/omapzoom, которые основаны на коде 2007 года, и там нет ничего. даже фреймбуффера. С фреймбуффером вообще беда на омапах. С клоками все запутано, у меня так и не завелось в omap4 и uboot пока что

Про L4 — видимо, будет отдельный пост. Пока что основные задачи — завести usb (линуксовый драйвер в Genode в целом удалось прикрутить, но данные идут только в configuration EP, а в остальные — нет), и фреймбуффер. На планшете плохо — нет uart (у меня, по крайней мере, кабель не собран по причине лени), и отлаживать тяжело

oxyd
l4 osFree Размер бинарника микроядра L4-Fiasco (оно и только оно находится в Ring0, усё остальное в отдельных адресных, в юзерспейсе) под x86-32 всего 370 640b сравните с типичным вядром линукса. ;)
dk
OS l4 programming Наверняка многие читали про L4 fast IPC design(http://l4ka.org/publications/1993/improving-ipc.pdf), который позволил объективно говорить о том, что microkernel approach с клиент-серверной архитектурой не только имеет право на жизнь, но и не так уж сильно проигрывает по performance монолиту, ибо message passing стал не многим медленнее системного вызова. Но тем не менее с клиент-серверной архитектурой в микроядре связан набор труднорешаемых проблем. Одна из них заключается в том, что сервер, принявший сообщение от клиента, начинает работать, тратя свой тайм-слайс, используя свой приоритет(что приводит к потенциальному priority inversion) и тратя свои ресурсы(например память). Одним из решений этой проблемы является так называемый thread-migrating IPC design. Идея проста: при посылке сообщения от клиента серверу, помимо самого сообщения серверу кидается тред клиента, который просыпается на сервере(со своим(клиентским) приоритетом, лимитами, тайм-слайсом), выгребает сообщение и начинает исполнять серверный код. Просто и гениально. На эту тему есть очень неплохая статья: "Vulnerabilities in Synchronous IPC Designs"(http://www.eros-os.org/papers/IPC-Assurance.ps).