Облачные вычисления / [Из песочницы] Введение в теорию взаимодействующих последовательных процессов (Communicating Sequential Processes — CSP)

Предисловие

Данный текст является переводом и сокращённым пересказом начальных глав книги Чарльза Э. Хоарома. Целью является ознакомление русскоязычной аудитории с данной алгеброй исчисления процессов, коя нашла достаточно широкое применение в современной вычислительной науке в связи с большим распространением параллельных систем. Наиболее близкими и понятными практическими применениями CSP, думаю, будут являться следующие языки программирования:

• Erlang
• <a rel="nofollow" href="http://ru.wikipedia.org/wiki/Go_(язык_программирования)">Go
• Limbo

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

Введение

Забудьте на время всё что вы знаете о компьютерах и программировании, вместо этого подумайте о объектах вокруг нас, которые могут взаимодействовать с нами или между собой согласно некоторым паттернам поведения. Представьте себе часы, телефон или же автомат по продаже сладостей. Возьмём для примера последний объект, для того что бы его описать определимся с теми действиями автомата, которые нам интересны, и дадим им свои имена. Тогда для простого автомата продающего шоколадку за монетку будет два действия:

• coin — опускание монетки в приёмник монет
• chock — получение шоколадки

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

• in1p — опускание одного рубля
• in2p — опускание двух рублей
• small — получение маленькой шоколадки
• large — получение большой шоколадки
• out1p — получение сдачей одного рубля

Множество имён событий, которые нас интересуют в данном описании объекта, называется алфавитом. Алфавит является неизменным и предопределённым свойством объекта. Логически невозможно что бы объект выполнил действие вне своего алфавита, как невозможно что машина по продаже шоколадок внезапно выдаст нам радиоуправляемый танк. Но в то же время, машина спроектированная для продажи шоколадок может не продать ни одной шоколадки, например потому что она сломалась или же просто потому что никто не хочет шоколадок, но не смотря на это событие chock останется в алфавите машины, даже если оно ни разу не произойдёт.

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

Каждое событие является атомарным, т.е. происходит мгновенно. Для описания события длящегося во времени применяется пара событий: начальное и конечное. В промежутке между ними могут происходить так же и другие события, а значит продолжающиеся во времени события могут перекрываться.

Другой деталью является намеренное отвлечение от точного времени исполнения, что упрощает описание и позволяет применять теорию вне зависимости от вычислительной скорости системы. В случаях же, где время исполнения является критичным, следует рассматривать данный вопрос отдельно от логической корректности дизайна система.

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

При выборе алфавита нам нет нужды разделять события происходящие по воздействию из вне (coin) и события производимые самим объектом (chock).

Введём для описания поведения некоего объекта термин процесс, который может быть описан с позиции ограниченного количества событий из алфавита объекта. Будем придерживаться далее следующего соглашения:

1. Слова начинающиеся с маленькой буквы обозначают отдельные события, например: coin, choc, in2p, out1p, а так же отдельные буквы a, b, c и т.д.
2. Слова в верхнем регистре обозначают процессы, например:
   
   • VMS — простая торговая машина
   • VMС — более сложная торговая машина

   кроме того буквы P, Q, R (применяется в законах) обозначают некие произвольные процессы

3. Буквы x, y, z являются переменными обозначающими событие
4. Буквы A, B, C обозначают множество событий
5. Буквы X, Y являются переменными обозначающими процесс
6. Алфавит процесса P обозначается как αP (альфа P), например:
   
   • αVMS = {coin, choc}
   • αVMС = {in1p, in2p, small, large, out1p}

Процесс с алфавитом A, который никогда не участвует ни в одном из событий из A обозначается как STOP_A.

Префикс

Пусть x это событие, а P это процесс, тогда:

(x → P ) (произносится как «x затем P»)

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

α(x → P ) = αP при условии x ∈ αP

Примеры:

1. Простая торговая машина ломающаяся после отдачи одной шоколадки:
   
   

   (coin → STOP_αVMS )
2. Простая торговая машина ломающаяся после обслуживания двух людей:
   
   

   (coin → (choc → (coin → (choc → STOP_αVMS ))))

   В самом начале машина может принять монетку, но не может отдать шоколадку, но после того как монетка вставленна машина больше не будет принимать монеты пока шоколадка не будет извлечена.

3. Указатель может двигаться по лабиринту только вверх и вправо по белым клеткам:
   
   

   αCTR = {up, right }
   CTR = (right → up → right → right → STOP_αCTR )

В третьем примере мы упростили запись опусканием скобок приняв соглашение что → ассоциативен справа.

Обратите внимание что следующие записи некорректны синтаксически:

P → Q
x → y

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

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

Таким образом мы чётко разграничиваем событие и процесс участвующий в одном или многих событиях.

Рекурсия

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

Рассмотрим обычные тикающие часы, рассматривая которые нам будут интересны лишь его тики, тогда:

α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. Зачастую удобно записывать это уравнение как:

μX: A•F (X)

где X — локальная переменная, которая может быть измененна:

μX: A•F (X) = μY: A•F (Y)

эквивалентность данных выражений вытекает из того, что уравнения:

X = F(X)
Y = F(Y)

имеют одинаковые решения.

В будущем мы будем использовать оба способа задания процесса: через уравнение и через μ. Во втором случае мы часто будет опускать упоминание алфавита A, т.к. он будет очевиден из контекста.

Примеры:

1. Бесконечные часы:
   
   

   CLOCK = μX: {tick}•(tick → X)
2. Торговый автомат продающий бесконечное количество шоколадок:
   
   

   VMS = μX: (coin → (choc → VMS))

   Как и было указано выше данная запись является укороченным вариантом более формальной записи:

   VMS = μX: {coin, chock}•(coin → (choc → VMS))
3. Машина разменивающая пятирублёвые монетки:
   
   

   αCH5A = {in5p, out2p, out1p}
   CH5A = (in5p → out2p → out1p → out2p → CH5A)
4. Другой вариант разменивающей машины с тем же алфавитом:
   
   

   CH5A = (in5p → out1p → out1p → out1p → out2p → CH5A)

Утверждение о том что защищённое выражение имеет решение и оно возможно уникально можно на пальцах показать через метод подстановок, подставляя в выражение процесс мы его удлиняем, что может продолжаться неограниченно, таким образом мы можем написать произвольно длинное (но конечное) описание процесса, а если два процесса на протяжении произвольно долгого времени ведут себя одинаково, то мы говорим что они одинаковы. Более формальное доказательство невозможно без точного математического определения, которое дано в следующих главах книги.

Заключение

Данная статья не покрыла даже и первой главы книги, но надеюсь дала примерное понимание что из себя представляет CSP и каким языком она пользуется. В дальнейшем в первой главе вводится выбор (для описания ветвления), косвенная рекурсия (для описания более сложных процессов). Доказываются на основе данного примитивного аппарата базовые законы алгебры процессов. Вторая половина первой главы посвящена следам процессов (записи действий произведённых процессов) и операций связанных сними.

Если данная тема будет интересна читателям, я с удовольствием её продолжу.

P.S.: Не смог найти более подходящий блог, если возможно подскажите куда лучше перенести статью.

Автор: newpavlov