Когда вы столкнулись с проблемой остановки в поле?
Когда вы когда-нибудь лично сталкивались с проблема остановки в полевых условиях? Это может быть, когда коллега / начальник предложил решение, которое нарушило бы фундаментальные ограничения вычислений, или когда вы сами осознали, что проблему, которую вы пытались решить, на самом деле решить невозможно.
Последний раз я придумал это, когда изучал шрифтовые шашки. Наш класс понял, что невозможно написать идеальную программу проверки типов (такую, которая будет принимать все программы, которые будут работать без ошибок типов, и отклонять все программы, которые будут запускаться с ошибками типов), потому что это, по сути, решит проблему остановки. . Другой случай произошел, когда мы в том же классе поняли, что на этапе проверки типов невозможно определить, произойдет ли когда-либо деление на ноль, потому что проверка того, является ли число во время выполнения нулем, также версия проблемы остановки.
@dmindreader - Нет. Большинство компиляторов / языков с типобезопасностью действительно просто проверяют типы, но можно увидеть диапазон значений для чего-то (иногда) с учетом статического анализа. Рассмотрим, как ReSharper или Coverity выдают предупреждения о «возможном нулевом значении».
Раньше я проектировал медицинские устройства. Однажды меня попросили включить в устройство с батарейным питанием световой индикатор, который указывал бы на то, что батарея разряжена.
@DavidSchwartz: Батарея, которая слишком разряжена для питания устройства, может питать светодиод достаточно долго, чтобы его заметил кто-то, кто может заменить батарею.
Ответы 13
Мне буквально назначили проблему остановки, например, «напишите плагин монитора, чтобы определить, постоянно ли не работает хост». Серьезно? Хорошо, я просто дам ему порог. «Нет, потому что он может вернуться позже».
Последовало большое теоретическое изложение.
Вау просто вау. Глубина нелогичности, которая должна существовать в сознании этого человека, просто сбивает меня с толку ...
Что ж, на самом деле это был довольно умный человек, который почувствовал себя довольно смущенным, когда понял проблему.
Просто вытащите вилку :-) Смотрите также en.wikipedia.org/wiki/STONITH
На самом деле эту проблему очень легко решить в .NET. Просто добавьте ссылку на System.Future, а затем в классе System.Future.Fact есть несколько статических методов, которые вы можете использовать. В вашем случае: if (System.Future.Fact.IsPermanent (делегат, чтобы проверить, не работает ли здесь сервер)) {...}
@Lasse, что было бы более правдоподобно, если бы мы говорили о Python :) (не то чтобы я не люблю .NET, но вы знаете ... import antigravity и все такое ...)
Я не думаю, что это правильно. Проблема остановки связана с кодом, который может решить, будет ли программа завершена на всех входах - без ее запуска. Ничто не мешает вам написать монитор, в котором вы запускаете рядом программу, которая может не завершиться.
Так останавливается программа (монитор) или нет?
@Erik Нет, ты нелогичны. Программа очень простая: host.self_destruct(); print("Permanently down.");.
@ LasseV.Karlsen Насколько я понимаю, System.Future еще не реализован. Однако я действительно вижу System.Future.ImplementSystemDotFuture() в документации по дизайну ...
@muntoo, похоже, у вас есть недостижимый код в строке 2
Сложный статический анализ кода может столкнуться с проблемой остановки.
Например, если виртуальная машина Java может доказать, что часть кода никогда не получит доступ к индексу массива за пределами границ, она может пропустить эту проверку и работать быстрее. Для некоторого кода это возможно; по мере усложнения становится проблемой остановки.
У Проект, над которым я сейчас работаю повсюду неразрешимые проблемы. Это генератор модульных тестов, поэтому в целом он пытается ответить на вопрос "что делает эта программа". Это пример проблемы с остановкой. Еще одна проблема, возникшая во время разработки, - это "даны две (тестовые) функции одинаковые"? Или даже "имеет ли значение порядок этих двух вызовов (утверждений)"?
Что интересно в этом проекте, так это то, что, хотя вы не можете ответить на эти вопросы в ситуациях все, вы может находите умные решения, которые решают проблему в 90% случаев, что на самом деле очень хорошо для этой области.
Другие инструменты, которые пытаются рассуждать о другом коде, такие как оптимизация компиляторов / интерпретаторов, инструменты статического анализа кода и даже инструменты рефакторинга, вероятно, столкнутся (и будут вынуждены искать обходные пути) проблему остановки.
Система тестирования Perl поддерживает счетчик тестов. Вы либо указываете количество тестов, которые собираетесь запустить, в верхней части программы, либо заявляете, что не собираетесь его отслеживать. Это защитит вас от преждевременного выхода из теста, но есть и другие охранники, так что это не так уж важно.
Время от времени кто-нибудь пытается написать программу, которая подсчитает для вас количество тестов. Это, конечно, преодолевается простым циклом. Они все равно продвигаются вперед, выполняя все более сложные трюки, пытаясь обнаружить петли, угадать, сколько итераций будет, и решить проблему остановки. Обычно они заявляют, что он просто должен быть «достаточно хорошим».
Другой распространенный вариант - «нам нужно устранить любые взаимоблокировки в нашем многопоточном коде». Совершенно разумный запрос с точки зрения управления, но для предотвращения взаимоблокировок в общем случае вы должны проанализировать все возможные состояния блокировки, в которые может попасть программа, что неудивительно, эквивалентно проблеме остановки.
Существуют способы частичного «решения» тупиковых ситуаций в сложной системе путем наложения другого уровня поверх блокировки (например, определенного порядка сбора данных), но эти методы не всегда применимы.
Почему это эквивалентно проблеме остановки:
Представьте, что у вас есть две блокировки, A и B, и два потока, X и Y. Если поток X имеет блокировку A и хочет также блокировку B, а поток Y имеет блокировку B и тоже хочет A, тогда у вас тупик.
Если и X, и Y имеют доступ как к A, так и к B, то единственный способ гарантировать, что вы никогда не попадете в плохое состояние, - это определить все возможные пути, которые каждый поток может пройти через код, и порядок, в котором они может приобретать и удерживать замки во всех этих случаях. Затем вы определяете, могут ли два потока когда-либо получить более одной блокировки в другом порядке.
Но определение всех возможных путей, которые каждый поток может пройти через код (в общем случае) эквивалентно проблеме остановки.
Почему невозможно? Конечно, производительность может снизиться из-за чрезмерной блокировки, но это не означает, что это проблема остановки! Или мне что-то здесь не хватает?
Много-много месяцев назад я помогал консультанту нашей компании, который внедрял очень сложную рельсовую систему для перемещения корзин с металлическими деталями в доменную печь с температурой 1500 градусов и обратно. Сама трасса представляла собой довольно сложную «мини-железнодорожную станцию» в цехе, которая в паре мест пересекалась. Несколько моторизованных поддонов перемещали корзины с деталями по расписанию. Очень важно, чтобы дверцы топки были открыты как можно короче.
Поскольку завод был полностью запущен, консультант не мог запустить свое программное обеспечение в «реальном времени», чтобы проверить свои алгоритмы планирования. Вместо этого он написал красивый графический симулятор. Когда мы наблюдали, как виртуальные поддоны перемещаются по его экранной схеме дорожек, я спросил: «Как вы узнаете, есть ли у вас какие-либо конфликты в расписании?»
Его быстрый ответ: «Легко - моделирование никогда не прекратится».
мета-части - вот почему мне потребовалось некоторое время, чтобы понять, что его система rails НЕ была веб-приложением на Ruby.
Мета! Мне пришлось перечитывать свой пост несколько раз, пока я не понял, что вы имели в виду! Конечно же, MetaL!
Это по-прежнему проблема шейдеров в приложениях на GPU. Если шейдер имеет бесконечный цикл (или очень длинный расчет), должен ли драйвер (по прошествии некоторого времени) остановить его, убить фрагмент или просто дать ему поработать? Для игр и других коммерческих материалов первое, вероятно, вам нужно, но для научных вычислений / вычислений на GPU вам нужно второе. Хуже того, некоторые версии окон предполагают, что, поскольку графический драйвер некоторое время не отвечал, он убивает его, что искусственно ограничивает вычислительную мощность при выполнении вычислений на графическом процессоре.
Нет API для приложения, чтобы контролировать, как драйвер должен вести себя или устанавливать тайм-аут или что-то в этом роде, и, конечно же, у драйвера нет способа узнать, завершится ли ваш шейдер или нет.
Не знаю, улучшилась ли эта ситуация в последнее время, но хотелось бы знать.
Однажды я работал над интеграционным проектом в области банкоматов (ATM). Клиент попросил меня сгенерировать отчет из моей системы о транзакциях, отправленных переключателем страны, которые не были получены моей системой !!
Пример 1. Сколько страниц в моем отчете?
Когда я учился программировать, я играл с созданием инструмента для распечатки красивых отчетов на основе данных. Очевидно, я хотел, чтобы он был действительно гибким и мощным, чтобы генератор отчетов завершал работу всех генераторов отчетов.
В итоге определение отчета оказалось настолько гибким, что было завершено по Тьюрингу. Он мог смотреть на переменные, выбирать между альтернативами, использовать циклы для повторения вещей.
Я определил встроенную переменную N, количество страниц в экземпляре отчета, поэтому вы можете поместить строку с надписью «page n of N» на каждой странице. Я сделал два прохода: первый для подсчета страниц (во время которого N было установлено равным нулю), а второй - для их фактического создания с использованием N, полученного на первом проходе.
Иногда первый проход вычислял N, а затем второй проход генерировал другое количество страниц (потому что теперь ненулевое N изменило бы то, что сделал отчет). Я пробовал делать пассы итеративно, пока N не успокоился. Затем я понял, что это безнадежно, потому что что, если это не успокоится?
Тогда возникает вопрос: «Могу ли я хотя бы обнаружить и предупредить пользователя, если итерация никогда не установит стабильное значение количества страниц, создаваемых их отчетом?» К счастью, к этому времени я заинтересовался чтением о Тьюринге, Геделе, вычислимости и т. д. И установил связь.
Спустя годы я заметил, что MS Access иногда печатает «Страница 6 из 5», что поистине чудесно.
Пример 2: компиляторы C++
В процессе компиляции шаблоны расширяются. Определения шаблонов можно выбрать из нескольких специализаций (достаточно хороших, чтобы служить «условием»), и они также могут быть рекурсивными. Итак, это полная по Тьюрингу (чисто функциональная) метасистема, в которой определения шаблонов - это язык, типы - значения, а компилятор - действительно интерпретатор. Это был несчастный случай.
Следовательно, невозможно изучить любую данную программу C++ и сказать, может ли компилятор в принципе завершить работу при успешной компиляции программы.
Поставщики компиляторов обходят это ограничение, ограничивая глубину стека рекурсивного шаблона. Вы можете настроить глубину в g ++.
«Как вы можете уверить меня, что ваш код на 100% не содержит ошибок?»
Я скептически отношусь к тому, что это эквивалентно проблеме остановки. Тривиальный код может быть доказан математически без ошибок.
Несколько лет назад я помню, как читал обзор (кажется, в журнале Byte) продукта под названием Basic Infinite Loop Finder или BILF. Предполагалось, что BILF просканирует ваш исходный код Microsoft Basic и найдет все петли, которые не завершились. Он утверждал, что может найти любые бесконечные циклы в коде.
Рецензент был достаточно сообразителен, чтобы указать, что для того, чтобы эта программа работала во всех случаях, она должна решить проблему остановки, и зашел так далеко, что предоставил математическое доказательство того, почему она не может работать во всех случаях.
В следующем выпуске они опубликовали письмо от представителя компании, в котором объяснялось, что проблема будет исправлена в следующем выпуске.
Обновлять: Я наткнулся на изображение статьи на imgur. Я вспомнил не тот журнал. Это были творческие вычисления, а не байты. В остальном это почти то же самое, что я запомнил.
Вы можете увидеть его версию в высоком разрешении на imgur.
Это весело! Есть ли где-нибудь копия?
Единственные результаты в Google - это этот пост и ссылки на него.
Это было бы в конце 70-х или начале 80-х. Интернет тогда был не так популярен ;-)
Когда компания BILF перестанет вести бизнес?
Из Функциональный обзор визуального редактора (Eclipse):
The Eclipse Visual Editor (VE) can be used to open any .java file. It then parses the Java source code looking for visual beans. ...
Some visual editing tools will only provide a visual model of code that that particular visual tool itself has generated. Subsequent direct editing of the source code can prevent the visual tool from parsing the code and building a model.
Eclipse VE, however, ... can either be used to edit GUIs from scratch, or from Java files that have been 'hardcoded' or built in a different visual tool. The source file can either be updated using the Graphical Viewer, JavaBeans Tree or Properties view or it can be edited directly by the Source Editor.
Может, мне пока стоит остаться с Матиссом.
Несвязно, вот кто-то просить проблема остановки в Eclipse.
Честно говоря, область применения VE довольно ограничена, и она, вероятно, не сойдет с ума от таких хитрых вещей, как отражение. Тем не менее, претензия на создание графического интерфейса пользователя из java-файла Любые кажется бесполезной.
Я нашел газету Беркли: Looper: облегченное обнаружение бесконечных циклов во время выполненияhttp://www.eecs.berkeley.edu/~jburnim/pubs/BurnimJalbertStergiouSen-ASE09.pdf
LOOPER может быть полезен, поскольку большинство бесконечных циклов - тривиальные ошибки. Однако этот документ даже не упоминает о проблеме остановки!
Что они говорят о своих ограничениях?
[LOOPER] typically cannot reason about loops where non-termination depends on the particulars of heap mutation in every loop iteration. This is because our symbolic execution is conservative in concretizing pointers, and our symbolic reasoning insufficiently powerful. We believe combining our techniques with shape analysis and more powerful invariant generation and proving would be valuable future work.
Другими словами, «проблема будет исправлена в следующем выпуске».
Обнаружение цикла выполнения, когда пространство состояний известно и зафиксировано, фактически разрешимо; см. cs.stackexchange.com/a/11646/2242.
разве системы статического типа не проверяют только тип переменной, а не ее значение? Я думаю, что ваш класс неправильно сформулировал вопрос, ожидая, что средство проверки статического типа отклонит ошибки времени выполнения во время компиляции.