Комунікуючі послідовні процеси

Взаємодія послідовних процесів (англ. Communicating Sequential Processes, CSP) — формальна мова для опису закономірностей взаємодії в рівночасних системах. Це член сім'ї математичних теорій рівночасності, відомої як алгебра або числення процесів, в основі якої лежить обмін повідомленнями через канали. CSP відіграв важливу роль у розробці мови програмування occam, а також вплинув на дизайн таких мов програмування, як Limbo, RaftLib, Go, та бібліотеки core.async в Clojure.

CSP описує послідовні процеси, які взаємодіють лише через передачу повідомлень (і не через використання спільної пам'яті).

CSP був вперше описаний в 1978, у публікації Гоара, але з тих пір суттєво змінився. CSP практично застосовувався в промисловості як інструмент для специфікації і верифікації рівночасних аспектів різних систем, таких як Transputer T9000, а також безпечної системи електронної комерції. Теорія самого CSP досі є предметом активних досліджень, у тому числі робота з підвищення його спектру практичної застосовності (наприклад, збільшення масштабів систем, які можуть бути проаналізовані).

Історія

Версія CSP, представлена в оригінальній публікації Хоара 1978 року була, по суті, рівночасною мовою програмування, а не численням процесів. CSP мав принципово інший синтаксис, ніж у більш пізніх версіях, не володів математично-визначеною семантикою і не був в змозі представляти необмежений недетермінізм. Програми в оригінальному CSP були написані, як паралельні композиції фіксованого числа послідовних процесів, які спілкувалися один з одним строго через синхронну передачу повідомлень. На відміну від пізніших версій CSP, кожному процесу призначалось явне ім'я, а джерело або адресат повідомлення визначались задаванням імені передбачуваного відправника або процесу отримувача. Наприклад процес

COPY = *[c:character; west?c -> east!c]

без перестану отримує символ від процесу west та відправляє цей символ процесу east. Паралельна композиція

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

присвоює ім’я west процесу DISASSEMBLE, X процесу COPY і east процесу ASSEMBLE та виконує ці три процеси паралельно.

Після публікації оригінальної версії CSP, Хоар, Стівен Брукс та Біл Роско розвинули та вдосконалили теорію CSP до її сучасної форми, алгебри процесів. Підхід використаний при перетворенні CSP в алгебру процесів, був обраний під впливом під впливом роботи Робіна Мілнера над Численням комунікуючих систем (CCS) та навпаки, CSP вплинула на CCS. Теоретична версія CSP була спочатку представлена у статті Брукса, Хоара і Роско 1984р, пізніше – у книзі Хоара «Communicating Sequential Processes», що була опублікована у 1985р. У вересні 2006 ця книга все ще була однією з найбільш цитованих публікацій у комп’ютерних науках всіх часів за версією Citeseer. Теорія CSP пережила декілька незначних змін з моменту публікації книги Хоара. Більшість змін була викликана появою автоматизованих інструментів для аналізу та верифікації процесів. «The Theory and Practice of Concurrency» від Роско описує новішу версію CSP.

Використання

Раннім і важливим використанням CSP була специфікація і верифікація елементів транспютера INMOS T9000, комплексного суперскалярного конвеєрного процесора, розробленого для підтримки крупномасштабного мультипроцесингу. CSP було використано у верифікації коректності конвеєра та процесора віртуального каналу (англ. Virtual Channel Processor), що керував позачіповими комунікаціями процесора.

Індустріальне використання CSP у розробці програмного забезпечення, зазвичай, сфокусоване на надійних та критично-безпечних системах. Наприклад, Bremen Institute for Safe Systems та Daimler-Benz Aerospace змоделювали з допомогою CSP систему керування помилками та інтерфейс авіоніки (з приблизно 23000 рядків коду) для використання на Міжнародній космічній станції, та проаналізували модель, перевіривши відсутність в їхньому проекті взаємних блокувань та livelock-ів.. Процес моделювання та аналізу допоміг відшукати помилки, які було б важко знайти, використовуючи лише тестування. Аналогічно, Praxis High Integrity Systems використали CSP-моделювання і аналіз під час розробки програмного забезпечення (приблизно 100000 рядків коду) для безпечної сертифікації смарт-карток. Praxis стверджує, що система має значно меншу частоту дефектів, порівняно з аналогічними системами.

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

Неформальний опис

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

Примітиви

CSP забезпечує два класи примітивів в алгебрі процесів:

Події

Події являють собою комунікацію чи інші взаємодії. Припускається що вони нероздільні і миттєві. Вони можуть мати як атомарні імена (наприклад вкл, викл), складені імена (наприклад кран.відкрити, кран.закрити), або події вводу/виводу (наприклад mouse?xy, screen!bitmap).

Примітивні процеси.

Примітивні процеси задають фундаментальні поведінки, наприклад STOP (процес який не комунікує, який також називають deadlock), та SKIP (який завжди має успішне завершення).

Алгебраїчні оператори

CSP має широкий спектр алгебраїчних операторів. Основними з них є:

Префікс

Оператор «префікс» з'єднує подію і процес для отримання нового процесу. Наприклад:

$a\rightarrow P$

процес який передає в навколишнє середовище подію ${\mathit {a}}$, після чого поводиться як процес ${\mathit {P}}$.

Детермінований вибір

Оператор детермінованого (або зовнішнього) вибору дозволяє визначити майбутній розвиток процесу як вибір між двома складовими процесами і дозволяє навколишньому середовищу зробити вибір по початковій події одного з процесів. Наприклад:

$\left(a\rightarrow P\right)\Box \left(b\rightarrow Q\right)$

це процес, який залежно від початкової події, ${\mathit {a}}$ або ${\mathit {b}}$, поводить себе як ${\mathit {P}}$ або ${\mathit {Q}}$. Якщо одночасно відбудуться і ${\mathit {a}}$ і ${\mathit {b}}$, вибір буде здійснено недетерміновано.

Недетермінований вибір

Оператор недетермінованого (або внутрішнього) вибору дозволяє визначити майбутній розвиток процесу як вибір між двома складовими процесами, але не надає навколишньому середовищу контроль над цим вибором. Наприклад:

$\left(a\rightarrow P\right)\sqcap \left(b\rightarrow Q\right)$

може поводити себе, як $\left(a\rightarrow P\right)$ чи $\left(b\rightarrow Q\right)$. Він може відкинути ${\mathit {a}}$ або ${\mathit {b}}$ і зобов’язаний продовжити роботу, якщо середовище пропонує і ${\mathit {a}}$, і ${\mathit {b}}$. Недетермінізм може бути ненавмисно введений у детермінований вибір, якщо початкові події обох сторін є ідентичними. Наприклад:

$\left(a\rightarrow a\rightarrow STOP\right)\Box \left(a\rightarrow b\rightarrow STOP\right)$

еквівалентно до

$a\rightarrow \left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)$

Чергування

Оператор чергування представляє абсолютно незалежну одночасну діяльність.

$P\;\vert \vert \vert \;Q$

поводить себе одночасно і як ${\mathit {P}}$, і як ${\mathit {Q}}$. Події з обох процесів довільно чергуються у часі.

Інтерфейсний паралелелізм

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

$P\left\vert \left[\left\{a\right\}\right]\right\vert Q$

перед виконанням події ${\mathit {a}}$ необхідно, щоб і ${\mathit {P}}$, і ${\mathit {Q}}$ були в змозі виконати цю подію. Тому, наприклад, процес

$\left(a\rightarrow P\right)\left\vert \left[\left\{a\right\}\right]\right\vert \left(a\rightarrow Q\right)$

може виконати подію ${\mathit {a}}$ і стати процесом

$P\left\vert \left[\left\{a\right\}\right]\right\vert Q$

в той час як на

$\left(a\rightarrow P\right)\left\vert \left[\left\{a,b\right\}\right]\right\vert \left(b\rightarrow Q\right)$

чекає deadlock.

Приховування

Оператор приховування дозволяє робити деякі події неможливими для спостереження. Тривіальний приклад:

$\left(a\rightarrow P\right)\setminus \left\{a\right\}$

який, припустивши, що подія ${\mathit {a}}$ не з’являється у ${\mathit {P}}$, спрощується до

${\mathit {P}}$

Рекурсія

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

Розглянемо механічний годинник, зважаючи на те, що нас цікавлять лише його тіки, тоді:

αCLOCK = {tick}

Після того як годинник тікнув, він залишаться тим же годинником, тоді ми можемо сказати, що об'єкт після тіку стає годинником що виглядає наступним чином:

CLOCK = (tick → CLOCK)

Підставляючи CLOCK в праву частину ми будемо отримувати:

CLOCK

   = (Tick → CLOCK) [початкове рівняння]

   = (Tick → (tick → CLOCK)) [перша підстановка]

   = (Tick → (tick → (tick → CLOCK))) [друга підстановка]

Отже поведінку годинника може бути описано як нескінченна кількість повторюючихся тиків:

tick → tick → tick → · · ·

Даний спосіб посилання на себе буде працювати тільки у випадку якщо з правого боку рівняння вказано вираз, що починається з префіксу, наприклад рівняння:

X = X

Нічого не визначає, тому йому відповідає будь-який процес. Будемо далі називати опис процесу починаються з префіксу «захищеним». Таким чином якщо F (X) захищене вираз містить ім'я процесу X і αX = A, то рівняння:

X = F (X)

має єдине рішення з алфавітом A.

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

Формальне визначення

Синтаксис

Синтаксис CSP визначає «легальні» способи комбінування подій і процесів. Нехай ${\mathit {e}}$ - подія, ${\mathit {X}}$ - множина подій. Тоді базовий синтаксис CSP можна визначити як:

${\begin{matrix}Proc&::=&{\textit {STOP}}&\;\\&|&{\textit {SKIP}}&\;\\&|&e\rightarrow {\textit {Proc}}&({\text{prefixing}})\\&|&{\textit {Proc}}\;\Box \;{\textit {Proc}}&({\text{external}}\;{\text{choice}})\\&|&{\textit {Proc}}\;\sqcap \;{\textit {Proc}}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{\textit {Proc}}\;\vert \vert \vert \;{\textit {Proc}}&({\text{interleaving}})\\&|&{\textit {Proc}}\;|[\{X\}]|\;{\textit {Proc}}&({\text{interface}}\;{\text{parallel}})\\&|&{\textit {Proc}}\setminus X&({\text{hiding}})\\&|&{\textit {Proc}};{\textit {Proc}}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{\textit {Proc}}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{\textit {Proc}}\;\triangleright \;{\textit {Proc}}&({\text{timeout}})\\&|&{\textit {Proc}}\;\triangle \;{\textit {Proc}}&({\text{interrupt}})\end{matrix}}$

Відзначимо, що в інтересах стислості, описаний синтаксис опускає процес $\mathbf {div}$, який являє собою «розбіжний процес», а також різні оператори, такі як алфавітний паралелелізм, конвеєризація та індексований вибір.

Формальна семантика

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

Денотативна семантика

Основними денотативними моделями в CSP є модель слідів (англ. traces model), модель стабільних невдач (англ. stable failures), та модель невдач/розбіжностей (англ. failures/divergences). Відображення з виразів що задають процеси на кожну з цих трьох моделей і задають денотативну смантику CSP.

Модель слідів визначає значення виразу процесу як множину послідовностей подій (слідів) які можна спостерігати при роботі процесу. Наприклад:

• ${\mathit {traces}}\left({\mathit {STOP}}\right)=\left\{\langle \rangle \right\}$ тому що ${\mathit {STOP}}$ не генерує ніяких подій
• ${\mathit {traces}}\left(a\rightarrow b\rightarrow {\mathit {STOP}}\right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ тому що процес $(a\rightarrow b\rightarrow {\mathit {STOP}})$ може не згенерувати події, згенерувати подію $a$, або послідовність подій $a,b$

Більш формально, процес $P$ в моделі процесів описується як ${\mathit {traces}}\left(P\right)\subseteq \Sigma ^{\ast }$ такий що:

1. $\langle \rangle \in {\mathit {traces}}\left(P\right)$ (тобто ${\mathit {traces}}\left(P\right)$ містить порожню послідовність)
2. $s_{1}\smallfrown s_{2}\in {\mathit {traces}}\left(P\right)\implies s_{1}\in {\mathit {traces}}\left(P\right)$ (тобто ${\mathit {traces}}\left(P\right)$ замкнута операцією взяття префіксу)

де $\Sigma ^{\ast }$ множина всіх можливих скінченних послідовностей подій.

Модель стабільних невдач розширює модель слідів множинами відмов, які є множинами подій $X\subseteq \Sigma$ які процес може відмовитись виконати. Невдача це пара $\left(s,X\right)$, що складається зі сліду $s$, та множини невдач $X$ яка визначає події які процес може відмовитись виконати коли він виконав слід $s$. Спостережувана поведінка процесу в моделі стабільних невдач описується парою $\left({\mathit {traces}}\left(P\right),{\mathit {failures}}\left(P\right)\right)$. Наприклад,

• ${\mathit {failures}}\left(\left(a\rightarrow {\mathit {STOP}}\right)\Box \left(b\rightarrow {\mathit {STOP}}\right)\right)=\left\{\left(\langle \rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}$
• ${\mathit {failures}}\left(\left(a\rightarrow {\mathit {STOP}}\right)\sqcap \left(b\rightarrow {\mathit {STOP}}\right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\emptyset \right),\left(\langle b\rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}$

Модель невдач/розбіжностей ще більше розвиває модель невдач, аби працювати з розбіжністю. Семантикою процесу в моделі невдач/розбіжностей є пара $\left({\mathit {failures}}_{\perp }\left(P\right),{\mathit {divergences}}\left(P\right)\right)$ де ${\mathit {divergences}}\left(P\right)$ визначається як множина всіх слідів які можуть привести до розбіжної поведінки, а ${\mathit {failures}}_{\perp }\left(P\right)={\mathit {failures}}\left(P\right)\cup \left\{\left(s,X\right)\mid s\in {\mathit {divergences}}\left(P\right)\right\}$.

Пов’язані засоби специфікації та формалізми

Деякі інші мови специфікації та формалізми були виведені з класичного CSP, включаючи:

• Timed CSP, який об’єднує в собі часову інформацію про системи реального часу
• Receptive Process Theory, спеціалізація CSP, що передбачає асинхронні операції відправлення
• CSPP
• HSCSP
• Wright, мова опису архітектури
• TCOZ, інтеграція Timed CSP і Object Z
• Circus, інтеграція CSP і Z
• CML (Compass Modelling Language), комбінація Circus і VDM, створена для моделювання SoS (Systems of Systems)
• CspCASL, розширення CCCASL, що інтегрує CSP
• LOTOS, міжнародний стандарт, що містить в собі особливості CSP і CCS

Посилання

• https://swtch.com/~rsc/thread/squint.pdf [Архівовано 11 Січня 2018 у Wayback Machine.]