Більшість сучасних інструментів статичної верифікації погано масштабуються на складне програмне забезпечення. Метою роботи була розробка інструменту, який стане золотою серединою між точними і повільними інструментами статичної верифікації і швидкими, але менш точними інструментами статичного аналізу. Основною ідеєю підходу є абстракція від точного взаємодії потоків і аналіз кожного потоку окремо від усіх інших, але в деякому оточенні, яке моделює вплив потоків друг на друга. Оточення містить опис можливих дій над розділяються даними і примітивами синхронізації, а також умов їх застосування. Варіюючи точність побудови оточення, можна добиватися необхідного балансу між швидкістю і точністю аналізу в цілому. Формальний опис пропонованого підходу було зроблено з використанням теорії адаптивного статичного аналізу. Це дозволило сформулювати умови і довести коректність пропонованого підходу в цих умовах. Для ефективного пошуку станів гонки використовується спеціальна модель пам'яті, яка дозволяє розділяти області пам'яті на непересічні регіони, які відповідають типам даних. Реалізація запропонованого підходу у фреймворку CPAchecker дозволяє перевикористати існуючі техніки аналізу з мінімальними змінами. А реалізація додаткових технік аналізу в рамках запропонованої теорії дозволяє підвищити точність аналізу. Результати проведених експериментів на двох наборах тестових завдань дозволяють зробити висновок про масштабованості і практичної застосовності методу.

Анотація наукової статті з комп'ютерних та інформаційних наук, автор наукової роботи - Андріанов П.С.


Analysis of correct synchronization of operating system components

Most of the software model checker tools do not scale well on complicated software. Our goal was to develop a tool, which provides an adjustable balance between precise and slow software model checkers and fast and imprecise static analyzers. The key idea of ​​the approach is an abstraction over the precise thread interaction and analysis for each thread in a separate way, but together with a specific environment, which models effects of other threads. The environment contains a description of potential actions over the shared data and synchronization primitives, and conditions for its application. Adjusting the precision of the environment, one can achieve a required balance between speed and precision of the complete analysis. A formal description of the suggested approach was performed within a Configurable Program Analysis theory. It allows formulating assumptions and proving the soundness of the approach under the assumptions. For efficient data race detection we use a specific memory model, which allows to distinguish memory domains into the disjoint set of regions, which correspond to a data types. An implementation of the suggested approach into the CPAchecker framework allows reusing an existed approaches with minimal changes. Implementation of additional techniques according to the extended theory allows to increase the precision of the analysis. Results of the evaluation allow confirming scalability and practical usability of the approach.


Область наук:

  • Комп'ютер та інформатика

  • Рік видавництва: 2019


    Журнал: Праці Інституту системного програмування РАН


    Наукова стаття на тему 'АНАЛІЗ коректно СИНХРОНІЗАЦІЇ КОМПОНЕНТІВ ЯДРА операційних систем'

    Текст наукової роботи на тему «АНАЛІЗ коректно СИНХРОНІЗАЦІЇ КОМПОНЕНТІВ ЯДРА операційних систем»

    ?DOI: 10.15514 / ISPRAS-2019-31 (5) -16

    Аналіз коректності синхронізації компонентів ядра операційних систем

    П.С. Андріанов, ORCID: 0000-0002-6855-7919 <Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її.>

    Інститут системного програмування ім. В.П. Іваннікова РАН, 109004, Россия, г. Москва, вул. А. Солженіцина, д. 25

    Анотація. Більшість сучасних інструментів статичної верифікації погано масштабуються на складне програмне забезпечення. Метою роботи була розробка інструменту, який стане золотою серединою між точними і повільними інструментами статичної верифікації і швидкими, але менш точними інструментами статичного аналізу. Основною ідеєю підходу є абстракція від точного взаємодії потоків і аналіз кожного потоку окремо від усіх інших, але в деякому оточенні, яке моделює вплив потоків друг на друга. Оточення містить опис можливих дій над розділяються даними і примітивами синхронізації, а також умов їх застосування. Варіюючи точність побудови оточення, можна добиватися необхідного балансу між швидкістю і точністю аналізу в цілому. Формальний опис пропонованого підходу було зроблено з використанням теорії адаптивного статичного аналізу. Це дозволило сформулювати умови і довести коректність пропонованого підходу в цих умовах. Для ефективного пошуку станів гонки використовується спеціальна модель пам'яті, яка дозволяє розділяти області пам'яті на непересічні регіони, які відповідають типам даних. Реалізація запропонованого підходу у фреймворку CPAchecker дозволяє перевикористати існуючі техніки аналізу з мінімальними змінами. А реалізація додаткових технік аналізу в рамках запропонованої теорії дозволяє підвищити точність аналізу. Результати проведених експериментів на двох наборах тестових завдань дозволяють зробити висновок про масштабованості і практичної застосовності методу.

    Ключові слова: стан гонки; роздільний аналіз потоків; статична верифікація; операційна система Linux

    Для цитування: Андріанов П.С. Аналіз коректності синхронізації компонентів ядра операційних систем. Праці ІСП РАН, тому 31, вип. 5, 2019, сс. 203-232. DOI: 10.15514 / ISPRAS-2019-31 (5) -16

    Analysis of correct synchronization of operating system

    components

    P.S. Andrianov, ORCID: 0000-0002-6855-7919 <Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її.>

    Ivannikov Institute for System Programming of the Russian Academy of Sciences, 25, Alexander Solzhenitsyn st., Moscow, 109004, Russia

    Abstract. Most of the software model checker tools do not scale well on complicated software. Our goal was to develop a tool, which provides an adjustable balance between precise and slow software model checkers and fast and imprecise static analyzers. The key idea of ​​the approach is an abstraction over the precise thread interaction and analysis for each thread in a separate way, but together with a specific environment, which models effects of other threads. The environment contains a description of potential actions over the shared data and synchronization primitives, and conditions for its application. Adjusting

    the precision of the environment, one can achieve a required balance between speed and precision of the complete analysis. A formal description of the suggested approach was performed within a Configurable Program Analysis theory. It allows formulating assumptions and proving the soundness of the approach under the assumptions. For efficient data race detection we use a specific memory model, which allows to distinguish memory domains into the disjoint set of regions, which correspond to a data types. An implementation of the suggested approach into the CPAchecker framework allows reusing an existed approaches with minimal changes. Implementation of additional techniques according to the extended theory allows to increase the precision of the analysis. Results of the evaluation allow confirming scalability and practical usability of the approach.

    Keywords: Data race; Thread-Modular approach; Software verification; Linux kernel

    For citation: Andrianov P.S. Analysis of correct synchronization of operating system components. Trudy ISP RAN / Proc. ISP RAS, vol. 31, issue 5, 2019, pp. 203-232 (in Russian). DOI: 10.15514 / ISPRAS-2019-31 (5) -16

    1. Введення

    Верифікація багатопоточних програм завжди була більш складним завданням, ніж верифікація послідовних програм. Точне обчислення всіх можливих чергувань (interleavings), призводить до комбінаторному вибуху числа станів. Тому, більшість інструментів статичної верифікації застосовують різні техніки оптимізації: редукція часткових порядків (partial order reduction) [1,2], абстракція лічильника (counter abstraction) [3] та інші. Тим не менше, більшість сучасних інструментів статичної верифікації погано масштабуються на промислове програмне забезпечення. Цей факт підтверджується результатами порівняння інструментів статичної верифікації на наборі завдань SV-COMP [4]. Завдання з категорії «многопоточность», засновані на драйвери операційної системи Linux, викликають значні труднощі для всіх інструментів статичної верифікації. Однією з альтернатив методам перевірки моделей є методи статичного аналізу, які націлені на швидкий пошук помилок без абсолютної впевненості в фінальному вердикті. Такі інструменти застосовують різні фільтри і евристики для прискорення аналізу і тому не можуть гарантувати коректність, тобто відсутність помилок. У даній роботі представлений підхід до статичної верифікації многопоточного програмного забезпечення, який дозволяє вибирати баланс між швидкістю і точністю проведеного аналізу.

    Суть пропонованого підходу полягає в наступному. Оскільки об'єктом верифікації буде велика многопоточная програма, ми заздалегідь відмовляємося від аналізу всієї програми з урахуванням всіх можливих взаємодій потоків і розглядаємо кожен потік по-окремо. В цьому випадку стану кожного потоку стають частковими, тобто вони не містять інформацію про інших потоках і, отже, не можуть описати повне стан всієї програми. Можливий вплив потоків друг від друга апроксимується зверху безліччю дій, яке потоки можуть здійснювати над розділяються даними, в тому числі примітивами синхронізації.

    Таким чином, апроксимація можливих дій, або ефектів, формується одночасно для всіх потоків і називається оточенням. Незважаючи на те, що оточення є єдиним для всіх потоків, звідси не випливає, що всі вхідні в нього ефекти будуть застосовані до деякого потоку, так як для кожного з ефектів визначаються умови його застосування, які залежать від використовуваного аналізу. Крім того, в умови застосування ефекту можуть включатися вимоги на конкретні оператори і стану потоку.

    Точність побудови оточення визначає багато в чому точність і швидкість роботи всього інструменту. Точність аналізу можна підвищити, комбінуючи різні техніки аналізу. Для реалізації цієї ідеї була використана платформа CPAchecker [5,6], 204

    яка надає багатий набір технік верифікації. Аналіз з роздільним розглядом потоків (thread-modular approach) [7-10] також можна реалізувати як одну з технік, яка вбудовується в CPAchecker і поповнює традиційний набір технік верифікації таких як, наприклад, CEGAR [11] і предикатна абстракція [12]. Ефективне розширення платформи CPAchecker вимагає не просто додавання ще одного виду аналізу. В ідеалі потрібно, щоб максимальна кількість видів аналізу могли працювати одночасно і обмінюватися даними між собою. Необхідною умовою такої тісної інтеграції є або слідування вже певної теорії CPA, або модифікація наявної теорії таким чином, що стара теорія виявлялася окремим випадком нової. Саме таке завдання ставилося в даному дослідженні. Пошук станів гонки зазвичай складається з двох основних етапів:

    1. побудова безлічі досяжних станів;

    2. знаходження в побудованому безлічі спеціальних станів, що утворюють стан гонки.

    Ці два кроки можуть виконуватися послідовно або паралельно в залежності від інструменту статичної верифікації. Наприклад, деякі інструменти статичної верифікації при додаванні кожного наступного стану перевіряють, чи не утворить воно стан гонки з деяким вже досяжним раніше станом аналізу. І в разі виявлення помилки, такий аналіз зупиняє своє виконання. Однак, такий спосіб є дуже повільним і непрактичним для пошуку станів гонки, хоча він успішно застосовується, наприклад, для вирішення завдань досяжності або пошуку помилок, пов'язаних з некоректним використанням пам'яті в послідовних програмах.

    Інструменти статичного аналізу, які шукають потенційні стану гонки, зазвичай використовують Lockset алгоритм для пошуку таких помилок. У запропонованому підході використовується більш точний алгоритм, в якому потенційний стан гонки є парою спільних переходів, які модифікують одну і ту ж пам'ять. Спільність тут означає, що два часткових стану двох потоків можуть бути частиною одного глобального стану. Таким чином, якщо розглядати тільки абстракцію над примітивами синхронізації, це зводиться до алгоритму Lockset, але при використанні інших варіантів аналізу, є більш точним. Предикатна абстракція разом з моделлю пам'яті BnB [14-16] дозволяє значно поліпшити роботу з доступами за вказівником і дозволяє зберегти коректність при розумних припущеннях. Оцінка підходу проводилася на безлічі завдань, заснованих на драйвери операційної системи Linux. Вони були підготовлені за допомогою системи Klever, яка дозволяє проводити верифікацію великих програмних систем [17, 18]. Klever розділяє великий обсяг коду на окремі фрагменти - верифікаційні завдання - і готує для них модель оточення. Основним внеском даної роботи є:

    1. розвиток теорії CPA, яка дозволяє комбінувати техніку thread-modular з іншими підходами, такими як предикатна абстракція;

    2. реалізація запропонованої теорії в інструменті CPAchecker, який був успішно апробований на безлічі завдань, заснованих на драйвери операційної системи Linux.

    Стаття організована таким чином. У розд. 2 представлені основні складності сучасних інструментів статичної верифікації та основи пропонованого підходу. У розд. 3 представлена ​​основна ідея підходу. Розд. 4 вводить основні визначення і модель програми. Наступні 7 розділів присвячені опису розширення теорії CPA: розд. 6 описує thread-modular підхід в термінах CPA, розд. 7 - 12 містять розширений опис основних аналізів (CPA). У розд. 13 описані основні

    особливості пошуку станів гонки в пропонованому підході. У розд. 14 представлені результати роботи інструменту на наборі SV-COMP і драйвери операційної системи Linux. У розд. 15 представлений короткий огляд родинних робіт.

    2. Приклад запуску існуючих інструментів верифікації

    Розглянемо приклад верифікаційної задачі1 з SV-COMP'19 [4]. Ця Верифікаційна завдання заснована на реальному стані гонкі2. Файл з вихідним кодом містить більше 7 000 рядків коду і 4 створюваних потоку: один потік для базових функцій platform пристрої, один - для обробки переривань, один - для функцій power management і один початковий потік, який виконує операції ініціалізації-деініціалізацію модуля. Всі примітиви синхронізації ядра (м'ютекси і спінлокі) були замінені на pthread м'ютекси. Відома помилка була записана, як завдання досяжності, в такий спосіб: tmp = tspi->rst; assert (tmp == tspi->rst);

    Докладні результати роботи інструментів можуть бути знайдені на офіційному сайті SV-COMP3. В основному, всі сучасні інструменти верифікації зіткнулися з проблемами:

    • CBMC: «pointer handling for concurrency is unsound - UNKNOWN»;

    • CPAchecker: «Unsupported feature: BDD-analysis does not support arrays»;

    • SMACK: «Exception thrown in lockpwn»;

    • yogar-cbmc: «out of memory»;

    • Ultimate: «Ultimate could not prove your program».

    Основним викликом для інструментів верифікації в цьому прикладі стала велика кількість операцій в потоках, велика частина з яких виконувалася над розділяються даними. Це означало, що потоки могли сильно впливати друг на друга. Це призводить до наступних підпроблеми, які зазвичай ігноруються при аналізі невеликих «навчальних» програм:

    1. Аналіз багатопоточних програм повинен бути досить точним, щоб видавати якомога меншу кількість помилкових попереджень, але бути досить ефективним, щоб вирішувати реальні завдання. Багато ефективні види аналізу не підтримують складні структури даних (наприклад, BDD аналіз [19], аналіз явних значень [20]). І навпаки, точні підходи викликають проблеми при аналізі довгих шляхів з перемиканнями між потоками (наприклад, аналіз предикатів [21], підхід з ограничиваемой перевіркою моделі [22]).

    2. Ефективне уявлення примітивів синхронізації. Багато підходи кодують блокування як змінні, які атомарному перевіряються і присвоюються (наприклад, [8, 10]). Кодовані таким чином блокування змішуються з іншими змінними і ускладнюють загальний аналіз.

    Крім того, завдання пошуку стану гонки в верифікаційних завданнях записується як завдання досяжності, що є підказкою для інструменту верифікації, який доступ до пам'яті може містити помилку. На практиці верифікатор не знає точне місце розташування потенційного стану гонки, і тому він повинен перевіряти всі

    1 https://github.com/sosy-lab/sv-benchmarks.git, sv-benchmarks / c / ldv-linux-3.14-races / linux-3.14-drivers-spi-spi-tegra20-sHnk.koxu.i

    2 https://patchwork.kernel.org/patch/9915305

    3 https://sv-comp.sosy-lab.org/2019/results/results-verified/META ConcurrencySafety.table.html 206

    можливі доступи до пам'яті. Це ще більше ускладнює завдання. У даній роботі представлений розроблений метод, який дозволяє вирішувати такі завдання.

    3. Схема пропонованого методу

    Як вже було сказано, в методах пошуку станів гонок умовно можна виділити два етапи, точніше, дві фази аналізу: побудова безлічі досяжних станів і перевірка вимог, в даному випадку, пошук парних станів, що утворюють гонку. Аналіз програми може проводитися шляхом послідовного чергування цих фаз або шляхом їх паралельного виконання. Зауважимо, що перевірка вимог зазвичай вимагає не дуже великих витрат, тому що являє собою умову на отримані стану. Прикладами таких перевірок можуть бути: відсутність станів спеціального виду (завдання досяжності), відсутність пари станів спеціального виду (завдання пошуку гонок). Побудова безлічі досяжних станів, навпаки, породжує ряд проблем, в першу чергу, пов'язаних з ефективністю. Розглянемо просту програму, в якій всього два потоки (рис. 1).

    volatile int g = 0;

    volatile int d = 0;

    Threadl {

    1 g = 1;

    2 d = 1;

    3

    }

    Thread2 {

    4 if (d == 1) {

    5 g = 2;

    6}

    }

    Мал. 1. Приклад невеликої програми Fig. 1. An example of a small program Це деякий модельний приклад, в якому використовується конструкція неявній синхронізації між потоками: перший потік инициализирует деякі дані (в даному випадку, глобальну змінну g), а потім виставляє прапор, що дані готові. Другий потік може використовувати ці дані тільки після виставлення прапора, тому в цьому прикладі немає стану гонки для змінної g. Класичні методи перевірки моделей перебирають всі можливі варіанти чергування двох потоків (приклад одного з можливих варіантів наведено на рис. 2).

    Thread 1 Thread 2

    g = 1;

    d = 1;

    [D == 1]

    g = 2;

    Мал. 2. Приклад одного варіанта виконання потоків Fig. 2. An example of an execution З точки зору інструменту статичної верифікації, необхідно розглянути повне безліч станів програми, які виникають при всіх можливих чергуваннях (рис. 3).

    Мал. 3. Побудова безлічі чергувань Fig. 3. Construction of interleaving set Навіть в простому прикладі і при різних оптимізацію загальне число станів зростає з катастрофічною швидкістю. Відбувається так званий «комбінаторний вибух» числа станів, що призводить до вичерпання ресурсів. Таким чином, класичні методи перевірки моделей не можуть забезпечити докази коректності програми. Прості методи статичного аналізу намагаються обчислити апроксимацію зверху можливих дій одного потоку на інший, так званий ефект потоку. Однак, вони не здатні простежувати складні залежності між змінними. Наприклад, залежності між глобальними змінними, які, в свою чергу, можуть бути модифіковані з інших потоків. У загальному випадку, це вимагає обчислення деякої нерухомої точки, що є небажаним при статичному аналізі, так як значно зростають вимоги до ресурсів. У підсумку, в таких складних випадках вважається, що глобальні змінні можуть приймати будь-які значення. А це, в свою чергу, знижує точність аналізу.

    Пропонований підхід базується на відомій ідеї роздільного аналізу потоків (thread-modular approach). Потоки в цьому випадку аналізуються по-окремо, одночасно з цим будується загальне для всіх потоків оточення, яке апроксимує зверху вплив інших потоків. Це оточення формується на основі аналізу всіх потоків, так як кожен потік є частиною оточення для інших потоків. Для кожного потоку визначається, як і в яких умовах він може модифікувати колективні дані, використовувати примітиви синхронізації і виконувати інші дії, що впливають на інші потоки. Точність аналізу потоку залежить від того, як точно буде сформовано оточення. Однак, залишається питання як ефективно обчислювати і представляти оточення.

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

    Ключовою ідеєю пропонованого підходу є розширення абстракції не тільки на стану програми, а й на операції, тобто, переходи потоку. Налаштовуючи рівень абстракції, можна отримувати варіанти аналізу, які будуть ближче до статичного аналізу багатопоточних програм, або до класичної статичної верифікації.

    потік 1

    Е = 1

    3

    Й-'1 S)

    I /

    3

    потік 2

    '0 .0-

    9-0. (J-в I->

    i /

    Мал. 4. Побудова абстрактних переходів двох потоків Fig. 4. Construction of abstract states of the first thread Рис. 4 показує частину абстрактного графа досяжності (Abstract Reachability Graph, ARG) для першого і другого потоку без впливу один на одного. Представлений аналіз заснований на простому аналізі явних значень [20], який відстежує тільки явні значення змінних. Перехід містить в собі абстрактне стан і абстрактну операцію. Перше абстрактне стан містить інформацію тільки про значення глобальної змінної x. Нова інформація про значення змінної y з'являється в дочірніх елементах, після того як виконаний перехід, відповідної ініціалізації змінної.

    Тепер необхідно врахувати вплив потоків друг на друга, тобто сформувати оточення. Будемо називати проекцією операції потоку опис її ефекту, відомого для інших потоків. Наприклад, будь-які модифікації локальних змінних потоку не впливають на інші потоки, тобто їх проекція є порожній операцією. Модифікація глобальної змінної є значущою для всіх потоків, тому її проекція повинна збігатися з самою операцією, або апроксимувати її зверху, наприклад, втрачаючи інформацію про точне присвоюється значення. При цьому в проекції може бути не тільки інформація про самій дії, а й про умови на його застосування до іншого потоку. Наприклад, на малюнку 5 перший потік, привласнюючи "g = 1" змінює значення змінної g з нуля на одиницю. Можна уявити проекцію цієї операції таким чином: якщо значення змінної x дорівнює нулю, то воно може бути змінено на одиницю. Іншими словами, проекція складається з двох частин: умови її застосування ([g == 0]) і безпосередньо дії (g ^ 1).

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

    Після побудови переходів в потоках незалежно один від одного (рис. 4), для всіх переходів обчислюються проекції. Для другого потоку, наприклад, це дія, яка змінює значення змінної x значення з нуля на трійку. Решта дії другого потоку не модифікують глобальні змінні і не породжують значущих проекцій. Потім ця проекція застосовується до кожного станом першого потоку. На малюнку 5 наведено результат застосування до першого переходу. Також цю проекцію можна застосувати і до другого, однак, ніяких нових шляхів це не породить. До третього переходу першого потоку застосувати цю проекцію можна, так як значення змінної x не задовольняє умові проекції. Застосування проекції до першого переходу породжує новий шлях виконання, який в свою чергу може породити нові проекції.

    Мал. 5. Побудова абстрактних переходів для двох потоків Fig. 5. Construction of abstract transitions for both of the threads На рис. 5 представлений варіант з точними проекціями, які розглядають переходи іншого потоку так, як вони є. На малюнку представлені не всі можливі проекції і породжені ними переходи. Наприклад, відсутня проекція переходу «g = 2» другого потоку.

    Для перевірки можливості стану гонки нам необхідно знайти два переходи, які модифікують одну змінну: «g = 1» в першому потоці і «g = 2» у другому. Далі, необхідно перевірити, чи є два абстрактних стану спільними, тобто, чи можуть вони бути частиною одного глобального стану. В даному випадку, в часткових станах потоку значення глобальних змінних мають різні значення, а значить, вони не можуть бути частиною одного глобального стану, тобто, зазначені два переходи не можуть бути виконані одночасно. Звідси випливає, що стан гонки відсутня.

    Пропонований підхід надає гнучкі варіанти конфігурації для вирішення кожного конкретного завдання. Як було показано на прикладах, проекції дій потоку можуть бути представлені більш точної абстракцією або, навпаки, занадто загальною. Проекції кількох операцій можуть бути об'єднані в одну або бути розглянуті по-окремо. Це дозволяє вибирати необхідний баланс між точністю та швидкістю. Розглянемо інший варіант побудови абстрактних переходів на рис. 6.

    Мал. 6. Побудова абстрактних переходів для двох потоків Fig. 6. Construction of abstract transitions for both of the threads

    Тут використовується більш абстрактне уявлення проекції, при якому кілька впливів потоку об'єднуються в одну проекцію (ефект від оточення). При цьому зазвичай втрачається деяка інформація. Зокрема, в даному випадку була втрачена інформація про точному значенні змінної g, і тому даний об'єднаний ефект може застосовуватися при будь-яких її значеннях. Це дозволяє скоротити число станів для аналізу.

    Приклад показує, як аналіз розглядає ефекти впливу одного потоку на інший, що гарантує коректність підходу. Більш того, він показує гнучкість підходу, який дозволяє варіювати рівень абстракції, наприклад, на стадії побудови проекції, вибираючи рівень абстракції кожного переходу в оточенні.

    4. Основні визначення

    У цьому розділі представлені основні визначення паралельної програми і досяжних конкретних станів програми, необхідні для опису математичної моделі паралельної (багатопотокової) програми і теорії CPA. Математичною моделлю паралельної програми буде програма на простому імперативною мовою, в якому є тільки такі оператори, які надають ефект на інші потоки або самі залежать від ефектів, що надаються іншими потоками. Такими операторами служать оператори присвоювання, перевірки умови (розгалуження), примітиви синхронізації, створення потоків. Формальний апарат опису таких моделей - це теорія, для побудови якої скористаємося простим імперативним мовою, досить виразним, щоб описувати моделі, згадані вище. Позначимо безліч операцій в моделі програмі Ops.

    Паралельна програма представляється автоматом потоку управління (Control Flow Automaton, CFA [5]), який складається з безлічі L точок програми (моделюються програмним лічильником, pc) і безліччю G? L * OpsxL дуг (ребер) потоку управління (моделюють операції, які виконуються, коли управління переходить від однієї точки в програмі до іншої). Операція створення потоку створює новий потік з ідентифікатором з безлічі T і цей потік починає своє виконання з деякою точки програми з L. Безліч змінних програми, які зустрічаються в операторах присвоювання і умовах з Ops позначаються X, а їх значення обмежимо безліччю цілих чисел'. Підмножини X, що містять тільки локальні і глобальні змінні, позначаються Xlocal і Xglobal відповідно. Операції захоплення / звільнення примітивів синхронізації визначаються на безлічі змінних-блокувань S, які мають значення з T U {1T}, де t? T означає, що відповідна блокування була захоплена потоком t, а 1T означає, що відповідна блокування не була захоплена.

    Конкретним станів програми називається четвірка (cpc, cl, cg, cs), де

    1. відображення cpc: T ^ L є частковою функцією з ідентифікаторів потоку в точку програми, в якій знаходиться цей потік;

    2. відображення cl: T ^ Clocal є частковою функцією з ідентифікаторів потоку в присвоювання локальних змінних їх значень, тобто Clocal: Xlocal ^ ред;

    3. відображення cg: Xglobal ^ ред є привласненням значень глобальних змінних;

    4. відображення cs: S ^ T U {1T} є привласненням значень змінним блокування.

    Безліч конкретних станів програми позначається як C. Відображення cpc і cl представляють собою локальну частину статків потоку, а cg і cs - глобальну. Позначимо dom - домен часткової функції, наприклад, dom (c;) = (t | 3 (t, -)? Cj.

    Для кожного стану c = (cpc, cl, cg, cs) ЄС повинна виконуватися умова dom (cpc) = dom (cl), що означає, що домени локальних частин стану повинні бути Консистентне і містити однакову кількість потоків. Це безліч позначимо dom (c) = dom (cpc) = dom (cl).

    g, t

    Визначимо відношення переходів ->? C х G х T х C, де дуга g Е G, а потік t Е T. Визначимо безліч конкретних переходів T = C х G х T. Елемент т Е T - це трійка т

    ч ^ ^ в! * 1 92 * 2 ^

    = (C, g, t). Будемо писати Ti ^ Т2 якщо 3c3 Е C: ci -> c2 -> c3. Семантику операцій визначимо пізніше. У будь-якому випадку коректний перехід g = (1,, 1 ') Е G повинен відповідати таким вимогам:

    1. перехід починається в стані c: t Е dom (c) Л cpc (t) = l.

    2. програмний лічильник потоку t переходить до точки 1 ': t Е dom (c') Л c'pc (t) = l '.

    3. кожен перехід в потоці t може змінити локальні частини тільки цього ж потоку, а локальні стану інших потоків повинні залишитися без змін; зауважимо, що для програм з покажчиками це не вірно, але поки ми не розглядаємо такі програми в теорії.

    Будемо позначати Reach ^ (f) = {т | 3ti, ..., Тп Е T, .т ^ Ti Тп = то}. будемо позначати

    eval (c, t, expr) значення виразу expr над змінними з Xlocal U Xglobal зі значеннями зі стану c ЄС потоку t Е T.

    4.1 Оператори умови

    Для дуги перевірки умови д = (I, assume (expr), V) Е G, t ЕТ, 1,1 'Е L перехід з

    g, t

    -> с, з = (СРС, cl, сд, cs), з = (з рс, з i, ЦД, з s) Е З існує, якщо

    dom (c) = dom (c '), тобто перехід не змінює безлічі потоків;

    • Ci = з i, cg = з g, cs = з s, тобто перехід не змінює значень змінних;

    • СРС (t) = I, с'рс (t) = V, тобто перехід відповідає загальним умовам на початок і кінець;

    • eval (c, t, expr) Ф 0, тобто значення змінних потоку задовольняють перевіряється умові.

    4.2 Оператори присвоювання

    g, t

    Для дуги присвоювання д = (I, assign (y, expr), I) Е G, t Е T, l, l Е L перехід з -> с, з = (Cpc, Ci, cg, cs), ^ = (с'рс, с'ьс'д, з's) Е З існує, якщо:

    • dom (c) = dom (c '), тобто перехід не змінює безлічі потоків;

    • ЧхЕХ ^ ХЕТ.с '^ х) ^ з: (с') (х), есяіхфуУСфС '

    leval (c, t, expr), якщо х = yht = t. , "(Сп (х), якщо ХФУ

    у Keval (c, t, expr), якщо х = у

    • cs = з's, безліч блокувань не змінюється при звичайному присвоєнні.

    • СРС (t) = I, с'рс (t) = V, тобто перехід відповідає загальним умовам на початок і кінець.

    4.3 Операції над примітивами синхронізації

    Визначимо операції над примітивами синхронізації acquire / release. Припускаємо, що операція acquire (s) в потоці t Е Т, де s Е S - це спеціальна змінна блокування, має стандартну семантику: атомарна перевірка значення змінної s і, в разі

    якщо s = ± t, привласнення їй ідентифікатора поточного потоку. Наприклад, така ж семантика розглядається в [8].

    g, t

    Для дуги захоплення блокування g = (I, acquire (s), I) E G, t E T, l, l EL перехід з -> с, c = (cpcci, cg, cs), c '= (c'pcc'i, c'g, c's) e З існує, якщо:

    • dom (c) = dom (c '), тобто перехід не змінює безлічі потоків;

    • cl = с \, сд = с'g, тобто перехід не змінює значень змінних;

    • СРС (t) = I, с'рс (t) = V, тобто перехід відповідає загальним умовам на початок і кінець;

    • cs (s) = 1т A c's (s) = t, Vs 'E S: s' Ф s ^ c's (s ') = cs (s').

    Операція звільнення блокування release (s) є зворотною до операції захоплення блокування і привласнює значення s = 1T, якщо це блокування була захоплена поточним потоком, тобто s = t.

    Для дуги звільнення блокування g = (l, release (s), V) EG, teT, l, l'eL перехід з

    g, t

    -> с, з = (СРС, cl, Cg, cs), з = (з рс, з t, cg, c s) E З існує, якщо:

    • dom (c) = dom (c '), тобто перехід не змінює безлічі потоків;

    • з1 = с'I, Cg = с'g, тобто перехід не змінює значень змінних;

    • СРС (t) = I, з 'рс (t) = V, тобто перехід відповідає загальним умовам на початок і кінець;

    • cs (s) = t A c's (s) = ± г, Vs 'E S: s' Ф s ^ c's (s ') = cs (s'). 4.4 Операція створення потоку

    Визначимо семантику операції thread_create (lv) таким чином, що поточний потік переходить в наступну точку програми, а новий потік створюється з ідентифікатором v E T і починає своє виконання з lv E L.

    У загальному випадку можливо необмежену створення потоків в програмі, якщо, наприклад, операція створення потоку зустрічається в циклі.

    Для дуги створення потоку g = (l, thread_create (lv), l ') E G, t E T, l, l' E L перехід з

    g, t

    -> с, c = (cpc, cl, cg, cs), з = (з pc, c l, cg, c s) E З існує, якщо:

    • v & dom (c) A dom (c ') = dom (c) U {v}, потік v додається в безліч потоків;

    • cl = c \, cg = с'g, cs = з's, тобто перехід не змінює значень змінних поточного потоку;

    • СРС (t) = I, с'рс (t) = V, тобто перехід відповідає загальним умовам на початок і кінець;

    • c'pc (v) = lv, тобто новий потік починає своє виконання зі свого початкового стану

    Поки ми не розглядаємо операції очікування потоку (thread_join (v)), так як вони будуть ускладнювати пояснення і доведення основної теореми коректності запропонованого підходу. Проте, їх підтримка також може бути додана.

    5. Адаптивний статичний аналіз з абстрактними переходами

    У класичній теорії адаптивного статичного аналізу (Configurable Program Analysis, CPA) [5, 6], абстрактне стан представляє безліч конкретних станів програми. У розширеній теорії, абстрактне стан є частковим і може не представляти ніяке стан програми. Ось чому функція конкретизації, яка зіставляє абстрактні стану з конкретними, в розширеній теорії

    відрізняється від класичної. Зокрема, вона визначається на безлічі абстрактних станів.

    Як наслідок, абстрактний перехід також є частковим. Тому аналіз не може гарантувати, що наступні конкретні переходи будуть досяжні за один крок оператора transfer. У загальному випадку для цього може знадобитися k кроків. Для підходу з роздільним аналізом потоків k = 2: аналіз виконує звичайний перехід в потоці, а потім поширює його на всі інші потоки в якості переходу в оточенні. Це вимагає двох ітерацій алгоритму.

    Визначимо формально адаптивний статичний аналіз з абстрактними переходами ГО = (D, П, merge, stop, prec, Він складається з абстрактного домену D, безліч точності П, оператор злиття merge, оператор зупинки stop, оператор настройки точності prec, і ставлення переходів

    1. Абстрактний домен D = (T,?, [[•]]) визначається безліччю T конкретних переходів, T? C х G х T, полурешеткой? над абстрактними переходами і функцією конкретизації [[.]]. Полурешетка? = (E, i, Т, з, U) складається з (можливо нескінченного) безлічі E абстрактних елементів, верхнього елементу решітки теє, нижнього елемента решітки iEE, частковий порядок з з E х E і функцію об'єднання U: E х E ^ E . Функція об'єднання визначає мінімальний елемент решітки, який більше заданих елементів.

    Функція конкретизації [[•]]: 2E ^ 2T для кожного безлічі абстрактних переходів R з E визначає безліч відповідних конкретних переходів програми. Основною відмінністю від класичної функції конкретизації - це визначення на безлічі абстрактних елементів. Таким чином, VR з Е | [[Д]] 3 Ue6fi [[{e}]]. Це означає, що сумарне знання від безлічі абстрактних переходів може бути більше, ніж об'єднання знання від кожного часткового переходу.

    2. Безліч точності П визначає можливу точність абстрактного домену. Аналіз використовує елементи точності, щоб відстежувати різні абстрактні стану з різною точністю. Пара (e, п) називається абстрактним елементом e з точністю п. Оператори на абстрактному домені параметризовані точністю.

    Для RCExn будемо позначати [[Д]] = [[U (e ^) 6fi {e}]].

    3. Ставлення переходів E х П х 2 e х E визначає для кожного часткового переходу е з точністю п можливий наступний перехід e '. При цьому результат може залежати від безлічі досяжних елементів R З E. Будемо позначати (е, п) e if (е, п, R, e) Е ^. Визначимо безліч Reachk по індукції: VR З Е | Reach 0 (R) = R

    Vk > 1 | Reach k + 1 (R) = ^ {e '| e ^ e '} U Reachk (R)

    eEReachk (R)

    Основна вимога до оператора transfer є апроксимація зверху безлічі конкретних переходів:

    3k > 1 | VR З E | Reach k (R) = ^ {т'1 t ^ т '}

    T Е [[й]]

    Ця вимога послаблює вимога на transfer класичної теорії. Воно означає, що оператор повинен видавати відповідні конкретні переходи на після одного кроку, як у класичній версії, а після k кроків. Для підходу з роздільним аналізом потоків k = 2, як ми побачимо надалі.

    4. Оператор злиття merge: ЕхЕхП ^ Е послаблює другий параметр, використовуючи інформацію від першого параметра і повертає новий абстрактний елемент з точністю, відповідної третього параметру. Оператор merge повинен задовольняти наступні умови:

    Ve, e 'Е E, n Е П: е' з тегде (е, е ', л)

    5. Оператор зупинки stop: Ex2Exnxn ^ {true, false} перевіряє, чи покривається абстрактний елемент, даний як перший параметр, безліччю елементів, даних як другий параметр. Оператор зупинки може, наприклад, шукати серед безлічі елементів такої, який покриває (с) даний елемент. Оператор зупинки повинен відповідати таким вимогам:

    Ve, e'Е Е, л Е n: stop (e, R, n) ^ VR з E: [[{e} U R]] з [[дід]]

    6. Функція настройки точності ргес: ЕхПх2ЕхП ^ Е>П обчислює новий абстрактний елемент і нову точність для заданого елемента з точністю і безлічі абстрактних елементів. Функція настройки точності може виконувати ослаблення (розширення) абстрактного елемента разом зі зміною точності. Функція настройки точності повинна задовольняти наступній вимозі:

    Ve, e 'Е E, n, n' Е n, R СЕхП: (е ', п') = prec (e, n, R) ^ е з е 'В цілому, безліч точності П, оператор зупинки stop, оператор об'єднання merge, оператор настройки точності prec залишаються такими ж, як і в класичній теорії CPA. На рис. 7 представлений основний алгоритм, який обчислює безліч досяжних абстрактних переходів, також не змінюється за винятком розширення оператора transfer.

    Мал. 7. Основною алгоритм CPA (D, eo, по) Fig. 7. The main algorithm CPA (D, eo, по) Для цього алгоритму основна теорема може бути доведена навіть з ослабленими вимогами. Доказ повторює доказ класичної теореми. Теорема (коректність). Для заданого адаптивного статичного аналізу з абстрактними переходами ГО, початкового стану e0 з точністю п0 алгоритм CPA (D, e0, п0) обчислює безліч абстрактних переходів, яке апроксимує зверху безліч досяжних конкретних переходів:

    [[СРА (ГО, е 0, Л0)]] 3 Reach ^ ([[[e0}]]) Слід зазначити, що на практиці використовується одночасно декілька різних CPA для аналізу вихідного коду. При цьому структура безлічі CPA нагадує деревоподібну, де корінь цього дерева надає оператори для основного алгоритму, представленого на рис. 7. Різні CPA взаємодіяти один з одним для підвищення точності аналізу. Так, в розд. 6 буде представлений верхнеуровневий CPA,

    215

    який вимагає наявність вкладеного CPA. Приклади вкладених CPA будуть представлені в розділах 7 - 11. CPA, представлений в розд. 12, реалізує паралельну композицію декількох вкладених аналізів. Розд. 13 описує, як реалізується пошук станів гонки за допомогою цих інструментів.

    Деякі службові CPA (CallstackCPA, AutomatonCPA), що не реалізують ніякі техніки аналізу, можуть бути застосовані без змін у порівнянні з класичною версією теорії, і тому не будуть описуватися далі. CPA, які реалізують різні техніки аналізу (аналіз явних значень, аналіз предикатів і ін.) Необхідно доопрацювати для того, щоб вони могли підтримувати переходи потоків в оточенні, в тому числі реалізувати оператор проекції. Ці CPA будуть описані у відповідних розділах.

    6. ThreadModularCPA

    У цьому розділі представлений CPA, який реалізує логіку підходу з роздільним аналізом потоків. Основна функціональність ThreadModularCPA полягає в обчисленні для кожного переходу в потоці потенційного ефекту для оточення, тобто проекцію цього переходу, а також в застосуванні отриманих ефектів оточення на відповідний потік.

    ThreadModularCPA включає в себе деякий внутрішній аналіз з розширеним безліччю операторів, які необхідні для роботи з оточенням: оператор проекції, оператор спільності, і оператор композиції. Спочатку формально визначимо розширення внутрішнього CPA.

    6.1 Розширення внутрішнього CPA

    Визначення CPA для підходу з роздільним аналізом потоків розширюється трьома новими операторами: I = (Di, П1, I, mergei, stopi, preci, compatibles ^, composei). Абстрактний домен DI = (TI,? I, ф1) складається з безлічі конкретних переходів TI, полурешеткі? I, і оператора композиції часткових станів ф1. Таким чином, внутрішній аналіз повинен визначити не функцію конкретизації [[•]], а оператор композиції ®, так як підхід з роздільним аналізом потоків вимагає однакової схеми обчислення конкретних станів.

    Як було вже сказано, стану і переходи є частковими, тому вони можуть не відповідати безпосередньо конкретним станів і переходів. Щоб отримати повний перехід, потрібно взяти композицію безлічі часткових переходів, які відповідають всім доступним потокам. Спільні часткові переходи можуть бути об'єднані в повний конкретний перехід за допомогою оператора композиції Е х Т х 2ЕхТ ^ 2T. Він повертає безліч конкретних переходів, яке відповідає даним частковим переходам.

    ® повинен відповідати полурешетке. Так, якщо один з абстрактних переходів менше, ніж інший, то композиція з тим же безліччю не повинна отримати більше безліч конкретних переходів.

    Оператор перевірки спільності compatibles E х E ^ {true, false} перевіряє, чи можуть два часткових переходу починатися із загального повного батьківського стану. Оператор проекції | p: E ^ E проектує перехід в потоці на інший потік. Наприклад, проекція може містити модифікації глобальних змінних, але опускати зміни локальних даних для потоку.

    composes E х E ^ E об'єднує два абстрактних переходу в один. Він застосовує абстрактну дугу з одного переходу до абстрактного станом іншого переходу.

    Надалі ми будемо використовувати оператор applyi, як комбінацію трьох операторів: | p, composei і compatiblei:

    Ve, e 'E E: apply (e.e') = {composel {e, e '\ p), ecnn compatible, {e, e' \ p)

    I 1, інакше

    Таким чином, оператор applyI означає, що переходи можуть бути об'єднані, тільки якщо вони сумісні. Результатом застосування оператора є новий перехід, який будемо називати переходом в оточенні, так як він є ефект оточення.

    6.2 CPA для роздільного аналізу потоків

    Визначимо спеціальний CPA, який реалізує логіку роздільного аналізу потоків: ТМ = (Dtm, ПТМ, ^ тм, mergeTM, stopTM, ргестм), який заснований на внутрішньому CPA I = (Di, П1, I, mergei, stopi, preci, compatiblei, | p, composei).

    Абстрактний домен DTM = (T,?, [[]]), Безліч конкретних переходів T = TI, а решітка? =? I. Функція конкретизації [[•]] виражається через оператор композиції ф1:

    ж

    VR ь Е: [[ «]] = U і ...... 3)

    к = 1 е 0, е'..., єк E R to, ti,. , TkE Т

    Ставлення переходів визначає наступні переходи, після чого застосовуються всі досягнуті переходи, як переходи в оточенні, до нових переходах, а нові переходи, як переходи в оточенні, - до вже досяжним (рис. 8).

    result: = (1;

    For each e: eo 1 e do result result U {?}: For each e? reached do

    result: - result U {apply (e \ e)} result: - result U {apply (e, e ')} end

    end

    return result_

    Мал. S. transferTM (eo, по, reached) Fig. S. transferTM (eo, по, reached) Безліч точності П, оператори merge, stop, prec відповідають операторам внутрішнього CPA.

    T. LocationCPA

    У цьому розділі представлений простий аналіз точок програми (Location Analysis) L = (Dl, П], ^ l, mergeL, stopL, precL, compatible], | p, composeL), який відстежує абстрактні точки програми. Аналіз розширює класичний LocationCPA для можливості застосування його разом з ThreadModularCPA.

    1. Абстрактний домен DL = (TL, EL, ®L). Абстрактний перехід складається з абстрактного стану s E El, і абстрактної дуги qE Е ^. Е [- це безліч абстрактних точок програми (англ. Program location), які відображаються на конкретні точки програми в CFA за допомогою функції loc: E [. Tf означає, що аналіз не знає, в якій саме точці програми знаходиться аналіз. Більш формально, loc (TSL) = L. У загальному випадку аналіз може використовувати абстрактними точками програми, які відповідають кільком конкретним точкам програми, але в подальшому буде

    описаний простий варіант аналізу, який розглядає тільки поодинокі точки програми:

    Vs? E [: s = TSLVs = ± 1 V loc (s) = {i)? L В цьому випадку використовується решітка? [Є плоскою, тобто будь-які два невироджених стану (нерівні Т? Або ± L) непорівнянні.

    Абстрактна дуга заснована на звичайній CFA дузі і містить тільки початкову точку програми і кінцеву: з е [х е?.

    2. Безліч точності є виродженим і містить тільки один елемент: П5 = {0}.

    3. Перехід e ^ L e ', e = (s, g), e' = (s ', g'), q = (pred, suc), q '= (pred', suc ') існує, якщо зміна точки програми відповідає абстрактної дузі. Більш формально, е е 'про loc (s) П loc (pred) Ф 0, Вд'? G: д '= (l'1, op, l'2) А 1'1? loc (pred ') П loc (s') А 1'2? loc (suc ') As' = suc.

    4. Оператор злиття merge не об'єднує елементи: mergeL (e, е ', п) = е'.

    5. Оператор зупинки stop розглядає унікальні стану: stopL (e, R, n) = (e? R).

    6. Точність не регулюється: precL (e, n, R) = (е, л).

    7. Перехід в одному потоці ніяк не впливає на перехід в іншому: Ve? EL, e = (s, g): e \ P = (s, e).

    8. Ve, e '? EL, e = (s, q): composeL (e, e ') = e = (s, q), де q = (s, s), так як перехід в одному потоці ніяк не може вплинути на становище іншої потоку.

    9. Ve1, e2? El: compatibleL (e1, e2) = true, так як два потоки можуть бути разом в будь-яких точках програми.

    8. ThreadCPA

    Визначимо простий аналіз потоків T = (Dt, Пт, ^ т, mergeT, stopT, ргест, compatible ^ | p, composeT), який відстежує ідентифікатори потоку.

    Аналіз потоків успадковує обмеження з [7] і обмежений програмами з кінцевим числом створінь потоків. Нехай в програмі є кінцеве число потоків, які ідентифікуються точками програми, в яких вони починають своє виконання, тобто Т з L і для кожного оператора створення потоку thread_create (pcv) завжди створюється потік з ідентифікатором pcv. Зауважимо, що інші типи аналізів не обмежені числом створінь потоків, більш того, можливе застосування більш складного аналізу потоків, який буде підтримувати необмежену кількість створінь. Таким чином, загальна теорія підтримує необмежене число створінь потоків.

    1. Абстрактний домен DT = (TT,? T, ®T) заснований на плоскій решітці над безліччю потоків T, де? Т =? T х? - ?. Безліч абстрактних станів = T U {± 7, ТІ, в якому будь-які два невироджених стану (нерівні Т? Або ± г) непорівнянні. Безліч абстрактних дуг містить безліч звичайних CFA дуг і порожній перехід в оточенні: ET = {± т, е, Tx} UG.

    2. Безліч точності є виродженим і містить тільки один елемент: Пт = {0}.

    3. Перехід e е ', е = (s, g), e' = (s ', g'), g = (-, op, -) існує, якщо

    • op Ф thread_create (pcv), s '= s, g'? G, тобто при будь-якої операції, крім створення потоку, стан не змінюється;

    • op = thread_create (pcv), s '= pcvVs' = s, g '? G. При створенні потоку створюються два дочірніх стану: одне відповідає створеному потоку, а інше -родітельскому.

    4. Оператор злиття merge не об'єднує елементи: mergeT (e, е ', л) = е'.

    5. Оператор зупинки stop розглядає унікальні стану: stopT (e, R, n) = (е Е R).

    6. Точність не регулюється: precT (e, л, R) = (е, л).

    7. Перехід в одному потоці ніяк не впливає на перехід в іншому: Ve Е ET, е = (s, g): е \ Р = (s, e). Переходи в оточенні (е-переходи) не можуть змінити ідентифікатор іншого потоку. Проте, проекція впливає на спільність станів, щоб переходи в потоці не застосовувалися, як ефекти оточення, до цього ж самого потоку.

    8. Ve, e 'Е ET, e = (s, q), e' = (s ', q'): composeT (e, e ') = e = (s, q').

    9. Ve1, e2 Е ET, ei = (si, qi), e2 = (s2, q2): compatibleT (e1, e2) = s1 Ф s2, так як два стани можуть бути разом, якщо вони відносяться до різних потокам.

    9. ValueCPA

    Визначимо аналіз явних значень V = (Dv, Пу, ^ у, mergev, stopv, precv, compatiblev, | p, composev), який відстежує явні значення змінних. Він складається з наступних елементів.

    1. Абстрактний домен dp = (Ту,? В, фу). ? У = (Еу, ^ у, Ту, Еу, Uv). Абстрактний перехід складається з абстрактного стану s Е Еу, а абстрактна дуга q Е Еу, таким чином, Еу = Е $ х EVT, а? У =? $ Х

    Абстрактне стан цього аналізу є відображенням з імен змінних в їх значення: Vs Е Ey, s: X ^ Z, де Z = J, U {Т2}. Таким чином, безліч абстрактних станів є плоскими гратами над цілими числами. Верхній елемент решітки Ту = [v \ VxЕX: v (x) = Tz}. є відображенням, в якому будь-яка змінна має будь-яке значення. А нижній елемент решітки = [v \ Зх Е X: v (x) = ^ z} є відображенням, в якому ніяка змінна не може мати ніякого явного значення. Такий стан є недосяжним при реальному виконанні програми. Порядок є тривіальним: будь-які два невироджених стану (нерівні Ту або ^ V) непорівнянні.

    Безліч абстрактних дуг містить безліч звичайних CFA дуг і переходи в оточенні, які визначаються зміною глобальних змінних: EV = 2X "ZUG.

    2. Точність аналізу явних значень визначається відстежувати змінними, таким чином безліч точності містить підмножини з усіх змінних програми: nv = 2х.

    3. Ставлення переходу е ™ v е ', е = (s, g), e' = (s ', g').

    I. g Е G, g = (-, op, -).

    a. g = (|, assume (expr), -):

    !^ Z, якщо $ c. (X ^ с): (expr Ф 0) / s з, якщо З! С. (Х ^ с): (expr Ф 0) / s або s (x) = з Tz, інакше

    Тут expr / v означає інтерпретацію виразу expr над змінними з X для абстрактного присвоювання v. А вираз (х ^ с): (expr Ф 0 ~) / s означає, що значення з у змінної х задовольняє інтерпретації.

    b. g = (|, assign (w, expr), |):

    (Exprеслі x = w Vx Е X: s '(x) = \

    (. S (x), інакше

    c. В інших випадках стан не змінюється s = s '.

    II. g ^ .X ^ Z, це означає, що ми маємо перехід, який змінює певні змінні. В цьому випадку, наступний стан

    4. Оператор злиття merge не об'єднує елементи: mergeV (e, е ', п) = е'.

    5. Оператор зупинки stop розглядає унікальні стану: stopV (e, R, n) = (е е R).

    6. Функція настройки точності обчислює нове абстрактне стан і точність, обмежуючи присвоювання тільки тими змінними, які містяться в точності: precV (e, n, R) = (в \ п, п).

    7. Перехід в оточенні може торкатися лише глобальні змінні: Ve е EV, e = (s, g): е \ Р = (salobal, galobal). Тут відображення salobal означає тільки ту частину, яка відноситься до глобальних змінних.

    8. Ve, e 'е EV, e = (s, q), e' = (s ', q'): composeV (e, e ') = е = (s, q').

    9. Ve1, e2 е EV, e1 = (s1, q1), e2 = (s2, q2): compatibleV (ei, e2) = Vx е xalobal: (x е dom (s1) Ах е dom (s2)) ^ foCO C s2 (x) Vs2 (x) C s ^ x)), що означає консистентность значень глобальних змінних.

    10. PredicateCPA

    У цьому розділі описаний відомий аналіз предикатів (Predicate Analysis) [21] з абстрактними переходами. Переходи аналізу предикатів складаються з двох частин: абстрактного стану і абстрактної дуги, яка може бути виражена або звичайною CFA дугою, або логічною формулою, що кодує виконувану операцію. Крім того, локальні змінні в цих формулах повинні бути перейменовані для уникнення колізії імен для різних потоків.

    Нехай P - це безліч формул над змінними програми в теорії без кванторів. Нехай P? P - це безліч предикатів, а v: X ^ ред - це відображення з змінних в їх значення. Визначимо v І <р, де v називається моделлю формули (р. Визначимо перейменування змінних 9: X ^ X 'з простору імен X в X', яке може бути застосовано до формул 0 (<р). позначимо

    Позначимо (ф) п декартову предикатную абстракцію формули ф. Позначимо SPop ^) - сильне постусловіем формули ф і операції op. Визначимо аналіз предикатів P = (Dp, Пр, ^ р, mergep, stopp, precp, compatiblep, | p, composeP), який відстежує здійсненність предикатів над змінними програми. Він складається з наступних компонентів:

    1. Абстрактний домен Dp = (TP,? Р, ®р). ? P = (Ep, ^ p, Tp, Cp, Up). Абстрактний перехід складається з абстрактного стану s е Ер, а абстрактна дуга q е Ej, таким чином, EP = x E'j, а? Р =? $ X? J.

    Ер = P, таким чином, стан є формулою першого порядку. Верхній елемент решітки є тотожно істинною формулою TP = true, а нижній елемент -тождественно помилковою: = false. Частковий порядок Cp? Ер x Ер визначається як eCp е 'про e ^ e'. Оператор злиття Up: Ер x Ер ^ Ер визначає найближчий елемент відповідно до частковим порядком.

    Абстрактна дуга QЕ Ej - це дія, яка може бути виражено або формулою, або звичайною CFA дугою: Ер = Ер U G.

    Ред = {

    x - x i, якщо хех .x - x, інакше;

    , і

    x i -> x, якщо x е X .x - x, інакше

    Не будемо наводити формальне визначення ®р, так як воно вимагає досить багато місця. Основна ідея полягає в тому, що він повертає безліч конкретних переходів, які відповідають формулі (найсильнішому постусловіем). Найбільш складна частина визначення це перевірка, чи може безліч часткових переходів відповідати єдиному глобальному переходу. Для переходу в потоці e0 зі звичайною CFA дугою q0? G і переходів в оточенні ei, ..., en перевірка складається з двох частин:

    a) для абстрактного стану s0 з e0 і всіх станів з переходів в оточенні si,., Sn існує загальна модель v;

    b) дуга qp з проекції eo | p покривається абстрактними дугами qj переходів в оточенні qp Е qj.

    формально,

    s т

    Ve0, e1, ..., en? ЕР, ei = (Si, qi), st? EP, qt? EP

    Cchecki? O, {el, ..., eJ) = BV: V І S0 A exlocal Д O-J Л | | | Л exiocai n (sn) Л (q0? G AVO < j < n: q, &GAe0 \ p = (sp, qp): qp Е q,

    2. Безліч точності Пр = 2P визначає точність абстрактного стану як безліч предикатів.

    3. Оператор об'єднання merge може мати кілька модифікацій, наприклад, mergejoin об'єднує обидві частини переходу:

    Ve, e '? ЕР, л? Пр, е = (s, g):

    !(S V s ', g), якщо g = g', g? G e ', якщо g? GAg'? TVg? TAg '? G (sV s'.gV g'), якщо g, g '? T mergeEq об'єднує тільки абстрактні дуги при рівних (або покритих) станах. mergesep не об'єднує елементи.

    4. Оператор зупинки stop перевіряє, чи покривається перехід e деяким іншим переходом в безлічі досяжності: stopP (e, R, n) = Be '? R: (е Е е ').

    5. Функція настройки точності prec обчислює предикатную абстракцію над предикатами в точності n: precP (e, n, R) = їв = (sn, q).

    6. Ставлення переходів e е ', е = (s, g), e' = (s, |). Так як аналіз предикатів не відслідковує релевантні дуги, він повертає всі можливі.

    Для g? G існує перехід е е 'з g = (•, op, •), якщо s' = (SPop (e)) n. Для g = <р? Р наступне абстрактне стан має вигляд s '= ф A е.

    7. Визначення проекції:

    !е, якщо g & G

    (Вхюса1, env (s), exiocai env ^ (з ^ .іначе

    Проекція визначає, як перехід виглядає як оточення потоку. Локальні змінні перейменовуються для уникнення колізії імен. Тому тільки предикати над глобальними змінними залишаються значущими. Стан (перша частина переходу) представляє абстракцію над глобальною частиною стану потоку. А дуга (друга частина переходу) відповідає конкретної операції над глобальними змінними.

    8. Ve, e '? ЕР, е = (s, q), e '= (s', q '): composeP (e, e') = е = (s, q ')

    9. Ve1, e2? EP, et = (si, qi), si? EP: compatibleP (ei, e2) = Bv: v І dxiocai 1 (s1) A

    Bxlocal 2 (s2)

    Перевірка спільності означає, що переходи можуть бути об'єднані в один глобальний. А це неможливо, якщо глобальні предикати неконсістентни, тобто не існує загальної моделі для двох часткових формул.

    11. LockCPA

    Визначимо аналіз примітивів синхронізації § = (Ds, ns, ^ s, merges, stops, precs, compatibles, | s, composes), який відстежує безліч захоплених блокувань (змінних синхронізації) для кожного потоку. Він складається з наступних компонентів:

    1. Абстрактний домен Ds = (Ts,? S, © s). ? S =? S x? S. ? S = 2s U {iS, TS} - це безліч всіх підмножин з змінних синхронізації, Is TS і Is 3

    ^ Т T T

    Is '^ Is is для всіх елементів Is, Is Q S. ET = {^ S,?, TS] UG.

    2. Для цього аналізу безліч точності містить тільки один елемент: П5 = {0}.

    3. Оператор переходу додає захоплювану блокування в безліч Is по час оператора acquire і видаляє її з нього під час оператора release. Формально, перехід е е ', е = (ls, g), e' = (ls ', g'), g = (-, ор, -) існує, якщо

    • op = acquire (s) і s Is A Is '= Is U {s}, g' E G.

    • op = release (s) і Is '= ls \ {s}, g' E G.

    • op = thread create (lv) і Is '= 0, g' E G

    • інакше, Is '= ls, g' E G.

    4. Оператор злиття merge не об'єднує елементи: merges (e, e ', n) = e'.

    5. Оператор зупинки stop перевіряє, чи існує стану, яке містить менше захоплених блокувань: stops (e, R, n) = Зе 'E R. (Е ^ е ').

    6. Точність не регулюється: precs (e, n, R) = (е, п).

    7. Визначення проекції: Ve E Es, e = (s, g): е \ Р = (s, e).

    Переходи в оточенні (е-переходи) не можуть змінити безліч захоплених блокувань, так як один потік не може вплинути на захоплені блокування іншого потоку. Проте, проекція сильно впливає на спільність станів, так як потоки не можуть захопити одну і ту ж блокування одночасно.

    8. Ve, e 'E Es, e = (ls, q), e' = (ls ', q'): composes (e, e ') = е = (ls, q').

    9. Ve:, e2 E Es, et = (lsi, qi), lsi E E $: compatibleP (e:, e2) = (Is П Is '= 0). Перевірка спільності сильно схожа на класичний алгоритм Lockset. Якщо існує одна і та ж блокування в обох станах, операції не можуть бути об'єднані, так як два потоки не можуть двічі захопити одну і ту ж блокування.

    12. CompositeCPA

    Аналіз використовується для комбінації різних технік аналізу разом. Приклади таких аналізів були описані вище. С = (Dc, Пс, ^ с, mergec, stopc, precc, compatiblec, | c, composec) включає в себе n вкладених аналізів Д; = (Di, П'mergeb stopb precb compatiblei, | i, composeO.

    1. Абстрактний домен DC = D1 x-- xDn реалізує декартовій твір всіх вкладених абстрактних доменів.

    2. Безліч точності також реалізує декартовій твір вкладених множин точності: Пс = П1 х - ХПП.

    3. Оператор переходу застосовує вкладені оператори переходу до відповідних частин стану. Таким чином, перехід можливий, якщо для всіх вкладених аналізів можливий перехід між відповідними вкладеними станами:

    Velt е2 Е EC: e1 ^ C е2 про V1 < i < п: е \ ^ Е12

    4. Оператор злиття merge викликає вкладені оператори: mergeC (e1, e2, n) = (merge1 (e}, Л1), ..., merge ^ e ™, е2, лп)).

    5. Оператор зупинки stop викликає вкладені оператори: Ve Е E, R Q Е, п Е n: stopC (e, R, n) = Ее Е R, V1 <i<n: stopi (ei, {el}, ni).

    6. Аналогічно оператор настройки точності викликає вкладені оператори: precC (e, n, R) = (prec1 (e1, n1, R), ..., precJl (en, nu, R)).

    7. Аналогічно оператор обчислення проекції викликає вкладені оператори: Ve Е EC ,: е \ Р = (е1 \ Р ..... єп \ Р).

    8. Ve1, e2 Е EC: composeC (e1, e2) = (compose1 (e}, е ^), ..., composen (e ", е2)).

    9. Ve1, e2 Е EC: compatibleC (e1, e2) = (compatible ^ !, йо), ..., compatiblen (e ", e2)).

    13. Пошук станів гонки

    Як вже було описано, пошук станів гонки розбивається на два етапи: побудова безлічі досяжних станів і пошук пар, які утворюють стан гонки. Для вирішення першої підзадачі застосовується набір з тих CPA, які були описані в попередніх розділах.

    Мал. 9. Приклад конфігурації CPA Fig. 9. An example of CPA configuration На рис. 9 представлений приклад конфігурації інструменту. Так, набір CPA містить ThreadModularCPA (розділ 6), в якості верхнеуровневого. У нього вкладено ARGCPA, який забезпечує зв'язок між різними абстрактними станами, в тому числі зв'язку «батьківський перехід - дочірній перехід», «проектується перехід - проекція» і ін. CompositeCPA (розд. 12) забезпечує паралельну роботу вкладених в нього CPA: LockationCPA ( розд. 7) моделює лічильник команд потоку, CallstackCPA забезпечує межпроцедурность аналізу, LockCPA (розд. 11) відстежує захоплення блокувань, ThreadCPA (розд. 8) відстежує точки створення потоків, PredicateCPA (розд. 10) реалізує аналіз предикатів. Важливо відзначити, що це не єдина можлива конфігурація інструменту. Більш того, для вирішення різних завдань можуть знадобитися різні конфігурації, тобто набори, використовуваних технік аналізу. Отже, за допомогою деякої конфігурації інструменту проводиться побудова абстрактного графа досяжності (англ. Abstract Reachability Graph, ARG) з абстрактних переходів. Тобто, по завершенню цього етапу є граф з переходів програми, які є досяжними при заданому рівні абстракції, тобто, зовсім не обов'язково вони будуть досяжними при реальному виконанні програми.

    Наступним етапом необхідно знайти серед цих переходів ті, які утворюють стан гонки.

    Зазвичай під станом гонки мається на увазі ситуація, при якій має місце одночасний доступ до деякої пам'яті з різних потоків, причому один з доступів має бути записом. Два основні питання, які виникають при статичному пошуку гонок: як визначити, що доступ проводиться до однієї і тієї ж пам'яті, і як визначити одночасність доступів. Далі будуть детально представлені ці дві особливості в пропонованому підході.

    При описі формальної моделі програми використовувався простий імперативний мову програмування, який підтримує колективні дані, представлені тільки глобальними змінними. У реальному програмному забезпеченні використовується велика кількість операцій з покажчиками, структурами і більш складними типами даних. Для роботи з ними використовується модель пам'яті BnB, яка розділяє всю пам'ять на непересічні безлічі регіонів. Кожен регіон відноситься до одного типу даних або полю структури, в разі якщо у нього не брався адресу. Така модель пам'яті має ряд обмежень. В першу чергу, вона не повністю підтримує адресну арифметику і кастірованіе, що накладає деякі додаткові умови на застосовність підходу. Крім того, вона може приводити до помилкових попереджень про помилки, в разі якщо два покажчика одного типу ніколи не вказують на одну і ту ж пам'ять.

    У разі, якщо виявилася пара доступів до однієї області пам'яті, в даному випадку, до одного регіону, необхідно перевірити можливість одночасного доступу до неї. Для цього використовується поняття спільності переходів. Спільність означає, що два часткових абстрактних стану можуть бути частиною одного глобального стану. Або, іншими словами, один перехід може бути застосований, як перехід в оточенні, до іншого переходу і навпаки, звідки випливає, що ці два переходи можуть бути виконані паралельно. Таким чином, запропонований підхід є узагальненням підходу Lockset [13], який визначає стан гонки, як два доступу до деякої пам'яті з непересічним безліччю блокувань. Одним з обмежень підходу Lockset є відсутність підтримки інших типів синхронізації. У розширенні підходу для цього використовується оператор compatible. Так як перевірка спільності використовує різні типи аналізу, включаючи аналіз примітивів синхронізації, аналіз предикатів і інші, такий спосіб є більш точним, ніж алгоритм Lockset. Отже, алгоритм пошуку станів гонки складається з наступних кроків:

    1. побудувати безліч досяжних абстрактних переходів (алгоритм 1);

    2. для кожного переходу визначити регіони пам'яті, до яких може проводитися доступ;

    3. для кожного регіону пам'яті спробувати підібрати пару спільних переходів, які утворюють стан гонки;

    4. перевірити кожну пару шляхів, що призводять до стану гонки, на досяжність і уточнити предикатную абстракцію в разі потреби [21].

    Слід додати, що алгоритм уточнення абстракції по контрприклад (англ. Counterexample Guided Abstraction Refinement, CEGAR [11]) був використаний без істотних модифікацій. Однак, в такому вигляді він дозволяє проводити уточнення тільки локальних шляхів в потоці, тобто не дозволяє виявити протиріччя між різними потоками. Однак, це не є принциповим обмеженням підходу, і при відповідному розширенні методу CEGAR на випадок підходу з роздільним розглядом потоків, можливо отримання більш точних результатів.

    14. Результати

    Підхід з роздільним помодульно аналізом потоків і абстракнимі переходами був реалізований в інструменті CPAchecker, як композиція наступних типів аналізу:

    1. Аналіз точок програми (англ. Location analysis) L;

    2. Аналіз стека викликів функціонально (англ. Callstack analysis) CS;

    3. Аналіз потоків (англ. Thread Analysis) T;

    4. Аналіз примітивів синхронізації (англ. Lock analysis) S (розділ 8);

    5. Аналіз предикатів з опціями (англ. Predicate analysis) P (розділ 7):

    I. Join - об'єднання абстрактних станів і абстрактних дуг. В даному варіанті все ефекти оточення предикатного аналізу об'єднуються в один, що, природно, знижує точність, але підвищує швидкість. II. Eq - об'єднання абстрактних дуг, якщо рівні абстрактні стану; III. Sep - переходи ніколи не об'єднуються.

    6. Аналіз явних значень (Value analysis) V [20].

    14.1 Результати на наборі завдань SV-COMP

    Набір завдань SV-COMP складається з тисячі вісімдесят дві завдань, велика частина з яких є невеликими прикладами близько 100 рядків коду. Однак, вони містять в собі нетривіальні механізми синхронізації, в тому числі алгоритми Деккера, Петерсона і ін. 7 завдань були підготовлені на основі драйверів ОС Linux. Всі завдання доступні в офіційному репозиторії SV-COMP4. Експерименти проводилися з використанням кластера з 191 машини VerifierCloud5. Були використані обмеження по пам'яті в 8 Гб і за часом 15 хвилин.

    Оцінка результатів реалізованого підходу в інструменті CPAchecker була проведена для наступних варіантів аналізу:

    1. Підходи з роздільним аналізом потоків з абстракцією переходів:

    a. Варіанти об'єднання для предикатного аналізу

    i. MergeJoin. (L, CS, T, S, P) Join.

    ii. MergeEq. (L, CS, T, S, P) Eq.

    iii. MergeSep. (L, CS, T, S, P) Sep.

    b. Value. Аналіз явних значень (L, CS, T, S, V).

    2. Threading. Аналіз чергувань, описаний в [17] використовує класичну теорію

    CPA і розглядає всі можливі чергування потоків.

    Табл. 1. Результати експериментів Table 1. Experiment Results

    Підхід MergeJoin MergeEq MergeSep Value Threading

    Знайдені 1026 1027 763 963 720

    помилки

    Справжні 805 806 548 752 720

    Помилкові 221 221 215 211 0

    Докази 27 28 28 30 165

    коректності

    Справжні 27 28 28 30 165

    Помилкові 0 0 0 0 0

    4 https://github.com/sosy-lab/sv-benchmarks

    5 https://vcloud.sosy-lab.org/cpachecker/webclient/master/info

    Незавершений аналіз 29 27 297 89 197

    Процесорний час, з Астрономічний час, з 16 800 10 200 15 900 9 630 278 000 258 000 75 300 64 900 93 700 67 500

    Результати (табл. 1) підтверджують, що підхід з роздільним аналізом потоків не пропускає помилок при деяких заздалегідь відомих обмеженнях. MergeJoin показує результати краще, ніж конфігурація MergeSep. Це відбувається, в основному, через велику кількість переходів в оточенні, які MergeSep розглядає по одному. MergeJoin об'єднує їх в один і застосовує за один раз. Це дозволяє зберегти величезну кількість часу. У той же час MergeSep дозволяє уникнути деяких неточностей через аналізу переходів по-окремо і видає меншу кількість помилкових повідомлень про помилки.

    Конфігурація Value є досить простим і швидким аналізом, але іноді вона змушена розглядати всі можливі варіанти значень змінних, що призводить до вичерпання ресурсів за часом.

    Класичний аналіз Threading є коректним і точним і не подає хибних вердиктів. Однак, він вимагає значного числа ресурсів, це є головним недоліком підходу. Ця конфігурація вирішила тільки один з семи складних завдань, заснованих на драйвери операційної системи Linux. Підходи до аналізу потоків по-окремо (MergeJoin, MergeEq, MergeSep) вирішують п'ять з семи таких завдань. Велика частина нових доказів коректності, отриманих новими підходами, (26 з 27 для MergeJoin) не знаходились класичними методами (Threading). Це також є одним з важливих вкладів даного методу.

    14.2 Пошук станів гонки в драйверах пристроїв

    Верифікаційні завдання, засновані на драйвери операційної системи Linux, були підготовлені системою Klever, яка призначена для верифікації різного програмного забезпечення [17, 18]. Вона розділяє великий обсяг цільового вихідного коду на окремі невеликі верифікаційні завдання. Для ядра операційної системи Linux Верифікаційна завдання відповідає одному модулю. Система Klever автоматично готує модель оточення модуля, яка включає в себе модель потоків, модель серцевини ядра і операцій над модулем. Після підготовки верифікаційної завдання Klever запускає верифікацію через загальний інтерфейс -BenchExec [23].

    Порівняння проводилося на підсистемі drivers / net / ядра операційної системи Linux 4.2.6, для якої Klever підготував 425 верифікаційних завдань. Експерименти також проводилися з використанням кластера з 191 машини VerifierCloud. Були використані обмеження по пам'яті в 8 Гб і за часом 15 хвилин. Алгоритм пошуку станів гонки за допомогою інструменту був описаний в розд. 12. При цьому підготовлені завдання не містили кодування стану гонки у вигляді перевірки завдання досяжності, тому було неможливо знову включити в порівняння учасників змагання SV-COMP, так як вони не підтримують пошук станів гонки. У порівнянні (табл. 2) брали участь такі зміни:

    1. Base. Конфігурація MergeJoin з попереднього пункту.

    2. Havoc. Конфігурація MergeJoin з попереднього пункту без можливості вилучення предикатів над глобальними змінними. Це означає, що аналіз не враховує значення глобальних змінних і вважає, що вони можуть мати випадкове значення.

    Табл. 2. Порівняння конфігурацій Base і Havoc Table 2. Comparing Base and Havoc Configurations

    Підхід Base Havoc

    Модулі з помилкою б 2б

    Коректні модулі 2б2 254

    Незавершений аналіз l57 l45

    Процесорний час, з l37 000 l25 000

    Модулі з помилкою означають, що в них було знайдено хоча б одне потенційне стан гонки. Конфігурація Havoc трохи швидша, але менш точна, тому вона не може довести коректність 8 коректних модулів, проте здатна виявити більше помилок. При цьому 6 з цих помилок були знайдені в пропущених коректних модулях, що означає, що знайдені помилки - помилкові через неточності аналізу. Але 13 помилок були відповідають незавершеного аналізу у Base конфігурації, що означає, що Havoc може знаходити нові помилки.

    Якщо вивчити ці 8 модулів, які були доведені, як коректні, то виявиться, що в них структура даних пристрою (дескриптора пристрою) була некоректно инициализирована при підготовці верифікаційної завдання, і тому в ній дійсно немає стану гонки. Насправді проблема пов'язана з підготовкою моделі оточення модуля (частина інфраструктури Klever), так як вони не враховує семантику даних.

    Частина отриманих помилок була проаналізована. Зазвичай для кожної верифікаційної завдання можуть бути отримані кілька потенційних станів гонки. Будемо називати їх попередженнями. Співвідношення справжніх попереджень до загальної кількості становить близько 42% (34 коректних попередження і 47 некоректних). Основною проблемою помилкових попереджень про помилки є проблеми з моделлю пам'яті (більш 90%). Решта попередження пов'язані зі специфікою ядра (наприклад, обробкою переривань), аналізом функціональних покажчиків, іншими примітивами синхронізації і ін. Цікаво, що таких проблем, пов'язаних з неточністю підходу, як були в задачах SV-COMP, в модулях операційної системи Linux не спостерігається. Це підтверджує припущення, що завдання SV-COMP є занадто штучними, по крайней мере в категорії багатопоточних завдань (Concurrency).

    З 24 повідомлень про можливий стан гонки 14 були підтверджені розробниками, для 8 не було отримано зворотної відповіді, і тільки в двох випадках знайдена гонка була визнана недосяжною через апаратної синхронізації пристрою. Однак більшість справжніх помилок були знайдені в «древніх» драйвери, а їх виправлення не є актуальним завданням. Тільки 4 виправлення з 14 були включені в основну гілку розробки ядра.

    Результати експериментів дозволяють стверджувати, що вдалося успішно інтегруватися з іншими техніками аналізу, які доступні у фреймворку CPAchecker. Такі підходи, як CEGAR, можуть бути застосовані з мінімальною кількістю змін технічного характеру. Деякі реалізації конкретних видів аналізу можуть бути використані без модифікацій (AutomatonCPA) або з мінімальними змінами в коді (CallstackCPA). Для деяких існуючої техніки аналізу (PredicateCPA, ValueCPA, CompositeCPA) була реалізована підтримка операцій над ефектами оточення, при цьому основна функціональність аналізу залишилася без змін. Зміни параметрів роботи інструменту (варіантів аналізу) досягається лише опцією запуску, тобто збирати заново інструмент не потрібно.

    З результатів видно, що для різних цілей може бути використані різні варіанти роботи інструменту: для невеликих завдань, типу SV-COMP, необхідні більш точні підходи. Для прикладних задач, типу драйверів, можуть бути корисні менш точні варіанти аналізу, щоб мати можливість отримати деяку оцінку коректності. Разом з тим, більш точні підходи, можуть застосовуватися для глибокої верифікації, яка вимагає певних ресурсів.

    15. Огляд схожих робіт

    Існуючі підходи до аналізу многопоточного програмного забезпечення мають різні властивості і продуктивність. З одного боку, існують точні підходи, які можуть довести коректність програм при деяких певних припущеннях. Починаючи з ограничиваемой перевірки моделей, більшість підходів докладають значних зусиль для оптимізації обходу простору станів програми. Прикладами таких оптимізацій можуть стати редукція часткових порядків [1], обмеження контексту [24, 25], та ін.

    Спробою абстрагуватися від нерелевантного оточення є підхід з роздільним аналізом потоків (thread-modular approach), який вперше був запропонований в [7]. Ця версія ще не використала жодної абстракцію. Підхід з роздільним аналізом потоків для формальної верифікації був представлений в [26]. Основна ідея була в пошуку інваріантів для кожного процесу, з яких потім має слідувати перевіряється властивість. Оцінка підходу проводилася для двох протоколів взаємного виключення. Предикатна абстракція була додана до цього підходу в [27]. Основною відмінністю було те, що розглядався тільки один потік з кількох копій. Тому оточення формувалося цим же потоком. При цьому ніякі примітиви синхронізації не розглядалися.

    Розширення підходу з роздільним аналізом потоків, яке використовує абстракцію, був представлений в [28] і потім реалізований в інструменті TAR [8]. Описаний в даній статті підхід має ряд відмінностей:

    TAR розглядає примітиви синхронізації, як звичайні змінні. Запропонований метод використовує спеціальний аналіз блокувань, який може застосовуватися спільно з іншими варіантами аналізу. Це дозволяє уникати зайвих ітерацій уточнення абстракції.

    TAR застосовує ефекти потоку, які безпосередньо отримані з операторів програми. CPALockator надає можливість абстракції (оператор elP) і об'єднання (оператор merge) різних переходів. Це може дозволяє вибирати баланс між швидкістю аналізу і його точністю.

    TAR підтримує фіксовану кількість потоків, в той час як запропонований метод теоретично підтримує необмежену кількість потоків. Для побудови оточення TAR використовує апроксимацію знизу, а запропонований метод - апроксимацію зверху.

    Схожий підхід також був реалізований в інструменті Threader [29]. Цей інструмент використовує апроксимацію зверху для побудови оточення, засновану на диз'юнкт Хорна. Також як і в інструменті CPALockator, Threader може шукати модульні докази, але при цьому він може шукати і немодульность, в яких враховуватись повної взаємодія між потоками.

    Існують різні техніки трансформації паралельної програми в послідовну (англ. Sequentialization) для подальшої перевірки її звичайними інструментами статичної верифікації [30-32]. Один із прикладів є WHOOP [33], який використовує цю техніку трансформації і не враховує взаємодію потоків. Більш того, він сильно використовує алгоритм Lockset і не може бути розширений 228

    якимись іншими аналізами. Він застосовується в якості преданаліза для більш точного інструменту CORALL [34].

    З іншого боку, існують безліч легковажних підходів, які можуть застосовуватися до величезного обсягу коду. Такі техніки визначаються слабкими вимогами до ресурсів і низькою точністю. Прикладами є RELAY [35] і Locksmith [36], які застосовувалися для аналізу коду операційної системи Linux. RELAY знайшов кілька тисяч попереджень, що вимагало застосування неточних фільтрів для скорочення цієї кількості. Цей інструмент взагалі не враховує взаємодію потоків.

    Інструмент Locksmith, навпаки, враховує точки створення потоків, але не може точно визначити колективні дані і способи взаємодії потоків. Він обчислює загальний ефект від потоку. У термінах представленої теорії використовується оператор merge, який об'єднує всі переходи в оточенні в один. При цьому експериментальна оцінка Locksmith показала, що він має проблеми з масштабністю. В [37] автори представили розширення аналізу алиасов Андерсена на випадок багатопоточних програм. Ідея був схожа на підхід з роздільним аналізом потоків, так як обчислювалося безліч операторів, яке могло виконуватися паралельно, а потім ці оператори застосовувалися до інших потокам.

    Також існують різні підходи для пошуку станів гонки в специфічному програмному забезпеченні. Наприклад, в низкоуровневом програмному забезпеченні з вкладеними переривань [38], пошук гонок у FreeRTOS [39, 40]. А також станів гонки спеціального виду - використання пам'яті після її звільнення (англ. Use-after-free) в драйверах пристроїв операційної системи Linux. Такі підходи показують досить хороші результати, але значно використовують специфіку вихідного коду або перевіряється властивості. Представлений в даній статті теоретичний підхід претендує на те, щоб бути більш загальним, проте це не скасовує того факту, що він може бути також покращено при використанні додаткової інформації про вихідний код або перевіряється властивості.

    16. Висновок

    У роботі представлений підхід до практичного пошуку станів гонки в складному програмному забезпеченні. Була розширена теорія CPA і реалізована в новому інструменті. Експерименти показали переваги підходу на великих верифікаційних завданнях перед існуючими техніками статичної верифікації. Невеликі завдання зі складною взаємодією потоків краще вирішуються іншими інструментами, так як запропонований підхід абстрагується від такої взаємодії. Однак наш підхід також не пропускає помилок (при деяких припущеннях) і може бути розвинений в майбутньому.

    Таким чином, можна зробити висновок, що основні вимоги до нового інструменту були виконані, тому що він успішно застосовується до різних програмних систем, в тому числі, до драйверів ОС Linux. Так само, як і в класичних методах статичної верифікації, може бути отримана гарантія відсутності помилок при виконанні зазначених припущень: вимог на оператори CPA і умов коректного розбиття на непересічні регіони BnB моделі.

    Запропонована теорія дозволяє описувати досить складні варіанти аналізу, в тому числі і ті, які не включаються до поняття аналізу з роздільним розглядом потоків. Проте, ця теорія не вичерпує всіх можливих підходів, і для ефективного опису масштабується підходу з частковим обчисленням чергувань буде потрібно її розширення. Однак, ця тема виходить за рамки даної статті.

    Одним з можливих напрямків розвитку підходу є додавання взаємодії потоків, можливо, не в повному обсязі, щоб зберегти масштабованість. Це може бути окремий аналіз CPA, який буде динамічно налаштовувати свою точність за допомогою алгоритму CEGAR, забезпечуючи певний проміжний варіант між підходом з роздільним аналізом потоків і перебором чергувань.

    Іншим можливим поліпшенням інструменту може стати інтеграція його з іншим підходом. Наприклад, комбінація швидкого підходу з роздільним аналізом потоків в якості першого етапу, а потім класичний великоваговий аналіз - на другому етапі. Це може бути реалізовано відповідно до ідеї кооперативної верифікації [42]. Ще одним можливим напрямком розвитку підходу є побудова реального шляху з чергуванням потоків на основі шляху з застосованими ефектами оточення. Цей шлях був би корисний для дослідження і уточнення абстракції.

    Список літератури / References

    [1]. Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. SIGPLAN Notices, vol. 49, issue 1, 2014 року, pp. 373-384.

    [2]. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag, Berlin, Heidelberg, 1996, 143 p.

    [3]. Gerard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening. Symbolic counter abstraction for concurrent software. Lecture Notes in Computer Science, vol. 5643, 2009 pp. 64-78.

    [4]. Dirk Beyer. Automatic verification of C and Java Programs: SV-COMP. Lecture Notes in Computer Science, vol. 11429, 2019, pp. 133-155.

    [5]. Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz. Configurable software verification: concretizing the convergence of model checking and program analysis. Lecture Notes in Computer Science, vol. 4590, 2007, pp. 504-518

    [6]. D. Beyer, T.A. Henzinger, and G. Theoduloz. Program analysis with dynamic precision adjustment. In Proc. of the 23rd IEEE / ACM International Conference on Automated Software Engineering, 2008, pp. 29-38.

    [7]. Cormac Flanagan and Shaz Qadeer. Thread-modular model checking. Lecture Notes in Computer Science, vol. 2648, 2003 pp. 213-224.

    [8]. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-Modular Abstraction Lecture Notes in Computer Science, vol. 2725, 2003 pp, 262-274.

    [9]. Byron Cook, Daniel Kroening, and Natasha Sharygina. Verification of Boolean programs with unbounded thread creation. Theoretical Computer Science, vol. 388, issue 1-3, 2007, pp. 227-242.

    [10]. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 412-417.

    [11]. E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. Lecture Notes in Computer Science, vol. 1855, 2000., pp. 154-169.

    [12]. Susanne Graf and Hassen Saidi. Construction of abstract state graphs with PVS. Lecture Notes in Computer Science, vol. 1254, 1997, pp. 72-83.

    [13]. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM SIGOPS Operating Systems Review, vol. 31, issue 5, 1997, pp. 27-37.

    [14]. Richard Bornat. Proving pointer programs in Hoare logic. Lecture Notes in Computer Science, vol. 1837 2000, pp. 102-126.

    [15]. R M Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, vol. 7, 1972, pp. 23-50.

    [16]. Pavel Andrianov, Karlheinz Friedberger, Mikhail Mandrykin, Vadim Mutilin, and Anton Volkov. CPA-BAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. Lecture Notes in Computer Science, vol. 10206 2017, pp. 355-359.

    [17]. Evgeny Novikov and Ilja Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402-416.

    [18]. Evgeny Novikov and Ilja Zakharov. Verification of operating system monolithic kernels without extensions. Lecture Notes in Computer Science, vol. 11247, 2018, pp. 230-248.

    [19]. Dirk Beyer and Karlheinz Friedberger. In Proc. of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2016, pp. 61-71.

    [20]. Dirk Beyer and Stefan Lowe. Explicit-state software model checking based on CEGAR and interpolation. Lecture Notes in Computer Science, vol. 7793, 2013, pp. 146-162.

    [21]. D. Beyer, M.E. Keremoglu, and P. Wendler. Predicate abstraction with adjustable-block encoding. In Proc. of 10th International Conference on Formal Methods in Computer-Aided Design 2010, pp. 189197.

    [22]. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without bdds. Lecture Notes in Computer Science, vol. Тисяча п'ятсот сімдесят дев'ять, 1999, pp. 193-207

    [23]. Dirk Beyer, Stefan Lowe, and Philipp Wendler. Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer, vol. 21, issue 1, 2019, pp. 1-29.

    [24]. Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. Lecture Notes in Computer Science, vol. 3440, 2005, pp. 93-107.

    [25]. Lucas Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer. Context-bounded model checking with esbmc 1.17. Lecture Notes in Computer Science, vol. 7214, 2012 pp. 534-537.

    [26]. Ariel Cohen and Kedar S. Namjoshi. Local proofs for global safety properties. Formal Methods in System Design, vol. 34, issue 2, 2009 pp. 104-125.

    [27]. Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In Proc. of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, 2004, pp. 1 -13.

    [28]. Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular verification is cartesian abstract interpretation. Lecture Notes in Computer Science, vol. 4281, 2006, pp. 183-197.

    [29]. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. ACM SIGPLAN Notices, vol. 46, issue 1m 2011, pp. 331-344.

    [30]. Akash Lal and Thomas Reps. Reducing concurrent analysis under a context bound tosequential analysis. Formal Methods in System Design, vol. 35, issue 1, 2009 pp. 73-97.

    [31]. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Reducing context-bounded concurrent reachability to sequential reachability. Lecture Notes in Computer Science, vol. 5643, 2009 pp. 477492.

    [32]. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. MU-CSeq: Sequentialization of C programs by shared memory unwindings. Lecture Notes in Computer Science, vol. 8413, 2014 року, pp. 402-404.

    [33]. Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. Fast and precise symbolic analysis of concurrency bugs in device drivers (t). In Proc. of the 2015 30th IEEE / ACM International Conference on Automated Software Engineering (ASE), 2015-го, pp. 166-177.

    [34]. Akash Lal, Shaz Qadeer, and Shuvendu K. Lahiri. A solver for reachability modulo theories. Lecture Notes in Computer Science, vol. 7358, 2012 pp. 427-443.

    [35]. Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. RELAY: Static race detection on millions of lines of code. In Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, 2007, pp. 205-214.

    [36]. Polyvios Pratikakis, Jeffrey S. Foster, and Michael Hicks. LOCKSMITH: Context-sensitive correlation analysis for race detection. In Proc. of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2006, pp. 320-331.

    [37]. Peng Di and Yulei Sui. Accelerating dynamic data race detection using static thread interference analysis. In Proc. of the 7th International Workshop on Programming Models and Applications for Multicores and Manycores, 2016, pp. 30-39.

    [38]. Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael Tautschnig. Effective verification of low-level software with nested interrupts. In the Europe Conference & Exhibition on Design, Automation & Test, 2015-го, pp. 229-234.

    [39]. Suvam Mukherjee, Arun Kumar, and Deepak D'Souza. Detecting all high-level dataraces in an RTOS kernel. Lecture Notes in Computer Science, vol. 10145 2017, pp. 405-423.

    [40]. Nikita Chopra, Rekha Pai, and Deepak D'Souza. Data races and static analysis for interrupt-driven kernels. Lecture Notes in Computer Science, vol. 11423, 2019, pp. 697-723.

    [41]. Jia-Ju Bai, Julia Lawall, Qiu-Liang Chen, and Shi-Min Hu. Effective static analysis of concurrency use-after-free bugs in Linux device drivers. In the USENIX Annual Technical Conference, 2019, pp. 255-268.

    [42]. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. Reducer-based construction of conditional verifiers. In Proceedings of the 40th International Conference on Software Engineering, 2018, pp. 1182-1193.

    Інформація про авторів / Information about authors

    Павло Сергійович АНДРІАНОВ - молодший науковий співробітник. Сфера наукових інтересів: статична верифікація, аналіз багатопоточних програм.

    Pavel Sergeevich ANDRIANOV - junior researcher. Research interests: software model checking, analysis of multithreaded software.


    Ключові слова: СТАН ПЕРЕГОНИ /РОЗДІЛЬНИЙ АНАЛІЗ ПОТОКІВ /СТАТИЧНА ВЕРИФІКАЦІЯ /ОПЕРАЦІЙНА СИСТЕМА LINUX /DATA RACE /THREAD-MODULAR APPROACH /SOFTWARE VERIFICATION /LINUX KERNEL

    Завантажити оригінал статті:

    Завантажити