Здравствуйте, AlexRK, Вы писали:
ARK>Так что сама идея довольно простая. Там, где верификатор не знает, корректная операция или нет — он заставляет программиста вставить рантайм-проверку.
А чё б ему самому не вставить проверку там, где он не уверен?
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Нет, извини, давай уточним. Если бы речь шла о том, что при существующей архитектуре процессора и ОС предлагается добавить эту статическую верификацию — это одно. Ты же предлагаешь существующую архитектуру заменить такой, в которой не будет аппаратной защиты вообще. А значит, все приложения смогут делать что им вздумается, если только не помешает статическая верификация.
И непонятно, ради чего так трахадзе.
Ошибки типе Spectre в софтварии известны уже давно — все эти подборы паролей/криптоключей, основанные на том, что верификация правильного и частично неправильного ключа может различаться по времени, это как раз оно. Статический верификатор, который заставляет программиста вставлять проверки, и считает на этом свою работу завершенной, от таких ошибок не спасает.
При всем при том, аппаратная проверка работает эффективнее и логически качественно проще. В ней не хватает лишь одного: она работает большими кусками, страницами и сегментами, а было бы клево, если бы ее можно было на пользовательский массив или строку натравить.
Просто нышешние процессора рассчитаны на то, что их аппаратные способы защиты будут использовать, как это делалось еще во времена VAX и System/370. Ну а системный софтварий пишется в рассчете на то, что процессора со времен VAX принципиально не изменились. Но это все меняется постепенно, по мере увеличения интереса к managed средам.
Здравствуйте, Pzz, Вы писали:
ARK>>Так что сама идея довольно простая. Там, где верификатор не знает, корректная операция или нет — он заставляет программиста вставить рантайм-проверку.
Pzz>А чё б ему самому не вставить проверку там, где он не уверен?
Да ради бога, пусть вставляет. Просто если он сам не вставит, а проверка в этом месте необходима, то программа не скомпилируется.
Пардон, неправильно понял. В смысле, почему бы самому компилятору не вставить?
Да, можно, почему нет. Если мы допускаем рантайм-ошибки и исключения, это самый простой выход — если проверка провалилась, генерим ошибку.
Там, где рантайм-ошибки и исключения не допускаются — например, в ядре ОС — там придется программисту самому вставлять проверки и реагировать на ошибки.
Здравствуйте, AlexRK, Вы писали:
ARK>Вы забываете про переключения контекста, которые очень сильно снижают производительность и выполняются в стстемах с аппаратной защитой _постоянно_. Статическая верификация позволяет выполнять весь код в одном «кольце» (да, собственно, кольца вообще не нужны).
Они снижают производительность лишь потому, что никто не заморачивался заоптимизировать их в процессоре так, чтобы они не снижали производительность. Но это постепенно меняется. В более-менее свежих интеловских процессорах кэш (и TLB?) стал привязан к "процессу", и при переключении процессов нет уже нужды инвалидировать весь кэш. Достаточно сказать процессору, что PID поменялся, а дальше оно само.
Здравствуйте, netch80, Вы писали:
T>>Ну как минимум одно достоинство у них всё-таки есть. В utf-8 cимвол по номеру в строке ищется за константное время,только если он английский. C utf-16 это распространяется на большинство языков, а с utf-32 — вообще на всё.
N>Стандартная и грубая ошибка. Символ ты так не найдёшь. Ты найдёшь кодовый пункт. Символ может иметь модификаторы. Чтобы их достоверно подключить, всё равно надо вызывать умную читалку, которая по таблице свойств будет проверять, что идёт за первым пунктом. Если ты этого не делаешь, твой код тупо некорректен.
Для utf-16 есть вроде набор языков символы которых ложатся в 2 байта, как latin1 в utf-8. То есть если знаешь точно, что у тебя в строке символы одного из этих языков — можно за константу выбирать. И я думал, что в utf-32 всё лезет в 4 байта, кроме всякой нечисти типа эмодзи, но похоже это неправда.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Ну и еще один момент. Переключение процессов в настольной системе — это (не всегда, конечно) следствие того, что пользователь выбрал иное окно. По той причине, что потоки оконных приложений, пока пользователь с их окнами не работает, в Windows обычно спят и процессор не загружают. А активация окна спящего GUI — потока — это такое количество всяких действий, на фоне которого переключение контекста есть всего лишь мелочь. Одна отрисовка окна чего стоит.
Ну нет, конечно. Там же еще куча всякой фоновой активности. Часто вообще не связанной с отрисовкой чего бы то ни было.
Здравствуйте, netch80, Вы писали:
N>Не из-за этого, а из-за своей изначальной инвалидности.
А инвалидность заключалась в том, что он исполнял х86ой код в 10 раз медленнее конкурентов.
Все остальные проблемы интел бы решил в течении пары лет.
N>Но остаётся вопрос принципиально разных архитектур (CPU vs. GPU) и оптимизаций под конкретное железо. А вот тут большая загвоздка — те, кто для конкуренции вылизывает даже 1%, не пойдут на тотальный AOT, потому что в нём всегда будет меньше гибкости. А таких достаточно много.
1)И все они сливают вот этой штуке http://halide-lang.org/
Программист из adobe убил 3 месяца на оптимизацию фильтра. Авторы halide за один день написали реализацию, которая работает в 2 раза быстрее. Изменив несколько строк сделали реализацию, для ГПУ которая работает в 7 раз быстрее.
2)Если очень хочется, то код можно заточить под конкретный процессор.
Создаём библиотеку примитивов процессора. И учим ВМ для этого процессора транслировать эти примитивы в соответствующие машинные коды.
Можно даже научить ВМ прозрачно подменять референсную реализацию на реализацию для конкретного процессора.
Можно даже сделать так чтобы было доказательство эквивалентности референсной реализации и реализации под конкретный процессор.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, alex_public, Вы писали:
_>А что ты называешь скриптами? Факт наличия интерпретатора на мой взгляд вообще ни о чём не говорит (он даже у C++ есть, а у Питона наоборот есть свой JIT вариант), да и выполнял я вышеописанные команды не в REPL, а набросав скрипт в Notepad++ и запустив в командной строке. Чаще всего скриптами называют как раз короткие фрагменты на языках с динамической типизацией. Ну и помимо этого весьма актуально отсутствие в языке всяческих обязательных каркасов приложения (типа main в C++ или вообще никчемного класса в Java/C#).
Ну вот собственно таким микропрограммам никто не мешает быть статически типизированными.
Более того писать их можно не в блокноте, а в полноценной ИДЕ которая если делать правильно будет запускаться за доли секунды.
Sublime запускается мгновенно. Когда нитра станет нативной она тоже будет стартовать доли секунды. Сейчас при старте .НЕТ тормозит.
WH>>2)Создание консольного приложения на C# занимает несколько секунд. _>Угу, в фантазиях. )
На практике.
_>Ну скажем тот же LLVM это вполне может. Правда там возникают вопросы с заменой стандартной библиотеки языка (под МК обычно используется специализированная версия)...
Там ещё много вопросов возникает.
_>Ну если проектировать с нуля (как хотел автор изначальной темки) непосредственно для этой задачи, то конечно можно сделать намного лучше существующих вариантов. Я имел в виду, что из всех уже готовых решений на данный момент, это выглядит наиболее подходящим вариантом. И кстати выбор команды WebAssembly это подтверждает.
Команду WebAssembly нужно разогнать за феерический идиотизм.
У них в низкоуровневом языке нет goto. Как они вообще до этого додумались?
И я знаю про релупер. Всё равно решение идиотское.
_>Проблема таких систем (кстати Midori/Singularity далеко не первые в этой области, намного раньше было например такое http://www4.cs.fau.de/Projects/JX/index.html решение), что они очень ультимативные: или всё прикладное ПО написано на соответствующем управляемом языке или система просто не работает (нельзя написать один критичный кусочек на голом ассемблере). Ну и соответственно пока я не увижу реализацию например кодека h.264 на управляемом языке, не уступающую по эффективности классическим нативным реализациям, то в нормальное будущее подобной ОС не поверю.
С этим проблем нет.
Дафна может доказывать любой императивный код включая ассемблер.
Ну и опять же halide полностью безопасный. И обгонять его озвереешь.
_>Хы, ну возможно. Я с самим языком подробно не возился, помню только что мы обсуждали нюансы с SIMD векторами... )
Я тоже. Просто внимательно документацию изучил.
_>Да, это известное деление и я считаю очень правильное. Что касается асинхронного варианта (в данной терминологии), то на мой взгляд самым лучшим решением для него является модель акторов.
1)Акторы и асинхронная модель в мидори друг другу не противоречат.
2)Акторы нужно делать правильно. Чтобы не получилось как в эрланге в котором получение сообщений из очереди О(размер очереди). И как следствие непредсказуемый уход в астрал если нагрузка кратковременно превысит некоторый порог.
3)В любом случае акторы отлаживать труднее чем то что есть в мидори. У них там есть отладчик, который прозрачно ходит между процессами.
_>В целом правильная платформа/язык из идеального мира конечно же должна обеспечивать распараллеливание на всех 3-ёх уровня сразу, а не как мы сейчас стыкуем разные технологии. Но то идеальный мир... )))
Так мы тут про идеальный мир и говорим.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>2. Либо запретить нативный язык как минимум для пользовательских программ. В ОС не запретишь — кто этим управляемым кодом управлять-то будет ?
Совершенно не обязательно. Представь себе конструкцию, в которой все нужные проверки вставляет компилятор, когда генерирует для твоей программы код на ассемблере, но если проверка сработает, то он (компилятор) вполне может сконструировать вызов библиотечной функции, которая написана на том же самом managed языке.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>А вот что будут делать, если в алгоритме статической верификации обнаружилась ошибка, а программы уже прошли этап этой верификации, разошлись в миллионах копий и теперь рушат ОС или получают доступ к чужой памяти — объясни. Срочно патчить все выпущенные программы ? Как ? Фирма, выпустившая эту программу, давно закрылась, авторы разбрелись кто куда.
Ну в принципе, организационно это лечится. Например так:
1. Чтобы программа в принципе запускалась, необходимо получить сертификат соответствия — электрическую подпись, которую выдают после прохождения верификации
2. Одним из условий является предоставление исходников, которые на возмездной основе хранятся в доверенном центре
3. Если в верификаторе обнаружилась дыра, то все программы переверифицируются
4. Если исправленный верификатор обнаружил в существующей программе ошибку, ее сертификат отзывается, и программа перестает запускаться
Большой бизнес, поди, был бы рад такому способу жизни. Я — не очень
Здравствуйте, AlexRK, Вы писали:
ARK>Вы никак не поймете простую вещь. Верификатор работает на этапе компиляции (ну, еще на этапе инсталляции происходит верификация промежуточного кода, но речь не об этом). Компилятор заставляет вставить рантайм-проверки в тех местах, где они нужны. Но это совершенно не эквивалентно тому, что есть в C#/Java! В управляемых языках проверки вставляются во всех местах, а в статически верифицированном коде — только там, где надо. Таких мест может быть на порядок меньше.
И находиться они будут исключительно в местах ввода внешних данных.
А внешние данные нужно проверять всегда.
Но если подумать всё ещё интереснее. На практике проверок будет намного меньше чем в нативном коде. Просто по тому что в нативном коде народ ставит кучу проверок чтобы ничего не упало. А в верифицируемом коде все эти проверки делает компилятор на этапе компиляции.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Эээ, минуту. В чем нашли-то ? В доказательствах или в теоремах ? Если первое — это на сами теоремы вообще-то никак не влияет. Ну нашли ошибку в доказательстве, но теорема-то верна ? Надо ее по-иному доказать, вот и все. PD>А вот если нашли случай неверности теоремы — это совсем иное.
В доказательствах некоторые из которых считались верными столетиями.
Но если в доказательстве есть ошибка, то откуда мы знаем, что теорема верна?
Собственно, мы обсуждаем крайне маловероятную цепочку событий, когда все пропустили ошибку в теореме и в доказательстве.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, AlexRK, Вы писали:
ARK>Вы никак не поймете простую вещь. Верификатор работает на этапе компиляции (ну, еще на этапе инсталляции происходит верификация промежуточного кода, но речь не об этом). Компилятор заставляет вставить рантайм-проверки в тех местах, где они нужны. Но это совершенно не эквивалентно тому, что есть в C#/Java! В управляемых языках проверки вставляются во всех местах, а в статически верифицированном коде — только там, где надо. Таких мест может быть на порядок меньше.
Если существует алгоритм, позволяющий более-менее правдоподобно сказать, где надо вставлять проверки, а где не надо, то никто не мешает применить этот алгоритм в компиляторе C#. Логически получившийся код будет работать так, словно проверки есть везде, но физически они будут присутствовать только в ключевых местах. Это называется оптимизация.
Здравствуйте, neFormal, Вы писали:
WH>>1)Запретить языки с динамической типизацией. WH>>в)Не ловят ошибки программистов. F>так никто не ловит
Это не правда. Даже C# очень много что ловит. А дафна ловит почти всё.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Sinclair, Вы писали:
S>Вывести новую архитектуру на рынок — это титанические инвестиции. А вот если бы основные современные платформы были бы построены на промежуточном коде, то новые процессоры бы выходили ежеквартально.
Оне и так регулярно выходят, у интела например. Со всяческими расширениями типа векторных операций и проч. CISC процессоры можно оптимизировать прозрачно для пользователя.
Здравствуйте, Pzz, Вы писали:
Pzz>Если существует алгоритм, позволяющий более-менее правдоподобно сказать, где надо вставлять проверки, а где не надо, то никто не мешает применить этот алгоритм в компиляторе C#.
Существует. Но без аннотаций в стиле дафны он ужасающи медленный.
Хуже того он тупо вставит проверки, но не исправит ошибки, которые найдёт и заставит исправить дафна.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, Pzz, Вы писали:
Pzz>Если существует алгоритм, позволяющий более-менее правдоподобно сказать, где надо вставлять проверки, а где не надо, то никто не мешает применить этот алгоритм в компиляторе C#. Логически получившийся код будет работать так, словно проверки есть везде, но физически они будут присутствовать только в ключевых местах.
В теории да. На практике написать статический анализатор для языка, специально не заточенного под это, весьма сложно. Все известные мне статические анализаторы написаны для очень простых языков.
Pzz>Это называется оптимизация.
Призывы к использованию других ОС приравнять к оправданию терроризма. Оправдывающих терроризм — расстрелять.
WH>Учим компилятор вставлять рантайм проверки в тех местах где он не смог статически доказать корректность. WH>Если проверка провалилась, то молча прибиваем процесс.
И молча же выписываем постановление автора программы — расстрелять.
Здравствуйте, Pzz, Вы писали:
Pzz>9. Firewall не нужен. Но право пользоваться сетью должно быть привязано к каждой программе, которой это нужно, и выдаваться ей путем явного запроса разрешения у человека
Здравствуйте, WolfHound, Вы писали:
WH>Ты знаешь, что внутри всех х86 процессоров живёт процессор с совершенно иной системой команд. Если выкинуть прослойку, которая конвертирует х86тые команды во внутренние команды то можно разогнать процессоры на десяток другой процентов. WH>10% производительности на ровном месте тебе мало?
Я слышал в пересказе через общего знакомого мнение мужика, работающего в Интеле, что frontend, который переваривает внешне видимую систему команд в реальную внутреннюю, штука довольно простая, кто угодно ее может сделать, и вообще, на результат она особо не влияет. Реальная разница как раз в исполнителе этих внутренних "настоящих" команд, и там искусство заключается в том, чтобы изучить, как реальный софтварий процессором пользуется, и сделать именно те оптимизации, которые требуются. И это очень трудоемко и денежно именно потому, что софтвария изучать приходится много. И именно поэтому разработка настоящих процессоров — это игра большого бизнеса, а изобретение очередной гениальной системы команд к победе в этой игре вообще не имеет отношения.
