forum.opennet.ru - "Проекту seL4 присуждена премия ACM Software System Award" (49)

"Проекту 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.dev/opennews/art.shtml?num=59091
Ответить \| Правка \| Cообщить модератору

Оглавление

Скоро Фуксия со своим Цирконом спустится и покроет всё стадо , Аноним (1), 22:34 , 06-Май-23, (1)

Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник Не хотел бы, пох. (?), 22:38 , 06-Май-23, (3) –1

Про джаву тоже говорили что он только для кофемашин И где сейчас джава Да она , Аноним (1), 23:11 , 06-Май-23, (5) +1

Ну да - на всех кладбищах enterprise environment Новых проектов на ней нет К, _ (??), 04:15 , 08-Май-23, (36)

Ксожалению, таки есть Для новых прозектов берут Швинг и продолжают пейсать на д, Аноним (38), 08:49 , 08-Май-23, (38) –1

А чем Котлин не джава , Аноним (39), 11:20 , 08-Май-23, (39) +1

Однако эти кладбища почему-то способны платить тебе стабильную хорошую ЗП, в о, Аноним (63), 21:00 , 11-Май-23, (63)

Да не везде, и вообще она давно закатывается И даже graalvm её не вытянет Как р, Заноним (?), 18:51 , 08-Май-23, (40)

Мне нравятся такие древние языки Чем меньше дешёвой школоты хочет с ней работа, Аноним (63), 21:01 , 11-Май-23, (64)

Ну на java столько понаписали, что ЗП ещё долго будут платить , Заноним (?), 00:28 , 12-Май-23, (65)

у гугла и на sel4 есть ОСhttps www opennet ru opennews art shtml num 57920, Аноним (43), 21:36 , 08-Май-23, (43) +1

Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать со, Анонн (?), 23:20 , 06-Май-23, (6) +7

Поэтому Hurd и не смогли дописать , Аноним (1), 23:29 , 06-Май-23, (7) –1

Нет, его к счастью писали, а не верифицировали-верифицировали Просто на фоне лин, пох. (?), 00:10 , 07-Май-23, (10) –2

в этом контексте для проектов уровня промышленных операционных систем звучит с, vitalif (ok), 23:32 , 06-Май-23, (8)

промышленная - это в промышленности Каким-нибудь приводом конвейера управлять, , пох. (?), 23:09 , 08-Май-23, (45)

верификацияСлово проверка ведь с более меньшим углеродным следом, товарищи , Аноним (22), 08:33 , 07-Май-23, (22) –1

Верификация - проверкаАутентификация - проверкаАвторизация - проверкаВалидация -, Аноним (41), 19:24 , 08-Май-23, (41) +5

Интересные подробности Я особенно обратил бы внимание на то, что 1 это всё пок, warlock66613 (ok), 20:58 , 08-Май-23, (42)

Скрыто модератором, InuYasha (??), 23:37 , 06-Май-23, (9) –1

Скрыто модератором, пох. (?), 00:11 , 07-Май-23, (11) +2

Скрыто модератором, Аноним (12), 01:01 , 07-Май-23, (12) –1

Скрыто модератором, Аноним (18), 03:56 , 07-Май-23, (18)
Скрыто модератором, пох. (?), 09:55 , 07-Май-23, (26) +1

Скрыто модератором, tty0 (?), 01:03 , 07-Май-23, (13)

Скрыто модератором, Прохожий (??), 02:08 , 07-Май-23, (16) –5

Скрыто модератором, пох. (?), 09:58 , 07-Май-23, (27)

Они что-то там на Haskell начудили, молодцы А я могу таким же образом мой код ве, Аноним (24), 08:54 , 07-Май-23, (24)

Нет Вы же наверняка используете сторонние библиотеки, как минимум стандартную б, warlock66613 (ok), 12:16 , 10-Май-23, (61)

шта А можно чуть подробнее, на что повлияла разработка seL4 Может, какие-то О, Аноним (29), 12:48 , 07-Май-23, (29)

https www opennet ru opennews art shtml num 59052Это Вам не подойдет , Аноним (31), 13:47 , 07-Май-23, (31) –1
Болгары восхитились Ну и вообще, чего докопался, это не троллейбус из буханки,, пох. (?), 16:34 , 07-Май-23, (32)
Проекту seL4 присуждена премия ACM Software System Award, Степан (?), 19:02 , 07-Май-23, (33)

О, точно, двадцать плетей басурманину Столешница, скоморох , пох. (?), 21:54 , 07-Май-23, (35) +1

на разработку современных систем применяемых в критически важных областях - авто, Аноним (43), 21:47 , 08-Май-23, (44) +1

чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа Когда п, пох. (?), 23:17 , 08-Май-23, (46)

майнстрим сейчас исключить человеческий фактор из управления автомобилямиhttps , Аноним (43), 10:27 , 09-Май-23, (47)

Ну вот тойета опередила тренд на десять лет Правда, исключенному человеческом, пох. (?), 11:28 , 09-Май-23, (48)
Майстрим сейчас, как и всегда - подоить доверчивых лошк W инвесторов и потребляd, Аноним (49), 12:37 , 09-Май-23, (49) +1

Ну зочем вы тгавите - Маск всего двух только пока и убил Ну трех если считать , пох. (?), 15:24 , 09-Май-23, (52)
для развития технологий нужны финансы это очевидно, но вы покупаете товары потом, Аноним (43), 16:25 , 09-Май-23, (54)

А в огороде бузина, это тоже очевидно Внезапно, можно развивать технологии и при, Аноним (49), 17:16 , 09-Май-23, (55)

внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации , Аноним (43), 23:28 , 09-Май-23, (59)

Угу, чисто правовые сложности опять танцорам мешают, а не то они бы всем показ, Аноним (49), 11:37 , 10-Май-23, (60) +1

сказки не надо рассказывать - когда там всплеск развития ИИ начался несколько , Аноним (43), 09:31 , 11-Май-23, (62) –1

с моей точки зрения вся эта идея формальной верификации микроядра и полученной з, Аноним (51), 14:04 , 09-Май-23, (51) –2

поток сознания эксперта опеннетаПро то что такое формальная верификация и как эт, пох. (?), 15:26 , 09-Май-23, (53) +1

Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдо, fidoman (ok), 19:45 , 07-Май-23, (34) –2
лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю р, Аноним (51), 14:03 , 09-Май-23, (50) –4

Сообщения [Сортировка по времени | 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.dev/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" +/–

Сообщение от warlock66613 (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

Почему "непонятно для чего"?
Как раз понятно - чтобы использовать его как запускалку виртуальных машин и быть уверенным что не выйдет за пределы виртуалки.
"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."

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

18. Скрыто модератором +/–

Сообщение от Аноним (18), 07-Май-23, 03:56

Осталось ешё верифицированную виртулку написать. Если неверифицированную, то можно Genode взять.

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

26. Скрыто модератором +1 +/–

Сообщение от пох. (?), 07-Май-23, 09:55

> Почему "непонятно для чего"?
> Как раз понятно - чтобы использовать его как запускалку виртуальных машин и
для запускалки виртуальных машин общего назначения а не чего-то совсем не от мира сего - надо уметь в сети, диски, межхостовый обмен, паравиртуализацию и Б-г знает чего еще кажущееся очевидным я забыл.
А тут ничего нет, пустыня.
> быть уверенным что не выйдет за пределы виртуалки.
виртуалка без сети, дисков и управления и так никуда не выйдет, а выйдет так пожалеет что вышла - потому что там опять ничегошеньки нет.
То есть написать это все (неизвестно, между нами, с какой итоговой производительносью и куда при этом пойдет верифицированность) наверное можно, но нереально - нет у человечества столько лишних кодеров.
Остаются только совсем уж странные нишевые применения, а поскольку те никогда не будут массовыми - рынок и в этих нишах выберет что попроще и попонятнее.

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

13. Скрыто модератором +/–

Сообщение от tty0 (?), 07-Май-23, 01:03

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

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

16. Скрыто модератором –5 +/–

Сообщение от Прохожий (??), 07-Май-23, 02:08

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

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

27. Скрыто модератором +/–

Сообщение от пох. (?), 07-Май-23, 09:58

> Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во
> время разработки. Остальные верифицировать займёт куда меньше времени.
да, просто прекрасно. Все время разработки уходит на борьбу с компилятором, потом чувак сдается и пишет unsafe {мамойклянус!}
Результат - компилятор успешно защитил, нет разработки нет и ошибок.
Не правда ли, ресдох?

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

24. "Проекту seL4 присуждена премия ACM Software System Award" +/–

Сообщение от Аноним (24), 07-Май-23, 08:54

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

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

61. "Проекту seL4 присуждена премия ACM Software System Award" +/–

Сообщение от warlock66613 (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.dev/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 +/–

Сообщение от Аноним (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 +/–

Сообщение от Аноним (51), 09-Май-23, 14:03

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

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

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

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

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2025 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру

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.dev/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"	+/–
	Сообщение от warlock66613 (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
	Почему "непонятно для чего"? Как раз понятно - чтобы использовать его как запускалку виртуальных машин и быть уверенным что не выйдет за пределы виртуалки. "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."
	Ответить \| Правка \| Наверх \| Cообщить модератору


	18. Скрыто модератором	+/–
	Сообщение от Аноним (18), 07-Май-23, 03:56
	Осталось ешё верифицированную виртулку написать. Если неверифицированную, то можно Genode взять.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	26. Скрыто модератором	+1 +/–
	Сообщение от пох. (?), 07-Май-23, 09:55
	> Почему "непонятно для чего"? > Как раз понятно - чтобы использовать его как запускалку виртуальных машин и для запускалки виртуальных машин общего назначения а не чего-то совсем не от мира сего - надо уметь в сети, диски, межхостовый обмен, паравиртуализацию и Б-г знает чего еще кажущееся очевидным я забыл. А тут ничего нет, пустыня. > быть уверенным что не выйдет за пределы виртуалки. виртуалка без сети, дисков и управления и так никуда не выйдет, а выйдет так пожалеет что вышла - потому что там опять ничегошеньки нет. То есть написать это все (неизвестно, между нами, с какой итоговой производительносью и куда при этом пойдет верифицированность) наверное можно, но нереально - нет у человечества столько лишних кодеров. Остаются только совсем уж странные нишевые применения, а поскольку те никогда не будут массовыми - рынок и в этих нишах выберет что попроще и попонятнее.
	Ответить \| Правка \| К родителю #12 \| Наверх \| Cообщить модератору


	13. Скрыто модератором	+/–
	Сообщение от tty0 (?), 07-Май-23, 01:03
	Проблема в том, что людей, которым нужен не продукт, а инструмент слишком мало. На этом проекте можно реализовать очень крутые вещи, к примеру, захардкодив ядро целиком в железе. Но это слишком долго, а значит будем по старинке - нестабильное ядро и много обновлений
	Ответить \| Правка \| К родителю #11 \| Наверх \| Cообщить модератору


	16. Скрыто модератором	–5 +/–
	Сообщение от Прохожий (??), 07-Май-23, 02:08
	С логикой и здравым смыслом у очередного местного аналитика (от слова анал) всё, как обычно, то есть никак. Если уж кто и будет задыхаться и дёргаться в припадках, так это Сишники. 9 тыс. строк кода и 8 лет верификации - прекрасная производительность (нет). Не говоря уж о стоимости. Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во время разработки. Остальные верифицировать займёт куда меньше времени.
	Ответить \| Правка \| К родителю #9 \| Наверх \| Cообщить модератору


	27. Скрыто модератором	+/–
	Сообщение от пох. (?), 07-Май-23, 09:58
	> Куда лучше всё-таки, когда от подавляющей части ошибок защищает компилятор прямо во > время разработки. Остальные верифицировать займёт куда меньше времени. да, просто прекрасно. Все время разработки уходит на борьбу с компилятором, потом чувак сдается и пишет unsafe {мамойклянус!} Результат - компилятор успешно защитил, нет разработки нет и ошибок. Не правда ли, ресдох?
	Ответить \| Правка \| Наверх \| Cообщить модератору

24. "Проекту seL4 присуждена премия ACM Software System Award"	+/–
Сообщение от Аноним (24), 07-Май-23, 08:54
Они что-то там на Haskell начудили, молодцы. А я могу таким же образом мой код верифицировать? У меня есть несколько крошечных проектов, на тысячу строк.
Ответить \| Правка \| Наверх \| Cообщить модератору


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

29. "Проекту seL4 присуждена премия ACM Software System Award"	+/–
Сообщение от Аноним (29), 07-Май-23, 12:48
> вручается за разработку программных систем, оказавших определяющее влияние на отрасль шта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)
Ответить \| Правка \| Наверх \| Cообщить модератору