https://ayles.github.io/doom-in-kernel/

Коллеги (на этот раз действительно коллеги!) подогнали прекрасное - Doom, на #eBPF, в ядре Linux.

"Прекрасное" потому что идет наперекор тому, как пытается работать eBPF.

eBPF, для каждой загружаемой программы, пытается доказать, что программа не зависнет, и что программа не ездит по памяти.

Второе, допустим, просто, поколения программистов вычистили исходники Doom так, что игра работает и без проездов.

Первое - сложно, и чуваки поступили, на мой вкус, весьма #изящно!

Они запилили свой компилятор поверх LLVM.

Он режет обычный C-код на "регионы" - куски без сложных циклов и вызовов. Регион обрывается на каждом вызове функции, возврате, неудобном обратном ребре цикла или yield. В конце он сохраняет state в память, и возвращает номер следующего региона.

Регионы гоняет маленький диспетчер из трёх вложенных ограниченных циклов: 32x2048x64, около 4*10^6 регионов за один вызов. Если бюджет кончился, программа возвращает "не доделано" с номером продолжения, и userspace вызывает её снова.

Ну а верификатор доказывает завершение не DOOM, а очередного региона и диспетчера.

И он может это сделать, потому что видит набор кусков, каждый из которых заканчивается обычным return, плюс цикл с константной границей. Прыжков "регион 18 -> регион 42" в графе управления нет: это число, записанное в память. Рекурсия, глубокие вызовы и длинные циклы существуют только во время исполнения, как последовательность этих чисел.

Я бы тут поинтересовался у коллег, почему того же самого нельзя было добиться source трансформацией кода, превратив его в async код через с++ корутины, трансформация ровно та же самая получается - куча блоков с return, и цикл dispatch над ними сверху, но сути это не меняет.