lect05 (К. Савенков - Верификация программ на моделях (2010)), страница 2

V1 ∩V2= ), формулаTS ( PG1 ) ||| TS ( PG2 )достоверно описывает параллельную композициюPG1 и PG2а если разделяемые переменные есть?Разделяемые переменные(пытаемся сначала раскручивать, затем чередовать)x = x *2 ||| x = x + 1 (в начале x = 3)αx=3α |||x=6βx=3β x=4αx = 3, x = 3βx = 6, y = 3x = 3, y = 4βαx = 6, x = 4Чередование графов программ• Пусть PGi  Loci , Acti , Effecti , i , Loc0,i , g0,i , i  1,2• Граф PG1 ||| PG2 над V1  V2 определяется такLoc1  Loc2 , Act1  Act2 , , Effect , Loc0,1  Loc0, 2 , g0,1  g0, 2где отношение перехода  определяется правиламиg:l1 1 l1 'g:l1 , l2 l1 ' , l2иg:l2 2 l2 'g:l1 , l2 l1 , l2 'и Effect ( , )  Effecti ( , ), если   Acti .Примерx = x *2 ||| x = x + 1 (в начале x = 3)αβαx=3βx=6x=4x=7x=8TS ( PG1 ) ||| TS ( PG2 )  TS ( PG1 ||| PG2 )Параллелизм и рандеву• Распределённые программы выполняютсяпараллельно;• Для моделирования взаимодействиянеобходимо придумать подходящиймеханизм;• В распределённой программе разделяемыхпеременных нет;• Передача сообщений:– синхронная передача сообщений (рандеву),– асинхронная передача сообщений (каналы).Рандеву• Распределённые процессы, взаимодействующиепри помощи синхронного обмена сообщениями– процессы вместе выполняют синхронизированныедействия,– взаимодействие обоих процессов происходитодновременно,– происходит “рукопожатие”;• Абстрагируемся от передаваемой информации;• H – набор синхронизированных действий:– действия, не принадлежащие H, независимы ичередуются,– действия из H должны быть синхронизированы.Пример рандеву00scan0storeprt_cmdstore1prt_cmd1printA ||H B ||H Printer1Параллельная композиция101printstoreprt_cmdscan100scan000print001110prt_cmdstore010print111scanprintscan011Рандеву систем переходов• Пусть TSi  Si , Acti , i , I i , APi , Li , i  1,2 и H  Act1  Act2• Тогда TS1 ||H TS2 определяется какS1  S2 , Act1  Act2 , , I1  I 2 , AP1  AP2 , L , где• L( s1 , s2 )  L1 ( s1 )  L2 ( s2 ) ,• отношение перехода  определяется правилами:s1 1 s1 's1 , s2 s1 ' , s2иs2 2 s2 'для   Hs1 , s2  s1 , s2 's1 1 s1 '  s2 2 s2 'для   Hs1 , s2  s1 ' , s2 'интерливинграндевуЗаметим, что TS1 ||H TS2  TS2 ||H TS1 , но (TS1 ||H1 TS2 ) ||H 2 TS3  TS1 ||H1 (TS2 ||H 2 TS3 )Попарное рандеву• Пусть TS1 || ...

|| TSn для H i , j  Acti  Act j с H i , j  Actk  для k  i, j• Пространство состояний TS1 || ... || TSn – этодекартово произведение множеств состояний TSi• для   Acti \ (Hi, j)и0i n0 j n i  jsi i si 's1 ,..., si ,..., sn s1 ,..., si ' ,..., sn• для   H i , j и 0  i  j  nsi i si '  s j j sj's1 ,..., si ,..., s j ,..., sn s1 ,..., si ' ,..., s j ' ,..., snСинхронный параллелизмПусть TSi  Si , Acti , i , I i , APi , Li , i  1,2 иAct  Act  Act , ( ,  )    TS1  TS2  S1  S2 , Act1  Act2 , , I1  I 2 , AP1  AP2 , Lгде L( s1 , s2 )  L1 ( s1 )  L2 ( s2 ) и  определяется так:s1 1 s1 ' s2 2 s2 ' s1 , s2  s1 ' , s2 'chan ch[0]={int}ch!M1 – αch?m – βАсинхронный параллелизм• Процессы взаимодействуют при помощиканалов (c ∈ Chan),• Каналы типизированы по передаваемымсообщениям (dom(c)),• Каналы – FIFO буфера, хранящие сообщения(соотв.

типа),• Емкость канала cap(c) – максимальное числосообщений, которое может буферизоватьканал,• cap(c) = 0 – взаимодействие сводится крандеву.Каналы• Процесс Pi = граф программы PGi + действия обменасообщениями Comm:c!v – передача значения v по каналу cc?x – приём сообщения по каналу c и присвоение его переменной xComm  c! v, c ? x | c  Chan, v  dom(c), x VP , dom( x)  dom(c)• Отправка и приём сообщений:– c!v помещает значение v в конец буфера c (если c не полон),– с?х забирает первый элемент буфера и присваивает егозначение x (если c не пуст),– cap(c) = 0 – у канала c нет буфера, отправка и приёмпроизводятся одновременно (рандеву),– cap(c) > 0 – отправка и приём никогда не происходятодновременно (асинхронная передача сообщений).Системы с каналами• Граф программы PG над (Var, Chan) задаётся сигнатуройPG  Loc, Act , Effect, , Loc0 , g0где Loc  (Cond(VP )  Act )  Loc  Loc  Comm  Loc• Система с каналами CS над (Var , Chan ) задаётся какi0 i  nCS  [ PG1 | ...

| PGn ]где PGi – графы программ над (Vari, Chan)Взаимодействие• Рандевуc!vli '– если cap(c)=0, то процесс Pi может выполнить li ?v– … только если Pj может выполнить l j clj'– эффект соответствует распределённому x = v• Асинхронная передача сообщений––––c!vli 'если cap(c) > 0, то процесс Pi может выполнить li … только если в с хранится меньше cap(c) сообщений,?vPj может выполнить l j cl j ', только если c не пуст… после чего первый элемент v извлекается из c иприсваивается x (атомарно)c!vc?vВыполнимо, еслиЭффектc не полонc не пустEnqueue(c,v)〈x=Front(c);Dequeue(c); 〉Модель на Promelamtype = {msg, ack};chan s_r = [2] of {mtype, bit};chan r_s = [2] of {mtype, bit};active proctype sender(){ bit seqno;do:: s_r!msg,seqno ->if:: r_s?ack,eval(seqno) ->seqno = 1 - seqno;:: r_s?ack,eval(1-seqno)fiod}active proctype receiver(){ bit expect, seqno;do:: s_r?msg,seqno ->r_s!ack,seqno;if:: seqno == expect;expect = 1 - expect::elsefiodmsg(0)ack(0)msg(1)ack(1)Считываем новое сообщениеСохраняем сообщениеИгнорируем сообщениеAlternating Bit Protocol(отправитель)seqno = 1 - seqno2r_s?[ack(eval(seqno))]:r_s?ack(eval(seqno))0nfull(s_r):s_r?msg(seqno)1r_s?[ack(eval(1-seqno))]:r_s?ack(eval(1-seqno))Alternating Bit Protocol(получатель)0expect = 1 - expects_r?[msg,seqno]s_r?msg(seqno)31nfull(r_s):r_s!ack(seqno)seqno == expect:τ (сохраняем сообщение)2! seqno == expect:τ (игнорируем сообщение)Значение канала• Оценка ξ значения канала с – это– отображение канала на последовательностьзначений: : Chan  dom(c) *– такое, что длина последовательности непревосходит ёмкости канала:len ( (c))  cap(c)– при этом  (c)  v1v2 ...vk означает, что v1 –верхнее сообщение в буфере• Исходная оценка 0 (c)   c  ChanОперационная семантика системы с каналами• Пусть CS  [ PG | ...

| PG ] – система с каналами над (Chan, Var), и1nPGi  Loci , Acti , Effecti , i , Loc0,i , g0,i , i  1, n• Система переходов TS(CS) описывается сигнатуройTS (CS )  S , Act , , I , AP, L , где• S  Loc1  ...  Locn   Eval (Var)  Eval (Chan)• Act  (  Act i )  0 i  n•  определяется правилами вывода на сл. слайдах• I  l1 ,..., ln , ,  | i (li  Loc0,i   g0 )  c(0 ( c)   )• AP  (  Loci )  Cond (Var )0 i  n• L( l1 ,..., ln , ,  )  l1 ,..., ln  g  Cond(Var) | gПравила вывода (I)• Интерливинг для   Actig:li  li 'n gl1 ,..., li ,..., ln , ,  l1 ,..., li ' ,..., ln , ' , • Синхронная передача сообщений черезc  Chan, cap(c)  0?xc!vli cli 'l j l j 'i  jl1 ,..., li ,..., l j ,..., ln , ,  l1 ,..., li ' ,..., l j ' ,..., ln , ' , где   [ x  v ] .Правила вывода (II)• Асинхронная передача сообщений черезc  Chan, cap(c)  0– получить значение по каналу c и присвоить переменной x:li  li 'len ( ( c )  k  0)   ( c )  v1...vk?xl1 ,..., li ,..., ln , ,  cl1 ,..., li ' ,..., ln , ' ,  'где   [ x  v1 ] и  '   [c  v2 ...vk ] .c? x– передать значение v  dom(c) по каналу c:li  li 'len ( ( c )  k  cap( c ))   ( c )  v1...vkc!vl1 ,..., li ,..., ln , ,  l1 ,..., li ' ,..., ln , ,  'c!vгде '   [c  v1...vk v ] .Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениСпасибо за внимание!Вопросы?.