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

Верификация  программ  на  моделях  Лекция  №8  Графы  программ.  Системы  с  каналами  взаимодействия.  Синхронный  и  асинхронный  параллелизм  Константин  Савенков  (лектор)  План  лекции  •  Графы  программ  •  Операционная  семантика  графов  программ:  –  последовательные  процессы,  –  чередование,  –  разделяемые  переменные,  –  синхронная  и  асинхронная  передача  сообщений  Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Различные  представления  программы  t   t   l  t   l   l  l   t   l  l  t  int main(){printf(}Исходный  код  программы  Взлетает,непадает,приземляетсяТребования  Граф  программы  (ACFG)  □(TAKEOFF →(!FALL)U(LANDED))Размеченная  система    переходов  Множество  вычислений  l   l   l   t  l   t   t   l  l   l   l  l   l  Спецификация  Допустимые  (линейного  времени)   последовательности  атомарных  высказываний  Множество  трасс  l  =  T  t  =  T  t  l  t  Язык  допустимых  трасс  Размеченные  системы  переходов  (напоминание)  •  описывают  поведение  системы;  •  ориентированный  граф:  узлы  –  состояния,  дуги  –  переходы;  •  состояние  –  счётчик  управления  +  значения  переменных  программы;  •  переход  (изменение  состояния)  –  выполнение  оператора  программы.

 Размеченные  системы  переходов  (напоминание)  aTS = S , Act, ⎯⎯→, I , AP, L•           S        –  множество  состояний,  •         Act                –  множество  действий,    τ    –  невидимое  действие,  a•         ⎯    ⎯→                        =          S        ×        Act                  ×        S      –  тотальное  отношение  переходов,  •         I      ⊆            S      –  множество  начальных  состояний,  •       AP                –  множество  атомарных  высказываний,  •       L        :      S        →              2      AP          –  функция  разметки.  Формальное  представление  программы  •  LTS  –  всевозможные  состояния  программы  и  переходы  между  ними;  •  Однако  модель  строится  в  виде  программы  на  специальном  языке;  •  Рассуждения  о  корректности  необходимо  перенести  на  текст  программы-­‐модели;  •  Для  этого  понятие  описания  программы  необходимо  формализовать;  •  Формальное  представление  программы:  граф  программы  и  его  семантика.

 Формальное  представление  программы  1.  граф,  задающий  структуру  программы;  2.  статическая  семантика  –  набор  ограничений,  которым  должна  удовлетворять  структура;  3.  операционная  семантика  –  понятие  состояния  программы  и  изменение  состояния  в  ходе  работы  программы.  то,  как  по  графу  строится  LTS  Вспомогательные  определения  •  D        P    –  единый  абстрактный  домен  данных  bool z;mtype {M1,M2} m = M1;proctype EQ(byte x, byte y){if:: (x == y) -> z = true:: else -> z = falsefi}DP ≡ intbool ⊂ intbyte ⊂ intmtype ⊂ intВспомогательные  определения  •  V      P      ∈          Var                    –  множество  переменных  (последовательной)  программы      P        ,  v•  ∀     v ∈VP , dom(v ) = DP ⊆ DPbool z;mtype {M1,M2} m = M1;proctype EQ(byte x, byte y){if:: (x == y) -> z = true:: else -> z = falsefi}VEQ = {z, m, x, y}Вспомогательные  определения  •  Функция  означивания  переменной:  vPη : VP → DP , ∀v ∈VP , η (v) ∈ Dbool z;mtype {M1,M2} m = M1;proctype EQ(byte x, byte y){if:: (x == y) -> z = true:: else -> z = falsefi}Примеры:  η (m) = M1 ∈ mtypeη ( x ) = 3 ∈ byteη ( z ) = true ∈ boolВспомогательные  определения  • Cond                        (    V        P    )      –  набор  булевых  условий  над  VP–  формулы  пропозициональной  логики  p1  ∧ p2 ∨ p3  –  используются  высказывания  вида   x ∈ Xp1  ≡  -­‐3  <  x  ≤  5  p2  ≡  m  =  M2  p3  ≡  y  <  2  *  x  Вспомогательные  определения  •  Эффект  операторов  формализуется  как  отображение  Effect : Act × Eval (Var ) → Eval (Var )…x = 17;if:: y = -2:: y = 3fi;…x = y + 5;…Пусть α ≡ x = y + 5,η1, 2 ( x ) = 17, η1 ( y ) = −2,η2 ( y ) = 3ТогдаEffect (α ,η1 )( x ) = η1 ( y ) + 5 = 3Effect (α ,η1 )( y ) = η1 ( y ) = −2Effect (α ,η2 )( x ) = η2 ( y ) + 5 = 8Effect (α ,η2 )( y ) = η2 ( y ) = 3Графы  программ  (статическая  семантика)  PG = Loc, Act, Effect, →, Loc0 , g0•     Loc                    –  множество  точек,  исходные  точки    Loc                0        ⊆            Loc                  ,  •     Act                    –  множество  действий,  •     Effect                          :      Act              ×        Eval                    (  Var                )      →            Eval                    (  Var                )      –  функция  эффекта,  •     →⊆                    Loc              ×        (  Cond                      (    V    P      )    ×        Act              )    ×      Loc                    –  отношение  перехода,  •     g      0    ∈        Cond                      (  V      P      )      –  начальное  условие,  g:αНотация : l ⎯⎯→l ' обозначаетl , g,α , l ' ∈→Пример  графа  программы  0,?,?  00: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:int x = 2;T:x = 2;1,2,?  1int y = 0;T:y = 0;22,2,0  x > 0x <= 0:τT:x -= 1;x > 03,1,1  y += 1;y += 1;T:y += 1;4x -= 1;3,2,0  x > 0:τ32,1,1  4,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)55,0,2  Пример  графа  программы  00: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:T:x = 2;0,  1,  2,  3,  4,  5  1T:y = 0;x > 0:τ3T:y += 1;x <= 0:τ5Act“x=2”,  “y=0”,  “y+=1”,  “x-­‐=1”,  τ  24LocT:x -= 1;Effect→Loc0 ="0"g 0 = ( x =# ) ∧ ( y = # )Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Как  из  PG  получить  TS?  •  Основная  идея  –  раскрутка  –  состояние:  точка  l  +  значение  данных  η  –  начальное  состояние:  начальная  точка  +  все  значения  данных,  удовлетворяющие  g0;  •  Атомарные  высказывания  и  разметка:  –  высказывания  вида:  “в  l”  и  “x∈D”,  где  D⊆dom(x);  –  состояние  <l,η>  размечается  высказыванием  “в  l”  и  всеми  высказываниями,  истинными  в  η;  g:α•  Если      l    ⎯          ⎯→                  l    '  и  g  истинно  в  η,  то  l ,η ⎯⎯→ l ' , Effect(α ,η )αСтруктурированная  операционная  семантика  Нотацияпосылкаследствиеозначает :•  если  посылка  истинная,  то  следствие  также  истинно;  •  это  т.н.

 правило  вывода;  •  если  посылка  тождественно  равна  истине,  то  следствие  –  аксиома.  Системы  переходов    графов  программ  •  Система  переходов  TS(PG)  графа  программы  PG = Loc, Act, Effect, →, Loc0 , g0над  переменными  V        P      описывается  сигнатурой  TS ( PG) = S , Act, →, I , AP, L , гдеS = Loc × Eval (VP )«состояние:  точка  l  +  значение  данных  η»  Системы  переходов    графов  программ  •  Система  переходов  TS(PG)  графа  программы  PG = Loc, Act, Effect, →, Loc0 , g0над  переменными  V        P      описывается  сигнатурой  TS ( PG) = S , Act, →, I , AP, L , гдеI = { l ,η | l ∈ Loc0 ,ηg0 }«начальное  состояние:  начальная  точка  +  все  значения  данных,  удовлетворяющие  g0»  Системы  переходов    графов  программ  •  Система  переходов  TS(PG)  графа  программы  PG = Loc, Act, Effect, →, Loc0 , g0над  переменными  V        P      описывается  сигнатурой  TS ( PG) = S , Act, →, I , AP, L , гдеAP = Loc ∪ Cond (VP )«высказывания  вида:  “в  l”  и  “x∈D”,  где  D⊆dom(x);»  Системы  переходов    графов  программ  •  Система  переходов  TS(PG)  графа  программы  PG = Loc, Act, Effect, →, Loc0 , g0над  переменными  V        P      описывается  сигнатурой  TS ( PG) = S , Act, →, I , AP, L , гдеL( l ,η ) = {l} ∪ {g ∈ Cond (VP ) | ηg}«состояние  <l,η>  размечается  высказыванием  “в  l”  и  всеми  высказываниями,  истинными  в  η»  Системы  переходов    графов  программ  •  Система  переходов  TS(PG)  графа  программы  PG = Loc, Act, Effect, →, Loc0 , g0над  переменными  V        P      описывается  сигнатурой  TS ( PG) = S , Act, →, I , AP, L , где→⊆ S × Act × S задано правиломg:αg:αl ⎯⎯→l '∧η gαl ,η ⎯⎯→l ' , Effect (α ,η )«Если    l    ⎯            ⎯→                    l    '  и  g  истинно  в  η,  то                                                                                              l    ,  η            ⎯      ⎯→    α                    l  '    ,    Effect                        (    α        ,  η        )        »  Системы  переходов    графов  программ  •  Система  переходов  TS(PG)  графа  программы  PG = Loc, Act, Effect, →, Loc0 , g0над  переменными  V        P      описывается  сигнатурой    TS ( PG) = S , Act, →, I , AP, L , где  •   S   = Loc × Eval (VP )g:αl ⎯⎯→l ' ∧n g•   →⊆   S × Act × S задано правилом l ,η ⎯⎯→αl ' , Effect (α ,η )•  I     = l ,η | l ∈ Loc0 , n g0•  AP     = Loc ∪ Cond (VP )•  L    ( l ,η ) = {l} ∪ {g ∈ Cond (VP ) | n g}{}Параллелизм  Чередование  (интерливинг)  (напоминание)  •  Абстрагируемся  от  того,  что  система  состоит  из  множества  компонентов;  •  Действия  независимых  компонентов  чередуются:  –  доступен  один  процессор,  выполнение  одного  действия  блокирует  другие;  •  Порядок  выполнения  процессов  неизвестен  –  Возможные  порядки  выполнения  независимых  процессов  P  и  Q:  PPPQPQPQPQPPPPQQQPQPPQPPPQQ.

. .. . .. . .Чередование  (интерливинг)  •  Обоснование  чередования:    эффект  от  параллельного  выполнения  независимых  действий  α  и  β  равен  эффекту  от  последовательного  выполнения  действий  α  и  β  в  произвольном  порядке;  •  Символьная  запись:  Effect (α ||| β ,η ) = Effect ((α ; β ) + ( β ;α ),η )–  «  |||    »    –  бинарный  оператор  чередования,  –   «;»  –  оператор  последовательного  выполнения,  –  «+»  –  оператор  недетерминированного  выбора.

   Чередование  (интерливинг)  x  =  x  +  1   ||| y  =  y  -­‐  2  α  x  =  0  α   |||x  =  1  y  =  7  β   =y  =  5  β  α  x  =  0,  y  =  7  x  =  1,  y  =  7  β  β  x  =  0,  y  =  5  x  =  1,  y  =  5  α  Чередование  систем  переходов  •  Пусть      TS          i    =            S    i  ,    Act            i  ,    →        i    ,    I  i  ,    AP          i  ,    L      i    ,    i      =      1    ,  2        –  две  системы  переходов  •  Система  переходов  TS            1      |||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 'αs1 , s2 ⎯⎯→s1 , s2 'Чередование  графов  программ  •  Для  графов  программ  PG1  (над  V1)  и  PG2  (над  V2)  без  разделяемых  переменных  (т.е.

 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,  x  =  3  β  β  x  =  3,  x  =  4  x  =  6,  x  =  4  α  Чередование  графов  программ  •  Пусть    PG          i    =          Loc            i  ,    Act            i  ,  Effect                    i  ,    →        i  ,  Loc              0  ,i    ,  g    0    ,i   , i = 1,2•  Граф    PG              1      |||      PG              2    над    V      1    ∪          V      2    определяется  так  Loc1 × Loc2 , Act1 ∪ Act2 , →, Effect, Loc0,1 × Loc0,2 , g0,1 ∧ g0,2где  отношение  перехода    →            определяется  правилами  g:αg:α  l1 ⎯⎯→l'l⎯⎯→1 12 l2 '2иg:αg:α  l1 , l2 ⎯⎯→ l1 ' , l2l1 , l2 ⎯⎯→l1 , l2 '  и Effect (α ,η ) = Effecti (α ,η ), если α ∈ Acti .Пример  x  =  x  *2   ||| x  =  x  +  1   (в  начале  x  =  3)  α  β  α  x  =  3  β  x  =  6  x  =  4  x  =  7  x  =  8  TS ( PG1 ) ||| TS ( PG2 ) ≠ TS ( PG1 ||| PG2 )Параллелизм  и  рандеву  •  Распределённые  программы  выполняются  параллельно;  •  Для  моделирования  взаимодействия  необходимо  придумать  подходящий  механизм;  •  В  распределённой  программе  разделяемых  переменных  нет;  •  Передача  сообщений:  –  синхронная  передача  сообщений  (рандеву),  –  асинхронная  передача  сообщений  (каналы).