Здравствуйте, smeeld, Вы писали:
S>Вам не кажется, что слишком многого хотите от компилятора? Организация логики исполнения и контроль S>соответствия ей во время исполнения-это прямая обязанность программиста, а не компилтора. На уровне CPU S>есть только набор инструкций, и компилятор занимается только тем, что переводит текст проги в последовательность S>этих инструкций. Ваше же требование заключается в том, чтоб компилятор, не много ни мало, придумывал логику исполнения.
Нет, требование совершенно не в том, чтобы компилятор придумывал логику исполнения.
И компилятор обычно занимается не только переводом кода из одного представления в другое. Он еще и запрещает реализацию логики исполнения, неправильной в каком-то смысле. Например, контроль типов — если передаваемый тип данных не соответствует требуемому, компилятор выдает ошибку.
Мое (гипотетическое) требование в том, чтобы компилятор запрещал компиляцию кода, содержащего неоткатываемые участки в границах некоторой транзакции. Из этого требования вытекает необходимость формализации терминов "транзакция", "откатываемый код", "неоткатываемый код" и т.п.
Вот видите, а вы говорите — все просто. MOV сделал и вуаля.
Здравствуйте, AlexRK, Вы писали:
ARK> Он еще и запрещает реализацию логики исполнения, неправильной в каком-то смысле. Например, контроль типов — если передаваемый тип данных не соответствует требуемому, компилятор выдает ошибку.
Это не контроль корректности логики исполнения, а контроль соответсвия стандарту ЯП. Две вообще разные сущности.
ARK>Мое (гипотетическое) требование в том, чтобы компилятор запрещал компиляцию кода, содержащего неоткатываемые участки в границах некоторой транзакции. Из этого требования вытекает необходимость формализации терминов "транзакция", "откатываемый код", "неоткатываемый код" и т.п.
Это нужно добавлять специальное подмножество в ЯП. Приблизительно то же саоме, что и параллелизация с OpenMP,
директивами # pragma omp... Что то вроде-#pragma transaction..... что будет заставлять компилятор генерить некоторый
шаблонную схему обмена данными, соответсвующей логике транзакций.
ARK>Вот видите, а вы говорите — все просто. MOV сделал и вуаля.
Прочитайте лучше, чо писал выше, MOV есть сама перекидка данных в/из устройства, этой операции должно будет
предшествовать множество иных операций в рамках процесса определения необходимости/возможности совершения
операции MOV, и являющееся частью реализации логики транзакционной модели взаимодействия с устройстовом.
Здравствуйте, AlexRK, Вы писали:
ARK>Но как же быть, если от вывода зависит, например, ввод в той же транзакции? Скажем, сперва что-то выводим на экран, а потом ждем реакции юзера — все в одной транзакции. Получается, такой сценарий работать не будет.
Ввод или форсирование записи (в виде барьерной инструкции) в данный момент тоже будет вызывать откат транзакции.
Ну и общая идея в том, чтобы транзакции таки не были слишком длинными.
ARK>Выходит, некие ограничения с ИО все же присутствуют. Насколько можно их формализовать — непонятно.
Не надо ничего делать — всё уже сделано. Даже сейчас для гарантированного инициирования IO нужно поставить инструкцию mfence, чтобы гарантировать правильный глобальный порядок записи. В случае с транзакциями инструкции mfence вызывают откат.
Здравствуйте, Mamut, Вы писали:
M>А кто виноват? Да вот те же Линус сотоварищи, винда и прочие МакОСи. Даже если тот же Линукс будет сидеть на 256 ядрах, это ничего никому не даст. Весь инструментарий, все библиотеки, все языки программирования, весь GUI как был, так и остается однопоточными. А те из языков, что не однопоточные, имеют прекрасные GIL или мьютексы, что тоже хорошему параллельному коду не способствуют.
Не надо вот так нормальные среды пинать. Zing JVM спокойно работает на тысяче процессоров и их GC масштабируется без проблем и на бóльшие объёмы. Естественно, полностью параллельно и конкурентно.
Здравствуйте, smeeld, Вы писали:
S>Это не контроль корректности логики исполнения, а контроль соответсвия стандарту ЯП. Две вообще разные сущности.
Это то же самое, но с другой точки зрения. В любом случае первичен контроль логики исполнения.
Мало того, существуют компиляторы, которые производят кучу дополнительных проверок, помимо "стандарта языка".
S>Это нужно добавлять специальное подмножество в ЯП. Приблизительно то же саоме, что и параллелизация с OpenMP, S>директивами # pragma omp... Что то вроде-#pragma transaction..... что будет заставлять компилятор генерить некоторый S>шаблонную схему обмена данными, соответсвующей логике транзакций.
Да, я как раз об этом и говорил ранее, когда начался разговор о границах транзакций.
Здравствуйте, AlexRK, Вы писали:
ARK>Это то же самое, но с другой точки зрения. В любом случае первичен контроль логики исполнения. ARK>Мало того, существуют компиляторы, которые производят кучу дополнительных проверок, помимо "стандарта языка".
Повторюсь, что у компилятора нет никаких способов контролировать логику исполнения определяемую алгоритмом.
Он следит только за ЯП, плюс дополнительные проверки, связанные с безопасностью или производительностью в форме
контроля за набором параметров, множество которых расписано разрабами компилятора. Это сущности,
связанные с свойствами генерации кода и его исполнения, и не имеющие никакого отношения к алгоритмам,
которые реализует конечный код. Логика исполнения же-это сущность относящаяся к алгоритмам. Последнее полностью
в зоне ответственности прикладного прогера, и не получится внедрить в компилятор механизмы проверки корректности
любого возможного алгоритма, который только может придумать прикладной прогер, это, повторюсь, будет уже Artificial Intelligence.
Контроль может быть только на уровне контроля за корректностью проведения некоторых операций в данном участке кода, в составе
реализации алгоритма, при явном задании для компилятора необходимости проводить такую проверку. Но это уже явно категория
специализированных конструкций ЯП, типа #pragma ...
C>Не надо вот так нормальные среды пинать. Zing JVM спокойно работает на тысяче процессоров и их GC масштабируется без проблем и на бóльшие объёмы. Естественно, полностью параллельно и конкурентно.
C>Так что можно, если немножко захотеть.
Zing is priced on a subscription basis per server. With per-server pricing, you don’t need to worry about core counts, memory size, or number of instances deployed per server. The annualized subscription price for Zing per physical server ranges from $3500 (for several hundred servers) to $7500.
Дешевле Erlang тогда взять.
Ну из-за того, что есть один Zing JVM и одна Erlang VM, общая суть не меняется.
Здравствуйте, smeeld, Вы писали:
S>Повторюсь, что у компилятора нет никаких способов контролировать логику исполнения определяемую алгоритмом.
Это не так.
http://en.wikipedia.org/wiki/Program_analysis http://en.wikipedia.org/wiki/Correctness_%28computer_science%29
S>Он следит только за ЯП, плюс дополнительные проверки, связанные с безопасностью или производительностью в форме S>контроля за набором параметров, множество которых расписано разрабами компилятора. Это сущности, S>связанные с свойствами генерации кода и его исполнения, и не имеющие никакого отношения к алгоритмам, S>которые реализует конечный код. Логика исполнения же-это сущность относящаяся к алгоритмам. Последнее полностью S>в зоне ответственности прикладного прогера, и не получится внедрить в компилятор механизмы проверки корректности S>любого возможного алгоритма, который только может придумать прикладной прогер, это, повторюсь, будет уже Artificial Intelligence.
Контроль правильности использования контрактов каналов в Singularity — это контроль логики исполнения?
А как насчет Typestates?
А теперь ссылки на то, как эти бредни скинтистов воплощены в конкретных компиляторах, желательно, в
GCC или LLVM, чтоб ссылки были на файлы с исходниками, а то в теориях, знаете ли, и что такое вселенная
известно, в каждой по своему, а в CS так вообще насочиняли бреда, которое к реальному железу отношения не
имеет, а для воплощения в программной реализации оно слишком отдалено от конретных задач, для каждой из который
правильней будет придумывать схемы и алгоритмы для каждой задачи самостоятельно, (что и делатется всеми практикующими
разработчиками) а не рыться в тоннах бреда, насочинённого скинтистами.
ARK>Контроль правильности использования контрактов каналов в Singularity — это контроль логики исполнения? ARK>А как насчет Typestates?
Не нужно википедий, там сочиняют все кому не лень, приведите ссылки на спеки существующих интерфейсов периферийных
устройств, CPU, в которых были бы прописаны реализованные механизмы контроля логики исполнения транзакционной модели
на их уровне, а не на уровне алгоритма прикладной программы.
Здравствуйте, smeeld, Вы писали:
S>А теперь ссылки на то, как эти бредни скинтистов воплощены в конкретных компиляторах, желательно, в S>GCC или LLVM, чтоб ссылки были на файлы с исходниками, а то в теориях, знаете ли, и что такое вселенная S>известно, в каждой по своему, а в CS так вообще насочиняли бреда, которое к реальному железу отношения не S>имеет, а для воплощения в программной реализации оно слишком отдалено от конретных задач, для каждой из который S>правильней будет придумывать схемы и алгоритмы для каждой задачи самостоятельно, (что и делатется всеми практикующими S>разработчиками) а не рыться в тоннах бреда, насочинённого скинтистами.
Demonstration of functional correctness
— Well-defined criteria
— Automated and/or model-based testing
— Formal techniques: model checking, theorem proving
Satisfaction of non-functional requirements
— No crashes due to runtime errors (division by zero, invalid pointer accesses, overflow and rounding errors)
— Resource usage
--- Timing requirements (e.g. WCET, WCRT)
--- Memory requirements (e.g. no stack overflow)
На сайте есть примеры реальных проектов (авиационное ПО).
S>Не нужно википедий, там сочиняют все кому не лень, приведите ссылки на спеки существующих интерфейсов периферийных S>устройств, CPU, в которых были бы прописаны реализованные механизмы контроля логики исполнения транзакционной модели S>на их уровне, а не на уровне алгоритма прикладной программы.
Я не знаю, есть ли что-то подобное для контроля логики транзакций. Именно поэтому я и спросил в начале разговора про сценарий с IO.
Как я понял из ответов, того, о чем я спрашивал, нет.
Интерфейсы периферийных устройств меня не интересуют, меня интересует корректное программирование.
Здравствуйте, AlexRK, Вы писали:
ARK>Ну вот пример реализации того, что вы называете "бреднями скинтистов" (с) ARK>http://www.astree.ens.fr/
Мне не нужны буклеты презентаций, мне нужны исходники, потому что всё вот это
Programm_analysis, Correctness(computer science) etc.
и прочее подобное, красиво звучащее и описываемое в теоретических сочинениях, в конкретных реализация, насколько знаю по просмотрам,
исходников GCC и LLVM, сводится к упомянутому
проверки, связанные с безопасностью или производительностью в форме контроля за набором параметров,
множество которых расписано разрабами компилятора.
Контроль может быть только на уровне контроля за корректностью проведения некоторых операций в данном участке кода, в составе
реализации алгоритма, при явном задании для компилятора необходимости проводить такую проверку.
Прикол в том, что строгой математической теоретической базы под Programm_analysis, Correctness(computer science) etc.
не существует, они представляю собой пространные рассуждения, коих насочинять можно сколько угодно. И в конкретных реализациях
всё сводится к самым что ни на есть
проверки и соответствия, связанные с безопасностью или производительностью в форме контроля за набором параметров, взаимосвязаных (графы или какие иерархические построения)или нет, множество которых расписано разрабами компилятора.
Здравствуйте, smeeld, Вы писали:
S>Мне не нужны буклеты презентаций, мне нужны исходники, потому что всё вот это
Ну, исходники доступны не для всего. Где исходники Windows 7, Oracle DBMS? Это не значит, что их не существует.
Вот есть опенсорсный анализатор, можете глянуть, если интересно: http://frama-c.com/download.html
Но там все на ML. И мне неизвестно, выполнялись ли на нем какие-то реальные проекты.
Вот еще индустриальный компилятор с исходниками: http://libre.adacore.com/download/
Надо мыло вводить, я сам не пробовал.
S>и прочее подобное, красиво звучащее и описываемое в теоретических сочинениях, в конкретных реализация, насколько знаю по просмотрам, S>исходников GCC и LLVM, сводится к упомянутому
GCC и LLVM, насколько мне известно, обладают весьма скудными возможностями статического анализа.
SPARK, ссылку на который я выше привел, анализирует гораздо больше. Но там язык Ada, а не C/C++.
А вообще все это уже очень далеко от параллелизма. Я, в принципе, получил ответ на свой изначальный вопрос. Будем ждать дальше, пока не появится что-то более вменяемое, чем существующие механизмы работы с транзакциями (на высоком уровне).
U>The whole "let's parallelize" thing is a huge waste of everybody's time. There's this huge body of "knowledge" that parallel is somehow more efficient, and that whole huge body is pure and utter garbage. Big caches are efficient. Parallel stupid small cores without caches are horrible unless you have a very specific load that is hugely regular (ie graphics).
U>И он прав. Разговоры про большое значение multi core и парралелизм были ещё в 2005 году на моей памяти. Саттеровские "free lunch is over" and shit предсказывали, что через 10 лет мы все будем сидеть толстой задницей на 256 корах. Нифига этого не случилось. А что случилось? Как раз таки что Линус говорит:
дедуля просто не в курсе как это заставить работать.
у нас, например, на работе десктопы испольются по своему правильному назаначению — как терминалы доступы к "нормальным машинам"
Здравствуйте, Mamut, Вы писали:
M>Дешевле Erlang тогда взять. M>Ну из-за того, что есть один Zing JVM и одна Erlang VM, общая суть не меняется.
Меняется. Мы видим, что такая масштабируемость вполне доступна. Причём её делают легкодоступной вполне себе прикладным программистам.
M>>Дешевле Erlang тогда взять. M>>Ну из-за того, что есть один Zing JVM и одна Erlang VM, общая суть не меняется. C>Меняется. Мы видим, что такая масштабируемость вполне доступна. Причём её делают легкодоступной вполне себе прикладным программистам.
Слишком медленно Отсюда и разочарование у некоторых Ну а для того, чтобы ОСи к этому подтянулись — ууу...
Здравствуйте, __kot2, Вы писали:
__>дедуля просто не в курсе как это заставить работать. __>у нас, например, на работе десктопы испольются по своему правильному назаначению — как терминалы доступы к "нормальным машинам"
А до внучеков не доходит, что дедуле и его свите по барабану десктопы, и всегда так было, что дедуля всегда развивал
масштабную движуху в среде разрабов в направлении развития Linux для того, чтоб вывести Linux, по показателям,
в ОС номер один для запуска прежде всего этих самых "нормальных машин". То, что "родные Unix" и прочие z/OS были потеснены
Linux-ом на этом фронте, известно, и дедуля желает вообще вышвырнуть родные благородные ОСя c "нормальных машин" и утвердить
на них Linux целиком и полностью, как это уже сделано на "почти нормальных машинах" aka midrange servers.
ЗЫ Внучеки, такие внучеки, думают что их песочница с песчаными пирамидками-вершина hi-tech-а, а, летающие вокруг на сверхзвуке ракеты,
так, отживающие кряхтения старых глупых дедуль.
Здравствуйте, smeeld, Вы писали: S>ЗЫ Внучеки, такие внучеки, думают что их песочница с песчаными пирамидками-вершина hi-tech-а, а, летающие вокруг на сверхзвуке ракеты, S>так, отживающие кряхтения старых глупых дедуль.
я ниче не понял если честно
мне вообще глубоко по барабану какая операционка стоит. у них у всех есть недостатки.
летания на ракете это про сайтики, чтоли? конечно, там все в io упирается. там вообще процессор не нужен
Здравствуйте, __kot2, Вы писали:
__>мне вообще глубоко по барабану какая операционка стоит. у них у всех есть недостатки. __>летания на ракете это про сайтики, чтоли? конечно, там все в io упирается. там вообще процессор не нужен
И ещё все внучеки как один уверены что Linux нигде кроме веб серваков не используется.
Для примера напомню, что БАК (тот, который коллайдер) на Linux целиком и полностью.
И про top500 промолчу, ибо уже аскомина, но внучеки то, похоже, и не знают.
Здравствуйте, smeeld, Вы писали: S>И ещё все внучеки как один уверены что Linux нигде кроме веб серваков не используется. S>Для примера напомню, что БАК (тот, который коллайдер) на Linux целиком и полностью. S>И про top500 промолчу, ибо уже аскомина, но внучеки то, похоже, и не знают.
а я и не про Линукс, я про то, где все упирается в размер кэша и io. просто хранение-пересылка данных.
