ПАРАЛЛЕЛЬНЫЕ ВЫЧИСЛЕНИЯ ~
УДК 004.423.4
МОДЕЛЬ ДИНАМИЧЕСКОГО ПАРАЛЛЕЛЬНОГО ИСПОЛНЕНИЯ ПРОГРАММ
© 2013 г. В.А. Васенин*, М.А. Кривчиков**
*Научно-исследовательский институт механики МГУ имени М. В. Ломоносова
119192 Москва, Мичуринский пр-т. , 1 **Механико-м,атем,атический факультет МГУ 119991 Москва, Ленинский горы, мкр., 1 E-mail: vasenin@msu.ru, maxim.krivchikov@gmail.com Поступила в редакцию 06.07.2012
Динамическое параллельное исполнение позволяет эффективно адаптировать программы для их выполнения в вычислительной среде параллельной архитектуры. В настоящей статье представлена формальная модель динамического параллельного исполнения программ без побочных эффектов. Для модели доказывается свойство, гарантирующее корректность параллельного исполнения.
1. ВВЕДЕНИЕ
Одной из основных тенденций современного этапа развития вычислительных средств и систем высокой производительности является увеличение количества параллельно обрабатываемых потоков вычислений. При разработке или модернизации существующего программного обеспечения эту тенденцию необходимо учитывать. В этой связи актуальным является процесс адаптации программ для их эффективного использования в вычислительной среде параллельной архитектуры.
Подходы к параллельному исполнению программ делят на статический и динамический. При статическом параллельном исполнении различные вычислительные потоки программы распределяются по вычислительным устройствам до запуска программы. При динамическом параллельном исполнении решение породить новый вычислительный поток принимается в процессе выполнения программы. В процессе адаптации программы для параллельного исполнения важно убедиться, что определенные свойства программы, в первую очередь результаты вычислений на отдельных этапах, сохраняются. Одной из гарантий выполнения этих и ряда других функциональных требований,
предъявляемых к программе, является возможность ее верификации с использованием модели, описывающей семантику программы. С этих позиций настоящая публикация представляет результаты, которые являются продолжением работы «Статическая формальная семантика стандарта ЕСМА-335» [1].
В данной публикации представлена базовая модель динамического параллельного исполнения программ, функции которых не имеют побочных эффектов, для случая, когда взаимодействие потоков вычислений может осуществляться путем порождения нового потока, который вычисляет значение некоторой функции программы, или ожидания результата вычислений от некоторого потока, порожденного ранее. Примерами реализации подобного подхода являются МиШЫвр [2] п \VwTS [3]. Под функциями, не имеющими побочных эффектов, в настоящей работе понимаются функции, возвращаемое значение которых зависит только от входных аргументов, и которые в процессе вычислений не изменяют значение глобальных переменных.
Для изучения свойств параллельного исполнения программ представляется целесообразным прежде всего абстрагироваться от вычислений, которые выполняются в программе, и исследовать свойства программы исключительно с по-
зиций порядка исполнения отдельных ее блоков. С этой целью в настоящей публикации использован язык управления потоком исполнения. В качестве примера применения предложенной модели к распространенным языкам программирования приводится способ преобразования подмножества программ, соответствующих стандарту ЕСМА-335, к языку управления потоком исполнения с использованием статической формальной семантики стандарта ЕСМА-335.
В настоящей публикации модель динамического параллельного исполнения программы представлена с использованием подхода к ее описанию на основе денотационной семантики, который был предложен в 1970-х гг. независимо Д. Скоттом и К. Стрейчи [4] и Ю.Л. Ершовым [5]. Для модели доказан набор утверждений, гарантирующих корректность исполнения программы с точки зрения результата ее исполнения. Подобные утверждения были доказаны для MultiLisp и NewTS с использованием операционной семантики. Однако денотационная семантика позволила получить такие результаты в более естественном и простом для интерпретации виде.
Представленная далее модель динамического параллельного исполнения программ описана со следующими ограничениями.
1. Считается определенной динамическая семантика некоторых блоков кода программы.
2. Отсутствует глобальное изменяемое состояние. Это ограничение означает, что результат выполнения любой функции программы зависит только от входных данных.
3. Функция, являющаяся точкой входа (entry point) программы, возвращает некоторое значение, которое считается результатом выполнения программы.
4. Взаимодействие вычислительных потоков программы производится с помощью системных вызовов двух видов: spawn — создание нового вычислительного потока, точкой входа которого является указанная функция; wait — ожидание завершения потока с определенным идентификатором и получение возвращенного потоком значения.
5. Обработку системных вызовов и планирование выполнения потоков осуществляет внешняя по отношению к программе система. Модель обработки системных вызовов и планирования потоков представлена в настоящей работе.
6. Определены два специальных режима исполнения программы, которые далее называются «режим исполнения по порядку» (inorder evaluation) и «режим исполнения по требованию» (lazy evaluation). При исполнении программы в этих режимах считается, что одновременно производить вычисление может только один поток.
7. Под режимом исполнения программы по порядку понимается такой способ планирования потоков вычислений, при котором после системного вызова spawn выполнение вызывающего потока приостанавливается до того времени, когда будет завершен поток, созданный в результате обработки системного вызова. Такой режим считается эквивалентным последовательному исполнению программы, при котором системный вызов spawn работает как вызов функции программы, а системный вызов wait получает значение, возвращенное функцией. Эквивалентность может быть определена и проверена в случае, когда определена динамическая семантика программы.
8. Под режимом исполнения программы по требованию понимается такой способ планирования потоков, при котором до первого системного вызова wait выполняется поток, соответствующий точке входа программы (далее — «главный поток»), а затем управление переходит к потоку, завершения которого ожидает главный поток. В результате каждого системного вызова wait управление переходит к тому потоку, завершения которого ожидает предыдущий. Таким образом, производятся только те вычисления, которые непосредственно необходимы для получения результата программы.
Такие ограничения относительно адекватно описывают семантику процессов параллельного исполнения программ без побочных эффектов. В
частности, пунктом 2 допускается использование общих блоков памяти при условии, что они используются только для чтения. Добавление других способов взаимодействия потоков вычислений, как отмечено в заключении, является одним из направлений дальнейших исследований.
2. ЯЗЫК УПРАВЛЕНИЯ ПОТОКОМ ИСПОЛНЕНИЯ
Язык управления потоком исполнения (управляющий язык) представляет собой императивный язык программирования, основное предназначение которого — описание порядка исполнения команд произвольного языка.
Прежде всего, введем параметры, с помощью которых достигается абстракция от деталей реализации императивного языка.
Домен § определяет допустимые значения локального состояния функции, включая локальные переменные, аргументы и возвращаемое значение. Функции языка управления потоком исполнения выражаются в семантике как преобразующие локальное состояние (§ ^ §). Домен СГ определяет функции, изменяющие локальное состояние. Такие функции используются для абстракции производимых программой вычислений, а также для задания исходного локального состояния функции при вызове или создании потока. Домен МГ определяет функции, выполняющие слияние локального состояния выполняемой функции с результатом вызова некоторой другой функции. Домен ВГ определяет функции, возвращающие булевское значение. В зависимости от результата выполнения таких функций, может быть выполнена та или иная ветвь программы. Домен ТГ определяет функции, которые содержат команды языка управления потоком исполнения.
С помощью семантики языка определяются окружения, которые устанавливают соответствие между блоками кода и функциями, определяющими их значение (рис. 1).
Се : СГ ^ § ^ § Ме : МГ ^ § ^ § ^ § Ве : ВГ ^ § ^ В
Рис. 1.
Окружения семантики императивного языка.
На рисунке 2 представлены параметры, отражающие специфику модели динамического параллельного исполнения. Домен Id определяет тип идентификаторов потоков, порождаемых при динамическом параллельном исполнении. Домен Var определяет переменные, содержащие идентификаторы потоков.
Id, Var
Vm : Var ^ Var
Рис. 2.
Параметры, отражающие специфику модели динамического параллельного исполнения.
Для упрощения изложения предположим, что идентификаторы потоков неизменяемы. Потребуем, чтобы значения переменных, содержащих идентификаторы потоков, передавались в качестве параметров в другие функции только с по-
Vm
На рисунке 3 представлен набор команд языка управления потоком исполнения St.
St = skip
| comp c
| si ; S2
| if b then st elses/
| while b do s
| call t, c, u, m
| v = spawn t, c, u
| wait v, m
Рис. 3.
Набор команд языка управления потоком исполнения.
skip
изменяя локальное состояние.
2. Для любой функции c из Cf, команда comp c выполняет вычисление, которое за-c
далее, изменив локальное состояние.
si s2 si ; s2
si
s2
4. Для любой функции b из Bf и для любых команд st, s/, команда if b then st else s/ вы-
b
ности условия, управление передается команде st. В случае ложности условия, управление передается команде Sf.
5. Для любой функции b из Bf, и для любой команды s, команда while b do s представля-
bS
6. Для любой функции t из Tf, для любой функции c из Cf, для любого модификатора u из Vm, а также для любой функции m из Mf, команда call t,c,u,m выполняет
t
c
ременные, содержащие идентификаторы потоков пере
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.