И этот персонал _намеренно_ поотключал всю защиту

Персонал *намеренно* *включил* аварийную защиту, как один из этапов выведения реактора из эксплуатации в связи с плановой профилактикой. Нда... Потом, все реакторы РБМК, и в РФ и за рубежом, проходили серьезную модернизацию системы управления и защиты. А виноват, конечно, персонал. Самое смешное, что на той же самой ЧАЭС на пятом энергоблоке, в начале 90-х годов произошла серьезная авария на ТГ с фейерверком и разрушением кровли турбинного зала. И реактор тогда показал хорошую степень самозащиты. Говорю же: пример с АЭС — крайне неудачный.

исследовать нужно стабильную работу системы в целом а не микроядрышка которое только тем и занято что делает безопасные memcopy

Без TCB, построенной по принципу минимализма, бесполезно даже начинать.

Персонал проводил эксперимент по выбегу ротора турбогенератора, система аварийного охлаждения реактора была отключена, главные циркуляционные насосы работали от выбегающей турбины, что привело к подаче перегретой воды в активную зону. Разрешение на проведение эксперимента было согласовано только с главным инженером станции. В общем нормальный пример, показывает что даже самое наисертифицированное ведро от кривых рук не спасает.

Без TCB

Без чего?

Без чего?

http://en.wikipedia.org/wiki/Trusted_computing_base

В общем нормальный пример, показывает что даже самое наисертифицированное ведро от кривых рук не спасает.

дураку еще и не такое может показаться.

У вас из всей base trusted только ядро, которое еще и микро. А то что начинать можно и без этой фигни нам подсказывает такая штука как построение надежных систем из ненадежных элементов. Система это не набор утилиток, это намного больше. И да, вас пока к АЭС лучше не подпускать :)

построение надежных систем из ненадежных элементов

это не всегда возможно

И да, вас пока к АЭС лучше не подпускать :)

причем тут твой чернобыль ?

уже были. поначалу фишкой этого ядра и NICTA была паравиртуализация. одно ядро на L4, другое на андроеде. потом было непонятно что. потом вроде как официально ондроед допиливали.
радость-радость, что можно пруфы и линки самому просмотреть. а то маловато было house os на хаскелле, melange на ml(ау,хартблид) и какой-то ос на ml и книжки математиков теорката — как-то особо нечем было упарываться.

Это уже можно заюзать вместе с GNU? Т.е. собрать что-то типа GNU/seL4, и чтобы работало?

Кто-нибудь может пояснить это? Очень любопытно.

В посте, на который я отвечал, речь шла о «влиянии багов», а не о «падении». Кстати, обычные баги в драйвере (не падения) и в микроядерной системе повлияют на все программы.

речь шла о том, что в монолитной ОС баг приведет к остановке всей системы, а в микроядерной - нет.

Терминалы точно не продолжат, насчет Eclipse RSE тоже сомневаюсь.

это повод задуматься о том, что надо что-то поменять в них, а не хаять микроядерные ОС в том, что у тебя один хрен все упадет и надо будет перезапускать.

речь шла о том, что в монолитной ОС баг приведет к остановке всей системы, а в микроядерной - нет.

Остановка системы или остановка работы основного серверного приложения - разница не принципиальная.

а не хаять микроядерные ОС, в том, что у тебя один хрен все упадет

Похоже, я ненароком задел твой фетиш.

Остановка системы или остановка работы основного серверного приложения - разница не принципиальная

с микроядром можно сделать строгое разделение критичного и некритичного кода с гарантией безопасной работы и IPC - на этом принципе и работают гипервизоры, на монолите ты никогда не сможешь дать такой гарантии для критичного кода - ошибка в любом некритичном для тебя месте ядра вызывает крах всей системы.

с микроядром можно сделать [...]

Я достаточно знаю о микроядрах. Но у меня период увлечения ими давно прошел и я смотрю трезво.

ошибка в любом некритичном для тебя месте ядра вызывает крах всей системы.

Микроядра сегодня - это костыль для запуска кода, который не умеют верифицировать, и seL4 это отлично демонстрирует (раньше похожую вещь продемонстрировал Mach). Верифицированное «обычное» ядро уделает микроядро по всем параметрам, а пока что технологии верификации «обычных» ядер обкатываются на микроядрах.

Верифицированное «обычное» ядро

пока что нет даже попыток сделать такое

уделает

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

Верифицированное «обычное» ядро

пока что нет даже попыток сделать такое

Если это вообще возможно сделать, исследования seL4 неминуемо приведут к этому. А тем временем есть и запасные варианты - например, писать ядра на безопасных языках.

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

Без нормальных ядер, гипервизоры - бесполезные игрушки.

Без нормальных ядер, гипервизоры - бесполезные игрушки

без тонн небезопасного кода который нет смысла переписывать гипервизор становится просто минималистичной микроядерной ОС.

без тонн небезопасного кода который нет смысла переписывать гипервизор становится просто минималистичной микроядерной ОС.

Некоторые гипервизоры - да, становятся. Правда, никакой полезной работы выполнить они не могут, но кого это интересует?

Правда, никакой полезной работы выполнить они не могут

Steam там конечно вряд ли для тебя сделают - это правда :)

Правда, никакой полезной работы выполнить они не могут

Steam там конечно вряд ли для тебя сделают

Что такое Steam и чем он полезен?

Что такое Steam

http://ru.wikipedia.org/wiki/Steam

полезен

что полезно в первую очередь решают разработчики

http://genode.org/about/road-map

и работают.

Остановка системы или остановка работы основного серверного приложения - разница не принципиальная.

время старта и диагностики как бы слегка разное, так что разница принципиальная.

Похоже, я ненароком задел твой фетиш.

не угадал.

Микроядра сегодня - это костыль для запуска кода, который не умеют верифицировать, и seL4 это отлично демонстрирует (раньше похожую вещь продемонстрировал Mach).

ну, ты сравнил. Mach это было давно и неправда (и вообще, он архитектурно тормоз by design с портами и capabilities). вообще за это время, пока у тебя проходил период увлечения устаревшим Mach, там кое-что происходило.

Микроядра сегодня - это костыль для запуска кода, который не умеют верифицировать

а экзоядро тогда — это костыль для запуска чего?

Верифицированное «обычное» ядро уделает микроядро по всем параметрам, а пока что технологии верификации «обычных» ядер обкатываются на микроядрах.

Верифицированное «обычное» ядро

WTF? и что будет с верификацией, если добавить драйвер?

Верифицированное «обычное» ядро уделает микроядро по всем параметрам

но не уделает экзоядро, которое уделает микроядро. и в чём тогда отличие такого мифического «верифицированного обычного ядра» и экзоядра?

Без нормальных ядер, гипервизоры - бесполезные игрушки.

что ты понимаешь под «нормальными ядрами»? паравиртуализованные?

Микроядра сегодня - это костыль для запуска кода, который не умеют верифицировать, и seL4 это отлично демонстрирует (раньше похожую вещь продемонстрировал Mach).

ну, ты сравнил

Похоже, ты не понял сравнения. Mach пускал single-server'ы тогдашних Unix, а нынешние микроядра пускают Linux.

вообще за это время, пока у тебя проходил период увлечения устаревшим Mach, там кое-что происходило.

Происходили бесконечные вариации L4. Да, это именно «кое-что».

Верифицированное «обычное» ядро

WTF?

Обычное ядро (Linux, скажем), для которого написана спецификация и верифицировано соответствие верификации. Что именно тебе непонятно?

Верифицированное «обычное» ядро уделает микроядро по всем параметрам

но не уделает экзоядро

Экзоядро by design ничего не умеет и всё делегирует библиотечной ОС. Там нечего уделывать.

в чём тогда отличие такого мифического «верифицированного обычного ядра» и экзоядра?

Гг. Ты еще спроси, в чем отличие экзоядра (неверифицированного) от обычного ядра (тоже неверифицированного).

что ты понимаешь под «нормальными ядрами»? паравиртуализованные?

Полнофункциональные (драйверы, сеть, ФС) ядра обычной архитектуры. Linux, если коротко.

что ты понимаешь под «нормальными ядрами»?

Полнофункциональные (драйверы, сеть, ФС) ядра обычной архитектуры. Linux, если коротко.

линуксоиды совсем в говно скатились - сравнивают нормальность ядер по количеству имеющихся драйверов. Напомню сообщение Торвальдса о Linux

It is NOT protable (uses 386 task switching etc), and it probably never will support anything other than AT-harddisks, as that's all I have :-(.

Дык. Верифицированный софт на деревьях не растет. И сам не размножается.

это временное упущение. недоработка, а не заслуга.

Его нужно писать... А зачем?

не нужно его писать всего руками и целиком. его надо синтезировать. посмотри на это как на алгебру (например, алгоритмы разбора контекстно-свободных языков глубоко связаны с алгоритмами перемножения матриц) или другие мат. модели : коалгебру и т.п., или из теорката и топологии (*); или же «система магов» Гёрцеля, гиперотношения на гипермножествах, модель бутстрапа (**), автореферентность.

с такой точки зрения, у нас есть 2 подхода:
1.
а) эвристически получить решение
b) формально его верифицировать
c) молиться, что в новом решении композиция будет составлена таким образом, что её получится верифицировать
d) продолжать эвристически получать «сложные» мат. модели (ср. диф-интегральные уравнения) как сложная композиция (ср. API) сложных объектов (ср. программы) в простых пространствах (ср. R-числа)

2.
a) получить формальную модель, «алгебру» (коалгебру, топосы языка, модель бутстрапа как «алгебра» на гипермножествах, теор.кат. и т.п.) — возможно, повторно использовав результаты из 1b
b) составить набор действий и моделей, а также их композиций из расчёта допустимых действий
c) убедиться, что верификация выполняется автоматически, т.к. действия выполнятся только допустимые — такие, чтобы формально верификация прошла успешно.
d) продолжать выводить, генерировать, синтезировать «простые» мат. модели (ср. коалгебра) как простая композиция (ср. кольцо) сложных объектов (ср. метапрограммы) в сложных пространствах (ср. комплексные, кватернионы,октонионы, гиперкомплексные, ..., финслеровы пространства, ..., топосы(***), категории и т.п.)

Я уж молчу, про то что окружение (тоже верифицированное), сможет дать определенные гарантии, что запускаемый софт не сможет сделать что-то, что не разрешено его ролью.

а эти гарантии тоже описать в виде модели ограничений «алгебры» 2b.

_____
(*) Barney Stratford, «The topology of language»:

many kinds of languages that are described by generative grammars can also be described in terms of the fixed point of a contraction mapping - in other words, that they are usually fractals in the sense that Barnsley (Barnsley, 1993) uses the term.

http://mathematicallinguistics.blogspot.be/2010/10/topology-of-language-space...

R. Thom, «Топология и лингвистика»

David Kephart, «Topology, Morphisms, and Randomness in the Space of Formal Languages»

(**)

(***)

(**)

сейчас активно разрабатывается математика, базирующаяся на теории гипермножеств [20]. В такой математике существуют объекты, которые содержат друг друга в качестве элементов, как бы это ни казалось парадоксальным обычному рассудку. Так, гиперфункция может содержать себя в области определения своего аргумента. Гёрцель ввел также понятие гиперотношения и показал, что именно такие конструкции хорошо описывают модели автопоэзиса и самомодифицирующейся системы Камписа. Гёрцель также предложил довольно широкий класс систем, которые он назвал “самогенерирующимися” или, менее формально, “система магов”

Модель бутстрапа означает полную само-согласованность, взаимообусловленность частей и целого, неклассическую (коллективную) элементарность. Реализуется такая система благодаря неопределенной рекурсивности в ее организации. При этом отвергается классический механистический элементаризм в виде линейной иерархии системных уровней, кончающейся внизу системой неделимых фундаментальных сущностей. В бутстрап – модели мира фактически не существует выделенных элементарных неделимых абсолютных сущностей. Эту идею ярко выразил Фритьоф Капра: “Вселенная рассматривается в качестве сети взаимосвязанных событий. Ни одно из свойств того или иного участка этой сети не имеет фундаментального характера; все они обусловлены свойствами остальных участков сети, общая структура которой определяется универсальной согласованностью всех взаимодействий”

Элементы бустрап-системы – взаимно-детерминирующие сущности, образующие с целым дуальную эмерджентно возникающую и относительно устойчивую пару. Кроме того, любые выделенные элементы либо существуют все вместе, либо не существуют совсем.

Другая, чисто материальная трактовка понятия означает буквально коллективное самопроизводство, когда все элементы участвуют в воспроизводстве друг друга и в коллективном воспроизводстве системы связей, ответственных за это производство. Такой логически замкнутый круг демонстрирует бутстрап в модели автопоэзиса, или минималистской модели живого организма, как биологической автономии, обобщенного метаболизма. Наконец, еще более решительный отказ от классического подхода к понятию система недавно предприняли системные теоретики, среди которых выделяется Кент Палмер

(***)

В 1944 г. Ганс Рейхенбах пришел к идее эквивалентности или симметрии логики и топологии: «Если бы мы попытались описать пространство с одной топологией с помощью пространства с другой топологией, появились бы каузальные аномалии», в частности «пространство одной размерности нельзя описать с помощью пространства другой размерности без допущения каузальных аномалий» (А.М. Мостепаненко, М.В. Мостепаненко). Вывод Рейхенбаха - «Топология пространства… связана с законами причинности» -лег в основу сформулированной в середине ХХ века теоремы Роберта Герока о дополнительности логики и топологии: «Если реализация физического процесса связана с изменением топологии, то с точки зрения старой топологии оно будет восприниматься внешним наблюдателем как неожиданное нарушение закона причинности» (И.А. Акчурин). Теорема Герока раскрывает топологический смысл теоремы Геделя: «Если мы используем классическую логику, то в случае, когда… происходит изменение топологии, оно будет нами восприниматься как резкое нарушение – в понятиях старой топологии – принципа причинности»

В начале 60-х годов ХХ века Александр Гротендик ввел в математику пространство с переменной топологией – «пространство в новом стиле» или «топос» (А. Гротендик). В топосе Гротендика реализуется симметрия логики и топологии, о которой говорит теорема Герока.

что ты понимаешь под «нормальными ядрами»?

Полнофункциональные (драйверы, сеть, ФС) ядра обычной архитектуры. Linux, если коротко.

линуксоиды совсем в говно скатились - сравнивают нормальность ядер по количеству имеющихся драйверов.

«Обычность» тоже. Но вообще, вот: http://nexua.org/niji/butthurt-form/

Mach пускал single-server'ы тогдашних Unix, а нынешние микроядра пускают Linux.

или Darwin (Darbat, тоже на L4).

Обычное ядро (Linux, скажем), для которого написана спецификация и верифицировано соответствие верификации. Что именно тебе непонятно?

и что получается, когда мы делаем в него insmod my-kernel-splice.ko ?

Экзоядро by design ничего не умеет и всё делегирует библиотечной ОС. Там нечего уделывать.

ИМЕННО ПОЭТОМУ оно не победимо :)))

Mach пускал single-server'ы тогдашних Unix, а нынешние микроядра пускают Linux.

или Darwin (Darbat, тоже на L4).

Да ради ТНБ. Darwin принципиально ничем не отличается от Linux.

Обычное ядро (Linux, скажем), для которого написана спецификация и верифицировано соответствие верификации. Что именно тебе непонятно?

и что получается, когда мы делаем в него insmod my-kernel-splice.ko ?

Что такое my-kernel-splice, зачем мы его insmod-им, и является ли он верифицированным?

Что такое my-kernel-splice, зачем мы его insmod-им, и является ли он верифицированным?

вопрос не в этом. не во всех этих кружках с ложечкой «а вы вот так — не делайте». вопрос в том, будет ли «верифицированное» моноядро оставаться верифицируемым при любых допустимых действиях.
сложная композиция сложных vs. простая композиция гиперсложных.
(а в идеале простая композиция простых, как в plan9, или в экзо - но идеал не достижим, так что достаточно так просто, как это возможно, не проще этого :( )

что ты понимаешь под «нормальными ядрами»? паравиртуализованные?

Полнофункциональные (драйверы, сеть, ФС) ядра обычной архитектуры. Linux, если коротко.

драйверы

DevIL: DSL семантика Nooks

сеть

Melange DSL

ФС

Plan-9 P9? или какой-то подобный протокол на базе FUSE?? да, с достаточно формальной моделью ФС тут напряг.

ядра обычной архитектуры. Linux, если коротко.

не нужен. если допилить указанные формальные модели, DSL и какой-то язык для формальных спеков. задавать спеки на устройство в виде некоторого DSL и генерировать, порождать из него через другие DSL «драйверы, сеть, ФС» в виде некоторого системно-зависимого API (понимаемого как DSL).

то немного подкрутив такой системно-зависимый DSL можно перенести драйвера в другую ОС.

а скрипач не нужен. нужно его формальное описание и порождающее проектирование алгебры коалгеброй через алгебру.

И причем тут Nooks?

немного подкрутив такой системно-зависимый DSL можно перенести драйвера в другую ОС.

У кого-то уже получилось? Нет? Я так и думал.

допилить указанные формальные модели, DSL и какой-то язык для формальных спеков. задавать спеки на устройство в виде некоторого DSL и генерировать, порождать из него через другие DSL «драйверы, сеть, ФС» в виде некоторого системно-зависимого API (понимаемого как DSL).

скрипач не нужен. нужно его формальное описание и порождающее проектирование алгебры коалгеброй через алгебру.

Ну тогда конечно. Удачи.

ядрёное native API как топосы Гротендика. а kernel девелоперы это «система магов» неформализованная.

Но вообще, вот: http://nexua.org/niji/butthurt-form/

я не страдаю подростковым максимализмом

у меня период увлечения ими давно прошел и я смотрю трезво

но твоя трезвость под большим сомнением, хотя мб это головокружение от успехов :)

PC99 это и есть «обычный x86 компьютер».

Необычный это PC98 какой-нибудь.

Выдаю персональное разрешение юзать seL4 вместе с GNU.

NEC PC-98