--- date: Jun 28, 2026 author: José Ruiz tags: embedded, certification, multicore --- # Сертифікація багатоядерних систем за допомогою Ada > Хосе Ф. Руїс, червень 2026, CC-BY 4.0. > [Джерело](https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.AEiC.2026.3). ---- > ## Анотація > Впровадження багатоядерних процесорів у критично важливих для > безпеки системах, таких як авіоніка, автомобілебудування та > залізничний транспорт, створює значні виклики для сертифікації, > пов'язані насамперед із детермінізмом, передбачуваністю та > керуванням інтерференцією. У цій статті розглядається, як мова > програмування Ada разом із її обмеженими профілями задач (Ravenscar > і Jorvik) та бібліотеками часу виконання на «голому залізі» > забезпечує надійну та придатну до сертифікації модель виконання для > багатоядерних систем, що відповідає таким настановам, як AC 20-193. > > Шляхом застосування статичного розподілу задач, планування з > фіксованим пріоритетом та простої моделі синхронізації, підхід Ada > систематично обмежує канали інтерференції та часову > нестабільність. Ця модель дозволяє проводити точний аналіз > планованості, спрощує заходи з верифікації та дає змогу > сертифікувати як саму багатоядерну бібліотеку часу виконання, так і > побудований на її основі застосунок. ---- ## Вступ Використання багатоядерного обладнання в критично важливих для безпеки системах стає дедалі актуальнішим. Через збільшення складності програмного забезпечення та вищі вимоги до продуктивності виникає потреба в додатковій обчислювальній потужності, тоді як застаріле обладнання робить одноядерні процесори дедалі рідкіснішими. Тому вбудовані системи реального часу, подібно до обчислень загального призначення, переходять на багатоядерні архітектури. Проте в системах з високим рівнем цілісності такий перехід вимагає збереження критичних властивостей: детермінізму, передбачуваності та придатності до аналізу. На початку 2010-х років розробники авіоніки почали впроваджувати багатоядерні процесори, керуючись потребами у продуктивності та необхідністю модернізації. На той час методи розробки та сертифікаційні настанови були розраховані переважно на одноядерні архітектури. Ані органи сертифікації, ані заявники не мали узгодженої методології для вирішення проблем, притаманних багатоядерним процесорам: конкуренції за спільні ресурси, часової інтерференції та ефектів паралельного виконання. Першою вагомою спробою подолати ці виклики став CAST-32A. Він містив рекомендації щодо стійкості до перешкод та аналізу синхронізації на багатоядерних платформах. Згодом ці зусилля лягли в основу Консультативного циркуляра AC 20-193 (2024 р.) — першої комплексної регуляторної бази для сертифікації багатоядерних систем, яка доповнює стандарти DO-178C, DO-254 та ARP4754A. Мова програмування Ada особливо добре підходить для розробки критично важливого для безпеки вбудованого програмного забезпечення. У 2005 році Ada представила профіль Ravenscar . Це обмежена підмножина моделі задач, створена для підтримки детермінованих, придатних до аналізу у часі програм на базі оптимізованого середовища виконання. Спочатку розрахований на одноядерні процесори, Ravenscar виявився надзвичайно ефективним для створення сертифікованих систем реального часу. Ada 2012 розширила цю модель на багатоядерні архітектури, застосувавши підхід повного розділення, що зберіг простоту та придатність до аналізу Ravenscar. Згодом, у 2022 році, з'явився профіль Jorvik, який послабив деякі обмеження Ravenscar та додав прив'язку захищених об'єктів до процесора. У цій статті аналізується, як ці мовні можливості та модель виконання задач допомагають дотримуватися суворих вимог багатоядерної сертифікації, з особливим акцентом на стандарті AC 20-193 ## Проблеми багатоядерної сертифікації Сертифікація програмного забезпечення в аерокосмічній галузі — це офіційний процес, за допомогою якого авіаційні органи встановлюють впевненість у тому, що програмне забезпечення для літаків є безпечним, надійним та відповідає нормативним вимогам. Оскільки програмне забезпечення виконує критично важливі функції контролю та моніторингу, цілі сертифікації наголошують на детермінізмі, правильності та відсутності ненавмисної поведінки. DO-178C визначає набір цілей та дій для демонстрації правильної поведінки програмного забезпечення за будь-яких операційних умов. Центральними для цих цілей є поняття передбачуваності, контрольованої складності та поведінки, яку можна перевірити заздалегідь. Усю поведінку програмного забезпечення необхідно визначити, переглянути та верифікувати, а властивості часу виконання — обґрунтувати, де це доречно. Сертифікація програмного забезпечення на багатоядерних процесорах є значно складнішою, ніж на одноядерних системах. На багатоядерних платформах кілька процесорів виконуються паралельно та конкурують за спільні апаратні ресурси, такі як шини пам'яті, кеші та контролери вводу/виводу. Таке спільне використання спричиняє часову нестабільність та ефекти інтерференції, які можуть поставити під загрозу детермінізм. AC 20-193 формалізує ці проблеми через концепцію **каналів інтерференції** — механізмів, за допомогою яких активність на одному процесорі може впливати на часові характеристики або поведінку програмного забезпечення, що виконується на іншому. Багато таких каналів зароджуються глибоко в мікроархітектурі апаратного забезпечення. Ними неможливо безпосередньо керувати на рівні програмного забезпечення, що ускладнює їх точне моделювання чи аналіз. Як наслідок, традиційних методів аналізу для одноядерних систем, де задачі здебільшого розглядаються ізольовано, стає недостатньо. Тепер для сертифікації необхідно надати докази того, що система зберігає стійкість навіть за найгірших умов інтерференції. Це означає, що часові та функціональні вимоги мають виконуватися, навіть коли всі процесори активні та конкурують за спільні ресурси. Кандидатам необхідно: * визначити всі потенційні канали інтерференції, * охарактеризувати найгірші сценарії конкуренції за ресурси, * впровадити стратегії пом'якшення впливу інтерференції та * надати результати верифікації або вимірювань, що підтверджують ефективність цих стратегій. Досягнення цих цілей вимагає дисциплінованої моделі виконання, глибокого розуміння апаратної платформи та програмних абстракцій, що мінімізують інтерференцію. Без таких заходів встановлення надійних меж часу виконання для найгіршого випадку стає непрактичним. ## Підхід Ada до безпеки багатоядерних систем Підхід, представлений у цій статті, використовує мову програмування Ada та сертифіковану бібліотеку часу виконання на «голому залізі» (bare-metal) для визначення простої статичної моделі виконання для багатоядерних систем, яка відповідає цілям AC 20-193. Модель характеризується такими принципами: * **Статичний розподіл задач:** задачі статично прив'язані до процесорів, міграція задач заборонена. * **Планування з фіксованим пріоритетом:** кожен процесор використовує планувальник з випередженням та фіксованим пріоритетом без квантування часу. Найпріоритетніша готова задача на кожному процесорі виконується, доки вона не заблокується або не буде випереджена. * **Незалежні планувальники:** кожен процесор підтримує власні черги готовності та затримки. * **Детермінована синхронізація:** для міжпроцесорного та внутрішньопроцесорного зв'язку використовуються захищені об'єкти на рівні бібліотеки. * **Статична обробка переривань:** кожне зовнішнє апаратне переривання статично призначається конкретному процесору; різні переривання можуть бути призначені різним процесорам (див. розділ 4.5). Обробники переривань використовують механізми синхронізації захищених об'єктів для запуску дій на іншому процесорі, коли це потрібно. * **Служби таймінгу високої роздільної здатності:** єдиний апаратний годинник забезпечує спільний орієнтир часу. Обробка затримок за потреби програмує таймери високої роздільної здатності. Цей підхід безпосередньо вирішує питання, порушені в AC 20-193, шляхом обмеження динамічної поведінки, зменшення та виявлення каналів інтерференції, а також забезпечення точного аналізу часових характеристик. ### Модель виконання та планування Профілі Ravenscar та Jorvik визначають детерміновані та придатні до аналізу моделі виконання, що підтримуються системами часу виконання зменшеного розміру та складності. Ці моделі дозволяють проводити точний аналіз планування за допомогою таких усталених методів, як аналіз швидкості та монотонності (RMA) та аналіз часу відгуку (RTA). Ada 2012 запровадила багатоядерну модель виконання як консервативне розширення одноядерного превентивного планування з фіксованим пріоритетом. Задачі статично розподіляються між процесорами, міграція заборонена, і кожен процесор незалежно планує свою чергу готовності. Такий розділений підхід дозволяє повторно використовувати методи одноядерного аналізу та спрощує підтримку під час виконання, зберігаючи при цьому планованість. Статичне розділення забезпечує фізичну та часову ізоляцію між ядрами, зменшуючи інтерференцію та підтримуючи вимоги до детермінізму AC 20-193. Хоча обидва профілі мають однакову фундаментальну модель виконання (статичні задачі, фіксовані пріоритети та захищені об'єкти на рівні бібліотеки), вони відрізняються обмеженнями синхронізації. Ravenscar обмежує кожен захищений об'єкт максимум одним входом із простим логічним бар'єром (одна булева змінна або атрибут), що дозволяє здійснювати простий аналіз планування. Jorvik послаблює ці обмеження, дозволяючи кілька захищених входів та загальні логічні бар'єри для кожного захищеного об'єкта, зберігаючи при цьому властивість обмеженого блокування (bounded-blocking), необхідну для аналізу часових характеристик. ### Сертифікована архітектура бібліотеки часу виконання У цій статті йдеться зокрема про бібліотеку середовища виконання GNAT Ada, розроблену компанією AdaCore для вбудованих програм на «голому залізі». Це середовище виконання розвивалося протягом багатьох років для підтримки різних цільових платформ; підтримку багатоядерності було додано у 2010 році для Ada 2012, і відтоді вона постійно вдосконалюється. Бібліотека виконання Ada складається з пасивних пакетів, тобто її код виконується лише у відповідь на явні виклики програми або зовнішні події, як-от переривання. Вона надає фундаментальні послуги, необхідні для підтримки програм на Ada, зокрема роботу з задачами та синхронізацію. Бібліотека виконання статично компонується з вбудованим виконуваним файлом, тому має бути сертифікована на той самий рівень гарантії, що й програма. Вона підтримує конфігурацію симетричної багатопроцесорності (SMP), де існує одна копія бібліотеки виконання, а вся пам'ять доступна для адресації будь-яким процесором. Ядро системи виконання, що реалізує обмежену модель задач, складається приблизно зі 100 пакетів на Ada загальним обсягом близько 11 тис. рядків коду (KSLOC) із середньою цикломатичною складністю 2,57. Додатково воно містить приблизно 1000 рядків асемблерного коду, специфічного для архітектури. Ці показники відповідають бібліотеці виконання GNAT Pro, що підтримує профілі Ravenscar та Jorvik для Ada 2022. ### Одноядерна та багатоядерна конфігурація Бібліотека виконання для багатоядерних систем походить безпосередньо від уже сертифікованої версії бібліотеки для одноядерних систем та вносить лише мінімальний набір змін. При конфігурації системи виконання задається максимальна кількість процесорів за допомогою статичної константи. Коли значення константи дорівнює одиниці, всі шляхи коду, специфічні для багатопроцесорних систем, статично вимикаються та оптимізуються компілятором. В результаті, згенерований бінарний файл для одноядерних систем не містить жодної багатоядерної функціональності. Наприклад, операція синхронізації може містити такий код, як: ```ada if Multiprocessor then Fair_Locks.Lock (Any_Lock); end if ; ``` де умова багатопроцесорності визначається як: ```ada Multiprocessor : constant Boolean := Max_Number_Of_CPUs /= 1; ``` Тут Max_Number_Of_CPUs — це параметр конфігурації, що представляє максимальну кількість процесорів, доступних на цільовій платформі. Така архітектура забезпечує використання спільної кодової бази для одноядерних та багатоядерних систем виконання, причому відмінності обмежуються лише 15 умовними конструкціями. Більшість коду середовища виконання є ідентичною в обох конфігураціях, що дає змогу максимально повторно використовувати артефакти верифікації та сертифікації, зокрема дані структурного покриття та низькорівневі докази верифікації. Це значно спрощує відповідність стандартам, таким як DO-178C, ISO 26262 та EN 50128, а також полегшує технічне обслуговування. ## Деталі впровадження У цьому розділі описано конкретну реалізацію багатоядерної моделі виконання в середовищі Ada для вбудованих систем. Основна увага приділяється запуску системи, активації задач, плануванню та координації між процесорами. Архітектура розроблена для мінімізації складності та обмеження динамічної поведінки. Вона забезпечує чітку відповідність між програмними абстракціями та апаратною платформою, що значно спрощує процес верифікації та сертифікації. ### Ініціалізація Ініціалізація системи координується процесором призначеним для початкового завантаження, щоб уникнути умов гонки. Після запуску цей процесор виконує низькорівневий асемблерний код запуску, відповідальний за ініціалізацію загального обладнання. Процесор початкового завантаження спочатку ініціалізує основні апаратні регістри та налаштовує рівень виконання для роботи в привілейованому режимі, відкриваючи необмежений доступ до регістрів керування. Потім він активує лише мінімальний набір апаратних функцій, необхідних для застосунку, як-от модуль обчислень з плаваючою комою (якщо він використовується) та механізми обробки пасток і винятків. Далі йде ініціалізація пам'яті: налаштування кешу та MMU (де це можливо), заповнення нулями розділу .bss, ініціалізація глобальних даних та налаштування головного вказівника стека. Після ініціалізації пам'яті та стану процесора система часу виконання створює внутрішні керуючі структури задач. Задачі статично призначаються процесорам згідно з параметрами конфігурації, і кожна задача додається до черги готовності свого статично призначеного процесора. Якщо цього вимагає застосунок, на цьому етапі ініціалізуються периферійні пристрої: системні годинники, таймери та UART-контролери. Встановлюються всі налаштовані обробники переривань, зокрема ті, що відповідають за закінчення часу таймера та міжпроцесорний зв'язок. Нарешті, керування передається задачі середовища, яка представляє початковий контекст виконання застосунку. ### Ініціалізація вторинного процесора Після того, як процесор початкового завантаження завершує глобальну ініціалізацію, решта процесорів виходять зі стану скидання (reset) і виконують спрощену послідовність ініціалізації. Кожен вторинний процесор виконує лише локальне налаштування, наприклад, ініціалізацію стека та необхідне маскування переривань. Вторинні процесори не виконують глобальну ініціалізацію обладнання, що дозволяє уникнути дублювання зусиль і виключає ризик виникнення умов гонки під час запуску. Натомість вони одразу переходять до циклу диспетчеризації задач. Кожен процесор містить статично визначену *задачу простою*, реалізовану як цикл низького енергоспоживання з очікуванням переривання. Ця задача простою має найнижчий пріоритет і виконується тоді, коли на процесорі немає інших готових задач. Задача простою не є частиною моделі планування застосунку і слугує лише для утримання процесора у стані очікування. ### Розподіл та планування задач Задачі статично розподіляються між процесорами за допомогою аспекту CPU, який визначає, на якому процесорі задача буде активована та виконуватися. Якщо цей аспект не вказано або якщо значення CPU дорівнює Not_A_Specific_CPU, задачу призначають на перший процесор. Кожен процесор використовує незалежний планувальник із фіксованим пріоритетом та витисканням. Черги готовності є локальними для кожного процесора та не перетинаються, а задачі диспетчеризуються суворо відповідно до їхнього пріоритету. Коли задача блокується або витискається, вона повертається до черги готовності свого призначеного процесора. Не існує механізму, який дозволив би задачі потрапити до черги готовності іншого процесора. Якщо задачі на різних процесорах змінюють внутрішні дані системи виконання, взаємовиключний доступ гарантують механізми міжпроцесорного блокування. Виконання задачі (або обробника переривань) на одному процесорі може вимагати оновлення черги готовності іншого процесора (і може навіть спричинити витіснення поточної задачі). Такі міжпроцесорні оновлення виконуються опосередковано: цільовому процесору надсилається міжпроцесорне переривання (IPI), після чого він самостійно виконує оновлення власних структур даних локально. Це підтримує інваріант, за яким кожен процесор є єдиним, хто може змінювати власну чергу готовності. ### Детермінована синхронізація Обмежені захищені об'єкти на рівні бібліотеки, визначені профілями Ravenscar та Jorvik, використовуються для міжпроцесорного та внутрішньопроцесорного зв'язку і синхронізації. Ті самі обмеження, що діють у профілях Ravenscar та Jorvik для одноядерних систем, застосовуються і до багатопроцесорних випадків. У багатоядерних системах захищені об'єкти покладаються на механізм «справедливого блокування» (Fair Lock), що забезпечує обмежене блокування та передбачуваний порядок доступу. Реалізація справедливого блокування гарантує, що отримання доступу є скінченним та здатним до аналізу процесом, що запобігає «голодуванню» (starvation) та підтримує аналіз часу виконання для найгіршого випадку. Справедливе блокування (Fair Lock) підтримує чергу FIFO для запитів, що очікують: кожній спробі отримання доступу присвоюється «квиток», а процесори отримують доступ відповідно до черги цих квитків. Це гарантує, що будь-який процесор, що очікує, отримає блокування протягом обмеженої кількості критичних секцій інших процесорів. Завдяки цьому час блокування для найгіршого випадку можна статично обчислити як B = (n − 1) · Ccs, де n — кількість процесорів, а Ccs — максимальний час виконання критичної секції. Операції блокування мають мінімальні накладні витрати та викликаються лише у чітко визначених точках синхронізації, що узгоджується з моделлю обмежених задач. Міжпроцесорний зв'язок обмежений явними операціями синхронізації та міжпроцесорними перериваннями, які використовуються для запуску перепланування на цільовому процесорі. Щоб спростити аналіз синхронізації та, де це можливо, забезпечити ефективну реалізацію, захищені об'єкти, до яких звертаються лише задачі в межах одного процесора, можуть використовувати оптимізовану одноядерну реалізацію. Ada 2022 запроваджує прив'язку захищених об'єктів до процесора (CPU affinity) (ALRM, D.16(15/5)), що дозволяє статично оптимізувати виконання захищених операцій. Захищені об'єкти, не прив'язані до конкретного процесора (тобто ті, до яких звертаються задачі з різних процесорів), покладаються на механізм «справедливого блокування». Це забезпечує взаємовиключний доступ між процесорами. Прив'язка захищеного об'єкта до того самого процесора, що й задачі-клієнти, усуває потребу в міжпроцесорній синхронізації. Глобальні захищені об'єкти, до яких звертаються задачі з різних процесорів, використовуються лише тоді, коли потрібна явна міжпроцесорна взаємодія, і їх застосування зумовлює накладні витрати на синхронізацію, про які йшлося раніше. ### Модель обробки переривань У системах, сумісних з Ravenscar та Jorvik, єдиним механізмом пов'язування коду обробки переривань на рівні застосунку є приєднання захищеної процедури до переривання. У багатопроцесорному контексті фундаментальна семантична модель залишається незмінною, проте виникають додаткові аспекти, пов'язані з взаємовиключним доступом та призначенням переривань процесорам. Взаємовиключний доступ для обробників переривань забезпечується семантикою захищених об'єктів, визначеною в Ada. Як наслідок, ті самі принципи проектування та обмеження, що застосовуються до внутрішньо- та міжпроцесорної синхронізації захищених операцій, рівною мірою стосуються і обробки переривань. Зокрема, уникнення непотрібної міжпроцесорної синхронізації є критично важливим для підвищення детермінізму та здатності до аналізу. Багатоядерне обладнання зазвичай дозволяє доставляти переривання одному або кільком процесорам шляхом налаштування масок спорідненості переривань. Хоча динамічна або багатоядерна доставка переривань може покращити середню швидкість реагування в системах загального призначення, вона значно ускладнює аналіз часових характеристик і створює додаткові джерела інтерференції через спільні шляхи обробки переривань та міжпроцесорну синхронізацію. Тому, для систем з високою цілісністю та відповідно до цілей AC 20-193, переривання статично призначаються одному процесору. Кожне переривання обробляється рівно одним процесором протягом усього терміну служби програми, хоча різні переривання можуть бути призначені різним процесорам. Такий підхід усуває міграцію переривань, запобігає конкуренції між процесорами за їх обробку та гарантує, що інтерференція, пов'язана з перериваннями, залишається локальною виключно для того процесора, якому призначено переривання. Крім того, призначення переривань тому самому процесору, де виконуються задачі, що використовують відповідні пристрої (використовуючи механізм прив'язки до процесора з Ada 2022 для захищених об'єктів), усуває необхідність міжпроцесорної синхронізації під час доступу до спільних даних. Така архітектура скорочує кількість каналів інтерференції, спрощує аналіз часу виконання та часу відгуку для найгіршого випадку, а також підтримує надійний розподіл між процесорами. Загалом, ця модель обробки переривань безпосередньо підтримує цілі AC 20-193 щодо детермінізму, стримування інтерференції та аналізованості завдяки забезпеченню статичного розподілу переривань, усуненню динамічних змін прив'язки до CPU та мінімізації міжпроцесорної взаємодії. ## Служби визначення часу Служби визначення часу мають бути передбачуваними, придатними до аналізу та стійкими до інтерференції. Середовище виконання Ada використовує апаратні таймери та статичні програмні структури, що обмежує використання спільних ресурсів та дозволяє уникнути динамічної поведінки. Цей підхід базується на визначених принципах і адаптується до можливостей апаратного забезпечення. #### Розділені черги затримок Черги затримок ведуться окремо для кожного процесора. Кожна черга містить події з часовими обмеженнями (затримки задач та зворотні виклики подій часу), впорядковані за абсолютним часом закінчення. Тільки задачам та обробникам, що виконуються на конкретному процесорі, дозволено додавати або видаляти записи з черги затримок цього процесора. Коли виникає переривання таймера, перша подія видаляється з черги, а таймер перепрограмовується для наступної затримки. З моменту свого створення середовище виконання GNAT Ada використовувало таймер одноразової дії (single-shot timer), що генерує переривання в момент закінчення часу очікування першої події. Така архітектура усуває потребу в багатопроцесорному захисті, зменшує складність і, що важливіше, обмежує інтерференцію між процесорами. #### Реалізації таймерів процесора На платформах, що забезпечують окремий фізичний таймер для кожного процесора (наприклад, 64-бітні архітектури Arm), кожен процесор незалежно програмує свій апаратний таймер, базуючись виключно на своїй локальній черзі затримок. Оскільки стан таймера реплікується для кожного процесора, під час встановлення або оновлення таймерних подій міжпроцесорна синхронізація не потрібна. Для захисту від паралельного доступу з боку задач, що виконуються на одному й тому самому процесорі, використовується лише локальне маскування переривань. Це усуває цілий клас каналів інтерференції, пов'язаних зі спільним обладнанням для вимірювання часу, і безпосередньо підтримує цілі AC 20-193 щодо зменшення інтерференції. Така реалізація одноразового таймера для кожного процесора доступна на платформах, що надають спеціалізоване апаратне забезпечення таймера для кожного ядра. Наприклад, на 64-бітних процесорах ARM це реалізовано за допомогою розширення архітектури Generic Timer. Платформи, на яких відсутні таймери для кожного процесора, потребують реалізації спільного таймера, описаної в наступному розділі. #### Реалізації спільних таймерів Деякі архітектури, як-от LEON3MP, забезпечують єдиний апаратний таймер, спільний для всіх процесорів. У цій конфігурації потрібні додаткові заходи для забезпечення безпечної роботи. Під час встановлення таймерних подій середовище виконання захищає доступ до стану спільного таймера за допомогою багатопроцесорних блокувань і обчислює найближчий термін дії для всіх процесорів перед перепрограмуванням апаратного таймера: ```ada procedure Update_Alarm (Alarm : Time) is Now : Time; Time_Difference : Time; begin if Multiprocessor then Lock (Alarm_Lock); end if; Now := Clock; if Alarm <= Now then Time_Difference := 1; else Time_Difference := Alarm - Now; end if; Time_Difference := Time'Min (Time_Difference, Max_Sleep); if Alarm < Pending_Alarm then Set_Hw_Alarm (Clock_Interval (Time_Difference)); Pending_Alarm := Alarm; end if; if Multiprocessor then Unlock (Alarm_Lock); end if; end Update_Alarm; ``` Використання явного блокування обмежує доступ до спільних ресурсів і робить інтерференцію явною та придатною до аналізу. Переривання від таймера обробляється на призначеному процесорі. Обробник виконується з вимкненими перериваннями для захисту локальних структур даних і використовує багатопроцесорне блокування лише під час доступу до спільного стану синхронізації часу. Коли час таймерних подій закінчується для задач, призначених іншим процесорам, обробник безпосередньо не змінює віддалені черги готовності. Натомість він надсилає міжпроцесорне переривання відповідному процесору, який виконує необхідні оновлення локально: ```ada procedure Alarm_Handler (Interrupt : Interrupts . Interrupt_ID) is Now : Time; Next_Alarm : Time; begin Enter_Kernel; if Multiprocessor then Lock (Alarm_Lock); Pending_Alarm := Time'Last; Unlock (Alarm_Lock); else Pending_Alarm := Time'Last; end if; Update_Clock (Now); Next_Alarm := Now + Max_Sleep; if Multiprocessor then for CPU_Id in CPU loop if CPU_Id /= Current_CPU then declare Alarm : constant Time := Get_Next_Timeout (CPU_Id); begin if Alarm <= Now then Poke_CPU (CPU_Id); elsif Alarm < Next_Alarm then Next_Alarm := Alarm; end if; end; end if; end loop; end if; Execute_Expired_Timing_Events(Now); Wakeup_Expired_Alarms(Now); Next_Alarm := Time'Min (Get_Next_Timeout (Current_CPU), Next_Alarm); Update_Alarm (Next_Alarm); Leave_Kernel; end Alarm_Handler; ``` Після отримання міжпроцесорного переривання, згенерованого Poke_CPU, кожен цільовий процесор виконує власні процедури Execute_Expired_Timing_Events та Wakeup_Expired_Alarms. Це дозволяє обробити події, термін дії яких минув, у локальній черзі затримок та звільнити будь-які задачі, час очікування яких закінчився. Процесор, що виконує обробку таймерних подій, запускає ці ж процедури безпосередньо (для подій, що належать до його власної черги). Хоча цей механізм робить інтерференцію явною, він ускладнює реалізацію та збільшує зусилля, необхідні для аналізу інтерференції та часових характеристик, порівняно з використанням приватних таймерів для кожного процесора. #### 64-бітні таймери На системах, що надають 64-бітний вільно працюючий апаратний лічильник (як-от 64-бітні процесори Arm), годинник можна зчитувати атомарно та когерентно між процесорами без будь-якого захисту перериваннями. Такі лічильники забезпечують достатній діапазон і роздільну здатність, щоб уникнути проблем із переповненням протягом життєвого циклу системи, тому оновлення, що викликаються перериваннями, відсутні. Оскільки зчитування годинника не змінює спільний стан і не потребує синхронізації, вони не створюють додаткових каналів інтерференції та повністю підтримують детермінований аналіз часових характеристик. #### 32-бітні таймери Коли доступний лише 32-бітний лічильник, середовище виконання розширює апаратний лічильник за допомогою програмно підтримуваної старшої частини (MSP). Переривання від таймерних подій гарантують, що MSP оновлюється принаймні один раз за період апаратного лічильника (додатковий спеціальний обробник переривань для годинника не потрібен). Розділення між апаратним забезпеченням та пам'яттю створює проблему узгодженості, оскільки неможливо зчитати годинник повністю як одну атомарну операцію. В одноядерних системах узгодженість забезпечується шляхом дворазового зчитування комбінованих значень апаратного та програмного забезпечення та вибору стабільного результату. У багатоядерних системах оновлення MSP можуть надходити з кількох процесорів. Тому алгоритм зчитування годинника виявляє паралельні оновлення та повторює спробу, доки не буде отримано значення, яке гарантовано знаходиться між початком і завершенням операції зчитування, з обмеженою кількістю ітерацій: ```ada function Clock return Time is First_MSP : Clock_Periods; Before_MSP : Clock_Periods; Before_LSP : Clock_Interval; Now_LSP : Clock_Interval; After_MSP : Clock_Periods; begin -- Ми можемо обмежити кількість ітерацій у циклі до 3. Якщо під час -- першого зчитування маємо 1, а потім MSP збільшується, ми знаємо -- що час знаходиться між 1 & X та 2 & X, а отже, перед -- 3 & 0. У другій ітерації ми можемо прочитати 2, а потім значення -- знову збільшується. Отже, фактичний час знаходиться між 2 & X -- та 3 & X , тобто фактичний час, тобто на момент виходу з Clock -- становить принаймні 2 & 0. Проте ми не знаємо, де між 2 & 0 та -- 3 & 0 він є. Потім ми читаємо втретє, і якщо ми читаємо -- 3, а потім зміна, це означає, що фактичний час -- між 3 & X та 4 & X (тобто принаймні 3 & 0), отже, в кінці -- третьої ітерації ми можемо повернути 3 & 0 як безпечне значення -- тобто між початком і кінцем виконання цього виклику функції Clock. for Iteration in 1 .. 3 loop -- На багатопроцесорних системах можуть бути паралельні оновлення -- програмного годинника (Update_In_Progress). -- На монопроцесорах цикл виконується лише один раз. loop Before_MSP := Software_Clock.MSP; exit when not Multiprocessor or else Before_MSP /= Update_In_Progress; end loop; Before_LSP := Software_Clock.LSP; Now_LSP := Clock_Interval (Read_Hw_Clock); After_MSP := Software_Clock.MSP; -- Якщо MSP у Software_Clock змінився (або змінюється), -- ми не знаємо часу, коли було оновлено програмний годинник. -- Реалізація не мусить оновлювати програмний годинник у момент, -- близький до переповнення (wraparound) LSP (це потрібно робити -- принаймні один раз за період апаратного годинника, але ми -- не знаємо, коли саме). Отже, повернення -- (Before_MSP + 1) & 0 є неправильним, оскільки оновлений -- LSP у Software_Clock не обов'язково має бути близьким до -- нуля. -- Звичайний випадок, без оновлень у MSP if Before_MSP = After_MSP then -- Якщо нам відомо значення програмного годинника в момент -- зчитування апаратного годинника, ми знаємо час, -- оскільки програмний годинник ніколи не відстає -- не більше ніж на один періоду. return Before_MSP + ( if Now_LSP < Before_LSP then 1 else 0) & Now_LSP; -- Після першої невдалої ітерації зберегти перше -- значення MSP, як посилання на початковий час -- коли ми ввіїшли у функцію Clock. elsif Iteration = 1 then First_MSP := Before_MSP; -- Під час другої або третьої ітерації, якщо значення годинника -- збільшилося на два або більше, тоді Before_MSP & 0 безумовно -- знаходиться в межах між початком та завершенням виконання -- цього виклику функції Clock. elsif Before_MSP - First_MSP >= 2 then exit; end if; end loop; return Before_MSP & 0; end Clock; ``` Цей підхід забезпечує монотонність та правильність, уникаючи блокувань чи затримок. ## Узгодження з настановами AC 20-193 У цьому розділі описано, як запропонована модель виконання, що базується на мові програмування Ada, обмежених профілях задач та сертифікованій системі виконання на «голому залізі», вирішує основні проблеми та відповідає цілям AC 20-193. ### Планування AC 20-193 вимагає, щоб модель виконання, конфігурація процесора та динамічна поведінка апаратного забезпечення були чітко визначені та відображені в даних планування. Статична модель виконання, описана в розділі 3 (фіксовані задачі, статичні пріоритети та прив'язка до процесора, відсутність динамічних операцій із задачами та обмежена синхронізація), безпосередньо задовольняє ці вимоги. Вона запобігає умовам гонки та взаємним блокуванням (deadlocks) за своєю конструкцією, виключає динамічні рішення щодо планування та обмежує всі взаємодії компонентів, що робить систему придатною до статичного аналізу та спрощує її документування в артефактах планування. Там, де спільних апаратних ресурсів неможливо уникнути (наприклад, годинників і таймерів), їхні механізми доступу та пов'язана з ними інтерференція повністю визначені та обмежені, як описано в розділі 4.6, що дозволяє систематично опрацьовувати їх під час верифікації та аналізу часових характеристик. ### Налаштування ресурсів багатоядерного процесора AC 20-193 вимагає, щоб усі ресурси багатоядерного процесора були чітко ідентифіковані, налаштовані та керовані для забезпечення передбачуваної та повторюваної поведінки системи. Це стосується як обчислювальних ресурсів (наприклад, ядер процесорів та обробки переривань), так і спільних апаратних ресурсів, які можуть утворювати канали інтерференції (наприклад, тактові генератори, таймери, кеші та міжз'єднання). У запропонованому підході багатоядерні ресурси, що безпосередньо впливають на модель виконання, налаштовуються статично під час ініціалізації системи. До них належать набір активних процесорів, прив'язка переривань та їх маршрутизація, ресурси визначення часу (тактові генератори та таймери), а також базові пристрої вводу/виводу, як-от UART. Після ініціалізації ці конфігурації залишаються незмінними протягом усієї роботи системи й не змінюються під час виконання, відповідно до цілей детермінізму та стійкості AC 20-193. Інші ресурси, пов'язані з багатоядерністю, зокрема ті, що стосуються спільних апаратних структур (як-от кеші та арбітраж DMA на міжз'єднаннях), виходять за межі системи виконання і тому є відповідальністю розробника застосунку. AC 20-193 чітко вимагає, щоб конфігурація та використання таких ресурсів були визначені, обґрунтовані та перевірені. ### Канали перешкод та використання ресурсів Центральною метою AC 20-193 є виявлення та зменшення каналів інтерференції, що виникають через використання спільних апаратних ресурсів. Зауважте, що навіть якщо між задачами немає явного потоку даних або керування, на рівні платформи існує зв'язок, який може спричинити інтерференцію між ними. Цей аналіз здебільшого є відповідальністю розробника системи, але Ada надає механізми, що мінімізують конкуренцію за ресурси: * **Задачі та захищені об'єкти** статично призначаються процесорам, що мінімізує міжпроцесорну конкуренцію. * **Переривання** статично направляються до призначених процесорів за допомогою механізмів апаратної прив'язки до процесора, що зменшує асинхронну інтерференцію. Бібліотека середовища виконання зменшує інтерференцію завдяки архітектурним та конфігураційним механізмам. Наприклад, реалізація служб визначення часу задовольняє наступні властивості: - **Виявлення та пом'якшення інтерференції:** Спільні ресурси визначення часу або усуваються (таймери для кожного процесора), або явно захищаються (спільні таймери), що робить канали інтерференції ідентифікованими та придатними до аналізу. - **Розділене виконання:** Операції визначення часу дотримуються принципу розподілу задач за процесорами, а віддалені ефекти опосередковуються виключно через міжпроцесорні переривання. - **Обмежений час виконання:** Усі операції, пов'язані з визначенням часу, включаючи зчитування годинника та обробку таймерних подій, виконуються зі статично обмеженою складністю. Платформи, що забезпечують таймери для кожного процесора та 64-бітні лічильники, додатково зменшують зусилля на сертифікацію завдяки усуненню спільного стану визначення часу та мінімізації синхронізації. ### Верифікація програмного забезпечення Заявники повинні довести, що застосунки функціонують правильно і мають достатньо часу для виконання в умовах інтерференції, яка виникає під час роботи всього програмного забезпечення на багатоядерному процесорі. Статична модель виконання Ravenscar/Jorvik, як описано в розділах 3 та 4, безпосередньо підтримує ці цілі. Точний аналіз часу відгуку та часу виконання для найгіршого випадку можливий, оскільки планування базується на фіксованих пріоритетах і є розділеним. Конкуренція обмежена, оскільки синхронізація обмежена і використовує придатні до аналізу «справедливі блокування». Чітке визначення пріоритетів задач, прив'язки до процесора та захищених об'єктів у вихідному коді забезпечує надійну простежуваність від проектних рішень до доказів верифікації. Розробник застосунку використовує ці обмеження для спрощення власної діяльності з верифікації. Сама бібліотека середовища виконання повинна забезпечити наступні верифікації, ґрунтуючись на найгіршому сценарії інтерференції: - **Детальний ручний огляд:** Забезпечити належний захист від паралельних оновлень внутрішніх даних середовища виконання. - **Тестування функціональної поведінки:** - **Задачі з різних процесорів, що використовують спільні захищені об'єкти:** Забезпечити захист доступу до даних, а також умовне блокування та розблокування задач. - **Задачі з різних ядер, що зчитують значення годинника та встановлюють таймери:** Забезпечити узгодженість зчитування та очікуваний порядок активації за часом. - **Верифікація часових характеристик:** - **Накладні витрати на захищений обробник переривань (ALRM, C.3.1(15)):** Виміряти час виконання з моменту активації переривання до виконання першої інструкції користувача у приєднаному захищеному обробнику переривань - **Взаємовиключний доступ (ALRM, D.12(6)):** Виміряти часові витрати на отримання взаємовиключного доступу до захищеного об'єкта без входів. - **Нульова затримка до заданого часу (Null delay until) (ALRM, D.9(11)):** Виміряти час обробки запиту на затримку, яка не призводить до блокування задачі, що зробила цей запит. - **Затримка до моменту настання (Delay until) (ALRM, D.9(13/5)):** Виміряти різницю між запитаним часом завершення затримки та фактичним часом відновлення роботи задачі після абсолютної тимчасової зупинки. ### Виявлення та обробка помилок, а також захисні механізми Передбачуване виявлення та стримування помилок є критично важливими для багатоядерних систем з високою цілісністю. Мова Ada, разом із її обмеженими профілями задач, забезпечує структуровану та придатну до аналізу основу для реалізації надійних захисних механізмів. Логіка на рівні застосунку відповідає за обробку часових та функціональних аномалій за допомогою таких механізмів * **Винятки на рівні задачі:** Ada підтримує структуровану обробку винятків у межах кожної задачі. Винятки, що виникають внаслідок апаратних подій, перевірок під час виконання або внутрішніх помилок обчислень, обмежуються задачею, в якій вони виникли, що запобігає їх поширенню на інші задачі та підтримує стабільність системи. * **Статичне запобігання помилкам:** Профілі Ravenscar та Jorvik усувають динамічне створення задач, неконтрольований доступ до спільних даних та необмежені пріоритети. Ці обмеження зменшують ймовірність помилок під час виконання та роблять виявлення помилок передбачуваним і придатним до аналізу. * **Цілісність через захищені об'єкти:** Примітиви синхронізації, зокрема захищені об'єкти та «справедливі блокування», гарантують атомарність і взаємовиключний доступ. Порушення, наприклад спроби входу до захищеного об'єкта всупереч протоколу стелі пріоритетів (ceiling protocol), викликають чітко визначені винятки, гарантуючи, що помилкові стани виявляються та стримуються. Моніторинг використання процесора в Ada можливий за допомогою годинників часу виконання. У багатоядерному середовищі виконання годинники часу виконання реалізуються шляхом зчитування глобального апаратного лічильника в точках диспетчеризації та витіснення задач і накопичення часу, що минув для кожної задачі. Оскільки задачі статично прив'язані до процесорів, нема міграції, тож коригування не потрібні, що спрощує реалізацію. Статичний характер моделі Ravenscar та Jorvik дійсно обмежує діапазон можливих реакцій на перевищення бюджету, але сама можливість моніторингу є достатньою для виявлення та реєстрації. ## Висновок Поєднання мови програмування Ada, її обмежених профілів задач та сертифікованої системи виконання на «голому залізі» забезпечує надійну та практичну основу для вирішення проблем багатоядерної сертифікації. Впроваджуючи статичну, детерміністичну та придатну до аналізу модель виконання, цей підхід систематично обмежує інтерференцію, уможливлює обґрунтований аналіз часу виконання та часу відгуку для найгіршого випадку, а також забезпечує чітке розділення між програмними компонентами. Ці властивості тісно узгоджуються з цілями та рекомендованими практиками AC 20-193, зокрема щодо контролю інтерференції, детермінізму та достовірності верифікації. Ada — це не просто мова реалізації; вона також служить явною специфікацією. Архітектурні рішення, такі як пріоритети задач та прив'язки до процесора, чітко відображені в коді та видимі для розробників, рецензентів та інструментів аналізу. Оскільки ці рішення видимі для компілятора, всі структури даних задач можна генерувати статично, що усуває потребу в динамічній пам'яті. Семантику мови чітко визначено в Довідковому посібнику з Ada, зокрема її поведінку щодо задач та багатопроцесорного режиму. У поєднанні з обмеженими профілями, такими як Ravenscar та Jorvik, це спрощує реалізацію, зменшує недетермінізм та сприяє передбачуваності й сертифікованості. Бібліотеки середовища виконання доповнюють мову, надаючи документовані, верифіковані механізми для вибору проектних рішень, не охоплених самою Ada, таких як розділення планувальника, використання апаратного таймера та призначення процесорів обробки переривань. Ці механізми, разом зі статичною моделлю виконання, гарантують, що як прикладне програмне забезпечення, так і базова бібліотека середовища виконання можуть бути сертифіковані з керованими зусиллями верифікації, меншою вартістю та зниженим технічним і програмним ризиком, зберігаючи при цьому високий рівень впевненості в правильності часових характеристик та стійкості системи. Апаратне забезпечення залишається ключовим фактором, що сприяє сертифікації. Механізми, описані в цій статті, зменшують складність, зумовлену апаратним забезпеченням, але ретельний вибір обладнання додатково посилює **придатність до аналізу**. Зокрема, 64-бітні архітектури спрощують доступ до годинника та зменшують інтерференцію, тоді як таймери для кожного процесора усувають конкуренцію за спільні таймери. Цей вибір у поєднанні зі статичною та детерміністичною моделлю виконання Ada забезпечує оптимізовану, сертифіковану стратегію для багатоядерних систем з високою цілісністю. Для застосунків, де потрібна вища впевненість, підмножина SPARK мови Ada дозволяє отримати формальний доказ функціональної коректності та відсутності помилок під час виконання за допомогою інструментів статичного аналізу. SPARK доповнює підхід, описаний у цій статті: середовище виконання забезпечує сертифіковану платформу виконання, тоді як SPARK надає механізм для формальної верифікації коду застосунку, який працює поверх нього. Альтернативною стратегією верифікації багатоядерних систем є використання гіпервізора або ядра розділення (наприклад, операційної системи розділення, сумісної зі стандартом ARINC 653), що забезпечує просторову та часову ізоляцію між розділами на апаратному рівні. Гіпервізори створюють надійніші межі для локалізації збоїв, проте вони додають ще один програмний рівень, який також потребує сертифікації, а його часові накладні витрати необхідно враховувати під час аналізу. Підхід до виконання Ada на «голому залізі» замінює апаратну ізоляцію на рівні розділів на простішу надійну обчислювальну базу. У такому разі середовище виконання та програма сертифікуються як єдине ціле. Це дозволяє уникнути накладних витрат гіпервізора та зменшити обсяг сертифікації, якщо архітектура системи не потребує суворої ізоляції розділів.