Уроки L4

21.04.2016 18:39:26

Австралийская НИКТА в лице тт. Хейзера и Элфинстоуна некоторое время назад выкатила отличную работу, описывающую двадцатилетнее развитие микроядер Эльчетыре. Очень люблю такое — видно, с чего начали, какие проблемы в разное время возникали, как они решались, к чему пришли. Интересно даже не само микроядро (хотя с Фисташкой я даже непосредственно сталкивался лет так семь назад), а наблюдение за реальной эволюцией системы.

Ситуация осложнена тем, что эльчетвёртых ядер довольно много, есть заметно фрагментированное семейство. И в этом семействе, в первую очередь, разумеется, педалируется то направление, которым занимались авторы, а именно, верифицируемое ядро ЭсЕЭльчетыре. Но это работе не мешает, да и мне самому эта вариация нравится больше всех, галочка формальной верификации очень уж красивая.