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

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

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

Історія

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

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

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

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

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

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

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

Раннім і важливим використанням CSP була специфікація і верифікація елементів INMOS T9000 Transputer, комплексного конвеєрного процесора, розробленого для підтримки крупномасштабного мультипроцесінгу. CSP було використано у верифікації коректності конвеєра та Віртуального Каналу Процесора, що керував позачіповими зв’язком процесора.

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

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

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

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

Примітиви

Введемо для опису поведінки об'єкту термін процес, який може бути описаний з позиції обмеженої кількості подій (алфавіту) об'єкта.

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

Будемо дотримуватися далі наступної угоди:

1. Слова починаються з маленької літери позначають окремі події, наприклад: coin, choc, in2uah, out1uah, а так само окремі літери a, b, c і т.д.
2. Слова у верхньому регістрі позначають процеси, наприклад: VMS - проста торгова машина, VMС - більш складна торгова машина. Крім того літери P, Q, R (застосовується в законах) позначають якісь довільні процеси.
3. Букви x, y, z є змінними, що позначають подію
4. Букви A, B, C позначають безліч подій
5. Букви X, Y є змінними позначають процес

Події

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

• coin - опускання монетки в приймач монет
• choc - отримання шоколадки.

У разі ж більш складної машини, яка торгує двома видами шоколадок: маленькою (за гривню) і великою (за дві), ми отримаємо наступні дії:

• in1uah - опускання однієї гривні
• in2uah - опускання двох гривень
• small - отримання маленької шоколадки
• large - отримання великий шоколадки
• out1uah - отримання рештою однієї гривні

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

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

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

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

Алфавіт процесу P позначається як αP (альфа P), наприклад:

• αVMS = {coin, choc}
• αVMС = {in1p, in2p, small, large, out1p}

Процес з алфавітом A, який ніколи не бере участь ні в одному з подій з A позначається як $STOP_{A}$.

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

Примітивні процеси будуются з елементів алфавіту. Розглянемо декілька прикладів:

• Проста торгова машина ламається після віддачі однієї шоколадки: coin → STOP_{αVMS}

• Проста торгова машина ламається після обслуговування двох людей: coin → (choc → (coin → (choc → STOP_{αVMS})))

На початку машина може прийняти монетку, але не може віддати шоколадку, але після того як монетка вставлена ​​машина більше не буде приймати монети поки шоколадка НЕ ​​буде витягнута.

Зверніть увагу що такі записи некоректні синтаксично:

• P → Q
• x → y

→ в обов'язковому порядку повинен приймати зліва подія. Ланцюжок же префіксів зобов'язана кінчатися процесом. Прикладом коректної записи будуть рівносильні запису:

• x → (y → STOP)
• x → y → STOP

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

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

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

Префікс

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

$a\rightarrow P$

процес, готовий до комунікації з навколишнім середовищем, а після ${\mathit {a}}$ поводиться, як процес ${\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.

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

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

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

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

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

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

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

$\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}}$

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

Синтаксис

Синтаксис CSP визначає «легальні» способи комбінування подій і процесів. Нехай - подія, - множина подій. Тоді базовий синтаксис 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}}$

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

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

Деякі інші мови специфікації та формалізми були виведені з класичного 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