5 - Графы программ. Системы с каналами взаимодействия. Синхронный и асинхронный параллелизм (1161369)

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

Текст из файла

Верификация программна моделяхЛекция №5Графы программ. Системы с каналамивзаимодействия. Синхронный иасинхронный параллелизмКонстантин Савенков (лектор)План лекции• Alternating Bit Protocol• Графы программ• Операционная семантика графовпрограмм:– последовательные процессы,– чередование,– разделяемые переменные,– синхронная и асинхронная передачасообщенийAlternating Bit Protocol(Bartlett и др., 1969)• Два процесса, отправитель и получатель;• К каждому сообщению добавляется один бит;• Получатель сообщает о доставке сообщения,возвращая бит отправителю;• Если отправитель убедился в доставкесообщения, он отправляет новое, изменяязначение бита;• Если значение бита не изменилось, получательсчитает, что идёт повтор сообщения.Функция eval()Отображает текущее значение xна константу, которая служитограничением дляпринимаемых сообщенийch!msg(12)ch?msg(eval(x))Сообщение будет принято, если значение переменной x равно 12Модель на 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)Считываем новое сообщениеСохраняем сообщениеИгнорируем сообщениеЗапускаем моделирование>./spin -u20 -c abp.pmlproc 0 = senderproc 1 = receiverq\p011s_r!msg,01.s_r?msg,02.r_s!ack,02r_s?ack,01s_r!msg,11.s_r?msg,12.r_s!ack,12r_s?ack,1------------depth-limit (-u20 steps) reached------------final state:------------#processes: 2queue 1 (s_r):queue 2 (r_s):20:proc 1 (receiver) line 19 "abp.pml"(state 7)20:proc 0 (sender) line7 "abp.pml"(state 7)2 processes created>Моделируем первые 20 шаговВерификация по умолчанию>./spin -a abp.pml> gcc -o pan pan.c>./pan(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claimassertion violationsacceptancecyclesinvalid end states- (none specified)+- (not selected)+State-vector 44 byte, depth reached 13, errors: 014 states, stored1 states, matched15 transitions (= stored+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)unreached in proctype senderline 15, state 10, "-end-"(1 of 10 states)unreached in proctype receiverline 27, state 10, "-end-"(1 of 10 states)>Чем и как проверяем?Какие свойства?Проделанная работаИспользуемая памятьОбнаруженнедостижимый код(процессы незавершаются)Графический интерфейс xspinПространства состояний в SPIN(«отладка» процесса верификации)Полезные инструменты• Просмотр пространства состояний:– параметры компиляции pan.c:• -DCHECK – выводить порядок обхода пространства состояний• -DVERBOSE -DSDUMP – выводить вектора состояний• -DBFS – обход в ширину (удобнее для анализа)– параметры запуска pan:• -d – вывод графов процессов (state – номер оператора)• Отключение оптимизаций:– параметры spin:• -o1 – отключение оптимизации потока данных,• -o2 – отключение удаления мертвых переменных,• -o3 – отключение слияния состояний– параметры компиляции pan.c:• -DNOREDUCE – отключение редукции частичных порядковОбратите внимание:• инициализация переменной (int x = 1) несчитается действием;• порождение (run) и завершение процесса –действия,– при использовании active в начальном состояниипроцесс уже запущен,– не только терминальное состояние, но итерминальное действие -end-;• процессы порождаются в случайном порядке,но завершаются в только порядке, обратномпорядку порождения (LIFO);• проверка стража ветвления – действие.Графы программСхема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениРазличные представленияпрограммыt t lt l ll t lltintmain(){printf(}Исходный кодпрограммыВзлетает,непадает,приземляетсяТребованияГраф программы(ACFG)□(TAKEOFF→(!FALL)U(LANDED))РазмеченнаясистемапереходовlllМножествовычисленийl l tt t ll ll lСпецификацияДопустимые(линейного времени) последовательностиатомарных высказыванийМножествотрассl=Tt=TtltЯзыкдопустимых трассРазмеченные системы переходов(напоминание)• описывают поведение системы;• ориентированный граф: узлы – состояния,дуги – переходы;• состояние – счётчик управления + значенияпеременных программы;• переход (изменение состояния) –выполнение оператора программы.Размеченные системы переходов(напоминание)TS  S , Act , , I , AP, La• S – множество состояний,• Act – множество действий, τ – невидимое действие,a  S  Act  S – тотальное отношение• переходов,• I  S – множество начальных состояний,• AP – множество атомарных высказываний,• L : S  2 AP – функция разметки.Формальное представлениепрограммы• LTS – всевозможные состояния программы ипереходы между ними;• Однако модель строится в виде программы наспециальном языке;• Рассуждения о корректности необходимоперенести на текст программы-модели;• Для этого понятие описания программынеобходимо формализовать;• Формальное представление программы: графпрограммы и его семантика.Формальное представлениепрограммы1.

граф, задающий структуру программы;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}VEQ  {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.

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

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций