Пример зачем нужна верификация программ: баг в сортировке Java-ы
Только с помощью верификации удалось найти ошибку в реализации Timsort-а, который сейчас используется на Java-е в качестве метода стандартной сортировки.Вот и реальная причина пропажи боингов в море!..
Какой минимальный размер массива, на котором удается воспроизвести ошибку?
Какой минимальный размер массива, на котором удается воспроизвести ошибку?на Java-е похоже 67108864
на CPython 2^49
Верификация - не решаемая в принципе проблема.
В общем случае, конечно, не решаемая - особенно для программ, в которых есть ошибки.
Например, в статье явно говорится, что у них не получилось построить инвариант для цикла сортировки просто потому, что там его не было.
Например, в статье явно говорится, что у них не получилось построить инвариант для цикла сортировки просто потому, что там его не было.
Например, в статье явно говорится, что у них не получилось построить инвариант для цикла сортировки просто потому, что там его не было.А может получиться так, что его не удастся построить потому, что они остановятся за час до того, как он мог бы быть построен. Проблема остановки она такая.
Проблема остановки она такая.Проблема останова здесь, вообще, не причем. Она же рассматривает вообще все возможные программы.
На практике же мы сталкиваемся с другим классом программ, с теми - поведение которых автор программы хочет предсказывать. И это означает, что автор программы использовал такие конструкции - поведение которых он мог легко предсказать.
Кстати, именно из-за этого был предан анафеме goto, и коды возрата ошибок стараются заменить на исключения.
Первое убирает проблему останова, второе - обеспечивает легко вычислимое предсказание, каким будет поведение программы при произвольной ошибке.
Первое убирает проблему останова, второе - обеспечивает легко вычислимое предсказание, каким будет поведение программы при произвольной ошибке.
обеспечивает легко вычислимое предсказание, каким будет поведение программы при произвольной ошибке.И как в этом помогают исключения?
И как в этом помогают исключения?То, что все возможные ошибки в любом месте взятого куска кода сводятся только к двум ситуациям:
- ошибки не было, программа последовательно выполняет записанные операторы
- ошибка была, программа прервала свою работу и начала разматывать стек вызовов, корректно восстанавливая свое состояние
Соответственно, дальше для проверки программы на корректность работы при ошибках достаточно верифицировать, что:
- все ошибки переводятся в исключения
- при размотки стека, всё состояние корректно восстанавливается.
A non-exhaustive list of notable aircraft/avionics using Ada;
Commercial
Airbus – Aircraft: A320, A330, A340, A350 XWB
Boeing – Aircraft: 787, 777, 767,757, 747-400, 737-200, (and others)
Java has also found its way into avionics systems like CIDS, OMS, EFB and IFE.расшифровки (вроде как не критические области):
CIDS - Cabin Intercommunication Data System
OMS - Onboard Maintenance System
EFB - Electronic flight bag
IFE - aircraft In-Flight Entertainment
взято отсюда:
http://www.linkedin.com/groups/Which-is-Major-Programming-l...
На практике же мы сталкиваемся с другим классом программ, с теми - поведение которых автор программы хочет предсказывать. И это означает, что автор программы использовал такие конструкции - поведение которых он мог легко предсказать.Очевидно, любой язык программирования эквивалентен (если помнить о конечной памяти) машине тьюринга, а значит для него верна теорема об останове. А за предсказаниями можно обращаться к гадалке.
Т.е. понятно, что как-то что-то со скрипом можно верифицировать. Например такие вещи как сортировка, которая суть вещь в себе, или же можно заставлять программиста писать программы так, чтобы тупая программа не надрывалась слишком сильно при анализе и заставлять его переписывать прогу, если вер. тулза не понимает программы. Такие попытки были, но зафейлились, поскольку указание необходимой инфы для верификации отнимало времени больше чем само программирование.
Вообще, история в первом посте прекрасный пример бесполезности верификации. Некорректный алгоритм прекрасно работал долгие годы, значит баг имел незначительные последствия. Уверен, что почти все программы некорректны, но прекрасно могут работать годами без ошибок.
Очевидно, любой язык программирования эквивалентен (если помнить о конечной памяти) машине тьюринга, а значит для него верна теорема об останове.Да. Эта теорема о том, остановится ли программа вообще.
На практике же задача соверешенно другая. Вопрос звучит так: остановится ли программа за менее, чем N тактов?
И эта задача разрешима - т.к. в худшем случае достаточно отсимулировать N тактов, чтобы ответить на этот вопрос.
В большинстве же случаев, ответить на этот вопрос можно намного быстрее, используя тот факт, что для многих крупных блоков известна оценка сверху - как много тактов они будут исполняться.
> Такие попытки были, но зафейлились, поскольку указание необходимой инфы для верификации отнимало времени больше чем само программирование.
Они зафейлились, потому что подход только зарождался и задача выписывания контрактов и инвариантов возглагалась на человека - что приводило к очень высокой трудоемкости.
Текущие подходы ориентированы на то, что инварианты восстанавливаются автоматически.
Такой подход, например, используется во Flow, в чекере JS от facebook. Ограничения на типы там восстанавливаются автоматически на основе кода.
Некорректный алгоритм прекрасно работал долгие годы, значит баг имел незначительные последствия. Уверен, что почти все программы некорректны, но прекрасно могут работать годами без ошибок.Да, ошибки это не страшно, но это только пока кто-то не начинает использовать ошибки против пользователя. Или от ошибок не начинает зависеть жизнь большого кол-ва людей.
Уверен, что почти все программы некорректны, но прекрасно могут работать годами без ошибок.Этот подход прекрасно иллюстрируется анекдотом:
- Обезьяна, ты что пилишь? Это ведь атомная бомба! Взорвётся!
- Ничего у меня ещё одна есть!
Да, ошибки это не страшно, но это только пока кто-то не начинает использовать ошибки против пользователя. Или от ошибок не начинает зависеть жизнь большого кол-ва людей.Первое неискоренимо, потому что быстронаписанный говнокод всегда будет побеждать вдумчивый мегакод, а второе и так решается выбором инструментов и методологией. Писали тут как-то про НАСА.
Некорректный алгоритм прекрасно работал долгие годы, значит баг имел незначительные последствия.Heartbleed тоже прекрасно работал долгие годы.
Этот подход прекрасно иллюстрируется анекдотом:Неправильно. На самом деле -
-Обезьяна, ты что пилишь? Это ведь атомная бомба! Взорвётся!
- Ничего у меня ещё одна есть!
- ...
- И похер, вася в соседнем городе тоже пилит и тот, кто успеет первый получит контракт на миллиард долларов.
второе и так решается выбором инструментов и методологиейВерификация - это и есть один из используемых инструментов.
Кстати, статически типизированные языки - это же и есть подмножество узко специализированных верификаторов. Они только проверяют не время выполнения, а то, что все результаты при всех вариантах выполнения уложатся в зафиксированные ограничения на тип результата.
Поэтому статическая типизация осложняет программирование. Нетипизированные языки имеют большую выразительную силу.
Как следствие, чем больше таких общих верификационных правил, тем сложнее писать программы.
Как следствие, чем больше таких общих верификационных правил, тем сложнее писать программы.
кто успеет первый получит контракт на миллиард долларов.Ты рассматриваешь только одну часть мира - стартапы. Для них да, кто первый успел того, и тапки.
Но кроме стартапов есть еще компании, которые уже заняли определенную нишу: google, yandex, facebook, microsoft. Для них становится жизненно важным уметь верифицировать тонны legacy кода. На ошибки, на потребление энергии, на потребление памяти, на соответствие новым требованиям и т.д.
Например, микрософт сначала потерял критически важные железки - потому что не смог быстро предсказывать ошибки в своем ПО; затем проиграл браузерную войну - потому что не смог предсказать насколько точно и быстро IE отрабатывает спецификацию html и css, а затем потерял планшеты - потому что не смог быстро выделить какие части больше всего жрут батарею.
Только с помощью верификации удалось найти ошибку в реализации Timsort-а, который сейчас используется на Java-е в качестве метода стандартной сортировки.Вот ещё что интересно было бы узнать. Просматривал ли кто-нибудь логи своей системы в поисках этого исключения? Если да, то нашли или нет?
То, что все возможные ошибки в любом месте взятого куска кода сводятся только к двум ситуациям:Ничего не понял.
- ошибки не было, программа последовательно выполняет записанные операторы
- ошибка была, программа прервала свою работу и начала разматывать стек вызовов, корректно восстанавливая свое состояние
Соответственно, дальше для проверки программы на корректность работы при ошибках достаточно верифицировать, что:
- все ошибки переводятся в исключения
- при размотки стека, всё состояние корректно восстанавливается.
Для проверки программы, использующей возвращаемые значения для сигнализирования об ошибках, на корректность достаточно верифицировать, что:
- все ошибки переводятся в правильные возвращаемые значения
- все возвращаемые значения корректно обрабатываются.
Приведи пример, когда делать некие выводы о программе с исключениями проще, чем об эквивалентной ей программе без исключений.
Для проверки программы, использующей возвращаемые значения для сигнализирования об ошибках, на корректность достаточно верифицировать, что:Разницу между верифицировать две ситуации и 4млрд. кодов возврата видишь? А она есть.
Разницу между верифицировать две ситуации и 4млрд. кодов возврата видишь? А она есть.И чем же найти в дереве вызовов все выражения вида raise Something сложнее, чем return n, где n - численная константа отличная от нуля?
И чем же найти в дереве вызовов все выражения вида raise Something сложнее, чем return n, где n - численная константа отличная от нуля?Тем что в первом случае не надо искать код обработки ошибки во всех функциях, которые используют данную функцию, а во втором - необходимо.
банальное
void* buf = malloc(..);
int* buf = new ..;
unique_ptr<int[]> buf = new ..;
В первом случае, необходимо отследить, что:
- все трассы выполнения кода использует buf только после того, как он проверен на buf != null
- все трассы делают free(buf)
Во втором случае, необходимо отследить, что:
- все трассы(включая трассу размотки стека) делают delete[] buf;
В третьем случае, необходимо отследить только, что buf имеет тип smart-поинтера.
Поэтому статическая типизация осложняет программирование. Нетипизированные языки имеют большую выразительную силу.Имхо, будущее за условно-статически типизированными языками. Появление auto/var и неявное выведение типов в статически-типизированных языках и применение static-checker-ов для нетипизированных - это как раз оно и есть.
При таком подходе типы есть, но программист не парится о том, чтобы их явно выписывать - компьютер это делает за него. Программист же лишь пользуется этим, поправляя те места - для которых компьютер вывел, что получившийся тип не совпадает с вариантом использования.
В первом случае, необходимо отследить, что:Задачи сопоставимой сложности по-моему.
- все трассы выполнения кода использует buf только после того, как он проверен на buf != null
- все трассы делают free(buf)
Во втором случае, необходимо отследить, что:
- все трассы(включая трассу размотки стека) делают delete[] buf;
Задачи сопоставимой сложности по-моему.Согласен. Именно поэтому и стараются - или использовать язык с GC, или внести в code-style использование smart-pointer-ов. Такие подходы позволяет убрать эту сложность.
Имхо, будущее за условно-статически типизированными языками.Вообще-то, они только теряли позиции в последние 15 лет. Пользуясь нетипизированными языками, понимаешь, что типов может быть бесконечное множество и объявлять несколько конкретных - это как делать все по уставу.
объявлять несколько конкретных - это как делать все по уставуЭтим грешат только языки, которые имеют два устаревших решения:
- жесткую привязку типов к их размещению в памяти
- повсеместное использование номинальной системы типов
К сожалению, это есть во всех main-stream статически-типизированных языках: C++, Java, C#.
Вообще-то, они только теряли позиции в последние 15 лет.Обоснуй.
Баг-то пофиксили уже, или нет?
Первое убирает проблему останова,while уже отменили?
while уже отменили?В программах используется два вида циклов - организация непрерывной работы и последовательное движение к цели.
Первый вид - это, например, цикл в очереди сообщений, а второе - цикл в функции сортировки.
Для первого нет необходимости верифицировать, что он закончится; а для второго - всегда есть
ps
Рекурсия - это тот же цикл, но с использованием стека. Для таких циклов необходимо верифицировать, что стек опустеет за кол-во итераций менее N.
всегда есть инвариант, уменьшающийся по мере приближения к целе.Разве инвариант - это не то, что не изменяется?
я бы не стал так категорично утверждать, что в конструкции
while (condition)
...
всегда есть такой инвариант. Но в любом случае, про goto все то же самое можно сказать, он ничем не лучше и не хуже в точки зрения верификации.
while (condition)
...
всегда есть такой инвариант. Но в любом случае, про goto все то же самое можно сказать, он ничем не лучше и не хуже в точки зрения верификации.
Разве инвариант - это не то, что не изменяется?Да, так оно и есть. Спасибо за уточнение.
В данном случае, речь, конечно, идет об "аннотации decreases", а не об инварианте.
В школьной математике это называли "полуинвариантом", но похоже терминология нестандартная.
goto хуже тем что он позволяет создавать irreducible loops.
goto хуже тем что он позволяет создавать irreducible loops.
всегда есть такой инвариантЕсли цикл написан без всякой цели или он содержит ошибку, то да - уменьшающегося выражения у него не будет.
Но в любом случае, про goto все то же самое можно сказать, он ничем не лучше и не хуже в точки зрения верификации.Goto портят блочную структуру программ. В следующем спагетти черт ногу сломит. И для него даже предусловия выделить проблематично у кодов code1-8, что уж говорит про уменьшающееся выражение для циклов.
A:
code1;
if (condition1)
{
code2;
goto C;
}
else
{
code3;
}
code4;
B:
code5;
if (condition2)
{
code6;
goto A;
}
else
{
code7;
goto B;
}
code8;
goto B;
C:
Еще веселее goto в asm-е, там можно прыгать в середину инструкции, что не только делает сложным выделение предусловий кода, но и дает другой набор инструкций на следующей итерации.
Goto портят блочную структуру программ. В следующем спагетти черт ногу сломит. И для него даже предусловия выделить проблематично у кодов code1-8, что уж говорит про уменьшающееся выражение для циклов.Для человека может и сложнее, а для полу-автоматической системы верификации — нет. Метод Флойда никто не отменял.
Для человека может и сложнее, а для полу-автоматической системы верификации — нет. Метод Флойда никто не отменял.Сложность - это кол-то требуемых тактов для выделения условий.
Чем больше goto в коде используется, тем больше требуется тактов для выделения предусловий, постусловий, инвариантов и условий уменьшения.
Для человека может и сложнее, а для полу-автоматической системы верификации — нет. Метод Флойда никто не отменял.Нет, при верификации составляется control flow graph, и дальше сложность верификации зависит не от размера графа, а от количества циклов в этом графе (на каждом цикле нужно выбрать по "точке сечения", в которой придумать инвариант). И не важно уже образован ли цикл с помощью while или с помощью goto
Сложность - это кол-то требуемых тактов для выделения условий.
Чем больше goto в коде используется, тем больше требуется тактов для выд
PS. Если алгоритм решения задачи не менять, а переписать все while на goto, то количество циклов от этого не увеличится. К слову, break из while по сути — тот же goto, только завуалированный
переписать все while на goto, то количество циклов от этого не увеличитсяКак из этого следует, что произвольные goto не усложняют анализ?
Все ли goto можно переписать на while? Все ли goto можно переписать на while без введения новых переменных? Все ли goto можно переписать на while без введения новых переменных и дублирования кода?
Перепиши, пожалуйста, код выше через while.
Как из этого следует, что произвольные goto не усложняют анализ?Такое ощущение, что мы на разных языках говорим. Goto вообще не влияют на сложность анализа. На сложность анализа влияет сложность графа потока управления. Точка.
Да, с помощью goto можно сделать произвольный граф потока управления. Да, с помощью while совсем произвольный граф сделать нельзя (но очевидно, можно сделать граф произвольной сложности). Как это связано со сложностью верификации конкретной программы? У тебя есть способ верификации while циклов, который не годится для goto?
Ты привел пример спагетти-кода, утверждаешь что его сложно верифицировать. Я не буду с этим спорить. Но почему ты считаешь, что в этом виноваты goto, а не ебанутый алгоритм вычисления? Можешь предложить реализацию того же алгоритма вычислений, но без использования goto, который было бы легко верифицировать?
Пример. Допустим у нас есть некий алгоритм A (считай блок-схема). Можно его запрограммировать с помощью while-циклов, а можно с помощью goto. Вопрос: как это повлияет на сложность верификации? Ответ: никак не повлияет. Если алгоритм описан с помощью блок-схемы, то сложность верификации будет определяться сложностью верификации самой блок-схемы. Синтаксический сахар в виде дополнительных инструкций и даже временных переменных современные число-молотилки проглотят и даже не подавятся.
while (condition)
{
...
if (!condition1)
break;
}
и
bool ok = true;
while (ok && condition)
{
...
ok = condition1;
}
совершенно эквивалентны в плане сложности верификации, что даже современные компиляторы могут выводить их эквивалентность.
Ну и раз ты просил, привожу:
f1:Считаешь такую программу стало легче верифицировать? Что в ней так принципиально изменилось? Да, я удалил недостижимый код code8, но это умеет делать любой компилятор. Если сможешь написать инварианты к while-циклам, то я смогу написать инварианты к твоей goto-версии
code1;
return true;
f2:
code2;
return true;
f5:
code5
return true;
while !(f1 && condition1 && f2)
code3
code4
while (f5 && !condition2)
code7
code6
Каждый набор выразительных средств подразумевает свой стиль построения программ. Программы на лиспе и на си пишутся в разном стиле, хотя у программиста есть возможность писать на обоих языках на фортране. Язык - это больше чем синтаксис и семантика. Это ещё и практики применения. Язык, который лишён goto и обходится одним лишь while, направляет программиста писать код более удобный для анализа циклов. А типизированные языки тоже направляют программиста на поддержание дополнительной структорной информации, упрощающей верификацию, и не особо нужной для запуска самой программы. При том, очевидно, в том же стиле можно писать и на нетипизированных языках, но это там не принято.
goto хуже тем что он позволяет создавать irreducible loops.Use COME FROM, Luke! :]
По-видимому, произвольные goto не усложняют анализ. Все верификационные тулы с которыми я сталкивался в качестве внутреннего представления кода подпрограммы используют control flow graph общего вида, а не структурированную хрень.
Этому две причины, по-моему.
Во-первых, настоящие программы не являются структурированными в строгом смысле, там водятся break, continue, return и исключения. Если бы тул базировался на каких-то гипотетических удобных свойствах структурированных программ, ему бы пришлось транслировать реальные программы в структурированную форму, и они бы от этого раздувались.
Во-вторых, непонятно а почему структурированная форма должна давать преимущества. Например если ты доказываешь частичную корректность программы в формализме Хоара, то количество инвариантов, которые тебе надо будет изобрести, равно числу back edges в графе или что-то типа того, неважно структрурированный он или спагеттиобразный.
Структурированная форма даёт некоторые преимущества человеку. Например, если кусок кода имеет одну точку входа и одну точку выхода, то рассуждать о нём удобно в терминах предусловия и постусловия. Но машине пофиг, она может взять фрагмент графа управления с несколькими точками входа и насколькими точками выхода, и назначить им разные наборы предусловий и наборы постусловий.
Да и вообще сложность и форма графа управления самого по себе понятия довольно условные. Можно взять программу со сложным графом управления, доказательство корректности которой требует кучи инвариантов в разных точках, и трансформировать её в программу с простым графом управления и насколькими дополнительными булевыми переменнными, доказательство корректности которой потребует меньшего количества инвариантов. Но инварианты будут сложнее, типа "flag and simple_invariant1 or not flag and simple_invariant2". В пределе можно вообще сделать граф управления в одну вершину (типа интерпретатор твоей оригинальной программы, где весь control state перенесён в данные это не упростит задачу верификации.
Этому две причины, по-моему.
Во-первых, настоящие программы не являются структурированными в строгом смысле, там водятся break, continue, return и исключения. Если бы тул базировался на каких-то гипотетических удобных свойствах структурированных программ, ему бы пришлось транслировать реальные программы в структурированную форму, и они бы от этого раздувались.
Во-вторых, непонятно а почему структурированная форма должна давать преимущества. Например если ты доказываешь частичную корректность программы в формализме Хоара, то количество инвариантов, которые тебе надо будет изобрести, равно числу back edges в графе или что-то типа того, неважно структрурированный он или спагеттиобразный.
Структурированная форма даёт некоторые преимущества человеку. Например, если кусок кода имеет одну точку входа и одну точку выхода, то рассуждать о нём удобно в терминах предусловия и постусловия. Но машине пофиг, она может взять фрагмент графа управления с несколькими точками входа и насколькими точками выхода, и назначить им разные наборы предусловий и наборы постусловий.
Да и вообще сложность и форма графа управления самого по себе понятия довольно условные. Можно взять программу со сложным графом управления, доказательство корректности которой требует кучи инвариантов в разных точках, и трансформировать её в программу с простым графом управления и насколькими дополнительными булевыми переменнными, доказательство корректности которой потребует меньшего количества инвариантов. Но инварианты будут сложнее, типа "flag and simple_invariant1 or not flag and simple_invariant2". В пределе можно вообще сделать граф управления в одну вершину (типа интерпретатор твоей оригинальной программы, где весь control state перенесён в данные это не упростит задачу верификации.
Во-вторых, непонятно а почему структурированная форма должна давать преимущества. Например если ты доказываешь частичную корректность программы в формализме Хоара, то количество инвариантов, которые тебе надо будет изобрести, равно числу back edges в графе или что-то типа того, неважно структрурированный он или спагеттиобразный.Не, вот тут ты все-таки не прав. Это утверждение как раз верно только для "структурированных" CFG.
Немного определений, чтобы не путаться:
Back edge - дуга (u, v) CFG такая, что v доминирует u.
"Структурированный" граф (reducible) - это такой граф (потока управления который становится ациклическим после удаления из него всех back edge. Иначе - "спагеттиобразный".
Ну так вот, если граф "структурированный" - то действительно, ставим по инварианту на каждый back edge, предусловия в начало и постусловия в конец, после чего у нас не остается в графе циклов не проходящих через контрольную точку. Ну и вперед - доказываем все переходы и получаем доказательство частичной корректности программы. В случае "спагеттиобразного" графа это не работает, так как после расстановки контрольных точек таким образом у тебя в графе останутся циклы, которые потребуют дополнительных контрольных точек для своего устранения, которые еще как-то нужно придумать как ставить.
Использование for, while, if then else, break, continue всегда дает "стурктурированный" граф, goto - не всегда. Пример:
if (cond3) {
label1:
code1;
if (cond1)
goto label2;
} else {
label2:
code2;
if (cond2)
goto label1;
} PS: в этом треде много странных утверждений наделал, но вот с goto он угадал.
А этот код, кстати, "хороший" с точки зрения машины. Человеку его не очень приятно читать (как и код с неправильными выравниваниями, например а машина спокойно увидит два цикла и немного мертвого кода.
A:
code1;
if (condition1)
{
code2;
goto C;
}
else
{
code3;
}
code4;
B:
code5;
if (condition2)
{
code6;
goto A;
}
else
{
code7;
goto B;
}
code8;
goto B;
C:
while (true) {
if (condition1) {
code2;
break;
}
code3;
code4;
while (true) {
code5;
if (condition2)
break;
code7;
}
code6;
}
Черт! Завидую!
Завидую и прусь от того, как вы быстро умеете перевести спагетти в структурированный код. Я так в голове не умею.
В результате, и пример подкачал - не получилось сгенерить реальное спагетти.
Завидую и прусь от того, как вы быстро умеете перевести спагетти в структурированный код. Я так в голове не умею.
В результате, и пример подкачал - не получилось сгенерить реальное спагетти.
Если алгоритм описан с помощью блок-схемы, то сложность верификации будет определяться сложностью верификации самой блок-схемы.Сам исходный алгоритм может быть сформулирован в виде структурной схемы, а может в виде спагетти.
И то, и другое будет работать, но первое будет требовать больше усилий для выделения предусловий и инвариантов.
При этом такие алгоритмы будут эквиваленты по результату, но не будут эквивалентны по ходу работы. И, соответственно, будет проблематично автоматически преобразовать из одного вида в другой.
Твоё определение back edges (не знаю насколько оно общепринятое) специально заточено под структурированные графы. Поэтому неудивительно, что у спагеттиобразных графов оказывается меньше back edges, чем надо инвариантов. Говоря "число back edges или что-то типа того", я имел в виду скорее что-то типа back edges in graph traversal. Впрочем, я не абсолютно уверен что это число не зависит от конкретного порядка обхода графа.
Но это всё мелкие детали. Множества стуктурированных и спагеттиобразных программ не пересекаются. В обоих множествах есть как простые, так и сложные программы. Поэтому основное утверждение "структурированные программы проще для автоматического анализа чем спагеттиобразные" неформально. Отсюда не следует автоматически его бессмысленность. Знание похоже ли на правду это утверждение представляет некоторую ценность для разработчиков тулов и для разработчиков доказуемо корректных программ. Мне кажется что это утверждение похоже на ложь.
Во-первых, потому что разработчики тулов не ведут себя так как если бы оно было похоже на правду. Во-вторых, потому что если его формализовать оно становится ложным.
В попытке его несколько формализовать я заменил "сложность для анализа" на "количество инвариантов, которые придётся изобрести" (с оговоркой про условность сложности control flow в отрыве от сложности memory state) и добавил "при прочих равных" в форме "при равных количествах back edges или типа того". Отсылка к back edges была неудачной идеей. Я по-прежнему считаю, что для любой вменяемой трактовке "при прочих равных" (например, при равной цикломатической сложности, или при равном количестве операторов goto (где while, if, contrinue, break и return считаются за goto или при равном количестве операторов вообще) это утверждение похоже на ложь.
Но это всё мелкие детали. Множества стуктурированных и спагеттиобразных программ не пересекаются. В обоих множествах есть как простые, так и сложные программы. Поэтому основное утверждение "структурированные программы проще для автоматического анализа чем спагеттиобразные" неформально. Отсюда не следует автоматически его бессмысленность. Знание похоже ли на правду это утверждение представляет некоторую ценность для разработчиков тулов и для разработчиков доказуемо корректных программ. Мне кажется что это утверждение похоже на ложь.
Во-первых, потому что разработчики тулов не ведут себя так как если бы оно было похоже на правду. Во-вторых, потому что если его формализовать оно становится ложным.
В попытке его несколько формализовать я заменил "сложность для анализа" на "количество инвариантов, которые придётся изобрести" (с оговоркой про условность сложности control flow в отрыве от сложности memory state) и добавил "при прочих равных" в форме "при равных количествах back edges или типа того". Отсылка к back edges была неудачной идеей. Я по-прежнему считаю, что для любой вменяемой трактовке "при прочих равных" (например, при равной цикломатической сложности, или при равном количестве операторов goto (где while, if, contrinue, break и return считаются за goto или при равном количестве операторов вообще) это утверждение похоже на ложь.
Твоё определение back edges (не знаю насколько оно общепринятое)Хым. Ну в dragonbook именно такое используется. Возможно это компиляторный жаргон, конечно.
A back edge is an edge a -> b whose head b dominates its tail a.
Я по-прежнему считаю, что для любой вменяемой трактовке "при прочих равных" (например, при равной цикломатической сложности, или при равном количестве операторов goto (где while, if, contrinue, break и return считаются за goto или при равном количестве операторов вообще) это утверждение похоже на ложь.Ну вообще у компиляторов есть некоторые осложнения с unreducible CFG, но я не готов так с ходу расписать какие именно, поэтому я пожалуй сольюсь. Тем более что я не уверен, что эти сложности будут также применимы к задаче формальной ферификации.
Использование for, while, if then else, break, continue всегда дает "стурктурированный" граф, goto - не всегда.если че, то "неструктурированный" граф всегда можно преобразовать к "структурированному", так что принципильно, есть goto или нет - тулам по барабану
твой пример, например, в "структурированном" виде можно написать как
if (!cond3)
code2;
if (cond2)
{
do {
code1;
if (!cond1)
break;
code2;
} while (cond2)
}
> у компиляторов есть некоторые осложнения с unreducible CFG
А кстати ты прав наверное. В стандартных data-flow analyses важен порядок итерирования, он влияет на время сходимости. Можно показать, что reverse postorder хорош для структурированных графов. Ничего не мешает применить его к неприводимому графу, но я допускаю что может получится несколько менее эффективно.
Так что можно вообразить какой-нибудь процесс в стиле abstract interpretation, итеративно уточняющий кандидаты в инварианты, и как он хорошо работает для структурированных программ.
А кстати ты прав наверное. В стандартных data-flow analyses важен порядок итерирования, он влияет на время сходимости. Можно показать, что reverse postorder хорош для структурированных графов. Ничего не мешает применить его к неприводимому графу, но я допускаю что может получится несколько менее эффективно.
Так что можно вообразить какой-нибудь процесс в стиле abstract interpretation, итеративно уточняющий кандидаты в инварианты, и как он хорошо работает для структурированных программ.
В основном все цикловые оптимизации будут несчастны, не увидев канонической формы цикла, в gcc сможешь увидеть условия типа LOOPS_IRREDUCIBLE — до свидания. Не берусь сказать сходу, связано ли это с некими глобальными проблемами, скорее всего, про индукционные переменные будет сложно сформулировать что-то вменяемое, ну и для структурных циклов проще писать оптимизации, зная, что вставка кода в заголовок будет доминировать тело, что можно посплитить обратную дугу и т.п. А мозг себе трахать из-за чуваков, пишущих несводимые циклы, никто не будет.
Dataflow может медленнее сходиться, это да.
Dataflow может медленнее сходиться, это да.
Оставить комментарий
Dasar
http://habrahabr.ru/post/251751/Только с помощью верификации удалось найти ошибку в реализации Timsort-а, который сейчас используется на Java-е в качестве метода стандартной сортировки.
1.1 Воспроизводим баг Timsort на Java
Если баг присутствует, вы увидите такой результат