Лекция 8. Графы программ. Системы с каналами взаимодействия. Синхронный и асинхронный параллелизм (К. Савенков - Верификация программ на моделях (2012)), страница 2

 Рандеву  •  Распределённые  процессы,  взаимодействующие  при  помощи  синхронного  обмена  сообщениями  –  процессы  вместе  выполняют  синхронизированные  действия,  –  взаимодействие  обоих  процессов  происходит  одновременно,  –  происходит  “рукопожатие”;  •  Абстрагируемся  от  передаваемой  информации;  •  H  –  набор  синхронизированных  действий:  –  действия,  не  принадлежащие  H,  независимы  и  чередуются,  –  действия  из  H  должны  быть  синхронизированы.    Пример  рандеву  0  scan  0  0  store  prt_cmd  store  1  prt_cmd  1  print  A ||H B ||H Printer1  Параллельная  композиция  101  print  scan  100  scan  000  store  print  prt_cmd  001  110  prt_cmd  010  print  store  111  scan  print  scan  011  Рандеву  систем  переходов  •  Пусть  TS        i    =          S    i  ,  Act          i  ,    →      i  ,    I  i  ,    AP        i  ,  L    i      ,  i    =      1    ,  2    и      H        ⊆       Act1 ∩ Act2•  Тогда    TS            1    ||    H        TS            2      определяется  как     S1 × S2 , Act1 ∪ Act2 , →, I1 × I 2 , AP1 ∪ AP2 , L , где•  L    (        s  1    ,    s  2        )    =        L    1    (  s    1    )    ∪        L      2  (    s    2    )  ,  •  отношение  перехода  →            определяется  правилами:  α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 )Попарное  рандеву  •  Пусть    TS      1    ||...

         ||    TS        n    для            H      i,    j  !        Act        i    "      Act          j        с      H      i,    j  "      Act          k    =      #          для            k    $      i,    j      •  Пространство  состояний      TS          1    ||      ...        ||      TS          n      –  это  декартово  произведение  множеств  состояний  TSi    •  для     α ∈ Acti \ (  H i , 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 ⎯⎯→s'∧s⎯⎯→i ij sj'jαs1,..., si ,..., s j ,..., sn ⎯⎯→s1,..., si ' ,..., s j ' ,..., snСинхронный  параллелизм  Пусть TSi = Si , Act i , →i , I i , APi , Li , i = 1,2 и∃Act × Act → Act , (α , β ) → α ∗ βTS1 ∗ TS2 = S1 × S2 , Act1 ∪ Act2 , →, I1 × I 2 , AP1 ∪ AP2 , Lгде    L    (        s    1  ,    s    2      )      =        L    1    (    s    1  )      ∪        L      2    (    s    2  )      и      →            определяется  так:  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  по  каналу  c  c?x  –  приём  сообщения  по  каналу  c  и  присвоение  его  переменной  x    Comm = {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              i    ,  Chan                        )      задаётся  как  0<i ≤ nCS = [ PG1 | ...

| PGn ]  где  PGi  –  графы  программ  над  (Vari,  Chan)  Взаимодействие  •  Рандеву  c!v–  если  cap(c)=0,  то  процесс  Pi  может  выполнить   li ⎯⎯→ li 'c? x⎯ l j '–  …  только  если  Pj    может  выполнить   l j ⎯⎯→–  эффект  соответствует  распределённому  x  =  v  •  Асинхронная  передача  сообщений  c!v–  если  cap(c)  >  0,  то  процесс  Pi    может  выполнить   li ⎯⎯→ li '–  …  только  если  в  с  хранится  меньше  cap(c)  сообщений,  –  Pj    может  выполнить  l    j    ⎯          c⎯→  ⎯  ?    x              l    j  ',  только  если  c  не  пуст  –  …  после  чего  первый  элемент  v  извлекается  из  c  и  присваивается  x  (атомарно)  c!v  c?x  Выполнимо,  если  Эффект  c  не  полон  c  не  пуст  Enqueue(c,v)  〈x=Front(c);Dequeue(c); 〉  Модель  на  Promela  mtype = {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)msg(1)ack(0)ack(1)Считываем  новое  сообщение  Сохраняем  сообщение  Игнорируем  сообщение  Alternažng  Bit  Protocol  (отправитель)  seqno  =  1  -­‐  seqno  2  r_s?[ack(eval(seqno))]:  r_s?ack(eval(seqno))  0  nfull(s_r):s_r!msg(seqno)  1  r_s?[ack(eval(1-­‐seqno))]:  r_s?ack(eval(1-­‐seqno))  Alternažng  Bit  Protocol  (получатель)  expect  =  1  -­‐  expect  0  s_r?[msg,seqno]  s_r?msg(seqno)  3  1  nfull(r_s):  r_s!ack(seqno)  seqno  ==  expect:  τ  (сохраняем  сообщение)  2  !  seqno  ==  expect:  τ  (игнорируем  сообщение)  Значение  канала  •  Оценка  ξ  значения  канала  с  –  это    –  отображение  канала  на  последовательность  значений:  ξ : Chan → dom(c) *–  такое,  что  длина  последовательности  не  превосходит  ёмкости  канала:  len (ξ (c)) ≤ cap(c)–  при  этом      ξ      (    c    )      =      v    1  v      2  ...

       v    k      означает,  что  v1  –  верхнее  сообщение  в  буфере  •  Исходная  оценка     ξ0 (c) = ε ∀c ∈ ChanОперационная  семантика  системы  с  каналами  •  Пусть      CS                =        [      PG              1    |    ...          |    PG                n    ]        –  система  с  каналами  над  (Chan,  Var),  и    PGi = 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   = (  Acti ) ∪ τ0<i ≤n• • • →            определяется  правилами  вывода  на  сл.  слайдах  I     = { l1,..., ln ,η, ξ | ∀i(li ∈ Loc0,i ∧η g0 ) ∧ ∀c(ξ0 (c) = ε )}     = (  Loci ) ∪ Cond (Var )AP0<i ≤n•  L    (   l1,..., ln ,η, ξ ) = {l1,..., ln }∪ {g ∈ Cond (Var) | ηg}Правила  вывода  (I)  •  Интерливинг  для   α ∈ Actig:αli ⎯⎯→ li '∧η 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:  ?xli ⎯c⎯→⎯li '∧len (ξ ( c ) = k > 0) ∧ ξ ( c ) = v1...vk?xl1 ,..., li ,..., ln ,η , ξ ⎯c⎯→⎯l1 ,..., li ' ,..., ln ,η ' , ξ 'где    η          =      η      [      x      =        v      1  ]      и        ξ      '    =      ξ      [    c        =        v    2    ...        v    k      ]    .  –  передать  значение  v      ∈        dom                  (c        )      по  каналу  c:  c!vli ⎯⎯→ li '∧len (ξ ( c ) = k < cap( c )) ∧ ξ ( c ) = v1...vkc!vl1 ,..., li ,..., ln ,η , ξ ⎯⎯→l1 ,..., li ' ,..., ln ,η , ξ 'где    ξ      '    =        ξ      [    c      =        v    1    ...

       v    k    v      ]    .  Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Спасибо за внимание!Вопросы?.