Здравствуйте, Куть, Вы писали:
К>У меня 3 вопроса: К>1. Есть ли ошибки в моём доказательстве?
С теоретической точки зрения — нет, все верно. Более того, схожие рассуждения имеют место во многих работах, например у Бишопа и сотоваришей: http://nob.cs.ucdavis.edu/bishop/notes/2008-cse-14/2008-cse-14.pdf По сути, они там приходят к тому, что доказать незащищенность программы (задача, сводимая к проблеме останова) возможно только прогнав ее через все возможные наборы входных данных и контролируя множество конфигураций, в которые при этом входит машина. С инженерной же точки зрения, в подобных рассуждениях мало пользы, поскольку, как уже упомянул Cyberax, в этом случае задача сводится к поиску циклов в графе состояний конечного автомата, количество вершин в котором растет по формуле S^N*X, где S — размер входного алфавита, N — количество доступной памями и X — количество состояний в программе МТ. Поэтому при решении реальных задач анализа кода стремятся максимально огрубить понятие "состояние" с тем, чтобы сократить их возможное количество, не теряя при этом в точности результатов. Как правило, для этого прибегают к группировке схожих состояний по каким-либо признакам и далее рассматривают каждую группу, как если бы это было одно состояние.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
Конечно. Например в анализаторе, разрабатываемом нами, используется символическая интерпретация и частично-конкретное выполнение анализируемого кода для построения графа потока управления, в вершинах которого описываются множества значений всех потоков данных, доступных в данной точке выполнения. По сути, это и есть верхнеуровневый аналог состояния программы. Далее мы строим по этим состояниям формулу достижимости того или иного пути в графе, приводящего к потенциальной уязвимости и решаем ее на SMT-солвере. Из решения такой формулы тривиально генерируется как эксплоит для существующей уязвимости, так и патч, закрывающий ее. Подробнее рассказывал об этом здесь и здесь (запись также есть тут).
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Здравствуйте, Куть, Вы писали:
К>У меня 3 вопроса: К>1. Есть ли ошибки в моём доказательстве?
Нет.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
Конечно.
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Всё. Программа с конечным множеством состояний теоретически может быть проверена на возможность остановки.
Но в реальности программы с конечным множеством состояний не представляют интереса.
Память это не только ОП, но и дисковая память. Последняя у нас потенциально бесконечна.
Кроме того МТ это "устройство" без внешнего ввода. А любой внешний ввод может быть представлен как бесконечная лента "событий".
Поэтому практически любая интерактивная программа, или программа, использующая данные на диске, попадает под проблему останова.
Здравствуйте, Куть, Вы писали:
К>У меня 3 вопроса: К>1. Есть ли ошибки в моём доказательстве?
Нет.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
В общем случае — нет, так как количество состояний для анализа легко может стать больше, чем сможет обработать любой реальный компьютер.
На практике во многих частных случаях — очень полезно, на чём компании типа Coverity и делают бизнес.
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Машина с конечной памятью не является МТ, это намного менее мощная конструкция. Машина с конечным объёмом памяти равномощна конечному автомату.
Здравствуйте, kochetkov.vladimir, Вы писали:
KV>Если для вычисления CounterExample требовалась бы МТ, то классического способа доказать выделенное просто не существовало бы. Однако, для вычисления x ^ n + y ^ n == z ^ n вероятно достаточно и стекового автомата, поэтому мы и имеем 130 страниц, доказывающих по сути, что на любых наборах входных данных этот автомат не достигнет допускающего состояния.
Какая-то хитрость в этих рассуждениях.
Память нам всяко нужна неограниченная (ибо числа x и n могут быть какими угодно большими).
И тут внезапно делается утверждение: "раз мы знаем заведомо останавливающийся алгоритм проверки, то можем обойтись чуть более глупой машиной, чем машина Тьюринга".
Ну раз обошлись более глупой машиной, значит, теорема Ферма к проблеме остановки не привязана.
Вот если бы проблема остановки гласила "любая достаточно заковыристая машина Тьюринга работает непредсказуемо долго", тогда процедура проверки контрпримера стала бы лотереей, а значит, и процедура доказательства стала бы лотереей.
Привет всем!
Недавно читал на хабре статью "Неразрешимые задачи и нижние оценки. Лекция Александра Шеня в Яндексе".
В очередной раз послушал о неразрешимости проблемы остановки. И мне не даёт покоя одна мысль, которой хочу с вами поделиться.
Суть проблемы остановки в следующем: доказано, что не существует программы (Анализатора), которому на вход подаётся программа, а на выходе — true, если программа останавливается и false, если она не останавливается.
Все доказательства неразрешимости проблемы остановки основываются на том, что у программ в распоряжении бесконечная память (бесконечная лента в машине Тьюринга).
Но, если мы требуем от Анализатора конечное время для остановки, и скорость работы Анализатора так же конечна, то логично было бы потребовать от программ работать с конечной памятью.
А с конечной памятью проблема останова становится разрешимой, Анализатор существует.
Доказательство:
Анализатор будет использовать виртуальную машину для запуска программ. Пусть "состояние" — это текущий снимок программы (слепок памяти, состояние регистров — всё то, что однозначно определяет условные переходы). Если дано "состояние 1", то с помощью виртуальной машины можно однозначно определить "состояние 2", в котором программа будет на следующем шаге, то есть мы имеем односвязный список состояний. Если программа останавливается, то список состояний не имеет циклов. Если программа не останавливается, то список состояний обязательно содержит цикл (т.к. память конечна, то и количество состояний конечно). Задача свелась к поиску цикла в односвязном списке, которую любят задавать на собеседованиях. А эта задача имеет решение.
У меня 3 вопроса:
1. Есть ли ошибки в моём доказательстве?
2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Здравствуйте, kochetkov.vladimir, Вы писали:
KV>Не с той стороны Если бы проблема останова была разрешима, то можно было бы свести доказательство Большой Теоремы Ферма к доказательству остановки алгоритма, выполняющего в цикле if (x ^ n + y ^ n == z ^ n) { Stop(); } для всех x,y и z.
К доказательству зацикливания, ты хочешь сказать?
Ну так оно и так сводится.
У нас есть цикл
for all n,x,y,z:
if CounterExample(n,x,y,z):
break
Доказываем классическим способом, что контрпример никогда не выполняется (130-страничный текст), откуда делаем вывод, что программа не останавливается. И что?
Здравствуйте, vdimas, Вы писали:
V>Это т.н. "символьные вычисления" — противоположность твоему подходу.
Этот "подход" был использован лишь как способ доказать на примере, что анализатор для программ с конечной памятью существует.
Напомню, что в оригинальной проблеме остановки Анализатора не существует.
V>Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1).
Наверное, спутал с индукцией? =)
V> Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно.
Целевая программа может никогда не завершится, а Анализатор всегда завершается.
Здравствуйте, gandjustas, Вы писали:
К>>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью? G>Конечно.
В лекции были приведены задачи, которые сводятся к задаче остановки:
— верна ли теорема Ферма xn + yn != zn для натуральных x, y, z и n > 2;
— есть ли нечетные совершенные числа;
— бесконечно ли множество простых близнецов.
С конечной памятью не выйдет проверить все натуральные числа, поэтому эти задачи не получится решить.
Так какие применения может иметь Анализатор для программ с конечной памятью?
G>Но в реальности программы с конечным множеством состояний не представляют интереса. G>Память это не только ОП, но и дисковая память. Последняя у нас потенциально бесконечна.
G>Кроме того МТ это "устройство" без внешнего ввода. А любой внешний ввод может быть представлен как бесконечная лента "событий".
При конечной разрядности и объеме памяти — вовсе не бесконечной (входные данные же тоже имеют ограничение по разрядности).
Тут правильно рядом напомнил Кайберакс, что в этом случае существует эквивалентный конечный автомат, т.е. взаимное расположение состояний автомата и входных данных обязательно будут повторяться.
G>Поэтому практически любая интерактивная программа, или программа, использующая данные на диске, попадает под проблему останова.
Да пофиг диск-то!
Взять обычную стековую машинку на жалкие 64к слов, где ширина слова пусть равна жалкие 16 бит. Полный перебор всех состояний такой стековой машинки займет больше времени, чем осталось жить вселенной. Это факториал из 64к!
Для сравнения, факториал из 255 равен ~3.35*10504
Там будет число с десятичной степенью около 600к ))
Т.е., даже если делаем миллиард операций в секунду — это минус 12 из степени. Взять еще все компьютеры мира — это еще минус 12-13 из степени. Ни о чём, кароч. ))
Здравствуйте, vdimas, Вы писали:
V>Это факториал из 64к!
Наврал, это будет в точности 64к64к, т.е. на один порядок степени меньше.
Для увеличения десятичной степени на порядок надо брать на ~3.3 разряда больше в слове и соответственно брать кол-во слов в 2 в степени ширины слова.
Но даже исходная машинка тоже ничего так для полного обхода, при том, что вселенной осталось порядка 101000 лет при самом позитивном раскладе. ))
Здравствуйте, vdimas, Вы писали:
V>Наврал, это будет в точности 64к64к, т.е. на один порядок степени меньше. V>Для увеличения десятичной степени на порядок надо брать на ~3.3 разряда больше в слове и соответственно брать кол-во слов в 2 в степени ширины слова.
V>Но даже исходная машинка тоже ничего так для полного обхода, при том, что вселенной осталось порядка 101000 лет при самом позитивном раскладе. ))
Во-первых, программа скорее всего будет использовать малую часть пространства состояний машины. Выше рассмотрен наихудший случай.
Во-вторых, суть в том, что анализатор остановится за конечное время, а не будет работать вечно.
Понятно, что алгоритм использовать в лоб непрактично, придется немного оптимизировать =)
Здравствуйте, Куть, Вы писали:
К>В лекции были приведены задачи, которые сводятся к задаче остановки: К>- верна ли теорема Ферма xn + yn != zn для натуральных x, y, z и n > 2;
Каким это образом?!
Теорема Ферма доказана за конечное время и конечную память. Значит, проблема остановки тоже решена?
К>С конечной памятью не выйдет проверить все натуральные числа, поэтому эти задачи не получится решить.
Чисел-то счётность, но доказательство же не методом перебора чисел, а методом перебора классов функций. Которых, по счастью, оказалось конечное количество.
Не, конечно, для любой задачи (?) можно придумать заведомо тупой алгоритм. Знаменитая задача о самой медленной сортировке — тому пример.
Здравствуйте, Кодт, Вы писали: К>Здравствуйте, Куть, Вы писали:
К>>В лекции были приведены задачи, которые сводятся к задаче остановки: К>>- верна ли теорема Ферма xn + yn != zn для натуральных x, y, z и n > 2;
К>Каким это образом?! К>Теорема Ферма доказана за конечное время и конечную память. Значит, проблема остановки тоже решена?
Не с той стороны Если бы проблема останова была разрешима, то можно было бы свести доказательство Большой Теоремы Ферма к доказательству остановки алгоритма, выполняющего в цикле if (x ^ n + y ^ n == z ^ n) { Stop(); } для всех x,y и z.
Здравствуйте, Кодт, Вы писали:
К>Доказываем классическим способом, что контрпример никогда не выполняется (130-страничный текст), откуда делаем вывод, что программа не останавливается. И что?
Если для вычисления CounterExample требовалась бы МТ, то классического способа доказать выделенное просто не существовало бы. Однако, для вычисления x ^ n + y ^ n == z ^ n вероятно достаточно и стекового автомата, поэтому мы и имеем 130 страниц, доказывающих по сути, что на любых наборах входных данных этот автомат не достигнет допускающего состояния.
Здравствуйте, Куть, Вы писали:
К>Во-первых, программа скорее всего будет использовать малую часть пространства состояний машины. Выше рассмотрен наихудший случай.
Я рассмотрел случай наилучшего кодирования, т.е. когда всё пространство состояний является валидным.
К>Во-вторых, суть в том, что анализатор остановится за конечное время, а не будет работать вечно.
Я плохо понимаю это утверждение для случая, скажем, парсера. Именно состояния парсера можно так закодировать для стековой машинки, чтобы сделать аналогичный описанному полный перебор его возможных состояний (с учетом максимальной глубины вложенности выражений). Примерную длину неповторяющейся входной последовательности я оценил. Вперед! ))
К>Понятно, что алгоритм использовать в лоб непрактично, придется немного оптимизировать =)
Алгоритм как алгоритм. Не перепрыгнет выше фундаментальных ограничений.
Ну.. допустим у тебя есть алгоритм, которые выдает «да» или «нет». На машине с конечной памятью он будет вывавать «да», «нет» и ENOMEM. Что, в общем-то эквивалентно «да», «нет», «фиг его знает». Для этой цели и твой анализатор не нужен, можно просто запустить алгоритм, подождать 10 минут, дней, лет и если алгоритм не закончил свою работу, то выдать «фиг его знает» с тем же результатом.
Здравствуйте, Mystic, Вы писали:
M>Ну.. допустим у тебя есть алгоритм, которые выдает «да» или «нет». На машине с конечной памятью он будет вывавать «да», «нет» и ENOMEM. Что, в общем-то эквивалентно «да», «нет», «фиг его знает». Для этой цели и твой анализатор не нужен, можно просто запустить алгоритм, подождать 10 минут, дней, лет и если алгоритм не закончил свою работу, то выдать «фиг его знает» с тем же результатом.
Алгоритм выполняется на виртуальной машине, в которой достаточное количество памяти, чтобы исключить ENOMEM, оставив только «да» и «нет».
Требуемое количество памяти конечно, и время работы алгоритма конечно.
Здравствуйте, vdimas, Вы писали:
V>Я рассмотрел случай наилучшего кодирования, т.е. когда всё пространство состояний является валидным.
Всё пространство состояний может быть валидным, но анализируемая программа скорее всего будет использовать только малое число (например 10-64k процента) возможных состояний.
Вкупе с группировкой состояний по классам эквивалентности, это настолько уменьшает время выполнения для некоторого множества программ, что вселенная даже ещё не успеет остыть =)
К>>Во-вторых, суть в том, что анализатор остановится за конечное время, а не будет работать вечно.
V>Я плохо понимаю это утверждение для случая, скажем, парсера. Именно состояния парсера можно так закодировать для стековой машинки, чтобы сделать аналогичный описанному полный перебор его возможных состояний (с учетом максимальной глубины вложенности выражений). Примерную длину неповторяющейся входной последовательности я оценил. Вперед! ))
Что "вперёд"?
Хочешь сказать, что на это уйдёт много времени? Я с этим и не спорю.
Или что алгоритм не завершится за конечное время? Вот с этим готов поспорить.
V>Алгоритм как алгоритм. Не перепрыгнет выше фундаментальных ограничений.
Здравствуйте, Куть, Вы писали:
К>Или что алгоритм не завершится за конечное время?
Для проверки работы парсера с ограничением по глубине вложенности выражений надо подать полный перебор всех возможных строк с учетом этого ограничения. Время будет конечное, но Вселенная не доживёт. Причем, не доживёт многие миллиарды раз. ))
V>>Алгоритм как алгоритм. Не перепрыгнет выше фундаментальных ограничений. К>И какие фундаментальные ограничения у алгоритма?
Но, если мы требуем от Анализатора конечное время для остановки, и скорость работы Анализатора так же конечна, то логично было бы потребовать от программ работать с конечной памятью.
Я привел тебе пример ОЧЕНЬ конечной памяти совершенно смешных объёмов по современным меркам.
Твоё допущение:
анализируемая программа скорее всего будет использовать только малое число (например 10-64k процента) возможных состояний
Не влазит ни в какие ворота, бо тогда мы сможем что-то утверждать лишь с 10-64k вероятностью.
Здравствуйте, vdimas, Вы писали:
V>Для проверки работы парсера с ограничением по глубине вложенности выражений надо подать полный перебор всех возможных строк с учетом этого ограничения. Время будет конечное, но Вселенная не доживёт. Причем, не доживёт многие миллиарды раз. ))
Всё, сорри за тупку, до меня дошло — ты хочешь перебрать все возможные строки. Я почему-то зациклился на одной строке. Ну да, тогда анализатор для этой программы будет выполняться долго. Как впрочем и сама программа, которая прогоняет все возможные строки через твой парсер, ведь он должен перебрать все 64k! состояний. Действительно, наихудший случай! А может, не нужно перебирать все строки, а можно как-нибудь сгруппировать их? А что, если Анализатор сам этим займётся на основе текста программы парсера, которую подали ему на вход?
Можно придумать и более короткий пример, для которого алилизатор будет долго работать — например, вызвать рекурсивную функцию Аккермана с аргументами, имеющими значения 4 или больше. Она тоже будет работать дольше, чем время жизни вселенной. Но люди как-то поняли, что она останавливается.
К>>И какие фундаментальные ограничения у алгоритма?
V>Я привел тебе пример ОЧЕНЬ конечной памяти совершенно смешных объёмов по современным меркам. V>Твоё допущение V>Не влазит ни в какие ворота, бо тогда мы сможем что-то утверждать лишь с 10-64k вероятностью.
Я писал про запуск парсера на одной строке, грубо говоря. Это свойство большинства алгоритмов: они не перебирают все возможные состояния, как твоя программа, которая запускает парсер на всех возможных строках.
Так какие фундаментальные ограничения у алгоритма?
Здравствуйте, Кодт, Вы писали:
KV>>Если для вычисления CounterExample требовалась бы МТ, то классического способа доказать выделенное просто не существовало бы. Однако, для вычисления x ^ n + y ^ n == z ^ n вероятно достаточно и стекового автомата, поэтому мы и имеем 130 страниц, доказывающих по сути, что на любых наборах входных данных этот автомат не достигнет допускающего состояния. К>Какая-то хитрость в этих рассуждениях.
Хитрость на поверхности:
Из неразрешимости проблемы останова следует то, что мы не можем иметь общий/единый алгоритм на МТ который доказывает не останов произвольного алгоритма на МТ.
Но из этого отнюдь не следует того, что для какого-то конкретного алгоритма МТ у нас не может быть алгоритма МТ доказательства его не останова.
Здравствуйте, Куть, Вы писали:
К>А может, не нужно перебирать все строки, а можно как-нибудь сгруппировать их? А что, если Анализатор сам этим займётся на основе текста программы парсера, которую подали ему на вход?
Вооот...
Это другой полюс исследований в этой области.
Делается это через "док-ва". В практическом плане на прямо сегодня — через дедукцию и парные ей альфа/бета-редукции. Есть некий набор примитивов, про которые известны их характеристики. Любая программа — комбинация таких примитивов с учетом их ограничений. Св-ва подавляющего большинства однопоточных алгоритмов можно вывести через св-ва их примитивов и способа их комбинации.
Это т.н. "символьные вычисления" — противоположность твоему подходу.
К>Но люди как-то поняли, что она останавливается.
Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1).
К>Я писал про запуск парсера на одной строке, грубо говоря. Это свойство большинства алгоритмов: они не перебирают все возможные состояния, как твоя программа, которая запускает парсер на всех возможных строках. К>Так какие фундаментальные ограничения у алгоритма?
"Алгоритм" не в состоянии сделать вывод о корректности программы за разумное время. "Алгоритм" может только выдать "да/нет" для конкретного набора входных данных. Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно. От того, что мы проэмулировали императивный вычислитель, мы не поменяли низлежащую вычислительную модель; мы лишь, считай, добавили немного отладочной информации. ))
Здравствуйте, Куть, Вы писали:
V>>Это т.н. "символьные вычисления" — противоположность твоему подходу. К>Этот "подход" был использован лишь как способ доказать на примере, что анализатор для программ с конечной памятью существует.
Похоже, ты уже споришь сам с собой. Я же не с этим спорил, а с тем, что в практическом плане это нам ничего не даёт.
К>Напомню, что в оригинальной проблеме остановки Анализатора не существует.
Я и не обсуждал эту проблему. Я демонстрировал, что твой Анализатор не работает лучше, чем сценарий непосредственного запуска самой программы. Именно поэтому предложил покопаться в альтернативном направлении.
V>>Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1). К>Наверное, спутал с индукцией? =)
Почему спутал? Индукцией является умозрительный вывод (человеком) характеристик алгоритма от i = 0, 1.. до произвольного N, в процессе же работы символьного анализатора происходит обратное — именно дедукция.
V>> Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно. К>Целевая программа может никогда не завершится, а Анализатор всегда завершается.
Я давал оценки времени этого "всегда завершается" для небольшой разрядности и небольшого (по современным меркам) пространства состояний — Вселенная успеет миллиарды миллиардов раз по кругу схлопнуться в ЧД и снова взорваться.
Т.е., в смысле здравого материализма — нет ровно никакой разницы.
Здравствуйте, Evgeny.Panasyuk, Вы писали:
EP>Но из этого отнюдь не следует того, что для какого-то конкретного алгоритма МТ у нас не может быть алгоритма МТ доказательства его не останова.
С этим никто и не спорит, просто напоминают, что такой алгоритм может быть выражен более простой моделью — КА, например. И прямо из св-в КА следует конечность мн-ва его состояний.
Здравствуйте, vdimas, Вы писали:
EP>>Но из этого отнюдь не следует того, что для какого-то конкретного алгоритма МТ у нас не может быть алгоритма МТ доказательства его не останова. V>С этим никто и не спорит, просто напоминают, что такой алгоритм может быть выражен более простой моделью — КА, например. И прямо из св-в КА следует конечность мн-ва его состояний.
Конкретный обсуждаемый алгоритм не может быть выражен в КА, при этом у нас есть доказательство его не останова.
Здравствуйте, vdimas, Вы писали:
V>Похоже, ты уже споришь сам с собой. Я же не с этим спорил, а с тем, что в практическом плане это нам ничего не даёт.
Ничего не даёт использование Анализатора вообще или конкретного описанного в доказательстве алгоритма (назовем его "наивным")?
Если наивного, то кто ещё спорит сам с собой =)
Если вообще, то есть практическое применение: http://rsdn.ru/forum/philosophy/6186702.1
V>Я и не обсуждал эту проблему. Я демонстрировал, что твой Анализатор не работает лучше, чем сценарий непосредственного запуска самой программы. Именно поэтому предложил покопаться в альтернативном направлении.
А я могу продемонстрировать, что это принципиально разные вещи.
Возьмём программу на питоне:
while True:
pass
print("Done")
Даже наивный Анализатор завершается мгновенно, а программа не завершается.
К>Она тоже будет работать дольше, чем время жизни вселенной. Но люди как-то поняли, что она останавливается. V>Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1). К>Наверное, спутал с индукцией? =) V>Почему спутал? Индукцией является умозрительный вывод (человеком) характеристик алгоритма от i = 0, 1.. до произвольного N, в процессе же работы символьного анализатора происходит обратное — именно дедукция.
Ты потерял контекст, мы и говорили о человеке. Аккерман опубликовал свою функцию в начале 20-го века.
V>Я давал оценки времени этого "всегда завершается" для небольшой разрядности и небольшого (по современным меркам) пространства состояний — Вселенная успеет миллиарды миллиардов раз по кругу схлопнуться в ЧД и снова взорваться. V>Т.е., в смысле здравого материализма — нет ровно никакой разницы.
Для программы выше ты не успеешь подумать о вселенной, а Анализатор уже завершится.
Здравствуйте, Куть, Вы писали:
V>>Я и не обсуждал эту проблему. Я демонстрировал, что твой Анализатор не работает лучше, чем сценарий непосредственного запуска самой программы. Именно поэтому предложил покопаться в альтернативном направлении. К>А я могу продемонстрировать, что это принципиально разные вещи. К>Возьмём программу на питоне: К>Даже наивный Анализатор завершается мгновенно, а программа не завершается.
Тем не менее, я продемонстрировал ситуацию, когда применение анализатора ничем не лучше.
А в подобных приведенному сниппету современные компиляторы разобраться могут сами — выдают предупреждение о бесконечной рекурсии и т.д.
К>Ты потерял контекст, мы и говорили о человеке. Аккерман опубликовал свою функцию в начале 20-го века.
Словоблудие уже пошло, сорри. Во времена Аккермана не было чему "работать дольше, чем время жизни вселенной", компьютеров еще не было. А если мы говорим о времени работы программы, то компьютер индукцию не умеет, он умеет обратное по заданным формулам.
V>>Т.е., в смысле здравого материализма — нет ровно никакой разницы. К>Для программы выше ты не успеешь подумать о вселенной, а Анализатор уже завершится.
Я по работе, бывает, сталкиваюсь с дедлоками или зацикливаниями системы из нескольких ммм, назовём их "агентами", то бишь относительно независимыми процессами в рамках одной программы (такое зацикливание тоже выглядит как дедлок для конкретного многопоточного алгоритма). Причем, описанные эффекты бывают наведены такими причудливыми сценариями, что без пол-литры и не разберешься))
Даже в MS не сумели полностью избавиться от дедлоков в их SQL-сервере по объективным причинам.
Так вот, мой посыл в том, что современная многопоточная программа — это автомат с охренительным пространством состояний. И именно для обычной современной программы подобный анализатор фактически бесполезен из-за указанных мною ограничений. Простое зацикливание обнаруживается простой отладкой и это такой ничтожный %% всех сценариев, что овчинка выделки не стоит. А вот найти потенциальный сценарий дедлока или зацикливания алгоритма (алгоритмов) из мн/ва общающихся процессов, прогнав всевозможные взаимные относительные состояния всех потоков исполнения — вот это, действительно, будет востребованная весчь. И всё моё участие здесь сводится к тому, чтобы на пальцах объяснить, что избранный тобой путь поставленную задачу принципиально не решает из-за фундаментальных ограничений этого подхода (например, из двух процессов по 100 состояний в каждом, после прогона их всевозможных взаимных состояний, получим 10тыщ различных состояний эквивалентного одного автомата, и я давал прикидки именно на такой порядок кол-ва состояний).
В общем, нужен другой подход. Нужен символьный анализ, нужен "алфавит" известных "кубиков", нужен анализ и декомпозиция алгоритмов до этих кубиков с известными св-вами и затем аналитический вывод св-в программы из знаний о св-вах известных композиций из известных кубиков и далее по иерархии таких композиций. Это навскидку. А как оно будет, если заняться этим всерьез — я ХЗ.
Перекуём баги на фичи!
Если бы проблема останова была разрешима, то можно было бы свести доказательство Большой Теоремы Ферма к доказательству остановки алгоритма, выполняющего в цикле if (x ^ n + y ^ n == z ^ n) { Stop(); } для всех x,y и z.
