Специализация функциональных программ методами суперкомпиляции тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Немытых, Андрей Петрович
- Специальность ВАК РФ05.13.17
- Количество страниц 331
Оглавление диссертации кандидат физико-математических наук Немытых, Андрей Петрович
Том 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 Результаты
Рекомендованный список диссертаций по специальности «Теоретические основы информатики», 05.13.17 шифр ВАК
Выявление и доказательство свойств функциональных программ методами суперкомпиляции2010 год, кандидат физико-математических наук Ключников, Илья Григорьевич
Полиномиальная вычислимость в семантическом программировании2023 год, кандидат наук Нечесов Андрей Витальевич
Семантика и анализ сложности алгоритмических проблем динамических систем и языков, использующих логическое программирование2009 год, доктор физико-математических наук Дехтярь, Михаил Иосифович
Трассирующая нормализация2018 год, кандидат наук Березун Даниил Андреевич
Методы и инструментальные средства формальной верификации функционально-потоковых параллельных программ2022 год, кандидат наук Ушакова Мария Сергеевна
Введение диссертации (часть автореферата) на тему «Специализация функциональных программ методами суперкомпиляции»
В семидесятых годах В. Ф. Турчин предложил ряд идей по автоматическому преобразованию программ, которые назвал суперкомпиляцией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 наименования.
Похожие диссертационные работы по специальности «Теоретические основы информатики», 05.13.17 шифр ВАК
Доказательство свойств функциональных программ методом насыщения равенствами2018 год, кандидат наук Гречаник Сергей Александрович
Исследование и реализация базовой вычислительной машины с внутренним языком высокого уровня2003 год, кандидат технических наук Чернов, Сергей Александрович
Математическое моделирование алгебраических и аналитических преобразований на ветвящихся структурах1997 год, доктор физико-математических наук Корольков, Юрий Дмитриевич
Автоматический вывод индуктивных инвариантов программ с алгебраическими типами данных2024 год, кандидат наук Костюков Юрий Олегович
Интеграция разнородных языковых механизмов в рамках одного языка программирования2002 год, кандидат физико-математических наук Столяров, Андрей Викторович
Список литературы диссертационного исследования кандидат физико-математических наук Немытых, Андрей Петрович, 2007 год
1. Разработаны и реализованы аппроксимирующие алгоритмы распознавания частично рекурсивных константных функций, частично рекурсивных функций проекции. Показано, что на некоторых примерах эти алгоритмы способны понижать временную сложность программы.
2. Предложено понятие частично рекурсивного монома конкатенации.
3. Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация супер компилятора доступна на Web-странице в режиме online 90.
Обратите внимание, представленные выше научные тексты размещены для ознакомления и получены посредством распознавания оригинальных текстов диссертаций (OCR). В связи с чем, в них могут содержаться ошибки, связанные с несовершенством алгоритмов распознавания. В PDF файлах диссертаций и авторефератов, которые мы доставляем, подобных ошибок нет.