[d | b / bro / ci / cu / dev / gf / hr / l / m / med / mi / mu / o / ph / r / s / sci / tran / tu / tv / x | es / vg | au / tr | a / aa / abe / c / fi / jp / rm / tan / to / ts / vn / vo]
[Burichan] [Futaba] [Gurochan] - [iiChantra] [Радио 410] [ii.booru-Архив РПГ] [acomics-cf-ost] [Cirnoid] [@] - [Архив - Каталог] [Главная]

[Назад]
Ответ
Leave these fields empty (spam trap):
Имя
Тема
Сообщение
Файл
Подтверждение
Перейти к [
Пароль (для удаления файлов и сообщений)
 
ЗАПРЕЩЕНО:
  • детская эротика/порнография
  • троллинг
 
  • Поддерживаются файлы типов GIF, JPG, MP4, OGV, PNG, WEBM размером до 4096 кБ.
  • Максимальное количество бампов треда: 500.
  • Всем посетителям рекомендуется ознакомиться с FAQ.

1558768530062.jpg - (1096 KB, 2064x1548, 20190525_090724.jpg)  
1096 KB №208496   #1

5ггц это предел развития процессоров на ближайшие 10-15 лет, дальше только 9999 ядер.
Что думаешь, Чи?

>> №208497   #2

>>208496
Квантовые компьютеры

>> №208498   #3

>>208497
Еще даже оптические в обиход не ввели...

>> №208499   #4

>>208498
Бывает. А пока стак ядер.

>> №208500   #5

>>208496
Я думаю, что софт надо писать лучше. Есть огромный потенциал в развитии инструментов для софта:

  • можно писать доказуемые программы
  • доказуемые программы можно продавать без поддержки с открытым исходным кодом
  • программы с отцрытыми исходниками можно интегрировать более тесно, компилировать под конкретное железо
>> №208502   #6

>>208500

> доказуемые программы

Што?

> продавать без поддержки с открытым исходным кодом

Што?

> программы с отцрытыми исходниками можно интегрировать более тесно, компилировать под конкретное железо

Ммм и получится так же криво как gimp под Windows с тупостями, которые не исправляются годами и годами?

Давай начистоту: из опенсорсного софта хорошего единицы, все остальное - большая свалка.

>> №208503   #7

>>208500

> можно писать доказуемые программы

Попахивает алгоритмической неразрешимостью в общем случае.

>> №208505   #8

>>208500

>Я думаю, что софт надо писать лучше.

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

>> №208506   #9

>>208500
Если бы софт грамотно писали, так бы на 640 килобайтах все и сидели. Тебе это надо? Никому не надо. Чем большему числу людей чувствительное место максимально выкрутят - тем выше шанс что чтото сделают нового в плане технического прогресса.

>> №208513   #10

>>208496

> 5ггц

Офигеть до чего техника дошла.
Пишу с 2х ядер по 2,2.

>> №208514   #11

>>208513
Помниться сидя в детстве на 1800мгц семпроне мечтал о 5ггц пентиуме, при том, что они были на 1 ядро, а теперь у меня в одной маленькой пластинке 8 пентиумов по 5ггц. Жаль только детство уже не вернуть. Тогда даже консоль на 8 бит, чернобелый тетрис и игрушка тамагочи казались вершиной счастья, не нужен был даже весь этот йоба графон.

>> №208518   #12

>>208513
И он ещё жалуется! Если начнём мерится кто с чего пишет, боюсь что даже я окажусь в аутсайдерах.

>> №208525   #13

>>208496
На 5- или 3-нанометровом техпроцессе индустрия перейдёт на другой полупроводниковый материал вместо кремния (индий-сурьма, может быть, или старый добрый арсенид галлия, или что-то ещё). Может, увидим и 100 ГГц, если придумают, как недорого производить оперативную память с адекватной таким процессорам быстродействием.

>> №208528   #14

>>208525
Либо начнут набирать популярность материнские платы с несколькими сокетами.
Процессор припаян — самый низкий ценовой сегмен.
1 сокет — бюджетный вариант.
2 сокета — средний.
И т.д.

>> №208531   #15

>>208528
Когда то очень давно так и было. Ядра бракованные и так сейчас на кристаллах блокируют. Может быть будут сразу по 20-30 пихать и продавать как 9-ядерные.

>> №208562   #16

>>208502

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

Нупонятн.

>Ммм и получится так же криво как gimp под Windows с тупостями, которые не исправляются годами и годами?

Я сказал "доказуемые программы". Гимп таковой не является.
>>208503
Большинство достижений человека алгоритмически недостижимы. Доказуемость не обязана быть автоматической.
>>208505
Никакие человеческие ресурсы не компенсируют недостатки инструментов.
>>208506
Речь идёт именно о том, что все практически полезные рубежи уже взяты. Теперь нужно.

>> №208563   #17

>>208500

>можно продавать без поддержки с открытым исходным кодом

/0
Продажи продуктов с открытым исходным кодом из продажи поддержки и состоят.

>> №208564   #18

>>208563
То есть, тебя не радует то, что целый класс рабочей силы будет свободен и может быть пущен на другие цели? Что люди больше не будут портить здоровье?

>> №208565   #19

>>208564
Может, ещё умирать не нужно будет?

>> №208567   #20

>>208565
Давай с простого начнём, там посмотрим.

>> №208571   #21

>>208564

>целый класс рабочей силы будет свободен

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

>> №208572   #22

>>208562
То что у кого то много раз не получилось, не означает что это невозможно. Я бы возразил конкретнее, но чтобы доказать свою правоту нужно сперва добиться. В данном конкретном случае добиться всего возможного.
>>208563
Продать можно что угодно. Даже снег эскимосу.

>> №208590   #23

>>208562

> Я сказал "доказуемые программы".

Что такое доказуемые программы?

>> №208592   #24

>>208497
Большие обещания для задач лишь одной области.

>> №208594   #25

>>208528

>Процессор припаян — самый низкий ценовой сегмен.

Телефоны-ноутбуки.

>1 сокет — бюджетный вариант.

Простые пеки, которые теперь только яумамыпрограммистам нужны.

>2 сокета — средний.

Серверы начального уровня.

>> №208595   #26

>>208571
Я вижу проблему в том, что люди не могут выращивать/добывать еду сами, если они не выживают в городе. Это я тоже обдумываю.
>>208572

>То что у кого то много раз не получилось, не означает что это невозможно. Я бы возразил конкретнее, но чтобы доказать свою правоту нужно сперва добиться. В данном конкретном случае добиться всего возможного.

Скажи поточнее, пожалуйста. Не уверен в том, что понимаю тебя.
>>208590
Доказуемо верные программы - это программы со определёнными входными данными, определёнными выходными данными, характеристиками видимых эффектов (ресурсоёмкость, защита от side channel-атак и прочее) и использующие математически определённое железо. Имея такое ТЗ можно написать программу и доказать её соответствие ТЗ, приняв характеристики железа, как аксиому. Баги в железе - отдельная тема. Если все программы, выполняемые на железе, верны, то с их помощью можно искать баги железа.
Есть много доказуемо правильных алгоритмов, но пока что нет инструментов для написания сложного доказуемо верного кода, и все популярные языки программирования не определены полностью и не всегда непротиворечивы.
Надеюсь, не очень сумбурно объясняюсь.

>> №208598   #27

>>208595
Так и представил математически доказуемый MS Word с определёнными входами и выходами.

>> №208599   #28

>>208598
Рад за тебя.

>> №208601   #29

>>208599
Что же за тебя нельзя порадоваться?

>> №208602   #30

>>208601
Отчего же? Радуйся. Работа есть, теперь я свою блажь воплотить могу даже.

>> №208605   #31

>>208514

> мечтал о 5ггц пентиуме, при том, что они были на 1 ядро

Они разве не до 3-х с небольшим максимум были?

>> №208613   #32

>>208605
Неправильно выразился, да. Просто 5 ггц казалось супер недостижимой величиной.
>>208525

>Может, увидим и 100 ГГц, если придумают,

Даже если бы придумали сейчас, маркетологи бы растягивали по 100-200мгц на каждое тик-так, чтобы выжать побольше денег с покупателей, так что это маловероятно.

>> №208615   #33

>>208613

>маркетологи бы растягивали по 100-200мгц на каждое тик-так, чтобы выжать побольше денег с покупателей

Так выпусти продукт быстрее чем те, которые растягивают, и завоюй рынок.

>> №208616   #34

>>208615
Для примера. Есть такой видеоредактор как VirtualDub. Он конвертирует видео со скоростью света. Как только автор от него устал, тот моментально устарел. Более кошерный мод даже быстрее. Да и до этого предпочитали FFmpeg, Sony Vegas и Adobe After Effects использовать. С графическими редакторами всё то же самое. Я сам предпочитаю использовать ненавистные продукты Adobe даже чтобы сохранить из буфера картинку. Хотя есть Paint. Если завтра кто выпустит аналог фотошопа размером с мегабайт, все посмеются и забудут. Может быть парочка особо тяжёлых неадекватов начнут пользоваться.

>> №208617   #35

>>208616
Это потому что лично у тебя пиратство выключило нормальные механизмы конкуренции в программном обеспечении. Если бы тебе нужно было заплатить полтысячи долларов за фотошоп и After Effects как профессиональные продукты, коими они являются, то ты бы не использовал их для сохранения картинок.
В физическом мире это все-таки работает на данный момент иначе — даже при всей маркетинговой раскрученности какого-нибудь айфона у всяких самсунгов, хуавеев и прочих китайфонов от китайской армии находится огромное количество пользователей.

>> №208620   #36

>>208615
Может тебе еще варп двигатель из палок и камней собрать?

>> №208622   #37

>>208620
Кстати, видел где то любопытный пример, как из них собрали то ли радиопередатчик, то ли радиоприёмник. И по моему там всё же какие то специальные специально обработанные материалы были. Пусть и неандертальским способом. Понятия не имею как это гуглить.

>> №208775   #38

>>208496
EE почти до 4 тянули по спекам.

>> №208776   #39

https://ark.intel.com/content/www/us/en/ark/products/27510/intel-pentium-4-processor-supporting-ht-technology-4-00-ghz-2m-cache-1066-mhz-fsb.html

Вот, 4. Но Атлону всё равно продувал.

>> №208803   #40

>>208496

>Что думаешь, Чи?

Думаю, что пора переходить с кремния на арсенид галлия.
Ну есть ещё VLIW, но массовое применение ему не найдётся. Больше для промышленной автоматики, числодробилок, САПР, ЦОС. Сейчас куча управляемого кода (скриптовые языки, JVM, .Net) и на таких процессорах он работает куда хуже, чем на RISC. Ну и боль и унижение при разработке компилятора (в МЦСТ, например, отделение компиляторов и языков программирования одно из самых больших).
А так - ещё специализированные процессора и ускорители.

>> №208804   #41

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

>> №208892   #42

>>208500

> можно писать доказуемые программы

Это какая-то функциональная лабуда?

> программы с отцрытыми исходниками можно интегрировать более тесно

Вот ычую! Было бы просто прекрасно, если бы программы умели намного плотнее взаимодействовать друг с другом. Например, регистрировать в системе что-то вроде потоков данных или протоколов, которые можно было бы прозрачно использовать из других программ. Что-то вроде развития идеи KParts, но более универсальное и пронизывающее всю систему. Или даже чтобы вообще можно было обойтись без обособленных программ, и вместо них компоновать произвольные комбинации из потоков данных и инструментов для их обработки. Или как-то так.

>> №208898   #43

>>208892

>Вот ычую! Было бы просто прекрасно, если бы программы умели намного плотнее взаимодействовать друг с другом.

Напиши Леннарту. Пусть интегрирует системд с гимпом и либраоффисом.

>> №208902   #44

>>208892

> Было бы просто прекрасно, если бы программы умели намного плотнее взаимодействовать друг с другом.

Это называется Win32 API, и это давно существует. Ты давно можешь перекидывать данные из одной программы в другую, вызывать сторонние функции из своей программы, ставить ловушки на события чужих программ. Только майки сейчас стали бодренько это закапывать под соусом борьбы за безопасность. Нелегко поймать событие, если каждая программа сидит в своей песочнице и ничего вокруг не видит. Да еще и документирование API практически свернули и вырвали справки из всех программ.
Хрен его знает, нахрена такое майкам. Полагаю, чтобы не оставлять без работы толпы индусов, пишущих копеечные узкоспециализированные программы. Ушел Билл и все стало разваливаться.
>>208500

> программы с отцрытыми исходниками можно интегрировать более тесно,

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

>> №208903   #45

>>208892>>208902
В данном конкретном случае я с ними полностью согласен. Вам вирей мало? Кому в здравом уме может понадобиться, чтобы программы произвольно вмешивались в работу друг-друга? Тоже за здоровую бессмысленную и беспощадную кровавую конкуренцию дофига, простите за выражение? А я вот за абсолютную беспросветную изоляцию и тотальное доминирование овервизора OS. Прямое бесконтрольное взаимодействие программных компонентов такой же рудимент как полная инициализация или упаси боже даже компиляция приложения при каждом запуске. У каждой программы как у каждого червячка должен быть вход и выход как у конвейера. И нечего им дозволять друг-другу под капот лезть чтобы без спроса кровеносные системы переплетать. Есть публичная зона и есть приватная.
>>208902
Закапывать живьём свои разработки - древняя традиция миркософта, которой они ещё ни разу не изменяли.

>> №208904   #46

Это точно. Современная индустрия программирования, она такая.

>> №208905   #47

>>208500

>• можно писать доказуемые программы

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

>>208525

>На 5- или 3-нанометровом техпроцессе индустрия перейдёт на другой полупроводниковый материал вместо кремния (индий-сурьма, может быть, или старый добрый арсенид галлия, или что-то ещё).

Уже давно есть HEMT, гетеробиполярные транзисторы, резонансно-туннельные диоды и прочие структуры, могущие в частоты до сотен ГГц, гетеробиполярные транзисторы SiGe даже делаются в составе смешанных цифровых и СВЧ узлов вроде WiFi адаптеров на 5ГГц на одном кристалле.
Процессоры на эти новые материалы и структуры никогда не перейдут - у всех новых материалов большая подвижность электронов и худшая у дырок. Не получится аналог CMOS с нулевым статическим потреблением и устойчивым состоянием с возможностью к выходу одного элемента подключить входы большого количества других, а значит накроется медным тазом возможность лепить миллиарды простаивающих большую часть времени блоков и сопроцессоров, конвейера, регистровые файлы и кеши адекватных размеров, все то что двигало прогресс в процессоростроении в последние десятилетия, будет откат назад до времён машин на мелкой ЭСЛ-логике, сотен киловатт потребляемой мощности и прочих радостей, только ещё добавится адовая сложность учёта задержек распространения сигналов по логическим составляющим такого ЦП и СВЧ-соединений тысяч чипов между собой (при частоте в 300ГГц длина волны 1мм, уже даже распространение ее в кристалле потребует учета).
Короче, мы заперты в кремнии, и выйдем из него только вместе со смертью массового применения тьюрингоподобных машин, например, если какой-нибудь другой принцип позволит медленно, но очень объемно аппаратно реализовывать нейросети и это станет выгоднее их симуляции в софте.

>> №208906   #48

>>208905
Нынешние нейросети в лучшем случае реализуются через наложение матриц.

>> №208907   #49

>>208903

> Вам вирей мало?

А я вот за запуск только проверенного кода. И современные числодробилки вполне могут это обеспечить, причем сразу несколькими способами. Зачем оборачивать код несколькими слоями защиты, если можно тупо его проверить? Опасность недокументированных уязвимостей? Так вы пишите код нормально, без дырок! Да и не спасают все эти обертки, если они изначально сделаны из дырявых штук.

>> №208908   #50

>>208892

> Что-то вроде развития идеи KParts, но более универсальное и пронизывающее всю систему.

D-Bus же.
>>208905

> любой ввод-вывод в реальный мир

С точки зрения теории ввод-вывод в реальный мир — просто ещё одна пара аргументов у функций. Если ты имеешь в виду, что поведение реального мира может отличаться от поведения его модели, то эта проблема не отменяет полезности доказательств.

> у всех новых материалов большая подвижность электронов и худшая у дырок

В том числе и у углеродных нанотрубок?

> миллиарды простаивающих большую часть времени блоков

Какие миллиарды блоков? Транзисторов-то не так давно миллиарды стало на одном кристалле.

> нулевым статическим потреблением и устойчивым состоянием

Зачем их полностью отключать от сигнала тактового генератора, если можно будет вместо этого заставить их работать на пониженной частоте, например на 5 ГГц?

>> №208909   #51

>>208908

>С точки зрения теории ввод-вывод в реальный мир — просто ещё одна пара аргументов у функций.

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

>В том числе и у углеродных нанотрубок?

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

>Какие миллиарды блоков? Транзисторов-то не так давно миллиарды стало на одном кристалле.

Пусть будет миллиарды ячеек памяти. Порядок величины не столь важен, так как альтернативы вроде арсенид-галлиевых полевых транзисторов с затвором Шоттки на порядков 5-6 менее плотны, иначе статическое потребление их просто расплавит.

>Зачем их полностью отключать от сигнала тактового генератора,

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

>> №208910   #52

>>208892

>Что-то вроде развития идеи KParts, но более универсальное и пронизывающее всю систему

Штука была сколь офигенная, столь и бесполезная. Не, кусок Амарока в Крусейдере — это было, конечно, вау прям как в Windows XP с WMP и IE, но какого-то реально толкового применения ей я за несколько лет сидения в третьекедах не нашёл. Меня как-то не парило переключить окно или рабочий стол тем более что уж что-что, а KWin, конечно, был тогда великолепен
Может, у Чии есть истории успеха с KParts?

>> №208911   #53

>>208907
А я может быть вообще строго за асемблер. Но писать будут индусы. Так то и в некоторых деревнях двери держали открытыми и позволяли другим брать что понравится из дома. Попробуй так сделать в интернациональном портовом мегаполисе. И проще сделать по уму 1 охранника, чем гарантировать эталонность каждого случайно заделанного в подвале гражданина. А иначе получим как с колибри с её 3,5 программами. Которые тоже к слову не 100% проверены. Сферических коней в вакууме делать в реальной жизни сложно.

>> №208914   #54

>>208909
Что думаешь о переходе на другой материал подложки, например на сапфир? Будет это в массовых микропроцессорах в 2020-ых?

>> №208915   #55

>>208892

>Это какая-то функциональная лабуда?

Парадигма несколько вторична. Я предполагаю, что функциональные программы доказать проще.
>>208905

>а любой ввод-вывод в реальный мир - это внепрограммные факторы, рушащие всю доказуемость.

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

>А если мы не можем гарантировать корректность корректность внутреннего состояния, то теряют смысл и все последующие выводы.

Запускай три копии, побеждает большинство.

>> №208916   #56

>>208915
Странное у тебя какое то мышление. Любой кто писал программы сложнее привет мир знает, что функциональное ядро там занимает от силы 1%. Остальное интерфейсы взаимодействия с внешним миром и защита от дурака обработчики нештатных ситуаций.

>> №208917   #57

>>208914
SOI уже применяли, например, в AMD K10. Эффект от него хорош в случае планарных транзисторов за счёт упрощения их изоляции, но сейчас переходят на объемные, где польза от него не столь выражена.

>>208915

>Как только будет доказанный софт, можно будет обнаруживать и исправлять или обходить ошибки в железе.

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

>Запускай три копии, побеждает большинство.

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

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

>> №208918   #58

>>208916
Это не данность, это следствие существующей модели взаимодействия ПО и ядра и того, как написаны ядра. Всегда останется лишь ненадёжность сети и дисков, остальное, как мне кажется, можно исключить.
>>208917

>Вероятность ошибки снижается в квадрате, при идеальном выборе большинства

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

>если бы сличение результатов было простой задачей, весь надёжный софт писался бы наймом трех смен индусов, пишущих три разные реализации софтины со сличением результата работы.

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

>> №208919   #59

>>208918

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

Квадрат вероятности одиночной ошибки, в случае независимых реализаций и трёх экземпляров, и выше вплоть до изначальной вероятности при наличии корелляции. Типичный пример корелляции - выбивание сразу нескольких соседних ячеек памяти от космических лучей при размещении запоминаемых данных в соседних областях.

>Если у тебя есть доказанная программа,

Ее принципиально не будет в силу несуществования среды для запуска прувера с гарантированной надёжностью.

> зачем тебе ещё две?

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

>> №208952   #60

>>208919

>Типичный пример корелляции - выбивание сразу нескольких соседних ячеек памяти от космических лучей при размещении запоминаемых данных в соседних областях.

Космические лучи имеют намного меньший масштаб, чем размер ячеек. Это не типичный пример.

>Квадрат вероятности одиночной ошибки, в случае независимых реализаций и трёх экземпляров

Игнорируешь мои слова. Вероятность одиночной ошибки и вероятность совпадения результатов при условии возникновения ошибки - совсем разные вещи.

>> №208959   #61

>>208952

>Космические лучи имеют намного меньший масштаб, чем размер ячеек.

При современных размерах транзисторов вторичная ионизация накрывает сразу большое количество соседних транзисторов, в особенности на гамме в много МэВ.
Резервировать приходится на уровне раскидывания по разным секциям кристалла или разным кристаллам.

>Игнорируешь мои слова. Вероятность одиночной ошибки и вероятность совпадения результатов при условии возникновения ошибки - совсем разные вещи.

Разные, но второе к нулю не сводится никаким количеством резервирования.

>> №208966   #62

>>208959
Вероятность ошибки меньшая, чем вероятность падения гигантского метеорита, тебя не устраивает?

>> №208967   #63

>>208919
>>208959
Олсо, не вижу, каким образом написание трёх разных программ поможет тебе гарантированно избежать ошибки.

>Для того чтобы сбои и баги не кореллировали между собой

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

>> №208968   #64

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

>> №208969   #65

>>208968

>Это сводит на нет все теоретические положительные свойства доказуемости.

Какие конкретно? Тред читал?

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

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

>> №208972   #66

>>208969

>Какие конкретно? Тред читал?

Достаточно просто завидеть упоминания доказуемости в контексте реальных программ, чтобы на этом чтение прекратить.

>Мне было бы гораздо проще тебя понять, если бы ты хотя бы какой-нибудь вывод своих суждений делал.

Какой вывод? Любая переменная размерностью n бит имеет 2^n число возможных состояний, любой if или switch множит число полных состояний программы. Оцени число полный состояний даже для чего-то вроде GNU cp, чтобы стала понятна принципиальная нереализуемость такой проверки, и по астрономическому времени на ее прохождение, и по вероятности сбоя проверяющей машины от случайных факторов. А проверять тебе придется все возможные статические состояни, потому что даже при полной детерминированности входных параметров случайные сбои железа могут создавать непредусмотренные самой программой переходы в другие состояния, но доказанная программа должна это уметь корректировать.

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

>> №208976   #67

>>208972
На прямой вопрос ответишь (который ты даже процитировал) - позволю ещё немного меня потролить.

>полных состояний программы

Если я не нашёл этот термин зв 5 минут гугления на русском и английском, он не общеупотребителен. Число "полные" тут точно не лишнее?

>Какой вывод? Любая переменная размерностью n бит имеет 2^n число возможных состояний, любой if или switch множит число полных состояний программы. Оцени число полный состояний даже для чего-то вроде GNU cp, чтобы стала понятна принципиальная нереализуемость такой проверки, и по астрономическому времени на ее прохождение

Оказывается, ты хочешь доказывать программы перебором. Я это не предлагал.

>> №208992   #68

>>208972

>доказанная программа должна это уметь корректировать.

Олсо, это ты так решил.

>> №208994   #69

>>208976

> Число "полные" тут точно не лишнее?

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

>> №209000   #70

>>208994

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

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

>> №209004   #71

>>209000
Математически определенное железо не существует в физическом мире, а ценность - штука по определению количественная, и ты не дал никаких количественных оценок полезности доказуемых практических программ.
Да, тут только сочувствовать.

>> №209179   #72
1562592569537.jpg - (178 KB, 623x629, 1553147753980.jpg)  
178 KB

ОП на связи. Жадная корпорация в 2к19 даже не подарит 8 ядер на 5ггц обычному пользователю. На макс частотах камень в играх троттлит, перегревается, сыпет ошибками. После длительных мучений и плясками с бубном, и всеми сопутствующими настройками биоса, пришлось смириться и скинуть настройки к дефолтным, одно ядрышко на 4.9, остальные 7 на 4.6.

>> №209183   #73

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

>> №209186   #74

Кажется, вот здесь что-то рассказывают про доказательное программирование.
https://whycardano.com/science-and-engineering/ru/#формальная-спецификация-и-верификация

Правда там скорее про доказуемо безопасный протокол...



Удалить сообщение []
Пароль
[d | b / bro / ci / cu / dev / gf / hr / l / m / med / mi / mu / o / ph / r / s / sci / tran / tu / tv / x | es / vg | au / tr | a / aa / abe / c / fi / jp / rm / tan / to / ts / vn / vo]
[Burichan] [Futaba] [Gurochan] - [iiChantra] [Радио 410] [ii.booru-Архив РПГ] [acomics-cf-ost] [Cirnoid] [@] - [Архив - Каталог] [Главная]