Конференция, посвященная 90-летию со дня рождения Алексея Андреевича Ляпунова

Россия, Новосибирск, Академгородок, 8 - 11 октября 2001 года,
(номер государственной регистрации 0320300063)

Тезисы докладов


Программирование

Обоснование оптимизирующих преобразований: Модели и результаты

Поттосин И.В., Уваров Д.Л.

ИСИ СО РАН (Новосибирск)

А.А.Ляпунов стоял у истоков внутренней проблематики программирования. Его операторный метод был основой первых областей системного и теоретического программирования в нашей стране: языков и систем программирования и теории схем программ. На операторном методе основывались входные языки первых советских трансляторов - программирующих программ. Первая формальная модель программ - операторные схемы Янова - была по существу формализацией понятий операторного метода.

Единство происхождения как информационных, так и математических моделей объясняет и одну из сторон их применения: в программирующих программах особое внимание уделялось оптимизации программ, а в схемах Янова рассматривались проблемы эквивалентных преобразований программ. Однако прямого взаимодействия между системными и теоретическими подходами не было: схемы Янова были слишком грубыми приближениями к реальным программам, не отражали ряд существенных для оптимизации программ свойств и не могли быть прямо используемы для обоснования практических оптимизирующих преобразований и алгоритмов их выполнения.

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

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

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

Желание построить существенно более мощную модель программ, пригодную для выражения широкого класса оптимизирующих преобразований, привело В.Н.Касьянова к разработке такой модели как крупноблочные схемы. Используя ряд понятий, введенных в линейных схемах, они существенно развивали эти схемы, учитывая и проблемы переименования, и нелинейность программной структуры. Крупноблочные схемы использовались, в основном, для переформулирования утверждений, доказанных для кратных схем.

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

Кратные схемы были очень простой моделью - даже для обоснования корректности таких преобразований, как объединение и расчленение циклов пришлось несколько развить модель. Для всего же множества преобразований чистки участков повторяемости гамаков, циклов, тел рекурсивных процедур Д.Л.Уварову пришлось ввести новую модель - регулярные схемы, среднюю по мощности модель между кратными и крупноблочными схемами. На этой модели были определены контекстные условия чистки гамаков и чистки тел рекурсивных процедур, а также была доказана оптимальность предложенных алгоритмов чистки регулярных схем (включающая чистку как гамаков, так и циклов) и чистки тел рекурсивных процедур.

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

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



Ваши комментарии
[SBRAS]
[Головная страница]
[Конференции]
[СО РАН]

© 2001, Сибирское отделение Российской академии наук, Новосибирск
© 2001, Объединенный институт информатики СО РАН, Новосибирск
© 2001, Институт вычислительных технологий СО РАН, Новосибирск
© 2001, Институт систем информатики СО РАН, Новосибирск
© 2001, Институт математики СО РАН, Новосибирск
© 2001, Институт цитологии и генетики СО РАН, Новосибирск
© 2001, Институт вычислительной математики и математической геофизики СО РАН, Новосибирск
© 2001, Новосибирский государственный университет
Дата последней модификации 06-Jul-2012 (11:45:21)