forum.opennet.ru - "Микроядро seL4 математически верифицировано для архитектуры ..." (197)

"Микроядро seL4 математически верифицировано для архитектуры ..."

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

"Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
Сообщение от opennews (?), 10-Июн-20, 12:28
Организация RISC-V Foundation сообщила о верификации работы микроядра seL4 на системах с архитектурой набора команд RISC-V. Верификация сводится к математическому доказательству надёжности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров RISC-V RV64, требующих повышенного уровня надёжности и гарантирующих отсутствие сбоев... Подробнее: https://www.opennet.me/opennews/art.shtml?num=53129
Ответить \| Правка \| Cообщить модератору

Оглавление

осталось только распространить risc-v в массах и тогда можно будет закопать x86, neAnonim (?), 12:28 , 10-Июн-20, (1) +13

Закопать то вряд ли, но это явно тот путь, по которому следует развиваться, Аноним (2), 12:33 , 10-Июн-20, (2) +12

Интел не позволит, закопают всех конкурентов в округе , Аноним (49), 16:43 , 10-Июн-20, (49) –1

Сначала интелю нужно повторить трюк Мюнхгаузена вытащить себя за волосы , а уж , erthink (ok), 16:48 , 10-Июн-20, (51) +4
Копать устанут - его уже толпа фирм взяли в оборот И кстати говорят что скоро фи, Аноним (-), 23:19 , 10-Июн-20, (108) +1

Тю, мелочи-то какие Займёмся сразу после отказа от империализма и излечения все, A.Stahl (ok), 12:55 , 10-Июн-20, (7) +19

Жалеешь 140 рублей , Сейд (ok), 13:15 , 10-Июн-20, (16)

, A.Stahl (ok), 13:52 , 10-Июн-20, (25) –1

https www crowdsupply com sifive hifive1-rev-b, Сейд (ok), 13:57 , 10-Июн-20, (26)

Мне показывает 59 , A.Stahl (ok), 14:42 , 10-Июн-20, (31)

https aliexpress ru item 4000818117666 html algo_pvid 39bba876-7da8-4940-9a95-, Аноним (41), 15:29 , 10-Июн-20, (41) +1

Трусы Большой Мужчина Женщина Купить Большой Проститутка Шланг, Ыр2.0 (?), 15:45 , 10-Июн-20, (44)
Просто любопытно вы в самом деле пользуетесь сайтом aliexpress на русском языке, ala (?), 16:44 , 10-Июн-20, (50) –3

Нисколько не поклонник, но разве на английском там сильно меньше удовольствий , erthink (ok), 16:50 , 10-Июн-20, (52) +2

Удивительно, но всё-таки сильно меньше По крайней мере, у меня такая выборка , n80 (?), 00:58 , 11-Июн-20, (120) +1
Английский более информативный , Аноним (132), 09:48 , 11-Июн-20, (132) –1

А ты пользуешься китайским вариантом или просто думаешь, что для алика родной ан, Аноним (86), 19:40 , 10-Июн-20, (86) +3

Алиэкспресс ориентируется на английский т к международный Таобао мандаринский , Аноним (132), 09:49 , 11-Июн-20, (133)
Просто на английском покупает сильно больше - так что этим можно и нормальный пе, Аноним (-), 14:33 , 11-Июн-20, (142) +1

Насколько знаю, при заходе с IP-адресов из RU областей aliexpress крайне настойч, n80 (?), 00:56 , 11-Июн-20, (119)
На английский переключаю, мандаринским ещё не овладел чтобы таобао читать , Аноним (132), 09:47 , 11-Июн-20, (131)
Но русскоязычный Ali показывает цены в национальной валюте В которой мы и плати, Аноним (166), 00:52 , 12-Июн-20, (166)

Понять по русскому описанию товара что это за неведомая штука в сколь-нибудь про, Аноним (171), 01:14 , 12-Июн-20, (171)

Промт-онлайн с ангийской версии Али не сильно лучше переведёт , Аноним (166), 01:14 , 13-Июн-20, (181)

А мне оно и не надо Если бы я не умел в инглиш, мой потолок в IT ограничивался , Аноним (-), 10:43 , 13-Июн-20, (186)

Кому этот перемикроконтроллер нужен-то Их rv64gc за килобакс производительностью, Michael Shigorin (ok), 18:58 , 10-Июн-20, (75) –1

Производителям домашней автоматизации , Сейд (ok), 22:43 , 10-Июн-20, (102)

Домашним автоматизаторам хватит пригоршни ЛА3, Аноним (49), 01:32 , 11-Июн-20, (126)

Да что там, спичек и желудей , Аноним (-), 14:34 , 11-Июн-20, (143) +1
ЛА3 потребуется очень большая пригоршня, т к триггеры, счётчики, регистры тоже , Аноним (166), 00:59 , 12-Июн-20, (167)

Как минимум, тем же, кому и остальные микроконтроллеры GigaDevice вообще презаня, n80 (?), 01:22 , 11-Июн-20, (124) +4

Спасибо В отличие от 90 флуда на этом сайте - у вас очень интересное сообщение, Леонид (??), 11:17 , 11-Июн-20, (137) +1
Еще у них есть ответвления F1xx-like которых в оригинале нет - например мелкие Q, Аноним (144), 14:41 , 11-Июн-20, (144) +1

Собственно, я об этой ситуации и говорил в 171 это давно напрашивалось, но ST , n80 (?), 02:23 , 14-Июн-20, (194)

Я честно говоря не понял почему в мелком корпусе, с usb и вообще F103-like обвес, Аноним (198), 06:15 , 15-Июн-20, (198)

https www sifive com boards hifive1-rev-b, Сейд (ok), 13:04 , 10-Июн-20, (12) –1
А risc-v сможет достичь сопоставимой производительности , Аноним (53), 16:57 , 10-Июн-20, (53) –1

RISC-V - это просто открытая система команд Соответственно, интель может прикру, erthink (ok), 17:17 , 10-Июн-20, (54) +6

Кроме этого есть еще и открытые реализации ядер Это, конечно, не интел - но воо, Аноним (144), 14:43 , 11-Июн-20, (145)

Risc-v это просто спецификация на набор команд Вот если вы сделаете хороший быс, NameName (?), 18:34 , 10-Июн-20, (70) +2

Все как в лучших домах - есть GCC и Clang И линухом это процессорное ядро подде, Аноним (162), 00:45 , 12-Июн-20, (162)

А потом откопать обратно , Аноним (118), 00:30 , 11-Июн-20, (118)

Вот, просто хороший DLS и никакой псевдонаучной претенциозности как у Rust , Аноним (3), 12:40 , 10-Июн-20, (3)

DSL, Аноним (3), 12:41 , 10-Июн-20, (5)
Что такое DLS Может DSL Domain Specific Language , Аноним (41), 12:45 , 10-Июн-20, (6)

да хватит играть уже с аббревиатурой LSD, Аноним (72), 18:39 , 10-Июн-20, (72) +17

Вообще-то оно на сишечке с асмом , Аноним (9), 13:01 , 10-Июн-20, (9) +1

Ядро на сишечке Пруф -- нет Причём пруф раз в 40 больше самого ядра , Аноним (14), 13:05 , 10-Июн-20, (14) +3

А вы чего хотели Скажите спасибо что он вообще за разумное время обсчитывается , Аноним (144), 14:44 , 11-Июн-20, (146)

Касперский при необходимости посчитает за разумное время любую NP-полную задач, Аноним (161), 21:47 , 11-Июн-20, (161) –2

Он сам как NP-полная задача , Аноним (162), 00:46 , 12-Июн-20, (163)

Всего-то пришлось свой компилятор C написать, и потом ещё 200к строк на Isabelle, Аноним (14), 13:04 , 10-Июн-20, (13)

В том то и элегантность решения, что компилятор C в 100500 раз проще Раста , Аноним (-), 14:34 , 10-Июн-20, (30) +2

Проще и безопаснее, так как в С нету unsafe, Аноним (33), 14:52 , 10-Июн-20, (33) +10
Вот вот, раст настолько убог что написание собственного компилятора С для каждой, Аноним (33), 14:54 , 10-Июн-20, (34)
Внезапный поворот компилятор, которым собирается seL4, написан ни разу не на C , Аноним (14), 18:17 , 10-Июн-20, (66) +1

Это как-то мешает собрать его компилятором си написаным на си , Аноним (162), 00:47 , 12-Июн-20, (164)

Слабое приплетание, на троечку , Аноним (17), 13:16 , 10-Июн-20, (17)

Давно в области безопасности не было таких хороших вестей, DmA (??), 12:40 , 10-Июн-20, (4) –1
может gnu hurd кто-нибудь перенесёт на seL4, Аноним (-), 12:59 , 10-Июн-20, (8) +2

Ноу проблем Сколько поатишь , Аноним (9), 13:02 , 10-Июн-20, (10)
Флаг в руки, ждём от тебя результатов , Аноним (11), 13:02 , 10-Июн-20, (11) –1
Люди, способные это сделать, не станут заниматься этим за идею , Аноним (17), 13:18 , 10-Июн-20, (18) +1
Было много попыток перевести Hurd с Mach на L4, к сожалению, все потерпели неуда, Сейд (ok), 13:19 , 10-Июн-20, (19)
смысл не в том, чтобы заменить gnu mach на seL4, а в том, чтобы gnu hurd работал, AnonAnonAnon (?), 13:32 , 10-Июн-20, (22)
Гурд жестко приколочен к 32 битам Его теперь проще переписать Это в вопросу о , Аноним (28), 14:12 , 10-Июн-20, (28) +2
На seL4 есть рабочая Genode https genode org , Аноним (41), 15:14 , 10-Июн-20, (35) +1

Genode под Nova пишется, все остальные ядра для галочки , bw (ok), 06:14 , 11-Июн-20, (128)

что-то не очень заметно, что на платах Arduino используется RISC-V, Аноним (-), 13:07 , 10-Июн-20, (15) –3

https www sifive com boards hifive1-rev-bhttps shop365481095 world taobao co, Сейд (ok), 13:36 , 10-Июн-20, (23)
https aliexpress ru item 4000299112762 html, Аноним (42), 15:36 , 10-Июн-20, (42)
Они анонсировали Arduino Cinque и 8230 всё Что, впрочем, нисколько не мешает к, Аноним (9), 20:14 , 10-Июн-20, (90)
Скоро ESP RISC-V подъедет, Аноним (182), 08:39 , 13-Июн-20, (182)

Вот это по настоящему важная новость Ещё бы понять, как наладить производство у, Аноним (21), 13:31 , 10-Июн-20, (21)

Берёшь L4 и https pulp-platform org и налаживаешь производство , Сейд (ok), 13:47 , 10-Июн-20, (24) +2

Эпл уже решило переходить на RISC-V вместо ARM , Аноним (28), 14:10 , 10-Июн-20, (27) –1

А что, они как-то обсуждали эту возможность , Аноним (41), 15:19 , 10-Июн-20, (37)

Я не слышал, но после такой будоражащей новости как эта могли и задуматься Не, Аноним (28), 17:36 , 10-Июн-20, (57) –1

Да и черт с ним с эплом Зато решили WD, Nvidia и много кто еще При том первая , Аноним (162), 00:50 , 12-Июн-20, (165)

Интересный исследовательский проект, но преподнесен ради хайпа вокруг RISC-V, ко, Аноним (29), 14:15 , 10-Июн-20, (29) +3

WD это хорошо он заменил mips на arm и riscv , но ты забыл про NVIDIA, лет 10 п, Аноним (40), 15:27 , 10-Июн-20, (40) –3

Чего лет 10 назад 10 лет назад архитектура только начала зарождаться Можно ссыл, Аноним (41), 15:36 , 10-Июн-20, (43) +2

Да, внезапно, nvidia стоит у истоков и первая радостно побежала экономить Насчё, Аноним (40), 16:11 , 10-Июн-20, (47) –2

Вы вообще всё здесь перепутали -- примерно так Нет Нет Нет Нет PS в отличие от , Michael Shigorin (ok), 19:07 , 10-Июн-20, (77) +3

Спасибо, я уже признал ошибку Это было про power9 , Аноним (40), 19:22 , 10-Июн-20, (80)

risc-v десктоп на power 9https ibb co 6gdgGHH, Михрютка (ok), 22:05 , 10-Июн-20, (97)

Он risc, это определённо И он десктоп , Аноним (40), 23:46 , 10-Июн-20, (112) –1

Очень хорошо сформулировано, erthink (ok), 16:00 , 10-Июн-20, (46) +2
Причём когда минимум из-за одного такого российского безфабричника восторчали уш, Michael Shigorin (ok), 19:05 , 10-Июн-20, (76) +1

А про кого это вы Вроде какая-то питерская контора занималась RISK-V, Леонид (??), 11:23 , 11-Июн-20, (138)

В своё время L4 было прорывом, но поезд несколько продвинулся за 25 лет Сейчас , erthink (ok), 14:50 , 10-Июн-20, (32) +4

Репутацию Kaspersky OS ещё никто не проверял Да и исходников её не покажут , Аноним (41), 15:18 , 10-Июн-20, (36) +3

Кому нужно уже показали, поэтому и пишу Проверка там в основном делается мате, erthink (ok), 15:51 , 10-Июн-20, (45) +3

R I Pо какой вообще проверке может идти речь при отсутствии открытых исходников , vitalif (ok), 18:16 , 10-Июн-20, (65) +1

Открыть исходники для проверки - это одно у M в таком режиме они открыты 25 л, erthink (ok), 18:24 , 10-Июн-20, (68) +4

Там даже систему виртуальной памяти пофиксить не могут, слишком сложный продукт , Аноним (118), 10:56 , 11-Июн-20, (136)

Хм, а где в слове натянуть есть упоминание верификации , erthink (ok), 14:03 , 11-Июн-20, (140) –1

Там хотя бы повторяемость сборки есть Открыты они А если по обновлениям приедет, vitalif (ok), 15:48 , 11-Июн-20, (153)

Рассуждая не зная предмета, вы просто рекламируете свою некомпетентность , erthink (ok), 16:09 , 11-Июн-20, (154) +1

Никого не волнует твоя компетентность Удел закрытой ОС - два с половиной закрыт, vitalif (ok), 16:28 , 11-Июн-20, (155)

Никому не интересно ваше ихпёртное мнение не читал, но осуждаю без базовой о, erthink (ok), 16:36 , 11-Июн-20, (156) +1

Да пусть идет, мне вообще пофиг, vitalif (ok), 20:08 , 11-Июн-20, (160)
Ихпертное мнение о структуре управления каспера можно на хабре почитать Дальше , Аноним (171), 01:16 , 12-Июн-20, (172) –2

Ничего себе, вы экспертное сообщество привели С таким же успехом можно и луком, Аноним (176), 09:53 , 12-Июн-20, (176)

Нормальное сообщество айтишников Получше многих других, имхо Хоть и хипстерско, Аноним (187), 10:46 , 13-Июн-20, (187) –1

Хз на счёт управления, не сведущ в вопросе, но видится мне, США не зря и не прос, Онаним (?), 21:46 , 14-Июн-20, (195) +1

мне это всегда нравилось у нас есть такие приборы но мы вам их не покажем изв, Михрютка (ok), 22:54 , 10-Июн-20, (104) +1

Считаем что стоили и выбросили, или что z OS всё еще строят 60 лет Тем не мен, erthink (ok), 23:11 , 10-Июн-20, (106) +2

z os в продуктиве работает все эти годы kasperskyos в продуктиве где-то работает, Михрютка (ok), 23:23 , 10-Июн-20, (109)

Ну RTFM ведь https os kaspersky ru projects На здоровье , erthink (ok), 23:57 , 10-Июн-20, (113) +1

Это по счастью будут в основном его проблемы, да нескольких везунчиков которым, Аноним (144), 14:49 , 11-Июн-20, (147)

Демагогия и FUD 1 мелкий , орки - А я верно предполагаю что в вашей системе , erthink (ok), 15:24 , 11-Июн-20, (152) +1

Оценка наиболее вероятного развития событий Такое счастье можно поюзать только , Аноним (168), 01:01 , 12-Июн-20, (168)

Что значит -- переиграет весь мир Весь мир и так себя самого переигрывает , НамеНаме (?), 17:58 , 13-Июн-20, (191)

Это реверанс в адрес если Kasperky OS взлетит Блин, скорее пингвины научатс, Аноним (-), 06:30 , 15-Июн-20, (199) –1

171 Танк шибко секретный Учёные могут и не знать 187 , Oxyd76 (?), 17:31 , 11-Июн-20, (157) –1
От того, что показали майору, нам не легче , Аноним (166), 01:06 , 12-Июн-20, (169) –1

ОЙ КАК ТОЛСТО , vitalif (ok), 15:22 , 10-Июн-20, (38) –2

Видимо стоит уточнить для местных ихпёртов, которые УВЫ не читали, но осуждают, erthink (ok), 17:48 , 10-Июн-20, (62) +4

Я всерьёз не могу это воспринимать даже Закрытое чудо, которое никто не видел, , vitalif (ok), 18:19 , 10-Июн-20, (67) +2

Т е если вы не трогали луну руками, то её нет Тем не менее, эту луну можно по, erthink (ok), 18:32 , 10-Июн-20, (69) +4

Там есть исходный код ядра и его можно собрать и запустить со своими правками , Аноним (98), 22:23 , 10-Июн-20, (98) +1

Нет Но за подробностями лучше RTFM , erthink (ok), 22:33 , 10-Июн-20, (99)

Разве это не принципиальный вопрос верификации И что там дают Уже собранную игр, Аноним (161), 10:55 , 11-Июн-20, (135) –1

Как там грится Джентльменамм верят на слово И тут мне карта как поперла, как п, Аноним (-), 06:31 , 15-Июн-20, (200) –1

Как будто репутация у вирусописателей Касперского чем-то сильно лучше Qualcomm , Аноним (39), 15:26 , 10-Июн-20, (39)
Касперский и репутация Хотя, может в каких-то там своих кругах , NameName (?), 17:24 , 10-Июн-20, (56) –3

Дефачка из PR-отдела отчаянно минусует, размазывая тушь соплями , NameName (?), 18:35 , 10-Июн-20, (71) –5

Ну не у каждой дефачке хватит соплей на вашу чушь , erthink (ok), 18:40 , 10-Июн-20, (73) +2

Ты смотри, а девачкам понравилось Плюсуют Бедненькие труженицы IT-сектора , НамеНаме (?), 18:22 , 11-Июн-20, (159)

Всё что я понял, что есть некая шайтан архитектура - RISC, есть её спецификации,, Аноним (48), 16:32 , 10-Июн-20, (48) –2

Ну Спарку можно сразу выкинуть , Аноним (49), 17:23 , 10-Июн-20, (55) +2

Почему , Аноним (48), 17:47 , 10-Июн-20, (60)

Теперь есть 15 конкурирующих стандартов , Аноним (28), 17:39 , 10-Июн-20, (58)

Что в этом плохого , Аноним (48), 17:47 , 10-Июн-20, (61)

А ты подумай Интел закрыт, как чёрт, жрёт, как слон, и ему абсолютно пох на к, Аноним (49), 18:46 , 10-Июн-20, (74) –3

Если бы не было 15 шт, было бы лучше, хуже Появится ещё 100500, пускай, если вз, Аноним (48), 19:27 , 10-Июн-20, (81) +2

Нет, НЕ хорошо Это - всего лишь показатель того, что отрасль так до сих пор и н, Аноним (176), 10:03 , 12-Июн-20, (179) –1

Ща им эппл подкатит годный сюрпризец кажись , Аноним (168), 01:07 , 12-Июн-20, (170)

УжЕ - нет И - никто, в ближайшие лет 30 - не подкатит Не до того будет , Аноним (176), 10:05 , 12-Июн-20, (180) –1

SuperH тоже risc И amd64 тоже risc, но это тщательно пытаются маскировать RISC, Аноним (40), 17:47 , 10-Июн-20, (59) +1

Какая из реализаций лучше всего подойдет для ПК, ноутов, планшетов, телефонов , Аноним (48), 17:53 , 10-Июн-20, (63) –1

Давно известно - волшебная , erthink (ok), 17:56 , 10-Июн-20, (64) +1

Подозреваю что ирония сарказм , Аноним (48), 19:28 , 10-Июн-20, (82) –1

Нет А то, что там RISC -- не называется AMD64 , Michael Shigorin (ok), 19:10 , 10-Июн-20, (78)

Скорее всего там технология аналогичная тому, что разрабатывала transmeta Дитя , Аноним (40), 19:20 , 10-Июн-20, (79)

Никто ничего не маскирует CISC это микрокод выполняющийся поверх RISC ядра Все, Аноним (83), 19:29 , 10-Июн-20, (83) –1

Возможно и так Когда-то я интересовался этим вопросом когда писал 16 битные пр, Аноним (40), 19:40 , 10-Июн-20, (85)

бранч предикторы - следствие наличия конвейера, а никак не микрокода RISC CISC , Аноним (83), 19:53 , 10-Июн-20, (87)

Но я не вижу тут противоречий Ведь x86 процессоры в частности нынешние архите, Аноним (40), 20:06 , 10-Июн-20, (88) –1

Это тавтология ВООБЩЕ ВСЕ CISC процессоры архитектурно содержат в себе RISC про, Аноним (83), 20:11 , 10-Июн-20, (89) –2

нет, это как раз ошибка Вся разница в том кто решает как правильно загружать ко, Cradle (?), 20:39 , 10-Июн-20, (92)

RISC-и тоже умеют в макрокомманды или как они называются, когда один опкод замен, Аноним из предыдущего ответа. (?), 20:58 , 10-Июн-20, (95) +1
PDP-11 не относят к RISC только по тому что во времена расcыпухи такого деления , Аноним (83), 22:49 , 10-Июн-20, (103)

https ru wikipedia org wiki D0 9A1801 D0 92 D0 9C1 , Cradle (?), 23:27 , 10-Июн-20, (110)

Да, я знаю про это Даже к друзьям на БуКашке периодически ходил играться для р, Аноним (83), 00:02 , 11-Июн-20, (115)

У меня вообще есть предположение, что слово RISC присваивают процессору, когда х, Аноним (83), 00:17 , 11-Июн-20, (116)

Нет У PDP-11 пачка омских режимов адресации, RISC всегда load store , Вебмакака (?), 12:25 , 11-Июн-20, (139)

load store - это вторичный половой признак Он является следствием, а не причино, Аноним (83), 14:25 , 11-Июн-20, (141)

Да сколько ж можно , Led (ok), 01:06 , 15-Июн-20, (197)

А что, разве в системе команд PDP11 не было команд, производящих изменения данны, Аноним (166), 01:16 , 12-Июн-20, (173)

VLIW EPIC разве не могут притворяться CISC Вроде и эльбрусы VLIW, притворяющи, Аноним (40), 20:45 , 10-Июн-20, (94)

CISC - это архитектура, а не система команд, а притворяются EPIC-и начиная с Кру, Аноним (83), 22:56 , 10-Июн-20, (105)

Там вон в новости про очередные дыры в интеле разрисовано что оно содержит RISC, Аноним (-), 14:51 , 11-Июн-20, (148)

Ну ты фантазёр 8230 , Аноним (9), 20:22 , 10-Июн-20, (91)

Люблю опеннет за наличие икспердов Люди уже даже эмулятор для микрокода 8080 на, Аноним (83), 22:39 , 10-Июн-20, (101)

Наличие микрокода не обязывает ядро быть RISCовым, Аноним (49), 01:16 , 11-Июн-20, (123)

Возможно он пытается сказать что блоки выполнения за uCode ROM сами по себе см, Аноним (-), 14:53 , 11-Июн-20, (149)

Бинго Первый тезка который это понял А то что у этих блоков выполнения вмест, Аноним (83), 18:12 , 11-Июн-20, (158)

Чиво RISC ядро появилось в 486, Аноним (98), 22:33 , 10-Июн-20, (100) +1

Если не Pentium II, Аноним (166), 01:27 , 12-Июн-20, (174)

MIPS это спецификация RISC от MIPS Technologies, Inc RISC-V это спецификация R, Аноним (132), 10:06 , 11-Июн-20, (134)

Так производите Даже какое-то из ядер выкладывали Просто это огроменный чип и , Аноним (-), 14:54 , 11-Июн-20, (150)

Пацаны это то самое открытое железо о котором мечтают все ГНУтые , Аноним (84), 19:35 , 10-Июн-20, (84)

нет, это только открытая система комманд без слишком явной привязки к какому-то , Cradle (?), 20:45 , 10-Июн-20, (93) +1

К тому же этих спецификаций вагон и маленькая тележка, я выше писал , Аноним (21), 21:04 , 10-Июн-20, (96) +1

Главное чтобы было всё без лицензионных отчислений , Аноним (-), 06:36 , 11-Июн-20, (129)

С виду - без, как начнёшь делать в железе - сразу появятся и отчисления и патен, Аноним (49), 02:32 , 12-Июн-20, (175) +1

О хо-хо, хо-хо , Аноним (185), 10:16 , 13-Июн-20, (185)

it is proved to be bug-free relative to a specificationТо есть, это всего-лишь д, Аноним (107), 23:18 , 10-Июн-20, (107) +2

Две банки жидкого азота господину Да, можно математически доказать, что проц бу, Аноним (49), 23:32 , 10-Июн-20, (111) +1

За науку я готов выпить хоть яду Проставляйся , Аноним (107), 23:59 , 10-Июн-20, (114) +1

Это не пить это для твоего проца , Аноним (49), 01:07 , 11-Июн-20, (121)

Мой проц справляется даже без радиатора Я давно уже не покупаю печки , Аноним (107), 01:24 , 11-Июн-20, (125)

Пусть сначала докажут что в самих спецификациях нет бага или бэкдора Для этого , Аноним (118), 00:26 , 11-Июн-20, (117) +1

Лучшее доказательство - отсутствие спекуляция при работе с памятью , Аноним (49), 01:11 , 11-Июн-20, (122) +2

Rowhammer у так например это похрен , Аноним (-), 14:55 , 11-Июн-20, (151) –1

А вы - точно понимаете значение употребляемых вами слов , Аноним (176), 09:57 , 12-Июн-20, (178)

Это, увы, не достижимо в принципе Ну так Рассель, Кантор, Гедоль ну и НамеНаме , НамеНаме (?), 18:02 , 13-Июн-20, (193)

https github com seL4 seL4 blob master src smp lock c 25 строк clh_lock_t big_, Vitaly (??), 05:11 , 11-Июн-20, (127)
А тем временем даже в Falcon 9 уже обыденный x86 , Онаним (?), 08:35 , 11-Июн-20, (130)

Нет Не обыденный Не обольщайтесь ложной простотой вопроса , Аноним (176), 09:54 , 12-Июн-20, (177) –1
В Еврефайтерах и Рафалях тоже х86 купленные на барахолке , а в Ф-22 960-тые и 8, НамеНаме (?), 17:55 , 13-Июн-20, (190)

Отличная новость, и ОС интересная Зато попиарили забесплатно закрытую нех о, Аноним (182), 09:51 , 13-Июн-20, (183) +1

Макса Чиркова деньги не интересуют , Аноним (185), 10:14 , 13-Июн-20, (184)
Какая страна, такая и ОС , Аноним (187), 10:49 , 13-Июн-20, (188)

По итогу самым безопасным окажется ядро Hello world , Аноним (201), 23:50 , 15-Июн-20, (201)

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

1. "Микроядро seL4 математически верифицировано для архитектуры ..." +13 +/–

Сообщение от neAnonim (?), 10-Июн-20, 12:28

осталось только распространить risc-v в массах. и тогда можно будет закопать x86

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

2. "Микроядро seL4 математически верифицировано для архитектуры ..." +12 +/–

Сообщение от Аноним (2), 10-Июн-20, 12:33

Закопать то вряд ли, но это явно тот путь, по которому следует развиваться

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

49. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (49), 10-Июн-20, 16:43

Интел не позволит, закопают всех конкурентов в округе.

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

51. "Микроядро seL4 математически верифицировано для архитектуры ..." +4 +/–

Сообщение от erthink (ok), 10-Июн-20, 16:48

> Интел не позволит, закопают всех конкурентов в округе.
Сначала интелю нужно повторить трюк Мюнхгаузена (вытащить себя за волосы), а уж потом может-быть, если повезет...

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

108. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (-), 10-Июн-20, 23:19

>  Интел не позволит, закопают всех конкурентов в округе.
Копать устанут - его уже толпа фирм взяли в оборот.
И кстати говорят что скоро фирму Интел будет ждать еще один приятный подарок: Эпл вроде бы на днях должен анонсировать переход на 64-битные ARM... :)

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

7. "Микроядро seL4 математически верифицировано для архитектуры ..." +19 +/–

Сообщение от A.Stahl (ok), 10-Июн-20, 12:55

>осталось только распространить risc-v в массах
Тю, мелочи-то какие. Займёмся сразу после отказа от империализма и излечения всех болезней.

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

16. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Сейд (ok), 10-Июн-20, 13:15

Жалеешь 140 рублей?

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

25. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от A.Stahl (ok), 10-Июн-20, 13:52

?

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

26. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Сейд (ok), 10-Июн-20, 13:57

https://www.crowdsupply.com/sifive/hifive1-rev-b

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

31. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от A.Stahl (ok), 10-Июн-20, 14:42

Мне показывает $59.

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

41. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (41), 10-Июн-20, 15:29

https://aliexpress.ru/item/4000818117666.html?algo_pvid=39bb...

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

44. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Ыр2.0 (?), 10-Июн-20, 15:45

Трусы Большой Мужчина Женщина Купить Большой Проститутка Шланг

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

50. "Микроядро seL4 математически верифицировано для архитектуры ..." –3 +/–

Сообщение от ala (?), 10-Июн-20, 16:44

Просто любопытно: вы в самом деле пользуетесь сайтом aliexpress на русском языке?
Серьёзно? Это не шутка? Вот прямо так его и читаете — со всеми их шлангами и многими удовольствиями?

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

52. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от erthink (ok), 10-Июн-20, 16:50

> Просто любопытно: вы в самом деле пользуетесь сайтом aliexpress на русском языке?
> Серьёзно? Это не шутка? Вот прямо так его и читаете — со
> всеми их шлангами и многими удовольствиями?
Нисколько не поклонник, но разве на английском там сильно меньше "удовольствий"?

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

120. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от n80 (?), 11-Июн-20, 00:58

Удивительно, но всё-таки сильно меньше. По крайней мере, у меня такая выборка.

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

132. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (132), 11-Июн-20, 09:48

Английский более информативный.

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

86. "Микроядро seL4 математически верифицировано для архитектуры ..." +3 +/–

Сообщение от Аноним (86), 10-Июн-20, 19:40

А ты пользуешься китайским вариантом или просто думаешь, что для алика родной английский?

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

133. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (132), 11-Июн-20, 09:49

Алиэкспресс ориентируется на английский т.к. международный. Таобао мандаринский т.к. внутренний.

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

142. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (-), 11-Июн-20, 14:33

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

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

119. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от n80 (?), 11-Июн-20, 00:56

Насколько знаю, при заходе с IP-адресов из RU областей aliexpress крайне настойчиво перенаправляет на версию с этим хтоническим ужасом от мира машинного перевода. И отучить его от этого настройками сайта и даже плагинами браузера становится всё труднее и труднее. Это какое-то безумие.

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

131. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (132), 11-Июн-20, 09:47

На английский переключаю, мандаринским ещё не овладел чтобы таобао читать.

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

166. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (166), 12-Июн-20, 00:52

Но русскоязычный Ali показывает цены в национальной валюте. В которой мы и платим.

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

171. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (171), 12-Июн-20, 01:14

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

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

181. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (166), 13-Июн-20, 01:14

Промт-онлайн с ангийской версии Али не сильно лучше переведёт.

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

186. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (-), 13-Июн-20, 10:43

> Промт-онлайн с ангийской версии Али не сильно лучше переведёт.
А мне оно и не надо. Если бы я не умел в инглиш, мой потолок в IT ограничивался бы заменой плашки памяти в древнем компе жэка. Оно мне надо?

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

75. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Michael Shigorin (ok), 10-Июн-20, 18:58

> Get a single HiFive1 Rev B dev kit, featuring the FE310-G002,
> SiFive's second generation open source RISC-V 32-bit SoC.
Кому этот перемикроконтроллер нужен-то?
Их rv64gc за килобакс производительностью не радует, а это...

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

102. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Сейд (ok), 10-Июн-20, 22:43

Производителям домашней автоматизации.

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

126. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (49), 11-Июн-20, 01:32

Домашним автоматизаторам хватит пригоршни ЛА3

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

143. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (-), 11-Июн-20, 14:34

> Домашним автоматизаторам хватит пригоршни ЛА3
Да что там, спичек и желудей.

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

167. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (166), 12-Июн-20, 00:59

ЛА3 потребуется очень большая пригоршня, т.к. триггеры, счётчики, регистры тоже придётся на них делать. Отсюда, к тому же, большое энергопотребление. И самое главное - жёсткая логика, нет гибкости.

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

124. "Микроядро seL4 математически верифицировано для архитектуры ..." +4 +/–

Сообщение от n80 (?), 11-Июн-20, 01:22

Как минимум, тем же, кому и остальные микроконтроллеры.
GigaDevice вообще презанятная контора в плане Особого Пути™.
Впервые я на них наткнулся с их клонами STM32 (GD32Fxxx): pin-to-pin совместимые клоны с без всякого стеснения срисованными даташитами и периферией. И, как минимум, одной маааленькой фишкой: бóльший объём flash-ROM за ту же или даже меньшую цену, достигли они этого за счёт того что вместо полноценной параллельной дорогой флеш-памяти (как у оригинала от ST) использовали отдельный кристалл последовательной флеш-памяти, разварив и залив несколько кристаллов в одном корпусе. А чтобы это не угробило производительность, они добавили между флеш-памятью и ядром дополнительное ОЗУ для кеширования, в итоге в некоторых задач (когда горячая область кода влезает в этот кеш) этот клон работает быстрее оригинала (где либо терпи wait states при чтении/исполнении из флеша, либо ручками копируй горячие функции в основное ОЗУ, либо бери более дорогой камень с кешем из коробки).
Потом они же придумали такой прикол, как серию из почти полных аналогов чипов серии STM32F0 (которые на весьма урезанном Cortex-M0), но с одним важным отличием в виде полноценного ядра Cortex-M3 (как у STM32F1). Это давно напрашивалось, но ST это посчитали не очень-то нужным, а подвальные китайцы взяли и реализовали.
Здесь вот другой их не менее впечатливший выкрутас — придумать серию GD32V, где вся периферия (включая адреса для MMIO) взята от соответствующих STM32Fxxx, но ядро заменено на RISC-V, т.е. в работающем проекте достаточно заменить несколько мест из CMSIS (типа использования инструкции WFI, wait for interrupt) и пересобрать другим компилятором, чтобы получить максимально безболезненный переход с ARM на RISC-V.
Т.е. с одной стороны — бесстыднейшее (и крайне спорное с юридической точки зрения) копирование и паразитирование на чужих идеях и наработках, а с другой — придумали и внедрили нечто мелкое, но очень даже полезное (не для всех, конечно). Пардон за такой оффтоп, но надеюсь что кому-то это тоже окажется интересным ~открытием или дополнят/поправят (раз уж затронули такую интересную мне тему).

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

137. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Леонид (??), 11-Июн-20, 11:17

Спасибо! В отличие от 90% флуда на этом сайте - у вас очень интересное сообщение

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

144. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (144), 11-Июн-20, 14:41

> минимум, одной маааленькой фишкой: бóльший объём flash-ROM за ту же или даже меньшую цену
Еще у них есть ответвления F1xx-like которых в оригинале нет - например мелкие QFN с USB и общим видом железа как у F1xx. У STMicro именно такого комбо почему-то и нет, при всем разнообразии. Неужто никто usb не хотел в мелком корпусе c F1xx? Да ну ладно?!
> кристалл последовательной флеш-памяти, разварив и залив несколько кристаллов в одном корпусе.
А вы их щупали? Флеху шить программно пробовали? Оно по flash controller не совместимо? А то даташит вроде как клон STM-ов 1 в 1.
> Здесь вот другой их не менее впечатливший выкрутас — придумать серию GD32V,
> где вся периферия (включая адреса для MMIO) взята от соответствующих STM32Fxxx,
> но ядро заменено на RISC-V,
Вот это они очень стебно прикололись. Надо будет как-нибудь повертеть в руках этот неведомый пепелац.
> Т.е. с одной стороны — бесстыднейшее (и крайне спорное с юридической точки
> зрения) копирование и паразитирование на чужих идеях и наработках
STMicro им как бы железки не давал - сами совместимые разработали. Почему так нельзя - науке неизвестно. Вроде бы API не есть копирайченая штука, оракла vs гугл на этой теме помнится завернули.
> кому-то это тоже окажется интересным ~открытием или дополнят/поправят (раз уж затронули
> такую интересную мне тему).
У узкоглазых есть и еще клоны STM32 от других фирм, разной степени кривизны. Вон там рядом какой-то чудак мыкается, у него оно в бутлоадер не входит чего-то.

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

194. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от n80 (?), 14-Июн-20, 02:23

> Еще у них есть ответвления F1xx-like которых в оригинале нет - например
> мелкие QFN с USB и общим видом железа как у F1xx.
> У STMicro именно такого комбо почему-то и нет, при всем разнообразии.
> Неужто никто usb не хотел в мелком корпусе c F1xx? Да ну ладно?!
Собственно, я об этой ситуации и говорил в «это давно напрашивалось, но ST это посчитали не очень-то нужным, а китайцы взяли и реализовали».

>> кристалл последовательной флеш-памяти, разварив и залив несколько кристаллов в одном корпусе.
> А вы их щупали? Флеху шить программно пробовали? Оно по flash controller
> не совместимо? А то даташит вроде как клон STM-ов 1 в 1.
А чего бы ему быть несовместимым? Поскольку общение с флеш-памятью что в оригинале, что тут идёт не напрямую, а через внутренний контроллер, этот самый контроллер прекрасно абстрагирует все подробности. В общем-то, наличие команд для стирание страницами и записи словами не зависит от типа флеш-памяти, это везде есть.
>> Т.е. с одной стороны — бесстыднейшее (и крайне спорное с юридической точки
>> зрения) копирование и паразитирование на чужих идеях и наработках
> STMicro им как бы железки не давал - сами совместимые разработали. Почему
> так нельзя - науке неизвестно. Вроде бы API не есть копирайченая
> штука, оракла vs гугл на этой теме помнится завернули.
Насколько я помню, тот же оракл на эту тему ещё долго будет пытаться что-нибудь у кого-нибудь отжать. Тут тоже момент тонкий: во-первых, не очень ясно, насколько сами и с нуля (или, как часто бывает, по знакомству что-то добыли с соседнего завода; если сам ST посчитает их угрозой, наверняка постарается накопать информацию о подобных эпизодах), во-вторых, могут докопаться до похожей маркировки (типа, почти до неразличимости, с торговыми марками и товарными знаками это стандартная практика; не могу сказать точно, насколько это применимо тут), рисунков и фраз из документации, может, какие-то решения по периферии вообще запатентованы. Но, вполне может быть (всё-таки я не юрист), что тут и правда ситуация «а что, так можно было?», т.е. просто кто-то первым понял что ничего не мешает сделать так, а остальные сами себя ограничивали, опасаясь проблем или не считая этот путь перспективным.
> У узкоглазых есть и еще клоны STM32 от других фирм, разной степени кривизны.
> Вон там рядом какой-то чудак мыкается, у него оно в бутлоадер не входит чего-то.
А можно подробнее и конкретнее? Интересно, что там ещё бывает из широко доступного.
Для меня большим открытием ещё в своё время стали WCH с их переходниками со всего подряд на всё подряд и самыми дешёвыми МК с аппаратным USB (CH55x), а также Padauk (PDK) с их сверхдешёвыми МК с однократно программируемой памятью (при этом есть ещё и варианты с тем же ядром и нормальной флеш-памятью, но там уже и цена повыше, так что это для отладки больше).

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

198. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (198), 15-Июн-20, 06:15

> Собственно, я об этой ситуации и говорил в «это давно напрашивалось, но
> ST это посчитали не очень-то нужным, а китайцы взяли и реализовали».
Я честно говоря не понял почему в мелком корпусе, с usb и вообще F103-like обвесом - "не очень нужное". Китайцы вот тоже. Минимум сравнимого что я знаю это F103 в qfn36, но у китайцев и мельче есть, qfn28 чтоли, выводок F150. Что-то ST с маркетингом перемудрил местами, имхо.
> А чего бы ему быть несовместимым? Поскольку общение с флеш-памятью что в
> оригинале, что тут идёт не напрямую, а через внутренний контроллер, этот
> самый контроллер прекрасно абстрагирует все подробности.
Ну вот в этом и вопрос был - смогли ли они вывесить аналогичный интерфейс железки. И это вопрос к тому кто реально пробовал этой железкой покомандовать, соответственно :)
> В общем-то, наличие команд для стирание страницами и записи словами не зависит
> от типа флеш-памяти, это везде есть.
Просто для SPI это технически дольше и сложнее. Но если железка-посредник оттранслирует интерфейс - почему бы и нет. Я кажется начинаю понимать как это: mem-mapped SPI подпертый кэшом каким-то, так? Узкоглазые вообще любят mmaped spi почему-то в своих чипах.
> Насколько я помню, тот же оракл на эту тему ещё долго будет
> пытаться что-нибудь у кого-нибудь отжать.
Пытаться то он может что угодно, но если получится, следующим шагом кто-нибудь запатентует алфавит и мы все дружно залетим за использование этого апи.
> по знакомству что-то добыли с соседнего завода; если сам ST посчитает
> их угрозой, наверняка постарается накопать информацию о подобных эпизодах),
1) Вероятно могут и сами что-то разработать.
2) ST тоже не все железки сами разработали, часть у других налицензировали.
3) ST постепенно поразвел зоопарк "HW IP versions" грубо говоря. Да, железо улучшили, но совместимость профакали и дескать используйте наши мегалибы и халы на каких-то мутных лицензиях - "только с чипами stmicro".
> А можно подробнее и конкретнее? Интересно, что там ещё бывает из широко доступного.
https://www.opennet.me/openforum/vsluhforumID3/120751.html#153 - где-то вокруг этого. Понятия не имею кто такой CS32, бывают и другие (на остальных фото маркировка нечитаема).
> Для меня большим открытием ещё в своё время стали WCH с их
> переходниками со всего подряд на всё подряд
Ну мне это уже не особо надо - у меня есть и просто FTDI'ки, а что-то сверх того я и сам фирмвару для мк накорябаю.
> и самыми дешёвыми МК с аппаратным USB (CH55x), а также Padauk (PDK) с их сверхдешёвыми
> МК с однократно программируемой памятью
Я миллионными тиражами не ворочаю, в иные ниши пристраиваюсь. F1xx мне пришлись по вкусу тем что дешевле какихнить атмег, при том что периферия и ядро сильно круче, а сложность системы... ну, "я в это более-менее врубился" - общий view чипа и чего я с ним делаю и зачем все же сформировался. А вот китайские глюки мне все же ни к чему в вещах для которых мне МК интересны :).
И цена около 1-2 баксов за чип меня не напрягает. А, еще и gcc'ом поддерживается, вплоть до возможности юзануть тулчейн из репов моего линуксного дистра. И stm32flash оттуда же, все-таки удобно.

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

12. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Сейд (ok), 10-Июн-20, 13:04

https://www.sifive.com/boards/hifive1-rev-b

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

53. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (53), 10-Июн-20, 16:57

А risc-v сможет достичь сопоставимой производительности?

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

54. "Микроядро seL4 математически верифицировано для архитектуры ..." +6 +/–

Сообщение от erthink (ok), 10-Июн-20, 17:17

> А risc-v сможет достичь сопоставимой производительности?
RISC-V - это просто открытая система команд. Соответственно, интель может прикрутить декодер RISC-V (RV64IMAFDC) к своим утюгам, и тогда будет RISV-V с сопоставимой производительностью.
P.S. На месте интеля я бы заслал такую фичу инженерам 1-2 года назад (как только спекулятивное исполнение накрылось тазом), и даже наверное начал бы вкладываться в разработку неготовых спецификаций (всё что "Open" в https://en.wikipedia.org/wiki/RISC-V#ISA_base_and_extensions).

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

145. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (144), 11-Июн-20, 14:43

> RISC-V - это просто открытая система команд. Соответственно, интель может прикрутить декодер
> RISC-V (RV64IMAFDC) к своим утюгам, и тогда будет RISV-V с сопоставимой производительностью.
Кроме этого есть еще и открытые реализации ядер. Это, конечно, не интел - но вообще нормальные 64-битные штуки, для небольших железок с линухом явно хватит.

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

70. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от NameName (?), 10-Июн-20, 18:34

Risc-v это просто спецификация на набор команд. Вот если вы сделаете хороший быстрый кристалл, то тогда будем вам и сопоставимая производительность. Но, опять же, хорошего кристалла недостаточно -- нужен хороший компилятор. Т.е. такой компилятор, который способен адекватно учесть особенности спецификации и её реализации.

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

162. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (162), 12-Июн-20, 00:45

Все как в лучших домах - есть GCC и Clang. И линухом это процессорное ядро поддерживается. И даже некоторые реально существующие SoC.

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

118. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (118), 11-Июн-20, 00:30

А потом откопать обратно.

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

3. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (3), 10-Июн-20, 12:40

Вот, просто хороший DLS и никакой псевдонаучной претенциозности как у Rust.

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

5. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (3), 10-Июн-20, 12:41

DSL

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

6. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (41), 10-Июн-20, 12:45

Что такое DLS? Может DSL (Domain Specific Language)?

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

72. "Микроядро seL4 математически верифицировано для архитектуры ..." +17 +/–

Сообщение от Аноним (72), 10-Июн-20, 18:39

да хватит играть уже с аббревиатурой LSD

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

9. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (9), 10-Июн-20, 13:01

Вообще-то оно на сишечке с асмом.

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

14. "Микроядро seL4 математически верифицировано для архитектуры ..." +3 +/–

Сообщение от Аноним (14), 10-Июн-20, 13:05

Ядро на сишечке. Пруф -- нет. Причём пруф раз в 40 больше самого ядра.

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

146. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (144), 11-Июн-20, 14:44

> Причём пруф раз в 40 больше самого ядра.
А вы чего хотели? Скажите спасибо что он вообще за разумное время обсчитывается.

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

161. "Микроядро seL4 математически верифицировано для архитектуры ..." –2 +/–

Сообщение от Аноним (161), 11-Июн-20, 21:47

> Скажите спасибо что он вообще за разумное время обсчитывается.
Касперский "при необходимости" посчитает за разумное время любую NP-полную задачу.

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

163. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (162), 12-Июн-20, 00:46

> Касперский "при необходимости" посчитает за разумное время любую NP-полную задачу.
Он сам как NP-полная задача.

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

13. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (14), 10-Июн-20, 13:04

Всего-то пришлось свой компилятор C написать, и потом ещё 200к строк на Isabelle, Haskell и прочих.

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

30. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (-), 10-Июн-20, 14:34

В том то и элегантность решения, что компилятор C в 100500 раз проще Раста.

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

33. "Микроядро seL4 математически верифицировано для архитектуры ..." +10 +/–

Сообщение от Аноним (33), 10-Июн-20, 14:52

Проще и безопаснее, так как в С нету unsafe

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

34. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (33), 10-Июн-20, 14:54

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

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

66. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (14), 10-Июн-20, 18:17

Внезапный поворот: компилятор, которым собирается seL4, написан ни разу не на C!

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

164. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (162), 12-Июн-20, 00:47

> Внезапный поворот: компилятор, которым собирается seL4, написан ни разу не на C!
Это как-то мешает собрать его компилятором си написаным на си? :)

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

17. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (17), 10-Июн-20, 13:16

Слабое приплетание, на троечку.

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

4. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от DmA (??), 10-Июн-20, 12:40

Давно в области безопасности не было таких хороших вестей

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

8. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (-), 10-Июн-20, 12:59

может gnu/hurd кто-нибудь перенесёт на seL4

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

10. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (9), 10-Июн-20, 13:02

Ноу проблем. Сколько поатишь?

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

11. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (11), 10-Июн-20, 13:02

Флаг в руки, ждём от тебя результатов.

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

18. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (17), 10-Июн-20, 13:18

Люди, способные это сделать, не станут заниматься этим "за идею".

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

19. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Сейд (ok), 10-Июн-20, 13:19

Было много попыток перевести Hurd с Mach на L4, к сожалению, все потерпели неудачу.

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

22. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от AnonAnonAnon (?), 10-Июн-20, 13:32

смысл не в том, чтобы заменить gnu mach на seL4, а в том, чтобы gnu/hurd работал поверх seL4;
иначе говоря, seL4 работает в режиме ядра, а gnu/hurd(gnu mach + translators) в режиме пользователя.

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

28. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (28), 10-Июн-20, 14:12

Гурд жестко приколочен к 32 битам. Его теперь проще переписать. Это в вопросу о программистских талантах Столлмана.

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

35. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (41), 10-Июн-20, 15:14

На seL4 есть рабочая Genode https://genode.org/ .

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

128. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от bw (ok), 11-Июн-20, 06:14

Genode под Nova пишется, все остальные ядра для галочки.

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

15. "Микроядро seL4 математически верифицировано для архитектуры ..." –3 +/–

Сообщение от Аноним (-), 10-Июн-20, 13:07

что-то не очень заметно, что на платах Arduino используется RISC-V

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

23. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Сейд (ok), 10-Июн-20, 13:36

https://www.sifive.com/boards/hifive1-rev-b
https://shop365481095.world.taobao.com/

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

42. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (42), 10-Июн-20, 15:36

https://aliexpress.ru/item/4000299112762.html

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

90. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (9), 10-Июн-20, 20:14

Они анонсировали Arduino Cinque и… всё.
Что, впрочем, нисколько не мешает купить другую похожую на Arduino платку с RISC-V.

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

182. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (182), 13-Июн-20, 08:39

Скоро ESP RISC-V подъедет

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

21. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (21), 10-Июн-20, 13:31

Вот это по настоящему важная новость. Ещё бы понять, как наладить производство устройств на нём.

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

24. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Сейд (ok), 10-Июн-20, 13:47

Берёшь L4 и https://pulp-platform.org// и налаживаешь производство.

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

27. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (28), 10-Июн-20, 14:10

Эпл уже решило переходить на RISC-V вместо ARM?

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

37. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (41), 10-Июн-20, 15:19

А что, они как-то обсуждали эту возможность?

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

57. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (28), 10-Июн-20, 17:36

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

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

165. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (162), 12-Июн-20, 00:50

> Эпл уже решило переходить на RISC-V вместо ARM?
Да и черт с ним с эплом. Зато решили WD, Nvidia и много кто еще. При том первая фирма процессоры делает со времен царя гороха.

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

29. "Микроядро seL4 математически верифицировано для архитектуры ..." +3 +/–

Сообщение от Аноним (29), 10-Июн-20, 14:15

Интересный исследовательский проект, но преподнесен ради хайпа вокруг RISC-V, который порядком надоел постоянной игрой слов и введением в заблуждение. RISC-V - это лишь открытый набор команд процессора, т.к. открытая спецификация. Сделано это во многом для экспериментов с процессорными архитектурами в университетской среде с целью иметь возможность переиспользовать единый компилятор и набор портированного ПО, не отвлекаясь на всё это от дизайна аппаратура.
Автор этой идеи решил коммерциализировать эту идею, так появилась SiFive, являющаяся классической HW IP + design services компанией, такой же как Arm. Их ядра ни разу не открытые и не бесплатные, но да, используют ту самую tools / SW экосистему. По сути, ребятки придумали модель, как за счет open source community решить одну из задач классического HW IP стартапа и быстро оказаться наравне с Arm по размерам экосистемы. Отлично, решили, вот только бизнес всё не взлетает, компания продолжает привлекать внешние инвестиции в развитие и всё больше уходит в design services. Открытость набора команд на качество процессорного ядра, реализующего этот набор, не влияет.
Другие коммерческие RISC-V вендоры почему-то образуются в РФ и Южной Америке. Наверно, потому что пытаются сыграть на волне импортозамещения. Что опять же к реальной технической конкуренции отношения не имеет и к open source процессорному ядру не приближает.
Вообще, идея открытой реализация ядра вызывает один большой вопрос “зачем?”. Ну вот есть оно и что?
Выпустить чип требует далеко не только процессорного ядра, но и других блоков (интерфейсы, памяти и т.п.). Выпустить production ready чип потребует еще и серьезным усилий по дизайну и верификации. Ну и само производство не дешевое удовольствие. Даже есть кто-то выпустил такой чип, в момент изготовления он становится куском кремния, патч на него больше не наложишь.
Еще есть очень крупные продуктовые компании (WD), которые способны сделать свою архитектуру и поддерживать её. Вот они экономят на группе разработки компилятора и отчислениях Arm-у, но почему-то используют эти решения в закрытых системах.
Можно залить в ПЛИС. И это хорошее решение, если заниматься исследованиями процессорных архитектур, но сомнительное, если нужен просто процессор.  Xilinx уже предоставляет бесплатное ядро в качестве микроконтроллера, а многие большие FPGA уже содержат Arm A процессор, если нужен мощный embedded CPU.

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

40. "Микроядро seL4 математически верифицировано для архитектуры ..." –3 +/–

Сообщение от Аноним (40), 10-Июн-20, 15:27

WD это хорошо (он заменил mips на arm и riscv), но ты забыл про NVIDIA, лет 10 применяющую risc-v  в своих видимокартах. Сейчас уже пару лет как есть "десктопы" на risc-v. Особо от x86 не отличаются, но асссемблерных оптимизаций в программах не завезли и поэтому немножко сливает в плане производительности. Цена на порядки адекватней эльбрусов, несмотря на то что в долларах.

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

43. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (41), 10-Июн-20, 15:36

Чего лет 10 назад? 10 лет назад архитектура только начала зарождаться.
Можно ссылочку на такой десктоп?

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

47. "Микроядро seL4 математически верифицировано для архитектуры ..." –2 +/–

Сообщение от Аноним (40), 10-Июн-20, 16:11

Да, внезапно, nvidia стоит у истоков и первая радостно побежала экономить. Насчёт дектопа… Ммм я перепутал с power9, извините.

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

77. "Микроядро seL4 математически верифицировано для архитектуры ..." +3 +/–

Сообщение от Michael Shigorin (ok), 10-Июн-20, 19:07

Вы вообще всё здесь перепутали -- примерно так:
>>> Сейчас уже пару лет как есть "десктопы" на risc-v.
Нет.
>>> Особо от x86 не отличаются
Нет!
>>> но асссемблерных оптимизаций в программах не завезли
>>> и поэтому немножко сливает в плане производительности.
Нет.
>>> Цена на порядки адекватней эльбрусов, несмотря на то что в долларах.
Нет!
PS: в отличие от Вас -- практик в обсуждаемом вопросе.

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

80. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (40), 10-Июн-20, 19:22

Спасибо, я уже признал ошибку. Это было про power9.

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

97. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Михрютка (ok), 10-Июн-20, 22:05

risc-v десктоп на power 9
https://ibb.co/6gdgGHH

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

112. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (40), 10-Июн-20, 23:46

Он risc, это определённо. И он десктоп.

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

46. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от erthink (ok), 10-Июн-20, 16:00

> Интересный исследовательский проект, но преподнесен ради хайпа вокруг RISC-V, который
> порядком надоел постоянной игрой слов и введением в заблуждение. RISC-V -
> это лишь открытый набор команд процессора, т.к. открытая спецификация.
> [...]
>
Очень хорошо сформулировано

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

76. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Michael Shigorin (ok), 10-Июн-20, 19:05

> Другие коммерческие RISC-V вендоры почему-то образуются в РФ и Южной
> Америке. Наверно, потому что пытаются сыграть на волне импортозамещения.
Причём когда минимум из-за одного такого российского безфабричника восторчали уши IBM, у меня лично наметились сомнения, что тут вообще речь про импортозамещение, а не прокорм стратегической лавки кинетического противника в условиях повышенной шагреневости рынков...
Собственно, кто знает всех этих сосновцевых с массухами -- тот и так понимает.

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

138. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Леонид (??), 11-Июн-20, 11:23

А про кого это вы? Вроде какая-то питерская контора занималась RISK-V

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

32. "Микроядро seL4 математически верифицировано для архитектуры ..." +4 +/–

Сообщение от erthink (ok), 10-Июн-20, 14:50

В своё время L4 было прорывом, но поезд несколько продвинулся за >25 лет.
Сейчас же уже есть Kaspersky OS, которая принципиально лучше L4 (конечно IMHO, ибо TL;DR):
- тот-же уровень верифицируемости (посредством мат. доказательства) при необходимости.
- различные модели безопасности.
- поддержка POSIX.
- возможность "security by design" для приложений (как сложных наборов компонентов/служб).
- также поддержка жесткого реального времени (пока не из каробки, но обещают).
Репутация же L4 оказалась "подмочена" дырявостью продуктов Qualcomm.

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

36. "Микроядро seL4 математически верифицировано для архитектуры ..." +3 +/–

Сообщение от Аноним (41), 10-Июн-20, 15:18

Репутацию Kaspersky OS ещё никто не проверял. Да и исходников её не покажут.

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

45. "Микроядро seL4 математически верифицировано для архитектуры ..." +3 +/–

Сообщение от erthink (ok), 10-Июн-20, 15:51

Кому нужно уже показали, поэтому и пишу.
"Проверка" там в основном делается "математикой", поэтому (в сравнении с Linux и тем более вендой) можно узбаготься.
Минусы, которые я пока вижу примерно такие:
- У Евгения (кажется) еще осталась надежда, что их когда-нибудь/может-быть пустят обратно на рынок США и сателлитов. Поэтому продукт подается (IMHO) слишком "глобалистически".
- В разработку вложено очень много (>15 лет), соответственно Евгений не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.

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

65. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от vitalif (ok), 10-Июн-20, 18:16

> не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
R.I.P
о какой вообще проверке может идти речь при отсутствии открытых исходников?

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

68. "Микроядро seL4 математически верифицировано для архитектуры ..." +4 +/–

Сообщение от erthink (ok), 10-Июн-20, 18:24

> > не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
> о какой вообще проверке может идти речь при отсутствии открытых исходников?
Открыть исходники для проверки - это одно (у M$ в таком режиме они открыты >25 лет).
А перейти на открытую лицензию и модель open source - это совсем другое.
Но палка тут о двух концах - если модель (и DSL её описания) окажутся удачными (а похоже так и есть), то повторить уже проверенную концепцию относительно просто поверх любого подходящего ядра (даже натянуть на Linux, хотя будет масса проблем).
Т.е. если Kasperky OS "взлетит" и при этом останется closed-source, то китайцы (или еще кто-то) повторят разработку за ~1-2 года.

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

136. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (118), 11-Июн-20, 10:56

>даже натянуть на Linux
Там даже систему виртуальной памяти пофиксить не могут, слишком сложный продукт стал, о какой верификации речь может идти? В лучшем случае миникс верифицируют.

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

140. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от erthink (ok), 11-Июн-20, 14:03

>>даже натянуть на Linux
>Там даже систему виртуальной памяти пофиксить не могут, слишком сложный продукт стал, о какой верификации речь может идти? В лучшем случае миникс верифицируют.
Хм, а где в слове "натянуть" есть упоминание верификации ?

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

153. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от vitalif (ok), 11-Июн-20, 15:48

> Открыть исходники для проверки
Там хотя бы повторяемость сборки есть? Открыты они.
А если по обновлениям приедет бэкдор например? Какой смысл в открытии "на посмотреть"?
Кода в ОС столько, что найти там все небезопасные вещи очень трудно, даже когда на одни исходники смотришь всем миром. А когда смотрит какая-то одна рабочая группа ограниченное время - это вообще ни о чём...
Не суйтесь вообще с закрытой ОС на рынок. Просто не лезьте. Закрытая ОС - это зло.

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

154. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от erthink (ok), 11-Июн-20, 16:09

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

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

155. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от vitalif (ok), 11-Июн-20, 16:28

Никого не волнует твоя компетентность. Удел закрытой ОС - два с половиной закрытых роутера.
Щас нам Касперский будет про безопасность рассказывать. С бэкдорами прямо от ФСБ, ага.

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

156. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от erthink (ok), 11-Июн-20, 16:36

> Никого не волнует твоя компетентность. Удел закрытой ОС - два с половиной
> закрытых роутера.
> Щас нам Касперский будет про безопасность рассказывать. С бэкдорами прямо от ФСБ,
> ага.
Никому не интересно ваше "ихпёртное" мнение (не читал, но осуждаю) без базовой осведомленности об обсуждаемом предмете.
Всегда кто-то "лает" и хейтит, а караван идёт (и с Эльбрусами, и с Альтом и т.д. и т.п. также).
Адью, мосье́.

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

160. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от vitalif (ok), 11-Июн-20, 20:08

Да пусть идет, мне вообще пофиг

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

172. "Микроядро seL4 математически верифицировано для архитектуры ..." –2 +/–

Сообщение от Аноним (171), 12-Июн-20, 01:16

> Никому не интересно ваше "ихпёртное" мнение (не читал, но осуждаю) без базовой
> осведомленности об обсуждаемом предмете.
Ихпертное мнение о структуре управления каспера можно на хабре почитать. Дальше каждый для себя сделает выводы сам.

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

176. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (176), 12-Июн-20, 09:53

Ничего себе, вы экспертное сообщество привели!!!
С таким же успехом можно и лукоморье упоминать.

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

187. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (187), 13-Июн-20, 10:46

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

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

195. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Онаним (?), 14-Июн-20, 21:46

Хз на счёт управления, не сведущ в вопросе, но видится мне, США не зря и не просто так это счастье выперли.

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

104. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Михрютка (ok), 10-Июн-20, 22:54

>>>Кому нужно уже показали
мне это всегда нравилось. "у нас есть такие приборы но мы вам их не покажем".
>>>- В разработку вложено очень много (>15 лет)
извиняюсь, os/360 меньше времени строили.
она за эти 15 лет реальное практическое применение хоть где-то нашла? или только "где надо, там и нашла"?
если нет, то это n-ый вариант hurd.

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

106. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от erthink (ok), 10-Июн-20, 23:11

> > В разработку вложено очень много (>15 лет)
> извиняюсь, os/360 меньше времени строили.
Считаем что стоили и выбросили, или что z/OS всё еще строят (~60 лет)?
Тем не менее, в любом случае - Ну и что?
> > Кому нужно уже показали
> мне это всегда нравилось. "у нас есть такие приборы но мы вам
> их не покажем".
>
> она за эти 15 лет реальное практическое применение хоть где-то нашла? или
> только "где надо, там и нашла"?
> если нет, то это n-ый вариант hurd.
Рассуждая не зная предмета, вы просто рекламируете свою некомпетентность.

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

109. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Михрютка (ok), 10-Июн-20, 23:23

z/os в продуктиве работает все эти годы.
kasperskyos в продуктиве где-то работает?
лет пять назад в россии рекламировали kasperskyos на крафтвеях. только что зашел на их сайт посмотреть, что как - сетевое "доверенное оборудование" с красивыми сертификатами почему-то на линуксе. как так?
>>>Рассуждая не зная предмета, вы просто рекламируете свою некомпетентность.
кто мешает вам рассудить со знанием? ну правда, вот я спросил, и еще повторюсь, мне не жалко:
kasperskyos в продуктиве где-то работает?
вы уж просветите нас, темных, если не сложно. я волшебное слово знаю: "Пожалуйста!"

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

113. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от erthink (ok), 10-Июн-20, 23:57

> kasperskyos в продуктиве где-то работает?
Ну RTFM ведь.
https://os.kaspersky.ru/projects/
> вы уж просветите нас, темных, если не сложно. я волшебное слово знаю:
> "Пожалуйста!"
На здоровье!

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

147. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (144), 11-Июн-20, 14:49

>  - В разработку вложено очень много (>15 лет), соответственно Евгений не
> решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
Это по счастью будут в основном его проблемы, да нескольких "везунчиков" которым это добровольно-принудительно втулили. А то что мелкий проприетарщик да еще с орками в управлении переиграет весь остальной мир - так не бывает.

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

152. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от erthink (ok), 11-Июн-20, 15:24

>>  - В разработку вложено очень много (>15 лет), соответственно Евгений не
>> решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
> Это по счастью будут в основном его проблемы, да нескольких "везунчиков" которым
> это добровольно-принудительно втулили.
Демагогия и FUD.
> А то что мелкий проприетарщик да еще с
> орками в управлении переиграет весь остальной мир - так не бывает.
1. "мелкий", "орки" - А я верно предполагаю что в вашей системе координат Макс является представителем "крупных эльфов" и реикарнацией Тони Старка ;)
2. "так не бывает" - ага, ни разу не было и вот опять ;)

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

168. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (168), 12-Июн-20, 01:01

> Демагогия и FUD.
Оценка наиболее вероятного развития событий. Такое счастье можно поюзать только если орк машет саблей и грозит отрезать голову.
> 1. "мелкий", "орки" - А я верно предполагаю что в вашей системе координат
Орки сами себя так назвали. Подробности этой истории можно найти на хабре...

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

191. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от НамеНаме (?), 13-Июн-20, 17:58

Что значит -- "переиграет весь мир"? "Весь мир" и так себя самого переигрывает. Безо всякой помощи. ИТ -- такой, какой он сейчас -- должен умереть.

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

199. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (-), 15-Июн-20, 06:30

> Что значит -- "переиграет весь мир"?
Это реверанс в адрес "если Kasperky OS "взлетит"". Блин, скорее пингвины научатся летать. Стоп, "given enough rocket power penguins can fly" (c) :D

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

157. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Oxyd76 (?), 11-Июн-20, 17:31

> Кому нужно уже показали, поэтому и пишу.
«Танк шибко секретный! Учёные могут и не знать!» ©

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

169. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (166), 12-Июн-20, 01:06

>Кому нужно уже показали, поэтому и пишу.
От того, что показали майору, нам не легче.

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

38. "Микроядро seL4 математически верифицировано для архитектуры ..." –2 +/–

Сообщение от vitalif (ok), 10-Июн-20, 15:22

> при необходимости
ОЙ КАК ТОЛСТО...

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

62. "Микроядро seL4 математически верифицировано для архитектуры ..." +4 +/–

Сообщение от erthink (ok), 10-Июн-20, 17:48

> > при необходимости
> ОЙ КАК ТОЛСТО...
Видимо стоит уточнить для местных ихпёртов, которые (УВЫ) не читали, но осуждают.
Логика ядра верифицирована, но в реальных применениях это мало что даёт (смотрим на факапы Qualcomm и т.п.):
- без верификации всех "ассемблерных вставок" при использовании на конкретной платформе.
- без верификации логики служб и приложений (с учетом взаимодействия и средств контроля ОС).
Соответственно, "при необходимости" - относилось к верификации примитивов (связанных с "посадкой" ОС на какую-то конкретную платформу) и к верификации приложений.
TL;DR
Kaspersky OS предлагает контроль взаимодействия отдельных компонентов (служб, приложений) как с ядром, так и между собой - это принципиальное отличие от L4.
Грубо говоря, принципы безопасности/надежности L4 распространяются с ядра на все приложения, службы и систему в целом.

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

67. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от vitalif (ok), 10-Июн-20, 18:19

Я всерьёз не могу это воспринимать даже. Закрытое чудо, которое никто не видел, а если даже откроют - то исходники не откроют. Но оно мегабезопасное. "Не имеющее аналогов в мире". Да ну нафиг.
Примерно на уровне QP ОС.
L4 лучше хотя бы тем, что она реальна, а не иллюзорна.

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

69. "Микроядро seL4 математически верифицировано для архитектуры ..." +4 +/–

Сообщение от erthink (ok), 10-Июн-20, 18:32

> Я всерьёз не могу это воспринимать даже. Закрытое чудо, которое никто не
> видел, а если даже откроют - то исходники не откроют. Но
> оно мегабезопасное. "Не имеющее аналогов в мире". Да ну нафиг.
Т.е. если вы не трогали луну руками, то её нет?
Тем не менее, эту "луну" можно потрогать https://os.kaspersky.ru/development/
(если руки растут из нужного места).

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

98. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (98), 10-Июн-20, 22:23

Там есть исходный код ядра и его можно собрать и запустить со своими правками?

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

99. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от erthink (ok), 10-Июн-20, 22:33

> Там есть исходный код ядра и его можно собрать и запустить со
> своими правками?
Нет.
Но за подробностями лучше RTFM.

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

135. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (161), 11-Июн-20, 10:55

> Т.е. если вы не трогали луну руками, то её нет?
Разве это не принципиальный вопрос верификации?
> Тем не менее, эту "луну" можно потрогать https://os.kaspersky.ru/development/
И что там дают? Уже собранную игрушку для написания хелловорлдов? Плюс "прямое согласие на сбор и обработку моих данных"

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

200. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (-), 15-Июн-20, 06:31

Как там грится? Джентльменамм верят на слово! И тут мне карта как поперла, как поперла!

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

39. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (39), 10-Июн-20, 15:26

Как будто репутация у вирусописателей Касперского чем-то сильно лучше Qualcomm.

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

56. "Микроядро seL4 математически верифицировано для архитектуры ..." –3 +/–

Сообщение от NameName (?), 10-Июн-20, 17:24

Касперский и репутация? Хотя, может в каких-то там своих кругах.

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

71. "Микроядро seL4 математически верифицировано для архитектуры ..." –5 +/–

Сообщение от NameName (?), 10-Июн-20, 18:35

Дефачка из PR-отдела отчаянно минусует, размазывая тушь соплями.

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

73. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от erthink (ok), 10-Июн-20, 18:40

> Дефачка из PR-отдела отчаянно минусует, размазывая тушь соплями.
Ну не у каждой "дефачке" хватит соплей на вашу чушь ;)

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

159. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от НамеНаме (?), 11-Июн-20, 18:22

Ты смотри, а девачкам понравилось. Плюсуют. Бедненькие труженицы "IT-сектора".

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

48. "Микроядро seL4 математически верифицировано для архитектуры ..." –2 +/–

Сообщение от Аноним (48), 10-Июн-20, 16:32

Всё что я понял, что есть некая шайтан архитектура - RISC, есть её спецификации, есть "разработчики" этих спецификаций и даже есть микропроцессоры. Все открытые процессоры это RISC, не RISC я не нашел.
разработчик    спецификация архитектуры        Реализации архитектуры
MIPS Technologies, Inc.    MIPS
OpenPOWER    POWER
университет Беркли    RISC-V
OpenCores    RISC         OpenRISC
OpenSPARC
Sun Microsystem    SPARC        UltraSPARC T1, UltraSPARC T2
Texas Instruments    SPARCv8        LEON2
Fujitsu    SPARCv9        SPARC64
Simply RISC    SPARC V9        S1 Core

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

55. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (49), 10-Июн-20, 17:23

Ну... Спарку можно сразу выкинуть.

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

60. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (48), 10-Июн-20, 17:47

Почему?

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

58. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (28), 10-Июн-20, 17:39

Теперь есть 15 конкурирующих стандартов.

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

61. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (48), 10-Июн-20, 17:47

Что в этом плохого?

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

74. "Микроядро seL4 математически верифицировано для архитектуры ..." –3 +/–

Сообщение от Аноним (49), 10-Июн-20, 18:46

А ты подумай... Интел закрыт, как чёрт, жрёт, как слон, и ему абсолютно пох на каких-то 15 открытых "конкурентов" с суперпуперэкономным ядром.

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

81. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (48), 10-Июн-20, 19:27

Если бы не было 15 шт, было бы лучше, хуже? Появится ещё 100500, пускай, если взлетит одна и хорошо.

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

179. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (176), 12-Июн-20, 10:03

Нет, НЕ хорошо. Это - всего лишь показатель того, что отрасль так до сих пор и находится в состоянии "не знаю, кто там, в яме, но сыр - точно очень любит". И речь здесь - совершенно - не о многовариантности получения одного и того же результата. Да! И, желательно, Тьюринга, лишний раз не поминать...

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

170. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (168), 12-Июн-20, 01:07

> абсолютно пох на каких-то 15 открытых "конкурентов" с суперпуперэкономным ядром.
Ща им эппл подкатит годный сюрпризец кажись.

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

180. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (176), 12-Июн-20, 10:05

УжЕ - нет. И - никто, в ближайшие лет 30 - не подкатит. Не до того будет.

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

59. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (40), 10-Июн-20, 17:47

SuperH тоже risc. И amd64 тоже risc, но это тщательно пытаются маскировать. RISC-V эта такая современная альтернатива мипсу (который тоже открыли и закопали, а ведь хорошая альтернатива арму была). В первую очередь стоит вопрос энергоэффективности и возможности свободно дизайнить кастомные чипы без космических откатов. В чём смысл сабжа я затрудняюсь ответить.

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

63. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (48), 10-Июн-20, 17:53

Какая из реализаций лучше всего подойдет для ПК, ноутов, планшетов, телефонов?

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

64. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от erthink (ok), 10-Июн-20, 17:56

> Какая из реализаций лучше всего подойдет для ПК, ноутов, планшетов, телефонов?
Давно известно - волшебная.

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

82. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (48), 10-Июн-20, 19:28

>Давно известно - волшебная.
Подозреваю что ирония сарказм.

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

78. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Michael Shigorin (ok), 10-Июн-20, 19:10

> amd64 тоже risc
Нет.  А то, что там RISC -- не называется AMD64.

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

79. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (40), 10-Июн-20, 19:20

Скорее всего там технология аналогичная тому, что разрабатывала transmeta. Дитя ежа с ужом и эмуляция класических интерфейсов для взаимодействия.

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

83. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (83), 10-Июн-20, 19:29

> И amd64 тоже risc, но это тщательно пытаются маскировать.
Никто ничего не маскирует. CISC это микрокод выполняющийся поверх RISC ядра. Всегда, даже в 8080.
Ваш Кэп.

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

85. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (40), 10-Июн-20, 19:40

Возможно и так. Когда-то я интересовался этим вопросом (когда писал 16 битные программы) и видел утверждения, что cisc в процессорах интел когда-то всё же был. Примерно с P6 всё пошло в разнос, тогда же появились все эти уязвимые бранч предикторы и всё остальное. Они были уязвимыми ещё 20 лет назад, мельдаун и спектра эксплуатируют давным давно известные архитектурные "особенности".

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

87. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 10-Июн-20, 19:53

бранч предикторы - следствие наличия конвейера, а никак не микрокода. RISC/CISC тут не при чем.

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

88. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (40), 10-Июн-20, 20:06

Но я не вижу тут противоречий. Ведь x86 процессоры (в частности нынешние) архитектурно являются RISC, что я изночально и утверждал.

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

89. "Микроядро seL4 математически верифицировано для архитектуры ..." –2 +/–

Сообщение от Аноним (83), 10-Июн-20, 20:11

> Ведь x86 процессоры (в частности нынешние) архитектурно являются RISC
Это тавтология. ВООБЩЕ ВСЕ CISC процессоры архитектурно содержат в себе RISC процессор как ядро.

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

92. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Cradle (?), 10-Июн-20, 20:39

нет, это как раз ошибка. Вся разница в том кто решает как правильно загружать конвеер и кэши - в risc этим преимущественно занимается компилятор, в cisc внутренняя логика со всеми своими branch prediction, в экстремальной vliw только компилятор. Поэтому собственно risc начались с mips архитектуры, хотя например pdp-11 по системе комманд тоже к ним относят.

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

95. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним из предыдущего ответа. (?), 10-Июн-20, 20:58

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

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

103. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 10-Июн-20, 22:49

> Поэтому собственно risc начались с mips архитектуры, хотя например pdp-11 по системе комманд тоже к ним относят.
PDP-11 не относят к RISC только по тому что во времена расcыпухи такого деления не было. Сделай кто сейчас совместимую однокристалку и она станет RISC-ом. Просто мне трудно представить зачем приделывать микрокод к процессору с ортогональной системой команд.

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

110. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Cradle (?), 10-Июн-20, 23:27

https://ru.wikipedia.org/wiki/%D0%9A1801%D0&#...

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

115. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 11-Июн-20, 00:02

Да, я знаю про это. Даже к друзьям на БуКашке периодически ходил играться "для расширения кругозора", сам обладая Спектрумом. Но официально RISC-ом он, как и MOS6502 не называется по той причине, что само понятие в широкие массы было введено только в 90-е.

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

116. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 11-Июн-20, 00:17

У меня вообще есть предположение, что слово RISC присваивают процессору, когда хотят громко произнести: "Мы избавились от микрокода чтобы получить одну команду за такт" и избегают когда нужно сказать что "Мы избавились от микрокода чтобы сэкономить на транзисторах"

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

139. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Вебмакака (?), 11-Июн-20, 12:25

Нет. У PDP-11 пачка омских режимов адресации, RISC всегда load/store.

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

141. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 11-Июн-20, 14:25

> Нет. У PDP-11 пачка омских режимов адресации, RISC всегда load/store.
load/store - это вторичный половой признак. Он является следствием, а не причиной и по этому не может считаться в отрыве от других признаков.
На то что является первичным, позволю себе сослаться на автора понятия RISC Джона Кока [1]:
This was the key realization: Imposing microcode between a computer and its users imposes an  expensive  overhead in performing the most frequently executed instructions. Thus, a key task in  designing the experimental machine was to investigate the consequences of exposing a microcomputer directly to the end user. In many  cases, a microcomputer limited to instructions executable in one cycle would execute a macro-instruction  in about  as many  cycles as a System/370 Model 168 executing the equivalent instruction. The great potential  was that  simple  instructions would run substantially faster for the same circuit family and cycle time because the overhead of executing a CISC (Complex Instruction-Set Computer) interpreter was pared away.
Он однозначно говорит что RISC получился из CISC удалением микрокода и его интерпретатора. Ортогональность, load/store и прочее - только следствия.
[1] The evolution of RISC technology at IBM: https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=5389855

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

197. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Led (ok), 15-Июн-20, 01:06

> по тому
> по этому
Да сколько ж можно?!

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

173. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (166), 12-Июн-20, 01:16

>хотя например pdp-11 по системе комманд тоже к ним относят.
А что, разве в системе команд PDP11 не было команд, производящих изменения данных прямо в ячейках памяти?

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

94. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (40), 10-Июн-20, 20:45

VLIW (EPIC) разве не могут притворяться CISC? Вроде и эльбрусы VLIW, притворяющийся CISC.

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

105. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 10-Июн-20, 22:56

> VLIW (EPIC) разве не могут притворяться CISC? Вроде и эльбрусы VLIW, притворяющийся CISC.
CISC - это архитектура, а не система команд, а притворяются EPIC-и начиная с Крузо именно поддержкой x86-х команд. И для последних вполне можно сделать и настоящий RISC-процессор, только кому это надо? С такой-то бессистемицей в опкодах.

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

148. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (-), 11-Июн-20, 14:51

> Это тавтология. ВООБЩЕ ВСЕ CISC процессоры архитектурно содержат в себе RISC процессор как ядро.
Там вон в новости про очередные дыры в интеле разрисовано что оно содержит. RISC это разве что с очень большой натяжкой совы на глобус.

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

91. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (9), 10-Июн-20, 20:22

> Всегда, даже в 8080.
Ну ты фантазёр…

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

101. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 10-Июн-20, 22:39

> Ну ты фантазёр…
Люблю опеннет за наличие икспердов. Люди уже даже эмулятор для микрокода 8080 написали, но местное сообщество все-равно говорит что его не существует: https://github.com/jdryg/8080Emu

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

123. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (49), 11-Июн-20, 01:16

Наличие микрокода не обязывает ядро быть RISCовым

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

149. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (-), 11-Июн-20, 14:53

> Наличие микрокода не обязывает ядро быть RISCовым
Возможно он пытается сказать что "блоки выполнения" за uCode ROM сами по себе смахивают на RISC? До некоторой степени, пожалуй, смахивают.

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

158. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (83), 11-Июн-20, 18:12

> Возможно он пытается сказать что "блоки выполнения" за uCode ROM сами по себе смахивают на RISC? До некоторой степени, пожалуй, смахивают.
Бинго! Первый тезка который это понял. А то что у этих "блоков выполнения" вместо номеров операций и регистров в системе команд используются номера SELECT-ов к логическим блокам, это просто так удобней для CISC.

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

100. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (98), 10-Июн-20, 22:33

> Всегда, даже в 8080.
Чиво??? RISC ядро появилось в 486

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

174. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (166), 12-Июн-20, 01:27

Если не Pentium II

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

134. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (132), 11-Июн-20, 10:06

>RISC-V эта такая современная альтернатива мипсу (который тоже открыли и закопали, а ведь хорошая альтернатива арму была).
MIPS это спецификация RISC от MIPS Technologies, Inc.
RISC-V  это спецификация RISC от RISC Foundation.

Какая из них лучше, хуже?
Вообще мне нравятся SPARC, почему бы их не производить - UltraSPARC T1, UltraSPARC T2?

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

150. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (-), 11-Июн-20, 14:54

> Вообще мне нравятся SPARC, почему бы их не производить - UltraSPARC T1, UltraSPARC T2?
Так производите. Даже какое-то из ядер выкладывали. Просто это огроменный чип и это будет большое, мучительное и дорогое приключение, а отбить затраты продажами этого... сможете?

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

84. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (84), 10-Июн-20, 19:35

Пацаны это то самое открытое железо о котором мечтают все ГНУтые?

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

93. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Cradle (?), 10-Июн-20, 20:45

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

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

96. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (21), 10-Июн-20, 21:04

К тому же этих спецификаций вагон и маленькая тележка, я выше писал.

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

129. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (-), 11-Июн-20, 06:36

Главное чтобы было всё без лицензионных отчислений.

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

175. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (49), 12-Июн-20, 02:32

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

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

185. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (185), 13-Июн-20, 10:16

О хо-хо, хо-хо! :(

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

107. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (107), 10-Июн-20, 23:18

it is proved to be bug-free relative to a specification
То есть, это всего-лишь доказательство что реализация соответствует спецификации безо всяких этих ваших багов. Это не гарантирует отсутствие багов в спецификации (недавние новости какбэ намекае) и не гарантирует отсутствие уязвимостей в самой архитектуре, которые, при наличии присутствия, превратят весь этот ваш матан в пшик, как мы наблюдаем уже второй год с x86

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

111. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (49), 10-Июн-20, 23:32

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

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

114. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (107), 10-Июн-20, 23:59

За науку я готов выпить хоть яду. Проставляйся.

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

121. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (49), 11-Июн-20, 01:07

Это не пить... это для твоего проца :)

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

125. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (107), 11-Июн-20, 01:24

Мой проц справляется даже без радиатора. Я давно уже не покупаю печки.

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

117. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (118), 11-Июн-20, 00:26

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

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

122. "Микроядро seL4 математически верифицировано для архитектуры ..." +2 +/–

Сообщение от Аноним (49), 11-Июн-20, 01:11

Лучшее доказательство - отсутствие спекуляция при работе с памятью.

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

151. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (-), 11-Июн-20, 14:55

> Лучшее доказательство - отсутствие спекуляция при работе с памятью.
Rowhammer'у так например это похрен.

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

178. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (176), 12-Июн-20, 09:57

А вы - точно понимаете значение употребляемых вами слов?

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

193. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от НамеНаме (?), 13-Июн-20, 18:02

Это, увы, не достижимо в принципе. Ну так Рассель, Кантор, Гедоль ну и НамеНаме считают.

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

127. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Vitaly (??), 11-Июн-20, 05:11

https://github.com/seL4/seL4/blob/master/src/smp/lock.c 25 строк.
clh_lock_t big_kernel_lock ALIGN(L1_CACHE_LINE_SIZE);
Да тут не только математически, но и астрально картами Таро можно обосновать.

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

130. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Онаним (?), 11-Июн-20, 08:35

А тем временем даже в Falcon 9 уже обыденный x86.

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

177. "Микроядро seL4 математически верифицировано для архитектуры ..." –1 +/–

Сообщение от Аноним (176), 12-Июн-20, 09:54

Нет. Не обыденный. Не обольщайтесь ложной простотой вопроса.

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

190. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от НамеНаме (?), 13-Июн-20, 17:55

В Еврефайтерах и Рафалях тоже х86 (купленные на барахолке), а в Ф-22 960-тые и 860-тые.

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

183. "Микроядро seL4 математически верифицировано для архитектуры ..." +1 +/–

Сообщение от Аноним (182), 13-Июн-20, 09:51

Отличная новость, и ОС интересная.
... Зато попиарили забесплатно закрытую нех от касперыча, чо.

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

184. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (185), 13-Июн-20, 10:14

>... Зато попиарили забесплатно закрытую нех от касперыча, чо.
Макса Чиркова деньги не интересуют.

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

188. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (187), 13-Июн-20, 10:49

> ... Зато попиарили забесплатно закрытую нех от касперыча, чо.
"Какая страна, такая и ОС".

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

201. "Микроядро seL4 математически верифицировано для архитектуры ..." +/–

Сообщение от Аноним (201), 15-Июн-20, 23:50

По итогу самым безопасным окажется ядро "Hello world".

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

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

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

Партнёры:

Хостинг:

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

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

1. "Микроядро seL4 математически верифицировано для архитектуры ..."	+13 +/–
Сообщение от neAnonim (?), 10-Июн-20, 12:28
осталось только распространить risc-v в массах. и тогда можно будет закопать x86
Ответить \| Правка \| Наверх \| Cообщить модератору


	2. "Микроядро seL4 математически верифицировано для архитектуры ..."	+12 +/–
	Сообщение от Аноним (2), 10-Июн-20, 12:33
	Закопать то вряд ли, но это явно тот путь, по которому следует развиваться
	Ответить \| Правка \| Наверх \| Cообщить модератору


	49. "Микроядро seL4 математически верифицировано для архитектуры ..."	–1 +/–
	Сообщение от Аноним (49), 10-Июн-20, 16:43
	Интел не позволит, закопают всех конкурентов в округе.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	51. "Микроядро seL4 математически верифицировано для архитектуры ..."	+4 +/–
	Сообщение от erthink (ok), 10-Июн-20, 16:48
	> Интел не позволит, закопают всех конкурентов в округе. Сначала интелю нужно повторить трюк Мюнхгаузена (вытащить себя за волосы), а уж потом может-быть, если повезет...
	Ответить \| Правка \| Наверх \| Cообщить модератору


	108. "Микроядро seL4 математически верифицировано для архитектуры ..."	+1 +/–
	Сообщение от Аноним (-), 10-Июн-20, 23:19
	> Интел не позволит, закопают всех конкурентов в округе. Копать устанут - его уже толпа фирм взяли в оборот. И кстати говорят что скоро фирму Интел будет ждать еще один приятный подарок: Эпл вроде бы на днях должен анонсировать переход на 64-битные ARM... :)
	Ответить \| Правка \| К родителю #49 \| Наверх \| Cообщить модератору


	7. "Микроядро seL4 математически верифицировано для архитектуры ..."	+19 +/–
	Сообщение от A.Stahl (ok), 10-Июн-20, 12:55
	>осталось только распространить risc-v в массах Тю, мелочи-то какие. Займёмся сразу после отказа от империализма и излечения всех болезней.
	Ответить \| Правка \| К родителю #1 \| Наверх \| Cообщить модератору


	16. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Сейд (ok), 10-Июн-20, 13:15
	Жалеешь 140 рублей?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	25. "Микроядро seL4 математически верифицировано для архитектуры ..."	–1 +/–
	Сообщение от A.Stahl (ok), 10-Июн-20, 13:52
	?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	26. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Сейд (ok), 10-Июн-20, 13:57
	https://www.crowdsupply.com/sifive/hifive1-rev-b
	Ответить \| Правка \| Наверх \| Cообщить модератору


	31. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от A.Stahl (ok), 10-Июн-20, 14:42
	Мне показывает $59.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	41. "Микроядро seL4 математически верифицировано для архитектуры ..."	+1 +/–
	Сообщение от Аноним (41), 10-Июн-20, 15:29
	https://aliexpress.ru/item/4000818117666.html?algo_pvid=39bb...
	Ответить \| Правка \| Наверх \| Cообщить модератору


	44. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Ыр2.0 (?), 10-Июн-20, 15:45
	Трусы Большой Мужчина Женщина Купить Большой Проститутка Шланг
	Ответить \| Правка \| Наверх \| Cообщить модератору


	50. "Микроядро seL4 математически верифицировано для архитектуры ..."	–3 +/–
	Сообщение от ala (?), 10-Июн-20, 16:44
	Просто любопытно: вы в самом деле пользуетесь сайтом aliexpress на русском языке? Серьёзно? Это не шутка? Вот прямо так его и читаете — со всеми их шлангами и многими удовольствиями?
	Ответить \| Правка \| К родителю #41 \| Наверх \| Cообщить модератору


	52. "Микроядро seL4 математически верифицировано для архитектуры ..."	+2 +/–
	Сообщение от erthink (ok), 10-Июн-20, 16:50
	> Просто любопытно: вы в самом деле пользуетесь сайтом aliexpress на русском языке? > Серьёзно? Это не шутка? Вот прямо так его и читаете — со > всеми их шлангами и многими удовольствиями? Нисколько не поклонник, но разве на английском там сильно меньше "удовольствий"?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	120. "Микроядро seL4 математически верифицировано для архитектуры ..."	+1 +/–
	Сообщение от n80 (?), 11-Июн-20, 00:58
	Удивительно, но всё-таки сильно меньше. По крайней мере, у меня такая выборка.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	132. "Микроядро seL4 математически верифицировано для архитектуры ..."	–1 +/–
	Сообщение от Аноним (132), 11-Июн-20, 09:48
	Английский более информативный.
	Ответить \| Правка \| К родителю #52 \| Наверх \| Cообщить модератору


	86. "Микроядро seL4 математически верифицировано для архитектуры ..."	+3 +/–
	Сообщение от Аноним (86), 10-Июн-20, 19:40
	А ты пользуешься китайским вариантом или просто думаешь, что для алика родной английский?
	Ответить \| Правка \| К родителю #50 \| Наверх \| Cообщить модератору


	133. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (132), 11-Июн-20, 09:49
	Алиэкспресс ориентируется на английский т.к. международный. Таобао мандаринский т.к. внутренний.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	142. "Микроядро seL4 математически верифицировано для архитектуры ..."	+1 +/–
	Сообщение от Аноним (-), 11-Июн-20, 14:33
	> А ты пользуешься китайским вариантом или просто думаешь, что для алика родной английский? Просто на английском покупает сильно больше - так что этим можно и нормальный перевод живыми переводчиками. А россиянам с их объемами рынка только на гуглтранслейт хватает. Поэтому русское описание товаров на али...
	Ответить \| Правка \| К родителю #86 \| Наверх \| Cообщить модератору


	119. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от n80 (?), 11-Июн-20, 00:56
	Насколько знаю, при заходе с IP-адресов из RU областей aliexpress крайне настойчиво перенаправляет на версию с этим хтоническим ужасом от мира машинного перевода. И отучить его от этого настройками сайта и даже плагинами браузера становится всё труднее и труднее. Это какое-то безумие.
	Ответить \| Правка \| К родителю #50 \| Наверх \| Cообщить модератору


	131. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (132), 11-Июн-20, 09:47
	На английский переключаю, мандаринским ещё не овладел чтобы таобао читать.
	Ответить \| Правка \| К родителю #50 \| Наверх \| Cообщить модератору


	166. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (166), 12-Июн-20, 00:52
	Но русскоязычный Ali показывает цены в национальной валюте. В которой мы и платим.
	Ответить \| Правка \| К родителю #50 \| Наверх \| Cообщить модератору


	171. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (171), 12-Июн-20, 01:14
	> Но русскоязычный Ali показывает цены в национальной валюте. В которой мы и платим. Понять по русскому описанию товара что это за неведомая штука в сколь-нибудь продвинутых случаях решительно невозможно. Но если хочется почитать анекдоты, пойдет.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	181. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (166), 13-Июн-20, 01:14
	Промт-онлайн с ангийской версии Али не сильно лучше переведёт.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	186. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (-), 13-Июн-20, 10:43
	> Промт-онлайн с ангийской версии Али не сильно лучше переведёт. А мне оно и не надо. Если бы я не умел в инглиш, мой потолок в IT ограничивался бы заменой плашки памяти в древнем компе жэка. Оно мне надо?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	75. "Микроядро seL4 математически верифицировано для архитектуры ..."	–1 +/–
	Сообщение от Michael Shigorin (ok), 10-Июн-20, 18:58
	> Get a single HiFive1 Rev B dev kit, featuring the FE310-G002, > SiFive's second generation open source RISC-V 32-bit SoC. Кому этот перемикроконтроллер нужен-то? Их rv64gc за килобакс производительностью не радует, а это...
	Ответить \| Правка \| К родителю #26 \| Наверх \| Cообщить модератору


	102. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Сейд (ok), 10-Июн-20, 22:43
	Производителям домашней автоматизации.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	126. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (49), 11-Июн-20, 01:32
	Домашним автоматизаторам хватит пригоршни ЛА3
	Ответить \| Правка \| Наверх \| Cообщить модератору


	143. "Микроядро seL4 математически верифицировано для архитектуры ..."	+1 +/–
	Сообщение от Аноним (-), 11-Июн-20, 14:34
	> Домашним автоматизаторам хватит пригоршни ЛА3 Да что там, спичек и желудей.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	167. "Микроядро seL4 математически верифицировано для архитектуры ..."	+/–
	Сообщение от Аноним (166), 12-Июн-20, 00:59
	ЛА3 потребуется очень большая пригоршня, т.к. триггеры, счётчики, регистры тоже придётся на них делать. Отсюда, к тому же, большое энергопотребление. И самое главное - жёсткая логика, нет гибкости.
	Ответить \| Правка \| К родителю #126 \| Наверх \| Cообщить модератору