lect_all (1161275), страница 6

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 6)

граф, задающий структуру программы;2. статическая семантика – наборограничений, которым должнаудовлетворять структура;3. операционная семантика – понятиесостояния программы и изменениесостояния в ходе работы программы.то, как по графу строится LTSВспомогательные определения• DP – единый абстрактный домен данных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Вспомогательные определения• VP 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}VMAX  {z, m, x, y}Вспомогательные определения• Функция означивания переменной: : VP  DP , v VP ,  (v )  DvPbool 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 (VP ) – набор булевых условий над VP– формулы пропозициональной логикиp1 ∧ p2 ∨ p3– используются высказывания вида x  Xp1 ≡ -3 < x ≤ 5p2 ≡ m = M2p3 ≡ 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 – множество точек, исходные точки Loc0  Loc ,•Act– множество действий,• Effect : Act  Eval (Var)  Eval (Var) – функция эффекта,•  Loc  (Cond(VP )  Act )  Loc – отношение перехода,• g0  Cond(VP ) – начальное условие,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;:x = 2;1,2,?1int y = 0;:y = 0;22,2,0x > 0x > 0:τ3x <= 0:τx -= 1;3,2,0:x -= 1;x > 03,1,1y += 1;y += 1;:y += 1;42,1,14,2,14,1,2x -= 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::x = 2;0, 1, 2, 3, 4, 51:y = 0;2x > 0:τ3:y += 1;4x <= 0:τ5Loc:x -= 1;Act“x=2”, “y=0”,“y+=1”, “x-=1”, τEffectLoc0 "0"g0  ( 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над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеS  Loc  Eval (VP )«состояние: точка l + значение данных η»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеI   l , | l  Loc0 ,g0 «начальное состояние: начальная точка +все значения данных, удовлетворяющие g0»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатурой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над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , гдеL( l , )  {l}  g  Cond(VP ) | g«состояние <l,η> размечается высказыванием “в l”и всеми высказываниями, истинными в η»Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , где S  Act  S задано правиломg:l l ' gl , l ' , Effect ( , )g:«Если l l ' и g истинно в η, тоl ,  l ' , Effect ( , ) »Системы переходовграфов программ• Система переходов TS(PG) графа программыPG  Loc, Act , Effect, , Loc0 , g0над переменными VP описывается сигнатуройTS ( PG )  S , Act , , I , AP, L , где•••••S  Loc  Eval (VP ) S  Act  S задано правиломg:l l ' n gl , l ' , Effect ( , )I   l , | l  Loc0 , n g0 AP  Loc  Cond(VP )L( l , )  {l}  g  Cond (VP ) | ngПараллелизмЧередование (интерливинг)(напоминание)• Абстрагируемся от того, что система состоит измножества компонентов;• Действия независимых компонентов чередуются:– доступен один процессор, выполнение одного действияблокирует другие;• Порядок выполнения процессов неизвестен– Возможные порядки выполнения независимыхпроцессов P и Q:PPPQPQPQPQPPPPQQQPQPPQPPPQQ.

. .. . .. . .Чередование (интерливинг)• Обоснование чередования:эффект от параллельного выполнениянезависимых действий и равен эффектуот последовательного выполнения действийи в произвольном порядке;• Символьная запись:Effect ( |||  , )  Effect (( ;  )  (  ; ), )– « |||» – бинарный оператор чередования,– «;» – оператор последовательного выполнения,– «+» – оператор недетерминированного выбора.Чередование (интерливинг)x = x + 1 ||| y = y - 2αx=0α |||x=1y=7β y=5βαx = 0, y = 7βx = 1, y = 7x = 0, y = 5βαx = 1, y = 5Чередование систем переходов• Пусть TSi  Si , Acti , i , I i , APi , Li , i  1,2– две системы переходов• Система переходов TS1 |||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 '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 = 3x = 3, x = 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 буфера, хранящие сообщения(соотв.

Характеристики

Список файлов лабораторной работы