Меня интересуют проверенные компиляторы, формализованные в теории типов Мартина-Лёфа, т.е. Coq / Agda. На данный момент я написал небольшой игрушечный пример. Тем самым я могу доказать, что мои оптимизации верны. Например, могут быть исключены дополнения с нуля, например, выражения типа «x + 0».
Существуют ли оптимизации, которые сложно выполнить с помощью обычного компилятора, которые могут служить хорошим примером? Можно ли доказать определенные свойства программы, которые допускают оптимизации, которые невозможно выполнить с обычным компилятором? (т.е. без вывода, который возможен с доказательством теоремы)
Мне были бы интересны идеи или примеры, а также ссылки на эту тему.
Смежный вопрос: доказательства корректности компилятора
редактирование: как Цуёси замечательно выразил в комментариях: я ищу методы оптимизации, которые сложно реализовать, если компилятор написан на (скажем) C, но проще в реализации, если компилятор написан на (скажем) Coq. Поскольку Agda компилируется в C (через haskell), можно делать все, что возможно в Agda, также и в C. Вероятно, единственное преимущество средств доказательства теорем, таких как Coq / Agda, заключается в том, что компилятор и оптимизации могут быть проверены.
edit2: В соответствии с предложением Vijay D я пишу то, что я прочитал до сих пор В основном я сосредоточился на Ксавье Леруа и проекте CompCert в INRIA (я думаю, что есть статья на 80 страниц, которая хорошо читается). Второй интерес был к работе Антона Сетцера по интерактивным программам. Я думал, что, возможно, его работа может быть использована для доказательства свойств программ ввода-вывода и бисимуляции программ ввода-вывода. Спасибо за упоминание Сьюэлл. Я слышал его выступление «Сказки из джунглей» в ICFP и читал, возможно, 2-3 его статьи. Но я специально не смотрел на его работу и работу его соавторов.
Я еще не выяснил, с чего начать или искать статьи по оптимизации компиляторов; например, какие оптимизации было бы интересно посмотреть в настройках проверенного компилятора.
Ответы:
В этой статье Ив Берто, Бенджамина Грегуара и Ксавье Леруа создается оптимизирующий компилятор для C-подобного языка, основанный исключительно на спецификации Coq. некоторые из этой технологии, по- видимому , используемые в компиляторе CompCert C .
Структурированный подход к доказательству оптимизации компилятора на основе анализа потока данных
в нем рассматривается правильность двух оптимизаций: постоянное распространение (CP) и исключение общих подвыражений (CSE), раздел 4. Эти оптимизации являются более продвинутыми, чем те, которые связаны с компилятором (ами), не основанными на Coq для того же языка. см., например, этот сравнительный график по сравнению с GCC. (Компилятор на основе Coq предположительно медленнее компилируется, хотя это редко упоминается!)
однако в конце статьи они отмечают, что в реальных компиляторах есть некоторые оптимизации компиляторов, которые не могут быть смоделированы в их рамках.
улучшенная оптимизация - не единственный элемент рассмотрения здесь, другой аспект заключается в том, что логика оптимизации компилятора может быть подвержена тонким дефектам, особенно из-за ее сложной природы. На протяжении многих лет было обнаружено, что у gcc есть ошибки в многочисленных логических процедурах оптимизации. например, ошибка gcc?
источник
Это эквивалентно расширению проверки типов для предоставления некоторых свойств программы оптимизатору. Я полагаю, что Tsuyoshi Ito прав, и вы, возможно, немного ошибаетесь в отношении Coq. Это отличный инструмент для обеспечения безошибочного компилятора, но в случае, который вы описываете, он не предоставляет больше возможностей для статического анализа.
Единственное, что я могу подумать об усилении статического анализа с помощью Coq, - это снабдить ваш язык утверждениями, содержащими некоторые написанные пользователем доказательства. - Если сам компилятор будет переведен на язык, включающий перо для динамической проверки типов, и если пользовательские доказательства будут преобразованы в функции, то можно будет применять эти функции в качестве предварительно требуемых свойств для некоторых подтипов или оптимизаций. - Это действительно даст больше возможностей компилятору.
Однако, насколько я вижу, это было бы весьма полезно для усиления подтипов. - Сложно заставить программиста знать, какое свойство в каком месте будет полезным для оптимизатора.
источник