Algebra-dynamic models for program parallelization
We propose algebra-dynamic models and a method for checking correctness of optimizing transformations for multithread programs and programs for graphical processing units. Proposed models are used together with rewriting rules technique to prove correctness of transformations and increase effectiven...
Saved in:
| Date: | 2025 |
|---|---|
| Main Authors: | , |
| Format: | Article |
| Language: | Russian |
| Published: |
PROBLEMS IN PROGRAMMING
2025
|
| Subjects: | |
| Online Access: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/845 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Problems in programming |
| Download file: |  |
Institution
Problems in programming| id |
pp_isofts_kiev_ua-article-845 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/af/f3bed0356b653f464c178f3b5e959eaf.pdf |
| spelling |
pp_isofts_kiev_ua-article-8452025-09-08T13:41:18Z Algebra-dynamic models for program parallelization Алгебро-динамические модели для распараллеливания программ Алгебро-динамічні моделі для розпаралелювання програм Doroshenko, A.Yu. Zhereb, K.A. UDC 681.3 УДК 681.3 УДК 681.3 We propose algebra-dynamic models and a method for checking correctness of optimizing transformations for multithread programs and programs for graphical processing units. Proposed models are used together with rewriting rules technique to prove correctness of transformations and increase effectiveness of program parallelization.Problems in programming 2010; 1: 39-55 Предложены алгебро-динамические модели и метод проверки корректности оптимизирующих преобразований для многопоточных программ и программ для графических ускорителей. Описано использование этих моделей с помощью техники переписывающих правил для доказательства корректности преобразований и повышения эффективности распараллеливания вычислений.Problems in programming 2010; 1: 39-55 Запропоновано алгебро-динамічні моделі та метод перевірки коректності оптимізуючих перетворень для мультипоточних програм та програм для графічних прискорювачів. Описано використання цих моделей за допомогою техніки переписувальних правил для доведенні коректності перетворень та підвищення ефективності розпаралелювання обчислень.Problems in programming 2010; 1: 39-55 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-09-08 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/845 PROBLEMS IN PROGRAMMING; No 1 (2010); 39-55 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2010); 39-55 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2010); 39-55 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/845/896 Copyright (c) 2025 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2025-09-08T13:41:18Z |
| collection |
OJS |
| language |
Russian |
| topic |
UDC 681.3 |
| spellingShingle |
UDC 681.3 Doroshenko, A.Yu. Zhereb, K.A. Algebra-dynamic models for program parallelization |
| topic_facet |
UDC 681.3 УДК 681.3 УДК 681.3 |
| format |
Article |
| author |
Doroshenko, A.Yu. Zhereb, K.A. |
| author_facet |
Doroshenko, A.Yu. Zhereb, K.A. |
| author_sort |
Doroshenko, A.Yu. |
| title |
Algebra-dynamic models for program parallelization |
| title_short |
Algebra-dynamic models for program parallelization |
| title_full |
Algebra-dynamic models for program parallelization |
| title_fullStr |
Algebra-dynamic models for program parallelization |
| title_full_unstemmed |
Algebra-dynamic models for program parallelization |
| title_sort |
algebra-dynamic models for program parallelization |
| title_alt |
Алгебро-динамические модели для распараллеливания программ Алгебро-динамічні моделі для розпаралелювання програм |
| description |
We propose algebra-dynamic models and a method for checking correctness of optimizing transformations for multithread programs and programs for graphical processing units. Proposed models are used together with rewriting rules technique to prove correctness of transformations and increase effectiveness of program parallelization.Problems in programming 2010; 1: 39-55 |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2025 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/845 |
| work_keys_str_mv |
AT doroshenkoayu algebradynamicmodelsforprogramparallelization AT zherebka algebradynamicmodelsforprogramparallelization AT doroshenkoayu algebrodinamičeskiemodelidlârasparallelivaniâprogramm AT zherebka algebrodinamičeskiemodelidlârasparallelivaniâprogramm AT doroshenkoayu algebrodinamíčnímodelídlârozparalelûvannâprogram AT zherebka algebrodinamíčnímodelídlârozparalelûvannâprogram |
| first_indexed |
2025-09-17T09:25:29Z |
| last_indexed |
2025-09-17T09:25:29Z |
| _version_ |
1850409914573258752 |
| fulltext |
Моделі та засоби паралельних і розподілених програм
39
УДК 681.3
А.Е. Дорошенко, К.А. Жереб
АЛГЕБРО-ДИНАМИЧЕСКИЕ МОДЕЛИ ДЛЯ
РАСПАРАЛЛЕЛИВАНИЯ ПРОГРАММ
Предложены алгебро-динамические модели и метод проверки корректности оптимизирующих преобра-
зований для многопоточных программ и программ для графических ускорителей. Описано использова-
ние этих моделей с помощью техники переписывающих правил для доказательства корректности пре-
образований и повышения эффективности распараллеливания вычислений.
Введение
В настоящее время активно разви-
ваются новые аппаратные платформы для
параллельных вычислений, такие как мно-
гоядерные процессоры [1] и графические
ускорители [2]. Эти устройства являются
доступными по цене и установлены в
большинстве современных компьютеров.
При этом эти платформы позволяют суще-
ственно повысить производительность
приложений, за счет их распараллелива-
ния. Однако современные средства разра-
ботки параллельных программ для таких
платформ являются достаточно сложными
и требуют от разработчика использования
новых моделей программирования и зна-
ния деталей аппаратной и программной
реализации.
Таким образом, актуальной являет-
ся задача автоматизации разработки па-
раллельных программ. В работах [3–5] ав-
торами предложен подход, основанный на
автоматизации преобразований программ с
использованием техники переписывающих
правил [6–8]. Однако при использовании
этого подхода возникает вопрос о кор-
ректности применяемых преобразований:
будет ли преобразованная программа эк-
вивалентна исходной, или в процессе пре-
образования были внесены ошибки?
В данной работе предложен метод
проверки корректности преобразований
для многопоточных программ и программ
для графических ускорителей. Для этих
платформ построены модели исполнения
программ с использованием алгебро-
динамического подхода [9]. В терминах
построенных моделей сформулированы
свойства, определяющие корректность
преобразований, и приведены условия, по-
зволяющие доказывать такие свойства.
Предложены методы построения модели и
проверки условий с использованием тех-
ники переписывающих правил. Приведены
примеры доказательства корректности
преобразований.
Вопрос доказательства корректно-
сти оптимизирующих преобразований дос-
таточно хорошо исследован в литературе.
Так, в работе [10] предложен алгоритм для
доказательства корректности оптимизи-
рующих преобразований, направленных на
изменение структуры циклов. Работы [11–
12] описывают системы Cobalt и Rhodium
для задания преобразований программ и
автоматического доказательства их кор-
ректности. Авторы [13] используют аппа-
рат темпоральной логики для ручного до-
казательства корректности некоторых
классических оптимизирующих преобра-
зований. В работе [14] описан разработан-
ный автором компилятор для подмножест-
ва языка C и доказана его корректность.
Однако все эти работы рассматривают
преобразования только в контексте работы
оптимизирующего компилятора, тогда как
в данной работе рассмотрены преобразо-
вания на уровне исходного кода.
Кроме того, в работах [10–13] ис-
пользуются способы записи преобразова-
ний, по сути эквивалентные переписы-
вающим правилам, но в каждом случае эта
функциональность реализована «с нуля»; в
результате используются непривычные
пользователю обозначения и отсутствуют
© А.Е. Дорошенко, К.А. Жереб, 2010
ISSN 1727-4907. Проблеми програмування. 2010. № 1
Моделі та засоби паралельних і розподілених програм
40
некоторые средства, стандартные для сис-
тем переписывающих правил. В данной
работе используется система Termware [6–
8], предоставляющая унифицированное
представление преобразований различных
видов. В этом смысле данная работа близ-
ка к [15], где используется система Maude
[16] для автоматического доказательства
определенных свойств многопоточных
программ. Однако в работе [15] сделана
попытка полностью автоматического дока-
зательства свойств программ путем пере-
бора всех вариантов исполнения, что при-
водит к невозможности использования та-
кого подхода для многих практических за-
дач в силу большой вычислительной
сложности. В данной работе использован
более практический подход, основанный
на комбинации статического анализа и ав-
томатической генерации тестов, поэтому
рассмотренный подход применим к более
широкому кругу задач.
Материал данной работы организо-
ван следующим образом. В разделе 1 по-
строена модель исполнения для многопо-
точных программ, а также рассмотрен ме-
тод доказательства корректности преобра-
зований на основе этой модели. Раздел 2
содержит аналогичную модель для про-
грамм, исполняемых на графических уско-
рителях. Раздел 3 описывает автоматиза-
цию использования моделей c помощью
системы переписывающих правил Term-
ware. Работу завершают выводы и направ-
ления дальнейшей работы.
1. Модель многопоточных
программ
1.1. Общее описание модели. Дан-
ный раздел описывает модель для много-
поточных программ. Однако общая схема
подхода, описанного здесь, будет исполь-
зована также для построения модели для
графических ускорителей (раздел 2).
Вначале опишем модель собственно
программы (синтаксическую модель), ис-
пользуя алгебру алгоритмов Глушкова
(АГ) [9]. Далее построим модель исполне-
ния программы (семантическую модель).
Для описания процесса исполнения ис-
пользуется алгебро-динамический подход
[9]. На основе описанных моделей опреде-
лим важнейшие свойства программ. Ис-
пользование этих свойств позволяет дока-
зывать корректность преобразований про-
грамм; рассмотрим примеры подобных до-
казательств для конкретных преобразова-
ний. Проверка описанных свойств прово-
дится в автоматизированном режиме, с ис-
пользованием системы Termware – этот
процесс описан в разделе 3.
1.2. Модель программы. Будем
использовать следующую упрощенную
модель программы на современных языках
программирования. Программа состоит из
множества компонентов, соответствующих
отдельным методам (функциям, процеду-
рам) языка программирования:
1{ ,..., }kP P P= .
Будем считать, что компонент опи-
сывается идентификатором (именем, уни-
кальным в пределах программы), а также
моделью кода:
( , )i i iP name code= .
Для моделирования кода будем ис-
пользовать алгебру алгоритмов Глушкова.
Процедурный код будем представлять в
виде выражения этой алгебры. Алгебра
Глушкова (АГ) является двухосновной ал-
геброй ( , )A Y U , содержащей множества
операторов Y и условий (предикатов) U .
В алгебре определены стандартные опера-
ции: логические операции конъюнкции
AND, дизъюнкции OR и отрицания NOT ,
последовательная композиция THEN ,
ветвление IF , итерация (цикл) WHILE .
На множествах операторов и усло-
вий вводятся базовые элементы, после чего
можно строить различные выражения ал-
гебры, которые будут описывать сложные
операторы и условия. Базовые операторы и
условия обычно зависят от предметной об-
ласти. Выделим один базовый оператор,
общий для всех предметных областей: вы-
зов метода ( )icall P .
1.3. Модель исполнения последо-
вательной программы. Для описания ис-
полнения программ будем использовать
общие понятия теории дискретных дина-
мических систем [9]. Дискретная динами-
ческая система (ДДС) определяется как
тройка 0( , , )S S d , где S – множество, на-
Моделі та засоби паралельних і розподілених програм
41
зываемое пространством состояний;
S0⊆ S – множество начальных состояний;
d S S⊂ × – бинарное отношение перехо-
дов в пространстве состояний. Система
может перейти из состояния is в состояние
js , если ( , )i js s d∈ .
Для построения модели исполнения
необходимо определить интерпретацию
выражений алгебры Глушкова, из которых
состоит программа. Пусть V – множество
переменных программы. Для простоты бу-
дем считать, что переменные не имеют ти-
па и принимают значения в некотором
универсальном множестве D . Частичные
отображения :b V D→ переменных на их
значения будем называть состояниями па-
мяти. Информационной средой является
множество состояний памяти:
{ : }B b V D= → .
Тогда операторы алгебры алгорит-
мов интерпретируются как функции на
множестве B , а условия – как предикаты
на том же множестве. Интерпретация ба-
зовых операторов и условий определяется
в рамках соответствующей предметной
области.
Теперь можно определить ДДС, ко-
торая описывает исполнение последова-
тельной программы. Состояния имеют вид
( , , )s b R F= , где b B∈ – текущее состоя-
ние памяти, R Y∈ – текущее состояние
управления, представленное в виде оста-
точной программы, *( )F P Y∈ → – стек вы-
зовов функций, т.е. последовательность
идентификаторов функций и операторов
АГ, описывающих состояние управления
данной функции. Начальное состояние для
заданной программы имеет вид
0 0( , ( ), ( ))m ms b Y P P= → ∅ , где mP – основ-
ная функция (точка входа в программу).
Отношение перехода задается следующи-
ми правилами перехода:
1) ( , , ) ( ( ), , )b yR F y b R F→ , где y Y∈ –
базовый оператор;
2) ( , ( , , ) , )b if u P Q R F →
( , , ), ( ) 1,
( , , ), ( ) 0;
b PR F u b
b QR F u b
=
→ =
3) ( , ( , ) , )b while u P R F →
( , ( , ) , ), ( ) 1,
( , , ), ( ) 0;
b Pwhile u P R F u b
b R F u b
=
→ =
4) ( , ( ) , (..., ))j ib call P R P→ ∅ →
( , ( ), (..., , ))j i jb Y P P R P→ → → ∅ ;
5) ( , , (..., , ))i jb P R Pε → → ∅ →
( , , (..., ))ib R P→ → ∅ .
Правило 1) определяет исполнение
базовых операторов. Правила 2) и 3) опи-
сывают ветвление и циклическую конст-
рукцию. Работа с функциями описана пра-
вилами 4) (вызов функции) и 5) (возврат из
функции).
Финальные состояния (из которых
невозможен переход ни в какое другое со-
стояние) имеют вид ( , , )fs b ε= ∅ .
Определенную таким образом ДДС
будем обозначать serS . Она моделирует
исполнение заданной последовательной
программы. Отметим, что система serS –
детерминированная, поскольку для
каждого состояния переход определен
однозначно.
1.4. Модель исполнения многопо-
точной программы. Основываясь на опи-
санной в предыдущем пункте модели ис-
полнения последовательной программы
serS , построим аналогичную модель для
параллельной многопоточной программы.
Будем строить модель путем рас-
ширения уже построенной модели serS . В
частности, модель программы остается
прежней. Будем предполагать, что код всех
потоков объединен в одной программе, как
это реализовано во всех современных язы-
ках, поддерживающих многопоточность
(таких как C/C++, C#, Java).
Для моделирования поведения по-
токов потребуется добавление новых опе-
раторов: запуска потока, критической
секции, синхронизации. Оператор
_ ( , )i jthread Pc l Tal описывает запуск фун-
кции на новом потоке. Этот оператор ис-
пользует два параметра: iP – идентифика-
тор функции для запуска и jT – идентифи-
катор потока, на котором будет запущена
Моделі та засоби паралельних і розподілених програм
42
функция. Операторы критической секции
( )ilock cs и ( )iunlock cs позволяют опреде-
лять участки кода, которые могут испол-
няться только на одном потоке. Операторы
синхронизации ( )iwait ev , ( )isignal ev и
( )ireset ev используются для взаимодейст-
вия потоков.
Модель исполнения, как и в после-
довательном случае, строится в виде ДДС.
В качестве состояний модели используют-
ся частичные отображения { }i is T s= →
множества T всех потоков на состояния
отдельных потоков. Множество всех пото-
ков T содержит специальный стартовый
поток 0T , а также все потоки jT , упоми-
наемые в операторах _ ( , )i jthread Pc l Tal .
Состояния отдельных потоков
( , , ) ser
i i is b R F S= ∈ аналогичны использо-
ванным в последовательной модели, т.е.
содержат состояние памяти b , состояние
управления iR и стек вызовов iF . Отме-
тим, что в модели с общей памятью со-
стояние памяти b является общим для
всех потоков. Это значит, что состояние
многопоточной программы можно было
бы более компактно переписать в виде па-
ры ' ( ,{ ( , )})i i is b T R F= → , т.е. вынести
общее состояние памяти из состояний от-
дельных потоков. Однако далее будем ис-
пользовать более длинную запись с дубли-
рованием b , чтобы подчеркнуть аналогию
с последовательной моделью (и облегчить
задание отношения переходов).
Начальное состояние имеет вид
0 0 0 0 0{ } { ( , ( ), ( ))}.ser
m ms T s T b Y P P= → = → → ∅
Исполняется только один поток, и его со-
стояние аналогично начальному состоя-
нию последовательной программы. Все
остальные потоки явно задаются в про-
грамме. Такая модель используется в
большинстве платформ для многопоточно-
го программирования.
Отношение переходов использует
уже определенное отношение serd для по-
следовательной программы. К правилам
1)–5), определенным в п. 1.3, добавим пра-
вила для новых операторов:
6) _ (, ,)( , )i jthreadb call RP FT →
( ,( , , ) ( ); ( ), )j i iT b Yb R F P P→ → ∅→ ;
7) { ( , ( ) , )}iT b lock cs R F→ →
{ ( { }, , )}i iT b cs T R F→ → ∪ → при
условии ( )b cs = ∅ или ( ) ib cs T= ;
8) { ( { }, ( ) , )}i iT b cs T unlock cs R F→ ∪ → →
{ ( { }, , )}iT b cs R F→ → ∪ → ∅ ;
9) ( , ( ) , ) ( , , )b wait ev R F b R F→ при
условии ( ) 1b ev = ;
10) ( , ( ) , )b signal ev R F →
( { 1}, , )b ev R F→ ∪ → ;
11) ( , ( ) , )b reset ev R F→
( { 0}, , )b ev R F→ ∪ → .
Правило 6) определяет создание но-
вого потока при срабатывании оператора
_ ( , )i jthread Pc l Tal . Правила 7), 8) описы-
вают поведение операторов критической
секции, а правила 9)–11) – поведение опе-
раторов синхронизации.
Отношение переходов для всей
многопоточной программы объединяет пе-
реходы отдельных потоков. Эта процедура
производится следующим образом: выби-
рается некоторое подмножество активных
потоков, для каждого из выбранных пото-
ков производится переход в соответствии с
отношением serd + , и новое состояние про-
граммы получается объединением состоя-
ний отдельных потоков. Новые состояния
отдельных потоков используют состояние
управление, определенное отношением
переходов для serS . Для определения со-
стояния общей памяти используется функ-
ция *:merge B B B× → . Эта функция меня-
ет состояние каждой переменной, которая
была изменена хотя бы в одном из пото-
ков. Формально,
0 1( , ,..., ) {k imerge b b b v= →
0
0
!{ ( ) | ( ) ( ), 1, }
}
( )
j i j i i
i
b v b v b v j k
b v
≠ =→
Моделі та засоби паралельних і розподілених програм
43
(здесь использовано обозначение ! A для
произвольного элемента множества A ).
Построенное отношение переходов
осталось дополнить еще одним правилом,
описывающим завершение работы потока.
12) 1 1 1 1{ ,..., , ( , , ),k k kT s T s T bε− −→ → → ∅
1 1,..., }k k n nT s T s+ +→ → →
1 1 1 1{ ,..., ,k kT s T s− −→ → →
1 1,..., }k k n nT s T s+ +→ → .
Таким образом, поток, который
достиг финального состояния в смысле
ДДС для последовательной программы,
завершает работу и исключается из списка
активных потоков.
Финальные состояния для многопо-
точной системы в целом могут быть двух
видов. В случае успешного завершения
работы всех потоков ДДС переходит в со-
стояние ( ,{})fs b′ = . Будем называть такое
состояние финальным, и отождествлять
его с финальным состоянием последнего
потока ( , , )fs b ε= ∅ . Также возможна си-
туация, когда все еще исполняются один
или несколько потоков, но ни один из них
не может совершить переход (потому что в
каждом из потоков очередным оператором
является lock или wait , и в правилах 7)
или 9) не выполняется условие перехода).
Такие состояния будем называть тупико-
выми.
Построенную ДДС для моделиро-
вания многопоточных программ будем
обозначать mtS . В отличие от системы
serS , система mtS не является детермини-
рованной, поскольку при каждом переходе
возможно выполнение произвольных ак-
тивных потоков.
1.5. Свойства программ. Исполь-
зуя построенные модели, можно формаль-
но описать некоторые свойства программ.
При этом возможно автоматическое вы-
числение таких свойств.
В данной работе рассматривается
применение моделей для доказательства
корректности преобразований программ.
Корректность преобразования подразу-
мевает тот факт, что исходная и преобра-
зованная программы дают одинаковый ре-
зультат. Формально это условие можно
сформулировать следующим образом.
Пусть выделено подмножество RV V⊂ ре-
зультирующих переменных. Тогда две
программы 1P и 2P будем называть экви-
валентными по результату, если для оди-
наковых начальных данных 0b , программы
одновременно приходят или не приходят в
финальные состояния 1 1( , , )fs b ε= ∅ и
2 2( , , )fs b ε= ∅ , при этом финальные со-
стояния памяти совпадают по результи-
рующим переменным: 1 2
R RV Vb b= .
Эквивалентность по результату яв-
ляется наиболее общим свойством, но не-
посредственная проверка этого свойства
практически нереализуема: требуется рас-
смотрение всех возможных путей испол-
нения программы, в зависимости как от
входных данных, так и вариантов выпол-
нения различных потоков. Поэтому необ-
ходимо введение более частных свойств,
описывающих корректность преобразова-
ний, которые могут быть проверены на
практике.
Сначала определим некоторые
свойства операторов АГ. Для каждого опе-
ратора y Y∈ определены множества
( )R y V⊂ переменных, от которых зависит
результат применения оператора, и
( )W y V⊂ переменных, которые изменя-
ются в результате применения оператора.
Два оператора 1 2,y y Y∈ являются зависи-
мыми (по данным), если
1 2( ) ( )R y W y∩ ≠ ∅ , или 1 2( ) ( )W y R y∩ ≠ ∅ ,
или 1 2( ) ( )W y W y∩ ≠ ∅ . Два оператора
1 2,y y Y∈ являются перестановочными,
(или коммутативными) относительно
операции композиции, если 1 2 2 1y y y y= .
Очевидно, что независимые операторы бу-
дут перестановочными; обратное неверно
(например, две копии одного оператора
y Y∈ всегда перестановочны, но они зави-
симы, если ( )W y ≠ ∅ ).
Теперь определим следующие свой-
ства программ: беступиковость, бескон-
фликтность и эквивалентность по операто-
рам. Программу P будем называть бесту-
пиковой, если при ее исполнении не возни-
Моделі та засоби паралельних і розподілених програм
44
кают тупиковые состояния. Все последова-
тельные программы (в модели serS ), оче-
видно, являются беступиковыми.
В модели mtS будем называть кон-
фликтным переходом ситуацию, когда
среди операторов, выполняющихся одно-
временно на разных потоках, есть зависи-
мые. Программу P будем называть бес-
конфликтной, если при ее исполнении не
возникают конфликтные переходы. Для
бесконфликтных программ нет необходи-
мости использовать функцию merge; вме-
сто объединения результатов одновремен-
ного воздействия нескольких операторов
можно применить эти операторы последо-
вательно, в любом порядке.
Если известен порядок исполнения
программы (последовательность перехо-
дов ДДС), можно определить историю ис-
пользования базовых операторов. Для это-
го добавим к состоянию ДДС еще одну
компоненту, h Y∈ . В начальном состоя-
нии положим h ε= . Также модифицируем
правило перехода 1):
( , , , ) ( ( ), , , )b yR F h y b R F hy→ .
При одновременном срабатывании
нескольких правил 1) на разных потоках,
будем добавлять соответствующие опера-
торы в произвольном порядке. Оператор h
в финальном состоянии будем называть
историей использования операторов.
Две истории 1 2,h h будем считать
эквивалентными, если 2h можно получить
из 1h последовательными перестановками
пар операторов, которые являются комму-
тативными. Две программы 1P и 2P будем
называть эквивалентными по операторам,
если для одинаковых начальных данных 0b
они производят эквивалентные истории
использования операторов.
Необходимость введения свойств
беступиковости, бесконфликтности и эк-
вивалентности по операторам обосновыва-
ется следующим утверждением.
Лемма 1. Если две программы 1P и
2P – беступиковые, бесконфликтные, а
также эквивалентные по операторам, то
они являются эквивалентными по резуль-
тату.
Кроме того, как будет показано в
дальнейшем, проверка этих свойств для
многих задач практически реализуема.
1.6. Проверка условий. Свойства
эквивалентности по операторам, беступи-
ковости и бесконфликтности, определен-
ные в предыдущем пункте, в общем случае
являются сложными для проверки. Однако
для определенных частных случаев можно
указать условия, достаточные для обеспе-
чения этих свойств, и при этом легко про-
веряемые. Приведем некоторые такие ус-
ловия.
Условие эквивалентности по опера-
торам фактически означает, что в про-
грамме переставлены некоторые операто-
ры, причем эти операторы должны быть
коммутативными. Возможна перестановка
операторов в пределах последовательной
композиции, в этом случае требование
коммутативности будем обозначать как
условие CommuteThen. Более частым слу-
чаем, однако, является перестановка опе-
раторов в пределах цикла: в этом случае
отдельные итерации цикла исполняются в
другом порядке, возможно в нескольких
циклах. Для обеспечения эквивалентности
по операторам необходимо проверить как
коммутативность отдельных итераций (ус-
ловие CommuteWhile), так и тот факт, что
существует взаимно однозначное соответ-
ствие между итерациями в двух програм-
мах (условие SameIterations).
Заметим, что проверка условий
коммутативности является достаточно
сложной, поскольку требует анализа
свойств всех операторов (включая вызовы
функций), а также возможных вариантов
исполнения программы. Возможна ситуа-
ция, когда для конкретной предметной об-
ласти известны факты коммутативности
некоторых операторов. Также коммута-
тивность может быть установлена на осно-
вании независимости операторов. В разде-
ле 3 будут рассмотрены некоторые спосо-
бы проверки коммутативности с использо-
ванием системы переписывающих правил
TermWare.
Для свойства бесконфликтности
можно сформулировать следующее усло-
вие: любые два оператора, которые явля-
ются зависимыми, и которые могут вы-
Моделі та засоби паралельних і розподілених програм
45
полняться на различных потоках, должны
находиться внутри критической секции с
одинаковым идентификатором (будем обо-
значать это условие AllNeededCS). Непо-
средственная проверка этого условия тре-
бует полного анализа зависимостей, что
является сложной задачей [10]. Однако в
некоторых частных случаях проверка уп-
рощается: например, независимыми будут
операторы, которые меняют только ло-
кальные переменные для потока.
Для свойства беступиковости нач-
нем со случая, когда в программе не ис-
пользуются операторы wait (т.е. потенци-
альные тупики могут возникнуть только
из-за операторов lock ). В этом случае
можно построить следующий ориентиро-
ванный граф критических секций. В каче-
стве вершин используются все используе-
мые в программе критические секции ics ;
дуга из ics в jcs добавляется в том случае,
если некоторый поток kT может выполнить
оператор ( )jlock cs , при этом ( )i kb cs T= ,
т.е. тот же поток уже занял ics . В этом
случае программа будет беступиковой, ес-
ли полученный граф будет ациклическим
(условие NoCyclesCS).
Частным случаем этого условия яв-
ляется ситуация, когда программа вообще
не содержит вложенных критических сек-
ций (условие NoNestedCS). В этом случае
граф критических секций не будет содер-
жать ребер, и автоматически будет ацик-
лическим. Данное условие достаточно
простое для проверки. Кроме того, если
программа ему удовлетворяет, можно
ожидать, что ее синхронизационные кон-
струкции проще для понимания разработ-
чиками.
В случае, когда в программе ис-
пользуются операторы wait , проверка бес-
тупиковости усложняется. В этом случае
для каждого оператора ( )iwait ev должен
найтись соответствующий оператор
( )isignal ev , при этом ( )iwait ev должен
сработать до очередного вызова ( )ireset ev .
Проверка такого условия для всех возмож-
ных вариантов исполнения программы
достаточно сложна.
Поэтому вместо общих условий от-
сутствия тупиков при использовании опе-
раторов wait , в данной работе рассматри-
ваются определенные шаблоны (паттерны)
их использования, которые гарантируют
корректность. Паттерны – это комбиниро-
ванные операторы, содержащие базовый
оператор wait , и которые являются един-
ственным способом его использования.
Рассмотрим два паттерна использо-
вания оператора wait . Первый, _ ( )iJoin T ,
определяет ожидание окончания работы
потока iT . Данный паттерн состоит из двух
частей. После последнего оператора, ис-
полняемого на потоке iT , вставляется опе-
ратор ( _ )isignal e Tv . Кроме того, исполь-
зуется комбинированный оператор (в дан-
ном случае эквивалентный базовому)
_ ( ) ( _ )i iJoin T w t evai T= . Кроме этих двух
операторов, точка синхронизации _ iev T
больше нигде не используется.
Второй паттерн, _ ( )iBarrier ts , оп-
ределяет в программе барьер, на котором
каждый поток ждет все остальные потоки.
Паттерн состоит из одного комбинирован-
ного оператора:
_ ( ) ( _ ); ( _ );
( _ , ( _ ); ( _ ),
( _ ,0); ( _ );
i i i
i i i
i i
Barrier bar lock cs b inc count b
if count b k unlock cs b wait ev b
assign count b signal ev b
=
<
( _ ))iunlock cs b .
Этот оператор использует дополни-
тельную переменную _ icount b, критиче-
скую секцию _ ics b и точку синхрониза-
ции _ iev b . В переменной _ icount b накап-
ливается количество потоков, которые
ожидают на барьере. Если это количество
меньше общего количества потоков, теку-
щий поток также ожидает; иначе все пото-
ки прекращают ожидание, и количество
потоков устанавливается равным 0.
Барьер не будет вызывать тупиков,
если общее количество потоков, где он ис-
пользуется, равно параметру k , а также в
каждом потоке срабатывает одинаковое
количество операторов _Barrier (условие
CorrectBarrier). Паттерн _ ( )iJoin T не бу-
дет вызывать тупиков, если беступиковой
Моделі та засоби паралельних і розподілених програм
46
является программа, полученная удалени-
ем оператора _ ( )iJoin T и всех последую-
щих операторов, исполняющихся на том
же потоке (условие CorrectJoin ).
Отметим, что во многих платфор-
мах многопоточного программирования
присутствует непосредственная реализа-
ция операторов _ Join и _Barrier , поэто-
му нет необходимости в реализации этих
паттернов с использованием операторов
wait и signal. Однако рассмотренные ус-
ловия остаются справедливыми и в этом
случае.
1.7. Пример доказательства кор-
ректности преобразования. Рассмотрим
пример использования построенной моде-
ли для доказательства корректности распа-
раллеливающего преобразования. Пусть
исходная последовательная программа
имеет следующий вид:
Ser=for(i,0,m,
for(j,0,n,
body(i,j))).
Здесь использован оператор цикла
со счетчиком for(var,min,max,body), кото-
рый выражается через общий оператор
цикла while. Рассмотрим два случая распа-
раллеливания. Первый случай реализуется,
когда итерации внешнего цикла являются
коммутативными. В этом случае возможно
распараллеливание на уровне этого цикла.
Рассмотрим следующее преобразование:
данный участок программы переходит в
параллельный эквивалент
Par1=for(k,0,threads,
call_thread(pbody1,Tk));
for(k,0,threads,
_Join(Tk)).
При этом вычисления переносятся в
функцию pbody1:
pbody1 =for(i,min(k),max(k),
for(j,0,n,
_AddLocks(body(i,j)))).
Эта функция повторяет структуру
исходного цикла, однако границы внешне-
го цикла зависят от номера потока и опре-
деляют ту часть итераций, которые выпол-
няются на данном потоке: min(k)=k*bs,
max(k)=min(m,(k+1)*bs), bs=m/threads.
Также в тело внутреннего цикла до-
бавляются необходимые критические сек-
ции (операция _AddLocks). Эта операция
заключает все зависимые операторы в кри-
тические секции, обеспечивая выполнение
условия AllNeededCS.
Теперь можно доказать следующее
утверждение.
Теорема 1. Программы Ser и Par1
эквивалентны по результату, если итера-
ции внешнего цикла в Ser коммутативны.
Доказательство. В силу леммы 1
достаточно проверить беступиковость и
бесконфликтность программы Par1 (для
последовательной программы эти свойст-
ва, очевидно, выполнены) и эквивалент-
ность по операторам программ Ser и Par1.
Беступиковость обеспечивается
свойством CorrectJoin: при удалении опе-
раторов _Join остается программа, не со-
держащая wait . К этой программе приме-
нимо условие NoNestedCS, поскольку опе-
рация _AddLocks исключает добавление
вложенных критических секций. Беступи-
ковость доказана.
Бесконфликтность следует из вы-
полнения условия AllNeededCS, которое
также обеспечивается операцией
_AddLocks.
Для доказательства эквивалентно-
сти по операторам необходимо проверить
условия CommuteWhile и SameIterations.
Первое из них выполнено по условию;
второе следует из построения циклов в
программе Par1. Действительно, можно
установить взаимно однозначное соответ-
ствие между итерацией с номером i в про-
грамме Ser и итерацией с номером (i mod
bs) в потоке i/bs программы Par1.
Таким образом, все условия выпол-
нены и теорема доказана.
Во втором случае распараллелива-
ния итерации внешнего цикла не являются
коммутативными, но этим свойством об-
ладают итерации внутреннего цикла. В
этом случае можно было бы применить
аналогичное преобразование к внутренне-
му циклу, однако в этом случае во внеш-
нем цикле происходило бы многократное
Моделі та засоби паралельних і розподілених програм
47
создание потоков, что привело бы к значи-
тельным накладными расходам. Поэтому
используем преобразование, которое соз-
дает потоки только один раз, но при этом
гарантирует правильный порядок выпол-
нения итераций внешнего цикла.
Для этого преобразования исполь-
зуется следующая функция, исполняемая
на потоках:
pbody2 =for(i,0,m,
for(j, min(k),max(k),
_AddLocks(body(i,j)));
_Barrier(bar)).
При этом распараллеливается внут-
ренний цикл и используется оператор
_ Barrier для обеспечения последователь-
ного исполнения итераций внешнего
цикла.
Для этого преобразования можно
сформулировать аналогичное утверждение
о корректности:
Теорема 2. Программы Ser и Par2
эквивалентны по результату, если
итерации внутреннего цикла в Ser комму-
тативны.
Доказательство. Аналогично тео-
реме 1. Дополнительно необходимо прове-
рить условие CorrectBarrier. Это условие
выполнено: операторы _Barrier исполня-
ются во всех потоках, при этом в каждом
потоке количество операторов одинаково и
равно m.
Таким образом, построенная модель
позволяет доказывать корректность преоб-
разований программ. Преобразования оп-
ределенного вида будут корректными, ес-
ли выполнены определенные условия, на-
кладываемые на программу. В разделе 3
будут рассмотрены некоторые способы
проверки таких условий.
2. Модель программ для гра-
фических ускорителей
2.1. Модель программы. В преды-
дущем разделе построена алгебро-
динамическая модель исполнения много-
поточной программы. В данном разделе
построим аналогичную модель для другой
программно-аппаратной платформы, а
именно для программ, которые исполня-
ются на графических ускорителях.
Программирование графических
ускорителей для решения задач, не связан-
ных непосредственно с обработкой графи-
ки, активно развивается в настоящее вре-
мя. Однако на данный момент не сущест-
вует единой общепризнанной платформы
для таких вычислений. Кроме того, раз-
личные платформы существенно отлича-
ются по используемым подходам и пара-
дигмам организации вычислений. Поэто-
му, в отличие от многопоточных про-
грамм, необходимо выбрать конкретную
платформу, для которой и будет построена
модель вычислений. Как и в работе [5], бу-
дем использовать платформу CUDA кор-
порации NVidia [17].
Особенностью программ для гра-
фических ускорителей является их разде-
ление на две части: код, который исполня-
ется на общецелевом процессоре (CPU) и
специализированный код для графическо-
го ускорителя (GPU). Эти части могут
быть реализованы на разных языках. На-
пример, в [5] рассматривались программы,
в которых CPU-код был реализован на C#,
тогда как GPU-код – на C for CUDA, спе-
циальном расширении языка С.
В модели программы эту особен-
ность будем учитывать следующим обра-
зом. По-прежнему будем рассматривать
программу как набор компонент; однако
теперь каждая компонента относится либо
к CPU-, либо к GPU-коду. При этом для
CPU и GPU наборы базовых операторов
могут различаться.
2.2. CPU-программа. При построе-
нии модели исполнения программ для
графических ускорителей будем отдельно
рассматривать исполнение на CPU и на
GPU. Для каждого режима построим соот-
ветствующую модель в виде ДДС. Модель
исполнения программы в целом, gcS ,
строится как объединение этих двух ДДС.
Код, относящийся к CPU, исполня-
ется так же, как и любая обычная про-
грамма. Поэтому для моделирования этой
части можно использовать одну из ранее
разработанных моделей serS или mtS . В
данной работе будем использовать модель
Моделі та засоби паралельних і розподілених програм
48
serS . Это значит, что CPU-часть програм-
мы выполняется последовательно, и не ис-
пользует средства многопоточности.
В модель serS потребуется добавить
средства взаимодействия с GPU. В данной
модели рассмотрим три новых оператора:
( )_ ,G Cgpucopy m m – копирование данных
в видеопамять, ( , )_ C Gcopy ack m mb – ко-
пирование результатов из видеопамяти, и
( , , )_ icall P bgp lock gridu – запуск кода (яд-
ра CUDA) на GPU. Соответственно потре-
буется добавить правила переходов, кото-
рые будут менять состояние ДДС gcS в
целом, а не только один из ее компонен-
тов. Формальное описание этих правил
приведено в п. 2.5, после рассмотрения
GPU-компонента.
2.3. GPU-программа: уровень
блоков. Модель gpuS исполнения кода на
GPU строится по тому же общему принци-
пу, что и многопоточная модель mtS .
Строится многоуровневая ДДС, на низшем
уровне которой моделируется исполнение
отдельных потоков. Для каждого потока
используется модифицированная ДДС
serS , и переходы ДДС отдельных потоков
объединяются в переход ДДС более высо-
кого уровня, например, с использованием
функции merge.
Первым важным отличием модели
для графических ускорителей от многопо-
точной модели mtS заключается в большей
сложности, которая требует использования
большего количества уровней. Модель mtS
содержит два уровня: отдельные потоки и
программу в целом. Модель gpuS содержит
один дополнительный уровень, а именно
уровень блоков. Отдельные потоки (пер-
вый уровень) объединяются в блоки (вто-
рой уровень), которые в свою очередь
формируют GPU-программу в целом (тре-
тий уровень).
Вторым отличием является наличие
иерархии памяти. В CUDA используется 5
видов памяти: регистры, разделяемая
(shared) память, кэш констант, кэш текстур
и глобальная память. В рамках модели ог-
раничимся рассмотрением двух наиболее
часто используемых видов памяти, а имен-
но shared память и глобальная память.
Различные виды памяти в модели
проявляются в виде дополнительных ком-
понентов состояния. Для низшего уровня
(потоков) состояние имеет вид
( , , , )g ss b b R F= , где ggb B∈ – состояние
глобальной памяти, ssb B∈ – состояние
shared памяти. Однако для упрощения мо-
дели будем объединять состояния различ-
ных видов памяти в общее состояние
g sb b b= ∪ , g sB Bb B∈ = × . Будем считать,
что все операторы и предикаты АГ также
действуют на объединенном множестве B .
На уровне потоков действуют пра-
вила перехода 1) – 5) (правило 4) имеет
дополнительное ограничение – вызывае-
мая функция должна работать на GPU, что
описывается модификатором __device__ в
C for CUDA).
На уровне блоков, аналогично сис-
теме mtS , состоянием является множество
потоков, каждый со своим состоянием
2 1{ }i is T s= → . В отличие от mtS , количест-
во потоков всегда одинаково и определя-
ется параметрами блока. Поэтому нет не-
обходимости в правиле 12) (завершение
потока).
Переходы на уровне блоков объе-
диняются из переходов на уровне потоков,
как и в mtS . Функция merge применяется к
обоим видам памяти ,g sb b (или к объеди-
ненной памяти b ). Отличие от многопо-
точной модели заключается в дополни-
тельном ограничении на переходы: все од-
новременно срабатывающие потоки долж-
ны исполнять одинаковые операторы (по-
скольку в архитектуре GPU на каждый
блок выделяется только одно управляющее
устройство).
Средства работы с потоками, со-
держащиеся в mtS , в случае GPU неприме-
нимы. Вместо них используется единст-
венный оператор _Barrier, поведение ко-
торого аналогично соответствующему пат-
терну для многопоточной модели. В C for
CUDA этот оператор реализован примити-
вом __syncthreads().
2.4. GPU-программа: уровень
программы. Уровень программы в целом
строится из уровня блоков таким же обра-
Моделі та засоби паралельних і розподілених програм
49
зом, как уровень блоков строился из уров-
ня потоков.
Состояниями программы являются
отображения из множества блоков в мно-
жество состояний уровня блоков:
3 2{ }j js B s= → . Как и на втором уровне,
количество блоков постоянно и определя-
ется параметрами запуска ядра.
В отличие от уровня блоков, shared
память является уникальной для каждого
блока, а не общей, как глобальная память
(или общая память в модели mtS ). Поэтому
объединение результатов функцией merge
на данном уровне используется только для
глобальной памяти gb .
Еще одной особенностью объеди-
ненных переходов на уровне всей про-
граммы является следующее ограничение:
не может начаться исполнение нового бло-
ка (который находится в начальном со-
стоянии уровня блоков), если существует
хотя бы один блок, который уже начал ис-
полняться, но не задействован в данном
переходе. Иными словами, не происходит
переключение между разными одновре-
менно исполняемыми блоками; каждый
блок, начавший исполняться, исполняется
до конца.
На уровне программы существуют
свои средства синхронизации (например,
атомарные операции). Однако они доступ-
ны не во всех устройствах, сильно замед-
ляют исполнение программы, к тому же
противоречат идеологии CUDA, согласно
которой блоки должны исполняться неза-
висимо и в произвольном порядке. Поэто-
му не будем включать эти средства в мо-
дель.
2.5. Взаимодействие CPU и GPU.
Совместная работа двух частей программы
координируется из CPU-кода, с использо-
ванием операторов copy_gpu, copy_back и
call_gpu . Первые два оператора копируют
данные между памятью, доступной CPU, и
глобальной памятью GPU. Формально это
сводится к тому, что некоторое множество
переменных (обычно массив) в состоянии
одного устройства принимают те же зна-
чения, что соответствующие переменные в
состоянии другого.
Оператор call_gpu собственно за-
пускает код для исполнения на графиче-
ском ускорителе. Его работа описывается
двумя правилами:
13) 0( , ( , )) ( , ( , , ))c c g
g is b s s P block grid∅ → ;
14) ( , ) (( , , ), ( , ))c g
f gs s b R F b′→ ∅
( , ( , )_ , , )c
is b call P blockgpu grid R F= .
Правило 13) описывает создание
начального состояния ДДС gpuS при ис-
полнении оператора call_gpu. Параметры
этого состояния – количество блоков, по-
токов, исполняемый модуль – извлекается
из параметров оператора. Отметим, что
оператор не удаляется из состояния управ-
ления: с точки зрения CPU, этот оператор
выполняется все время, пока идут вычис-
ления на GPU. Правило 14) срабатывает,
когда вычисления на GPU окончены. Оно
очищает состояние управления GPU, и за-
вершает выполнение оператора call_gpu.
Состояние памяти CPU в процессе вычис-
лений на GPU не меняется: требуется яв-
ное копирование результатов вычислений
оператором copy_back.
2.6. Свойства GPU-программ. К
программам для графических ускорителей
применимы те же свойства, что и для мно-
гопоточных программ. Однако некоторые
из этих свойств имеют определенные осо-
бенности для GPU-программ.
Свойство эквивалентности по опе-
раторам требует уточнения, поскольку в
CPU- и GPU-программах используются
различные наборы базовых операторов,
которые действуют на различных множе-
ствах переменных. Поэтому для определе-
ния эквивалентности будем отождествлять
те переменные из памяти CPU и глобаль-
ной памяти GPU, между которыми произ-
водилось копирование с помощью опера-
торов copy_gpu или copy_back. Также бу-
дем отождествлять одинаковые по смыслу
операторы, которые действуют на этих
множествах.
Определение бесконфликтности ос-
тается прежним. Особенность GPU-
программ заключается в отсутствии эф-
фективных средств обеспечения бескон-
фликтности, поэтому это свойство должно
быть обеспечено в самой программе.
Моделі та засоби паралельних і розподілених програм
50
Из-за ограниченного набора средств
синхронизации, для проверки беступико-
вости GPU-программ применимо единст-
венное условие CorrectBarrier. При этом
оно упрощается, поскольку используется
всегда правильное количество потоков.
Таким образом, это условие сводится к то-
му, что в каждом потоке оператор _Barrier
используется одинаковое количество раз.
2.7. Преобразования GPU-
программ. В качестве примера использо-
вания построенной модели для графиче-
ских ускорителей, рассмотрим преобразо-
вания той же последовательной програм-
мы, которая рассматривалась в п. 1.7. По-
строим преобразования последовательной
программы в программу для GPU, для
обоих случаев (когда возможно распарал-
леливание внешнего и внутреннего цикла).
В первом случае, преобразованная
программа имеет следующий вид:
Gpu1=copy_gpu;
call_gpu(gbody1,block2d,grid2d);
copy_back.
Производится копирование необхо-
димых данных в видеопамять, затем вызов
ядра gbody1, затем копирование результа-
тов. Ядро запускается в двумерном режи-
ме, измерения которого соответствуют
двум исходным циклам. Ядро gbody1 име-
ет вид
gbody1 =assign(i,_GetCoor(x));
assign(j,_GetCoor(y));
_CpuToGpu(body(i,j)).
Сначала вычисляются номера ис-
ходных итераций i и j, для этого исполь-
зуются параметры текущего потока. После
этого исполняется тело внутреннего цикла
для этих значений. При этом используется
функция _CpuToGpu для преобразования
между операторами CPU- и GPU-
программ. Отметим, что в данном случае
выделяется по одному потоку на каждую
итерацию, в отличие от многопоточной
программы, где использовалось ограни-
ченное количество потоков, на каждом из
которых выполнялось большое количество
итераций цикла.
Для второго случая, т.е. распарал-
леливание внутреннего цикла, программа
имеет следующий вид:
Gpu2=copy_gpu;
for(i,0,m,
call_gpu(gbody2,block1d,grid1d));
copy_back.
Здесь вызов ядра gbody2 происхо-
дит в цикле. При этом копирование дан-
ных между обычной памятью и видеопа-
мятью происходит только один раз. Ядро
gbody2 соответствует только внутреннему
циклу:
gbody2 = assign(j,_GetCoor(x));
_CpuToGpu(body(i,j)).
В данном случае нельзя было ис-
пользовать тот же метод, что в многопо-
точной программе (однократный вызов яд-
ра и синхронизация между итерациями
внешнего цикла). Это объясняется невоз-
можностью синхронизации потоков, при-
надлежащих к разным блокам.
Для GPU-программ также можно
сформулировать утверждения о коррект-
ности преобразований.
Теорема 3. Программы Ser и Gpu1
эквивалентны по результату, если итера-
ции внешнего цикла в Ser независимы.
Теорема 4. Программы Ser и Gpu2
эквивалентны по результату, если итера-
ции внутреннего цикла в Ser независимы.
Доказательство проводится анало-
гично теореме 1. Заметим, что в случае
GPU необходимо потребовать более силь-
ное ограничение, а именно независимость
итераций цикла. Это ограничение позволит
обеспечить бесконфликтность даже при
отсутствии критических секций или анало-
гичных средств.
3. Использование переписы-
вающих правил
3.1. Система Termware. Описан-
ные в разделах 1 и 2 модели предоставля-
ют теоретические средства для проверки
корректности преобразований программ.
Однако для их эффективного использова-
ния необходимы также программные сред-
Моделі та засоби паралельних і розподілених програм
51
ства автоматизации. В частности, уже
упоминалась сложность проверки условий,
которые определяют корректность преоб-
разований. В данной работе для автомати-
зации проверки условий используется сис-
тема переписывающих правил Termware,
которая также используется для автомати-
зации самих преобразований [3–5].
Termware предназначена для описа-
ния преобразования над термами, т.е. вы-
ражениями вида f(t1, …, tn). Для задания
преобразований используются правила
Termware, т.е. конструкции вида source
[condition] -> destination [action].
Здесь source – исходный терм
(образец для поиска), condition – усло-
вие применения правила, destination –
преобразованный терм, action – допол-
нительное действие при срабатывании
правила. Каждый из 4 компонентов прави-
ла может содержать переменные (которые
записываются в виде $var), что обеспечи-
вает общность правил. Компоненты con-
dition и action являются необязатель-
ными. Они могут исполнять произвольный
процедурный код, в частности использо-
вать дополнительные данные о программе.
3.2. Переход между представле-
ниями программы. Одним из средств,
предоставляемых системой Termware, яв-
ляется переход от исходного кода про-
граммы, например, на языке C#, к пред-
ставлению программы в виде терма (соот-
ветствующему дереву синтаксического
разбора). Такое представление, по сути,
является моделью программы, хотя и низ-
коуровневой (поскольку каждая синтакси-
ческая конструкция языка программирова-
ния явно представлена в модели). Подоб-
ные модели использовались для описания
преобразований программ в [5].
Однако в данной работе, как и в [3–
4], используется более высокоуровневое
представление программы, в виде опера-
торов алгебры Глушкова. Такое представ-
ление является более компактным, к тому
же оно удобнее для теоретического анали-
за. С другой стороны, оно требует специ-
альных средств для получения модели и
преобразования ее в код программы. Та-
ким средством может быть, например, ин-
струментарий ИПС [3].
В данной работе рассмотрим другой
способ преобразования, с использованием
средств Termware. Для некоторой пред-
метной области можно сформулировать
список операторов и предикатов АГ, и со-
ответствие между ними и реализующим их
кодом. Это соответствие можно сформу-
лировать таким образом, что появится
возможность использовать переписываю-
щие правила Termware для автоматическо-
го перехода между двумя уровнями пред-
ставления программы.
Для этого будем использовать пат-
терны Termware. В общем случае, паттерн
определяется двумя системами правил: pR
– система правил для выделения паттерна
из произвольного терма, gR – система
правил для расшифровки паттерна. В бо-
лее частном случае паттерн задается парой
термов pt – обозначение паттерна (эле-
мент модели высокого уровня) и gt – обра-
зец, задающий паттерн (элемент модели
низкого уровня). В этом случае
{ }p g pR t t= → и { }g p gR t t= → .
Примером такого задания паттернов
могут быть _Join и _Barrier, определенные
в п. 1.6. В этом случае в качестве pt вы-
ступают сами операторы _Join или
_Barrier, а в качестве gt – их реализация в
виде комбинированного оператора.
Если для некоторой предметной об-
ласти заданы операторы и предикаты вы-
сокоуровневой модели в виде паттернов из
операторов низкоуровневой модели, ста-
новится возможна разработка программы
на любом из уровней: высокоуровневая
модель (алгебра алгоритмов), низкоуров-
невая модель (дерево синтаксического раз-
бора), исходный код. Например, для уже
существующего приложения можно при-
менить парсер Termware для перехода к
дереву синтаксического разбора. После
этого используются паттерны и соответст-
вующие правила pR для перехода к алгеб-
ро-алгоритмическому представлению. В
этом представлении возможно осуществ-
ление некоторых преобразований, в т.ч.
проверка корректности с использованием
описанных в разделах 1 и 2 моделей.
Моделі та засоби паралельних і розподілених програм
52
Далее используются правила gR
для перехода от высокоуровневой к низко-
уровневой модели, и затем генератор
Termware для воссоздания исходного кода.
При этом возможно использование допол-
нительных преобразований на уровне де-
рева синтаксического разбора, а также не-
посредственное внесение изменений в ис-
ходный код, для тех случаев, когда не реа-
лизованы соответствующие преобразова-
ния. Это позволяет повысить удобство
разработки, поскольку для реализации ка-
ждого преобразования можно использо-
вать наиболее подходящие средства.
3.3. Проверка условий по модели
программы. В п. 1.6 приведены примеры
условий, которые используются при дока-
зательстве корректности преобразований.
Для проверки некоторых из этих условий
можно использовать переписывающие
правила. В этом случае Termware исполь-
зуется не для преобразования одной про-
граммы (модели программы) в другую, а
для вычисления некоторых свойств про-
граммы.
В качестве примера рассмотрим
систему правил для проверки условия
NoNestedCS:
1. Method($head,$body) -> Method
($head,[m0:$body],_Mark).
2. [m0:lock($cs):$x] -> [ lock($cs):
m1($cs):$x].
3. [m1($cs):unlock($cs):$x] ->
-> [unlock($cs): m0:$x].
4. [m1($cs):lock($cs1):$x] ->
->NIL [error()].
5. [m0:$x:$y] -> [$x: m0:$y].
6. [m1($cs):$x:$y] ->
-> [$x: m1($cs):$y].
Здесь правило 1 добавляет в начало
тела каждого метода специальный терм-
маркер m0, который используется для об-
хода всех операторов метода. Правило 2
запоминает идентификатор критической
секции, заменяя маркер m0 на m1. Правило
3 соответствует правильному варианту ис-
пользования, когда внутри критической
секции нет других критических секций.
Правило 4 срабатывает при невыполнении
условия NoNestedCS; в этом случае систе-
ма правил сообщает об ошибке. Правила 5
и 6 носят служебный характер и обеспечи-
вают продвижение маркеров m0 и m1 по
операторам.
Следует отметить, что невыполне-
ние условия NoNestedCS еще не свидетель-
ствует об ошибке: в этом случае необхо-
димо проверять более общие условия, на-
пример, NoCyclesCS.
3.4. Проверка условий с помощью
тестов. Для многих условий их проверка
по модели программы является очень
сложной. Примером может служить Com-
muteWhile – условие, позволяющее выпол-
нять итерации цикла в произвольном по-
рядке, что необходимо для распараллели-
вания.
Для проверки этого условия, вместо
статического анализа кода программы (или
соответствующей модели), можно исполь-
зовать результаты исполнения кода. При
этом генерируются специальные тестовые
программы, которые запускают необходи-
мый код, получают результаты его испол-
нения и сравнивают эти результаты с ожи-
даемыми. Ожидаемые результаты можно
получить путем исполнения исходной про-
граммы (которая предполагается правиль-
ной).
В простейшем случае в качестве
тестов можно использовать преобразован-
ную программу (полностью или частично
– только те методы, которые были измене-
ны). При этом к программе необходимо
добавить проверку результатов, что реали-
зуется простыми правилами Termware.
Преимуществом такого подхода яв-
ляется то, что проверяется исполнение
именно той программы, которая является
результатом преобразования. Недостаток
может заключаться в том, что некоторые
ошибки в параллельных программах могут
проявляться только при специальных ус-
ловиях. Поэтому вполне возможно, что
при исполнении тестов результаты совпа-
дут с ожидаемыми, тогда как при реальном
использовании программы будут возни-
кать ошибки.
Чтобы уменьшить вероятность по-
добной ситуации, можно использовать до-
Моделі та засоби паралельних і розподілених програм
53
полнительные тесты, которые используют
специальным образом преобразованный
код. Например, для проверки условия
CommuteWhile можно сгенерировать по-
следовательную программу, содержащую
тот же цикл, но с обращенным порядком
итераций. Если в исходной программе ите-
рации были перестановочны, то такая мо-
дифицированная программа должна давать
тот же результат. В противном случае ре-
зультат может как отличаться, так и совпа-
дать (если при конкретном способе пере-
становки операторов случайно получается
такой же результат). Можно использовать
и более сложные перестановки, например,
развернуть цикл на 2 итерации и переме-
шать операторы из этих итераций.
Особенность тестов такого вида за-
ключается в том, что если тест не прохо-
дит, это свидетельствует о невыполнении
условия. Если же тест проходит, это не
может гарантировать выполнение свойст-
ва. Поэтому необходимо использовать не-
сколько различных тестов. Преимущество
Termware заключается в том, что перепи-
сывающие правила позволяют автоматизи-
ровать создание большого количества тес-
тов для каждой конкретной программы.
3.5. Пример использования. Рас-
смотрим пример использования описанно-
го подхода на конкретной задаче – про-
грамме для реализации игры «Жизнь» [18].
Задача была изначально реализована в ви-
де последовательной программы на языке
C#. Далее к ней были применены преобра-
зования для перехода к параллельным реа-
лизациям: многопоточной и для графиче-
ского ускорителя.
Исходная последовательная про-
грамма соответствует общей схеме, рас-
смотренной в п. 1.7. Внешний цикл соот-
ветствует последовательному проведению
итераций игры, тогда как внутренний цикл
является обходом всех ячеек в пределах
одной итерации. В этом случае реализует-
ся второй из рассмотренных случаев: воз-
можно распараллеливание по внутреннему
циклу, тогда как итерации внешнего цикла
могут выполняться только последователь-
но. Для проверки данного условия были
сгенерированы тесты с использованием
перестановки итераций, которые были
описаны в п. 3.4.
Для случая многопоточной про-
граммы было применено преобразование
Par2, описанное в п. 1.7. Преобразование
применялось на уровне алгебро-
алгоритмического представления про-
граммы, поэтому использовались перепи-
сывающие правила для перехода между
низкоуровневым и высокоуровневым
представлением программы. После преоб-
разования программы в многопоточную к
ней были применены некоторые оптими-
зирующие преобразования, описанные в
работе [4] (в частности, использование ло-
кальных копий общих данных).
Была измерена производительность
преобразованных программ, для оценки
эффективности преобразований. Измеря-
лось время выполнения 500 итераций, для
поля 512x512. Результаты измерений при-
ведены в таблице.
Как видно из результатов, исходное
распараллеливание оказалось неэффектив-
ным, и полученная программа оказалась
даже менее производительной, чем после-
довательная версия. Это объясняется не-
эффективным использованием средств
синхронизации (более подробно данный
вопрос рассмотрен в [4]). Однако приме-
нение оптимизирующих преобразований
позволило достичь вполне заметного уско-
рения.
Таблица. Результаты измерений
Вариант Время исполнения, с
Последовательный 9,8
Многопоточный 27,8
Оптимизированный 3,4
Реализация преобразования той же
последовательной программы в программу
для графического ускорителя описана в
работе [19]. Распараллеливающие и опти-
мизирующие преобразования позволили
достичь ускорения в 25 раз. При этом ис-
пользование высокоуровневой модели по-
зволило достаточно кратко описать все ис-
пользованные преобразования, а также
скрыть от разработчика различие между
конкретными языками реализации после-
довательной программы (C#) и GPU-части
параллельной программы (C for CUDA).
Моделі та засоби паралельних і розподілених програм
54
Выводы
В работе предложен метод доказа-
тельства корректности распараллеливаю-
щих преобразований, основанный на при-
менении алгебро-динамических моделей и
системы переписывающих правил Term-
ware. Построены модели исполнения мно-
гопоточных программ и программ для
графических ускорителей. Для этих моде-
лей сформулированы свойства программ, и
предложен метод проверки этих свойств с
использованием переписывающих правил.
Предложенный метод позволяет автомати-
зировать проверку корректности для мно-
гих оптимизирующих преобразований.
Дальнейшие исследования в данном
направлении предполагают формулирова-
ние дополнительных условий, обеспечи-
вающих корректность преобразований, а
также реализацию переписывающих пра-
вил для проверки данных условий. Также
возможна интеграция с системами для ав-
томатического доказательства теорем, с
целью более полной автоматизации про-
цесса доказательства корректности.
1. Akhter S., Roberts J. Multi-Core Program-
ming. Increasing Performance through Soft-
ware Multi-threading. – Intel Press, 2006. –
336 p.
2. General-Purpose Computation Using Graph-
ics Hardware. http://www.gpgpu. org .
3. Дорошенко А.Е., Жереб К.А., Яценко Е.А.
Формализованное проектирование эффек-
тивных многопоточных программ // Про-
блеми програмування. – 2007. – № 1. –
С. 17–30.
4. Дорошенко А.Е., Жереб К.А., Яценко Е.А.
Об оценке сложности и координации вы-
числений в многопоточных программах //
Проблеми програмування. – 2007. – № 2. –
С. 41–55.
5. Дорошенко А.Е., Жереб К.А. Разработка
высокопараллельных приложений для гра-
фических ускорителей с использованием
переписывающих правил // Проблеми про-
грамування. – 2009. – № 3. – С. 3–18.
6. Doroshenko A., Shevchenko R. A Rewriting
Framework for Rule-Based Programming Dy-
namic Applications, Fundamenta Informati-
cae. – 2006. – Vol. 72, N 1–3. –P. 95–108.
7. TermWare. – http://www.gradsoft.com.ua/
products/termware_rus.html .
8. Дорошенко А.Е., Шевченко Р.С. Система
символьных вычислений для программи-
рования динамических приложений // Про-
блеми програмування. – 2005. – № 4. –
С. 718–727.
9. Андон Ф.И., Дорошенко А.Е., Цейтлин Г.Е.,
Яценко Е.А. Алгеброалгоритмические мо-
дели и методы параллельного программи-
рования. – Киев: Академпериодика, 2007. –
631 с.
10. Kundu S., Tatlock Z., and Lerner S. Proving
optimizations correct using parameterized
program equivalence. In Proceedings of the
2009 ACM SIGPLAN Conference on Pro-
gramming Language Design and Implementa-
tion (Dublin, Ireland, June 15–21, 2009).
PLDI '09. – P. 327–337.
11. Lerner S., Millstein T., and Chambers C.
Automatically proving the correctness of
compiler optimizations. In Proceedings of the
ACM SIGPLAN 2003 Conference on Pro-
gramming Language Design and Implementa-
tion (San Diego, California, USA, June 09–
11, 2003). PLDI '03. – P. 220–231.
12. Lerner S., Millstein T., Rice E., and Chambers
C. Automated soundness proofs for dataflow
analyses and transformations via local rules.
SIGPLAN Not. – 2005. – Vol. 40, N 1. –
P. 364–377.
13. Lacey D., Jones N. D., Van Wyk E., and
Frederiksen C. C. Proving correctness of
compiler optimizations by temporal logic. In
Proceedings of the 29th ACM SIGPLAN-
SIGACT Symposium on Principles of Pro-
gramming Languages (Portland, Oregon,
January 16–18, 2002). POPL '02. –
P. 283–294.
14. Leroy X. Formal certification of a compiler
back-end or programming a compiler with a
proof assistant. In Conference Record of the
33rd ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages
(Charleston, South Carolina, USA, January
11–13, 2006). POPL '06. – P. 42–54.
15. Farzan A., Chen F., Meseguer J., and Rosu
G. Formal Analysis of Java Programs in
JavaFAN. In Int. Conf. on Computer Aided
Verification, Boston, Mass., 2004.
16. Timothy Winkler, “Programming in OBJ and
Maude”, in Functional Programming, Concur-
rency, Simulation and Automated Reasoning,
International Lecture Series 1991–1992,
Springer-Verlag, McMaster University, Ham-
ilton, Ontario, Canada, 1993. – P. 229–277.
17. NVidia CUDA technology. http://www.
nvidia.com/cuda .
Моделі та засоби паралельних і розподілених програм
55
18. Conway’s Game of Life
http://en.wikipedia.org/wiki/Conway
%27s_Game_of_Life.
19. Дорошенко А.Е., Жереб К.А. Автоматиза-
ция разработки приложений для графиче-
ских ускорителей с использованием пере-
писывающих правил // Труды 5 Вос-
точно-европейской научно-практической
конференции по программной инженерии
CEE-SECR 2009. – Москва, 28–29 октября
2009.
Получено 17.12.2009
Об авторах:
Дорошенко Анатолий Ефимович,
доктор физико-математических наук,
профессор, заведующий отделом теории
компьютерных вычислений Института
программных систем НАН Украины,
Жереб Константин Анатольевич,
младший научный сотрудник.
Место работы авторов:
Институт программных систем
НАН Украины,
03680, Киев-187,
Проспект Академика Глушкова, 40.
Тел.: (044) 526 1538.
e-mail: dor@isofts.kiev.ua,
zhereb@gmail.com
|