The OpenNET Project / Index page

[ новости /+++ | форум | wiki | теги | ]

Открыт код сверхнадёжного микроядра seL4

29.07.2014 09:20

Компания General Dynamics C4 Systems и австралийский исследовательский центр NICTA открыли под свободными лицензиями исходные тексты микроядра seL4 (Secure Embedded L4), компоненты математического доказательства его надёжности и сопутствующий код для построения высоконадёжных операционных систем. Ядро открыто под лицензией GPLv2, а утилиты и работающий в пространстве пользователя код содержит как элементы под лицензией GPLv2, так и компоненты под лицензией BSD.

Микроядро seL4 нацелено на предоставление повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. В частности, Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) применяет seL4 для повышения защищённости программных систем, используемых в военных беспилотных летательных аппаратах.

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

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

Для разработчиков предлагается компоненто-ориентированная платформа для разработки приложений CAmkES, позволяющая моделировать и создавать системы на основе seL4 в виде коллекции взаимодействующих между собой компонентов. Также поставляется набор примеров и прототипов систем на основе seL4, подборка драйверов, библиотека для создания драйверов, порт Си-библиотеки Musl. Из поддерживаемых аппаратных архитектур отмечены ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) и x86. Поддерживается запуск поверх микроядра seL4 ядра Linux, в данном случае seL4 выступает в роли гипервизора.

  1. Главная ссылка к новости (https://github.com/seL4...)
  2. OpenNews: Сверхнадёжное ядро seL4 будет переведено в разряд открытых проектов
  3. OpenNews: На базе гипервизора seL4 создана платформа для создания высокозащищённых систем
  4. OpenNews: Найден способ формального подтверждения 100% отсутствия ошибок в программе
Лицензия: CC-BY
Тип: К сведению
Ключевые слова: sel4, microkernel
При перепечатке указание ссылки на opennet.ru обязательно
Обсуждение (129) Ajax | 1 уровень | Линейный | Раскрыть всё | RSS
  • 1.2, evkogan (?), 09:39, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Сначала нужен список поддерживаемого оборудования
    И список портиротированного ПО
    У кого-то такая инфа?
     
     
  • 2.4, уке (?), 09:47, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +32 +/
    У меня инфа. Поддерживается железо:
    F-16, M1 Abrams, Piranha, MX, SAPS, MASP, GDMX, TDRSS.
     
     
  • 3.17, commiethebeastie (ok), 10:27, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +7 +/
    Демократичненько
     
  • 3.39, Аноним (-), 14:12, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    ссылку или бабабол
     
     
  • 4.54, Аноним (-), 16:33, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +5 +/
    Да балабол, но все равно ржачно.
     
  • 3.52, Fantomas (??), 16:14, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +5 +/
    > У меня инфа. Поддерживается железо:
    > F-16, M1 Abrams, Piranha, MX, SAPS, MASP, GDMX, TDRSS

    Классно M1 Abrams, сервер, серверная и дизельгенератор в одном флаконе )))

     
     
  • 4.61, Аноним (-), 17:23, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Ога! Можно WoT гонять :)
     
     
  • 5.69, Аноним (-), 18:56, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Ога! Можно WoT гонять :)

    Только тут подсказывают что для того чтобы гусеница за 30 секунд чинилась - надо технологии сильно заппгрейдить.

     
     
  • 6.90, Аноним (-), 03:45, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Не знаю как там у абраши и с наших православных танков 3/4 этого форума тупо трак от земли не оторвут :) Какой там заменить :)
     
     
  • 7.106, Аноним (-), 20:36, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Так я и говорю - технологии надо сильно прокачать. Ну там например выводок нанороботов, который гусеницу на месте пересобирать будут. Впрочем, при таких технологиях танки уже не требуются: наноботы могут ведь не только смонтировать гусеницу, но и размонтировать гусеницу на танке врага. Да и вообще весь танк.
     
     
  • 8.108, arisu (ok), 20:43, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    да и самих врагов тоже, им пофигу, что ломать ... текст свёрнут, показать
     
     
  • 9.120, Аноним (-), 04:34, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Это наверное опционально, низкоприоритетная задача Враги узрев такую разборку б... текст свёрнут, показать
     
     
  • 10.126, arisu (ok), 14:17, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    вообще, всё наоборот намного выгодней разломать врагов и оставить полезную техн... текст свёрнут, показать
     
  • 4.111, Anonizmus (?), 20:53, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Классно M1 Abrams, сервер, серверная и дизельгенератор в одном флаконе )))

    Боюсь стоимость владения вас не обрадует...


     
  • 2.7, anonim (?), 09:49, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +4 +/
    >У кого-то такая инфа?

    Да, у кого-то есть.

     
  • 2.8, Аноним (-), 09:50, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Ну беспилотники уже поддерживаются. Дело за малым.
     

  • 1.5, re (?), 09:47, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +14 +/
    про титаник тоже так говорили
     
     
  • 2.9, Аноним (-), 09:50, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +18 +/
    Так все правильно - капитан и айсберг не были составными частями корабля, на них гарантия не распостранялась.
     
  • 2.37, Кевин (?), 13:59, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +4 +/
    каким бы надёжным не был сейф, его всегда можно бросить в вулкан (с)
     
  • 2.60, Аноним (-), 17:22, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Т.е. не мне одному кажется, что математики что-то не учли???
     
     
  • 3.101, umbr (ok), 15:35, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Учли, и пофиксили в следующих релизах. Титаник, Олимпик и Британик так и плавали непатченные.
     
  • 2.84, Аноним (-), 00:43, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    есть мнение, что говоруны эти были лицами заинтересованными
     

  • 1.10, Аноним (-), 09:53, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +8 +/
    > даёт основание считать решения на базе seL4 самыми надёжными в мире.

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

     
     
  • 2.11, Аноним (-), 10:11, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    >> даёт основание считать решения на базе seL4 самыми надёжными в мире.
    > Никто не спорит что примитивный тасксвичер можно написать без багов. Теперь удачи
    > написать без багов обвязку, без которой все это примерно столь же
    > полезно как выключенный компьютер.

    То есть ты хочешь сказать, что все ваши поделки априорно бажные? Я правильно тебя понимаю?

     
     
  • 3.13, Аноним (-), 10:18, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +11 +/
    Я хочу сказать что все мало-мальски сложные программы апнриори бажные. И хрен вы их валидируете математически.
     
     
  • 4.29, chinarulezzz (ok), 12:03, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Зависит от инструмента, подхода к разработке, и человека. К критическим задачам нужно подходить скрупулёзно. Априори бажность - хорошая отговорка для тех кто проектирует лифты, корабли, самолёты, автотехнику, робототехнику. Баги бывают, чо. Невнимательность - всего лишь невнимательность, и ничего с этим поделать нельзя.
     
     
  • 5.40, Crazy Alex (ok), 14:33, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +2 +/
    К критическим задачам надо подходить скурпулезно. Делая резервирование, проводя тщательное тестирование, используя статические анализаторы, чтобы указать человеку на подозрительные части кода и т.д. И при этом - учитывая, что узел таки имеет шанс отказать и планируя реакции на это - на разных ровнях системной иерархии.

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

     
     
  • 6.46, cmp (ok), 15:54, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    согласен, добавлю только, что эксперимент по созданию сверх надежного, но крайне... текст свёрнут, показать
     
     
  • 7.53, evkogan (?), 16:32, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Только одно, но ничто не мешает ядру не просто прибить драйвер, а перезапустить. А тогда разница очень большая.
     
     
  • 8.55, Аноним (-), 16:50, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Драйвер, может, и перезапустится, но перезапустится ли железка ... текст свёрнут, показать
     
  • 8.57, cmp (ok), 17:01, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –2 +/
    Железка и драйвер работают синхронно - перезапуск драйвера, в лучшем случае поте... текст свёрнут, показать
     
     
  • 9.79, Аноним (-), 23:58, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Особенно прикольно AMDшники GPU ресторят при сбоях Они пытаются восстановить со... текст свёрнут, показать
     
  • 9.105, arisu (ok), 19:10, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +2 +/
    скажи, ты говоришь так же, как и пишешь 8212 монотонно, укладывая в одно пред... текст свёрнут, показать
     
  • 8.58, Crazy Alex (ok), 17:03, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Насколько я понимаю, единственный более-менее надежный вариант реакции - громко ... текст свёрнут, показать
     
  • 8.71, Аноним (-), 19:01, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    По моим наблюдениям за ядром линукса это обычно так встает колом железка, а пот... текст свёрнут, показать
     
     
  • 9.115, Vkni (ok), 22:07, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Понятно, что если железка-дрянь, то АппаратноПрограммныйКомплекс тоже будет плох... текст свёрнут, показать
     
     
  • 10.121, Аноним (-), 08:58, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    С железом тенденция ровно обратная - становится быстрее-выше-сильнее-навороченне... текст свёрнут, показать
     
  • 7.104, arisu (ok), 19:08, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > 20 процентов программы (кода) удовлетворят потребности 80% пользователей.

    жаль только, что для разных пользователя эти двадцать процентов включают разные фичи.

     
  • 6.66, chinarulezzz (ok), 18:49, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Просто невнимательность, но не просто Не надо умных слов, друг Люди делают не ... текст свёрнут, показать
     
     
  • 7.80, Аноним (-), 23:59, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > Просто невнимательность, но не просто. Не надо умных слов, друг. Люди делают
    > не понимая что именно они делают также в области проектирования и
    > программирования. Не надо оправданий, тем более из области философии и психологии,

    А это не оправдания, это капитанинг. Иногда, даже если не хочется делать баг - он может всpaться. Человеческий мозг - не цифровой компьютер, поэтому не обладает идеальной надежностью и 100% воспроизводимостью работы.

     
     
  • 8.113, Anonizmus (?), 21:14, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    А кусок кремния таки прямо обладает b 100 b надежностью и воспроизводимостью... текст свёрнут, показать
     
     
  • 9.122, Аноним (-), 08:59, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Так его люди делали, со всеми вытекающими ... текст свёрнут, показать
     
  • 7.88, Ordu (ok), 02:11, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Про философию я соглашусь, она здесь неуместна, но игнорировать психологию совсе... текст свёрнут, показать
     
     
  • 8.93, pavlinux (ok), 04:47, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Нэт, это физиология изучает Хвать уже муть писать, спутали всё Алгоритмы с ре... текст свёрнут, показать
     
     
  • 9.100, Ordu (ok), 13:53, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ну раскройте глаза нам глупым или, как говорится, GTFO Впрочем я уверен, что вы... текст свёрнут, показать
     
  • 8.134, chinarulezzz (ok), 03:05, 01/08/2014 [^] [^^] [^^^] [ответить]  
  • +/
    не нужно думать что знания нашей психики завершены То что мы ошибаемся не означ... текст свёрнут, показать
     
  • 5.62, Аноним (-), 18:31, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Вот у лифта может быть дубовый алгоритм, который воможно провалидировать математ... текст свёрнут, показать
     
     
  • 6.70, chinarulezzz (ok), 18:57, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Людям свойственно ошибаться.

    и свойственно _не_ ошибаться.

    > И ничего с этим поделать нельзя.

    можно, они же знают что им свойственно...

    > Но это можно учесть. Есть множество инженерных принципов.

    Хорошо. Это разумно.

    > Или вон у одного из боингов бортовые компьютеры созданы из разной комплектухи, а софт
    > писан 2-я разными командами на 2-х разных ЯП.

    Тоже хорошо. Только бы не делали три, понимаешь? На случай если первые два ку-ку. А потом четыре, на случай если первые три ку-ку.

     
     
  • 7.73, Аноним (-), 19:11, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Только когда вся программа и рантайм - размером с hello world, да еще транслятор... текст свёрнут, показать
     
     
  • 8.77, chinarulezzz (ok), 19:33, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    тогда очевидно что программа должна стремиться к выполнению желательно одной фун... текст свёрнут, показать
     
     
  • 9.82, Аноним (-), 00:32, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Не обязательно Но программа должна быть или простой как топор, или должно быть ... текст свёрнут, показать
     
     
  • 10.133, chinarulezzz (ok), 02:58, 01/08/2014 [^] [^^] [^^^] [ответить]  
  • +/
    не обязательно, но стремление хорошее, даже лучшее из возможных, принимая во вни... текст свёрнут, показать
     
  • 6.94, pavlinux (ok), 05:03, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >> Априори бажность - хорошая отговорка для тех кто проектирует лифты,
    > Вот у лифта может быть дубовый алгоритм, который воможно провалидировать математически.
    > Хотя у современных лифтов это уже не факт - в больших
    > зданиях лифты принимают решения куда ехать исходя из количества людей и
    > оптимальности поездки

    Какая в пязду оптимальная поездка, на несвязаном графе с  последовательными узлами?

     
     
  • 7.110, Аноним (-), 20:51, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ты недооцениваешь лифты. Даже в простом лифте высотных зданий и офисов люди указывают вверх им или вниз. Так что из очевидных оптимизаций - как минимум лифт может пытаться ехать последовательно вверх и последовательно вниз. А если лифт уже полный - можно и не останавливаться, даже если и вызвали, например. А в чем пойнт похлопать дверями и уехать дальше? В более продвинутых может учитываться еще и количество ожидающих. А иногда и на какой этаж они хотят. А иной экспонат нынче уже норовит заняться и бизнес аналитикой: делается распознавание морды лица, а потом "Ага, это - хрен Вася из 100500-го офиса, он по статистике обычно ездит с 30-го этажа на 105-й".
     
  • 3.23, Andrey Mitrofanov (?), 11:06, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > То есть ты хочешь сказать, что все ваши поделки априорно бажные? Я

    Ваши тоже. _Все_. http://lib.ru/ANEKDOTY/errors.txt_with-big-pictures.html

    +++Чем больше программист делает ошибок, тем быстрее он делается ученым.

     
     
  • 4.63, Аноним (-), 18:40, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Ваши тоже. _Все_. http://lib.ru/ANEKDOTY/errors.txt_with-big-pictures.html

    ЧСХ, в каждой шутке есть доля правды :).

     
  • 2.12, Аноним (-), 10:15, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    зато дарповы гранты.
     
  • 2.21, Mihail Zenkov (ok), 10:53, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Если отказаться от бесполезного bloatware (kde/gnome/systemd/etc) с кучей модных фишек, а решать реальные узкоспециализированные задачи, то все получится. Например, система управления зажиганием ДВС (реальное время, счет на микросекунды) может уложиться в 1000 строк на C для atmega8 и еще успевать выводить статистику на экран.
     
     
  • 3.25, Аноним (-), 11:27, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Если отказаться от бесполезного bloatware (kde/gnome/systemd/etc) с кучей модных фишек,
    > а решать реальные узкоспециализированные задачи, то все получится. Например, система управления
    > зажиганием ДВС (реальное время, счет на микросекунды) может уложиться в 1000
    > строк на C для atmega8 и еще успевать выводить статистику на
    > экран.

    Это объясняет и оправдывает тысячи дистров линя?

     
  • 3.41, Crazy Alex (ok), 14:45, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Угу А потом вам понадобится какая-то хитрая алгоритмика для экономии топлива А... текст свёрнут, показать
     
     
  • 4.72, Mihail Zenkov (ok), 19:06, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Угу. А потом вам понадобится какая-то хитрая алгоритмика для экономии топлива. А потом - дополнить её для снижения выбросов. А потом еще что-то... А потом получится "KDE, версия для системы зажигания ДВС". Вероятнее всего - разложенная на несколько камней чтобы удержать-таки те самые микросекунды, что её ни разу не упростит.

    Вот это и есть overengineering ибо дальнейшее усложнение алгоритмов повышает сложность практически по экспоненте и также снижает стабильность и предсказуемость. Выигрыш при этом максимум 5% по эффективности и то в идеальных условиях на новой машине, пока естественный разброс при износе узлов его не перекрыл. Гляньте ecomodder.com, там весит топ по топливной экономичности машин и большинство из них до 2000-го года.

     
     
  • 5.81, Crazy Alex (ok), 00:16, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Выигрыш - в том, что ты продашь больше машин, показав людям эту экономию или это уменьшение выбросов.

    А вообще - не стоит цепляться к примеру. Речь шла о том, что усложнение систем - штука повсеместная и естественная. Точно так же, как монолитные материалы уступают место композитам, например - от лыж до домов. Точно так же, как вместо очага с поленьями сейчас имеем автоматические котлы с хитрыми форсунками, автоматикой и черт знает чем еще. Также как вместо полоски железа в современных ножах - порошковая сталь. И так далее, и тому подобное. И с "простейшей автоматикой" то же самое - выше где-то пример с лифтами уже приводили. С алгоритмикой работы отопления и вентиляции - то же самое, всё сложнее становится. Везде так.

     
     
  • 6.95, pavlinux (ok), 05:32, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Речь шла о том, что усложнение систем - штука повсеместная и естественная.

    Детский садик Ромашка.

    Панимаешь в чём вся х..ня - доступные материалы - для говна,
    говно не должно жить в каменном доме, с камином.
    В доме говна - нужны системы кондиционирования и вентиляции.
    Говно должно думать, что оно не говно. Для этого само говно,
    производит для говна, продукцию из/на говне.
    В основной массе, говно знающие, что делает говно, само верит
    в то, что производит. И начинает думать, что если каждое говно
    покупает, то, чем я хуже остального говна.

    Говну не нужен дом из мрамора, гавну нужен просто дом.
    Газбетон, ДСП, ПВХ, ... - типичный состав дома говна.

    Так же говно, покупает лыжи Salomon за 1500$ и ботинки к ним за 3000$,
    правда у говна даже нет 3-ого разряда по ОФП.  

     
  • 6.97, Mihail Zenkov (ok), 13:17, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Везде очень по-разному Я в курсе про котлы вентиляцию etc Там также все неодно... текст свёрнут, показать
     
  • 5.89, Аноним (-), 03:02, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Гляньте ecomodder.com, там весит топ по топливной экономичности машин и большинство из них до 2000-го года.

    "Невидимая рука рынка" как бы намекает - зачем тратиться на топливную экономичность, когда можно потратить в 10 раз меньше на пиар и хомячки все равно всё купят.

     
  • 4.116, Vkni (ok), 22:30, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > А всё потому, что по факту весь этот софт - монолитен. В том смысле, что для того,
    > чтобы заменить, удалить или добавить любой компонент нужны приличные усилия и
    > знания.

    И вот тут мы опять смотрим на Хы с разными WM. :-)

     
     
  • 5.127, arisu (ok), 14:27, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > И вот тут мы опять смотрим на Хы с разными WM. :-)

    а также на никсовую консоль и старый добрый принцип «одна задача — одна программа». но всё это неимоверно сложно для ЦА всяких DE.

     
  • 3.64, Аноним (-), 18:45, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Если отказаться от бесполезного bloatware (kde/gnome/systemd/etc) с кучей модных фишек,

    А также выбросить GPU со спеками на 900 страниц, чипы беспроводной сети у которых драйвер на 70% состоит из воркэраундов их багов и попыток развесить чип с минимальными потерями, ну и все такое прочее :).

     
     
  • 4.75, Mihail Zenkov (ok), 19:15, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > А также выбросить GPU со спеками на 900 страниц, чипы беспроводной сети
    > у которых драйвер на 70% состоит из воркэраундов их багов и
    > попыток развесить чип с минимальными потерями, ну и все такое прочее
    > :).

    Да нужно выбрасывать или делать их совершенно независимыми узлами, дабы в случае их подвисания основная часть могла нормально функционировать дальше. Меня не вдохновляет перспектива сбоя системы жизнеобеспечения (если я или кто-то из людей мне небезразличных окажется от нее зависим) только по тому, что кто-то решил, что без красивого 3d интерфейса с 120fps уныло и куда веселее соединить несколько важных модулей по wi-fi.

     
     
  • 5.83, Аноним (-), 00:35, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Да нужно выбрасывать

    Нужно? Выбрасывайте, разрешаю.

    > или делать их совершенно независимыми узлами,

    Как вы себе это представляете? Вот хочется вам картинку на экран рисовать - попробуйте при этом от GPU не зависеть, да? Или там при кидании пакетов по сети - от чипа сетевки. Или там при записи на диск - от чипа контроллера на мамке, чипа на диске, немеряной фирмвари накопителя и что там еще. Сферическое железо в вакууме это круто, но если например у вас отвалился диск - как вы себе представляете продолжение работы чтобы софт не заметил отвал диска?

     
     
  • 6.96, pavlinux (ok), 05:47, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • –3 +/
    >[оверквотинг удален]
    > Нужно? Выбрасывайте, разрешаю.
    >> или делать их совершенно независимыми узлами,
    > Как вы себе это представляете? Вот хочется вам картинку на экран рисовать
    > - попробуйте при этом от GPU не зависеть, да? Или там
    > при кидании пакетов по сети - от чипа сетевки. Или там
    > при записи на диск - от чипа контроллера на мамке, чипа
    > на диске, немеряной фирмвари накопителя и что там еще. Сферическое железо
    > в вакууме это круто, но если например у вас отвалился диск
    > - как вы себе представляете продолжение работы чтобы софт не заметил
    > отвал диска?

    Аноним, съибни, а! Ну лошара же последний.

     
     
  • 7.123, Аноним (-), 09:02, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Ну лошара же последний.

    Отправь СМСку с текстом "не лох!" на короткий номер. Ведь чем больше СМС ты пошлешь, тем больше ты не лох :).

     
  • 6.98, Mihail Zenkov (ok), 13:27, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >> или делать их совершенно независимыми узлами,
    > Как вы себе это представляете?

    Точно также как строится микроядерная ОС.
    Есть контроллер с основной программой, простой идеально отлаженный и проверенный. Он управляет остальными узлами. В случае зависания одного из узлов контроллер его перезапускает. В случае отказа узла, контроллер задействует дублирующий узел. Узлы естественно с hotplug.

     
     
  • 7.124, Аноним (-), 09:03, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Точно также как строится микроядерная ОС.

    Ну да, то-есть сферическое железо в вакууме, которое никто никогда не увидит, кроме десятка операторов ядерных реакторов на всю планету.

     
  • 3.85, Аноним (-), 00:44, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > зажиганием ДВС (реальное время, счет на микросекунды) может уложиться в 1000
    > строк на C для atmega8

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

    > и еще успевать выводить статистику на экран.

    Зато считает с комариной скоростью, да и сколь-нибудь нормальный интерфейс пользователя отрисовать не способна. Каждому свое. Не всем надо супер-хард-реалтайм и убер-мега-гипер-надежность ценой нагибания всех остальных свойств.

    Спору нет, автомобиль из титана сантиметровой толщины будет сложнее разбить. А еще он будет стоить как самолет, обладать погаными разгонными характеристиками и выпускаться в количестве 5 штук в год, ибо поди еще обработай этот чертов титан...  

     
     
  • 4.99, Mihail Zenkov (ok), 13:42, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ненужно передергивать Есть этап усовершенствования системы, после которого даль... текст свёрнут, показать
     
     
  • 5.112, Аноним (-), 20:58, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Ненужно передергивать. Есть этап усовершенствования системы, после которого дальнейшее
    > совершенствование практически ничего не дает кроме усложнения, снижения надежности и ремонтопригодности.

    А тут тоже зависит от. Что понимать под ремонтом? Возможность сделать радиолампу на замену сгоревшей в гараже? Возможность перепаять транзистор? Замена стандартной микросхемы логики? Смена сбойнувшего проца? Вынимание сервера из стойки и замена на такой же, но исправный? Где та грань?...

     
     
  • 6.117, Mihail Zenkov (ok), 03:11, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > А тут тоже зависит от. Что понимать под ремонтом? Возможность сделать радиолампу
    > на замену сгоревшей в гараже? Возможность перепаять транзистор? Замена стандартной микросхемы
    > логики? Смена сбойнувшего проца? Вынимание сервера из стойки и замена на
    > такой же, но исправный? Где та грань?...

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

     
     
  • 7.118, Аноним (-), 04:05, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Вот тут мы и приходим к самому главному Да, три гидролинии в самолете - имеют н... текст свёрнут, показать
     
     
  • 8.125, Mihail Zenkov (ok), 13:52, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Обычно в квартире ставят шаровый кран на вводе и перед каждой точкой разбора Эт... текст свёрнут, показать
     
  • 4.114, Anonizmus (?), 22:05, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Я вот до сих пор не могу понять почему массовые автомобили не выпускают из алюминия?..
     
     
  • 5.119, Аноним (-), 04:21, 31/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > выпускают из алюминия?..

    Потому что он мягкий как черти что, и при ДТП из юзера будет фарш. Обратите внимание чем обычно заканчиваются авиакатастофы...

     
     
  • 6.130, Аноним (-), 02:23, 01/08/2014 [^] [^^] [^^^] [ответить]  
  • +/
    >> выпускают из алюминия?..
    > Потому что он мягкий как черти что, и при ДТП из юзера
    > будет фарш. Обратите внимание чем обычно заканчиваются авиакатастофы...

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

     
  • 2.50, an (??), 16:06, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    как я понимаю микрокод (и аппаратный алгоритм) процессора по сути компонент тасксвитчера?
    И ошибки в микрокоде никто не отенял, во всяком случае для процессоров, в которых он есть.
    Какой тогда смысл в сверхнадежной системе?


     

  • 1.14, bav (ok), 10:19, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Гг. Осталось теперь математически доказать надежность всех остальных сервисов, которые делаю этот обглодышь минимально юзабельным.
     
     
  • 2.26, Аноним (-), 11:28, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –2 +/
    > Гг. Осталось теперь математически доказать надежность всех остальных сервисов, которые
    > делаю этот обглодышь минимально юзабельным.

    Летают и работают. А у вас в протоны датчики уебиметром заколачивают. Чья б мычала...

     
     
  • 3.32, Гость (?), 12:33, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Что доказывает качество конструкции и огромный запас прочности, на фоне которого, воздействие кувалдометром просто ничтожно.
     
     
  • 4.33, rain87 (?), 13:13, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    ровно до тех пор, пока датчик вверх ногами не прикувалдят
     
  • 3.65, Аноним (-), 18:47, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Летают и работают.

    Конкретно с seL4 летает, вероятно очень мало всего.

    > А у вас в протоны датчики уебиметром заколачивают.

    А это аппаратный баг, от него никакое микроядро не спасет.

     

  • 1.15, Аноним (-), 10:21, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +14 +/
    Ща поверх него запилят "сверхнадёжное" ПО на JavaScript и HTML5.
     
  • 1.16, Аноним (-), 10:27, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +8 +/
    Надо еще доказать корректность компилятора которым это все собирается.
     
     
  • 2.35, Mirraz (ok), 13:37, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    А ещё математически доказать 100% надёжность и корректность работы процессоров, на которых это ядро выполняется.
     
  • 2.36, Аноним (-), 13:41, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >Надо еще доказать корректность компилятора которым это все собирается.

    http://compcert.inria.fr/

     
     
  • 3.86, Аноним (-), 00:47, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > http://compcert.inria.fr/

    А что, сам на себе без багов он писаться не захотел? А то он на ocaml завязан и что там еще. А кто будет проверять проверяющего?

     

  • 1.18, IMHO (?), 10:32, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    еще одно ядро
     
  • 1.19, хрю (?), 10:41, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/
    там кода кот наплакал. код, конечно, легко читается и всё такое, но там ничего особо и нет. плюс оно, как я понимаю, не реалтайм.
     
     
  • 2.20, IMHO (?), 10:48, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    ну так правильно, с тяжолым ядром в верх не полетишь, избавляются от груза
     
  • 2.68, Аноним (-), 18:54, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    > там кода кот наплакал. код, конечно, легко читается и всё такое

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

     
     
  • 3.76, Mihail Zenkov (ok), 19:27, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > Так в этом то и весь пойнт сверхнадежных - надо спихнуть все
    > проблемы на других, а моя хата с краю, ничего не знаю.
    > Люди этот сверхнадежный принцип уже столетиями используют ;].

    Нет, здесь принцип не бери на себя большую ответственность, чем реально можешь потянуть. Если каждый модуль такой системы будет его передерживаться, то можно получить действительно стабильную систему. Вопрос остается с производительностью: модулей будет очень много и вероятно существенный процент cpu уйдет на пересылку сообщений между ними.

     
     
  • 4.87, Аноним (-), 00:48, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Нет, здесь принцип не бери на себя большую ответственность, чем реально можешь
    > потянуть.

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

     

  • 1.22, Аноним (-), 10:54, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    > GPLv2, так и компоненты под лицензией BSD

    Франкенштейн

     
  • 1.24, Аноним (-), 11:20, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > применяет seL4 для повышения защищённости программных систем, используемых в военных беспилотных летательных аппаратах.

    Персиянские операторы "Автобазы" подтверждают.

     
  • 1.27, Аноним (-), 11:35, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Ну что, ждем новости типа: "В ядре seL4 обнаружена критическая уязвимость ...".

    Хотя думаю, что такое мало вероятно скорее по причине того, что это ядро используют 2 с половиной человека, а еще меньше людей пытаются его вольно или невольно сломать.

    И да, кстати, то, что ядро формально соответствует спецификации, не гарантирует, что в спецификации могут ошибки.

     
     
  • 2.47, YetAnotherOnanym (ok), 15:54, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > не гарантирует, что в спецификации могут ошибки.

    Да-да-да, вполне возможно, что ошибки не могут в спецификации.

     

  • 1.28, Какаянахренразница (ok), 11:52, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +3 +/
    > Открыт код сверхнадёжного микроядра seL4

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

     
  • 1.30, chinarulezzz (ok), 12:08, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Просто офигительная новость. Актуальное микроядро под GPL лицензией, да еще и нашедшее реальное применение - это то, что когда-то не хватило GNU.
     
     
  • 2.31, ШТО (?), 12:30, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    К сожалению, сейчас оно не подойдет для GNU, так как нужна лицензия GPLv3+, иначе им нет смысла развивать платформу, которую могут тивоизировать.
     

  • 1.34, Аноним (-), 13:34, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    где то уже читал про математическое доказательство и микроядро, и при чем недавно ...
     
     
  • 2.38, Аноним (-), 14:03, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +7 +/
    > где то уже читал про математическое доказательство и микроядро, и при чем недавно ...

    если читал там, где "где-то" пишут без дефиса, а "причём" раздельно, то это был дилетантский бред

     
     
  • 3.44, Аноним (-), 15:39, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Ну чего набросились, парень радуется, что читать научился. Следующий этап - научиться писать!
     

  • 1.42, trdm (ok), 14:56, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Кажется беспилотник уже ломали в 2012 году.
    Уверены они что система надежная?
    http://xakep.ru/news/58149/
     
     
  • 2.56, Алексей (??), 16:59, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +1 +/
    По сути они заглушили сигналы GPS и подменили их своими. Никакого взлома тут не было - обычная глушилка. Сейчас американцы как раз работают над мегаточными гироскопами, которые будут позволять выдерживать направление, не используя показания GPS.
     
     
  • 3.91, Аноним (-), 04:23, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Сейчас американцы как раз работают над мегаточными гироскопами...

    Хорошо бы, ибо - тупик :-| ... да вот только в отличае от тебя - амеры не дураки :-(
    PS: Гороскопы времён WWII позволяли работать тем стратегам ночью. С точностью до города, да :) но дык больше полувека прошло уж как ...


     
     
  • 4.103, Аноним (-), 17:30, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > PS: Гороскопы времён WWII позволяли работать тем стратегам ночью.

    Ну, так все правильно - днем же звезд не видать. Как же с гороскопом без звезд-то работать. А стратеги, видно, те еще астрологи...


     
     
  • 5.109, Anonizmus (?), 20:48, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > Ну, так все правильно - днем же звезд не видать. Как же
    > с гороскопом без звезд-то работать. А стратеги, видно, те еще астрологи...

    Вот немецкая разведка с помощью форса гороскопов сорвала отступление французских войск...


     

  • 1.43, my (?), 15:06, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Что-то не компилится.
    > as: unrecognized option '-mcpu=cortex-a9'
     
     
  • 2.48, Kodir (ok), 15:58, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Там надо исправить: '-mcpu=microwave'
     
     
  • 3.74, Аноним (-), 19:14, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Там надо исправить: '-mcpu=microwave'

    Судя по вышеизложеннному, -mcpu=F-16.

     
  • 2.128, Аноним (-), 02:14, 01/08/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Ну если ты пытаешься заставить ассемблер с компилировать код с оптимизацией под ЦП, то помочь тебе нечем.
     

  • 1.45, Zenitur (ok), 15:43, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Если там не Systemd то ненужно. Ведь всё, на чём нет Systemdб крутые хакеры объявляют устаревшим и не модным.
     
     
  • 2.49, Andrey Mitrofanov (?), 16:01, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Пусть Поттер это генералу Динамиксу в лицо скажет! >/<
     

  • 1.51, Пропатентный тролль (?), 16:09, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    А была ли доказана безошибочность программ, которые использовались при провекри безошибочности?
     
     
  • 2.78, Аноним (-), 22:06, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • –1 +/
    А была ли доказана безошибочность программ, которые использовались при проверке безошибочности программ, которые использовались при проверке безошибочности?
     
     
  • 3.92, Аноним (-), 04:24, 30/07/2014 [^] [^^] [^^^] [ответить]  
  • +/
    Нет не была. Почему тест крэшился :))))

     

  • 1.59, Аноним (-), 17:12, 29/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –4 +/
    Чем оно надёжнее проверенного Windows Core?
     
     
  • 2.67, Аноним (-), 18:52, 29/07/2014 [^] [^^] [^^^] [ответить]  
  • +4 +/
    > Чем оно надёжнее проверенного Windows Core?

    Чем windows core.

     

  • 1.102, Аноним (-), 16:15, 30/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Рилтайм от блекбери круче, инф100!1 да и кореос торт а не печенько рекламное
     
  • 1.107, Anonizmus (?), 20:43, 30/07/2014 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    Это что попытка диверсии типа программы "Звездных войн"?

     
     
  • 2.129, Аноним (-), 02:17, 01/08/2014 [^] [^^] [^^^] [ответить]  
  • +/
    > Это что попытка диверсии типа программы "Звездных войн"?

    Звери, а не люди: провоцируют вероятного противника писать софт вместо того, чтобы менять нескучные обои в своем болгеносе.

     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Спонсоры:
    MIRhosting
    Fornex
    Hosting by Ihor
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2019 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру