A3. stÎ P => P/(st) = ( P/s )( P/t ) ;
A4. s Î A * => A */s = A * ;
A5. s Î P => (c-> P ) / (c-> s ) = P/s ;
A6. c Î P0 - Q0 => ( P | Q ) / ( c-> s ) = (P/< c >) / s ;
A7. c Î P0 Ç Q0 => ( P | Q ) / ( c-> s ) = ( (P/< c >) |(Q/< c >) )/ s ;
A8. s Î P - ( s=<> )Ú ( s0Î P0 & s' Î P/< s0> ) .
Замечание . Свойство A8 означает , что если известно P0 и для
любого c Î P0 определен процесс P/< c> , то процесс определен полностью . Отсюда следует , что можно ввести другой способ
определения процесса , который предусматривает определение процесса парой ( I , F ),где множество I -начальное состояние процесса , а функция F отображает каждый элемент c Î I в процесс P/< c > (по аналогии с определением автомата - функция переходов ) . Отсюда , в дополнение к теоретико-множественному способу определения , вводится так называемое процедурное определение процесса . Процедурное определение процесса является более адекватным с точки зрения реализации процесса в отличие от теоретико -
- множественного определения .
С другой стороны для исследования свойств процессов более удобным
является теоретико- множественная модель , представляющая достаточ-но эффективную математическую базу для формулировки и доказа-тельства свойств процессов . Существуют также и другие модели представления процессов в теории CSP , которые не рассматриваются
в рамках данного пособия .
Примеры процедурного определения.
А) Для процесса R = ( c-> P ) :
R0 = { c } &
R /< c > = P
.
Б) Для процесса R = ( a-> P ) | ( b-> Q ) :
R0 = { a, b } &
ì P , если x=a
R /< x > = í
î Q , если x=b .
B) Для процесса R = P | Q :
R0 = P0 È Q0 &
ì P , если x Î P0 - Q0
R /< x > = í Q , если x Î Q0 - P0
î P/<x> | Q/<x> , если x Î P0 Ç Q0 .
Упражнения к разделу . Доказать свойства A1 -A8 .
2.5.2.5. Последовательная композиция .
Если P и Q -процессы , то последовательная композиция (P; Q) выполняется как процесс P до успешного завершения P , затем выполняется как процесс Q . Если процесс P не завершается успешно , то переход на выполнение процесса Q не может быть осуществлен . Признаком успешного завершения процесса (следа ) является событие успешного завершения , обозначаемое символомÖ . Формально последовательная композиция определяется следуюшим образом :
(P; Q) = df { s; t | sÎ P & tÎ Q } .
Определим процесс SKIP = df { <> , < Ö > } , который понадобится нам в
дальнейших рассуждениях . Также , как процесс FAIL , процесс SKIP
" ничего не делает ", но в отличие от процесса FAIL завершается всегда
успешно .
Cправедливы следующие свойства :
S1. SKIP , (P; Q) являются процессами ;
S2 (P;Q ) ; R = P;(Q;R) ( свойство ассоциативности ) ;
S3. FAIL ; P = FAIL ;
S4. SKIP ; P = P;SKIP = P ;
S5. (c-> P ) ; Q =c-> (P ; Q) , если с ¹ Ö ;
S6. ( P | Q ) ; R = ( P ; R ) | ( Q ; R ) ;
S7. ( P ; Q ) 0 = P 0 , если Ö Ï P 0 ;
S7'. ( P ; Q ) 0 = ( P 0 - { < Ö > } ) È Q 0 , если Ö Î P0 ;
Примеры .
А) if b then P = (b->P) | (ù b -> SKIP ) ;
Б) (b->P) | (ù b -> SKIP ); Q = ( b-> ( P;Q )) | (ù b -> Q )
Упражнения к разделу . Доказать свойства S1 -S7' .
2.5.2.6. Параллельная композиция.
Пусть P - процесс в алфавите A , а Q - процесс в алфавите B . Тогда
через PA || B Q обозначается операция параллельной композиции
процессов P и Q в алфавите (A È B) . Каждое событие , принадлежащее
пересечению алфавитов (A Ç B) и соответственно являющееся общим
событием , определяет точку взаимодействия параллельно
выполняемых процессов P и Q . Событие из множества A-B предполагает участие только процесса P , а событие из множества B-A предполагает участие только процесса Q . Отсюда следует , что любой след процесса PA || B Q после удаления из него событий из
множества B-A превращается в след процесса P , а после удаления из него событий из A-B превращается в след процесса Q . Приведенные выше рассуждения обосновывает следующее определение параллелизма :
PA || B Q = df { s | sÎ (AÈ B) * & s é A Î P & s é A Î Q }
Cправедливы следующие свойства :
C1. Операция || коммутативна и ассоциативна ;
C2. P ||P = P ; _____
C3. (P ||P) 0 = majority( A Ç B , P0, Q0 ) , где
majority( X , Y , Z ) =( XÇ Y ) È ( YÇ Z ) È ( ZÇ X ) ;
C4. sÎ P || Q => ( P || Q )/s = ( P/( s éaP) ) || ( Q/( s éaQ) ;
Пусть aÎ A-B , bÎ B-A , c,c0,c1Î A Ç B , c0 ¹c1 . Тогда :
C5. ( c->P ) || ( c->Q ) = c -> (P || Q) ;
C6. ( c0-> P) || ( c1-> Q )= FAIL ;
C7. ( a-> P ) || ( c->Q ) = a-> ( P || ( c->Q )) ;
C7'. ( c-> P ) || ( b->Q ) = b-> ( (c->P) || Q ) ;
C8. ( a->P ) || ( b->Q ) = ( a-> ( P || ( b->Q ))) | ( b-> (( a-> P) ||Q ))
2.5.2.7. Взаимодействие параллельных процессов.
Пусть P и Q - параллельно выполняемые процессы . Если
aP Ç aQ = Æ , то это означает , что процессы P и Q не взаимодействуют друг с другом. Однако этот случай не представляет особого интереса в исследовании свойств параллельных процессов , поскольку с точки зрения математической модели при отсутствии взаимодействия безразлично , параллельно выполняются процессы или выполняются последовательно друг за другом. Поэтому будем рассматривать случай , когда aP Ç aQ ¹ Æ .
Взаимодействие параллельно выполняемых процессов осуществляется
путем обмена сообщениями , то есть один из процессов передает сообщение , а другой принимает его. Для передачи данных от одного процесса к другому в теории CSP используются каналы передачи
данных . Вводятся две операции : c ! m -операция передачи
сообщения m через канал c , c ? x -операция приема сообщения из канала с в переменную x . В теории CSP рассматривается случай синхронного взаимодействия процессов , который предусматривает одновременное выполнение операций c ! m и c ? x . Таким образом одновременное выполнение этих операций позволяет трактовать его как единое неделимое событие взаимодействия процессов . Последнее определяется следующим соотношением :
( c!m-> P ) || ( c?x-> F(x) ) = c-> ( P || F(m) ) .
Упражнения к разделу 2.5.2 . Определить следующие процессы :
1) abstar - процесс , принимающий любое количество букв a , после
которого следует любое количество букв b ;
2) anbn - процесс , принимающий любое количество букв a , после
которого следует точно такое же количество букв b ;
3) сопрограмма cor( P, Q ) - процесс , поведение которого определяется
следующей схемой :
P --- off --- off --
¬ ¬¯ ¬¯
¯ ¯
Q-------on ------ , где
{ on , off } Ç ( aP È a Q ) = Æ , a cor( P, Q ) = { on , off } È ( aP È a Q ) ;
выполнение сопрограммы начинается с процесса P , который
выполняется до активизации события off , после которого запускается
процесс Q , который в свою очередь отрабатывает до активизации
события on , после которого продолжает выполняться процесс P ,
и т.п. ) ;
4) stoppable(P) - процесс , который выполняется как P до активизации
события stop , после которого процесс stoppable(P) завершает успешно свою работу ; stopÏ aP , a stoppable(P) = aP È { stop } ;
5) resetable(P) - процесс , который выполняется как P до активизации
события reset , после которого resetable(P) стартует с начала ;
resetÏ aP , a resetable (P) = aP È { reset } .
6) backtrackable(P) - процесс , который выполняется как P до активизации события back , после которого backtrackable (P) стартует с начала ;
backÏ aP , a backtrackable (P) = aP È { back } .
Пример процедурного определения процесса (stoppable(P) ).
stoppable(P) 0 = P0 È { stop } &
ì SKIP , если x = stop
stoppable(P)/<x> = í
î stoppable( P/<x> ) , если x ¹ stop (x) ( xÎ P0 ) .
2.5.3. Язык параллельного программирования OCCAM.
OCCAM - язык высокого уровня, предназначенный для выполнения параллельного программирования и создания транспьютеров . Является результатом совместной разработки корпорации INMOS и Оксфордского университета . Концепция OCCAM базируется на теории взаимодействующих процессов, Свое название получил в честь английского философа XIV в. Уильяма Оккама, поскольку в основе разработки языка был использован провозглашенный им принцип: «Сущность не должна превышать необходимость» («бритва Оккама»). В соответствии с упомянутым принципом из двух одинаково эффективных вариантов решений принимается наиболее простое. Язык OCCAM используется в транспьютерах первых и всех последующих выпусков.
Полное описание языка OCCAM можно найти в книге [9] . Здесь же
ограничимся рассмотрением ряда примеров , с помощью которых
проиллюстрируем основные особенности программирования на
языке OCCAM .
Взаимодействие параллельно выполняемых процессов осуществляется
путем обмена сообщениями . Для передачи данных от одного процесса к другому используются каналы передачи данных и следующие операторы : channel ? variable - ввод сообщения из канала channel
в переменную variable , channel ! expression - вывод значения
выражения expression в канал channel .
Рассмотрим следующий пример . Пусть требуется ввести из канала chan1 некоторое числовое значение в переменную x , затем вывести
в канал chan2 результат возведения этого же числа в квадрат . Схематически это это можно представить так :
chan1 -> |x x*x | -> chan2 .
Соответствующая программа на языке OCCAM выглядит следующим образом :
VAR x:
SEQ
chan1 ? x
chan2 ! x*x
Здесь оператор
SEQ
P
Q
определяет последовательную композицию конструкций P и Q ( P;Q ) .
Теперь потребуем , чтобы этот процесс выполнялся в цикле пока x>0 .
В этом случае мы имеем :
VAR x:
WHILE x>0
SEQ
chan1 ? x
chan2 ! x*x
Рассмотрим теперь следующую конструкцию :
PAR
VAR x:
WHILE x>0
SEQ
chan1 ? x
chan2 ! x*x
VAR y:
WHILE y>0
SEQ
chan3 ? y
chan4 ! y*y
Здесь оператор
PAR
P
Q
определяет параллельную композицию конструкций P и Q ( P ||Q ) .
В этом случае мы имеем два независимых параллельных процесса :
chan1 -> |x x* x |-> chan2
chan3 -> |y y* y | -> chan4
Теперь преобразуем приведенную выше следующим образом :
chan1 -> |x x * x |