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

На правах рукописи

Немытых Андрей Петрович

СПЕЦИАЛИЗАЦИЯ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ МЕТОДАМИ СУПЕРКОМПИЛЯЦИИ

05 13 17 — Теоретические основы информатики

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

^"/^^ы-е (-1.'

□□3173135

Переславль-Залесский — 2007

003173135

Работа выполнена в Институте программных систем РАН

Научный руководитель

Официальные оппоненты

Ведущая организация

доктор физико-математических наук, член-корреспондент РАН Абрамов Сергей Михайлович

доктор технических наук, профессор

Хорошевский Владимир Федорович, ВЦ РАН

кандидат физико-математических наук,

Романенко Сергей Анатольевич, ИПМ им М В Келдыша РАН

Институт проблем передачи информации им А А Харкевича РАН

Защита состоится $ " 2007 в ч мин на заседании

Диссертационного совета Д 002 084 01 в Институте программных систем РАН по адресу 152020, г Переславль-Залесский, Ярославской области, Институт программных систем РАН

С диссертацией можно ознакомиться в библиотеке Института программных систем РАН

Автореферат разослан " 8 " о/стл^,^ 2007

Ученый секретарь Диссертационного совета кандидат технических наук

Пономарева С М

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Транслятор из языка РЕФАЛ-графов в язык С реализован А П Конышевым [1] Часть РЕФАЛ программ, которые используются в

дессертации в качестве тестовых примеров для суперкомпилятора SCP4, принадлежат А В Корлюкову [2], [4], [5]

Научная новизна. Все основные результаты являются новыми Предложено несколько новых алгоритмов специализации Для некоторых из ранее известных полуавтоматических/неформальных методов специализации разработаны алгоритмы, позволившие добиться их полной автоматизации На основе разработанных алгоритмов реализован экспериментальный специализатор SCP4, который является первым полностью автоматическим специализатором программ, основанным на методах суперкомпиляции

Практическая и теоретическая ценность. Представленные в диссертации алгоритмы распознавания синтаксической мономиальности программ и вычисления выходных форматов компонент факторизации дерева потенциальных вычислений могут быть полезны для решения классических задач самоприменения специализаторов, поставленных А П Ершовым [8], Е Футамурой [9] и В Ф Турчиным [14], [16] В разделе 16 3 диссертационной работы подробно рассматриваются возможности алгоритма распознавания синтаксических мономов для понижения порядка временной сложности остаточных программ в задачах самоприменения Данная диссертационная работа дает положительный ответ на долго стоявший открытым вопрос о принципиальной возможности построения полностью автоматического суперкомпилятора, что является значительным шагом в направлении внедрения технологии суперкомпиляции в практику программного обеспечения современных компьютеров В диссертации показано, что суперкомпилятор 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 m 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 работах [24], [25], [26], [27], [28], [29], [30], [31], [32], [33], [34], [35], [36], [37], [38], перечисленных в конце списка литетатуры

Работа [25] опубликована в издании, входившем в перечень ВАК на момент публикации и имеющемся в перечне ВАК на данный момент Работа [26] является монографией автора диссертации

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

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

СОДЕРЖАНИЕ РАБОТЫ

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

Определение 1 Реализацией функционального языка программирования назовем четверку (Р,0,и,1), где множество Р называется множеством 3?-программ, множество Б называется множеством Ш-данных, частично рекурсивные функции и РхИ ► И и Т Р х 5 N называются соответственно универсальной функцией (или семантикой) и сигнализирующей функцией времени языка Ж Здесь N - множество натуральных чисел

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

Пусть дана реализация функционального языка программирования = (Р,Б,и,Т), где Б = для некоторого множества М Пусть

программа р(х,у) из Р, реализует функцию1 F(a;,у) X х 1' н где X С С В Зафиксируем значение первого аргумента этой функции х0 6 X В задаче специализации требуется построить другую программу q(y) Е Р такую, что

^У € = р(*о>у)) Л ^ Т(р,х0,у))

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

Выше приведена частная формулировка общей задачи специализации программ В общей постановке требуется проспециализировать программу по данному контексту применения самой программы или, более широко, ее подпрограмм Разные уточнения понятия оптимальности определяют конкретные аппроксимации задачи специализации как таковой

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

Во второй главе дан набросок структуры суперкомпилятора 8СР4, приведена его блок-схема Дано неформальное введение в функциональный язык программирования РЕФАЛ-5, в терминах которого в диссертационной работе исследуются методы суперкомпиляции

В третьей главе определен язык параметров, описывающий состояния РЕФАЛ машины, в частности, - ее входную точку

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

1 'Го есть именно функцию, а не частичную функцию

В пятой главе описывается один из основных инструментов преобразований, который называется прогонкой Прогонка есть метаобобщение одного шага РЕФАЛ машины РЕФАЛ машина работает с полем зрения (рабочей памятью), описывающей конкретное состояние машины Прогонка работает с параметризованным полем зрения

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

Алгоритмы свертки, в частности, включают в себя

• Механизм выделения функции-цикла в результате анализа последовательности параметризованных стеков, находящихся в опорных узлах метадерева развертки вдоль пути от корня этого дерева к текущему (анализируемому) узлу (Глава 6)

• Алгоритмы вложения (раздел 6 1) и обобщения параметризованных конфигураций (раздел 6 1)

• Обнинский алгоритм расщепления стека функций, принадлежащий В Ф Турчину (раздел 6 3 11)

• Алгоритм расщепления данной задачи на специализацию на подзадачи (раздел 6 1)

Введено отношение «похожести» (раздел 6 3 1), связывающее семантическое проявление цикла в метадереве с синтаксическими структурами в этом дереве Это отношение представлено, как пересечение отношения «похожести» чисто функциональной структуры стеков (последовательности имен функций) и «похожести» параметрического

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

Введено понятие последовательности временного развития стека (раздел 6 3 11)

Определение 2 Пусть дан конечный алфавит А = {а;} Пусть W - множество конечных слов над А, включая пустое слово Пусть даны функция G A i—► W и некоторое слово s £ W Определим последовательность (быть может, конечную) с записью времен рождения stacks

1 stacko = (s,0)

2 пусть определен stacht = fa,, t) u,, где a, G A, t € N, a u, -оставшаяся часть последовательности stacht Тогда

stack,+1 = TzmeiGCot), МахТгте) u,,

где МахТгте есть максимум по вторым компонентам пар из stack, ТгтеСа ш, time) = (а,Ьгте+1) Тгте(ш, tzme+l), Тгте( , t%me) - , ,где а € А, ш € W

Последовательность stacks назовем временным развитием стека (G,s)

Описаны стратегии алгоритмов свертки

• Алгоритм вложения просматривает опорные узлы, лежащие на пути от корня метадерева до текущего узла, в порядке времени создания этих узлов (раздел 6 2)

• Обобщение просматривает опорные узлы вдоль пути от текущего узла до корня мета-дерева, то есть в направлении противоположном ориентации (противоположном просмотру этих узлов алгоритмом вложения) (раздел 6 3 5)

Доказано, что местность сред двух префиксов, выделяемых обнинским алгоритмом Турчина, совпадают (раздел 6 3 11, Утверждение 2)

Доказаны теоремы

• Частично рекурсивная функция, определяемая обобщенным параметризованным стеком, является расширением частично рекурсивной функции, которая определена стеком заменяемого предыдущего опорного узла (раздел 6 3 2, Теорема 1)

• Результат подстановки параметров, построенной обобщением предыдущего стека, в параметризованные вызовы функций в обобщенном стеке определяет частично рекурсивную функцию заменяемого предыдущего опорного узла (раздел 6 3 2, Теорема 2)

Рассмотрены свойства результатов вложения и обобщения, с точки зрения временной эффективности последующего выполнения результата преобразований (раздел 6 4) В частности, показано, что в процессе обобщения информация о параметризованных средах может быть потеряна тремя принципиально разными способами

• разбиением задачи на подзадачи и описанием связей между ними,

• обобщением параметризованных выражений с построением нерекурсивных (без функциональных вызовов) сводящих подстановок, которые остаются в метадереве возможных вычислений,

• обобщением параметризованных выражений с построением рекурсивных сводящих подстановок, которые остаются в метадереве возможных вычислений

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

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

В процессе свертки могут быть построены три типа компонент

1. самодостаточные - все ребра исходящие из вершин таких подграфов

заканчиваются только в вершинах данного подграфа,

2. компоненты содержащие только вершины, исходящие ребра из которых

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

3. компоненты, в которых существуют вершины с исходящими из них

ребрами, которые заканчиваются на базисных узлах являющихся корнями поддерева, факторизация которого еще не завершена (далее в этом случае мы будем говорить, что подграф ссылается на непрофакторизованную часть мета-дерева)

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

В десятой главе описываются алгоритмы глобального анализа компоненты факторизации F, ключевыми из которых являются алгоритм автоматического построения выходного формата функции F по ходу дела суперкомпиляции (раздел 10 1 2) и алгоритм распознавания мономов конкатенации (раздел 10 2) Вводится понятие частично рекурсивного монома конкатенации (раздел 10 2 2)

Определение 3 Пусть дана п-местная частичная функция

F(xi,X2, ,Х„) DATA" i-> DATA±

где DATA - множество данных РЕФАЛа Скажем, что F частичный моном приписывания, если существует такая конечная последовательность натуральных чисел ki,k2, , km , что на области

определения функции верно тождество

F(xux2, ,х„) = хк-

где Vs (0 < s < т) О < js < п Здесь операция умножения -приписывание, возведение в степень относится к этой же операции

Пусть Refal„ есть РЕФAJI-подобный язык, в котором разрешены только n-местные функции-определения (точное определение см в разделе 10 2 2)

Определение 4 Пусть дана Refaln программа Р такая, что местности всех определений из Р совпадают и равны п Пусть Ft{x\,x2, ,хп) входные форматы определений из Р И пусть дана конечная последовательность натуральных чисел ki,k2, , kn , где kj > 0 для всех j Пусть \у\> обозначает у, , у ,где у повторено j раз Формальным повышением местности программы Р по отношению к п-ке к\, /с2, , kn назовем ее следующее преобразование для всех г

• каждую левую часть left-part = pi, ,рп каждого предложения из Р преобразуем к виду [pi]fcl, , \pn]k" ,

• каждый функциональный вызов <Ft argi, ,argn> программы Р преобразуем к виду <Ft [argi]fcl, , [arg„]fc">

Построенную программу обозначим Pkuk*' и назовем k\,k2, ,kn местной по отношению к Р (Определения из

pkiM, ,k„ будем

обозначать аналогично 'k" )

Определение 5 Пусть дана Refal„ программа Р такая, что местности всех определений из Р совпадают и равны п Пусть F,(xi,x2, ,хп) входные форматы определений из Р И пусть дана перестановка а элементов последовательности 1, ,п Формальной перестановкой параметров программы Р посредством а, назовем ее следующее преобразование для всех г

• каждую левую часть left-part = pi, , р„ каждого предложения из Р преобразуем к виду pff(1), ,рст(„),

• каждый функциональный вызов <Ft argy, ,argn> программы Р преобразуем к виду <F, arga^, , arga(n)>

Построенную программу обозначим "Р и назовем а-переставленной по отношению к Р (Определения из аР будем обозначать аналогично aFl )

Определение 6 Назовем Re fair, программу Р синтаксическим мономом, если существует конечная последовательность натуральных чисел , кп (где к} > О для всех j), для которой определена программа pk\M, ,k„ ^ и существует такая перестановка а последовательности 1, , гп (тп = к\ + + кп) , что после формальной замены в программе

(Т j)k\ .

• каждого функционального вызова

<function-name arga(i), , arga(m)>

конкатенацией его аргументов arga^ о.г9а(т),

• каждой левой части

patternст(1), ,patterna{m) каждого предложения конкатенацией его образцов patterna(\) patterna(m),

левая часть left-side каждого предложения sentence программы opkito, ,k„ будет графически совпадать с правой частью этого предложения

Доказана теорема о достаточном условии частичного монома конкатенации (раздел 10 2 2, Теорема 2)

Теорема 1 (достаточное условие мономиалъности)

В обозначениях определения 6 Пусть F}{xi, , хп) есть входной формат определения definition Fj Пусть уг обозначает г-тый член последовательности [xi]fcl, , [xn\kn, тогда для всех j - F3 из синтаксического монома Р определяет частичную функцию F3,

ЯвЛЯЮЩуЮСЯ частичным МОНОМОМ Уа(1) Уа(т)

Fj(xi, , хп) = Уа(\) Уа(т)

Описана стратегия выбора гипотезы мономиальности (раздел 10 2 3)

Пусть программа Р содержит ровно одно определение F и пусть <F х\, , хп> есть его входной формат Рассмотрим все пассивные предложения2 из F plt, ,р„, = right-side, Пусть обозначают некоторые фиксированные данные РЕФАЛа Предположим, что для каждого г существует хотя бы одна точка d\t, , dnt такая, что определение F описывает частичную функцию, при вызове которой <F , dn> на первом же шаге машины, отождествление произойдет в

предложении рх,, = right-side, То есть набор данных , dn%

представляет собой один из базисных случаев рекурсивного определения F Правая часть right-side,, по определению, не будет изменена в предполагаемом процессе анализа на мономиальность Следовательно, если Р частичный синтаксический моном, тогда существует моном Мг от формальных переменных Xi, ,х„ такой, что результат подстановки вместо этих переменных соответственно pi,, , pni есть right-side, Для всех г и j должно выполняться графическое равенство М,{х\, ,х„) = Mj(xu ,х„)

Описанная выше стратегия порождения гипотезы обладает одним существенным недостатком построение гипотезы неоднозначно

2Правые части которых не содержат вызовов функций

Теорема 2 В обозначениях данного раздела (см выше), пусть в программе Р существует хотя бы одно предложение ,рщ =

ггдМ-э'ьб.е^ такое, что ггдЫ-згд.е, не содержит вызовов функций и для всех к образцы р^ отличны от пустых выражений Тогда может существовать лишь конечное число гипотез, которые можно построить в рамках описанной выше стратегии

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

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

В двенадцатой главе описывается алгоритм уменьшения местности (арности) функций

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

В четырнадцатой главе анализируются семантические понятия временной эффективности представленные в остаточной программе на языке РЕФАЛ-графов (внутреннем языке преобразований БСР4), которые не могут быть адекватно описаны терминами РЕФАЛа-5 - в его конкретной модели вычислений

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

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

конфигураций в момент преобразований Последний был описан выше и в данной главе уточняется вводится подтипизация параметров (раздел 16 2), уточняются алгоритмы прогонки (раздел 16 2 1) и свертки (раздел 16 2 2) Рассматривается приложение алгоритма распознавания мономов конкатенации в задаче самоприменения (раздел 16 3)

В семнадцатой главе описано большое число преобразований простых программ, демонстрирующих возможности суперкомпилятора SCP4 Даны примеры классического использования специализатора в качестве компилятора из некоторого языка L в объектный язык специализатора, в нашем случае РЕФАЛ В качестве языка L используются язык Машины Тьюринга и язык Регистровой Машины Указывается на удачное приложение методов суперкомпиляции для верификации параметризованных коммуникационных протоколов

В восемнадцатой главе формулируется модель вычислений РЕФАЛ программ В рамках этой модели дается оценка ускорения, получаемого в результате суперкомпиляции рассмотренного ранее интерпретатора Машины Тьюринга Turing (раздел 17 1, пример 10) Рассматривается вопрос о соотношении логического и физического времени исполнения программы Исследуются характеристики суперкомпилятора SCP4, в частности, доказана следующая теорема (раздел 18 1, Теорема 1)

Теорема 3 Для любой программы Prog на языке Машины Тьюринга (МТ) результат специализации суперкомпилятором SGP4 интерпретатора Тиггпд по Prog не содержит терминологии программы Prog То есть включает в себя только синтаксические единицы Prog, описывающие данные на ленте текущие символы в ячейках и записываемые в ячейки символы Следовательно, происходит <гэффективная,» компиляция программы Prog из языка МТ в РЕФАЛ

В девятнадцатой главе рассмотрен язык разметки программы, посредством которого программист может объявить суперкомпилятору SCP4 стратегии преобразований этой программы или подсказать ему правильный выбор конкретных локальных действий

В двадцатой главе описаны некоторые свойства рассматриваемой нами реализации РЕФАЛа-5, которые являются принципиальными с точки зрения простоты построения суперкомпилятора

В главе Общее заключение автор диссертации формулирует нерешенные задачи, решение которых, могло бы внести существенный вклад в дальнейшее понимание природы задачи автоматической специализации программ как таковой

В двадцать первой главе перечислены основные результаты диссертационной работы, сведения об апробации и приложении этих результатов

В Приложении дается и анализируется результат специализации интерпретатора Машины Тьюринга по программе умножения натуральных чисел посредством суперкомпилятора SCP4

Основные результаты.

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

2 На основе полуавтоматических процедур обобщения параметризованных конфигураций, представленных в работах В Ф Турчина [14], [16], [17], [19], разработаны и реализованы алгоритмы обобщения параметризованных конфигураций Улучшены качественные характеристики этих алгоритмов с точки зрения построения более эффективных остаточных программ.

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

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

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

5 Разработан и реализован экспериментальный автоматический суперкомпилятор БСР4, предметной областью которого является функциональный язык программирования РЕФАЛ-5 Демонстрация суперкомпилятора доступна на \ЭДеЪ-странице в режиме оп-1те [37]

6 Исследованы характеристики суперкомпилятора ЭСР4

СПИСОК ЛИТЕРАТУРЫ

[1] Конышев А П Компилятор из языка Рефал-графов в язык С исходные тексты и демонстрация 2000 [Электрон ресурс]// http //www botik ru/pub/local/scp/refal5/

[2] Корлюков А В , Пособие по суперкомпилятору SCP4, 1999 [Электрон ресурс]// http //www refal net/supercom htm

[3] Корлюков А В Получение формул в математике // Тезисы докладов VIII Белорусской математической конференции, стр 178, 2000 [Электрон ресурс]//

http //www bsu by/Converences/kon£8/Sections/Abstrl4/Korlukov/Kor]ukov htm

[4] Корлюков А В Несколько примеров преобразований программ суперкомпилятором SCP4 2001 [Электрон ресурс]// http //www refal net/~korlukov/pearls/

[5] Корлюков А В Суперкомпилируем суперагентов // Альфа, Т 1, стр 89-98 Гродно Гродненский государственный университет, 2001

[6] Chmutov S V, Ga.yd.ar Е А , Ignatovich I М, Kozadoy V F, Nemytykh А Р , Pinchuk V A Implementation of the symbol analytic transformation language FLAC // LNCS, Vol 429, pp 276 / The Proc of DISCO'90 Springer-Verlag, 1990

[7] Chmutov S V, Nemytykh A P, Gaydar E A , Ignatovich, / M, Kozadoy V F, Pinchuk V A The symbol analytic transformation language FLAC sources, executable modules, 1991 [Электрон ресурс]// ftp //www botik ru/pub/local/scp/flac/flac386 zip

[8] Ershov A P Mixed computation potential applications and problems for study // Theoretical Computer Science, Vol 18, pp 41-67

[9] Futamura Y Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler // Systems Computers Controls , Vol 2(5), pp 4550, 1971 (An updated version of the paper was republished m J HigherOrder and Symbolic Computation, Vol 12, pp 381-391, 1999 )

[10] Gluck R , Turchin V F Application of metasystem transition to function inversion and transformation // The Proc of the ISSAC'90, pp 286-287 ACM Press, 1990

[11] Nemytykh A P, Pinchuk V A Program Transformation with Metasystem Transitions Experiments with a Supercompiler // LNCS, Vol 1181, pp 249-260 / The Proc of the Perspectives of System Informatics, Springer-Verlag, 1996 ftp//ftp botik ru/pub/local/APP/meta-trans ps gz

[12] Nemytykh A P , Pinchuk V A , Turchin, V F A Self-Applicable Supercompiler // LNCS, 1110, pp 322-337 / The Proc of Partial Evaluation, International Seminar Danvy o , Gluck R , Thiemann P (Eds ) Spnnger-Verlag, 1996 (ftp //ftp botik ru/pub/local/APP/self-appl ps gz)

[13] Turchin V F A supercompiler system based on the language REFAL // SIGPLAN Notices, Vol 14(2), pp 46-54 1979

[14] Turchin V F The Language Refal, the Theory of Compilation and Metasystem Analysis // Courant Computer Science Report #20, New York University, 1980

[15] Turchin V F, Nireberg R , Turchin D V Experiments with a supercompiler // Conference Record of the ACM Symposium on LISP and Functional Programming, pp 47-55 ACM Press, 1982

[16] Turchin V F The concept of a supercompiler // ACM Transactions on Programming Languages and Systems, Vol 8, pp 292-325 ACM Press, 1986

[17] Turchin V F The algorithm of generalization m the supercompiler // The Proc of the IFIP TC2 Workshop, Partial Evaluation and Mixed Computation, 531-549 North-Holland Publishing Co , 1988

[18] Turchin V F Refal-5, Programming Guide and Reference Manual Holyoke, Massachusetts New England Publishing Co , 1989 (electronic version http //www botik ru/pub/local/scp/refal5/, 2000)

[19] Turchin V F Metacomputation in the language Refal 1990 (unpublished, private communication)

[20] Turchin V F Program Transformation with Metasystem Transitions // J of Functional Programming, Vol 3(3), pp 283-313 1993

[21] Turchin V F Metacomputation Metasystem transition plus supercompilation // LNCS, Vol 1110, pp 481-509 / The Proc of the PEPM'96 Springer-Verlag, 1996

[22] Turchin V F Supercompilation Techniques and results // LNCS, Vol 1181, pp 227-248 / The Proc of Perspectives of System Informatics Springer-Verlag, 1996

[23] Turchin VF, Turchin DV, Konyshev AP, Nemytykh AP Refal-5 sources, executable modules [Электрон ресурс]// http //www botik ru/pub/local/scp/refal5/, 2000

ПУБЛИКАЦИИ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

[24] Лисица А П, Немытых А П Работа над ошибками / / Программные системы теория и приложения Т 1, стр 195-232, М Физматлит, 2006 (доступна на ftp //www botik ru/pub/local/scp/refal5/psta_errors2006 pdf)

[25] Лисица А П, Немытых А П Верификация как параметризованное тестирование (эксперименты с суперкомпилятором SCP4) / / Программирование Т 33(1), стр 22-43, М , 2007

[26] Немытых А П Суперкомпилятор SCP4 Общая структура М УРСС, 2007 152 с

[27] Korlyukov А V, Nemytykh А Р Supercompilation of Double Interpretation (How One Hour of the Machine's Time Can Be Turned to One Second) / / Вестник национального технического университета „Харьковского политехнического института", Т 1, рр 123-150 Харьков, 2004 (электронная версия

http //www refal net/ ~ korlukov/scp2mt/ Karliukou__ Nemytykh pdf,

исходные тексты и демонстрация

http //www refal net/~korlukov/demo_scp4xslt zip)

[28] Lisitsa A , Nemytykh A P Verification of parameterized systems using supercompilation A case study // The Proc of the Third Workshop on Applied Semantics (APPSEM05) / Hofmann M , Loidl H W (Eds ), pp 1215 Fraunchiemsee, Germany Ludwig Maximillians Universitat Munchen 2005, September Accessible via

ftp //www botik ru/pub/local/scp/refal5/appsem_verification2005 ps

[29] Lisitsa A , Nemytykh A P Towards verification via supercompulation // The Proc of the 29th Annual Internationa] Computer Sofware and Applications Conference COMPSAC 2005 / Workshops and Fast Abstracts Volume, pp 9-10 IEEE 2005

[30] Lisitsa A , Nemytykh A P Reachability Analysis m Verification via Supercompilation // The Proc of the Satellite Workshops of DTL 2007 / TUCS General Publication, No 45, Part 2, pp 53-67 Turku, Finland June 2007

[31] Lisitsa A , Nemytykh АРА Note on Specialization of Interpreters // LNCS, Vol 4649, pp 237-248 / The Proc of The 2-nd International Symposium on Computer Science m Russia Springer, 2007

[32] Nemytykh A P Supercompiler SCP4 Use of quasi-distributive laws in program transformation // Wuhan University Journal of Natural Sciences , Vol 95(1-2), pp 375-382 / The Proc of International Software Engineering Symposium Wuhan, China. 2001, March

[33] Nemytykh АРА Note on Elimination of Simplest Recursions // The Proc of the ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp 138-146 ACM Press Aizu, Japan 2002

[34] Nemytykh A P The Supercompiler SCP4 General Structure (extended abstract) 11 LNCS, Vol 2890, pp 162-170 / The Proc

of the Perspectives of System Informatics Sprmger-Verlag, 2003 (ftp //www botik ru/pub/local/scp/refal5/nemytykh_PSI03 ps gz)

[35] Nemytykh A P Playing on REFAL // The Proc of the International Workshop on Program Understanding, pp 29-39 Novosibirsk - Altai Mountains July 2003 (http //www botik ru/pub/local/scp/refal5/korlyukov html)

[36] Nemytykh A P The Supercompiler SCP4 General Structure // Программные системы теория и приложения Т 1, стр 448-485 М Физматлит, 2004 (ftp //ftp botik ru/pub/loca]/scp/refa]5/GenStruct ps gz)

[37] Nemytykh A P, Turchin, V F The Supercompiler SCP4 sources, on-lme demonstration 2000 [Электрон ресурс]// http //www botik ru/pub/local/scp/refal5/

[38] Turchin V F, Nemytykh A P Metavariables Their implementation and use m Program Transformation // Technical Report CSc TR 95-012 City College of the City University of New York, 1995

Работа [25] опубликована в издании, входившем в перечень ВАК на момент публикации и имеющемся в перечне ВАК на данный момент В этой статье автором разработан метод верификации параметризованных коммуникационных протоколов посредством суперкомпиляции интерпретаторов этих протоколов Используя суперкомпилятор SCP4, автор успешно применил этот метод для верификации серии cache coherence протоколов

В статье [24] автор показал, что разработанный им метод верификации параметризованных протоколов посредством суперкомпиляции может быть применен для поиска тестовых примеров, указывающих на ошибки в спецификациях

В работах [28], [29] автором были заложены основы метода верификации, отмеченного выше

Работа [26] является монографией автора диссертации В работе [27] автор показал, что использование суперкомпиляции для специализации двойной интерпретации может улучшить

мультипликативную константу во временной сложности на три порядка

В статье [30] автор построил формальную модель суперкопиляции, достаточную для успешной верификации некоторого класса параметризованных cache coherence протоколов

В работе [31] автор показал, что верификацию коммуникационных протоколов можно рассматривать как специализацию их интерпретаторов по фиксированной части начальной конфигурации этих протоколов

Здесь [37] представлены исходные тесты суперкомпилятора SCP4, реализованного автором

В работе [38] автором был построен язык параметров, описания параметризованных конфигураций, позволяющий уточнять постановки задач на самоприменение

Все остальные указанные работы были выполнены автором диссертации без соавторов

Том I

Введение

1 Анализ результатов диссертации в контексте исследований в области специализации программ

1.1 О двух постановках задачи специализации.

1.2 Обзор результатов в области специализации программ

1.3 Исторический обзор развития методов суперкомпиляции

2 Схема структуры преобразователя программ SCP

3 Язык параметров

3.1 Параметризованные множества данных.

3.2 Параметризованные множества полей зрения (стеков) и РЕФАЛ-выражений.

4 Язык РЕФАЛ-графов

4.1 Синтаксис.

4.1.1 Синтаксис входного подмножества.

4.2 Семантика.

4.3 Язык РЕФАЛ-5 и язык РЕФАЛ-графов.

4.3.1 О неравномерности шагов РЕФАЛ-машины.

4.3.2 Дерево отождествления в языке РЕФАЛ-графов.

5 Прогонка

5.1 Общая структура прогонки.

5.2 Перестройка стека функций.

5.3 Стратегия выбора входного формата.

5.4 К вопросу о целях преобразований.

6 Свёртка

6.1 Вложение.

6.2 Стратегия обхода дерева при факторизации.

6.3 Обобщение.

6.3.1 Отношение «похожести».

6.3.2 Обобщение конфигураций.

6.3.3 Обобщение параметризованных выражений.

6.3.4 Обобщение и построение «отрицательной» информации. ИЗ

6.3.5 Стратегия обхода метадерева при обобщении.

6.3.6 Обнинское условие и транзитные вершины.

6.4 К вопросу о целях преобразований.

6.4.1 Изменение местности параметризованной среды при её обобщении.

7 Развёртка

7.1 Стратегия развития дерева.

7.2 Стратегии развития стека функций.

7.3 К вопросу о целях преобразований.

8 Подграф - компонента факторизации

9 Чистка экранируемых ветвей

10 Глобальный анализ

10.1 Анализ в терминах языка РЕФАЛ-графов.

10.1.1 Пустые подграфы.

10.1.2 Выходные форматы.

10.1.3 Графы определяющие константу.

10.1.4 Проекции.

10.2 Анализ в терминах языка РЕФАЛ.

10.2.1 Тождественность.

10.2.2 Мономы конкатенации.

10.2.3 Стратегия выбора гипотезы мономиальности.

10.2.4 Частичные выражения.

10.3 Чистка поглощаемых ветвей.

Том II

11 Использование результатов глобального анализа

11.1 Одношаговые подграфы.

11.2 Пустые подграфы.

11.3 Рекурсивные подграфы. Повторная специализация.

11.4 Квази-дистрибутивность подзадачи.

11.4.1 Правая квази-дистрибутивность.

11.4.2 Левая квази-дистрибутивность.

11.5 К вопросу о целях преобразований.

12 Чистка входных, выходных формальных параметров и вызовов функций

13 Чистка повторных определений

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

13.2 Повторные определения.

14 Неадекватная выразимость результата преобразований средствами РЕФАЛа

15 Разметка свойств переменных и компиляция в Си (или в язык сборки)

15.1 Уменьшение числа копирований.

15.2 Хвостовая рекурсия.

16 Поднятие параметра (уточнение языка параметров). О синтаксисе входных точек

16.1 Постановка задач на специализацию.

16.2 Подтипы параметров.

16.2.1 Уточнение прогонки.

16.2.2 Уточнение свёртки.

16.3 Синтаксические мономы в задаче самопримеиения.

16.4 Язык MST-схем.

17 Несколько примеров преобразований 227 17.1 Простейшие примеры.

17.2 Специализация самоописания РЕФАЛа.

17.3 Другие эксперименты.

18 О соотношении сложности

18.1 Анализ двух примеров.

18.2 Общие замечания.

18.2.1 Простейшая модель суперкомпиляции.

18.2.2 Ограничения на стиль программирования.

19 Разметка входной программы

19.1 Псевдокомментарии.

19.2 Псевдофункции.

20 О свойствах модели вычислений 288 Общее заключение

21 Результаты

В семидесятых годах В. Ф. Турчин предложил ряд идей по автоматическому преобразованию программ, которые назвал суперкомпиляцией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) <T(p,x0,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.