Validation of correctness of autotuning code transformations with rewriting rules technique
Article presents an approach to correctness validation of autotuning optimizational transformations. Autotuner is considered as dynamic discrete system and validation is reduced to verification of characteristic of equivalence by result of representation of initial and optimized program versions in...
Saved in:
| Date: | 2020 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
PROBLEMS IN PROGRAMMING
2020
|
| Subjects: | |
| Online Access: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/429 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Problems in programming |
| Download file: |  |
Institution
Problems in programming| _version_ | 1859502061427621888 |
|---|---|
| author | Ivanenko, P.A. |
| author_facet | Ivanenko, P.A. |
| author_sort | Ivanenko, P.A. |
| baseUrl_str | https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| collection | OJS |
| datestamp_date | 2020-12-07T15:40:57Z |
| description | Article presents an approach to correctness validation of autotuning optimizational transformations. Autotuner is considered as dynamic discrete system and validation is reduced to verification of characteristic of equivalence by result of representation of initial and optimized program versions in autotuning formal model. In partial cases this validation can be done automatically using source code and rewriting rules technique.Problems in programming 2020; 2-3: 368-374 |
| first_indexed | 2025-07-17T09:40:27Z |
| format | Article |
| fulltext |
Методи машинного навчання
© П.А. Іваненко, 2020
368 ISSN 1727-4907. Проблеми програмування. 2020. № 2–3. Спеціальний випуск
УДК 004.4`2 https://doi.org/10.15407/pp2020.02-03.368
ПРО АНАЛІЗ КОРЕКТНОСТІ АВТОТЬЮНІНГУ ПРОГРАМ
З ВИКОРИСТАННЯМ ТЕХНІКИ ПЕРЕПИСУВАЛЬНИХ ПРАВИЛ
П.А. Іваненко
У роботі запропоновано підхід до перевірки коректності оптимізаційних перетворень паралельних програм, що виконуються
автотьюнером. Автотьюнер розглядається як еволюційна дискретна динамічна система й перевірка коректності зводиться до
перевірки властивості еквівалентності за результатом представлень вихідної і оптимізованої версій програм у формальній моделі
автотьюнінгу. Цю перевірку у часткових випадках можна виконати автоматично за вихідним кодом за допомогою техніки
переписувальних правил.
Ключові слова: автоматизація оптимізації паралельних програм, автотьюнінг , алгебро-динамічні моделі, техніка переписувальних
правил, перевірка коректності перетворень.
Article presents an approach to correctness validation of autotuning optimizational transformations. Autotuner is considered as dynamic
discrete system and validation is reduced to verification of characteristic of equivalence by result of representation of initial and optimized
program versions in autotuning formal model. In partial cases this validation can be done automatically using source code and rewriting rules
technique.
Key words: automation of parallel program optimization, autotuning, algebra-dynamic models, rewriting rules technique, validation of code
transformations correctness.
В работе представлен подход к проверке корректности оптимизационных преобразований параллельных программ, выполняемых
автотьюнером. Автотьюнер рассматривается как эволюционная дискретная динамическая система, а проверка корректности
сводится к проверке свойству эквивалентности по результату интерпретаций исходной и оптимизированной программ в
формальной модели автотьюнинга. Эту проверку в частных случаях можно выполнять автоматически по исходному коду
программы с помощью техники переписывающих правил.
Ключевые слова: автоматизация оптимизации параллельных программ, автотьюнинг, алгебро-динамические модели, техника
переписывающих правил, проверка корректности преобразований.
Вступ
Сучасний стан розвитку науки свідчить про те, що для розв'язання складних науково-технічних задач
необхідні значні обчислювальні потужності, а їх раціональне використання завжди було однією з головних
проблем під час розробки прикладних програм. Сучасні процесори мають багато ядер й багато рівнів кеш-
пам'яті, що додатково ускладнює архітектуру мультипроцесорних обчислювальних систем. Оптимальна
програма має ефективно розподіляти обчислення між усіма ядрами, а також максимально ефективно
використовувати усі рівні пам'яті: від процесорного кешу до жорсткого накопичувача. Таку програму важко
створити, навіть знаючи наперед характеристики цільового обчислювального середовища (ОС), а етап
налаштування потребує значних зусиль. Написання програми, яка буде одразу оптимальною у різних ОС
виявляється неможливою задачею через занадто велике розмаїття сучасних процесорів.
Отже, для досягнення максимальної ефективності програми (тобто, мінімального часу її виконання)
необхідне її додаткове налаштування (тюнінг) під ОС, в якому вона буде виконуватися. Сучасна методологія
самоналаштування (автотюнінгу) дозволяє автоматизувати це налаштування. Ідея автотюнінгу полягає в
емпіричному оцінюванні декількох варіантів програми й вибору найкращого. Традиційно підбір виконує
окрема програма-тюнер. Вона ж відповідає за генерацію різних модифікацій вихідної програми. Основними
критеріями оцінки, зазвичай, є швидкодія й точність отриманих результатів.
У цілому дії програми-тюнера є досить шаблонними – обрати/створити нову версію програми й отримати
емпіричну оцінку її швидкодії. Програмне рішення, запропоноване у роботі, дозволяє тюнеру автоматично
генерувати нові коректні версії програм, спираючись на експертне знання розробника, оформлене у вигляді
метаданих у вихідному коді.
В роботі, на прикладі методу вибору оптимальної стратегії обходу індексованих структур даних для
покращення швидкодії оптимізовуваної програми, проілюстровано як можна автоматизувати перевірку
коректності перетворень вихідного коду програми. Ця перевірка спирається на властивості, сформульовані у
термінах дискретних динамічних систем для паралельних програм.
Властивості програм
Виконання будь-якої програми можна змоделювати з використанням теорії дискретних динамічних
систем (ДДС) [1]. ДДС задається як трійка (𝑆0, 𝑆, 𝑑), де 𝑆 – простір станів; 𝑆0 ⊆ 𝑆 – множина початкових станів;
𝑑 ∈ 𝑆 × 𝑆 – бінарне відношення переходів у просторі станів. Система може перейти із стану 𝑠𝑖 в стан 𝑠𝑗 якщо
(𝑠𝑖,𝑠𝑗) ∈ 𝑑. Повне визначення ДДС з переліком базових операторів й виразів можна знайти у [1]. Формальна
модель автотюнінгу 𝑆tune, що представлена як еволюційне розширення моделі дискретних динамічних систем
Методи машинного навчання
369
будується у роботі [2]. Вона базується на ДДС для мультипоточних програм 𝑆𝑚𝑡, яка в свою чергу побудована
на моделі rпослідовних програм 𝑆𝑠𝑒𝑟. Програми у цих моделях представлені у вигляді виразів алгебри
Глушкова (АГ) [7], які інтерпретуються як функції ДДС.
Визначимо деякі властивості програм, які допоможуть проаналізувати коректність й ефективність
оптимізаційних перетворень, що виконує тьюнер. Під коректністю перетворень будемо розуміти те що вихідна
й перетворена програми повертають однаковий результат. Формально цю умову можна сформулювати
наступним чином. Нехай задана підмножина 𝑉𝑅 ⊂ 𝑉 результуючих змінних. Тоді дві програми 𝑃1 й 𝑃2 будемо
називати еквівалентними за результатом, якщо для однакових початкових даних 𝑏0програми одночасно
приходять або не приходять в фінальні стани 𝑠𝑓
1 = (𝑏1, 𝜀, ∅) й 𝑠𝑓
2 = (𝑏2, 𝜀, ∅), причому ці фінальні стани пам’яті
співпадають за результуючими змінними 𝑏𝑉𝑅
1 = 𝑏𝑉𝑅
2 .
Аналогічним чином, використовуючи поняття ∆- відхилення з попереднього підрозділу, введемо поняття
∆(дельта)-коректності для класу задач, які дозволяють поступитися точністю результатів обчислень заради
пришвидшення швидкодії програми. Дві програми 𝑃1 й 𝑃2 будемо називати еквівалентними за результатом з ∆-
точністю, якщо для однакових початкових даних 𝑏0 програми одночасно приходять або не приходять в фінальні
стани 𝑠𝑓
1 = (𝑏1, 𝜀, ∅) й 𝑠𝑓
2 = (𝑏2, 𝜀, ∅), причому ці фінальні стани пам’яті відхиляються не більше ніж на
величину ∆: 𝑟(𝑏𝑉𝑅
1 , 𝑏𝑉𝑅
2 ) ≤ ∆.
Еквівалентність за результатом – достатньо загальна властивість, проте реалізувати перевірку цієї
властивості в загальному випадку практично неможливо оскільки для цього необхідний аналіз усіх можливих
шляхів виконання програми в залежності від вхідних даних й варіантів виконання різних потоків. Тому
необхідно визначення більш часткових властивостей для опису коректності перетворень, які можуть бути
практично перевірені.
Спочатку визначимо деякі властивості операторів АГ. Для кожного оператора 𝑦 ∈ 𝑌 визначені множини
𝑅(𝑦) ⊂ 𝑉 змінних, від яких залежить результат застосування оператора, й 𝑊(𝑦) ⊂ 𝑉 змінних, які змінюють
значення в результаті виконання оператора. Два оператора 𝑦1, 𝑦2 ∈ 𝑌 будемо називати залежними (за даними),
якщо 𝑅(𝑦1) ∩ 𝑊(𝑦2) ≠ ∅ або 𝑊(𝑦1) ∩ 𝑅(𝑦2) ≠ ∅, або 𝑊(𝑦1) ∩ 𝑊(𝑦2) ≠ ∅. Два оператори 𝑦1, 𝑦2 ∈ 𝑌 є
перестановочними або, комутативними (відносно операції композиції) якщо 𝑦1𝑦2 = 𝑦2𝑦1. Очевидним є те що
незалежні оператори є перестановочними, проте обернене твердження не є істинним – наприклад, дві копії
одного оператора 𝑦 ∈ 𝑌 завжди перестановочні, але вони залежні якщо 𝑊(𝑦) ≠ ∅.
Тепер визначимо наступні властивості програм: безтупиковість, безконфліктність й еквівалентність за
операторами. Програму 𝑃 будемо називати безтупиковою, якщо при її виконанні не з’являються тупикові
стани (стан коли неможливе подальше виконання залишку програми у ДДС). Очевидно що усі послідовні
програми в моделі 𝑆𝑠𝑒𝑟 є безтупіковими.
В моделі 𝑆𝑚𝑡 будемо називати конфліктним переходом ситуацію коли існують залежні оператори, які
виконуються одночасно у різних потоках. Програму 𝑃 будемо називати безконфліктною якщо при її виконанні
не з’являються конфліктні переходи. Для безконфліктних програм можна не використовувати функцію merge
(2.2). Замість об’єднання результатів одночасного виконання декількох операторів можна виконати ці
оператори послідовно у будь-якій послідовності.
Якщо відома послідовність виконання програми (послідовність переходів ДДС), можна визначити
історію використання базових операторів [9]. Для цього додамо до стану ДДС ще одну компоненту ℎ ∈ 𝑌 . В
початковому стані ℎ = 𝜀. Також модифікуємо правило переходу (1): (𝑏, 𝛾𝑅, 𝐹, ℎ) → (𝛾(𝑏), 𝑅, 𝐹, ℎ𝛾). При
одночасному виконанні декількох правил (1) у різних потоках будемо додавати відповідні оператори 𝑦 у
довільному порядку. Оператор ℎ у фінальному стані будемо називати історією використання операторів.
Дві історії ℎ1, ℎ2 будемо вважати еквівалентними (відносно визначеної системи рівності операторів АГ)
якщо ℎ2 можна отримати з ℎ1 послідовним застосуванням операції рівності до операторів історії. Зокрема,
система рівності завжди включає усі відношення які визначають комутативність операторів. Тобто ℎ2 також
можна отримати із ℎ1 послідовними перестановками комутативних пар операторів. Дві програми 𝑃1 й 𝑃2
будемо називати еквівалентними за операторами якщо для однакових вхідних даних 𝑏0 вони породжують
еквівалентні історії виконання операторів.
Тепер можна сформулювати наступне твердження:
Лема 1. Якщо дві програми 𝑃1 й 𝑃2 безтупікові, безконфліктні й еквівалентні за операторами, то вони
еквівалентні за результатом.
Доведення. Безтупикові програми не переходять у тупикові стани, отже вони або переходять в
фінальний стан або не зупиняються взагалі. В останньому випадку історія операторів буде нескінченно, а тому,
якщо така ситуація має місце для𝑃1, то вона буде виконуватися й для 𝑃2. Отже перша частина визначення
еквівалентності за результатом доведена. Перевіримо тепер, що на однакових вихідних даних програми
обчислюють однаковий результат. Обчислення програми можна представити у вигляді виконання деякого
комбінованого оператора 𝑦𝑓 над вихідним станом пам’яті 𝑏0: 𝑏𝑓 = 𝑦𝑓𝑏0. Виходячи з побудови ДДС 𝑆𝑠𝑒𝑟 й 𝑆𝑚𝑡,
комбінований оператор є послідовною композицією операторів, які виконуються на кожному переході ДДС.
Для системи 𝑆𝑚𝑡 кожен перехід поєднує множину переходів окремих потоків; проте для безконфліктних
програм перехід системи, вцілому, еквівалентний послідовній композиції переходів окремих потоків, які
розглядаються у довільному порядку.
Методи машинного навчання
370
Таким чином для безконфліктних програм комбінований оператор співпадає з історією виконання
операторів, тобто 𝑦𝑓 = ℎ. З визначення еквівалентності за операторами виплаває, що ∀𝑏 ∈ 𝐵, (ℎ1𝑏)𝑉𝑅
=
(ℎ2𝑏)𝑉𝑅
, тобто історії операторів діють однаково на результуючі данні. Тому 𝑏𝑉𝑅
1 = (ℎ1𝑏0)𝑉𝑅
= (ℎ2𝑏0)𝑉𝑅
= 𝑏𝑉𝑅
2 ,
що й треба було довести.
Отже чином перевірка еквівалентності за результатом зводиться до перевірки цих трьох властивостей,
що є цілком можливим для багатьох задач.
Перехід між різними представлення програми
Якщо обирати підхід до трансформації вихідного коду програм виходячи суто з “практичних” міркувань
то в деяких випадках достатньо було б представлення програм у вигляді текстового файлу. Наприклад, для
заміни значення константи яка задає початкове значення деякої змінної програми. Проте, такі структурні зміни
як обернення ітерацій циклу потребують більш високорівневого представлення, зокрема для того щоб
трансформація не залежала від форматування вихідного коду.
Також можна використовувати представлення програми у вигляді дерева синтаксичного розбору. Для
побудови такого представлення використовують синтаксичний аналізатор відповідної мови програмування,
який іноді називають парсером. Дерево синтаксичного розбору все ще можна віднести до низькорівневого
представлення оскільки кожна синтаксична конструкція мови програмування явно представлена в моделі.
Як вже зазначалося, модель програми у вигляді операторів АГ – більш високорівневе представлення, яке
є більш компактним. Також вона краще підходить для теоретичного аналізу. Проте вона потребує додаткових
спеціалізованих засобів для побудови моделі й перетворення її в код програми. Також варто зауважити, що, на
відміну від низькорівневих моделей, побудована модель мультипоточних програм не залежить від мови
програмування, хоч і є специфічною для деякої предметної області.
Також для виконання перетворень можна використовувати фреймворк Termware [3], [4], який спирається
на техніку переписувальних правил. Цей фреймворк дозволяє для деякої предметної області визначити
відповідність між операторами й предикатами АГ й програмним кодом деякої(деяких) мови програмування [8].
Така відповідність дає змогу використовувати переписувальні правила Termware для автоматичного переходу
між двома рівнями представлення програми.
Наведемо поняття паттернів для Termware, за допомогою яких будемо визначати відповідність. Паттерн
буде задаватися парою < 𝑡𝑝, 𝑡𝑔 >, де 𝑡𝑝 – позначення паттерна який задає новий елемент моделі високого рівня
а 𝑡𝑔 - зразок що визначає паттерн (елемент моделі низького рівня).
Простим прикладом може бути паттерн Join для операції очікування завершення роботи іншого потоку.
Для нього 𝑡𝑝 = __ 𝐽𝑜𝑖𝑛($𝑥) а комбінований оператор 𝑡𝑔 = 𝑤𝑎𝑖𝑡(__𝑇𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑖𝑜𝑛𝐸𝑣𝑒𝑛𝑡($𝑥)). Цей паттерн містить
змінну $𝑥 й використовує додатковий паттерн __𝑇𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑖𝑜𝑛𝐸𝑣𝑒𝑛𝑡($𝑥) для визначення частини терму.
Якщо для деякої предметної області визначені предикати й оператори високорівневої моделі – це робить
можливим створення програми на будь-якому з рівнів: низькорівневий вихідний код та дерево синтаксичного
розбору або високорівнева модель АГ. В роботі розглядається застосування методів автотьюнінгу до вже
написаних програм, тобто парсер Termware трансформує вихідний код у синтаксичне дерево. Далі
застосовуються патерни й переписувальні правила для переходу до алгебро-алгоритмічного представлення, в
якому можна перевірити коректність. Далі з використанням іншої системи переписувальних правил можна
виконати зворотній перехід до низькорівневої моделі, по якій генератор Termware може відтворити початкову
версію вихідного коду, так і породити нову з додатковими модифікаціями.
Перевірка властивостей
Властивості безтупіковості, безконфліктності й еквівалентності за операторами, які було визначено у
попередньому підрозділі, в загальному випадку важко перевірити. Проте, для окремих часткових випадків,
можна вказати достатні умови для забезпечення цих властивостей, які легше перевірити. Розглянемо деякі такі
умови.
Умова еквівалентності за операторами практично значить що деякі комутативні оператори програми
були переставлені у історії виконання. Вимогу комутативності для перестановки операторів в межах
послідовної композиції будемо позначати як CommutativeOperators. У випадках коли окремі ітерації циклу
виконуються в іншій послідовності для еквівалентності за операторами необхідно щоб комутативними були
окремі ітерації (будемо позначати цю умову як CommutativeIterations) а також щоб була взаємно однозначна
відповідність між ітераціями у обох програмах (вихідна й перетворена). Останню умову позначимо
IdenticalIterations.
Перевірка умов комутативності – достатньо складна задача у загальному випадку, оскільки потребує
аналізу властивостей усіх операторів, викликів функцій й можливих варіантів виконання програми. У багатьох
випадках комутативність можна встановити на основі незалежності операторів циклу (для умови
CommutativeIterations), що значно легше зробити з використанням техніки переписувальних правил. У інших
випадках будемо виконувати перевірку результатів програми.
Наприклад, для перевірки властивості CommutativeIterations деякого циклу програми можна згенерувати
програму з оберненим порядком ітерацій. Якщо у вихідній програмі ітерації були перестановочними то
Методи машинного навчання
371
модифікована програма повинна обчислити той самий результат. Очевидно що співпадіння результатів тесту
ще не гарантує комутативності ітерацій оскільки можлива ситуація коли на деякому іншому наборі даних
результати обчислень будуть відрізнятися. Для зменшення вірогідності такої ситуації можна використовувати
тести з більш складними трансформаціями. Наприклад, розгорнути дві ітерації циклу у одну й перемішати
оператори цих ітерацій.
Важливою перевагою використання фреймворку TermWare й техніки переписувальних правил є
можливість автоматизувати створення великого набору різних тестів для кожної конкретної програми.
Умову безконфліктності можна сформулювати наступним чином: будь-які два залежні оператора, що
можуть виконуватися у різних потоках, повинні бути захищеними відповідними критичними секціями
(секціями з однаковими ідентифікаторами). Далі будемо позначати цю умову як AllNeededCS. Безпосередня
перевірка цієї умови вимагає виконання повного аналізу залежностей програми і є складною задачею [11].
Проте, в деяких часткових випадках перевірка значно спрощується. Наприклад, незалежними будуть оператори
які змінюють лише локальні змінні для потоку.
Перейдемо до розгляду властивості безтупиковості й почнемо з випадка коли в програмі відсутні
оператори wait. Цю умову легко перевірити за допомогою простої системи правил TermWare:
wait($x) ->NIL [error()];
Без операторів wait потенційні тупикові ситуації можуть з’явитися лише через використання операторів
lock. В цьому випадку залежність між критичними секціями можна зобразити у вигляді орієнтованого графа:
вершинами будуть усі критичні секції програми 𝑐𝑠𝑖 а ребро з вершини 𝑐𝑠𝑖 в 𝑐𝑠𝑗 додається у випадку коли
деякий потік 𝑇𝑘 може виконати оператор 𝑙𝑜𝑐𝑘(𝑐𝑠𝑗) з критичної секції 𝑐𝑠𝑖. У такій інтерпретації безтупиковість
програми еквівалентна властивості ациклічності (позначимо як NoCyclicCriticalSections) побудованого графа.
Частковим випадком є ситуація коли програма не містить критичних вкладених секцій (умова
NoEmbeddedCriticalSections) – граф критичних секцій буде ациклічним оскільки в ньому взагалі не буде ребр.
Цю умову досить легко автоматично перевірити з використанням переписувальних правил TermWare:
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 додає спеціальний маркувальний терм 𝑚0 в початок кожного методу. Цей терм
використовується під час обходу усіх операторів методу. Правило 2 замінює маркер 𝑚0 на 𝑚1 якщо при обході
зустрічається критична секція. Правило 3 виконує зворотне перетворення якщо маркер пересувається до точки
завершення критичної секції й нові секції не зустрічаються (виконується властивість
NoEmbeddedCriticalSections). Якщо ж умова NoEmbeddedCriticalSections порушується – система правил
сигналізує про помилку за рахунок правила 4. Правила 5 й 6 забезпечують пересування маркерів 𝑚0 й 𝑚1 між
операторами методу.
Звісно, порушення умови NoEmbeddedCriticalSections ще не вказує на те що у програмі є помилка яка
призводить до тупика. В таких випадках необхідно перевіряти більш загальну вимогу NoCyclicCriticalSections.
Варто зауважити що багато прикладних паралельних програм задовольняють властивості
NoEmbeddedCriticalSections оскільки такий стиль використання синхронізації суттєво простіше для розуміння.
Перевірка безтупиковості суттєво ускладнюється якщо в програмі використовуються оператори wait – у
цьому випадку для кожного оператора 𝑤𝑎𝑖𝑡(𝑒𝑣𝑖) має бути присутнім відповідний оператор 𝑠𝑖𝑔𝑛𝑎𝑙(𝑒𝑣𝑖). Це
дуже важко перевірити для усіх можливих варіантів виконання програми.
Тому замість загальних умов безтупиковості при використанні операторів wait будемо формулювати й
розглядати деякі шаблони їх використання, для яких гарантується коректність.
Наприклад, оператор бар’єрного очікування 𝐵𝑎𝑟𝑟𝑖𝑒𝑟(𝑡𝑠𝑖), який задає точку в програмі у якій кожен потік
очікує усі інші або деяку частину, може бути заданий наступним чином:
𝐵𝑎𝑟𝑟𝑖𝑒𝑟(𝑘, 𝑏𝑖) = 𝑙𝑜𝑐𝑘(𝑐𝑠𝑏𝑖
); 𝑖𝑛𝑐(𝑐𝑜𝑢𝑛𝑡_𝑏𝑖); 𝑖𝑓(𝑐𝑜𝑢𝑛𝑡_𝑏𝑖 < 𝑘, 𝑢𝑛𝑙𝑜𝑐𝑘(𝑐𝑠_𝑏𝑖); 𝑤𝑎𝑖𝑡(𝑒𝑣_𝑏𝑖), 𝑎𝑠𝑠𝑖𝑔𝑛(𝑐𝑜𝑢𝑛𝑡_𝑏𝑖, 0);
𝑠𝑖𝑔𝑛𝑎𝑙_𝑎𝑙𝑙(𝑒𝑣_𝑏𝑖); 𝑢𝑛𝑙𝑜𝑐𝑘(𝑐𝑠_𝑏𝑖))
Як видно з визначення, цей складений оператор використовує додаткову змінну 𝑐𝑜𝑢𝑛𝑡_𝑏𝑖, критичну
секцію 𝑐𝑠_𝑏𝑖 й точку синхронізації 𝑒𝑣_𝑏𝑖. У додатковій змінній зберігається кількість потоків які вже очікують
за бар’єром. Якщо їх менше за параметр 𝑘 – поточний потік також буде очікувати. Як тільки потоків збирається
𝑘 штук – усі вони вивільнюються й у змінну 𝑐𝑜𝑢𝑛𝑡_𝑏𝑖 записується 0.
Оператор бар’єру не буде спричиняти тупики якщо загальна кількість потоків де він використовується
рівна 𝑘 й у кожному потоці виконується однакова кількість операторів 𝐵𝑎𝑟𝑟𝑖𝑒𝑟. У багатьох сучасних мовах з
Методи машинного навчання
372
підтримкою багатопоточності є безпосередня імплементація оператора бар’єру тому немає необхідності
реалізовувати його через базові оператори wait та signal. Проте сформульована умова безтупіковості програми з
бар’єрами в цьому випадку також залишається істинною.
Метод вибору оптимальної стратегії обходу індексованих структур даних
Розглянемо метод оптимізації використання процесорного кешу програмами з ітеративною схемою
обчислень. Як відомо, сучасні процесори мають декілька рівнів кешів з різною швидкістю доступу. Розміри цих
кешів зазвичай відрізняються на порядок тому швидкодія програми сильно залежить від частоти переміщення
даних між цими рівнями. Запропонований метод автоматично згенерує і оцінить швидкодію інверсного
напрямку ітерування даними й, у першу чергу, орієнтований на задачі що працюють з великими багатомірними
даними. Для одномірних масивів послідовне зчитування елементів масиву у більшості випадках автоматично
буде найшвидшим за рахунок апаратної оптимізації – доступ до “сусідніх” елементів значно швидший якщо
вони вміщуються у одну кеш-лінію. Проте, якщо програма працює з багатовимірними масивами або з їх
представленням у одновимірному масиві – частіше за все сусідні з точки зору ітерацій циклу елементи не
будуть потрапляти до однієї кеш-лінії. Тому варто оцінити усі комбінації ітерування – їх кількість рівна 2d, де d
– кількість вкладених циклів.
Позначимо вихідний варіант програми через P1 а її трансформовану варіацію зі зміненим напрямком
ітерування довільного циклу через ReversedCycleP1. Перевірка властивості комутативності ітерацій
CommutativeIterations в загальному вигляді є складною для перевірки тому розглянемо декілька часткових
випадків, для яких така перевірка можлива.
Введемо нову властивість яка характеризує обчислення що виконуються в межах ітерацій одного циклу.
Будемо казати що ітерації циклу задовольняють вимоги AllLocalVariables якщо внутрішні оператори
використовують лише внутрішні змінні. Ця властивість перевіряється системою переписувальних правил
Termware яка дозволяє використовувати лише одну зовнішню змінну – лічильник циклу.
Теорема 1. Ітерації циклу є комутативними (властивість CommutativeIterations) якщо вони
задовольняють властивості AllLocalVariables.
Доведення досить очевидне оскільки властивість AllLocalVariables виключає будь-яку залежність за
даними між різними ітераціями циклу.
Зауважимо що властивість AllLocalVariables не має великої практичної цінності – оператори циклу не
використовують індексованих структур (одно/багатовимірні масиви) й зміна напрямку ітерування не впливає на
ефективність використання кешів, тому швидкодія програми не буде залежати від виконуваної трансформації.
Тому розглянемо більш універсальний випадок коли оператори циклу або читають або записують
значення у зовнішні змінні але ніколи не роблять це одночасно. Така властивість (далі будемо позначати як
ReadOrWriteAccessToVariables) виключає рекурентну схему обчислень. Ця властивість, як і AllLocalVariables,
виключає залежність за даними між ітераціями циклу, з чого випливає виконання умови їх комутативності
CommutativeIterations. Типовим прикладом такої схеми обчислень є простий послідовний алгоритм множення
матриць – кожна ітерація циклу зчитує відповідні значення з вихідних матриць й записує результат у іншу
змінну.
Сформулюємо ще одну властивість – властивість “локальності” операторів циклу у тому сенсі що вони
виконуються в одному потоці й не залежать від даних з інших потоків. Будемо позначати таку властивість
циклів через OnlySequentialCalculations. Цю властивість легко перевірити системою переписувальних правил
яка забороняє використання операторів для багатопоточної взаємодії call_thread,wait,signal,signal_all,lock та
unlock.
Теорема 1. Програми P1 й ReversedCycleP1 еквівалентні за результатом якщо ітерації трансформованих
циклів задовольняють властивостям OnlySequentialCalculations й ReadOrWriteAccessToVariables.
Доведення. Для доведення теореми, згідно з лемою 1 необхідно перевірити властивості безтупиковості,
безконфліктності й еквівалентності за операторами програм P1 й ReversedCycleP1.
Безтупиковість обох програм випливає з властивості OnlySequentialCalculations й характеру
трансформації – змінюється лише напрям ітерування циклу(ів).
Відсутність взаємодії між потоками гарантує відсутність конфліктних переходів у P1 й ReversedCycleP1 а
тому й безконфліктність програм.
Для доведення еквівалентності за операторами необхідно щоб виконувалися умови CommutativeIterations
й IdenticalIterations. Умова IdenticalIterations гарантується самою трансформацією – змінюється лише порядок
ітерацій циклу а не їх кількість. Властивість же CommutativeIterations (комутативність ітерацій циклу) випливає
з умови ReadOrWriteAccessToVariables.
Програмна реалізація
Як було зазначено раніше, на додачу до перевірки властивостей переписувальні правила також
дозволяють автоматизувати різноманітні шаблони трансформацій вихідного коду програм. Застосування
методу вибору оптимальної стратегії обходу індексованих структур даних на практиці можна звести до
розмічення циклів у вихідному коді програми прагмами-коментарями. За цими мітками автотьюнер згенерує
Методи машинного навчання
373
систему переписувальних правил, яка ‘розверне’ ітерації циклу у зворотному напрямку. Наприклад, у мові Java
для циклів типу:
//bidirectionalCycle
for (int loopVar = 0; loopVar <42; loopVar ++){
…………………
}
Відповідне переписувальне правило виглядає наступним чином:
ForStatement(
LoopHead(
ForInit(VariableDeclarator(Id("loopVar"),Literal($initialValue))),
RelationalExpression(Identifier("loopVar"),"<",Literal($endValue)),
ForUpdate(StatementExpression(Identifier( "loopVar "),"++"))),
Block(.....)
) ->
ForStatement(
LoopHead(
ForInit(VariableDeclarator(Id("loopVar"),Literal($endValue))),
RelationalExpression(Identifier("loopVar"),">",Literal($initialValue)),
ForUpdate(StatementExpression(Identifier( "loopVar "),"--"))),
Block(.....)
)
Це правило, використовуючи пропозиційні змінні [5], міняє місцями початкове і фінальне значення
лічильника циклу й замінює оператор зміни значення цього лічильника на кожній ітерації циклу.
Приклад застосування
Запропонований метод було використано під час оптимізації паралельного алгоритму задачі
короткотермінового метеорологічного прогнозування [9]. Ця задача була обрана для практичного розгляду,
оскільки вона має високу обчислювальну складність і природну необхідність у максимально швидкому й
точному результаті. Її програмна реалізація поєднує геометричне та операторне розщеплення а схема обчислень
є ітеративною. Для зберігання даних використовуються чотиривимірні масиви. Повний опис математичної
моделі, декомпозиції області обчислень та методу розщеплення можна знайти у [6].
Чисельний експеримент проводився на гомогенній ЕОМ зі спільною пам’яттю й 24-ма задіяними
процесорами. Зміна лише напрямку ітерування даними в результаті дала покращення загального часу
виконання обчислень у 13 %. Що, у сукупності з геометричною декомпозицією вхідних даних й паралельною
реалізацією операторного розщеплення, дозволило досягти мультипроцесорного прискорення 𝑊 (24) = 18.36
загальної ефективність 𝐸(24) = 0.76, що є гарним показником.
Висновки
В роботі запропоновано підхід до перевірки коректності оптимізаційних перетворень паралельних
програм, що виконуються автотьюнером, з використанням техніки переписувальних правил. Гнучкість підходу
полягає у тому, що цю перевірку у часткових випадках можна виконати автоматично за вихідним кодом
програми. Підхід було проілюстровано на прикладі методу вибору оптимальної стратегії обходу індексованих
структур даних для програм з ітеративною схемою обчислень. Цей метод застосовано до оптимізації
паралельного алгоритму складної прикладної задачі короткотермінового метеорологічного прогнозування.
Результати практичного експерименту підтвердили доцільність застосування методу.
Література
1. Андон Ф.И., Дорошенко А.Е., Цейтлин Г.Е., Яценко Е.А. Алгеброалгоритмические модели и методы параллельного
программирования. Киев: Академпериодика, 2007. 631 с.
2. Иваненко П.А., Дорошенко А.Ю. Метод автоматической генерации автотюнеров для параллелных программ. Кибернетика и
системный анализ. 2014. № 3 С. 75–83
3. TermWare http://www.gradsoft.ua/products/termware_rus.html
4. Дорошенко А.Е., Шевченко Р.С. Система символьных вычислений для программирования динамических приложений. Проблеми
програмування. 2005. № 4. С. 718–727.
5. TermWare tutorial, http://www.gradsoft.ua/rus/Products/termware/docs /tutorial_rus.html
6. Черниш Р.І. Модифіковане адитивно-усереднене розщеплення, його паралельна реалізація та застосування до задач метеорології:
автореф. дис. канд. фіз.-мат. наук, Київ: КНУ ім. Т. Шевченка. 2010 p.
7. Глушков В.М. Алгебра. Языки. Программирование, 3-е изд. К: Наукова думка, 1989. с. 376.
Методи машинного навчання
374
8. Дорошенко А.Ю., Бекетов О.Г., Жереб К.А., Іваненко П.А., Овдій О.М., Шевченко Р.С., Яценко Е.А. Формальні та адаптивні методи й
інструментальні засоби паралельного програмування. Проблеми програмування. 2017, № 3. С. 19–30.
9. Дорошенко А.Ю., Іваненко П.А., Овдій О.М., Яценко О.А. Автоматизоване проектування програм для розв’язання задачі
метеорологічного прогнозування. Проблеми програмування. 2016. № 1. C. 102–115.
References
1. Andon P.I., Doroshenko A.Y., Zhereb K.A., Yatsenko O.A. Algebra-Algorithmic Models and Methods of Parallel Programming. Kyiv:
Akadem- periodyka, 2018. 192 p. (in Ukrainian).
2. Ivanenko P.A., Doroshenko A.Y. Method of Automated Generation of Autotuners for Parallel Programs. Cybernetics and Systems Analysis.
2014. N 3. P.75–83. (in Russian).
3. TermWare http://www.gradsoft.ua/products/termware_rus.html. (in Russian).
4. Doroshenko A.Y., Shevchenko R.S. System of symbolic calculations for dynamic applications programming. Problems in programming. 2005.
N 4. P. 718–727. (in Ukrainian).
5. TermWare tutorial, http://www.gradsoft.ua/rus/Products/termware/docs /tutorial_rus.html. (in Russian).
6. Chernysh R.I. Modified additive-averaged decomposition method, it’s parallel implementation and application to meteorology tasks. (2010):
abstract of dissertation of candidate of science in Physics and Math. Kyiv: Taras Shevchenko National University of Kyiv. (in Ukrainian).
7. Hlushkov V.M., Algebra. Languages. Programming (1989), 3rd edition. Kyiv: Naukova dumka. 376 p. (in Russian)
8. Doroshenko А.Y., Beketov, Zhereb K.A., Ivanenko P.A., Ovdii О.М., Shevchenko R.S., Yatsenko O.A. Formal and adaptive methods and
software tools of parallel programming. Problems in programming. 2017. N 3. P. 19–30. (in Ukrainian).
9. Doroshenko А.Y., Ivanenko О.М. Ovdii O.A. Yatsenko. Automated program design for solution of weather forecasting problem. Problems in
programming. 2016. N 1. P. 102–115. (in Ukrainian)
Одержано 10.03.2020
Про авторів:
Іваненко Павло Андрійович,
кандидат фізико-математичних наук,
науковий співробітник.
Кількість наукових публікацій в українських виданнях – 28.
Кількість наукових публікацій в зарубіжних виданнях – 3.
https://orcid.org/0000-0001-5437-9763.
https://scholar.google.com.ua/citations?user=aV5SrrAAAAAJ.
Місце роботи авторів:
Інститут програмних систем НАН України,
03187, м. Київ-187, проспект Академіка Глушкова, 40.
Тел.: (38)(044) 526-21-48.
E-mail: paiv@ukr.net
|
| id | pp_isofts_kiev_ua-article-429 |
| institution | Problems in programming |
| keywords_txt_mv | keywords |
| language | Ukrainian |
| last_indexed | 2025-07-17T09:40:27Z |
| publishDate | 2020 |
| publisher | PROBLEMS IN PROGRAMMING |
| record_format | ojs |
| resource_txt_mv | ppisoftskievua/24/58737510bc3bd05bee55a972cf87e424.pdf |
| spelling | pp_isofts_kiev_ua-article-4292020-12-07T15:40:57Z Validation of correctness of autotuning code transformations with rewriting rules technique Об анализе корректности автотьюнингу программ с использованием техники переписывающих правил Про аналіз коректності автотьюнінгу програм з використанням техніки переписувальних правил Ivanenko, P.A. automation of parallel program optimization; autotuning; algebra-dynamic models; rewriting rules technique; validation of code transformations correctness UDC 004.4`2 автоматизация оптимизации параллельных программ; автотьюнинг; алгебро-динамические модели; техника переписывающих правил; проверка корректности преобразований УДК 004.4`2 автоматизація оптимізації паралельних програм; автотьюнінг; алгебро-динамічні моделі; техніка переписувальних правил; перевірка коректності перетворень УДК 004.4`2 Article presents an approach to correctness validation of autotuning optimizational transformations. Autotuner is considered as dynamic discrete system and validation is reduced to verification of characteristic of equivalence by result of representation of initial and optimized program versions in autotuning formal model. In partial cases this validation can be done automatically using source code and rewriting rules technique.Problems in programming 2020; 2-3: 368-374 В работе представлен подход к проверке корректности оптимизационных преобразований параллельных программ, выполняемых автотьюнером. Автотьюнер рассматривается как эволюционная дискретная динамическая система, а проверка корректности сводится к проверке свойству эквивалентности по результату интерпретаций исходной и оптимизированной программ в формальной модели автотьюнинга. Эту проверку в частных случаях можно выполнять автоматически по исходному коду программы с помощью техники переписывающих правил.Problems in programming 2020; 2-3: 368-374 У роботі запропоновано підхід до перевірки коректності оптимізаційних перетворень паралельних програм, що виконуються автотьюнером. Автотьюнер розглядається як еволюційна дискретна динамічна система й перевірка коректності зводиться до перевірки властивості еквівалентності за результатом представлень вихідної і оптимізованої версій програм у формальній моделі автотьюнінгу. Цю перевірку у часткових випадках можна виконати автоматично за вихідним кодом за допомогою техніки переписувальних правил.Problems in programming 2020; 2-3: 368-374 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2020-09-16 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/429 10.15407/pp2020.02-03.368 PROBLEMS IN PROGRAMMING; No 2-3 (2020); 368-374 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2020); 368-374 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2020); 368-374 1727-4907 10.15407/pp2020.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/429/432 Copyright (c) 2020 PROBLEMS IN PROGRAMMING |
| spellingShingle | automation of parallel program optimization autotuning algebra-dynamic models rewriting rules technique validation of code transformations correctness UDC 004.4`2 Ivanenko, P.A. Validation of correctness of autotuning code transformations with rewriting rules technique |
| title | Validation of correctness of autotuning code transformations with rewriting rules technique |
| title_alt | Об анализе корректности автотьюнингу программ с использованием техники переписывающих правил Про аналіз коректності автотьюнінгу програм з використанням техніки переписувальних правил |
| title_full | Validation of correctness of autotuning code transformations with rewriting rules technique |
| title_fullStr | Validation of correctness of autotuning code transformations with rewriting rules technique |
| title_full_unstemmed | Validation of correctness of autotuning code transformations with rewriting rules technique |
| title_short | Validation of correctness of autotuning code transformations with rewriting rules technique |
| title_sort | validation of correctness of autotuning code transformations with rewriting rules technique |
| topic | automation of parallel program optimization autotuning algebra-dynamic models rewriting rules technique validation of code transformations correctness UDC 004.4`2 |
| topic_facet | automation of parallel program optimization autotuning algebra-dynamic models rewriting rules technique validation of code transformations correctness UDC 004.4`2 автоматизация оптимизации параллельных программ автотьюнинг алгебро-динамические модели техника переписывающих правил проверка корректности преобразований УДК 004.4`2 автоматизація оптимізації паралельних програм автотьюнінг алгебро-динамічні моделі техніка переписувальних правил перевірка коректності перетворень УДК 004.4`2 |
| url | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/429 |
| work_keys_str_mv | AT ivanenkopa validationofcorrectnessofautotuningcodetransformationswithrewritingrulestechnique AT ivanenkopa obanalizekorrektnostiavtotʹûninguprogrammsispolʹzovaniemtehnikiperepisyvaûŝihpravil AT ivanenkopa proanalízkorektnostíavtotʹûnínguprogramzvikoristannâmtehníkiperepisuvalʹnihpravil |