научный журнал по математике Программирование ISSN: 0132-3474

ЛИСИЦА А.П., НЕМЫТЫХ А.П. — 2010 г.

Пусть дана программа P(d), реализующая частично рекурсивную функцию ц. Рассмотрим на области определения последней функцию OP, значением которой является путь вычисления программы P на фиксированном данном d0. Пусть программа Q(p,d) определена тогда и только тогда, когда p = OP (d); причем Q(OP (d),d)= P (d). Программа Q(p,d), абсурдная с точки зрения ее практического вычисления на конкретных входных данных, может быть практически полезной при ее автоматическом мета-анализе. В статье показывается, как программа Q(p,d) может быть использована для верификации программы P(d) по постусловию. Предлагаемый метод опробован на задачах верификации протоколов когерентности кэша и других распределенных вычислительных систем.

ВИРБИЦКАЙТЕ И.Б., ГРИБОВСКАЯ Н.С. — 2010 г.

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

НУРИЕВ Р.М. — 2010 г.

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

ЗОБНИН А.И. — 2010 г.

В этой обзорной работе представлен общий подход к известному алгоритму вычисления базисов Гребнера F5, созданному Ж.-Ш. Фожером в 2002 г.

ЛЕПИХОВ А.В., СОКОЛИНСКИЙ Л.Б. — 2010 г.

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

ШТЕЙНБЕРГ Р.Б. — 2010 г.

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

ПОДЛОВЧЕНКО Р.И. — 2010 г.

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

ИСАЕВ И.К., СИДОРОВ Д.В. — 2010 г.

В статье описывается Avalanche - инструмент обнаружения программных дефектов при помощи динамического анализа. Avalanche использует возможности динамической инструментации программы, предоставляемые Valgrind [1], для сбора и анализа трассы выполнения программы. Результатом такого анализа становится либо набор входных данных, на которых в программе возникает ошибка, либо набор новых тестовых данных, позволяющий обойти ранее не выполнявшиеся и, соответственно, еще не проверенные фрагменты программы. Таким образом, имея единственный набор тестовых данных, Avalanche реализует итеративный динамический анализ, при котором программа многократно выполняется на различных, автоматически генерированных тестовых данных, при этом каждый новый запуск увеличивает покрытие кода программы такими тестами. Описаны принципы работы Avalanche, а также приведены результаты применения инструмента к нескольким проектам с открытым исходным кодом. Было обнаружено свыше 15 программных дефектов, многие из которых подтверждены и уже исправлены разработчиками.

ШАКИРОВ Р.Н. — 2010 г.

Обсуждается практика использования автоматических методов обнаружения и компенсации ошибок в классе cBigNumber, написанном на языке C++ для выполнения операции над неограниченными целыми числами. Класс реализует штатные операции языка C++, извлечение квадратного корня, возведение в степень по модулю и проверку на простоту по методу Миллера-Рабина. Тестирование класса проведено в автоматическом режиме. Достоверность вычислений обеспечивается встроенными средствами контроля и компенсации ошибок.

КАЛЕНКОВА А.А. — 2010 г.

На основе предложенных нами ранее графов анализа потоков работ [1] и известного метода условной конверсии [2] создан новый алгоритм верификации потоков работ. Алгоритм использует булеву алгебру, что отражено в его названии - алгоритм булевой верификации (АБВ). АБВ работает с произвольными перекрывающимися структурами графа и циклами. Временная сложность предлагаемого алгоритма в случае с насыщенными графами не превышает таковую для большинства других алгоритмов верификации потоков работ [3-6]. В процессе верификации АБВ определяет условие выполнения каждой вершины графа, что дает возможность дополнительно создать алгоритм оптимизации потоков работ. В отличие от известных алгоритмов структурной оптимизации потоков работ, базирующихся на применении шаблонных преобразований [7, 8], предлагаемый алгоритм оптимизации позволяет максимально (в пределах цикла) распараллелить поток работ, содержащий произвольные перекрывающиеся структуры.

ФИЛИППОВ А.Н. — 2010 г.

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

БУРДОНОВ И.Б., КОСАЧЕВ А.С. — 2010 г.

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

АБРАМОВ С.А., БОГОЛЮБСКАЯ А.А., ЕДНЕРАЛ В.Ф., РОСТОВЦЕВ В.А. — 2010 г.

Годовой отчет о работе научно-исследовательского семинара по компьютерной алгебре.

БУДЬКО Д.А., ПРОКОПЕНЯ А.Н. — 2010 г.

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

РЯБЕНКО А.А., ХМЕЛЬНОВ Д.Е. — 2010 г.

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

БАШКИН В.А. — 2010 г.

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

НОВИКОВ Ф.А., НОВОСЕЛЬЦЕВ В.Б. — 2010 г.

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

МАХОРТОВ С.Д. — 2009 г.

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

ДРОЗДОВ А.Ю., НОВИКОВ С.В. — 2009 г.

В данной работе описывается автоматический распараллеливатель программ, созданный на базе компонентного подхода к построению оптимизирующих компиляторов и встроенный в технологическую цепочку gcc. В работе рассмотриваются детали использования аналитических и оптимизационных компонент для построения авто-распараллеливателя и алгоритм распараллеливания с использованием библиотеки OpenMP. В заключении приведены результаты работы авто-распараллеливателя по производительности на подмножестве задач из пакетов Spec2006 и NAS parallel benchmarks.

ДОЛГОВА Е.Н., ЧЕРНОВ А.В. — 2009 г.

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