The OpenNET Project / Index page

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



"Проекту seL4 присуждена премия ACM Software System Award"
Вариант для распечатки  
Пред. тема | След. тема 
Форум Разговоры, обсуждение новостей
Изначальное сообщение [ Отслеживать ]

"Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от opennews (??), 06-Май-23, 22:34 
Проект, развивающий открытое микроядро seL4, получил премию ACM Software System Award, ежегодно присуждаемую Ассоциация вычислительной техники (ACM), наиболее авторитетной международной организации в области компьютерных систем. Премия присуждена за достижения в области математического доказательства надёжности работы, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям и признаёт готовность использования в критически важных применениях. Проект seL4 показал, что можно не только полностью провести формальную верификацию  надёжности и безопасности для проектов уровня промышленных операционных систем, но и добиться этого без ущерба производительности и универсальности...

Подробнее: https://www.opennet.ru/opennews/art.shtml?num=59091

Ответить | Правка | Cообщить модератору

Оглавление

Сообщения [Сортировка по времени | RSS]


1. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (1), 06-Май-23, 22:34 
Скоро Фуксия со своим Цирконом спустится и покроет всё стадо.
Ответить | Правка | Наверх | Cообщить модератору

3. "Проекту seL4 присуждена премия ACM Software System Award"  –1 +/
Сообщение от пох. (?), 06-Май-23, 22:38 
Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник?

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

В принципе, конечно, от sel4 тоже толку никакого, занятный но феерично ненужный артефакт.

Ответить | Правка | Наверх | Cообщить модератору

5. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от Аноним (1), 06-Май-23, 23:11 
Про джаву тоже говорили что он только для кофемашин. И где сейчас джава? Да она везде, бро!
Ответить | Правка | Наверх | Cообщить модератору

36. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от _ (??), 08-Май-23, 04:15 
Ну да - на всех кладбищах (enterprise environment). Новых проектов на ней нет. Как и предсказывалось - новый Кобол :(
Ответить | Правка | Наверх | Cообщить модератору

38. "Проекту seL4 присуждена премия ACM Software System Award"  –1 +/
Сообщение от Аноним (38), 08-Май-23, 08:49 
Ксожалению, таки есть. Для новых прозектов берут Швинг и продолжают пейсать на джяве. И логика в этом есть, и есть причины так делать.
Ответить | Правка | Наверх | Cообщить модератору

39. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от Аноним (39), 08-Май-23, 11:20 
А чем Котлин не джава?
Ответить | Правка | Наверх | Cообщить модератору

63. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (63), 11-Май-23, 21:00 
> на всех кладбищах (enterprise environment)

Однако эти "кладбища" почему-то способны платить тебе стабильную хорошую ЗП, в отличие от "новых проектов" твоего одноклассника Васяна на модных язычках, от которых писаются кипятком все пацаны на раёне

Ответить | Правка | К родителю #36 | Наверх | Cообщить модератору

40. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Заноним (?), 08-Май-23, 18:51 
Да не везде, и вообще она давно закатывается. И даже graalvm её не вытянет.
Как ранее сказали - очередной cobol.
Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

64. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (63), 11-Май-23, 21:01 
Мне нравятся такие "древние" языки.
Чем меньше дешёвой школоты хочет с ней работать - тем больше моя ЗП
Ответить | Правка | Наверх | Cообщить модератору

65. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Заноним (?), 12-Май-23, 00:28 
Ну на java столько понаписали, что ЗП ещё долго будут платить.
Ответить | Правка | Наверх | Cообщить модератору

43. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от Аноним (43), 08-Май-23, 21:36 
> Скоро Фуксия

у гугла и на sel4 есть ОС

https://www.opennet.ru/opennews/art.shtml?num=57920

Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

6. "Проекту seL4 присуждена премия ACM Software System Award"  +7 +/
Сообщение от Анонн (?), 06-Май-23, 23:20 
Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать софт.
Там всего меньше 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

Ответить | Правка | Наверх | Cообщить модератору

7. "Проекту seL4 присуждена премия ACM Software System Award"  –1 +/
Сообщение от Аноним (1), 06-Май-23, 23:29 
Поэтому Hurd и не смогли дописать.
Ответить | Правка | Наверх | Cообщить модератору

10. "Проекту seL4 присуждена премия ACM Software System Award"  –2 +/
Сообщение от пох. (?), 07-Май-23, 00:10 
Нет, его к счастью писали, а не верифицировали-верифицировали.

Просто на фоне линукса это неповоротливое чудовище (с драйверами, как нельзя более кстати, копипащенными из линукса же) оказалось никому совершенно не нужным.

Т.е. добились что оно загружалось и можно было даже набрать /bin/ls - но что делать дальше все равно никто не знал.

А это недоразумение даже и такого не может.

Ответить | Правка | Наверх | Cообщить модератору

8. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от vitalif (ok), 06-Май-23, 23:32 
в этом контексте "для проектов уровня промышленных операционных систем" звучит слегка забавно
Ответить | Правка | К родителю #6 | Наверх | Cообщить модератору

45. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от пох. (?), 08-Май-23, 23:09 
промышленная - это в промышленности. Каким-нибудь приводом конвейера управлять, с положением на две позиции - заготовка едет и заготовка стоит.

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

Ответить | Правка | Наверх | Cообщить модератору

22. "Проекту seL4 присуждена премия ACM Software System Award"  –1 +/
Сообщение от Аноним (22), 07-Май-23, 08:33 
верификация

Слово "проверка" ведь с более меньшим углеродным следом, товарищи.. )

Ответить | Правка | К родителю #6 | Наверх | Cообщить модератору

41. "Проекту seL4 присуждена премия ACM Software System Award"  +5 +/
Сообщение от Аноним (41), 08-Май-23, 19:24 
Верификация - проверка
Аутентификация - проверка
Авторизация - проверка
Валидация - проверка
Ответить | Правка | Наверх | Cообщить модератору

42. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от warlock66613email (ok), 08-Май-23, 20:58 
Интересные подробности. Я особенно обратил бы внимание на то, что 1) это всё пока без поддержки многоядерности/мультипроцессорности, 2) им пришлось жёстко отказаться от указателей на стек: если в коде указатель, то его цель — в куче. Довольно серьёзные ограничения, особенно если подумать о них вместе.
Ответить | Правка | К родителю #6 | Наверх | Cообщить модератору

9. Скрыто модератором  –1 +/
Сообщение от InuYasha (??), 06-Май-23, 23:37 
Ответить | Правка | Наверх | Cообщить модератору

11. Скрыто модератором  +2 +/
Сообщение от пох. (?), 07-Май-23, 00:11 
Ответить | Правка | Наверх | Cообщить модератору

12. Скрыто модератором  –1 +/
Сообщение от Аноним (12), 07-Май-23, 01:01 
Ответить | Правка | Наверх | Cообщить модератору

18. Скрыто модератором  +/
Сообщение от Аноним (18), 07-Май-23, 03:56 
Ответить | Правка | Наверх | Cообщить модератору

26. Скрыто модератором  +1 +/
Сообщение от пох. (?), 07-Май-23, 09:55 
Ответить | Правка | К родителю #12 | Наверх | Cообщить модератору

13. Скрыто модератором  +/
Сообщение от tty0 (?), 07-Май-23, 01:03 
Ответить | Правка | К родителю #11 | Наверх | Cообщить модератору

16. Скрыто модератором  –5 +/
Сообщение от Прохожий (??), 07-Май-23, 02:08 
Ответить | Правка | К родителю #9 | Наверх | Cообщить модератору

27. Скрыто модератором  +/
Сообщение от пох. (?), 07-Май-23, 09:58 
Ответить | Правка | Наверх | Cообщить модератору

24. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (24), 07-Май-23, 08:54 
Они что-то там на Haskell начудили, молодцы.

А я могу таким же образом мой код верифицировать?

У меня есть несколько крошечных проектов, на тысячу строк.

Ответить | Правка | Наверх | Cообщить модератору

61. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от warlock66613email (ok), 10-Май-23, 12:16 
Нет. Вы же наверняка используете сторонние библиотеки, как минимум стандартную библиотеку.
Ответить | Правка | Наверх | Cообщить модератору

29. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (29), 07-Май-23, 12:48 
> вручается за разработку программных систем, оказавших определяющее влияние на отрасль

шта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)

Ответить | Правка | Наверх | Cообщить модератору

31. "Проекту seL4 присуждена премия ACM Software System Award"  –1 +/
Сообщение от Аноним (31), 07-Май-23, 13:47 
https://www.opennet.ru/opennews/art.shtml?num=59052
Это Вам не подойдет?
Ответить | Правка | Наверх | Cообщить модератору

32. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от пох. (?), 07-Май-23, 16:34 
> А можно чуть подробнее, на что повлияла разработка seL4?

"Болгары восхитились!"

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

> (проверяемая, клоуны!)

этому - десять плетей за иноземные слова воспрещенные.
Не клоуны, а скоморохи!

Клоуны - это когда в DF докопался до адамантина на один лишний кубик.

Ответить | Правка | К родителю #29 | Наверх | Cообщить модератору

33. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Степан (?), 07-Май-23, 19:02 
> декстопа
> проверяемая, клоуны
Ответить | Правка | К родителю #29 | Наверх | Cообщить модератору

35. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от пох. (?), 07-Май-23, 21:54 
О, точно, двадцать плетей басурманину! Столешница, скоморох!

Ответить | Правка | Наверх | Cообщить модератору

44. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от Аноним (43), 08-Май-23, 21:47 
> на что повлияла разработка seL4?

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

https://en.wikipedia.org/wiki/PikeOS

Ответить | Правка | К родителю #29 | Наверх | Cообщить модератору

46. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от пох. (?), 08-Май-23, 23:17 
чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа. Когда при наличии двухканального датчика индус ляпает еще один китайский глючный (потому что не знает про второй канал или не умеет вообще в тот датчик) а потом кодит такое что счастливый клиент убивается апстену. Всем похрену.

https://en.wikipedia.org/wiki/PikeOS
It enables users to build certifiable smart devices for the Internet of things (IoT)

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

Ответить | Правка | Наверх | Cообщить модератору

47. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (43), 09-Май-23, 10:27 
> мне кажется что мэйнстрим сейчас - как в тойете с педалью газа

майнстрим сейчас исключить человеческий фактор из управления автомобилями

https://www.mobileye.com/

> Т.е. и этим прекрасным микроскопом просто забивают гвозди

они зарабатывают на всём, денег больше всего в ширпотребе. В автомобилях выпускаемых в Германии используют открытый фреймворк l4re

https://www.kernkonzept.com

Ответить | Правка | Наверх | Cообщить модератору

48. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от пох. (?), 09-Май-23, 11:28 
Ну вот тойета опередила тренд на десять лет. Правда, "исключенному" человеческому фактору кажется не очень понравилось вляпываться в стену.

Ответить | Правка | Наверх | Cообщить модератору

49. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от Аноним (49), 09-Май-23, 12:37 
> майнстрим сейчас исключить человеческий фактор из управления автомобилями
> https://www.mobileye.com/

Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
Маск вон, уже почти десять лет - "еще немного и уже почти совсем скоро" и ниче, пипл хавает за обе щеки.

А в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится.

Ответить | Правка | К родителю #47 | Наверх | Cообщить модератору

52. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от пох. (?), 09-Май-23, 15:24 
Ну зочем вы тгавите - Маск всего двух только пока и убил. (Ну трех если считать отправленного в космос с билетом в один конец)
Ответить | Правка | Наверх | Cообщить модератору

54. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (43), 09-Май-23, 16:25 
> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.

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

Ответить | Правка | К родителю #49 | Наверх | Cообщить модератору

55. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (49), 09-Май-23, 17:16 
>> Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
> для развития технологий нужны финансы это очевидно, но вы покупаете товары потому что лош.к ?

А в огороде бузина, это тоже очевидно.

Внезапно, можно развивать технологии и при этом выдавать продвинутых ассистентов в качестве промежуточного результата - _уже__работающих_, хоть и с определенными ограничениями, как например мерседес с их ассистентом, прошедшим SAE-Level-3 сертификацию.
А можно почти 10 лет просто обещать "уже почти совсем готово еще чуть-чуть!".

> а я думаю что для собственного комфорта. Но конечно можете и на собачках скакать вместо автомобилей. И ж..у берестой подтирать, бумага для лошк.в

"Как вместо ответа по существу или хотя бы по теме, создать абстрактное соломенное чучело и победить его, Опеннетная Демонстрация №100501"


Ответить | Правка | Наверх | Cообщить модератору

59. "Проекту seL4 присуждена премия ACM Software System Award"  +/
Сообщение от Аноним (43), 09-Май-23, 23:28 
> Внезапно, можно развивать технологии и при этом выдавать продвинутых ассистентов в качестве промежуточного результата - _уже__работающих_, хоть и с определенными ограничениями, как например мерседес с их ассистентом, прошедшим 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 что-то не сильно стремное в этой области появится" это просто газификация луж

Ответить | Правка | Наверх | Cообщить модератору

60. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от Аноним (49), 10-Май-23, 11:37 
> внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации L3 производитель берёт на себя отвественность при аварии по вине автопилота, а мерседесы сертифицирован только в Германии и штате Невада

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


> https://autocrypt.io/the-state-of-level-3-autonomous-driving.../
> технически возможен L5 уже сейчас, см YeyQ Ultra

Он "возможен" уже хрен его знает сколько лет - но только "на свой страх и риск". Т.е. то самое пресловутое "прорыв уже-почти-еще-немного".

> а ваши "в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится" это просто газификация луж

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

Ответить | Правка | Наверх | Cообщить модератору

62. "Проекту seL4 присуждена премия ACM Software System Award"  –1 +/
Сообщение от Аноним (43), 11-Май-23, 09:31 
> Он "возможен" уже хрен его знает сколько лет - но только "на свой страх и риск".

сказки не надо рассказывать - когда там всплеск развития ИИ начался ? несколько лет назад, и ты не понимаешь очевидных вещей - ответственность за ТС и отвественность за управление ТС это пипец какие разные вещи, никто за действия водителей отвественности не несёт кроме самого водителя, а начиная с L3 производитель автомобиля должен за это нести ответственность.

Ответить | Правка | Наверх | Cообщить модератору

51. "Проекту seL4 присуждена премия ACM Software System Award"  –2 +/
Сообщение от Анонимemail (51), 09-Май-23, 14:04 
с моей точки зрения вся эта идея формальной верификации микроядра и полученной за это награды преувеличена и не имеет реальной ценности.

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

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

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

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

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

Ответить | Правка | К родителю #46 | Наверх | Cообщить модератору

53. "Проекту seL4 присуждена премия ACM Software System Award"  +1 +/
Сообщение от пох. (?), 09-Май-23, 15:26 
поток сознания эксперта опеннета

Про то что такое формальная верификация и как это работает - читать ему разумеется, не интересно и незачем, у него уже есть ценное мнение.

Ответить | Правка | Наверх | Cообщить модератору

34. "Проекту seL4 присуждена премия ACM Software System Award"  –2 +/
Сообщение от fidoman (ok), 07-Май-23, 19:45 
Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдоры на месте.
Ответить | Правка | Наверх | Cообщить модератору

50. "Проекту seL4 присуждена премия ACM Software System Award"  –4 +/
Сообщение от Анонимemail (51), 09-Май-23, 14:03 
лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю разрабатывать прикладные решения на языке си-плюсплюс в среде майкрософт визуал студио, а для моих задач со средней нагрузкой предпочтительнее простой монолитный ядренной архитектуры виндовс,которая проверенная временем и хорошо изученная, а эти "легковесные" микроядра только усложняют работу без очевидных преимуществ для обычного прикладного разработчика,как говорится "если не сломалось - не чини" и кто то явно преувеличивает значимость этого проекта чтобы получить гранты и деньги, поэтому я не вижу ничего выдающегося в этом проекте и его награждении
Ответить | Правка | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема




Партнёры:
PostgresPro
Inferno Solutions
Hosting by Hoster.ru
Хостинг:

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