Кіріспе

Бір мезгілдестік теориясындағы формалды модель. Компьютер ғылымында, байланысты жолмен орындалатын процестер (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 хабар алмасуы негізінен хабарды жіберуге және қабылдауға қатысатын процестер арасындағы кездесуді қамтиды, яғни жіберуші қабылдаушы оны қабылдауға дайын болғанға дейін хабарламаны жібере алмайды. Керісінше, актерлік жүйелердегі хабар алмасу негізінен асинхронды болып табылады, яғни хабарды беру мен қабылдау бір уақытта болуы міндетті емес, және жіберушілер қабылдаушылар оларды қабылдауға дайын болмас бұрын хабарламаларды жібере алады. Бұл тәсілдер де бір-бірінің қосымшасы ретінде қарастырылуы мүмкін, себебі кездесуге негізделген жүйелер асинхронды хабарлама жүйелері сияқты жұмыс істейтін буферленген байланыс құру үшін пайдаланылуы мүмкін, ал асинхронды жүйелер жіберушілер мен қабылдаушыларды синхрондау үшін хабарлама/құптау протоколын пайдаланып кездесу стиліндегі байланысты құру үшін пайдаланылуы мүмкін. Жоғарыда айтылған қасиеттер міндетті түрде Хоардың бастапқы CSP мақаласына сілтеме жасамайды, бірақ Go және Clojure ядросы сияқты іске асырылымдарда көрінетін идеяның қазіргі заманғы түріне сілтеме жасайды. Асинхронды. Бастапқы мақалада арналар спецификацияның маңызды бөлігі емес еді, ал жіберуші және қабылдаушы процестер бір-бірін аты арқылы анықтайтын.