Коммуникация последовательных процессов

Формальная модель в теории параллелизма

В информатике коммуникативные последовательные процессы ( CSP ) являются формальным языком для описания моделей взаимодействия в параллельных системах . ^[1] Это член семейства математических теорий параллелизма, известных как алгебры процессов или исчисления процессов , основанные на передаче сообщений по каналам . CSP оказал большое влияние на разработку языка программирования occam ^{[1] [2]} , а также повлиял на разработку таких языков программирования, как Limbo , ^[3] RaftLib , Erlang , ^[4] Go , ^{[5] [3]} Crystal , и core.async Clojure . ^[6]

CSP был впервые описан в статье Тони Хоара в 1978 году ^[7] , но с тех пор существенно изменился. ^[8] CSP практически применялся в промышленности как инструмент для определения и проверки параллельных аспектов множества различных систем, таких как T9000 Transputer , ^[9] , а также как безопасная система электронной коммерции. ^[10] Сама теория CSP также до сих пор является предметом активных исследований, включая работу по расширению ее диапазона практической применимости (например, увеличение масштаба систем, которые можно легко проанализировать). ^[11]

История

Версия CSP, представленная в оригинальной статье Хоара 1978 года, по существу представляла собой язык параллельного программирования, а не исчисление процессов . Он имел существенно другой синтаксис , чем более поздние версии CSP, не обладал математически определенной семантикой ^[12] и не мог представлять неограниченный недетерминизм . ^[13] Программы в оригинальном CSP были написаны как параллельная композиция фиксированного числа последовательных процессов, взаимодействующих друг с другом строго посредством синхронной передачи сообщений. В отличие от более поздних версий CSP, каждому процессу присваивалось явное имя, а источник или место назначения сообщения определялись путем указания имени предполагаемого процесса отправки или получения. Например, процесс

КОПИРОВАТЬ = *[c:character; запад?c → восток!c]

неоднократно получает символ от процесса с именем westи отправляет этот символ процессу с именем east. Параллельная композиция

[запад::РАЗБОРКА || X::КОПИРОВАТЬ || восток::ASSEMBLE]

присваивает имена westпроцессу DISASSEMBLE, Xпроцессу COPYи eastпроцессу ASSEMBLEи выполняет эти три процесса одновременно. ^[7]

После публикации оригинальной версии CSP Хоар, Стивен Брукс и А. В. Роско разработали и усовершенствовали теорию CSP до ее современной алгебраической формы. На подход, использованный при разработке CSP в алгебру процессов, повлияла работа Робина Милнера по исчислению коммуникационных систем (CCS) и наоборот. Теоретическая версия CSP была первоначально представлена ​​в статье Брукса, Хоара и Роско в 1984 году ^[14] , а затем в книге Хоара « Communicating Sequential Processes» ^[12] , которая была опубликована в 1985 году. В сентябре 2006 года эта книга все еще оставалась третий по цитируемости справочник по информатике всех времен по версии Citeseer ^{[ нужна ссылка ]} (хотя это ненадежный источник из-за характера выборки). Теория CSP претерпела несколько незначительных изменений со времени публикации книги Хоара. Большинство этих изменений было вызвано появлением автоматизированных инструментов для анализа и проверки процессов CSP. В книге Роско «Теория и практика параллелизма» ^[1] описана новая версия CSP.

Приложения

Ранним и важным применением CSP было его использование для спецификации и проверки элементов INMOS T9000 Transputer , сложного суперскалярного конвейерного процессора, предназначенного для поддержки крупномасштабной многопроцессорной обработки. CSP использовался для проверки правильности как конвейера процессора, так и процессора виртуального канала, который управлял внешней связью процессора. ^[9]

Промышленное применение CSP для разработки программного обеспечения обычно фокусируется на надежных и критически важных системах. Например, Бременский институт безопасных систем и компания Daimler-Benz Aerospace смоделировали в CSP систему управления отказами и интерфейс авионики (состоящий из около 23 000 строк кода), предназначенных для использования на Международной космической станции, и проанализировали модель, чтобы подтвердить, что в их конструкции не было тупиковых и живых блокировок. ^{[15] [16]} Процесс моделирования и анализа позволил выявить ряд ошибок, которые было бы трудно обнаружить с помощью одного лишь тестирования. Аналогичным образом компания Praxis High Integrity Systems применила моделирование и анализ CSP во время разработки программного обеспечения (около 100 000 строк кода) для безопасного центра сертификации смарт-карт, чтобы убедиться, что их конструкция безопасна и не имеет тупиковых ситуаций. Praxis утверждает, что у этой системы гораздо меньший процент дефектов, чем у сопоставимых систем. ^[10]

Поскольку CSP хорошо подходит для моделирования и анализа систем, включающих сложный обмен сообщениями, он также применяется для проверки протоколов связи и безопасности. Ярким примером такого рода приложений является использование Лоу CSP и средства проверки уточнений FDR для обнаружения ранее неизвестной атаки на протокол аутентификации с открытым ключом Нидхэма-Шредера , а затем для разработки исправленного протокола, способного отразить эту атаку. ^[17]

Неофициальное описание

Как следует из названия, CSP позволяет описывать системы с точки зрения составных процессов, которые работают независимо и взаимодействуют друг с другом исключительно посредством передачи сообщений . Однако «последовательная» часть имени CSP теперь является неправильным употреблением, поскольку современный CSP позволяет определять процессы-компоненты как как последовательные процессы, так и как параллельную композицию более примитивных процессов. Отношения между различными процессами и способ взаимодействия каждого процесса со своей средой описываются с помощью различных алгебраических операторов процесса. Используя этот алгебраический подход, можно легко построить довольно сложные описания процессов из нескольких примитивных элементов.

Примитивы

CSP предоставляет два класса примитивов в своей алгебре процессов:

События

События представляют собой коммуникации или взаимодействия. Они считаются неделимыми и мгновенными. Это могут быть атомарные имена (например , on , off ), составные имена (например, Valve.open , Valve.close ) или события ввода/вывода (например, mouse?xy , screen!bitmap ).

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

Примитивные процессы представляют фундаментальное поведение: примеры включают STOP (процесс, который ничего не передает, также называемый взаимоблокировкой ) и SKIP (который означает успешное завершение).

Алгебраические операторы

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

Префикс

Префиксный оператор объединяет событие и процесс для создания нового процесса. Например,

$${\displaystyle a\to P}$$

это процесс , который желает взаимодействовать со своим окружением и после a ведет себя как процесс P.

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

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

$${\displaystyle (a\to P)\Box (b\to Q)}$$

— это процесс, который готов сообщить начальные события a и b и впоследствии ведет себя как P или Q , в зависимости от того, какое начальное событие выбирает среда. Если бы и a , и b были сообщены одновременно, выбор был бы решен недетерминированно.

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

Оператор недетерминированного (или внутреннего) выбора позволяет определить будущую эволюцию процесса как выбор между двумя составляющими процессами, но не позволяет среде контролировать, какой из составных процессов будет выбран. Например,

$${\displaystyle (a\to P)\sqcap (b\to Q)}$$

может вести себя как или . Он может отказаться принять a или b и обязан сообщать только в том случае, если среда предлагает и a , и b . Недетерминизм может быть непреднамеренно привнесен в номинально детерминированный выбор, если исходные события обеих сторон выбора идентичны. Так, например, ${\displaystyle (a\to P)}$ ${\displaystyle (b\to Q)}$

$${\displaystyle (a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})}$$

эквивалентно

$${\displaystyle a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}}$$

Чередование

Оператор чередования представляет собой полностью независимую параллельную деятельность. Процесс

$${\displaystyle P\;|||\;Q}$$

ведет себя как P и Q одновременно. События обоих процессов произвольно чередуются во времени.

Параллельный интерфейс

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

$${\displaystyle P\;|[\{a\}]|\;Q}$$

требует, чтобы P и Q были в состоянии выполнить событие a, прежде чем это событие может произойти. Так, например, процесс

$${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$$

может участвовать в событии а и стать процессом

$${\displaystyle P\;|[\{a\}]|\;Q}$$

пока

$${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$$

просто зайдет в тупик.

Прячется

Оператор скрытия позволяет абстрагировать процессы, делая некоторые события ненаблюдаемыми. Тривиальный пример сокрытия:

$${\displaystyle (a\to P)\setminus \{a\}}$$

что, предполагая, что событие a не появляется в P , просто сводится к

$${\displaystyle P}$$

Примеры

Одним из типичных примеров CSP является абстрактное представление автомата по продаже шоколада и его взаимодействия с человеком, желающим купить шоколад. Этот торговый автомат может выполнять два разных события: «монета» и «шоколад», которые представляют собой внесение платежа и доставку шоколада соответственно. Автомат, который требует оплаты (только наличными) перед тем, как предложить шоколад, можно записать так:

$${\displaystyle \mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

Человека, который может решить использовать монету или карту для совершения платежей, можно смоделировать следующим образом:

$${\displaystyle \mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\Box (\mathrm {card} \rightarrow \mathrm {STOP} )}$$

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

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

тогда как если бы синхронизация требовалась только для «монеты», мы бы получили

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)}$$

Если мы абстрагируем этот последний составной процесс, скрывая события «монеты» и «карты», т.е.

$${\displaystyle \left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}}$$

мы получаем недетерминированный процесс

$${\displaystyle \left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP} }$$

Это процесс, который либо предлагает событие «choc», а затем останавливается, либо просто останавливается. Другими словами, если мы будем рассматривать абстракцию как внешний взгляд на систему (например, тот, кто не видит решения, принятого этим человеком), будет введен недетерминизм .

Формальное определение

Синтаксис

Синтаксис CSP определяет «законные» способы объединения процессов и событий. Пусть e — событие, а X — набор событий. Тогда основной синтаксис CSP можно определить как:

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

Обратите внимание, что в целях краткости в представленном выше синтаксисе опущен процесс , который представляет дивергенцию , а также различные операторы, такие как параллелизация в алфавитном порядке, конвейерная обработка и индексированный выбор. ${\displaystyle \mathbf {div} }$

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

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

Денотационная семантика

Тремя основными моделями CSP являются модель трасс , модель устойчивых сбоев и модель сбоев/расхождений . Семантические отображения выражений процесса в каждую из этих трех моделей обеспечивают денотационную семантику для CSP. ^[1]

Модель трассировок определяет значение выражения процесса как набора последовательностей событий (трасс), выполнение которых можно наблюдать. Например,

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

Более формально смысл процесса P в модели трасс определяется следующим образом : ${\displaystyle \mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }}$

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

где – множество всех возможных конечных последовательностей событий. ${\displaystyle \Sigma ^{\ast }}$

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

$${\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\Box \left(b\rightarrow \mathrm {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\}}$$

$${\displaystyle \mathrm {failures} \left(\left(a\rightarrow \mathrm {STOP} \right)\sqcap \left(b\rightarrow \mathrm {STOP} \right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}}$$

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

Инструменты

За прошедшие годы был создан ряд инструментов для анализа и понимания систем, описываемых с использованием CSP. Ранние реализации инструментов использовали различные машиночитаемые синтаксисы для CSP, что делало входные файлы, написанные для разных инструментов, несовместимыми. Однако большинство инструментов CSP в настоящее время стандартизированы на машиночитаемом диалекте CSP, разработанном Брайаном Скаттергудом, иногда называемом CSP _M. ^[18] Диалект CSP _M обладает формально определенной операционной семантикой , которая включает встроенный функциональный язык программирования .

Самый известный инструмент CSP, вероятно, — это «Failers/Divergence Refinement 2» ( FDR2 ), коммерческий продукт, разработанный компанией Formal Systems (Europe) Ltd. FDR2 часто описывается как средство проверки моделей , но технически это средство проверки уточнений , в том смысле, что он преобразует два выражения процесса CSP в системы меченых переходов (LTS), а затем определяет, является ли один из процессов уточнением другого в рамках некоторой указанной семантической модели (следы, сбои или сбои/расхождения). ^[19] FDR2 применяет различные алгоритмы сжатия пространства состояний к процессам LTS, чтобы уменьшить размер пространства состояний, которое необходимо исследовать во время уточняющей проверки. На смену FDR2 пришла FDR3, полностью переписанная версия, включающая, среди прочего, параллельное выполнение и встроенную проверку типов. Он выпущен Оксфордским университетом, который также выпустил FDR2 в период 2008–2012 годов. ^[20]

Средство проверки уточнения Adelaide ( ARC ) ^[21] — средство проверки уточнения CSP, разработанное Группой формального моделирования и проверки в Университете Аделаиды . ARC отличается от FDR2 тем, что внутри он представляет процессы CSP как упорядоченные двоичные диаграммы решений (OBDD), что облегчает проблему взрыва состояний явных представлений LTS, не требуя использования алгоритмов сжатия пространства состояний, таких как те, которые используются в FDR2.

Проект ProB [22], реализуемый ^{Институтом} информатики Университета Генриха Гейне в Дюссельдорфе, изначально был создан для поддержки анализа спецификаций, построенных с помощью метода B. Однако он также включает поддержку анализа процессов CSP как посредством уточнения, так и проверки модели LTL . ProB также можно использовать для проверки свойств комбинированных спецификаций CSP и B. ProBE CSP Animator интегрирован в FDR3.

Набор инструментов для анализа процессов (PAT) ^{[23] [24]} — это инструмент анализа CSP, разработанный в Школе вычислительной техники Национального университета Сингапура . PAT может выполнять уточняющую проверку, проверку модели LTL и моделирование процессов CSP и Timed CSP. Язык процессов PAT расширяет CSP поддержкой изменяемых общих переменных, асинхронной передачи сообщений, а также различных конструкций процессов, связанных со справедливостью и количественными показателями времени, таких как deadlineи waituntil. Основной принцип проектирования языка процессов PAT заключается в объединении языка спецификаций высокого уровня с процедурными программами (например, событием в PAT может быть последовательная программа или даже вызов внешней библиотеки C#) для большей выразительности. Изменяемые общие переменные и асинхронные каналы обеспечивают удобный синтаксический сахар для известных шаблонов моделирования процессов, используемых в стандартном CSP. Синтаксис PAT похож, но не идентичен синтаксису CSP _M. ^[25] Принципиальными различиями между синтаксисом PAT и стандартным CSP _M являются использование точек с запятой для завершения выражений процесса, включение синтаксического сахара для переменных и присваиваний, а также использование немного другого синтаксиса для внутреннего выбора и параллельной композиции.

VisualNets ^[26] создает анимированные визуализации систем CSP на основе спецификаций и поддерживает CSP с синхронизацией.

CSPsim ^[27] — ленивый симулятор. Он не моделирует проверку CSP, но полезен для исследования очень больших (потенциально бесконечных) систем.

SyncStitch — это средство проверки уточнений CSP с интерактивной средой моделирования и анализа. Имеет графический редактор диаграмм перехода состояний. Пользователь может моделировать поведение процессов не только с помощью выражений CSP, но и с помощью диаграмм перехода состояний. Результаты проверки также отображаются графически в виде деревьев вычислений и могут анализироваться в интерактивном режиме с помощью периферийных инструментов проверки. В дополнение к уточняющим проверкам он может выполнять проверку взаимоблокировок и проверку работоспособности.

Связанные формализмы

Несколько других языков спецификаций и формализмов были получены из классического несинхронизированного CSP или вдохновлены им, в том числе:

• Timed CSP ^{[ постоянная мертвая ссылка ]} , которая включает в себя информацию о времени для рассуждений о системах реального времени.
• Теория рецептивных процессов, специализация CSP, которая предполагает асинхронную (т. е. неблокирующую ) операцию отправки.
• КСПП
• HCSP
• TCOZ, интеграция Timed CSP и Object Z
• Circus, интеграция CSP и Z на основе объединяющих теорий программирования.
• CML. Архивировано 19 февраля 2020 г. в Wayback Machine (язык моделирования COMPASS), комбинации Circus и VDM , разработанной для моделирования систем систем (SoS).
• CspCASL, расширение CASL , интегрирующее CSP.
• LOTOS — международный стандарт ^[28] , включающий в себя функции CSP и CCS .
• PALPS, вероятностное расширение с местами для экологических моделей, разработанное Анной Филиппу и Маурисио Торо Бермудесом.

Сравнение с моделью актера

В том, что касается параллельных процессов, обменивающихся сообщениями, модель актера во многом похожа на CSP. Однако эти две модели делают принципиально разные выборы в отношении предоставляемых ими примитивов:

• Процессы CSP анонимны, а субъекты имеют личность.
• CSP использует явные каналы для передачи сообщений, тогда как системы субъектов передают сообщения именованным субъектам назначения. Эти подходы можно рассматривать как двойственные друг другу в том смысле, что процессы, поступающие по одному каналу, фактически имеют идентификатор, соответствующий этому каналу, в то время как связь между актерами на основе имен может быть нарушена путем создания акторов, которые ведут себя как каналы.
• Передача сообщений CSP по сути предполагает встречу между процессами, участвующими в отправке и получении сообщения, то есть отправитель не может передать сообщение до тех пор, пока получатель не будет готов его принять. Напротив, передача сообщений в системах субъектов принципиально асинхронна, т.е. передача и прием сообщений не обязательно должны происходить одновременно, и отправители могут передавать сообщения до того, как получатели будут готовы их принять. Эти подходы также можно считать двойственными друг другу в том смысле, что системы на основе рандеву могут использоваться для построения буферизованных коммуникаций, которые ведут себя как асинхронные системы обмена сообщениями, в то время как асинхронные системы могут использоваться для построения коммуникаций в стиле рандеву с использованием сообщения/ протокол подтверждения для синхронизации отправителей и получателей.

Обратите внимание, что вышеупомянутые свойства не обязательно относятся к оригинальной статье CSP Хоара, а скорее к современному воплощению идеи, как это видно в таких реализациях, как Go и Clojure core.async. В исходной статье каналы не были центральной частью спецификации, а процессы отправителя и получателя фактически идентифицировали друг друга по имени.

Премия

В 1990 году « Королевская премия за технологические достижения была вручена… вычислительной лаборатории [Оксфордского университета] ». Эта награда является признанием успешного сотрудничества между лабораторией и Inmos Ltd.… Флагманским продуктом Inmos является « транспьютер », микропроцессор со многими деталями, которые обычно необходимы дополнительно, встроенными в один и тот же компонент ». ^[29] По словам Тони Хоара, ^[30] «INMOS Transputer был воплощением идей… создания микропроцессоров, которые могли бы взаимодействовать друг с другом по проводам, протянутым между их терминалами. У основателя было видение, что идеи CSP созрели для промышленного использования, и он положил это в основу языка программирования транспьютеров, который получил название Occam . … По оценкам компании, это позволило им поставить оборудование на год раньше, чем это могло бы произойти в противном случае. Они подали заявку и выиграли Королевскую премию за технологические достижения совместно с вычислительной лабораторией Оксфордского университета».

Смотрите также

• Теория следов , общая теория следов.
• Моноид трассировки и моноид истории
• Удобный язык программирования
• язык программирования XC
• VerilogCSP — это набор макросов , добавленных в Verilog HDL для поддержки связи последовательных процессов по каналам связи.
• Joyce — язык программирования, основанный на принципах CSP, разработанный Бринчом Хансеном примерно в 1989 году.
• SuperPascal — язык программирования, также разработанный Бринчом Хансеном под влиянием CSP и его более ранней работы с Джойсом .
• Ада реализует такие функции CSP, как рандеву.
• DirectShow — это видеофреймворк внутри DirectX , он использует концепции CSP для реализации аудио- и видеофильтров.
• OpenComRTOS — это официально разработанная сетецентрическая распределенная RTOS, основанная на прагматичном расширении CSP.
• Автомат ввода/вывода
• Модель параллельного программирования
• TLA+ — еще один формальный язык для моделирования и проверки параллельных систем.

Рекомендации

1. Роско, AW (1997). Теория и практика параллелизма (PDF) . Прентис Холл . ISBN 978-0-13-674409-2.
2. Инмос (12 мая 1995 г.). Справочное руководство occam 2.1 (PDF) . СГС-Томсон Микроэлектроника Лтд., документ ИНМОС 72 occ 45 03.
3. Кокс, Расс. «Лаборатории Bell и темы CSP» . Проверено 15 апреля 2010 г.
4. «10 академических и исторических вопросов» . Проверено 15 ноября 2021 г.
5. «Часто задаваемые вопросы: зачем строить параллелизм на идеях CSP?». Язык программирования Go . Проверено 15 октября 2021 г.
6. Хики, Рич (28 июня 2013 г.). «Каналы Clojure core.async» . Проверено 15 октября 2021 г.
7. Хоар, ЦАР (1978). «Общение последовательных процессов». Коммуникации АКМ . 21 (8): 666–677. дои : 10.1145/359576.359585 . S2CID  849342.
8. Абдалла, Али Э.; Джонс, Клифф Б.; Сандерс, Джефф В. (2005). Коммуникация последовательных процессов: первые 25 лет. ЛНКС . Том. 3525. Спрингер. ISBN 9783540258131.
9. Барретт, Г. (1995). «Проверка модели на практике: процессор виртуального канала T9000». Транзакции IEEE по разработке программного обеспечения . 21 (2): 69–78. дои : 10.1109/32.345823.
10. Холл, А; Чепмен, Р. (2002). «Правильность по конструкции: разработка коммерческой безопасной системы» (PDF) . Программное обеспечение IEEE . 19 (1): 18–25. CiteSeerX 10.1.1.16.1811 . дои : 10.1109/52.976937. 
11. Криз, С. (2001). Независимая от данных индукция: проверка модели CSP сетей произвольного размера (доктор философии). Оксфордский университет . CiteSeerX 10.1.1.13.7185 . 
12. Хоар, ЦАР (1985). Коммуникация последовательных процессов . Прентис Холл. ISBN 978-0-13-153289-2.
13. Клингер, Уильям (июнь 1981 г.). Основы акторной семантики (докторская диссертация по математике). Массачусетский технологический институт. hdl : 1721.1/6935.
14. Брукс, Стивен; Хоар, Африка ; Роско, AW (1984). «Теория связи последовательных процессов». Журнал АКМ . 31 (3): 560–599. дои : 10.1145/828.833 . S2CID  488666.
15. Бут, Б.; М. Куварас; Дж. Пелеска; Х. Ши (декабрь 1997 г.). «Анализ тупиковых ситуаций для отказоустойчивой системы». Материалы 6-й Международной конференции по алгебраической методологии и программным технологиям (AMAST'97) . стр. 60–75.
16. Бут, Б.; Дж. Пелеска; Х. Ши (январь 1999 г.). «Комбинирование методов динамического анализа отказоустойчивой системы». Материалы 7-й Международной конференции по алгебраической методологии и программным технологиям (AMAST'98) . стр. 124–139.
17. Лоу, Г. (1996). «Взлом и исправление протокола открытого ключа Нидхэма – Шредера с использованием FDR». Инструменты и алгоритмы построения и анализа систем (TACAS) . Спрингер-Верлаг. стр. 147–166.
18. Scattergood, JB (1998). Семантика и реализация машиночитаемого CSP ( доктор философии ). Вычислительная лаборатория Оксфордского университета .
19. Роско, AW (1994). «CSP для проверки модели». Классический разум: очерки в честь К. А. Хоара . Прентис Холл.
20. «Введение — документация FDR 4.2.4» . www.cs.ox.ac.uk. _
21. Парашкевов, Атанас Н.; Янчев, Джей (1996). «ARC – инструмент для эффективного уточнения и проверки эквивалентности CSP». IEEE Международный. Конф. по алгоритмам и архитектурам параллельной обработки ICA3PP '96 . стр. 68–75. CiteSeerX 10.1.1.45.3212 . 
22. Леушел, Майкл; Фонтейн, Марк (2008). «Исследование глубин CSP-M: новый инструмент проверки, соответствующий требованиям FDR» (PDF) . ИКФЕМ 2008 . Спрингер-Верлаг. Архивировано из оригинала (PDF) 19 июля 2011 г. Проверено 26 ноября 2008 г.
23. Вс, июнь; Лю, Ян; Донг, Джин Сон (2009). «PAT: к гибкой проверке в условиях справедливости» (PDF) . Материалы 20-й Международной конференции по компьютерной верификации (CAV 2009) . Конспекты лекций по информатике. Том. 5643. Спрингер. Архивировано из оригинала (PDF) 11 июня 2011 г. Проверено 16 июня 2009 г.
24. Вс, июнь; Лю, Ян; Донг, Джин Сон (2008). «Возврат к CSP для проверки модели: введение в набор инструментов для анализа процессов» (PDF) . Материалы Третьего международного симпозиума по использованию формальных методов, верификации и валидации (ISoLA 2008) . Коммуникации в компьютерной и информатике. Том. 17. Спрингер. стр. 307–322. Архивировано из оригинала (PDF) 8 января 2009 г. Проверено 15 января 2009 г.
25. Вс, июнь; Лю, Ян; Донг, Джин Сон; Чен, Чуньцин (2009). «Интеграция спецификаций и программ для спецификации и проверки системы» (PDF) . IEEE Международный. Конф. по теоретическим аспектам программной инженерии TASE '09 . Архивировано из оригинала (PDF) 11 июня 2011 г. Проверено 13 апреля 2009 г.
26. Грин, Марк; Абдаллах, Али (2002). «Анализ производительности и настройка поведения для оптимизации коммуникационных систем». Коммуникационные архитектуры процессов 2002 .
27. Брук, Филипп; Пейдж, Ричард (2007). «Ленивое исследование и проверка моделей CSP с помощью CSPsim». Коммуникационные архитектуры процессов 2007 .
28. ISO 8807, Спецификация языка временного упорядочения
29. Герайнт Джонс (1990). «Острый как бритва: Королевская премия компьютерной лаборатории». Журнал Oxford Magazine (59, четвертая неделя, семестр Троицы).
30. Лен Шустек (март 2009 г.). «Интервью с CAR Hoare». Коммуникации АКМ . 52 (3): 38–41. дои : 10.1145/1467247.1467261. S2CID  1868477.

дальнейшее чтение

• Хоар, ЦАР (2004) [1985]. Коммуникация последовательных процессов. Прентис Холл Интернэшнл. ISBN 978-0-13-153271-7.
  • Эта книга была обновлена ​​Джимом Дэвисом из вычислительной лаборатории Оксфордского университета , а новое издание доступно для загрузки в виде PDF-файла на веб-сайте using CSP.
• Роско, AW (1997). Теория и практика параллелизма . Прентис Холл . ISBN 978-0-13-674409-2.
  • Некоторые ссылки, относящиеся к этой книге, доступны здесь. Полный текст доступен для загрузки в формате PS или PDF из списка академических публикаций Билла Роско.

Внешние ссылки

• PDF-версия книги Хоара CSP – действуют ограничения авторских прав, перед загрузкой просмотрите текст страницы.
• Аннотация CSP (китайская версия), некоммерческий перевод и аннотационная работа, основанная на книге Прентис-Холла (1985 г.), китайской версии Чаочэня Чжоу (1988 г.) и онлайн-версии Джима Дэвиса (2015 г.).
• WoTUG, группа пользователей систем CSP и occam, содержит некоторую информацию о CSP и полезные ссылки.
• «Цитаты CSP» от CiteSeer