Введение

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

В информатике, коммуникационные последовательные процессы (CSP) — это формальный язык для описания моделей взаимодействия в конкурентных системах. Он относится к семейству математических теорий параллелизма, известных как алгебры процессов или исчисления процессов, основанных на передаче сообщений по каналам. CSP оказал значительное влияние на разработку языка программирования occam, а также повлиял на разработку языков программирования, таких как Limbo, RaftLib, Erlang, Go.

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

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

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

Синтаксис

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

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

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

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

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

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