Исходное сообщение
"Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..." Отправлено Xasd, 25-Июн-14 01:19
> Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным. тыг ведь видов ошибок можно допустить -- намного-много больше :-) как минимум -- вот например что часто бывает: * состояние гонки. в той или иной форме -- невероятно-частая ошибка. * некорректная проверка источника событий. (или вообще забывают проверять источник -- а сразу выполняют действие связанное с событием). * утечка ресурсов. например утечка может быть связана с неполным алгоритмом учёта состояния ресурсного объекта  (например: алгоритм -- учитывает не все возможные ситуации.. такое бывает СВЕХ-часто в ПО).