Компиляторы в песочницах и сравнение программ
Продолжаем тему “про алгоритмы“, на примере циклов и компиляторов. Запись алгоритма на языке высокого уровня (ЯВУ) – это некоторый пересказ того, что должно выполняться вычислителем. На то он и язык высокого уровня. При этом, обычно, вычислителем исполняется не запись на ЯВУ, а некоторый результат преобразования компилятором. То есть, алгоритм, казалось бы, один. Но, во-первых, может быть много разных записей этого алгоритма на многих разных языках. Даже если удалось удачно определить, что означает фраза “две программы реализуют один алгоритм” (отдельная проблема), то, при минимально содержательном определении, машинное доказательство того, что разные записи соответствуют одному алгоритму – составит большую трудность (в общем виде соответствующее сравнение вообще неразрешимо, но это другая история, а несложные конечные автоматы, обычно, как-то эффективно сравнить всё же можно). Трудности на этом направлении гарантируют, что даже если реализован некий автоматический перевод с одного ЯВУ на другой, это вовсе и не означает, что результат не менее автоматического анализа переведённой программы применим к программе исходной.
Другими словами, если у вас есть добротный анализатор для языка Fortran (для языка, не для алгоритмов), то он вовсе не обязательно эффективен для программ на Haskell, которые транслированы (ну, предположим) в код на Fortran: проверяться всё равно будет Fortran-программа. Это сильно сужает возможности по созданию полезных универсальных “анализаторов кода на ЯВУ”.
Во-вторых, на практике записи алгоритма обрабатывают разные компиляторы, которые переводят его в разный машинный код для разных вычислителей – то есть, для разной аппаратуры. Можно ли тут что-то вообще доказывать о программе, выбросив из рассмотрения компилятор и аппаратуру? Вряд ли. Вообще, а если две реализации некоторого алгоритма дают одинаковый вывод на эталонном наборе входных данных, то означает ли это, что и в рамках реализации записан один и тот же алгоритм? Не обязательно, но степень соответствия действительности кодирования тут сильно зависит от строгости определений.
Предположим, что на процессоре “Имярек-7” команда MOV (“копирующая/перемещающая какие-то данные”) не просто сама по себе Тьюринг-полная (как в x86), но ещё и содержит “особенность” реализации, приводящую к тому, что число 0xFFFFFFFF превращается в 0x0, если сделать два MOV подряд из ОЗУ в регистр REG1. Поэтому, чтобы какие-то детали гарантировать относительно программы и реализации алгоритма, нужно в рассмотрение включить и аппаратные особенности. Сделать это автоматическим способом непросто. Отчасти поэтому-то и появляются всякие разные трансляции в “байт-код”, пригодный для исполнения “песочницей” (например, “Java-машиной”, если хотите): в такой конфигурации можно построить какие-то формальные описания и для языка, и для “машины”, которая его интерпретирует. Можно показать, что тут, при следовании некоторым принципам, всё разрабатывается безопасно (и это, действительно, так, но далеко не в общем случае).
Если же что-то всё же пошло не так, то оно пошло из-за дефекта реализации “машины”, а эта реализация находится за пределами модели. Это удобное сужение темы: если у вас код вылезает из песочницы, то проблема существует над песочницей, а не в ней; песочница хороша по определению: существовала бы проблема в ней – вылезать и не требовалось бы, да.
Представьте, что сложную схему отношений между записями алгоритмов, разными языками высокого уровня, компиляторами и аппаратурой зарисовали в виде графа, где направленные рёбра – это стрелки, обозначающие преобразование кода. Например, перевод с одного ЯВУ на другой. Или перевод в машинный код. Или перевод в подмножество состояний конечного автомата, соответствующего процессору. Тут за каждой стрелкой скрываются целые наборы “схлопывающих” и забывающих отображений, при которых различные способы представлений на стороне начального узла все переводятся в единственный способ на стороне узла конечного (такое вот “ядро” отображения). Например, циклы for, while, do – все схлопываются в сочетание операторов if, потому что только так позволяет записывать целевой язык. Тогда базовые логические преобразования, записываемые формально, могут и совпадать, но вот большое количество возможностей по внесению особенностей и ошибок в исходный код – останется вне пределов доступности для того или иного анализатора, схлопнувшись, что называется, до неразличимости.
Адрес записки: https://dxdt.ru/2024/10/09/14017/
Похожие записки:
- Chrome и проверка веб-страниц в браузере
- Сертификаты с коротким сроком действия и централизация
- Устройства Apple и Starlink
- Кодирование в рунах
- Скобки и минус девять в Google-таблице
- Метки в текстах LLM и целевое влияние на результат
- Шифр "Кузнечик" на ассемблере arm64/AArch64 со 128-битными инструкциями
- Распознавание TLS-клиентов в трафике
- URL и ссылки в письмах
- Реплика: внешние капча-сервисы и сегментация
- Занятный замок Fichet 787
Написать комментарий