🍝 Філософи, що обідають — взаємне блокування та конкурентність

Задача філософів, що обідають — це уявний експеримент і тест для контролю конкурентності, запропонований Едсгером Дейкстрою 1965 року і пізніше популяризований Тоні Гоаром. П'ять філософів по черзі думають і їдять, але для їжі потрібно тримати дві виделки одночасно — по одній з кожного боку, — тоді як між кожною сусідньою парою доступна лише одна виделка. Завдання полягає в тому, щоб розробити протокол, за яким кожен філософ зрештою поїсть, а система не заблокується і жоден філософ не голодуватиме.

Виберіть стратегію у випадному списку на лівій панелі (Наївна, Впорядкування ресурсів, Арбітр або Ліміт 4 місця), потім натисніть «Відтворити», щоб запустити симуляцію безперервно, або «Крок», щоб просуватися по одному такту. Спостерігайте за полотном: блакитні кола — філософи, що думають, жовтогарячі — голодні й намагаються схопити виделки, зелені — ті, хто їсть. Панель статистики відстежує загальну кількість з'їдених страв і автоматично виявляє взаємне блокування.

У наївному режимі взаємне блокування настає, коли всі п'ять філософів одночасно стають жовтогарячими (голодні), кожен тримаючи рівно одну виделку й чекаючи на іншу. Детектор взаємного блокування спрацьовує, коли кожна виделка належить голодному філософу і жоден не тримає обидві — стан, з якого прогрес неможливий. На полотні з'являється червоне повідомлення «ВЗАЄМНЕ БЛОКУВАННЯ — циклічне очікування!», і симуляція автоматично зупиняється.

Коффман та інші (1971) визначили чотири необхідні умови, які мають виконуватися одночасно, щоб сталося взаємне блокування: (1) взаємне виключення — ресурс може належати лише одному процесу одночасно; (2) утримання й очікування — процес утримує принаймні один ресурс, чекаючи на інший; (3) відсутність витіснення — ресурс не можна забрати примусово; (4) циклічне очікування — у графі розподілу ресурсів існує цикл. Кожна стратегія запобігання взаємному блокуванню працює, порушуючи хоча б одну з цих чотирьох умов.

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

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

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

Едсгер В. Дейкстра представив цю задачу 1965 року як екзаменаційну вправу в Технологічному університеті Ейндговена, спочатку формулюючи її як «палички для їжі», а не виделки. Він розробив її, щоб проілюструвати підводні камені наївного використання семафорів і мотивувати структуровані примітиви конкурентності. Тоні Гоар пізніше переформулював її у вигляді, що нині широко викладається — п'ять філософів, п'ять виделок — у своїй книзі 1985 року «Communicating Sequential Processes», закріпивши її як канонічний навчальний приклад взаємного блокування, голодування та взаємного виключення.

Взаємне блокування — це глобальна зупинка системи: усі учасники заблоковані, і прогрес неможливий без зовнішнього втручання. Голодування — це порушення справедливості: система загалом продовжує рухатися, але один або кілька окремих філософів постійно обходяться й ніколи не встигають поїсти. Рішення може бути вільним від взаємного блокування, але все одно допускати голодування — наприклад, якщо два філософи, що ділять виделку, завжди ідеально чергуються, а третій завжди виключений. Надійні рішення, як-от протокол Чанді-Місри, гарантують і відсутність взаємного блокування, і зрештове обслуговування кожного філософа.

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

Так. Алгоритм Чанді-Місри (1984) — це повністю розподілене рішення на основі обміну повідомленнями, яке досягає як відсутності взаємного блокування, так і відсутності голодування без жодного центрального арбітра: філософи передають «брудні» й «чисті» токени разом із виделками за протоколом запитів. Новіші роботи застосовують транзакційну пам'ять (HTM/STM), щоб зробити захоплення кількох ресурсів атомарним на рівні апаратного забезпечення чи середовища виконання, усуваючи потребу в явному впорядкуванні. Дослідження протоколів успадкування пріоритету вирішують суміжну проблему інверсії пріоритетів, а формальні інструменти верифікації, такі як TLA+, регулярно використовуються для доведення відсутності взаємного блокування у промислових конкурентних системах.