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

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

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

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

История

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

COPY = *[c:символ; запад?c → восток!c]

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

[west::РАЗОБРАТЬ || X::КОПИРОВАТЬ || east::СОБЕРИ]

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

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

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

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

Примитивы

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

События

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

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

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

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

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

Префикс

Префиксный оператор объединяет событие и процесс для создания нового процесса. Например, это процесс , который готов общаться с окружающей средой и после a ведет себя как процесс P. $${\displaystyle a\to P}$$

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

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

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

Недетерминированный (или внутренний) оператор выбора позволяет определить будущую эволюцию процесса как выбор между двумя компонентными процессами, но не позволяет среде контролировать, какой из компонентных процессов будет выбран. Например, может вести себя как либо или . Он может отказаться принять a или b и обязан сообщать только в том случае, если среда предлагает как a, так и b . Недетерминизм может быть непреднамеренно введен в номинально детерминированный выбор, если начальные события обеих сторон выбора идентичны. Так, например, эквивалентно $${\displaystyle (a\to P)\sqcap (b\to Q)}$$ ${\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 )}}$$

Чередование

Оператор чередования представляет собой полностью независимую параллельную активность. Процесс ведет себя как P и Q одновременно. События из обоих процессов произвольно чередуются во времени. $${\displaystyle P\;|||\;Q}$$

Интерфейс параллельный

Интерфейсный параллельный оператор представляет собой параллельную активность, которая требует синхронизации между компонентными процессами: любое событие в наборе интерфейсов может произойти только тогда, когда все компонентные процессы способны участвовать в этом событии. Например, процесс требует, чтобы P и Q оба могли выполнить событие a до того, как это событие может произойти. Так, например, процесс может участвовать в событии a и стать процессом , в то время как просто заблокируется. $${\displaystyle P\;|[\{a\}]|\;Q}$$ $${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$$ $${\displaystyle P\;|[\{a\}]|\;Q}$$ $${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$$

Скрытие

Оператор скрытия предоставляет способ абстрагировать процессы, делая некоторые события ненаблюдаемыми. Тривиальный пример скрытия — это то, что, предполагая, что событие a не появляется в P , просто сводится к $${\displaystyle (a\to P)\setminus \{a\}}$$ $${\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 обладает формально определенной операционной семантикой , которая включает встроенный функциональный язык программирования .

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

Adelaide Refinement Checker ( ARC ) ^[21] — это CSP-проверщик уточнения, разработанный Formal Modelling and Verification Group в Университете Аделаиды . ARC отличается от FDR2 тем, что он внутренне представляет процессы CSP как упорядоченные двоичные диаграммы решений (OBDD), что устраняет проблему взрыва состояний явных представлений LTS, не требуя использования алгоритмов сжатия пространства состояний, таких как те, которые используются в FDR2.

Проект ProB ^[22] , который размещен в Институте информатики, Университете Генриха Гейне в Дюссельдорфе, изначально был создан для поддержки анализа спецификаций, построенных в методе B. Однако он также включает поддержку анализа процессов CSP как посредством проверки уточнения, так и проверки модели LTL . ProB также может использоваться для проверки свойств объединенных спецификаций CSP и B. Аниматор ProBE CSP интегрирован в 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 или вдохновлены им, в том числе:

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

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

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

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

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

Награда

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

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

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

Ссылки

1. Роско, AW (1997). Теория и практика параллелизма (PDF) . Prentice Hall . ISBN 978-0-13-674409-2.
2. Inmos (1995-05-12). Справочное руководство по occam 2.1 (PDF) . SGS-Thomson Microelectronics Ltd., документ INMOS 72 occ 45 03.
3. Cox, Russ. "Bell Labs and CSP Threads" . Получено 2010-04-15 .
4. "10 академических и исторических вопросов" . Получено 2021-11-15 .
5. "FAQ: Зачем строить параллелизм на идеях CSP?". Язык программирования Go . Получено 15.10.2021 .
6. Хики, Рич (28.06.2013). "Clojure core.async Channels" . Получено 15.10.2021 .
7. Hoare, CAR (1978). «Взаимодействующие последовательные процессы». Сообщения ACM . 21 (8): 666–677. doi : 10.1145/359576.359585 . S2CID  849342.
8. Абдалла, Али Э.; Джонс, Клифф Б.; Сандерс, Джефф У. (2005). Коммуникационные последовательные процессы: первые 25 лет. LNCS . Том 3525. Springer. ISBN 9783540258131.
9. Barrett, G. (1995). «Проверка моделей на практике: процессор виртуальных каналов T9000». Труды IEEE по программной инженерии . 21 (2): 69–78. doi :10.1109/32.345823.
10. Hall, A; Chapman, R. (2002). «Корректность по конструкции: разработка коммерческой безопасной системы» (PDF) . IEEE Software . 19 (1): 18–25. CiteSeerX 10.1.1.16.1811 . doi :10.1109/52.976937. 
11. Creese, S. (2001). Независимая от данных индукция: проверка модели CSP сетей произвольного размера (D. Phil.). Оксфордский университет . CiteSeerX 10.1.1.13.7185 . 
12. Hoare, CAR (1985). Коммуникационные последовательные процессы . Prentice Hall. ISBN 978-0-13-153289-2.
13. Клингер, Уильям (июнь 1981 г.). Основы семантики акторов (докторская диссертация по математике). MIT. hdl :1721.1/6935.
14. Брукс, Стивен; Хоар, К. А. Р .; Роско, А. В. (1984). «Теория взаимодействующих последовательных процессов». Журнал ACM . 31 (3): 560–599. doi : 10.1145/828.833 . S2CID  488666.
15. Buth, B.; M. Kouvaras; J. Peleska; H. Shi (декабрь 1997 г.). «Анализ тупиков для отказоустойчивой системы». Труды 6-й Международной конференции по алгебраической методологии и программным технологиям (AMAST'97) . стр. 60–75.
16. Buth, B.; J. Peleska; H. Shi (январь 1999). «Объединение методов анализа динамической блокировки отказоустойчивой системы». Труды 7-й Международной конференции по алгебраической методологии и программным технологиям (AMAST'98) . стр. 124–139.
17. Лоу, Г. (1996). «Взлом и исправление протокола открытого ключа Нидхэма–Шредера с использованием FDR». Инструменты и алгоритмы для построения и анализа систем (TACAS) . Springer-Verlag. стр. 147–166.
18. Scattergood, JB (1998). Семантика и реализация машиночитаемых CSP ( D.Phil. ). Оксфордская вычислительная лаборатория .
19. Роско, AW (1994). «Проверка моделей CSP». Классический ум: Эссе в честь К. А. Хоара . Prentice Hall.
20. "Введение — документация FDR 4.2.4". www.cs.ox.ac.uk .
21. Парашкевов, Атанас Н.; Янчев, Джей (1996). «ARC – инструмент для эффективного уточнения и проверки эквивалентности для CSP». IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96 . pp. 68–75. CiteSeerX 10.1.1.45.3212 . 
22. Leuschel, Michael; Fontaine, Marc (2008). "Probing the Depths of CSP-M: A new FDR-compliant Validation Tool" (PDF) . ICFEM 2008 . Springer-Verlag. Архивировано из оригинала (PDF) 2011-07-19 . Получено 2008-11-26 .
23. Сан, Цзюнь; Лю, Ян; Дун, Цзинь Сун (2009). "PAT: на пути к гибкой верификации в условиях справедливости" (PDF) . Труды 20-й Международной конференции по компьютерной верификации (CAV 2009) . Конспект лекций по информатике. Том 5643. Springer. Архивировано из оригинала (PDF) 2011-06-11 . Получено 2009-06-16 .
24. Сан, Цзюнь; Лю, Ян; Дун, Цзинь Сун (2008). "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit" (PDF) . Труды Третьего международного симпозиума по использованию формальных методов, верификации и валидации (ISoLA 2008) . Коммуникации в области компьютерных и информационных наук. Том 17. Springer. стр. 307–322. Архивировано из оригинала (PDF) 2009-01-08 . Получено 2009-01-15 .
25. Сан, Цзюнь; Лю, Ян; Донг, Цзинь Сун; Чэнь, Чуньцин (2009). "Интеграция спецификаций и программ для спецификации и верификации систем" (PDF) . IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09 . Архивировано из оригинала (PDF) 2011-06-11 . Получено 2009-04-13 .
26. Грин, Марк; Абдалла, Али (2002). «Анализ производительности и настройка поведения для оптимизации коммуникационных систем». Архитектуры коммуникационных процессов 2002 .
27. Брук, Филлип; Пейдж, Ричард (2007). «Ленивое исследование и проверка моделей CSP с помощью CSPsim». Архитектуры процессов взаимодействия 2007 .
28. ISO 8807, Язык спецификации временного упорядочения
29. Geraint Jones (1990). «Острый как бритва: Премия королевы за вычислительную лабораторию». Oxford Magazine (59, четвертая неделя, триместр Тринити).
30. Лен Шустек (март 2009 г.). «Интервью с К. А. Р. Хоаром». Сообщения ACM . 52 (3): 38–41. doi :10.1145/1467247.1467261. S2CID  1868477.

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

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

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

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