[Главная] [ ПСПА лаб. ] [ "Ботик" лаб. ] [ АП лаб. ] [ ПО и АС мультипроцессорных систем ] [ Региональные компьютерные сети. ] [ Метавычисления, функциональные языки программирования ] [ Исследование задач малой размерности ] [ Сотрудники ] [ Публикации ]

Метавычисления, функциональные языки программирования

• Метавычисления и суперкомпиляция
• Метапрограммирование
• Функциональные языки программирования: Рефал, Flac
• Системы компьютерной алгебры: CAC, DoCON

Метавычисления и суперкомпиляция

Термин метавычисления означает раздел теории и практики программирования, связанный с построением конструктивных метасистем — метапрограмм над программами,— и, за счет этого, реализации условий для метасистемных переходов (эволюции) в "мире программ", реализации конструктивных и эффективных методов анализа, вычисления и преобразования программ. Заметим, что Кондратьев Н. В., организатор и первый руководитель лаборатории АП, автоматизацию программирования понимал именно как всемерное развитие методов метавычисления (в том числе — суперкомпиляции) и внедрение их в практику программирования.

Работы в области суперкомпиляции для языка программирования Рефал имели для некоторых сотрудников ИЦМС ИПС РАН давнюю предысторию: Кондратьев Н. В. и Абрамов С.М. под руководством профессора Турчина В. Ф. занимались данными исследованиями еще в далекие 1970-ые годы. И в стенах ИПС РАН данные работы выполнялись в тесном сотрудничестве с проф. Турчиным В. Ф., который в эти годы проживал в США и работал на факультете информатики Университета города Нью-Йорка (Computer Science Department, the City University of New York.).

В данных работах ведущую роль играл Немытых А. П., в разные годы принимали участие Абрамов С. М., Чмутов С. В., Конышев А. П., Игнатович И. М., Козадой В. Ф., Пинчук В. А., Чмутова Н. А. 

Суперкомпиляция   [1-82, 6-95, 7-95, 8-96, 9-96]   является одним из методов метавычислений, мощной техникой преобразования программ. Ближайшие аналоги (частичные вычисления, deforestation, частичная дедукция, смешенные вычисления) являются более изученными методами, но суперкомпиляция стала более мощным инструментом, при помощи которого можно решить не только решаемые другими методами задачи, но и более сложные. Суперкомпиляция является некоторым видом абстрактной интерпретации, где используется не только полная информация (как в частичных вычислениях) о некоторых аргументах, но и частичная информация. Результаты работ по суперкомпиляции, полученные в ИЦМС ИПС РАН, неоднократно докладывались на международных конференциях и семинарах в Переславле-Залесском, Новосибирске, Нью-Йорке (США), Копенгагене (Дания), Dagstuhl Castle (Германия), Токио (Япония), Пекине (Китай), Ливерпуле (Великобритания), Турку (Финляндия)

Данные работы были поддержаны:

• РФФИ, грант No 94-01-01352-а, "Совместная реализация языков программирования REFAL+ и FLAC", 1994-1995 гг.;
• ГКНТ РФ (проект No 2468, "Автоматическое преобразование программ", 1997-1998 гг.);
• грантом фонда "The U.S. CRDF", грант No RM1-254, 1997-1998 гг.;
• Федеральным агентством по науке и инновациям (проект No 2007-4-1.4-18-02-064, "Верификация программ посредством их параметризованного тестирования специализаторами на базе моделей этих программ, реализация верификатора для языка программирования Java"), 2007-2008 гг.;
• совместным грантом РФФИ и Государственного фонда естественных наук (ГФЕН) Китая, грант No 07-07-92100-ГФЕН_а, "Развитие методов суперкомпиляции для типизированного функционального языка", 2007-2009 гг.;
• РФФИ, грант No. 08-07-00280-а, "Развитие технологий высокопродуктивного параллельного программирования суперкомпьютеров на основе функционального языка Рефал Плюс и методов метавычислений", 2008-2010 гг.

По направлению "суперкомпиляция для языка Рефал" в 1994-1993 годах выполнялась разработка основных принципов суперкомпиляции. В 1995 году был разработан метод расширения входного языка суперкомпилятора с плоского диалекта языка Рефал до строгого Рефала (за счет матасистемного перехода), была на практике продемонстрирована способность суперкомпилятора из наивного алгоритма поиска неизвестного образца фиксированной длины автоматически сгенерировать алгоритм Кнута-Морриса-Пратта. В том же году был разработан метод автоматического построения программы, решающей обратную задачу по отношению к заданной программе, разработан язык рекурсивного описания информации о данных специализируемой программы, поддерживающий рекурсивное использование суперкомпилятора [6-95, 7-95]. В 1996 году был разработан метод регулярной апроксимации функциональных программ для их более эффективной специализации [8-96]. В 1998 году был разработан функциональный язык Мета-Рефал, ориентированный на метавычисления и реализацию формальных преобразователей программ, реализована первая версия компилятора из Мета-Рефал в язык Рефал. В языке синтаксически поддерживаются как метапеременные, так и метакодировка [6-96]. В 1999 году суперкомпилятор для языка Рефал был доведен до "реальной экспериментальной версии" (См. www.botik.ru/pub/local/scp/refal5/): в качестве входных программ он принимал любые реальные программы на языке Рефал-5. В 2000 году суперкомпилятор Scp4 получил дальнейшее развитие: разработана и реализована первая версия компилятора из языка Рефал-графов (язык внутреннего представления программ в суперкомпиляторе Scp4) в язык программирования С (компилятор оптимизирует функции с "хвостовой" рекурсией и позволяет повысить временную эффективность результата суперкомпиляции, в среднем, в пять раз). В 2008 году начаты работы по графической поддержке интерфейса суперкомпилятора SCP4 и адаптации алгоритмов Хмелевского и Маканина решения уравнений в свободной полугруппе для разработки и анализа описания свойств параметризованных Рефал-конфигураций.

Кроме работ по суперкомпиляции для языка Рефал в ИЦМС ИПС РАН проводится серия работ по общим вопросам метавычислений и их применений в теории и практики программирования (Абрамов С. М.) в рамках которых формулируются и исследуются новые понятия теоретических основ информатики:

• инверсное вычисление программ, инверсная семантика, инверсное программирование, повышение эффективности инверсных вычислений [2-89, 2-91, 3-00, 10-01, 3-02, 4-02, 6-03] ;
• окрестностный анализ и его применение, окрестностное тестирование программ [1-83, 2-83, 1-84, 3-87, 2-93, 3-94] ;
• нестандартные семантики, нестандартные диалекты языков программирования, модификаторы семантик, метавычисления (инверсные вычисления, окрестностный анализ, суперкомпиляция) как примеры нестандартных семантик, использование специализации (суперкомпиляции) для эффективной реализации нестандартных семантик [8-95, 7-98, 4-00, 5-00].

К области метавычислений относятся и работы 1995 года Пименова С. П. [4-94, 5-94], в которых рассматривается связь между специализацией программ и параллелельными вычислениями в среде Т-системы. Данные работы можно считать предвестниками сегодняшних исследований в ИЦМС ИПС РАН на близкую тему [5-04].

В июле 2008 года в Переславле-Залесском в Институте программных систем имени А.К. Айламазяна РАН прошла первая международная конференция по метавычислениям "μετα 2008".

Метапрограммирование

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

Совместно с А.П. Лисицей (бывшим сотрудником ИПС РАН) из Лаборатории верификации Ливерпульского университета (University of Liverpool, http://www.csc.liv.ac.uk/) разработан метод верификации параметризованных вычислительных систем посредством суперкомпиляции их программных моделей. Под параметризованной вычислительной системой мы понимаем систему, в которой количество участников взаимодействия в процессе эволюции системы конечно, но не известно сколько. Нити в много-поточных Java-программах могут служить примером таких участников. Свойства корректности, которые проверяется, формулируются в терминах недостижимости определенного вида глобальных состояний, рассматриваемой вычислительной системы. Суперкомпилятор специализирует программную модель этой вычислительной системы по свойствам начальных состояний системы. Удачная верификация модели выражается в преобразовании скрытой семантической информации об интересующем нас свойстве модели в явную очевидную синтактическую информацию результата преобразований программной модели суперкомпилятором. Разработанный метод можно охарактеризовать также как параметризованное тестирование.

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

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

• ряд параметризованных протоколов корректности когерентности кэша;
• несколько параметризованных много-поточных моделей Java программ, описанных в терминах однопоточных моделей;
• ряд свойств распределенных вычислительных систем, описанных в терминах сетей Петри.

При интерактивном использовании суперкомпилятора SCP4 найдены ошибки и построены тесты, указывающие на эти ошибки, в

• некорректной спецификации Dragon протокола когерентности кэша;
• некорректной спецификации абстрактной модели протокола Inc/Dec (Atomic Increments and decrements on a Point object) взаимодействия нитей в много-поточной Java программе;
• спецификации SPS2 протокола когерентности кэша.

Причем, если в первых двух случаях эти ошибки оказались только ошибками публикаций конкретных спецификаций (то есть, у авторов протоколов, как выяснилось, имелись корректные спецификации соответствующих протоколов), то протокол SPS2 оказался некорректным по существу. Обнаруженная в протоколе SPS2 ошибка присутствует во всех опубликованных спецификаци этого протокола (см., например, Xuemei Zhao, Sammut K., Fangpo He, Shaowen Qin, Split Private and Shared L2 Cache Architecture for Snooping-based CMP, Computer and Information Science, 2007. ICIS 2007. 6th IEEE/ACIS International Conference on Volume, Issue, 11-13 July 2007 Page(s):900 - 905) и авторы протокола не смогли разумно отреагировать на указание им найденной ошибки.

Некоторые результаты экспериментов по верификации параметризованных вычислительных систем посредством суперкомпилятора SCP4 представлены на странице: http://refal.botik.ru/protocols/. Исследования в области верификации проводились в 2004-2008 гг.

Функциональные языки программирования: Рефал, Flac

Разработка систем программирования для функциональных языков было одним из традиционных направлений работ лаборатории АП. В разные годы здесь выполнялись реализации на различных платформах таких языков как: Микро-Пролог, RL, Рефал-6, Flac и др.  Результаты работ по реализации языка Flac представлены на странице: http://www.botik.ru/pub/local/scp/flac/.

В рамках работ по суперкомпиляции для языка Рефал в 1994-2008 годы велось сопровождение (Немытых А. П., Конышев А. П.) системы программирования Рефал-5 и перенос ее на различные платформы (См. www.botik.ru/pub/local/scp/refal5/): Linux, Free BSD, Windows95/98, Windows-NT, Windows-XP, Windows-Vista, Windows Mobile 5.0, MS-DOS, OS/2.

В 1991-1992 году лаборатория АП сотрудничает с основными разработчиками языка и системы программирования Рефал Плюс [2-88, 3-89], а с 1994 года сопровождение и развитие данной разработки выполняется в ИЦМС ИПС РАН (Козадой В. Ф., Абрамов С. М., Немытых А. П.). В 1995 году выполнен перенос реализации Рефал Плюс в среду операционной системы Linux, выполнены работы по расширению системы в сторону поддержки двух языков: Рефала Плюс и Flac. Система Flac+Рефал Плюс поддерживалась для различных платформ: MS DOS, MS DOS/Protected Mode, OS Linux.

Сегодня данный проект продолжен в работах, связанных с новым подходом к реализации системы программирования Рефал Плюс для различных платформ (включая и мультипроцессорные системы) [7-03, 6-04, 7-04].

Системы компьютерной алгебры: CAC, DoCON.

Выполнение серии работ по системам компьютерной алгебры CAC и DoCON заняло более десяти лет (Мешвелиани С. Д.).

В начале 1990-ых годов на языке программирования Flac был разработан прикладной пакет компьютерной алгебры CAC [3-93], который затем (1994-1993 гг.) был переведен в среду системы программирования Flac+Рефал Плюс. Эти работы стали основой для разработки программы Построитель алгебраических областей (DoCon).

Построитель алгебраических областей (DoCon) [9-95, 11-01]  является результатом применения функционального программирования и так называемого "категорного подхода" в вычислительной алгебре [11-01]. Задание вычислений в такой системе основано на том, что всякий конструктор области ("Многочлен", "Дробь", "Вектор" и др.) рассматривается как алгоритмический функтор, то есть как функтор, порождающий некий стандартный набор алгоритмов для набора операций (+, -, *, ...) для области назначения через алгоритмы соответствующего (возможно, другого) набора действий областей, данных функтору.

В 1995 году в качестве платформы для реализации пакета DoCon был выбран современный язык функционального программирования Haskell. На нем была написана первоначальная версия "Построителя алгебраических областей" [9-95].

Дальнейшее развитие пакета (См. www.botik.ru/pub/local/Mechveliani/docon/) и выпуск (1998-2003 года) очередных версий пакета DoCon-2  [3-93] связано с:

• усовершенствованием архитектуры, основанной на правиле "описание области — в элементе области";
• расширением математической библиотеки (например, реализацией программы разложения на множители многочленов двух переменных над конечным полем коэффициентов методом Григорьева Д. Ю.).

Программный пакет DoCon-2, как средство для символьных вычислений в научных исследованиях, установлен на машине международного центра ресурсов вычислителной алгебры Unite' Mixte de Service MEDICIS\footnote(См. www.medicis.polytechnique.fr).

К данной разработке примыкает и реализация проекта стандартной библиотеки (См. www.botik.ru/pub/local/Mechveliani/basAlgPropos) основной алгебры BAL-0.01 для языка программирования Haskell, в которой предложены средства модификации существующей библиотеки алгебры языка Haskell при использовании его для программирования математических приложений (Мешвелиани С. Д.).

Последнее изменение: 21.01.2009