Содержание к диссертации
Введение
1 Анализ результатов диссертации в контексте исследований в области специализации программ 24
1.1 О двух постановках задачи специализации 25
1.2 Обзор результатов в области специализации программ . 27
1.3 Исторический обзор развития методов суперкомпиляции . 34
2 Схема структуры преобразователя программ SCP4 45
3 Язык параметров 55
3.1 Параметризованные множества данных 55
3.2 Параметризованные множества полей зрения (стеков) и РЕФАЛ-выражений 58
4 Язык РЕФАЛ-графов 60
4.1 Синтаксис 60
4.1.1 Синтаксис входного подмножества 63
4.2 Семантика 63
4.3 Язык РЕФАЛ-5 и язык РЕФАЛ-графов 66
4.3.1 О неравномерности шагов РЕФАЛ-машины 66
4.3.2 Дерево отождествления в языке РЕФАЛ-графов 70
5 Прогонка 72
5.1 Общая структура прогонки 73
5.2 Перестройка стека функций 84
5.3 Стратегия выбора входного формата 85
5.4 К вопросу о целях преобразований 86
6 Свёртка 91
6.1 Вложение 92
6.2 Стратегия обхода дерева при факторизации 97
6.3 Обобщение 99
6.3.1 Отношение «похожести» 101
6.3.2 Обобщение конфигураций 107
6.3.3 Обобщение параметризованных выражений 112
6.3.4 Обобщение и построение «отрицательной» информации . ИЗ
6.3.5 Стратегия обхода метадерева при обобщении 117
6.3.6 Обнинское условие и транзитные вершины 118
6.4 К вопросу о целях преобразований 120
6.4.1 Изменение местности параметризованной среды при
её обобщении 124
7 Развёртка 129
7.1 Стратегия развития дерева 130
7.2 Стратегии развития стека функций 130
7.3 К вопросу о целях преобразований 132
8 Подграф - компонента факторизации 135
9 Чистка экранируемых ветвей 137
10 Глобальный анализ 139
10.1 Анализ в терминах языка РЕФАЛ-графов 140
10.1.1 Пустые подграфы 141
10.1.2 Выходные форматы 143
10.1.3 Графы определяющие константу 146
10.1.4 Проекции 147
10.2 Анализ в терминах языка РЕФАЛ 147
10.2.1 Тождественность 149
10.2.2 Мономы конкатенации 152
10.2.3 Стратегия выбора гипотезы мономиальности 162
10.2.4 Частичные выражения 165
10.3 Чистка поглощаемых ветвей 168
Том II 170
11 Использование результатов глобального анализа 171
11.1 Одношаговые подграфы 171
11.2 Пустые подграфы 172
11.3 Рекурсивные подграфы. Повторная специализация 172
11.4 Квази-дистрибутивность подзадачи 176
11.4.1 Правая квази-дистрибутивность 177
11.4.2 Левая квази-дистрибутивность 179
11.5 К вопросу о целях преобразований 180
12 Чистка входных, выходных формальных параметров и вызовов функций 188
13 Чистка повторных определений 193
13.1 Глобальность базисных конфигураций внутри задачи и по задачам 193
13.2 Повторные определения 194
14 Неадекватная выразимость результата преобразований средствами РЕФАЛа-5 198
15 Разметка свойств переменных и компиляция в Си (или в язык сборки) 202
15.1 Уменьшение числа копирований 202
15.2 Хвостовая рекурсия 205
16 Поднятие параметра (уточнение языка параметров). О синтаксисе входных точек 208
16.1 Постановка задач на специализацию 208
16.2 Подтипы параметров 212
16.2.1 Уточнение прогонки 213
16.2.2 Уточнение свёртки 217
16.3 Синтаксические мономы в задаче самопримеиения 217
16.4 Язык MST-схем 220
17 Несколько примеров преобразований 227
17.1 Простейшие примеры 227
17.2 Специализация самоописания РЕФАЛа 242
17.3 Другие эксперименты 259
18 О соотношении сложности 262
18.1 Анализ двух примеров 262
18.2 Общие замечания 272
18.2.1 Простейшая модель суперкомпиляции 275
18.2.2 Ограничения на стиль программирования 279
19 Разметка входной программы 281
19.1 Псевдокомментарии 281
19.2 Псевдофункции 286
20 О свойствах модели вычислений 288 Общее заключение 291
21 Результаты 298
Список литературы
- Обзор результатов в области специализации программ
- Параметризованные множества данных
- Язык РЕФАЛ-5 и язык РЕФАЛ-графов
- Обобщение и построение «отрицательной» информации
Введение к работе
В семидесятых годах В. Ф. Турчин предложил ряд идей по автоматическому преобразованию программ, которые назвал суперкомпиляцией1. Он поставил задачу создать инструменты для наблюдения за операционной семантикой программы, когда фиксирована функция F, вычисляемая этой программой.
Результатом таких наблюдений должно стать построение нового алгоритмического определения некоторого продолжения функции F. Новый алгоритм строится с целью более быстрого вычисления F на конкретных аргументах.
Позже, рядом авторов эти идеи В. Ф. Турчина изучались и в той или иной мере доводились до алгоритмов.
В диссертации разработан и реализован экспериментальный суперкомпилятор, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Обсуждению разработанных методов и алгоритмов, их исследованию и посвящена данная работа; автор также рассматривает структуру и принципы работы построенного преобразователя программ. Показывается большое количество результатов преобразований реализованным суперкомпилятором и комментируются эти примеры. Основные принципы
'По нашему мнению, название выбрано весьма неудачно. Суперкомпиляция не является компиляцией, подобно многозначной функции, которая не является функцией (или векторному полю, которое не является полем). Английский вариант «supeicompilation» немного более премлсм, и было бы правильно «переводить» его словом «надкомпиляция».
построения суперкомпилятора SCP4 обсуждались с Валентином Фёдоровичем Турчиным. Более того, он инициировал и поддерживал эту работу.
Само понятие «более быстрого вычисления», безусловно, требует уточнения. В диссертации имеется в виду некоторое логическое время, хотя на практике часто оно отражает физическое время. Вопрос о соотношении этих времён рассматривается в одном из разделов данной диссертационной работы.
Языком реализации оптимизатора SCP4 также является РЕФАЛ-5. Язык программирования РЕФАЛ (В. Ф. Турчин [69], [74]) -функциональный язык первого порядка с аппликативной (вызовы по значению) семантикой. Грубо говоря, программа на РЕФАЛе представляет собой систему переписывания термов. Предложения упорядочены, и выбор предложения происходит посредством сопоставления с образцом. Для построения термов используются два конструктора. Первый конструктор - конкатенация2 - бинарный, ассоциативный и используется в инфиксной записи, что позволяет опускать его скобки. Знак пробела служит для обозначения этого конструктора, Второй конструктор одноместный. Синтаксически он обозначается только его скобками, то есть без имени. Функциональный вызов оформляется угловыми скобками; причём, имя вызываемой функции записывается непосредственно после открывающей скобки. В РЕФАЛе все функции являются одноместными, термы принято называть выражениями. Пустая последовательность принадлежит к множеству базисных константных термов и называется
Приписывание.
«пустым выражением». По определению, это единица конкатенации (левая и правая). Все остальные базисные константные термы называются «символами». Базисные неконстантные термы (переменные): е.name, s.name и t.name. Значением е-переменной может быть любое константное выражение, значением s-псременной - любой символ, значением t-переменной - любой символ или выражение в круглых скобках (указанный выше одноместный конструктор). Ассоциативность конкатенации делает множество РЕФАЛ-термов более выразительным, по сравнению с множеством LISP-термов. Объект исследования.
Определение 1 Реализацией функционального языка программирования 9 назовем четвёрку (P,D,U,J), где множество Р называется множеством ^.-программ, множество D называется множеством ^.-данных; частично рекурсивные функции U: PxD і—» D и Т : Р х D \—> N называются соответственно универсальной функцией (или семантикой) и сигнализирующей функцией времени языка К. Здесь N - множество натуральных чисел.
Ниже мы будем использовать обозначение р(х) как сокращение для U(p,x).
Пусть дана реализация функционального языка программирования Ш = (Р, D ,11,1), где D = \JnNMn для некоторого множества М. Пусть программа р(х, у) из Р, реализует функцию3 F(x, у) : X xY *-+ Z, где X С D. Y с D, Z С D. Зафиксируем значение первого аргумента этой функции xq є X. В задаче специализации требуется построить другую программу
3То есть именно функцию, а не частичную функцию.
10 q(y) ЄР такую, что
Vy K(q(y) = p(x0)y)) Л (T(q,y) < T(p,x0,y)).
Программу q называют остаточной программой. Содержательная задача состоит в построении оптимальной q (по времени исполнения). Таким образом, программа q представляет некоторое продолжение функции F(xQ,y) по второй компоненте.
Выше приведена частная формулировка общей задачи специализации программ. В общей постановке требуется проспециализировать программу по данному контексту применения самой программы или, более широко, её подпрограмм. Другим простым примером контекста является композиция применения двух подпрограмм h и g, реализующих соответственно функции Н : X н-> К\G : Image (Я) х У i—> Z; здесь X. У, Z - подмножества множества D. Пусть программа р(х,у) есть композиция h и g: р(х,у) = g(h(x),у). В этом случае требуется построить остаточную программу q(x,y) такую, что
\/х Є ХУу Є Y.(q(x,y) = р(х,у)) Л (T(q,x,y) < Т(р,х,у)).
То есть снова требуется построить оптимальную программу, определяющую продолжение функции F(x,y), представленную композицией g(h(x) ,у).
Разные уточнения понятия оптимальности определяют конкретные аппроксимации задачи специализации как таковой.
В данной работе под программами понимаются программы на функциональных языках программирования.
Актуальность темы. Технология программирования естественно развивается в сторону оперирования понятиями задачи, которая стоит перед программистом, а не понятиями универсального прибора, на котором программа будет исполняться. Это стимулирует развитие языков программирования высокого уровня позволяющих адекватно отражать объектную область задачи. К таким языкам, например, относятся функциональные и логические языки (LISP, REFAL, PROLOG, HASKELL, ML, SCHEME и др.), а также различные языки, специализированные на конкретную область их применения. С другой стороны, аппаратная реализация современных широко используемых ЭВМ поддерживает фон-неймановскую модель вычислений; что приводит к неэффективной реализации таких языков - посредством интерпретации - более того, часто не прямой, а косвенной - через другую интерпретацию. К подобной неэффективности приводит и любое структурное программирование само по себе; ибо его целью является создание гибких, легко понимаемых и изменяемых программ. Всё чаще программы вычисляются другими программами, а потому естественно ожидать, что первые будут содержать простейшие структуры, ведущие к накладным расходам, которые никогда бы не допустил квалифицированный программист.
Методы автоматической оптимизации структурированных программ высокого уровня (а не программ отшлифованных профессиональными программистами на языках программирования низкого уровня) и призваны предоставить свободу развития новым технологиям программирования.
Одним из активно развивающихся здесь направлений является
автоматическая специализация программ. Предположим, что вы купили дистрибутив операционной системы LINUX. В момент её установки на вашем компьютере вы должны указать его аппаратные характеристики, то есть эти характеристики являются аргументами программы-установщика. Возникает желание максимально настроить LINUX на ваше железо, ибо в другом контексте он вам не понадобится. В этом и состоит задача специализации. Операционную систему вы устанавливаете однажды и, потому, стоит предложить поработать автоматическому специализатору, даже если его работа достаточно продолжительна во времени.
Суперкомпияция есть набор методов автоматической специализации программ, написанных на функциональных языках.
Идеи лежащие в основе суперкомпиляции, с одной стороны, существенно мощней идей широко распространённой техники специализации, известной как частичные вычисления; с другой стороны, методы суперкомпиляции намного менее разработаны, чем методы частичных вычислений. И, до недавнего времени, не существовало ни одного экспериментального специализатора-суперкомпилятора, с которым могли бы экспериментировать не только его разработчики, но и иные пользователи. По существу, оставался открытым вопрос о принципиальной возможности построения полностью автоматического суперкомпилятора. Данная диссертационная работа даёт положительный ответ на этот вопрос.
Цели работы. Диссертационное исследование было направлено на решение следующих основных задач:
1. Построить и реализовать новые алгоритмы специализации
функциональных программ, основанные на методах суперкомпиляции. Упростить и довести до алгоритмов полуавтоматические процедуры, представленные в работах В. Ф. Турчина [65], [67], [68], [70], и/или улучшить качественные характеристики этих процедур с точки зрения построения более эффективных остаточных программ.
Разработать и довести до алгоритмов методы построения выходных форматов функций-подпрограмм.
Построить экспериментальный автоматический суперкомпилятор, с которым могли бы экспериментировать посторонние пользователи. Изучить характеристики этого суперкомпилятора.
Общая методика работы. Большая часть идей, используемых в диссертации, хорошо известна в рамках суперкомпиляции. Основным инструментом анализа и преобразований программ является метаинтерпретация этих программ. Преобразования производятся по ходу дела метаинтерпретации (в режиме on-line) и остаточная программа строится исключительно на основе этой интерпретации, а не посредством пошаговой чистки исходной (преобразуемой) программы. Используемый параметрический язык описания конфигураций метадерева возможных вычислений является языком первого порядка.
Предметной областью нашего суперкомпилятора SCP4 является функциональный язык программирования РЕФАЛ-5. Этот же язык является языком реализации суперкомпилятора. Большинство алгоритмов работают в терминах внутреннего языка РЕФАЛ-графов, который
ориентирован на адекватное описание временной эффективности. Это язык более низкого уровня по отношению к РЕФАЛу, но работает с теми же данными. Тем не менее, некоторые свойства преобразуемых алгоритмов формулируются в понятиях самого РЕФАЛа и соответствующие алгоритмы используют эти понятия.
Идеи методов построения выходных форматов компонент факторизации метадерева потенциальных вычислений, глобального анализа и распознавания мономов конкатенации (как и само понятие этих мономов) полностью оригинальны. После глобального анализа компоненты факторизации, производится повторная специализация этой компоненты по свойствам, выявленным глобальным анализом.
После основной стадии преобразований, отдельным проходом производится чистка входных и выходных формальных параметров, излишних вызовов функций.
Транслятор из языка РЕФАЛ-графов в язык С реализован А. П. Конышевым [7]. Часть РЕФАЛ программ, которые используются в дессертации в качестве тестовых примеров для суперкомпилятора SCP4, принадлежат А. В. Корлюкову [8], [10], [11].
Основные результаты.
Разработаны и реализованы аппроксимирующие алгоритмы распознавания частично рекурсивных константных функций, частично рекурсивных функций проекции.
Па основе полуавтоматических процедур обобщения параметризованных конфигураций, представленных в работах
В. Ф. Турчина [65], [67], [68], [70], разработаны и реализованы алгоритмы обобщения параметризованных конфигураций. Улучшены качественные характеристики этих алгоритмов с точки зрения построения более эффективных остаточных программ.
Разработан и реализован алгоритм построения выходных форматов компоненты факторизации F метадерева возможных вычислений в режиме online (по ходу дела суперкомпиляции); что позволяет сразу использовать построенный формат для специализации по нему как других компонент-функций, вызывающих функцию F, так и самой функции F.
Предложено понятие частично рекурсивного монома конкатенации. Доказана теорема о достаточном условии частично рекурсивного монома конкатенации; на основании этой теоремы разработан и реализован алгоритм распознавания частично рекурсивных синтаксических мономов конкатенации. Показано, что на некоторых примерах этот алгоритм способен понижать временную сложность программы с экспоненциальной до константной 0(1).
Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация суперкомпилятора доступна на Web-странице в режиме on-line [90].
Исследованы характеристики суперкомпилятора 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 проведен анализ современного состояния проблемы автоматической специализации программ, сделан обзор научных работ, проводимых в этой области. Рассмотрены разные подходы к постановке задачи специализации как таковой; проведён обзор основных достижений полученных к данному моменту в области специализации функциональных программ; анализируются принципиальные отличия суперкомпиляции от других существующих методов; делается исторический обзор попыток построения суперкомпиляторов. Поясняется положение методов, разработанных в
диссертации, в контексте текущих исследований. (21 страница)
В главе 2 дан набросок структуры суперкомпилятора SCP4, приведена его блок-схема. Дано неформальное введение в функциональный язык программирования РЕФАЛ-5, в терминах которого в диссертационной работе исследуются методы суперкомпиляции. (10 страниц)
В главе 3 определён язык параметров, описывающий состояния РЕФАЛ машины; в частности, - ее входную точку. (5 страниц)
В главе 4 определён язык РЕФАЛ-графов. Под языком РЕФАЛ-графов понимается язык, позволяющий показать структуру промежуточного состояния программы в процессе ее преобразований. (12 страниц)
В главе 5 описывается один из основных инструментов преобразований, который называется прогонкой. Прогонка есть метаобобщение одного шага РЕФАЛ машины. РЕФАЛ машина работает с полем зрения (рабочей памятью), описывающей конкретное состояние машины. Прогонка работает с параметризованным полем зрения. (19 страниц)
В главе 6 описываются алгоритмы свёртки метадерсва возможных вычислений. Подробно рассматриваются принципы стратегий, на которых основаны эти алгоритмы. Свёртка факторизует метадерево возможных вычислений и вызывается непосредственно после прогонки. Свёртка естественно разделяется на два логически замкнутых инструмента: вложение и обобщение. Оба эти инструмента используют не только синтаксические, но и семантические свойства стека функций. Алгоритмы
свёртки являются критическими алгоритмами, суперкомпиляции с точки зрения успешной оптимизации по времени преобразуемой программы: именно они (вместе с алгоритмами глобального анализа) аппроксимируют решение задачи специализации как таковой. (37 страниц)
В главе 7 даны принципы развёртки специализируемой программы. Развёртка перестраивает структуру параметризованных стеков функций в листьях грозди прогонки, согласно некоторой стратегии; выбирает в поле зрения суперкомпилятора лист, стек которого будет предметом преобразования следующего вызова прогонки. В этой главе описываются реализованные в суперкомпиляторе SCP4 стратегии, управляющие развёрткой, (б страниц)
В главе 8 вводится понятие компоненты факторизации метадерева возможных вычислений. Дана классификация компонент факторизации с точки зрения их глобального анализа. (2 страницы)
В главе 9 описываются основные свойства алгоритма чистки семантически недостижимых ветвей компонент факторизации метадерева возможных вычислений. (2 страницы)
В главе 10 описываются алгоритмы глобального анализа компоненты факторизации F, ключевыми из которых являются алгоритм автоматического построения выходного формата функции F по ходу дела суперкомпиляции и алгоритм распознавания мономов конкатенации. Вводится понятие частично рекурсивного монома конкатенации. Доказана теорема о достаточном условии частичного монома конкатенации. Показано, что па некоторых примерах эти алгоритмы способны понижать временную сложность программы с экспоненциальной до константной
0(1). (32 страницы)
В главе 11 описываются принципы использования результатов глобального анализа компоненты факторизации. (17 страниц)
В главе 12 описывается алгоритм уменьшения местности (арности) функций. (5 страниц)
В главе 13 описывается стратегия глобальности использования заголовков (входных форматов) подфункций. Глобальность заголовков компонент факторизации может сократить число этих компонент в остаточной программе. (5 страниц)
В главе 14 анализируются семантические понятия временной эффективности представленные в остаточной программе на языке РЕФАЛ-графов (внутреннем языке преобразований SCP4), которые не могут быть адекватно описаны терминами РЕФАЛа-5 - в его конкретной модели вычислений. (4 страницы)
В главе 15 анализируются принципы анализа остаточной программы, позволяющие отобразить ее на языке Си достаточно эффективно. (7 страниц)
В главе 16 описывается формальный язык постановки задач на суперкомпиляцию и связи его с языком параметров описаний конфигураций в момент преобразований. Последний был описан выше и в данной главе уточняется: вводится подтипизация параметров. (19 страниц)
В главе 17 описано большое число преобразований простых программ, демонстрирующих возможности суперкомпилятора SCP4. Даны примеры классического использования специализатора в качестве компилятора из некоторого языка L в объектный язык специализатора, в нашем случае
РЕФАЛ. В качестве языка L используются язык Машины Тьюринга и язык Регистровой Машины. Указывается на удачное приложение методов суперкомпиляции для верификации параметризованных коммуникационных протоколов. (35 страниц)
В главе 18 формулируется модель вычислений РЕФАЛ программ. В рамках этой модели даётся оценка ускорения, получаемого в результате суперкомпиляции рассмотренного ранее интерпретатора машины Тьюринга. Рассматривается вопрос о соотношении логического и физического времени исполнения программы. (19 страниц)
В главе 19 рассмотрен язык разметки программы, посредством которого программист может объявить суперкомпилятору SCP4 стратегии преобразований этой программы или подсказать ему правильный выбор конкретных локальных действий. (7 страниц)
В главе 20 описаны некоторые свойства рассматриваемой нами реализации РЕФАЛа-5, которые являются принципиальными с точки зрения простоты построения суперкомпилятора. (2 страницы)
В главе «Общее заключение» автор диссертации формулирует нерешённые задачи, решение которых, могло бы внести существенный вклад в дальнейшее понимание природы задачи автоматической специализации программ как таковой. (8 страниц)
В главе 21 перечислены основные результаты диссертационной работы, сведения об апробации и приложении этих результатов. (4 страницы)
В приложении даётся и анализируется результат специализации интерпретатора Машины Тьюринга по программе умножения натуральных
чисел посредством суперкомпилятора SCP4. (7 страниц).
Обзор результатов в области специализации программ
В этой части кратко рассматриваются три основных современных подхода к специализации программ: частичные вычисления, суперкомиляция, generalized partial computation. Анализируются и сравниваются их основные свойства, указываются принципиальные ограничения. Вводятся понятия offline и online специализаций; показываются их достоинства и недостатки. Анализируются эксперименты Джонса-Романеико offline самоприменения частичных вычислителей.
На пути реализации основополагающих идей, сформулированных А. П. Ершовым, В. Ф. Турчиным и Ё. Футамурой, встретились серьёзные трудности. Позже Н. Д. Джонс (Дания) предложил ослабить первоначально поставленные цели за счёт упрощения методов специализации («partial evaluation») [42], [43]. Эта упрощённая техника «частичных вычислений» наиболее разработана к данному моменту. Она решает первую задачу специализации. Пытаясь решить задачи самоприменения специализатора (они рассматриваются подробно в Главе данной диссертации), также сформулированные в 70-х годах независимо вышеуказанными тремя исследователями, Н. Д. Джонс с сотрудниками сделали ещё один принципиальный шаг в сторону упрощения, но теперь уже не постановки задачи, а ограничения подходов к её решению. В университете Копенгагена (Н. Д. Джонс, П. Сестофт, X. Сондергаад) в 1983 году удалось решить аппроксимирующие задачи самоприменения Копенгагенского частичного вычислителя mix. Здесь следует отметить, что всегда существует сигнализирующая функция времени Т (см. постановки задач), делающая любую задачу специализации программы р(хд,у) тривиальной и бессодержательной. А именно, функция Т, которая позволяет построить следующую остаточную программу: q(y) { - р(х0)у); } то есть, просто повторив код исходной программы, зафиксировав в её входной точке данное значение аргумента. Первые результаты самоприменения mix, содержательно, незначительно отличались от приведённой тривиальной остаточной программы. Как пишет Н. Д. Джонс в статье 1993 года [43j, длина остаточной программы, полученной в результате решения простейшей задачи самоприменения тіхСтіхСрсьх.у))1 mix по данной трёхстрочной программе ро(х,у), была пятьсот страниц текста. Здесь значения у неизвестны обеим копиям mix; значение аргумента х известно специализируемому mix, но неизвестно специализирующему mix. Анализируя остаточную программу, копенгагенская группа предложила понятия «online» и «offline» методов специализации [42]. Чуть ниже мы рассмотрим эти понятия. Выбор более простых «offline» методов позволил в 1984 году решить более приемлемые аппроксимирующие задачи самоприменения частичного вычислителя mix [42], [60]. Введя инструменты повышения местности («арности») специализируемых программ и их подпрограмм в рамках «offline» подхода, С. А. Романенко [15], [58], [59] удалось в 1987 году существенно улучшить временные и структурные характеристики остаточных программ задач самоприменения Московского частичного вычислителя unmix. Название его статьи, описывающей unmix, говорит само за себя «Генератор компиляторов, порожденный самоприменением специализатора, может иметь ясную и естественную структуру» [15].
Offline специализация разделяет в отдельные стадии-проходы анализ исходной программы р и метаинтерпретацию локальных шагов этой программы, выполнение которых может быть выполнено без знания конкретных значений неизвестной части аргументов этих шагов. На вход первой стадии, которая называется связыванием по времени (ВТА2), подаётся р и указание, какие из её аргументов будут известны на второй стадии преобразований (метаиитерпретации), а не сами значения этих аргументов, и какие неизвестны. Первые называются статическими, вторые - динамическими. На выходе у ВТА размеченная программа рапп, в которой каждое элементарное действие помечено как статическое, если его можно однозначно проинтерпретировать без знания конкретных значений динамической части входов этих действий-шагов. Аргументы каждого шага также размечаются на статические и динамические; анализ «движения» статической информации по программе р производится ВТА. Задача, поставленная перед ВТА как таковая, очевидно, алгоритмически неразрешима. Повсюду здесь, по умолчанию, имеется в виду некоторая аппроксимация сформулированной ВТА-задачи. На вход второй стадии, которая собственно и называется, при этом подходе, словом «специализация» подаётся результат ВТА - рапп и значения её статических аргументов. «Специализация» (вторая стадия) логически проста и алгоритмизируема; все содержательные проблемы перенесены в ВТА. Группа Н. Д. Джонса, как и С. А. Романенко, решили не оригинальную классическую задачу самоприменения, а задачу mix(mixann(pQnn,x)y))3, которая существенно проще классической: обе копии mix производят лишь вторую стадию преобразований, не занимаясь связыванием по времени. Позже эксперименты, offline самоприменения Джонса-Ромапепко повторялись и уточнялись в разных направлениях рядом авторов. Здесь существенно, что входные данные (как статические, так и динамические, представленные параметрами) каждого шага программы просматриваются только один раз (одним проходом) на этапе «специализации» (второй стадии).
Параметризованные множества данных
В этой части определяется язык описания множеств РЕФАЛ-данных: его удобно представить парой pd+ и pd_. Первая часть представляет «положительную» информацию о данных (не использующую логическую связку отрицания), вторая «отрицательную» (синтаксис, использующий отрицание - «не равно»).
Сначала определим язык описания множеств РЕФАЛ-данных: его удобно представить парой pd+ и pd_. Первая часть представляет «положительную» информацию о данных, вторая - «отрицательную». Определение 2 pd : : = [pd+, pd_], здесь (жирные скобки являются метасимволами. pd+ :: = pterm pd+ I О pterm :: = param I (pd+) I data param :: = s-parameter I e-parameter I t-parameter s-parameter :: = s.name t-parameter :: = t.name e-parameter :: = e.name data ::= SYMBOL data I (data) data I Q
Параметры типа s - s.name представляют множество всех РЕФАЛ-симолов, параметры типа е - е. пате представляют множество всех константных выражений (данных РЕФАЛа), параметры типа t -- t.name представляют объединение множества всех РЕФАЛ-симолов и множества всех константных выражений в круглых скобках [см. Введение], data - данное РЕФАЛа. Остальные термы из pd+ интерпретируются по их индукционному построению.
Подчеркнём, что синтаксическое совпадение языка pd+ с языком образцов РЕФАЛа достаточно случайно и для другого суперкомпилятора язык pd мог бы быть иным (например, мог бы иметь выразительные возможности описания регулярных множеств). Чтобы исключить путаницу между переменными и параметрами мы будем именовать параметры числами, а переменные идентификаторами (если нет явного указания). Определение 3 pd_ ::= restriction, pd І О I 0 restriction :: = s-parameteri ф s-parameter I s-parameter ф SYMBOL / SYMBOL ф s-parameter I SYMB0L1 ф SYMB0L2 I e-parameter ф D
Поясним семантику: s. namei ф s. name2 - ограничение множеств значений параметров: два множества не пересекаются; s.name ф SYMBOL и SYMBOL Ф s. name - ограничение множества значений параметра s. name (SYMBOL не принадлежит этому множеству); SYMBOLi ф SYMB0L2 - пустое множество, если символы SYMBOLi SYMBOL2 совпадают; или тавтология, если эти символы графически различны; е.name ф U - ограничение множества значений параметра е.name (это множество не содержит пустого РЕФАЛ-выражения); Q - пустое выражение представляет тавтологию. Графически совпадающие параметры в одной паре pd представляют одно и то же множество. Запятая здесь, и в паре определяющей pd, интерпретируется как знак пересечения множеств. 0 - обозначает пустое множество.
Множество термов pd предупорядочено отношением включения описываемых его элементами множеств данных. Терм-пара вида [е. name, ] описывает всё множество данных, и потому сравним с любым другим термом-парой и не меньше его. Существуют бесконечные неубывающие цепи различных пар-термов pd, несводящихся друг к другу переименованием параметров.
В этой части язык параметризованных мноэ/сеств РЕФАЛ-данных расширяется до языка первого порядка описания параметризованных стеков функций.
Язык параметров, используемый SCP4, является языком первого порядка: нет параметров, в область определения которых входили бы имена функций или конструктор вызова функции. Все имена функций представлены непосредственно сами собой, конструкторы функциональных вызовов < . . . > - константной кодировкой в данных (Call ...). Внутри скобок - информация о вызове: в частности, описание области определения аргументов и области значения этого вызова на языке описания данных pd+. Графически совпадающие параметры в аргументах разных вызовов в стеке представляют одно и то же множество. Связи между элементами стека описываются через формальные выходные переменные out.name, которые являются лишь фиксированными мета-именами значений соответствующих функциональных вызовов. «Отрицательная» часть описания параметров является общей для всех вызовов в стеке.
Язык РЕФАЛ-5 и язык РЕФАЛ-графов
Повсюду в данной работе будем предполагать, что дерево развивается слева направо. То есть везде под деревом мы имеем ввиду ориентированное слева направо корневое помеченное дерево с раскрашенными и упорядоченными сверху вниз рёбрами.
Транслятор из РЕФАЛа-5 в язык графов строит дерево разбора последовательности образцов конкретной «функции» - подпрограммы. Ветвления в этом дереве безоткатные [см. 4.2]. Дерево обеспечивает одновременное сопоставление с общими частями образцов нескольких подряд идущих предложений. Структура дерева зависит от конкретного базиса элементарных образцов. Каждая ветвь содержит «отрицательную» информацию о значениях переменных (которые определены последовательностью элементарных образцов) выразимую в языке рестрикций restrictions [см. определение синтаксиса 4.1] и зависящую от предикатов на вышестоящих ветвях. Цифры в квадратных мета-скобках являются номерами ветвей в конкретном ветвлении. Приведём результат этой трансляции в более привычных терминах: F { case e.inp of s.v e.u — case s.v of A — e.out := e.u; not A — e.out := s.v e.u; D — e.out := D ; } Здесь стрелка показывает ребро дерева. Заключение
В главе определён язык РЕФАЛ-графов, позволяющий показать структуру промежуточного состояния программы в процессе ее преобразований. Входная часть этого языка допускает U-пошаговую реализацию. Дан сравнительный анализ внешнего объектного языка суперкомпилятора SCP4 и его внутреннего объектного языка. Показана принципиальность конкретной модели вычислений объектного языка. Проведён краткий сравнительный анализ модели вычислений конкретного интерпретатора языка РЕФАЛ-5 с моделями вычислений, на которых основаны реализации других диалектов РЕФАЛа. Показано, что понятия модели вычислений реализации РЕФАЛа-5 более локальны по сравнению с другими реализациями. Свойство локальности понятий упрощает логику суперкомпилятора.
Данная глава посвящена одному из основных инструментов преобразований, который называется прогонкой. Прогонка есть метаобобщение одного шага РЕФАЛ-машины. РЕФАЛ-машина работает с полем зрения (рабочей памятью), описывающей конкретное состояние машины. Прогонка работает с параметризованным полем зрения. Глава начинается с проведением аналогии между школьным алгоритмом решения уравнений с параметрами и алгоритмом прогонки.
Рассмотрим школьный алгоритм вычисления корней квадратного уравнения, данный в неформальном языке. Будем считать числовые коэффициенты мономов данными, а оставшуюся часть синтаксической структуры уравнения - программой. Таким образом, наш алгоритм превратился в «интерпретатор» - решатель программы-уравнения, в котором нет циклов (мы предполагаем, что арифметические операции являются базисными примитивами). Теперь рассмотрим квадратные уравнения с параметрами: некоторые из данных-коэффициентов стали параметрами. Школьник, решающий такие уравнения, владеет понятием алгоритма прогонки. Ответ, естественно, всегда выражается в терминах параметров и представляет собой дерево разбора этих параметров, в котором исполнены алгебраические действия равномерные по значениям параметров. Напомним, что ранее [см. Главу 2] мы назвали результат прогонки гроздью.
Выбрав язык параметров, мы можем уточнить понятие прогонки во входном подмножестве языка РЕФАЛ-графов. В данной главе рассматривается только это подмножество.
В этой части подробно в неформальных терминах описывается алгоритм прогонки, за исключением некоторых конкретных стратегий этого алгоритма. Результатом прогонки данного параметрически описанного поля зрения является дерево разбора параметров (далее -- гроздь,) и преобразований полей зрения, соответствующих сужению параметров на конкретных ветвях этого дерева. Формулируются и доказываются свойства алгоритма прогонки. Работа прогонки демонстрируется рядом примеров. Напомним, что Step: Progx Name args xData" н StackxData" . Шаг абстрактной машины языка РЕФАЛ-гафов состоит из двух логических этапов. На первом этапе выбирается ветвь (путь) от корня графа Name до его «листа» end-of -branch, на втором этапе - происходит модификация стека в соответствии с синтаксисом end-of-branch и вычисленной на первом этапе средой. Рассмотрим интерпретацию подробнее.
На первом этапе происходит ряд сопоставлений значений переменных из текущей среды с элементарными образцами. (Задача сопоставления РЕФАЛ-выражения Ехрг с образцом Pattern является задачей решения уравнения Pattern = Ехрг. Результат решения есть значения переменных из образца Pattern либо информация о том, что уравнение корней не имеет.)
Обобщение и построение «отрицательной» информации
Если на пути от корня мстадсрсва до текущего узла нашёлся опорный узел «похожий» на текущий, тогда параметризованное описание стека в найденном (предыдущем) опорном узле разбито на две части (как результат обнинского условия): первая часть является точкой входа в предполагаемый цикл, вторая часть - контекст вычислений этого цикла. stack_prev = (ai,tmi) . . . (a.j,tmj) context stack_curr = (aijt ) . . . (a;,t .) middle context
Предположение заключается в том, что, начиная с текущего узла, процесс возможных вычислений будет «повторяться». Оба префикса являются точками входа в цикл: предыдущий - в первую итерацию цикла, текущий - во вторую. Чтобы профакторизовать мета-дерево, необходимо свести с помощью подстановки параметров параметрическое описание среды текущего префикса к среде предыдущего. Если такой подстановки не существует, тогда описание этих двух сред «обобщаются», то есть строится параметризованная среда, которую можно свести к обеим средам префиксов с помощью подстановок параметров. Предыдущий префикс заменяется на обобщённый и, таким образом, утверждение о возможности факторизации метадерева посредством алгоритма вложения становится более слабым: все параметризованные описания стеков, которые можно было подстановкой Subst свести к предыдущему стеку, можно свести и к обобщённому посредством композиции подстановки построенной обобщением и подстановки Subst.
По определению, верхняя4 функциональная и временная структура предыдущего и текущего контекстов совпадают. Следовательно, среды контекстов будут совпадать при любом конкретном потенциальном вычислении. Но их параметризованные описания (описания значений переменных из сред) могут отличаться: описание параметризованной среды текущего контекста является некоторым уточнением параметризованной среды предыдущего контекста. Это уточнение определяется путём от предыдущего узла до текущего. Каждое уточнение может произойти лишь посредством подстановки значений параметров и формальных выходных переменных в рсі+-часть описания среды и соответствующего изменения pcL-части, так как во всех других случаях изменения параметризованного контекста его временная структура, по определению, изменяется. Если в процессе уточнений (сужений) параметрически описанной среды контекста не было пи одной подстановки значений формальных выходных переменных out.name, тогда описание среды текущего контекста сводится к описанию среды предыдущего контекста композицией этих подстановок параметров. Иначе необходимо «обобщить» описания сред контекстов аналогично обобщению префиксов.
Ветви метадерева с корнем в предыдущем опорном узле отбрасываются. Задача разбивается на две: обобщённые префикс и контекст. Узлы описывающие эти задачи и задачи, определяющиеся (возможно) функциональной сводящей подстановкой, а также связи между этими задачами, помещаются на место предыдущего узла. Результат вычисления построенных задач объявляется произвольным, то есть выходная среда в этот момент преобразований неопределена - описывается новыми е-параметрами. Как и в случае вложения, эти задачи являются входными точками отдельных преобразований. Зафиксируем сказанное в виде утверждений.
Теорема 1 Частичная функция, определяемая обобщённым параметризованным стеком, является расширением частичной функции, которая определена стеком заменяемого предыдущего опорного узла.
Теорема 2 Результат подстановки параметров, построенной обобщением предыдущего стека, в параметризованные вызовы функций в обобщённом стеке определяет частичную функцию заменяемого предыдущего опорного узла (функцию, которую определял этот предыдущий узел).
