2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 6
Текст из файла (страница 6)
Поскольку студент еще и учится, ему выплачнваетса стипендия. Как троечнику, ему полагаеюя стипендия всего в 15 долларов. Бухгвлтерашя программа БухСофт2 универсспета в конце месяца должна увеличить счет этого студент» на 15 долларов. Таким образом, в двух независимых процессорах даа параллельных процесса независимо выполнают операции над одним элементом общей памяти: БулСофт1 з Х„ш Х„+ 3000 БуяСофт2:Х„ж Х„+15 К концу месяца студент рассчитывает, по после двух выплат у него на счете будет 3015 долларов, достаточные для покупки подеряшн ной иномарки.
К его ршочарованию, на счете оказалось только 15 доллщюв, хотя обе программы отработали и, по распечаткам, все дены и ему переведены. Причиной некорректности является ошибка в разработанной студентом про. грамме: отсутствие синхронизации двух параллельных процессов, выполняющих одновременный доступ к общим данным.
Подобные ошибки типичны в программах, разработанных студентамн-недоучками, пропускавшими лекции по теории параллельных процессов. Хотя операция начисления зарплаты записывается как Хп. Ха+С, реапьноь каждом процессе она выполняется как три неделимых операции: 1. Чтение в регистр значения из памяти. 2. Увеличение значения регистра. 3. Запись значения мз регистра в память, Если процесс Б]аСгьфт1 выполняет все три свои операции либо ДО, либо ПОСЛЕ того, как процесс БухСгпфьт2 выполмит все свои операции, то значение Х„в результате увеличится на С, + Сз, т.
е. программы будут работать правильно. Существует, однако, очень малаа вероятносп того, что этн дае группы операций будут выполняться независимо работающими процессамн приблизительно в одно время. В этом случае асинхронное параллельное выполнение незавнсимык процессов может привести к тому, что неделимые микрокоманды размых процессов будут выполняться по очереди в некотором порядке. В итоге мы можем получить невкигщнный результат: одно из маме пений значения обшей перемеммой, которое выполняет либо один, либо другой процесс, будет шперяно.
Таким образом, бухгалтерская программа, разработаннап студентом, работвег корректно "почти" все время, но иногда, очень редко, программа будет работать неправильно. Выявить подобные тонкие ошибки синхронизации параллельных процессов никаким тестированием невозможно, они зависят от относительных скоростей процессов, времени начала выполнения операций ит. п. Приывр 1.2 Программа ршпелення множеств 1165].
Эта просим программа состоит из двух параллельно фумкционируюших взаимодействующих процессов, ппащ и ьагде. Процесс жмщ оперирует на конечном множестве чисел з, проилсс ьагде оперирует на конечном множестве ь. Процессы зппю и пегое взаимодействуют посредсгвом посылки сообщений, обмениваясь числами из этих множеств по каналу с1 ст аы11 к затяге И ПО КанЩГУ сэ ог загсе К апаш ДО тех пор, пока в з не соберутся все минимальные значения обоих множеств, а в ь не ссберугся максимальные значения множеств.
лмее ( Рве. 1Л. Пврвшвльвал программа ранмлвппв миоаеств Процесс аы11 на шокдом шаге ищет максимальное значение в мнохистве з и посылает его процессу ьвкдв по каналу с(, затем принимает ст мыл найденное этим процессом минимальное значение 1, посланное пб капаау сг! Вв»11! ! веем ах! ввх(51! с1(ки; 5! 5-(ивх(5) (! с22х! 5! 94х(! ви! »их(5(! '(ив>к -в /7 цикл выполи»овся, пока па>к с1(ввв! 5! 5 два!(5(1' с2?к! ш алх(! вх! вах(51! Процесс ьвв!(в на шпкдом шаге принимает от шаш найденное им максимальное значение з, вкланное по каналу с~ сам ишет минимальное значение .
во мнакестве ь и шшылжт его процессу пввш по каналу с(( ьвгдв!! ьвдпв с(гу! ы-(вду(! ва! Ып(Ы! сг(ва! ь! 1 (ва(! ип! в1п(ш! [васу в // цикл вылови»сто», пока ил<у с12у! ь! илу(! «а! в1п(ш! с2!ап! Ь! Ь (ка(! вп!ав(п(Ь) Взаимодействие по каналам с( н сг очень простое — зто сннхроннал коммуникецив (хзндшейк, рандеву), прн которой посылка одним пропаном данных в канал момет быль выполнена в том и только в том случае, если другой процесс готов прочесть зтн данные. Почти на всех вариаипш исходных двииыр эта параллельиая программа работает верно: процессы завершаются, по их завершении есе даиные сохраияются, число значений в кажаом мивкесгве не изменяется, каждый элемент з не больше каждого элемеигз ь.
Очень редко при некотором вполие определенном соотношении между зиачеииями элементов множеств з и ь эта параллельная программа работает некорректно: один из процессов будет бесконечно шкидать коммуникации с другим, который до этого благополучно завершился. Правильность ягой программы иельзя доказать тестированием: почти на всех наборах исходных данных зта программа работает правильно. Только строгий формальный анализ, верификация программы может обиарухапь ошибку. Пример 1.3 Протокол )У.С.Еупсй (105).
Зтст протокол был приведен Уильямом Линчем как пример убедительно выглшшщей, но некорректной распределенной программы, опубликованной "одним иэ основных производителей вычислительной техники". Цель протокола — полнодуплексная передача (т. е, одновременная передача в обоих направлениях) последовательностей символов через иеиаямкиую среду между пользователями а и в. Каждое сообщение имеет две части: информационный символ и управляющую часть. Управляющая часть принятого сообщения всегда содержит один из трех управляющих символов: еск саек или вгг. Если сообщение принято без ошибок, оио содержит «ск или саек в управляющей части.
Какал мшкет поискать сообщения, но не мсжет терять, дублировать или вставлять новые. Предполагается, что все ошибки передачи обнаруживаются июкним уровнем протокола, верхний уровень при этом получает символ егг в управляющей части сообшеииа. Правила фуикциоиироввнмя протокола описываются его разработчиком так: "В ответном сообщении в управлающей его части посылается пгжожительиое подтверждение асц если получеииое перев этим сообщение ие содержало ошибок, в ответ посылается отрицательное подтверждение пасв, если было прииато ошибочное сообщение.
Если получеииое сообщение несло отрицкшльиое подтверждение или само оказалось ошибочным, то в ответ посылаются старые данные, в противиом случае пссылакпся следующие данные". Формаяизоеаннсе представление этих прямил в стиле ЗПЬ дано иа рис. 1.2, ж Схема полностью соответствует правилам: полученное новое сообщение мгс может иметь три возможных типа (три разных значения в управляющей части). Если пришло неискаженное сообщение, которое содержит "саек" в управляющей части, то в ответном сообщении посылается положительное подтверждение н покторяеюя ранее переданный символ "с".
Если принвтсе сообщение не искалоэо и оно содераоп 'аск' в управляющей части, то ответ в "с" выбирается новый символ для передачи, и он посылается с пслолщтельным подтверждением "аск". Если полученное сообщение искажено, то в ответном сообщении повторно посылаются старме данные (старый информационный символ) и отрицательное подтверждение "песк" получения информации в предыдущем сообщении. рне. 1.2, е. Ожнбка в протоколе Ф.СЛ.упса гт се ~а р 'п' Рис. 1.2, 6. Ошибка в протоюле ЦГ.С.Ьупсн Правила функционирования аыглкшгт абсолютно корректно, однако этот протокол содержит несколько ошибок.
Во-первых, если нет данных для передачи в одном из направлений, то передача и в другом направлении останавливается. Эту ошибку можно преодолеть, передавая какую-нибудь пустую информацию, если нет содержательной информации. Во-вторых, протокол имеет проблемы с инициализацией: после старта на обоих концах процессы будут ожидать сообщения ст партнера, т. е.
с первого шага протокол блокируется. Аналогичные проблемы существуют с завершением передачи: как оба процесса могут договориться о прекращении обмегш"г Очевидно, что необходимы специальные правила инициализации и завершения передачи, которые сами могут оказаться непростыми и содержать ошибки. гяаев г В-третьик, протокол содержат серьезную принципиальную ошибку: при некоторых редка встречающихся сценариях протокол может ошибочно принять дубликат предыдущих данных квк очередную инфорыашпо. Одни из таких сценариев приведен на рис. 1.2, б: процесс а передает процессу в сообщение с, в противололожион направлении процесс в передает процессу а сообщение н. Двойная повторяющаяся ошибка в канала, искажыощая как положительное подтверждение от а к в.
так и следующее сообщение. содержащее отрицательное подтверждение от в к гь приводит к дублированию принятия сообщения н процессом л. Таким обриюы, протокол работает правильно "почти всегда", зта логическая ошибка проявляется при редкик сочетаниях условий передачи. Испрышенне этой ошибки требует пересисчра всей логики протокола. Существуют лн другие ошибочные сцеьырии поведения этого протокола7 Ни тщательные просмотры такса, ни тестирование ие могут гарантировать огсутетвие ошибок в этом протоколе. Изпк, несыогра на простоту н очевидность правил передачи сообщений в эшы протокола, в неы содержатся тонкие логические ошибки, которые очень непросто обнаружить, и не совсем понятно, как нх исправлять.
Как указывает У. Линч, "подобные ошибки хотя и очень редко, но случаются, и именно их редкость делает их сбнарулиние в работакяцей систеые чрезвычайно трудиын. Такой неадекватный алгоритм будет ряботшь правильно "почти все арена"". Поскольку подобные ошибки в параллельных снсшнах выавнть тесгированнеи нельзя, едннственныи средством нх обнаружения явлвется верификация. Все серьезные разработчики сякяуот правилу: "любая параялельнав программа должна рассматриваться как некорректная до тех пор. локл ле доказало обратное". 1,3.
Общая схема верификации. Проверка моделей (тоде! слесЮля) Станларт ИСО 9000:2000 определяет процессы верификации и валнданли изготавливаемого продукта следуюшнн образом: ьу Верификация — подтверждение на основе представления объективных свидетельств того, что установленные требования были выполнены. 0З Впяидавкя — подтверждение на основе представление объективных свидетельств того, что требования, предназначенные для конкретного использования или применения, выполнены. кнх нне ние иое ада ще.
гсеикн Ни й в ень аст удаве ни- ~ИЯ. ро" 1ЫХ ви- ль- Хотя зти два определенна, как н сами термины, кюкупи почвы одшшковыми, в них есть существенное различие: (У Верификация (от лат, кепи — верный) — это проверка того, что продукт удовлетворяет сформулированным требованиям. ьг Вагидоиия (от лвт.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
