Специализация функциональных программ методами суперкомпиляции

В семидесятых годах В. Ф. Турчин предложил ряд идей по автоматическому преобразованию программ, которые назвал суперкомпиляцией1. Он поставил задачу создать инструменты для наблюдения за операционной семантикой программы, когда фиксирована функция F, вычисляемая этой программой.

Результатом таких наблюдений должно стать построение нового алгоритмического определения некоторого продолжения функции F. Новый алгоритм строится с целью более быстрого вычисления F на конкретных аргументах.

Позже, рядом авторов эти идеи В. Ф. Турчина изучались и в той или иной мере доводились до алгоритмов.

В диссертации разработан и реализован экспериментальный суперкомпилятор, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Обсуждению разработанных методов и алгоритмов, их исследованию и посвящена данная работаавтор также рассматривает структуру и принципы работы построенного преобразователя программ. Показывается большое количество результатов преобразований реализованным суперкомпилятором и комментируются эти примеры. Основные принципы.

По нашему мнению, название выбрано весьма неудачно. Суперкомпиляция не является компиляцией, подобно многозначной функции, которая не является функцией (или векторному полю, которое не является полем). Английский вариант «supercompilation» немного более премлсм, и было бы правильно «переводить» его словом «надкомгтиляция». построения суперкомпилятора SCP4 обсуждались с Валентином Фёдоровичем Турчиным. Более того, он инициировал и поддерживал эту работу.

Само понятие «более быстрого вычисления», безусловно, требует уточнения. В диссертации имеется в виду некоторое логическое время, хотя на практике часто оно отражает физическое время. Вопрос о соотношении этих времён рассматривается в одном из разделов данной диссертационной работы.

Языком реализации оптимизатора SCP4 также является РЕФАЛ-5. Язык программирования РЕФАЛ (В. Ф. Турчин [69], [74]) -функциональный язык первого порядка с аппликативной (вызовы по значению) семантикой. Грубо говоря, программа на РЕФАЛе представляет собой систему переписывания термов. Предложения упорядочены, и выбор предложения происходит посредством сопоставления с образцом. Для построения термов используются два конструктора. Первый конструктор — конкатенация2 — бинарный, ассоциативный и используется в инфиксной записи, что позволяет опускать его скобки. Знак пробела служит для обозначения этого конструктора, Второй конструктор одноместный. Синтаксически он обозначается только его скобками, то есть без имени. Функциональный вызов оформляется угловыми скобкамипричём, имя вызываемой функции записывается непосредственно после открывающей скобки. В РЕФАЛе все функции являются одноместными, термы принято называть выражениями. Пустая последовательность принадлежит к множеству базисных константных термов и называется.

2 Приписывание. пустым выражением". По определению, это единица конкатенации (левая и правая). Все остальные базисные константные термы называются «символами». Базисные неконстантные термы (переменные): е.name, s.name и t.name. Значением е-переменной может быть любое константное выражение, значением s-переменной — любой символ, значением t-переменной — любой символ или выражение в круглых скобках (указанный выше одноместный конструктор). Ассоциативность конкатенации делает множество РЕФАЛ-термов более выразительным, по сравнению с множеством LISP-термов.

Объект исследования.

Определение 1 Реализацией функционального языка программирования К назовём четвёрку (P, D, U, T), где множество Р называется множеством программ, множество D называется множеством^{.-данныхчастично} рекурсивные функции U PxD i—" D и Т: Р х D > N называются соответственно универсальной функцией (или семантикой) и сигнализирующей функцией времени языка К. Здесь N — множество натуральных чисел.

Ниже мы будем использовать обозначение р (х) как сокращение для U (p, x).

Пусть дана реализация функционального языка программирования 5? = (Р, 0,11,1), где D = Jn€NMn для некоторого множества М. Пусть программа р (х, у) из Р, реализует функцию3 F (x, у): X xY ь-" Z, где X С D. Y С D, Z С D. Зафиксируем значение первого аргумента этой функции 6 X. В задаче специализации требуется построить другую программу.

3То есть именно функцию, а не частичную функцию. q (y) € P такую, что.

Vye y.(q (y) — р (х0,у)) Л (T (q, y).

Программу q называют остаточной программой. Содержательная задача состоит в построении оптимальной q (по времени исполнения). Таким образом, программа q представляет некоторое продолжение функции F (xQ, y) по второй компоненте.

Выше приведена частная формулировка общей задачи специализации программ. В общей постановке требуется проспециализировать программу по данному контексту применения самой программы или, более широко, её подпрограмм. Другим простым примером контекста является композиция применения двух подпрограмм h и g, реализующих соответственно функции Н: X н-> K, G: Image (Я) х У i—> Z здесь X. У, Z — подмножества множества D. Пусть программа р (х, у) есть композиция h и g: р (х, у) = g (h (x), у). В этом случае требуется построить остаточную программу q (x, y) такую, что х е ХУу е y.(q (x, у) = р (х, у)) A (T (q, x, y) < Т (р, х, у)).

То есть снова требуется построить оптимальную программу, определяющую продолжение функции F (x, y), представленную композицией g (h (x), у).

Разные уточнения понятия оптимальности определяют конкретные аппроксимации задачи специализации как таковой.

В данной работе под программами понимаются программы на функциональных языках программирования.

Актуальность темы

Технология программирования естественно развивается в сторону оперирования понятиями задачи, которая стоит перед программистом, а не понятиями универсального прибора, на котором программа будет исполняться. Это стимулирует развитие языков программирования высокого уровня позволяющих адекватно отражать объектную область задачи. К таким языкам, например, относятся функциональные и логические языки (LISP, REFAL, PROLOG, HASKELL, ML, SCHEME и др.), а также различные языки, специализированные на конкретную область их применения. С другой стороны, аппаратная реализация современных широко используемых ЭВМ поддерживает фон-неймановскую модель вычисленийчто приводит к неэффективной реализации таких языков — посредством интерпретации — более того, часто не прямой, а косвенной — через другую интерпретацию. К подобной неэффективности приводит и любое структурное программирование само по себеибо его целью является создание гибких, легко понимаемых и изменяемых программ. Всё чаще программы вычисляются другими программами, а потому естественно ожидать, что первые будут содержать простейшие структуры, ведущие к накладным расходам, которые никогда бы не допустил квалифицированный программист.

Методы автоматической оптимизации структурированных программ высокого уровня (а не программ отшлифованных профессиональными программистами на языках программирования низкого уровня) и призваны предоставить свободу развития новым технологиям программирования.

Одним из активно развивающихся здесь направлений является автоматическая специализация программ. Предположим, что вы купили дистрибутив операционной системы LINUX. В момент её установки на вашем компьютере вы должны указать его аппаратные характеристики, то есть эти характеристики являются аргументами программы-установщика. Возникает желание максимально настроить LINUX на ваше железо, ибо в другом контексте он вам не понадобится. В этом и состоит задача специализации. Операционную систему вы устанавливаете однажды и, потому, стоит предложить поработать автоматическому специализатору, даже если его работа достаточно продолжительна во времени.

Суперкомпияция есть набор методов автоматической специализации программ, написанных на функциональных языках.

Идеи лежащие в основе суперкомпиляции, с одной стороны, существенно мощней идей широко распространённой техники специализации, известной как частичные вычисленияс другой стороны, методы суперкомпиляции намного менее разработаны, чем методы частичных вычислений. И, до недавнего времени, не существовало ни одного экспериментального специализатора-суперкомпилятора, с которым могли бы экспериментировать не только его разработчики, но и иные пользователи. По существу, оставался открытым вопрос о принципиальной возможности построения полностью автоматического суперкомпилятора. Данная диссертационная работа даёт положительный ответ на этот вопрос.

Цели работы. Диссертационное исследование было направлено на решение следующих основных задач:

1. Построить и реализовать новые алгоритмы специализации функциональных программ, основанные на методах суперкомпиляции. Упростить и довести до алгоритмов полуавтоматические процедуры, представленные в работах В. Ф. Турчина [65], [67], [68], [70], и/или улучшить качественные характеристики этих процедур с точки зрения построения более эффективных остаточных программ.

2. Разработать и довести до алгоритмов методы построения выходных форматов функций-подпрограмм.

3. Построить экспериментальный автоматический супсркомпилятор, с которым могли бы экспериментировать посторонние пользователи. Изучить характеристики этого суперкомпилятора.

Общая методика работы. Большая часть идей, используемых в диссертации, хорошо известна в рамках суперкомпиляции. Основным инструментом анализа и преобразований программ является метаинтерпретация этих программ. Преобразования производятся по ходу дела метаинтерпретации (в режиме on-line) и остаточная программа строится исключительно на основе этой интерпретации, а не посредством пошаговой чистки исходной (преобразуемой) программы. Используемый параметрический язык описания конфигураций метадерева возможных вычислений является языком первого порядка.

Предметной областью нашего суперкомпилятора SCP4 является функциональный язык программирования РЕФАЛ-5. Этот же язык является языком реализации суперкомпилятора. Большинство алгоритмов работают в терминах внутреннего языка РЕФАЛ-графов, который ориентирован на адекватное описание временной эффективности. Это язык более низкого уровня по отношению к РЕФАЛу, но работает с теми же данными. Тем не менее, некоторые свойства преобразуемых алгоритмов формулируются в понятиях самого РЕФАЛа и соответствующие алгоритмы используют эти понятия.

Идеи методов построения выходных форматов компонент факторизации метадерева потенциальных вычислений, глобального анализа и распознавания мономов конкатенации (как и само понятие этих мономов) полностью оригинальны. После глобального анализа компоненты факторизации, производится повторная специализация этой компоненты по свойствам, выявленным глобальным анализом.

После основной стадии преобразований, отдельным проходом производится чистка входных и выходных формальных параметров, излишних вызовов функций.

Транслятор из языка РЕФАЛ-графов в язык С реализован А. П. Конышевым [7]. Часть РЕФАЛ программ, которые используются в дессертации в качестве тестовых примеров для суперкомпилятора SCP4, принадлежат А. В. Корлюкову [8], [10], [11]. Основные результаты.

1. Разработаны и реализованы аппроксимирующие алгоритмы распознавания частично рекурсивных константных функций, частично рекурсивных функций проекции.

2. Па основе полуавтоматических процедур обобщения параметризованных конфигураций, представленных в работах.

В. Ф. Турчина [65], [67], [68], [70], разработаны и реализованы алгоритмы обобщения параметризованных конфигураций. Улучшены качественные характеристики этих алгоритмов с точки зрения построения более эффективных остаточных программ.

3. Разработан и реализован алгоритм построения выходных форматов компоненты факторизации F метадерева возможных вычислений в режиме online (по ходу дела суперкомпиляции) — что позволяет сразу использовать построенный формат для специализации по нему как других компонент-функций, вызывающих функцию F, так и самой функции F.

4. Предложено понятие частично рекурсивного монома конкатенации. Доказана теорема о достаточном условии частично рекурсивного монома конкатенациина основании этой теоремы разработан и реализован алгоритм распознавания частично рекурсивных синтаксических мономов конкатенации. Показано, что на некоторых примерах этот алгоритм способен понижать временную сложность программы с экспоненциальной до константной 0(1).

5. Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация суперкомпилятора доступна на Web-странице в режиме on-line [90].

6. Исследованы характеристики супсркомпилятора. SCP4.

Научная новизна. Все основные результаты являются новыми. В частности, реализованный суперкомпилятор SCP4 является первым реальным экспериментальным полностью автоматическим специализатором программ, построенным на основе методов суперкомпиляции.

Практическая и теоретическая ценность. Представленные в диссертации алгоритмы распознавания синтаксической мономиальности программ и вычисления выходных форматов компонент факторизации дерева потенциальных вычислений могут быть полезны для решения классических задач самоприменеиия специализаторов, поставленных А. П. Ершовым [28], Ё. Футамурой [29] и В. Ф. Турчиным [65], [67]. В одном из разделов диссертационной работы подробно рассматриваются возможности алгоритма распознавания синтаксических мономов для понижения порядка временной сложности остаточных программ в задачах самоприменсния. Данная диссертационная работа даёт положительный ответ на долго стоявший открытым вопрос о принципиальной возможности построения полностью автоматического суперкомпиляторачто является значительным шагом в направлении внедрения технологии суперкомпиляции в практику программного обеспечения современных компьютеров. В диссертации показано, что суперкомпилятор SCP4 может использоваться для автоматической верификации коммуникационных протоколов, посредством специализации их программных моделей. Например, были успешно верифицированы следующие cache coherence протоколы: IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, Synapse N+l, DEC Firefly, Berkeley, Xerox PARC Dragon.

Апробация работы. Результаты работы докладывались и обсуждались на следующих конференциях:

• Международный Software Engineering симпозиум, Китай, 2001.

• Международный симпозиум Partial Evaluation and Semantics-Based Program Manipulation в Азии (Asia-PEPM), Япония, 2002.

• Международный симпозиум Computer Science in Russia, Екатеринбург, 2007.

• Международная конференция Perspectives of System Informatics посвященная памяти Андрея Ершова, Новосибирск, 2003.

• Международная конференция Program Understanding, Новосибирск-Алтай, 2003.

• Международная конференция Information Systems Technology and its Applications, Харьков, 2003.

• Международная конференция «Программные системы: теория и приложения», Переславль-Залесский, 2004.

• Международная конференция Reachability Problems, Финляндия, 2007.

• Российско-Французский коллоквиум Some mathematical problems of technological importance, Laboratoire Poncelet, Московский Независимый Университет, 2005.

• Научные семинары ИПС РАН, ИПМ РАН, ИСП РАН, ИППИ РАН, Institute of Software Китайской Академии Наук, университетов г.

Ухань (Wuhan University)(Китай), г. Токио (Waseda University), г.

Ливерпуль (The University of Liverpool).

Публикации. Основные результаты диссертации опубликованы в 15 работах [77], [78], [79], [80], [81], [82], [83], [84], [85], [86], [87], [88], [89], [90], [91], перечисленных в конце списка литетатуры. Работа [78] опубликована в издании, входившем в перечень ВАК на момент публикации и имеющемся в перечне ВАК на данный момент. Работа [79] является монографией автора диссертации.

Структура и объём работы. Диссертация объёмом 322 страницы состоит из введения, двадцати одной основной главы, которые разбиты на части и разделы, заключения и приложения. Каждая глава и каждая часть начинаются с кратких введений, выделенных курсивом. Каждая глава заканчивается заключающей частью, в которой кратко сформулированы результаты данной главы. В главе «Результаты» сформулированы основные результаты диссертационной работы. Список цитируемой литературы состоит из 91 наименования.

1. Разработаны и реализованы аппроксимирующие алгоритмы распознавания частично рекурсивных константных функций, частично рекурсивных функций проекции. Показано, что на некоторых примерах эти алгоритмы способны понижать временную сложность программы.

2. Предложено понятие частично рекурсивного монома конкатенации.

3. Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация супер компилятора доступна на Web-странице в режиме online 90.