Комментарии 11
К сожалению, в силу неразрешимости проблемы останова, практически полезные результаты получить таким путём нельзя.
Опять комменты крадут, да что ж такое-то?! :-)
Нагуглилось, что немножко можно https://arxiv.org/pdf/1711.04422.pdf. Вокруг этой работы красивое облако: https://www.connectedpapers.com/main/978f7a92f93f92b6fc59db199184ed104937942d/Souper%3A-A-Synthesizing-Superoptimizer/graph
Для небольших машин Тьюринга (2 символа, число состояний меньше 5) проблема останова разрешима, так как известно значение BB (busy beaver: максимальное число шагов, которая машина может сделать до остановки). Если программа работает большее число шагов, значит она никогда не остановится.
Но - да, с практической точки зрения толку от этого нет, так как BB(n) (где n - число состояний машины) растёт быстрее любой функции вычислимой на машине Тьюринга. Начало последовательности BB(n): 4, 6, 13, ≥4098, >10↑↑15, а что дальше - неизвестно.
Последнее значение записано в стрелочной нотации Кнута и обозначает 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10.
Впрочем, при супероптимизации с той же практической точки зрения можно отбрасывать программы выполняющиеся дольше какого-то времени или использующие большее количество памяти, чем нужно.
Близкая задача для решения опубликованная математиком из г. Иванова. :)
Программа поиска Fort-программы по тестам
P.S. Используются генетические алгоритмы.
Здесь можно многое доработать
Список стоило начать с "взять чо-нить побыстрее питона и получить нахаляву (без изменения алгоритма) ускорение раз в сто", после чего добавить многопоточности и ускориться ещё раз в 16+ (в зависимости от кол-ва ядер).
"Настоящий" супероптимизатор штука непрактичная, так как действительно все перебрать нереально. Но можно прикрутить различные алгоритмы сокращения перебора и получить тоже интересные результаты. Это уже не будет супероптимизатором (нет гарантии оптимальности), но тоже интересно, и гораздо более реально.
В качестве магистерской работы в универе я писал оптимизатор, который использовал генетические алгоритмы для оптимизации кода на низкоуровневом языке (у меня были бэкенды к байткоду JVM, очень сокращенному набору ассемблера x86 и какой-то версии языка пиксельных шейдеров). Получались интересные результаты, когда сперва не понимаешь вообще, почему этот код эквивалентен исходному.
Писал про это на хабр в 2015 - https://habr.com/ru/articles/265195/
Проблема останова это прям проблема, и произвольную программу конечно таким не обработаешь. Но для генерации локальных оптимизаций для компилятора вполне рабочий вариант. Приходится правда повозиться с верификацией, чтобы доказать что новый и исходный фрагменты кода действительно генерируют всегда эквивалентные результаты. Но это можно свести к решению задачи SMT, и для этого есть готовые инструменты.
Прошу помощи зала: помнится, на Хабре было несколько похожих статей, где рассматривался вопрос поиска некоего алгоритма брутфорсом опкодов миниатюрной ВМ. Так вот, не могу найти статью, в которой рассказывалось, как искалась "программа", помещавшаяся в 64-битное число (внутри которого кодировались инструкции стековой машины в обратной польской нотации), собственно перебором всех 64-битных чисел. Может, кто-то помнит эту статью или хотя бы волшебные слова из неё?
Мой первый супероптимизатор