Здравствуйте, alex_public, Вы писали:

_>Даже для 3-ёх строчных скриптов? ) Вот буквально вчера у меня тут обнаружилось, что fb2 файлы скаченные с одного известного сайта имеют некорректную структуру (содержат html entities, хотя fb2 — это обычный xml) и из-за этого не читаются некоторым ПО. Проблема была решена (причём для целой папки таких fb2 файлов за раз) за минуту в три строчки на Питоне. На популярных статических языках я бы к этому времени успел бы разве что оборудовать инфраструктуру (настроить проект или скрипты сборки) и перешёл бы к написанию обязательного каркаса приложения...
1)Скриптам никто не мешает быть статически типизированными.
2)Создание консольного приложения на C# занимает несколько секунд.

_>Согласен (и кстати для МК не обязательно делать исключение).
Тут ИМХО нельзя всех под одну гребёнку.

_>И думаю что идеальной заменой нативного кода должно быть что-то вроде LLVM IR. Согласен? )
Формат промежуточного кода отдельный и большой разговор.
Туда как минимум нужно добавить дафну. Ну и стековая ВМ гораздо практичнее для такого применения.

WH>>3)За основу ОС берем мидори. http://joeduffyblog.com/2015/11/03/blogging-about-midori/
_>Крайне сомнительно.
Обоснуй.

WH>>в)Добавляем http://halide-lang.org/ для параллельного программирования.
_>Ну "параллельное программирование" — это громко сказано. Всё же в общем случае оно делится (на современном железе) на 3 совместно работающих уровня: SIMD, многоядерность (решения типа OpenMP), кластеры (решения типа MPI). И данный язык, насколько я помню, занимался решением только нижнего уровня параллельности (SIMD).
Не правильно. В текущей реализации SMID и многоядерность. Но саму модель можно и на кластер натянуть. В данном случае между многоядерностью и кластером разницы никакой.

Но тут я имел в виду немного другое. Я делю многопоточное программирование на 2 типа.
Асинхронное. Это когда мы много ждём и мало считаем.
Параллельное. Это когда у нас есть пачка данных и нам её нужно очень быстро посчитать.

Асинхронное программирование в мидори сделано хорошо.
Параллельное тоже есть, но по сравнению с halide детский сад.

Здравствуйте, AlexRK, Вы писали:

PD>>Компиляция прошла давно, на машине пользователя бинарник. Машинные коды верифицировать будем ?

ARK>Не, на машине пользователя некое промежуточное представление (высокоуровневый бинарник). Это промежуточное представление тоже верифицируется (при установке программы), но более упрощенным алгоритмом.

Вчера ты мне приводил пример на С-подобном языке с этой самой верификацией, и говорил, что после того, как она прошла, программа признается готовой к употреблению. Предполагалась компиляция в нативный код. Теперь вдруг вылезло промежуточное представление, которое нужно еще раз верифицировать, уже на машине пользователя. Я что-то запутался. И зачем, ее , кстати, верифицировать на машине пользователя, если она уже один раз 100% надежно отверифицирована ?

Здравствуйте, Sharov, Вы писали:

S>Не уверен, что замечательно. Если для драйверов я еще могу представить промежуточное исполнение и всяческие jit-оптимизации. То для real-time уже не очень -- там надо сразу, быстро и гарантированно без задержек.
Зачем JIT? JIT не нужен. Кто мешает компилировать при установке приложения?

Здравствуйте, samius, Вы писали:


PD>>Вот тут не понял. Писать с нуля, конечно, придется. Но в итоге хочу я одновременно иметь 2 работающих приложения. И вариант, что мы с одного на другое переключаемся так, что когда одно работает, другое работать не имеет права, не принимается — это уже не многопрограммный режим, а бог знает что. Одно приложение с недоказанной корректностью обращений к памяти (какой-то фоновый процесс, которому часами работать надо), другое — нужна гарантия недоступности их памяти. И что делать ?
S>а) соглашаться на бог знает что.

Рухнет ведь.

S>б) высаживать приложение с недоказанной корректностью на другую машину.

Это ты пользователю скажи. Дескать, вот тебе одни программы, а вот другие. Купи 2 машины (заплати двойные деньги), ну а мы, так и быть, поможем тебе по сети организовать их взаимодействие. Если, конечно, при передаче по сети плохая машина не передаст что-то плохое хорошей машине . Зато будет статическая верификация.

S>в) переходить на многопроцессорные машины и гонять программы с разным клеймом на физически разных процессорах.

Хм, а в чем отличие от многоядерности на одном процессоре ? Только кеши изолированы, а память-то нет.
Ну и, пардон, но предлагать разработчику тех же материнок бросить все, что они сейчас делают, и делать только многопроцессорные машины — пошлют они тебя очень далеко.
Кстати, и стоить они будут несколько дороже. А во имя чего ?
Утопия.

Здравствуйте, Sharov, Вы писали:

PD>>Я не знаю, насколько она там критична (вряд ли), но сомневаюсь, что MS согласится за любые деньги ее дорабатывать.

S>Куда денутся.

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

Здравствуйте, Pavel Dvorkin, Вы писали:

scf>>Чтобы после переезда в другую страну включаешь кофеварку, она лезет на сервер. И сервер знает, что а) это та же кофеварка б) она теперь в другой стране. Решает проблему аутентификации и локализации.

PD>Чудно, а ее теперь как из внешнего мира искать ?
Она может сама себя найти, подключившись к серверу. Лучше каждой кофеварке знать свой сервер, чем серверу хранить список адресов всех кофеварок. Если не нравится — есть куча способов, от DNS до распределенных сетей.

PD>Хм. Я все же хочу пооптимизировать сам на уровне ассемблера. Запретишь ?
Да. Если вендор выпускает новое цпу с интересными командами, это его проблема, чтобы тесты и тяжелые программы компилировались в эффективный нейтив. Ну или продавливать расширение байткода для векторных операций к примеру.

PD>Связи между вырубанием сети, лимитами а диске и ограничением цпу (что имеется в виду, кстати?) и изоляцией процессов не вижу.
Под изоляцией процессов я понимаю в том числе разграничение разделяемых ресурсов (см. выше) и готовность процесса к тому, что ресурсы ему урежут.

Здравствуйте, scf, Вы писали:

PD>>Чудно, а ее теперь как из внешнего мира искать ?
scf>Она может сама себя найти, подключившись к серверу. Лучше каждой кофеварке знать свой сервер, чем серверу хранить список адресов всех кофеварок.

Она-то себя и так найдет, еще бы, а мне из другой части света как к ней добраться ?

>Если не нравится — есть куча способов, от DNS до распределенных сетей.

Так, стоп. Во-первых, о DNS пока речи не было — к этой кофеварке был прибит ее адрес, а DNS имя вроде как не прибивали ? Если же предлагаешь дать ей DNS имя — оно тоже прибито или нет ? Если нет — ты получишь систему, в которой вместо IP адресов будут DNS-имена. Такое сделать в принципе можно — в конце концов IP-адреса это тоже "деревья", но с узлами в виде масок подсетей, а DNS имена — это деревья из текстовых строк. Но чем это лучше будет ?


PD>>Хм. Я все же хочу пооптимизировать сам на уровне ассемблера. Запретишь ?
scf>Да. Если вендор выпускает новое цпу с интересными командами, это его проблема, чтобы тесты и тяжелые программы компилировались в эффективный нейтив. Ну или продавливать расширение байткода для векторных операций к примеру.

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

PD>>Связи между вырубанием сети, лимитами а диске и ограничением цпу (что имеется в виду, кстати?) и изоляцией процессов не вижу.
scf>Под изоляцией процессов я понимаю в том числе разграничение разделяемых ресурсов (см. выше) и готовность процесса к тому, что ресурсы ему урежут.

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

Здравствуйте, Pavel Dvorkin, Вы писали:


PD>Заставить MS что-то делать, чего она делать не хочет — ну разве что господь бог может, а на Земле — никто.

Я Вас умоляю... Как минимум правительство США, да и другой развитой страны тоже. Если оне хотят в этой стране получать прибыль без проблем. Вопрос выгоды, если надо будет и в 98 будут ковыряться.

Здравствуйте, Pavel Dvorkin, Вы писали:

WH>>Мы говорим про крайне гипотетический случай, когда нашли ошибку в верификаторе.
PD>Что-то мне говорит, что ошибка в программе (даже если она и верификатор) — случай совсем не крайне гипотетичный
Верификатор — это не просто программа. Это критически важная программа. Он доказан математически.
Чтобы понять насколько это серьёзно попробуй, не трогая предикаты и сигнатуру SelectionSortRange написать внутри неё что-то кроме сортировки.
https://rise4fun.com/Dafny/pX4N

PD>Ну тогда я , видимо, не вполне верно твои соображения понял. С AlexRK речь шла о статической верификации на уровне исходного языка, после прохождения которой и компиляции там же программа признается корректной и выпускается в мир. О промежуточном коде там и речи не было, как и о компиляции на этапе установки.
Как мы выяснили ты его не так понял.

PD>Переизложи, пожалуйста, свою точку зрения, кто кого и когда верифицирует и компилирует, и какой у тебя код есть — исходный, промежуточный , нативный, и кто что где делает.
На машине разработчика:
1)Компилируем исходный код в промежуточное представление. Что-то вроде MSIL только грамотно сделанное.
2)Верифицируем полученный промежуточный код. Для того чтобы убедиться, что компилятор не сгенерировал что-то бредовое.
3)Сохраняем промежуточный код в файл.

На машине пользователя:
1)Загружаем промежуточное представление из файла.
2)Верифицируем для того чтобы убедиться, что злобный хакер не сгенерировал что-то бредовое.
3)Из промежуточного представления генерируем нативный код.
4)Верифицируем машинный код. Чтобы убедиться, что генератор нативного кода бред не сгенерировал.
5)Сохраняем нативный код для последующей быстрой загрузки. Опционально добавляем контрольную сумму для того чтобы убедиться, что носитель информации не дурит.

В качестве оптимизации возможно генерация машинного кода на некотором доверенном сервере. И исполнение подписанного этим сервером кода.
PD>Да уж. Надеяться на то, что проблемы с программой, которая изначально рушит ОС, а потом перестает работать, так как ОС ее признада недостойной, решаются с помощью неофициальных патчей — это замечательный деловой подход для разработчиков Ос
Чем больше ты рассказываешь про этот случай, тем больше он походит на неуловимого Джо.
Короче разработчик ОС просто пошлёт одного неудачника и всё.

PD>Эхе-хе... Алгоритмы и методы компиляции тоже вроде как доказаны, а компиляторы порой падают.
Современные компиляторы не имеют примерно никакого отношения к тем алгоритмам, которые доказаны. Ибо эти алгоритмы крайне непрактичны. Это я тебе как разработчик компиляторов говорю.

Здравствуйте, Sharov, Вы писали:


S>Я Вас умоляю... Как минимум правительство США, да и другой развитой страны тоже.

Ну-ну. Впрочем, это уже в Политику.

>Если оне хотят в этой стране получать прибыль без проблем.

Сдается мне , что они ее уже 40 лет получают без проблем. И совсем неплохую получили

>Вопрос выгоды, если наЮдо будет и в 98 будут ковыряться.

И в какую же сумму ты оцениваешь затраты на то, чтобы превратить MS из фирмы, производящей ПО исключительно на продажу в фирму, которая делает что-то по заказу ?

Здравствуйте, scf, Вы писали:

scf>Ну или продавливать расширение байткода для векторных операций к примеру.
Не нужно. Из байткода вообще нужно убрать всё что можно. И если хорошо подумать убрать оттуда можно почти всё.
Достаточно положить эти операции в отдельную библиотеку. Реализация по умолчанию будет использовать базовые операции.
Компилятор родного процессора будет использовать соответствующие операции. А все остальные код из библиотеки.

Здравствуйте, WolfHound, Вы писали:

WH>2)Запретить нативный код.
WH>Проблема нативного кода в том, что он не даёт заменять систему команд процессоров.

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

Здравствуйте, WolfHound, Вы писали:

WH>Верификатор — это не просто программа. Это критически важная программа. Он доказан математически.

Ладно, пусть так.


PD>>Ну тогда я , видимо, не вполне верно твои соображения понял. С AlexRK речь шла о статической верификации на уровне исходного языка, после прохождения которой и компиляции там же программа признается корректной и выпускается в мир. О промежуточном коде там и речи не было, как и о компиляции на этапе установки.
WH>Как мы выяснили ты его не так понял.

Ну насколько я его правильно понял — я его уже спросил, подождем его ответа. Вчера мое понимание того, что он писал, у него возражений не вызывало.

http://rsdn.org/forum/philosophy/7022763.1

Автор: Pavel Dvorkin
Дата: 17.01.18

Утверждение же, что "мы выяснили" — пардон, но зрительская масса как будто ничего не заявляла. Я то есть. Я лишь выяснил, что тебя я неправильно понял.

PD>>Переизложи, пожалуйста, свою точку зрения, кто кого и когда верифицирует и компилирует, и какой у тебя код есть — исходный, промежуточный , нативный, и кто что где делает.
WH>На машине разработчика:
WH>1)Компилируем исходный код в промежуточное представление. Что-то вроде MSIL только грамотно сделанное.
WH>2)Верифицируем полученный промежуточный код. Для того чтобы убедиться, что компилятор не сгенерировал что-то бредовое.
WH>3)Сохраняем промежуточный код в файл.

WH>На машине пользователя:
WH>1)Загружаем промежуточное представление из файла.
WH>2)Верифицируем для того чтобы убедиться, что злобный хакер не сгенерировал что-то бредовое.
WH>3)Из промежуточного представления генерируем нативный код.
WH>4)Верифицируем машинный код. Чтобы убедиться, что генератор нативного кода бред не сгенерировал.
WH>5)Сохраняем нативный код для последующей быстрой загрузки. Опционально добавляем контрольную сумму для того чтобы убедиться, что носитель информации не дурит.

Вот теперь понял. Все ясно. Правда, последнее едва ли нужно — контрольная сумма и так в секторе есть.

Ну что скажу... В общем, достаточно стройно и логично.
Я только не уверен в том, что этот алгоритм верификации действительно будет 100% надежным. То, что он , как ты говоришь, доказан — охотно готов поверить, но все равно не убеждает.

Дело в том, что ты тут привел идеальную схему. А вот что ты писал чуть раньше

>ОС находит те места, которые не может верифицировать и добавляет туда проверку.

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

А вот строгого доказательства того, что таких случаев будет действительно исчезающе мало — я не вижу. И мне остается только верить тебе на слово, что это будет очень редко, настолько редко, что этим можно пренебречь.

А почему я обязан верить ? Ты же не сказал, что есть доказательство, что этот "остаточный член" пренебрежимо мал по сравнению с суммой ряда ?

После этого уверенность в 100% надежности и математической доказанности этой верификации у меня как-то пропадает.

Это все равно, как если бы кто-то сказал — доказано, что сумма углов треугольника в Евклидовой геометрии равно 180, но в 0.0000000000000001% случаев это все же не так.
Если это и впрямь не так в этом проценте случаев — значит, Евклидова геометрия неверна.

Понимаешь, в чем дело ? Законы физики, тем более химии (говорю как химик по образованию) никогда не обязаны выполняться 100%. Механика Ньютона верна, пока не вмешаются релятивистские поправки, а строго говоря, неверна вообще, но эта неверность исчезающе мала и несущественна. В химии теория, которая на 80% дает правильный ответ , а в остальных 20% совсем неверный — замечательная теория. А вот в аксиоматической теории один контр-случай ставит под сомнение всю теорию.

Поэтому у меня возникают сомнения.

Здравствуйте, Pavel Dvorkin, Вы писали:

ARK>>Не, на машине пользователя некое промежуточное представление (высокоуровневый бинарник). Это промежуточное представление тоже верифицируется (при установке программы), но более упрощенным алгоритмом.
PD>Вчера ты мне приводил пример на С-подобном языке с этой самой верификацией, и говорил, что после того, как она прошла, программа признается готовой к употреблению.

Да, готовой в том плане, что она гарантированно корректна и не содержит ошибок времени выполнения.

PD>Предполагалась компиляция в нативный код.

Приношу свои извинения, если я такое писал, то насчет нативного кода я погорячился.

PD>Теперь вдруг вылезло промежуточное представление, которое нужно еще раз верифицировать, уже на машине пользователя. Я что-то запутался. И зачем, ее , кстати, верифицировать на машине пользователя, если она уже один раз 100% надежно отверифицирована ?

Да, нужно, по той причине, что до пользователя может дойти искаженное (случайно или преднамеренно) представление. Но промежуточное представление гораздо проще исходной программы, и его верификация, соответственно, тоже.

Здравствуйте, AlexRK, Вы писали:


ARK>Да, нужно, по той причине, что до пользователя может дойти искаженное (случайно или преднамеренно) представление.

Это не решается цифровой подписью или контрольной суммой ? Вроде как с этим особой проблемы и сейчас нет.


>Но промежуточное представление гораздо проще исходной программы, и его верификация, соответственно, тоже.

Если цифровая подпись в порядке, контрольная сумма md5 в порядке (потребовать их обязательную проверку ничего не стоит, демиург же!), то зачем еще верифицировать ?

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>И в какую же сумму ты оцениваешь затраты на то, чтобы превратить MS из фирмы, производящей ПО исключительно на продажу в фирму, которая делает что-то по заказу ?

Придлагаю оффтоп закончить, а то мы уже совсем в дебри ушли.

Здравствуйте, WolfHound, Вы писали:

WH>Зачем JIT? JIT не нужен. Кто мешает компилировать при установке приложения?

В натив ? А почему сразу нельзя?

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Здравствуйте, samius, Вы писали:

S>>а) соглашаться на бог знает что.

PD>Рухнет ведь.
максимум — зависнет. Поначалу.

S>>б) высаживать приложение с недоказанной корректностью на другую машину.

PD>Это ты пользователю скажи. Дескать, вот тебе одни программы, а вот другие. Купи 2 машины (заплати двойные деньги), ну а мы, так и быть, поможем тебе по сети организовать их взаимодействие. Если, конечно, при передаче по сети плохая машина не передаст что-то плохое хорошей машине . Зато будет статическая верификация.
Лучше я скажу это, чем то, что никаких гарантий надежности нет и не закладывалось на уровне выбора ЯП в пользу мощности, и то что для выполнения программ, требующих надежности, нет вообще ни одного гарантированного способа их выполнить без утечки.

S>>в) переходить на многопроцессорные машины и гонять программы с разным клеймом на физически разных процессорах.

PD>Хм, а в чем отличие от многоядерности на одном процессоре ? Только кеши изолированы, а память-то нет.
Да, пардон, я думал что проблема с кэшами.

Здравствуйте, samius, Вы писали:

PD>>Рухнет ведь.
S>максимум — зависнет. Поначалу.

Хрен редьки ...

S>>>б) высаживать приложение с недоказанной корректностью на другую машину.

PD>>Это ты пользователю скажи. Дескать, вот тебе одни программы, а вот другие. Купи 2 машины (заплати двойные деньги), ну а мы, так и быть, поможем тебе по сети организовать их взаимодействие. Если, конечно, при передаче по сети плохая машина не передаст что-то плохое хорошей машине . Зато будет статическая верификация.
S>Лучше я скажу это, чем то, что никаких гарантий надежности нет и не закладывалось на уровне выбора ЯП в пользу мощности, и то что для выполнения программ, требующих надежности, нет вообще ни одного гарантированного способа их выполнить без утечки.

Да живем же как-то без всего этого. И 0 кольцо вполне изолировано, да и в 3 кольце определенная изоляция по UAC есть. А ты нагородил огород, заставил пользователя вторую машину покупать, а теперь заявляешь — никаких гарантий надежности нет. Что-то все это крайне сомнительно, чтобы могло взлететь.

Здравствуйте, lpd, Вы писали:

lpd>Зачем может понадобиться заменять систему команд процессора?
Чтобы процессор работал быстрее.

lpd>У нас регулярно появляются принципиально новые процессорные архитектуры, которые в разы быстрее и лучше предыдущих?
Так по тому и не появляются что невозможно перетащить на эти процессоры все программы.

lpd>Сложно скомпилировать программу под все нужные процессоры?
Одну нет.
А вот все программы невозможно.

lpd>Лично я бы запретил распространять программы в промежуточных кодах, т.к. это усложняет и запутывает развертывание без значительной пользы.
Это просто противоречит вообще всему.
В случае с промежуточным кодом у тебя один бинарник который работает везде.
В случае с нативом у тебя процессор * ОС.