Важливість концепції власності для досягнення безпеки памʼяті#
Автор: С. Такер Тафт (AdaCore)
Подія: ARG / IFIP WG 2.4, Саванна, Джорджія, березень 2026
Джерело: Презентація перед обговореннями пропозицій AI22-0148-1 та AI22-0152-1
Матеріал ґрунтується на презентаційних слайдах і протоколі засідання ARG (березень 2026). Пропозиції AI22-0148-1 (необовʼязкові компоненти) та AI22-0152-1 (розширювані компоненти) ще не прийняті до стандарту Ada. Синтаксичні приклади є ілюстративними і можуть змінитися в процесі стандартизації.
Вступ#
Безпека памʼяті перетворилася з академічної проблеми на регуляторну вимогу. У Сполучених Штатах, зокрема в урядових проєктах, тепер необхідно демонструвати, що програмне забезпечення написано безпечною для памʼяті мовою. Ada потрапила до схваленого списку, як і Rust. Обидві мови мають «небезпечні» люки для виходу, тому жодна з них не є безумовно безпечною, але обидві незрівнянно кращі за C чи C++ за замовчуванням.
Концепція, що лежить в основі, — власність — передує Rust більш ніж на два десятиліття. Серед основоположних робіт — докторська дисертація Дейва Кларка 2001 року з власності обʼєктів і зарахування, а також подальші формальні теорії Алдрича, Бояпаті та Алекса Потаніна. Ключовий висновок: власність є звільняючою дисципліною — вона забезпечує безпеку памʼяті без накладних витрат на виконання та недетермінованості збирача сміття.
Мови зі збирачем сміття технічно безпечні для памʼяті, але ніколи не здобули реального визнання у вбудованих системах критичної безпеки. Недетермінованість, вимоги до довіри, складність збирача — нічого з цього несумісне з жорсткими гарантіями реального часу або формальною сертифікацією. Тому перевага надається таким мовам, як Ada і Rust, де виділення і звільнення памʼяті відбуваються передбачуваними, чітко визначеними способами.
Існує два різновиди власності: власність вказівників (підхід Rust) і власність обʼєктів, що ґрунтується на вміщенні. Розглянемо обидва.
Два різновиди власності#
Власність вказівників#
Власність вказівників будується на одному фундаментальному інваріанті: у будь-який момент часу існує щонайбільше один власний вказівник на будь-який заданий обʼєкт у купі.
Присвоєння використовує семантику переміщення. Коли власний вказівник присвоюється новій змінній, початковий вказівник стає нульовим — він більше не є власником обʼєкта. Нова змінна стає єдиним власником. Саме це Rust називає «переміщенням» значення.
Короткочасний доступ без набуття власності реалізується через перевірник позичань. Позичання — це посилання, яке статично гарантовано матиме менший час життя, ніж власний вказівник. Поки позичання активне, власник заморожений — його не можна перемістити або знищити. Перевірник позичань забезпечує це під час компіляції без будь-яких витрат під час виконання.
У C++ аналогом є std::unique_ptr: власний розумний вказівник, що передає
власність при переміщуючому присвоєнні.
Власність вказівників забезпечує повністю динамічні структури даних із повною безпекою памʼяті. Проте існує одне важливе структурне обмеження: не можна будувати циклічні структури даних із власними вказівниками. Якщо вузол A є власником вузла B, а вузол B вказує назад на вузол A — інваріант власності руйнується. Для циклів потрібен інший механізм.
Власність обʼєктів#
Власність обʼєктів використовує принципово інший підхід. Замість того, щоб мати у власності вказівник на обʼєкт десь у купі, ви маєте у власності сам обʼєкт як безпосередній компонент — підкомпонент, що міститься всередині власника.
Це можна назвати моделлю квіткового горщика: обʼєкт містить свої підкомпоненти так само, як горщик містить ґрунт і рослини. Коли горщик викидають, усе в ньому іде разом із ним. Власність еквівалентна вміщенню.
Ключова вимога, що робить це можливим, — компоненти повинні мати можливість зростати і скорочуватися, включно зі скороченням до нуля. Це те, що пропонується називати необовʼязковими і розширюваними компонентами.
Це суттєве відхилення від поточних моделей компіляції Ada. Компілятори Ada зазвичай припускають, що компоненти мають фіксований розмір після створення. З дискримінованими записами можна змінювати розміри, але типова реалізація заздалегідь виділяє максимальний розмір для будь-якого варіанту. Власність обʼєктів вимагає гнучкішої моделі: обʼєкти мають повʼязану арену зберігання — область памʼяті — і підкомпоненти виділяються з цієї арени за потреби.
Прецеденти такого підходу включають мови Hermes і NIL від дослідницького підрозділу IBM наприкінці 1980-х і 90-х років, а також мову ParaSail.
Оскільки кожен обʼєкт є власним і самодостатнім, немає різниці між глибоким і поверхневим копіюванням — все є власним, тому копія завжди є глибокою за визначенням. Короткочасні посилання на компоненти все ще дозволені — аналогічно до передачі параметрів за посиланням у поточній Ada.
Необовʼязкові та розширювані компоненти#
Синтаксис#
Для підтримки власності обʼєктів необхідний синтаксис, що виражає відсутність обʼєкта або компонента. Запропонований синтаксис відображає існуючу нотацію Ada для виключення нуля:
Як
not nullперед позначенням підтипу виключає нуль,так
or nullпісля позначення підтипу дозволяє нуль.
Необовʼязковий компонент є нульовим за замовчуванням — аналогічно компоненту типу доступу.
Операція |
Синтаксис |
Семантика |
|---|---|---|
Копіювання |
|
Глибока копія, Y незмінний |
Переміщення |
|
X стає власником, Y → null |
Обмін |
|
Обмін вмістом, без виділення памʼяті |
Для циклічних структур даних — які неможливо представити через власність вказівників — власність обʼєктів використовує узагальнене індексування. Замість прямого вказівника на вузол зберігається індекс у таблиці вузлів. Таблиця вузлів є власником фактичних обʼєктів. Індекс у таблицю не може «зависнути», оскільки таблиця контролює час життя обʼєктів. Курсори в контейнерах природно стають індексами — вони не можуть стати недійсними внаслідок вставок або видалень в інших місцях контейнера.
Приклад: бінарне дерево#
type Tree_Node is record
Content : Integer;
Left : Tree_Node or null;
Right : Tree_Node or null;
end record;
Компоненти Left і Right є необовʼязковими. Листовий вузол має обидва
встановленими в null. Внутрішній вузол є безпосереднім власником своїх
лівого і правого піддерев — вони містяться в ньому, а не вказані в окремій
купі.
Коли вузол звільняється — через вихід з області видимості або через присвоєння нового значення батьківському вузлу — усе піддерево, яке він містить, звільняється автоматично. Рекурсивно, ієрархічно, без жодного явного обходу з боку програміста.
Для передачі піддерева використовується семантика переміщення:
Root.Left := Subtree'Move;
Після цього Subtree є нульовим, а Root.Left є власником того, що раніше
містив Subtree. Жодного виділення памʼяті, жодного копіювання — лише зміна
власності. Це модель квіткового горщика в дії: викиньте корінь — і все дерево
зникне.
Приклад: звʼязаний список#
type Linked_List is record
Data : String or null;
Next : Linked_List or null;
end record;
Data також є необовʼязковим — це компонент типу String змінного розміру.
Не лише структурні звʼязки є необовʼязковими: самі корисні навантаження даних
можуть бути власними компонентами змінного розміру.
Ініціалізація списку агрегатом:
L := (Data => "Hello", Next => (Data => "World", Next => null));
Подальше оновлення з іншим розміром рядка:
L.Data := "Universe";
Це присвоєння змінює розмір L.Data. Управління сховищем обробляє це
прозоро, перевиділяючи памʼять всередині арени за потреби. З точки зору
програміста — це просто присвоєння.
Власність і автоматичне управління сховищем#
Критичним наслідком власності — як заснованої на вказівниках, так і заснованої
на обʼєктах — є те, що явне звільнення памʼяті зникає з інтерфейсу
програміста: ніякого Unchecked_Deallocation, ніякої визначеної
користувачем фіналізації для цілей управління памʼяттю.
При власності вказівників: коли унікальний вказівник виходить з області видимості або йому присвоюється нове значення, раніше призначений обʼєкт негайно звільняється. Збирач не потрібен — інваріант єдиного власника гарантує відсутність інших посилань.
При власності обʼєктів: коли обʼєкт виходить з області видимості, його вся ієрархія вміщення звільняється — усі необовʼязкові компоненти, усі підкомпоненти підкомпонентів, усі рядки змінної довжини. Рекламація є ієрархічною та негайною.
Більшість використань типів Controlled та фіналізації в Ada на практиці
призначені для управління памʼяттю. При власності обʼєктів мова автоматично
управляє памʼяттю, тому фіналізація для цієї мети стає непотрібною.
Реалізація може використовувати фіналізацію внутрішньо (пул зберігання є
контрольованим типом), але це деталь реалізації, а не щось, чим управляє
програміст.
Обмежені арени зберігання#
Проблема обмеження для вбудованих систем#
Для вбудованих і критично-безпечних систем необмежене зростання сховища є неприйнятним. Необхідна можливість гарантувати найгірший сценарій споживання памʼяті під час компіляції або під час інтеграції системи.
Для одного розширюваного компонента — наприклад, String, обмеженого
максимально 256 символами — обмеження є простим: оголошується максимальний
розмір. Для дерева розширюваних обʼєктів задача складніша: кожен вузол
може мати розширювані компоненти, і саме дерево може зростати. Необхідно
відстежувати і обмежувати загальне сховище, споживане всім деревом.
Обмеження також вводить проблеми фрагментації: якщо вузли всередині обмеженої арени створюються і знищуються з різною швидкістю, може виникнути ситуація, коли неможливо виділити новий вузол, хоча загальний використаний простір нижче межі — через фрагментацію вільного простору. Це потребує ретельної уваги в дизайні.
Аспект Bound#
type Linked_List is record
Data : String or null;
Next : Linked_List or null;
end record with Bound => 1000;
Аспект Bound => 1000 означає: загальне сховище для будь-якого екземпляра
Linked_List — включно з усіма рекурсивно вкладеними звʼязками Next і
всіма рядками Data — обмежене 1000 одиницями зберігання.
Логічне представлення: ланцюжок вузлів, кожен із рядком
Data.Фізичне представлення: єдина арена зберігання з 1000 одиниць, з якої виділяються всі структури вузлів і рядкові дані.
Це забезпечує передбачуване споживання памʼяті в найгіршому випадку — критично важливе для вбудованих застосунків із жорсткими обмеженнями памʼяті.
Janus/Ada вже робить щось подібне для масивів, що залежать від дискримінанту: вони зберігаються і управляються окремо та перевиділяються при зміні дискримінанту. Власність обʼєктів узагальнює це для довільних типів компонентів.
Повна картина#
З необовʼязковими і розширюваними обʼєктами під дисципліною власності ми маємо мову з гнучкістю і простотою використання скриптової мови — можна будувати довільно складні, неоднорідні структури даних з природним синтаксисом — але з ефективністю, детермінованістю та безпекою памʼяті компільованої системної мови.
Ніяких витоків сховища
Ніяких висячих посилань
Ніякого використання після звільнення (use-after-free)
Ніякого подвійного звільнення (double-free)
Ніякого явного звільнення памʼяті в коді користувача
Для неоднорідних ієрархій вузлів — наприклад, AST у компіляторі — визначається ієрархія типів вузлів за допомогою варіантів або розширення типу, екземпляри зберігаються в таблиці вузлів, а індекси в таблиці використовуються як безпечні посилання. Таблиця вузлів є власником фактичних обʼєктів. Будуєте циклічні структури? Використовуйте індекси. Будуєте курсори? Використовуйте індекси. Вставки та видалення в таблиці ніколи не роблять існуючі індекси недійсними.
Це справжній крок вперед у дизайні мов: не просте копіювання функції з Rust, а синтез переваг власності — безпека памʼяті, детермінована рекламація — без складності явного управління вказівниками або анотацій перевірника позичань.
Власність у багатопотоковому середовищі#
Ada є принципово конкурентною мовою — задачі, захищені обʼєкти та паралельні конструкції є першокласними. Що відбувається з власністю обʼєктів, коли задіяно кілька потоків?
Пʼять викликів багатопотокового управління сховищем#
Локальність посилань. Обʼєкти, до яких певний потік часто звертається, мають бути близько в памʼяті. Міжпотокові сплески кешу є дорогими.
Помилкове спільне використання (false sharing). Обʼєкти, що належать різним потокам, не повинні спільно використовувати кеш-рядки, оскільки записи в обʼєкт одного потоку анулюють кеш-рядок для іншого потоку.
Накладні витрати на синхронізацію. Захоплення глобального блокування при кожному виділенні серіалізує всі потоки, знищуючи масштабованість.
Фрагментація. Довготривалі системи, що безперервно виділяють і звільняють обʼєкти різних розмірів, накопичують фрагментацію і деградують.
Балансування між ядрами. Сама інфраструктура управління сховищем не повинна ставати вузьким місцем, що заважає незалежним потокам рухатися вперед.
Глобальна купа проти куп на потік#
Традиційний підхід — глобальна спільна купа зі збирачем сміття (Java, C#, ML-сімейство, Go). Всі потоки виділяють памʼять з тієї самої купи. Збирач мусить періодично обходити всі досяжні обʼєкти з усіх потоків одночасно. Це фундаментальне вузьке місце масштабованості: паузи збирача впливають на всі потоки, бар'єри запису додають накладні витрати до кожного збереження вказівника, глобальна купа стає точкою суперечки.
Альтернатива — купи на потік: кожен потік виділяє памʼять з власної приватної купи без глобальної синхронізації. Це усуває більшість суперечок за виділення, але вводить нову проблему: коли один потік виробляє обʼєкти, які має споживати інший потік, потрібен або протокол передачі з блокуванням, або копіювання обʼєктів через межі куп, що зводить нанівець мету.
Управління на основі регіонів#
Оптимальний компроміс — управління сховищем на основі регіонів, теоретично розроблене Тофте і Талпіним, та вдосконалене на практиці в мові Cyclone.
Основна ідея: замість виділення окремих обʼєктів у глобальну купу і їх індивідуального звільнення, обʼєкти виділяються в регіони і звільняються цілими регіонами одночасно.
Кожна лексична область видимості має повʼязаний регіон. Коли область видимості виходить, весь регіон звільняється за одну операцію — без обходу по обʼєктах, без підрахунку посилань, без виявлення сміття. Вартість пропорційна кількості блоків у регіоні, а не кількості обʼєктів. Результат: нульове накопичення сміття, негайне і передбачуване звільнення при виході з області видимості, дешеві операції переміщення та обміну всередині регіону.
Регіони в багатопотоковій програмі#
При кількох потоках ключова ідея — розділення логічних регіонів від фізичних блоків регіонів.
Логічний регіон — це домен власності, повʼязаний з конкретною областю видимості та її потоком-власником. Фізично регіон складається з кількох блоків — суміжних ділянок сирої памʼяті, що можуть бути позичені з батьківського регіону за потреби.
Коли потік породжує дочірню задачу, дочірня задача може позичати невикористані частини поточного блоку батьківського потоку. При завершенні вона повертає позичені блоки. Міжрегіональні операції вимагають захоплення блокування цільового регіону — але кожен регіон має своє блокування, і вони потрібні рідко.
Викрадання задач (work-stealing) природно вписується в цю модель: коли потік викрадає задачу з черги іншого потоку, він також бере відповідальність за регіон, повʼязаний з цією задачею. Сховище викраденої задачі переміщується разом із нею, зберігаючи інваріант єдиного власника.
Фундаментальний інваріант: у будь-який момент часу логічний регіон є власністю рівно одного потоку — того, що виконується в межах області видимості цього регіону. Це інваріант єдиного власника, піднятий до рівня цілих регіонів.
Статистика: ParaSail як практичний приклад#
Реальні числа з середовища виконання ParaSail (тестовий запуск, 120 000 загальних виділень):
| Тип виділення | Частка | ||:| | Нові виділення потоком-власником | 42% | | Повторні виділення потоком-власником | 26% | | Всього потоком-власником (без синхронізації) | 68% | | Нові виділення непотоком-власником | 29% | | Повторні виділення непотоком-власником | 1% |
Ключовий висновок: власність концентрує операції сховища на потоці-власнику. 68% усіх виділень обробляються повністю локально, без жодної міжпотокової синхронізації.
Висновки#
Власність забезпечує безпеку памʼяті без збирача сміття — як при власності вказівників (Rust), так і при власності обʼєктів. Інваріант єдиного власника гарантує, що звільнена памʼять не буде доступна знову, а виділена памʼять завжди буде звільнена.
Власність обʼєктів є простішою для користувачів, ніж власність вказівників. Немає перевірника позичань, немає явних анотацій часу життя, немає ключового слова
move, розкиданого по коду. Програміст оголошує, що компоненти є необовʼязковими або розширюваними, — мова управляє рештою.Власність обʼєктів вимагає необовʼязкових і розширюваних компонентів — це суть пропозицій AI22-0148-1 та AI22-0152-1 для Ada. Обмежені арени зберігання (аспект
Bound) роблять підхід придатним для вбудованих застосунків і систем критичної безпеки.Власність обʼєктів дає кращу локалізацію сховища, ніж власність вказівників: підкомпоненти живуть у тій самій арені, що й їхній власник, що покращує поведінку кешу при обходах.
Управління на основі регіонів вирішує складнощі багатопотоковості без повернення до глобальної купи зі збирачем сміття. Блокування на рівні регіону та однопотокова власність регіону дають масштабоване, передбачуване управління сховищем.
Власність обʼєктів — це природна одиниця безпеки кількох потоків під час компіляції. Регіон, що містить власний обʼєкт і всі його підкомпоненти, належить рівно одному потоку одночасно. Статичне забезпечення цього дає свободу від гонок даних як гарантію під час компіляції, а не перевірку під час виконання.
Матеріал підготовлено на основі презентації С. Такера Тафта (AdaCore) на засіданні ARG / IFIP WG 2.4, Саванна, Джорджія, березень 2026.