Внедрение CSP (передача последовательных процессов) в Scala

Question

Я пытаюсь реализовать парсер и семантику для CSP в Scala . Я уже реализовал синтаксический анализатор, и теперь я занят работой над семантической частью языка. Я совершенно новичок в мире параллельных систем и недетерминированных выборов. Вот мой вопрос:

Я хочу реализовать "Недетерминированный выбор" и "Параллель интерфейса", как описано здесь.

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

Кто-нибудь сталкивался с этой проблемой раньше и знает хороший алгоритм?

Answer 1

Мое очень ограниченное понимание CSP заключается в том, что операторы CSP соответствуют следующим типам Haskell:

-- Prefixing corresponds to functions
x :: A
P :: B
x -> P :: A -> C

-- Choice corresponds to product
P :: A
Q :: B
P □ Q :: (A, B)

-- Non-determinism corresponds to sum
-- I don't know how to make the non-determinism symbol, so I use (△)
P :: A
Q :: B
(P △ B) :: Either A B

Затем вы можете использовать алгебраические изоморфизмы для сокращения выражений CSP. Используя пример из Википедии:

(coin -> STOP) □ (card -> STOP)

-- translates to the following Haskell type:
(coin -> Stop, card Stop)

-- which is algebraically isomorphic to:
(Either coin card -> Stop)

-- translates in reverse back to CSP:
coin □ card -> STOP

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

(a -> a -> STOP) □ (a -> b -> STOP)

-- translates to the following Haskell type:
(a -> a -> STOP, a -> b -> STOP)

-- which is algebraically isomorphic to:
a -> Either a b -> STOP

-- translates in reverse back to CSP:
a -> (a △ b) -> STOP

Я до сих пор не нашел эквивалент параллельного интерфейса. Кажется, это не соответствует элегантной концепции.

Answer 2

Это сложная тема. Сторона разбора - легкая часть. Написание правильных параллельных примитивов очень сложно и почти наверняка потребует формальной проверки с использованием такого инструмента, как FDR.

Если вас интересует только написание части анализатора выражений, а не примитивов параллелизма, вы можете предпочесть использовать JCSP, который уже предоставляет эти примитивы в Java API. Авторы этого (UKC) использовали формальную проверку для проверки его компонентов, особенно канала и альтернативных (выборочных) частей.