Проект, развивающий открытое микроядро seL4, получил премию ACM Software System Award, ежегодно присуждаемую Ассоциация вычислительной техники (ACM), наиболее авторитетной международной организации в области компьютерных систем. Премия присуждена за достижения в области математического доказательства надёжности работы, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям и признаёт готовность использования в критически важных применениях. Проект seL4 показал, что можно не только полностью провести формальную верификацию надёжности и безопасности для проектов уровня промышленных операционных систем, но и добиться этого без ущерба производительности и универсальности...Подробнее: https://www.opennet.ru/opennews/art.shtml?num=59091
Скоро Фуксия со своим Цирконом спустится и покроет всё стадо.
Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник?Не хотел бы тебя огорчать, дружище, но это дно. С него спускаться дальше некуда. Сдохла твоя фикция, не взлетела.
В принципе, конечно, от sel4 тоже толку никакого, занятный но феерично ненужный артефакт.
Про джаву тоже говорили что он только для кофемашин. И где сейчас джава? Да она везде, бро!
Ну да - на всех кладбищах (enterprise environment). Новых проектов на ней нет. Как и предсказывалось - новый Кобол :(
Ксожалению, таки есть. Для новых прозектов берут Швинг и продолжают пейсать на джяве. И логика в этом есть, и есть причины так делать.
А чем Котлин не джава?
> на всех кладбищах (enterprise environment)Однако эти "кладбища" почему-то способны платить тебе стабильную хорошую ЗП, в отличие от "новых проектов" твоего одноклассника Васяна на модных язычках, от которых писаются кипятком все пацаны на раёне
Да не везде, и вообще она давно закатывается. И даже graalvm её не вытянет.
Как ранее сказали - очередной cobol.
Мне нравятся такие "древние" языки.
Чем меньше дешёвой школоты хочет с ней работать - тем больше моя ЗП
Ну на java столько понаписали, что ЗП ещё долго будут платить.
> Скоро Фуксияу гугла и на sel4 есть ОС
Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать софт.
Там всего меньше 10к строк кода ("8,700 lines of C code and 600 lines of assemble" если быть точным).При этом "затраты" на аналогичную верификацию при уже проработанной методологии - 8 (восемь) человеко-лет ("kernel plus proof of 8 py")
В процессе верификации пришлось писать кучу уточнений,
нашли 16 дефектов до второй фазы верификации, сама формальная верификация нашла 144 дефекта и необходимость внести 54 изменения. Т.е. где-то 1 дефект на 50 строк си/асм кода.Подробности тут: https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
Поэтому Hurd и не смогли дописать.
Нет, его к счастью писали, а не верифицировали-верифицировали.Просто на фоне линукса это неповоротливое чудовище (с драйверами, как нельзя более кстати, копипащенными из линукса же) оказалось никому совершенно не нужным.
Т.е. добились что оно загружалось и можно было даже набрать /bin/ls - но что делать дальше все равно никто не знал.
А это недоразумение даже и такого не может.
в этом контексте "для проектов уровня промышленных операционных систем" звучит слегка забавно
промышленная - это в промышленности. Каким-нибудь приводом конвейера управлять, с положением на две позиции - заготовка едет и заготовка стоит.Или еще что незамысловатое. Тут верю, вполне годится. Ну если pic какой слишком сложно этим озадачить.
верификацияСлово "проверка" ведь с более меньшим углеродным следом, товарищи.. )
Верификация - проверка
Аутентификация - проверка
Авторизация - проверка
Валидация - проверка
Интересные подробности. Я особенно обратил бы внимание на то, что 1) это всё пока без поддержки многоядерности/мультипроцессорности, 2) им пришлось жёстко отказаться от указателей на стек: если в коде указатель, то его цель — в куче. Довольно серьёзные ограничения, особенно если подумать о них вместе.
Сейчас растоманы не просто нервно курят в сторонке, а задыхаются в дыму, дёргаясь в припадках )
Ну если честно - их ресдох хотя бы был похож на законченую операционную систему. А тут голое микроядро непонятно для чего, зато верифицированное.
Почему "непонятно для чего"?
Как раз понятно - чтобы использовать его как запускалку виртуальных машин и быть уверенным что не выйдет за пределы виртуалки.
"seL4 can run Linux in a virtual machine. seL4 is [...] hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming."
Осталось ешё верифицированную виртулку написать. Если неверифицированную, то можно Genode взять.
> Почему "непонятно для чего"?
> Как раз понятно - чтобы использовать его как запускалку виртуальных машин идля запускалки виртуальных машин общего назначения а не чего-то совсем не от мира сего - надо уметь в сети, диски, межхостовый обмен, паравиртуализацию и Б-г знает чего еще кажущееся очевидным я забыл.
А тут ничего нет, пустыня.
> быть уверенным что не выйдет за пределы виртуалки.
виртуалка без сети, дисков и управления и так никуда не выйдет, а выйдет так пожалеет что вышла - потому что там опять ничегошеньки нет.
То есть написать это все (неизвестно, между нами, с какой итоговой производительносью и куда при этом пойдет верифицированность) наверное можно, но нереально - нет у человечества столько лишних кодеров.
Остаются только совсем уж странные нишевые применения, а поскольку те никогда не будут массовыми - рынок и в этих нишах выберет что попроще и попонятнее.
Проблема в том, что людей, которым нужен не продукт, а инструмент слишком мало. На этом проекте можно реализовать очень крутые вещи, к примеру, захардкодив ядро целиком в железе. Но это слишком долго, а значит будем по старинке - нестабильное ядро и много обновлений
С логикой и здравым смыслом у очередного местного аналитика (от слова анал) всё, как обычно, то есть никак.Если уж кто и будет задыхаться и дёргаться в припадках, так это Сишники. 9 тыс. строк кода и 8 лет верификации - прекрасная производительность (нет). Не говоря уж о стоимости.
Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во время разработки. Остальные верифицировать займёт куда меньше времени.
> Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во
> время разработки. Остальные верифицировать займёт куда меньше времени.да, просто прекрасно. Все время разработки уходит на борьбу с компилятором, потом чувак сдается и пишет unsafe {мамойклянус!}
Результат - компилятор успешно защитил, нет разработки нет и ошибок.Не правда ли, ресдох?
Они что-то там на Haskell начудили, молодцы.А я могу таким же образом мой код верифицировать?
У меня есть несколько крошечных проектов, на тысячу строк.
Нет. Вы же наверняка используете сторонние библиотеки, как минимум стандартную библиотеку.
> вручается за разработку программных систем, оказавших определяющее влияние на отрасльшта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)
https://www.opennet.ru/opennews/art.shtml?num=59052
Это Вам не подойдет?
> А можно чуть подробнее, на что повлияла разработка seL4?"Болгары восхитились!"
Ну и вообще, чего докопался, это не троллейбус из буханки, это корабль в бутылке в форме буханки. Кросивое! Поставить в музей на центральное место экспозиции, ходить вокруг на цыпочках, умиляться. Потом, когда-нибудь, обнаружим что интел впилил ее в ядро своего ME заместо нынешнего (тоже троллейбуса но гораздо менее выдающегося) или еще где в подобном месте всплывет.
> (проверяемая, клоуны!)
этому - десять плетей за иноземные слова воспрещенные.
Не клоуны, а скоморохи!Клоуны - это когда в DF докопался до адамантина на один лишний кубик.
> декстопа
> проверяемая, клоуны
О, точно, двадцать плетей басурманину! Столешница, скоморох!
> на что повлияла разработка seL4?на разработку современных систем применяемых в критически важных областях - автомобильной, медицинской, аерокосмической, военной. Сейчас майнстрим - гипервизор на клонах L4, см например
чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа. Когда при наличии двухканального датчика индус ляпает еще один китайский глючный (потому что не знает про второй канал или не умеет вообще в тот датчик) а потом кодит такое что счастливый клиент убивается апстену. Всем похрену.https://en.wikipedia.org/wiki/PikeOS
It enables users to build certifiable smart devices for the Internet of things (IoT)Т.е. и этим прекрасным микроскопом просто забивают гвозди.
Ну в общем логично, учитывая eclipse и прочий трэшачок.
> мне кажется что мэйнстрим сейчас - как в тойете с педалью газамайнстрим сейчас исключить человеческий фактор из управления автомобилями
> Т.е. и этим прекрасным микроскопом просто забивают гвозди
они зарабатывают на всём, денег больше всего в ширпотребе. В автомобилях выпускаемых в Германии используют открытый фреймворк l4re
Ну вот тойета опередила тренд на десять лет. Правда, "исключенному" человеческому фактору кажется не очень понравилось вляпываться в стену.
> майнстрим сейчас исключить человеческий фактор из управления автомобилями
> https://www.mobileye.com/Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
Маск вон, уже почти десять лет - "еще немного и уже почти совсем скоро" и ниче, пипл хавает за обе щеки.А в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится.
Ну зочем вы тгавите - Маск всего двух только пока и убил. (Ну трех если считать отправленного в космос с билетом в один конец)
> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.для развития технологий нужны финансы это очевидно, но вы покупаете товары потому что лош.к ? а я думаю что для собственного комфорта. Но конечно можете и на собачках скакать вместо автомобилей. И ж..у берестой подтирать, бумага для лошк.в
>> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
> для развития технологий нужны финансы это очевидно, но вы покупаете товары потому что лош.к ?А в огороде бузина, это тоже очевидно.
Внезапно, можно развивать технологии и при этом выдавать продвинутых ассистентов в качестве промежуточного результата - _уже__работающих_, хоть и с определенными ограничениями, как например мерседес с их ассистентом, прошедшим SAE-Level-3 сертификацию.
А можно почти 10 лет просто обещать "уже почти совсем готово еще чуть-чуть!".
> а я думаю что для собственного комфорта. Но конечно можете и на собачках скакать вместо автомобилей. И ж..у берестой подтирать, бумага для лошк.в"Как вместо ответа по существу или хотя бы по теме, создать абстрактное соломенное чучело и победить его, Опеннетная Демонстрация №100501"
> Внезапно, можно развивать технологии и при этом выдавать продвинутых ассистентов в качестве промежуточного результата - _уже__работающих_, хоть и с определенными ограничениями, как например мерседес с их ассистентом, прошедшим SAE-Level-3 сертификацию.внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации L3 производитель берёт на себя отвественность при аварии по вине автопилота, а мерседесы сертифицирован только в Германии и штате Невада
https://autocrypt.io/the-state-of-level-3-autonomous-driving.../
технически возможен L5 уже сейчас, см YeyQ Ultra
https://www.mobileye.com/technology/eyeq-chip
а ваши "в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится" это просто газификация луж
> внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации L3 производитель берёт на себя отвественность при аварии по вине автопилота, а мерседесы сертифицирован только в Германии и штате НевадаУгу, "чисто правовые сложности" опять танцорам мешают, а не то они бы всем показали.
Внезапно, это и есть тот самый "нюанс, Петька" - когда производитель берет ответственность за свои заявления, а не прячет мелким шрифтом "работающий супер-автопилот-аналогов-нет ... только будьте готовы в любой момент перехватить управления и если что, мы не виноваты, виноваты вы!".
> https://autocrypt.io/the-state-of-level-3-autonomous-driving.../
> технически возможен L5 уже сейчас, см YeyQ UltraОн "возможен" уже хрен его знает сколько лет - но только "на свой страх и риск". Т.е. то самое пресловутое "прорыв уже-почти-еще-немного".
> а ваши "в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится" это просто газификация луж
Ну давай ссылку, где приобрести такую бибику, раз газификатор тут не ты. Только учти - "не сильно стремное" предполагает как раз, что произовдитель не только умеет в красивый маркетинг и обещания, но и еще и отвечать за свои слова.
> Он "возможен" уже хрен его знает сколько лет - но только "на свой страх и риск".сказки не надо рассказывать - когда там всплеск развития ИИ начался ? несколько лет назад, и ты не понимаешь очевидных вещей - ответственность за ТС и отвественность за управление ТС это пипец какие разные вещи, никто за действия водителей отвественности не несёт кроме самого водителя, а начиная с L3 производитель автомобиля должен за это нести ответственность.
с моей точки зрения вся эта идея формальной верификации микроядра и полученной за это награды преувеличена и не имеет реальной ценности.во-первых для большинства реальных задач разработчикам подобные фокусы с "абстрактной точностью" не нужны, нам надо производительные и стабильные решения, а не надменные громоздкие конструкции инженеров.
во-вторых я не верю что полная формальная верификация реально возможна, в любой сложной системе остаются упущения и баги которые обнаружатся только во время работы.
в-третьих похоже что весь этот проект продвигается ради грантов и личного признания его создателей, несмотря на отсутствие какой-либо реальной пользы для большинства пользователей. пиар и завышенные ожидания - основные инструменты для привлечения средств.
поэтому лично я считаю что эта награда не оправдана и проект не решает реальные проблемы, скорее это очередное "блестящее" теоретическое предложение без настоящей ценности, а награда лишь демонстрирует избирательность экспертов.
в целом мне кажется что много шума из ничего, типичная "технологическая хайпа" с целью получения финансирования и продвижения, а не ради каких-то реальных достижений или прорывов
поток сознания эксперта опеннетаПро то что такое формальная верификация и как это работает - читать ему разумеется, не интересно и незачем, у него уже есть ценное мнение.
Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдоры на месте.
лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю разрабатывать прикладные решения на языке си-плюсплюс в среде майкрософт визуал студио, а для моих задач со средней нагрузкой предпочтительнее простой монолитный ядренной архитектуры виндовс,которая проверенная временем и хорошо изученная, а эти "легковесные" микроядра только усложняют работу без очевидных преимуществ для обычного прикладного разработчика,как говорится "если не сломалось - не чини" и кто то явно преувеличивает значимость этого проекта чтобы получить гранты и деньги, поэтому я не вижу ничего выдающегося в этом проекте и его награждении