Математические основы программирования. Теория схем программ. Семантическая теория программ
Введение
Следуя А. П. Ершову, мы употребляем термин «теоретическое программирование» в качестве названия математической дисциплины, изучающей синтаксические и семантические свойства программ, их структуру, преобразования, процесс их составления и исполнения. Это словосочетание построено по аналогии с названиями таких наук, как теоретическая физика, теоретическая механика и т. д. В такой аналогии есть глубокий смысл: во всех случаях теоретическая научная дисциплина изучает фундаментальные понятия и законы основной науки и на основании обнаруженных закономерностей строит более частные математические модели исследуемых объектов, на которых ставит и решает прикладные задачи. В нашем случае ситуация усложняется еще тем, что объект моделирования – программа – уже представляет собой абстрактный объект.
В настоящее время сложились следующие основные направления исследований теоретического программирования.
1. Математические основы программирования. Основная цель исследований – развитие математического аппарата, ориентированного на теоретическое программирование, разработка общей теории машинных вычислений. Эта теория тесно соприкасается с теорией алгоритмов и вычислимых функций, теорией автоматов и формальных языков, логикой, алгеброй, с теорией сложности вычислений.
2. Теория схем программ. В этих работах внимание концентрируется на изучении структурных свойств и преобразований программ, а именно тех, которые отличают программы от других способов задания алгоритмов. Главным объектом исследования становится схема программы – математическая модель программы, в которой с той или иной степенью детализации отражено строение программы, взаимодействие составляющих ее компонентов.
3. Семантическая теория программ. Семантика программы или отдельных конструкций языков программирования – это их смысл, математический смысл для программиста и описание функционирования для машины. Этот раздел теоретического программирования изучает методы формального описания семантики программ, семантические методы преобразования и доказательства утверждений о программах. В частности, работы по методам проверки семантической правильности программ нацелены на автоматизацию их отладки и автоматический синтез программ.
4. Теория вычислительных процессов и структур (теория параллельных вычислений). Исследования в этой области направлены на разработку и обоснование новых методов программирования, прежде всего методов программирования параллельных процессов. В частности, изучаются модели, структуры и функционирование операционных систем, методы распараллеливания алгоритмов и программ, ведется поиск новых архитектурных принципов конструирования вычислительных машин и систем на основе результатов и рекомендаций теоретического программирования и вычислительной математики.
5. Прикладные задачи теоретического программирования. Сюда в первую очередь относятся разработка и обоснование алгоритмов трансляции и алгоритмов автоматической оптимизации программ.
Две дисциплины государственного стандарта специальности 220400 – Программное обеспечение вычислительной техники и автоматизированных систем – «Теория языков программирования и методы трансляции» и «Теория вычислительных процессов» рассматривают основы теоретического программирования. Первая дисциплина охватывает первый и последний пункты нашей, не претендующей на классификационную строгость и полноту, рубрикации. Вторая дисциплина, составляющая предмет настоящего курса, раскрывает пункты 2 – 4.
Программа как формализованное описание процесса обработки данных
Описать процесс - значит определить последовательность состояний заданной информационной среды. Если мы хотим, чтобы по заданному описанию требуемый…Правильная программа и надежная программа
В связи с тем, что задание на программу обычно формулируется не формально, а также из-за неформализованности понятия ошибки в программе, нельзя… Альтернативой правильной программы является надежная программа. Надежность… Разрабатываемая программа может обладать различной степенью надежности. Как измерять эту степень? Так же как в…Схемы программ
Краткое математическое предисловие
1.1.1. Функции и графы
Ведем некоторые соглашения об обозначениях элементов теории множеств и логики.
Множество – есть набор несовпадающих объектов, которые мы будем задавать явным перечислением, и заключать в фигурные скобки. Например: D - множество дней недели:
D = { Пн, Вт, Ср, Чт, Пт, Сб, Вс }, D1 = { Вт, Ср, Чт, Пн, Сб, Пт, Вс }.
D и D1 эквивалентны, т.е. порядок элементов не важен.
Будем использовать обозначения:
x Î A - x есть элемент и принадлежит множеству A; x Ï A - x не является элементом множества А.
Для бесконечных множеств метод перечисления элементов множества не применим, для этого используется характеристическое свойство А = {x | p(x)}, где х – переменная, значениями которой являются некоторые объекты, а р – свойство тех и только тех значений х, которые являются элементами задаваемого множества.
Пустое множество - множество, которое не содержит ни одного элемента, обозначается Ø или {}.
Если каждый элемент множества А является элементом множества В, то множество А является подмножеством множества В, будем писать A Ì B.
Если хотя бы один элемент множества А не является элементом множества В, то множество А не является подмножеством множества В и это записывается А Ë В.
Декартовым произведением А1 ´ А2 ´ … ´ Аn множеств А1, А2 … и Аn называется множество {(a1, a2, …, an) | a1 Î A1, a2 Î A2, , an Î An}, а An обозначает А ´ А ´ … ´ А (n раз).
Функцией, отображающей множество Х во множество Y (обозначение F: X → Y), называется множество F Í X´Y такое, что для любых пар (x, y)ÎF и (x’ y’)Î F из x = x’ следует, что y = y’.
Множество {x | (x, y) Î F} – область определения функции F (или множество значений ее аргумента); множество {y | (x, y) Î F} – область значений функции F.
Функцию F: X → Y называют n-местной функцией над множеством А, если Y = A и X = An.
Предикатом называют функцию, областью значений которой является множество символов-цифр {0, 1}. При этом говорят, что предикат P: X → {0, 1} истинен для x Î X, если P(x) = 1, и ложен, если P(x) = 0. Отношение на множестве Х – это двухместный предикат P: X2 → {0, 1}.
Алфавитом называют непустое конечное множество символов. Например, V1 = {a, b}, V2 = {0, 1}, V3 = {a, +, 1, =} – алфавиты. Словом в алфавите V называется конечный объект, получаемый выписыванием одного за другим символов V, например, а + 1 = 1 + а – слово в алфавите V3, 101011 – слово в алфавите V2, abaab – слово в алфавите V1. Длина слова – число символов в нем, пустое слово не содержит ни одного символа.
Множество всех слов в алфавите V обозначается V*.
n-местной словарной функцией над алфавитом V называют n-местную функцию над V*, т. е. функцию из V* ´ V* ´ … ´ V* (n раз) в V*.
Направленным графом называется тройка G = (V, E, Ф), где V - множество вершин, Е – множество дуг, а Ф – функция из Е в (VÈ{ω})2 , ω Ï V. Дуга е называется входом графа, если Ф(е) = (w, u), для u Î VÈ{ω}; внутренней, если Ф(е) = (u1, u2) для u1,u2 Î V; выходом, если Ф(е) = (u,w), для u Î VÈ{ω}. Дуга е, являющаяся одновременно и входом и выходом графа, называется висячей; для нее Ф(е) = (w, ω). Дуги, не являющиеся внутренними, называются также свободными.
Говорят, что дуга е инцидентна вершине u, если е выходит из u или ведет в u. Две дуги смежны, если существует хотя бы одна инцидентная им обеим вершина. Вершина u называется наследником вершины u’, если в графе имеется хотя бы одна такая дуга, что Ф(е) = (u’, u).
Рисунок 1.1.
Изображенный на рисунке 1.1 граф G1 содержит 4 вершины, 8 дуг. Дуга е1 – входная, дуга е6 – выходная, дуга е8 – висячая, остальные дуги внутренние; вершины u1 и u3 наследники вершины u1.
Путем в графе G называется последовательность …uieiui+1… дуг и вершин, такая, что для всех i Ф(еi) = (ui,ui+1). Образом пути называется слово, составленное из пометок проходимых дуг и вершин.
Две вершины u1,u2 графа G называются связанными, если u1 = u2 или существует маршрут е1, …,еn графа G такой, что дуга е1 инцидентна вершине u1, а дуга еn – вершине u2.
1.1.2. Вычислимость и разрешимость
Данное в п. 1.1.1. определение функции не содержит указаний о том, как для заданных значений аргументов получить соответствующие значения функции. Было бы практичнее переформулировать это определение таким образом, чтобы оно содержало конструктивную процедуру, или алгоритм, нахождения значений функции. Однако такое определение уже приведенного выше, т. е. определяет лишь некоторый подкласс функций, которые называют вычислимыми функциями.
Тьюринг в середине 30-х годов формализовал способ получения значений вычислимой функции с помощью абстрактной «математической машины», вычисляющей значения функции по значениям ее аргументов. Конкретная машина Тьюринга задает конкретную вычислимую функцию и его гипотеза (тезис) состояла в том, что каждая функция, для которой существует алгоритм нахождения ее значений, представима некоторой машиной Тьюринга, т. е. является вычислимой. Тезис Тьюринга не может быть доказан, так как наряду с формальным понятием вычислимой функции он содержит эмпирическое понятие алгоритма. Однако интуиция, отсутствие опровергающих примеров и равносильность различных формализаций вычислимости убеждают в справедливости этого тезиса.
Машина Тьюринга Т задает словарную функцию над некоторым алфавитом V и представляет собой описание машины — набор (F, Q, q0, #, I) - и правило функционирования, общее для всех машин, где
V — алфавит машины;
Q — конечное непустое множество символов, называемых состояниями машины (Q Ç V =Æ);
q0 — выделенный элемент множества Q, называемый начальным состоянием;
# — специальный «пустой» символ, не принадлежащий ни V, ни Q;
I — программа машины.
Программа машины — это конечное множество слов вида qa ® q'a’d, называемых командами, где q, q' Î Q, a, a' Î V È {#}; ® — вспомогательный символ-разделитель; d — элемент множества {l, r, р}, содержащего три специальных символа, которых нет ни в V, ни в Q. Предполагается также, что в программе I никакие две команды не могут иметь одинаковую пару первых двух символов.
Правило функционирования поясним неформально на распространенной «физической» модели машины Тьюринга. Машина состоит из потенциально бесконечной (в обе стороны) ленты, управления и головки, перемещаемой вдоль ленты (см. рисунок). Лента разбита на клетки, которые могут содержать символы из алфавита V или быть пустыми, т. е. содержать символ #. Управление на каждом шаге работы машины находится в одном из состояний из Q, расшифровывает программу, которая однозначно определяет поведение машины и управляет головкой. Головка в каждый момент расположена против некоторой клетки ленты и может считывать символы с ленты, записывать их на ленту и перемещаться в обе стороны вдоль ленты. Машина функционирует следующим образом. В начальный момент на ленте записано некоторое слово из V, а управление находится в начальном состоянии q0. Начальное слово, равно как и слова, появляющиеся в процессе работы машины, ограничено с двух сторон пустыми символами #. Головка обозревает крайний слева символ заданного слова.
Работа машины состоит в повторении следующего цикла элементарных действий:
1) считывание символа, находящегося против головки;
2) поиск применимой команды, а именно той команды qa ® q'a'd, в которой q — текущее состояние управления, а — считанный символ;
3) выполнение найденной команды, состоящее в переводе управления в новое состояние q', записи в обозреваемую головкой клетку символа а' (вместо стираемого символа а) и последующем перемещении головки вправо, если d = r, влево, если d = I, или сохранении ее в том же положении, если d = р.
Машина останавливается в том и только в том случае, если на очередном шаге ни одна из команд не применима. Результат работы остановившейся машины — заключительное слово на ленте.
Машина Тьюринга, перерабатывая начальные слова на ленте в заключительные, задает словарную функцию, для которой начальные слова - значения аргумента, заключительные - значения функции. (Для представления n-местной функции начальное слово на ленте имеет вид #a1 #a2 # … #an #, где подслова a1, a2,…, an не содержат символа #. При интерпретации заключительного слова на ленте как значения функции символ # игнорируется). Если машина не останавливается, начав работу с некоторым словом на ленте, то функция, задаваемая машиной, считается неопределенной для этого слова. Таким образом, машина Тьюринга Т задает частичную функцию FT и способ вычисления ее значений. Хотя машины Тьюринга оперируют со словами, они могут задавать и числовые функции в силу установленной выше связи между словами и числами.
По определению, функция F является (частично) вычислимой, если существует машина Тьюринга Т такая, что FT = F. Говорят также, что для функции F существует (частичный) алгоритм вычисления ее значений, задаваемый машиной Т.
Для машины Тьюринга, как и для всех других формальных способов задания алгоритмов, включая программы для ЭВМ, характерны следующие свойства:
1) конструктивность — машина Тьюринга представляет собой конечный объект, построенный по определенным правилам из базовых объектов;
2) конечность — процесс нахождения значений функции для тех значений аргументов, для которых она определена, состоит из конечного числа шагов;
3) однозначность — результат работы машины единственным образом определяется начальным словом;
4) массовость — машина работает с любым начальным словом на ленте, составленным из символов ее алфавита.
Машина Тьюринга однозначно задается своей программой. Если упорядочить ее команды и закодировать последовательность команд словом в алфавите машины Тьюринга, то можно получить ее описание в собственном алфавите. Заметим, что одной и той же машине Тьюринга соответствуют различные словарные представления в ее алфавите в зависимости от выбора упорядочений множеств Q, V, I, но по любому из этих представлений программа машины восстанавливается однозначно.
Изучая свойства программ и их математических абстракций – схем программ, мы ставим целью автоматизацию программирования, в том числе автоматический анализ свойств программ и их преобразования, осуществляемые с помощью других, специальных программ. Поэтому нас интересуют алгоритмы, которые могли бы по любой предъявленной программе установить, завершит ли она работу или будет «циклить», дают ли две программы, исходная и оптимизированная, один и тот же результат, является ли программа синтаксически правильной и т. д.
Массовые алгоритмические проблемы формулируются следующим образом. Необходимо указать алгоритм, который бы определял, обладает ли предъявленный объект из некоторого класса объектов интересующим нас свойством, принадлежит ли он множеству М всех объектов, обладающих этим свойством. Если существует такой частичный алгоритм, то говорят, что множество перечислимо, а поставленная массовая алгоритмическая проблема частично разрешима. Если этот алгоритм к тому же всюду определен, то множество М разрешимо и поставленная проблема также разрешима. Существуют неразрешимые проблемы и даже проблемы, которые не являются частично разрешимыми, что свидетельствует о существовании невычислимых функций.
Пусть V – алфавит, М Í V – множество слов в V.
Характеристической функцией множества М называется предикат FM: V* → {0, 1}, всюду определенный на V*: FM (а) = 1, если а Î М, и FM (а) = 0, если а Ï М.
Частичная характеристическая функция множества М – это функция НМ: V* → {1}, определенная только для слов из М и имеющая вид НM (а) = 1 для всех а Î М.
Множество М называется разрешимым, если его характеристическая функция вычислима. Множество М перечислимо, если его частичная характеристическая функция вычислима. Разрешимость множества М означает, что существует всегда останавливающаяся (оканчивающая работу за конечное время) машина Тьюринга, позволяющая для любого слова в алфавите V через конечное число шагов установить, принадлежит ли это слово множеству М или нет. Перечислимость множества М означает, что существует машина Тьюринга, которая останавливается в том и только том случае, если предъявленное слово принадлежит множеству М.
Приведем без доказательства несколько важных теорем.
Теорема (Пост). Множество М Í V* разрешимо тогда и только тогда, когда М и его дополнение М’ = V*\M перечислимы.
Машина Тьюринга, начав работу, или останавливается, или работает бесконечно. Проблема остановки формулируется так. Пусть М – множество всех пар слов в алфавите V, в каждой паре первое слово – словарное представление некоторой машины Тьюринга, второе – такое слово, что эта машина останавливается, начав работу над ним. Является ли множество М неразрешимым.
Теорема (Тьюринг). Проблема остановки машины Тьюринга неразрешима.
Последняя теорема демонстрирует существование невычислимых функций. Из тезиса Тьюринга следует, что для неразрешимых проблем нельзя построить алгоритм, который решал бы их, например, с помощью ЭВМ.
Проблема зацикливания состоит в следующем: существует ли алгоритм, хотя бы частный, который выясняет заранее для произвольной машины Тьюринга будет ли она работать бесконечно.
Теорема. Проблема зацикливания машины Тьюринга не является частично разрешимой.
1.1.3. Программы и схемы программ
Схемы программ - это математические модели программ, описывающие строение программы, или точнее строение множества программ, где конкретные операции и функции заменены абстрактными функциональными и предикатными символами. Следующий пример программ вычисления факториала n! и переворачивания слов поясняет различие между программами и их схемой S1.
begin integer x, y; begin integer x, y; begin
ввод(x); ввод(x); ввод(x);
y:=1; y:=ε; y:=a;
L: ifx=0 then gotoL1; L: ifx=0 then gotoL1; L: if p(x) then gotoL1;
y:=x*y; y:=CONSCAR(x, y); y:=g(x, y);
x:=x-1; x:=CDR(x); x:=h(x);
goto L; goto L; goto L;
L1: вывод(y); L1: вывод(y); L1: вывод(y);
End end end
Функция CONSCAR (суперпозиция функций CONS и CAR из языка Лисп) приписывает первую букву первого слова ко второму слову (т. е. CONSCAR(аб, в) = ав), а функция CAR стирает первую букву слова (т. е. CAR(аб) = б).
Стандартные схемы программ
Стандартные схемы программ (ССП) характеризуются базисом и структурой схемы. Базис класса фиксирует символы, из которых строятся схемы, указывает их роль… Полный базис В класса стандартных схем состоит из 4-х непересекающихся, счетных множеств символов и множества…Свойства и виды стандартных схем программ
ССП S в базисе В тотальна (пуста), если для любой интерпретации I базиса В программа (S, I) останавливается (зацикливается). Стандартные схемы S1 и S2 в базисе В функционально эквивалентны (S1 ~ S2),… Примеры тотальных, пустых и эквивалентных схем S2, S3, S4, S5 приведены на рисунке 1.3.Моделирование стандартных схем программ
Конечный одноленточный (детерминированный, односторонний) автомат обнаруживают ряд полезных качеств, используемых в теории схем программ для… Одноленточный конечный автомат (ОКА) над алфавитом V задается набором A = { V, Q, R, q0, #, I } и правилом функционирования, общим для всех таких автоматов. В наборе АРекурсивные схемы
Среди упомянутых выше методов формализации понятия вычислимой функции метод Тьюринга — Поста основан на уточнении понятия процесса вычислений, для… Язык Фортран — типичный представитель операторных языков. С другой стороны,… Примером рекурсивно определяемой функции является факториальная функция FACT: Nat → Nat:Трансляция схем программ
Программы для ЭВМ, будь-то программы, записанные на операторном языке, или программы на рекурсивном языке, универсальны в том смысле, что любую… Мы будем сравнивать классы схем, у которых базисы согласованны в том смысле,… Схема S1 из класса W и схема S2 из класса W’ функционально эквивалентны, если для любой интерпретации I согласованных…Обогащенные и структурированные схемы
Выделяют следующие классы обогащенных схем: класс счетчиковых схем, класс магазинных схем, класс схем с массивами. Классы счетчиковых и магазинных схем образован добавлением в базис ССП… Счетчик — интерпретированная переменная, у которой областью значений является множество Nat; начальное значение…Семантическая теория программ
Описание смысла программ
Руководство по использованию языка программирования должно включать описание каждой конструкции языка, как по отдельности, так и в совокупности с… В большинстве руководств определение семантики дается в виде обычного текста.… Задача определения семантики языка программирования рассматривается теоретиками давно, но до сих пор не найдено…Преобразователь предикатов.
«Условие, характеризующее множество всех начальных состояний, при которых запуск обязательно приведет к событию правильного завершения, причем… Условие называют слабейшим, так как чем слабее условие, тем больше состояний… Если S - некоторый оператор (последовательность операторов), R - желаемое постусловие, то соответствующее слабейшее…Fi
Вариант 2.
задать (N, M);
if N > 0 AND M > 0 → n, m := N, M;
do n > m → n := n – m П m > n → m := m – n od;
выдать (n)
Fi
Дадим формальное определение слабейшего предусловия для оператора цикла DO.
Пусть предикат H0(R) определяет множество состояний, в которых выполнение DO завершается за 0 шагов (в этом случае все охраны с самого начала ложны, после завершения R имеет значение истина):
H0(R) = NOT BB AND R
Другими словами, требуется, чтобы оператор цикла DO завершил работу, не производя выборки охраняемой команды, что гарантируется первым конъюнктивным членом предиката H0(R): NOT BB = T. При этом истинность R до выполнения DO является необходимым условием для истинности R после выполнения DO.
Определим предикат Hk(R) как множество состояний, в которых выполнение DO заканчивается за k шагов при значении R истина (Hk(R) будет определяться через Hk-1(R)):
Hk(R) = H0(R) OR wp(IF, Hk-1(R)), k > 0 → wp(DO, R) = ($ k: k ³ 0: Hk(R)).
Это значит, что должно существовать такое значение k, что потребуется не более, чем k шагов, для обеспечения завершения работы в конечном состоянии, удовлетворяющем постусловию R.
Определение DO. Если предикаты Hk(R) задаются в виде
Hk(R) = NOT B AND R, k = 0
Hk(R) = wp(IF, Hk-1(R)), k > 0, → wp (DO,R)=($ k: k ³ 0: Hk(R))
Основная теорема для оператора цикла. Пусть оператор выбора IF и предикат P таковы, что для всех состояний справедливо
(P AND BB) => wp(IF, R). (2.3)
Тогда для оператора цикла справедливо:
(P AND wp(DO, T)) => wp(DO, P AND NOT BB).
Эта теорема известна как основная теорема инвариантности для цикла. Предикат Р, истинный перед выполнением и после выполнения каждого шага цикла, называется инвариантным отношением или просто инвариантом цикла. В математике термин «инвариантный» означает не изменяющийся под воздействием совокупности рассматриваемых математических операций.
Поясним смысл теоремы. Условие (2.3) означает, что если предикат P первоначально истинен и одна из охраняемых команд выбирается для выполнения, то после ее выполнения P сохранит значение истинности. После завершения оператора, когда ни одна из охран не является истиной, будем иметь:
P AND NOT BB.
Работа завершится правильно, если условие wp(DO, T) справедливо и до выполнения DO. Так как любое состояние удовлетворяет T, то wp(DO,T) является слабейшим предусловием для начального состояния такого, что запуск оператора цикла DO приведет к правильно завершаемой работе.
Доказательство.
Из определения DO следует:
Если H0(T)= NOT BB AND T, k=0
Hk(T)=wp(IF, Hk-1(T)), k>0, → wp(DO,T)=($ k: k ³ 0: Hk(T))
H0(P AND NOT BB)=P AND NOT BB;
Hk(P AND NOT BB)=wp(IF, Hk-1(P AND NOT BB), → wp(DO, P AND NOT BB)=($ k ³ 0: Hk(P AND NOT BB))
С помощью метода математической индукции можно доказать, что из условия (2.3) следует
(P AND Hk(T)) => Hk(P AND NOT BB), k ³ 0
Тогда имеем
P AND wp(DO, T) = ($k: k ³ 0: P and Hk(T) ) => ($k: k ³ 0: Hk(P AND NOT BB) ) = wp(DO, P AND NOT BB)
Следовательно, (P AND wp(DO, T)) => wp(DO, P AND NOT BB).
Чтобы использовать аксиоматическую семантику с данным языком программирования для доказательства правильности программ или для описания формальной семантики, для каждого вида операторов языка должны быть определены аксиомы или правила логического вывода. С ними мы познакомимся в п. 2.3 «Верификация программ».
В аксиоматической семантике система (2.1) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и/или интерпретации определяемых объектов.
Для интерпретации системы функций (2.1) вводится понятие аксиоматического описания <S, A> - логически связанной пары понятий: S - сигнатура используемых в системе символов функций f1, f2, ..., fm и символов констант (нульместных функциональных символов) c1, c2, ..., cI, а A - набор аксиом, представленный системой. Предполагается, что каждая переменная xi, i=1, ..., k, и каждая константа ci, i=1, ..., l, используемая в A, принадлежит к какому-либо из типов данных t1, t2, ..., tr, а каждый символ fj, j=1, ..., m, представляет функцию, типа: ti1 ti2 ... tik ® ti0. Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных ti = ti', i=1, ..., r, и конкретные значения констант ci = ci', i = 1, ..., l.
К. Хоaр построил аксиоматическое определение набора типов данных, которые потом Н. Вирт использовал при создании языка Паскаль.
Пример 2.6. Рассмотрим систему равенств:
УДАЛИТЬ(ДОБАВИТЬ(m,d))=m,
ВЕРХ(ДОБАВИТЬ(m,d))=d,
УДАЛИТЬ(ПУСТ)=ПУСТ,
ВЕРХ(ПУСТ)=ДНО,
где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ - символы функций, а ПУСТ и ДНО - символы констант, образующие сигнатуру этой системы. Пусть D, D1 и М - некоторые типы данных, такие, что m Î M, d Î D, ПУСТ Î M, ДНО Î D1, а функциональные символы представляют функции следующих типов:
УДАЛИТЬ: M ® M,
ДОБАВИТЬ: M, D ® M,
ВЕРХ: M ® D1.
Данная сигнатура вместе с указанной системой равенств, рассматриваемой как набор аксиом, образует аксиоматическое описание абстрактного типа данных, называемого магазином.
Зададим интерпретацию символов ее сигнатуры: D - множество значений, которые являются элементами магазина, M - множество состояний магазина, M = {d1,d2, ... ,dn: di Î D, i=1, ..., n, n ³ 0}, D1=D È {ДНО}, ПУСТ={}, а ДНО - особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.
При определении семантики полного языка программирования с использованием аксиоматического метода для каждого вида операторов языка должны быть сформулированы аксиома или правило логического вывода. Но определение аксиом и правил логического вывода для некоторых операторов языков программирования - очень сложная задача. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства утверждений о программах» (Э. Дейкстра).
Напрашивающимся решением такой проблемы является разработка языка, подразумевающего использование аксиоматического метода, т.е. содержащей только те операторы, для которых могут быть написаны аксиомы или правила логического вывода. К сожалению, подобный язык оказался бы слишком маленьким и простым что отражает нынешнее состояние аксиоматической семантики как науки.
Аксиоматическая семантика является мощным инструментом для исследований в области доказательств правильности программ, она также создает великолепную основу для анализа программ, как во время их создания, так и позднее. Однако ее полезность при описании содержания языков программирования весьма ограничена как для пользователей языка, так и для разработчиков компиляторов.
2.1.3. Денотационная семантика
Денотационная семантика - самый строгий широко известный метод описания значения программ. Она прочно опирается на теорию рекурсивных функций. Всестороннее рассмотрение денотационной семантики - длительное и сложное дело. Здесь мы познакомимся лишь с ее основными принципами.
Основной концепцией денотационной семантики является определение для каждой сущности языка некоего математического объекта и некоей функции, отображающей экземпляры этой сущности в экземпляры этого математического объекта. Поскольку объекты определены строго, то они представляют собой точный смысл соответствующих сущностей. Сама идея основана на факте существования строгих методов оперирования математическими объектами, а не конструкциями языков программирования. Сложность использования этого метода заключается в создании объектов и функций отображения. Название метода «денотационная семантика» происходит от английского слова denote (обозначать), поскольку математический объект обозначает смысл соответствующей синтаксической сущности.
Для введения в денотационный метод мы используем очень простую языковую конструкцию - двоичные числа. Синтаксис этих чисел можно описать следующими грамматическими правилами:
<двоичное_число> → 0
| 1
| <двоичное_число> 0
| <двоичное_число> 1
Для описания двоичных чисел с использованием денотационной семантики и грамматических правил, указанных выше, их фактическое значение связывается с каждым правилом, имеющим в своей правой части один терминальный (основной) символ. Объектами в данном случае являются десятичные числа.
В нашем примере значащие объекты должны связываться с первыми двумя правилами. Остальные два правила являются, в известном смысле, правилами вычислений, поскольку они объединяют терминальный символ, с которым может ассоциироваться объект, с нетерминальным, который может представлять собой некоторую конструкцию.
Пусть область определения семантических значений объектов представляет собой множество неотрицательных десятичных целых чисел Nat. Это именно те объекты, которые мы хотим связать с двоичными числами. Семантическая функция Мb отображает синтаксические объекты в объекты множества N согласно указанным выше правилам. Сама функция Мb определяется следующим образом:
Мb('0') = 0, Мb('1')=1
Мb(<двоичное_число> '0') = 2 * Мb(<двоичное_число>)
Мb(<двоичное_число> ‘1’) = + 2 * Мb(<двоичное_число>) + 1
Мы заключили синтаксические цифры в апострофы, чтобы отличать их от математических цифр. Отношение между этими категориями подобно отношениям между цифрами в кодировке ASCII и математическими цифрами. Когда программа считывает число как строку, то прежде, чем это число сможет использоваться в программе, оно должно быть преобразовано в математическое число.
Пример 2.7. Описание значения десятичных синтаксических литеральных констант.
<десятичное_число> → 0|1|2|3|4|5|6|7|8|9
| <десятичное_число> (0|1|2|3|4|5|6|7|8|9)
Денотационные отображения для этих синтаксических правил имеют следующий вид:
Md(‘0') = 0, Md('1') = 1, ,..., Md('9') = 9
Мd(<десятичное_число> '0') = 10 * Мd(<двоичное_число>)
Мd(<десятичное_число> ‘1’) = 10 * Мd(<десятичное_число>) + 1
…
Мd(<десятичное_число> '9') = 10 * Мd(<десятичное_число>) + 9
Денотационную семантику программы можно определить в терминах изменений состояний идеального компьютера. Подобным образом определялись операционные ceмантики, приблизительно так же определяются и денотационные. Правда, для простоты они определяются только в терминах значений всех переменных, объявленных в программе. Операционная и денотационная семантики различаются тем, что изменения состояний в операционной семантике определяются запрограммированными алгоритмами, а в денотационной семантике они определяются строгими математическими функциями. Пусть состояние s программы определяется следующим набором упорядоченных пар: {<i1, v1>, <i2, v2>, …, <in, vn>}.
Каждый параметр i является именем переменной, а соответствующие параметры v являются текущими значениями данных переменных. Любой из параметров v может иметь специальное значение undef, указывающее, что связанная с ним величина в данный момент не определена.
Пусть VARMAP - функция двух параметров, имени переменной и состояния программы. Значение функции VARMAP(ik, s) равно vk (значение, соответствующее параметру ik в состоянии s).
Большинство семантических функций отображения для программ и программных конструкций отображают состояния в состояния. Эти изменения состояний используются для определения смысла программ и программных конструкций. Отметим, что такие языковые конструкции, как выражения, отображаются не в состояния, а в величины.
Выражения являются основой большинства языков программирования. Более того, мы имеем дело только с очень простыми выражениями. Единственными операторами являются операторы + и *; выражения могут содержать не более одного оператора; единственными операндами являются скалярные переменные и целочисленные литеральные константы; круглые скобки не используются; значение выражения является целым числом. Ниже следует описание этих выражений в форме БНФ:
<выражение> → <десятичное_число> | <переменная>
| <двоичное_выражение>
<двоичное_выражение> → <выражение_слева> <оператор>
<выражение_справа>
<оператор> → + | *
Единственной рассматриваемой нами ошибкой в выражениях является неопределенное значение переменной. Разумеется, могут появляться и другие ошибки, но большинство из них зависят от машины. Пусть Z - набор целых чисел, a error - ошибочное значение. Тогда множество Z È {error} является множеством значений, для которых выражение может быть вычислено.
Ниже приведена функция отображения для данного выражения Е и состояния s. Символ º обозначает равенство по определению функции.
Me (<выражение>,s) º
case <выражение> of
<десятичное_число> => Md(<десятичное_число>, s)
< переменная> => if VARMAP(<переменная>,s) = undef
then error
else VARMAP(<переменная>, s)
<двоичное_выражение> =>
if(Me(<двоичное_выражение>.<выражение_слева>,s) = undef OR
Me(<двоичное_выражение>.< выражение_справа >, s) = undef)
then error
else if(<двоичное_выражение>.< оператор > = '+' then
Me(<двоичное_выражение>.<выражение_слева>, s) +
Me(<двоичное_выражение>.<выражение_справа>, s)
else Me(<двоичное_выражение>.<выражение_слева>, s) *
Me(<двоичное_выражение>.<выражение_справа>, s)
Оператор присваивания - это вычисление выражения плюс присваивание его значения переменной, находящейся в левой части. Сказанное можно описать следующей функцией:
Ма(х = Е, s) º if Me(E, s) = error
then error
else s' = {< i1', v1' >, < i2', v2' >,..., < in', vn' >} where
for j = 1, 2, ..., n, vj’ = VARMAP(ij’, s) if ij <>x;
Me(E, s) if ij = x
Отметим, что два сравнения, выполняющиеся в двух последних строках (ij<> x и ij = х), относятся к именам, а не значениям.
После определения полной системы для заданного языка ее можно использовать для определения смысла полных программ этого языка. Это создает основу для очень строгого способа мышления в программировании.
Денотационная семантика может использоваться для разработки языка. Операторы, описать которые с помощью денотационной семантики трудно, могут оказаться сложными и для понимания пользователями языка, и тогда разработчику следует подумать об альтернативной конструкции.
С одной стороны, денотационные описания очень сложны, с другой - они дают великолепный метод краткого описания языка.
2.1.4. Декларативная семантика
Декларативная семантика является существенной характеристикой языков логического программирования, в которых программы состоят из объявлений (деклараций), а не из операторов присваивания и управляющих операторов. Эти объявления в действительности являются операторами, или высказываниями, в символьной логике.
Основная концепция декларативной семантики заключается в том, что существует простой способ определения смысла каждого оператора, и он не зависит от того, как именно этот оператор используется для решения задачи. Декларативная семантика значительно проще, чем семантика императивных (применяющихся в компьютерах с фон-неймановской архитектурой) языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности выполнения программы.
Формальное определение семантики становится общепринятой частью определения нового языка. Стандартное описание языка PL/I включает в себя VDL-подобную нотацию, описывающую семантику операторов PL/I, а для языка Ada было разработано определение на основе денотационной семантики. Тем не менее, изучение формальных определений семантики не оказало такого сильного влияния на практическое определение языков, как изучение формальных грамматик — на определение синтаксиса. Ни один из методов определения семантики не оказался по настоящему полезным ни для пользователя, ни для разработчиков компиляторов языков программирования.
Языки формальной спецификации.
Второй из перечисленных факторов важен, поскольку способ использования языка, как, оказалось, серьезно влияет на эволюцию языка. Если рассматривать… описать эскизную модель (функциональности, поведения); доказать, что модель корректна (не противоречива, консистентна);Верификация программ.
Методы доказательства правильности программ.
Можно сказать, что требование отсутствия ошибок в программном обеспечении совершенно естественно и не нуждается в обосновании. Но как убедиться в… К неформальным методам доказательства правильности программ относят отладку и… Тестирование – процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы. Суть…Использование утверждений в программах.
Утверждения используются для доказательства правильности программ. Тогда утверждения необходимо формулировать в некоторой формальной логической системе. Обычно используется исчисление предикатов первого порядка.
Исчисление - это метод или процесс рассуждений посредством вычислений над символами. В исчислении предикатов утверждения являются логическими переменными или выражениями, имеющими значение T - истина или F - ложь. Наша цель - при написании программы некоторым способом доказать истинность утверждения (2.2) - триады Хоара {Q} S {R}. Для этого нужно уметь записывать его в исчислении предикатов и формально доказывать его истинность.
Предикат, помещенный в программу, был нами назван утверждением. Утверждается, что он истинен в соответствующий момент выполнения программы. В предусловии Q нужно отражать тот факт, что входные переменные получили начальные значения. Для обозначения начальных значений будем использовать большие буквы.
Пример 2.8. Пусть надо определить приближенное значение квадратного корня: s = sqrt(n), где n, s Î Nat. Определим постусловие в виде:
R: s*s £ n < (s+1)*(s+1).
Пример 2.9. Даны целочисленные n > 0 и массив a[1,...,n]. Отсортировать массив, т.е. установить
R: (" i: 1 £ i < n: a[i] £ a[i+1]).
Пример 2.10. Определить x как максимальное значение массива a[1,...,n]. Определим постусловие:
R: {x = max({y | y Í a})}.
Для построения программы следует определить математическое понятие max. Тогда
R: {($ i: 1 £ i £ n: x = a[i]) AND (" i: 1 £ i £ n: a[i] = x)}.
Пример 2.11. Пусть имеем программу S обмена значениями двух целых переменных a и b. Сформулируем входное и выходное утверждения программы и представим программу S в виде предиката:
{ a = A AND b = B } S { a = B AND b = A }, (2.4)
где A, B - конкретные значения переменных a, b.
Программа вместе с утверждениями между каждой парой соседних операторов называется наброском доказательства. Последовательно, для каждого оператора программы формулируя предикат (2.4), можно доказать, что программа удовлетворяет своим спецификациям. Представим набросок доказательства для программы S:
{ a = A AND b = B }
r := a; { r = a AND a = A AND b = B };
a := b; { r = a AND a = B AND b = B };
b := r; { a = B AND b = A }.
Не обязательно набросок доказательства должен быть настолько полным. Для документирования программы нужно вставить достаточно утверждений, чтобы программа стала понимаемой.
Программа, содержащая утверждения для ее документирования, называется аннотированной программой. Чтобы использовать утверждения для доказательства правильности программы, необходимы соответствующие правила верификации.
Правила верификации К. Хоара.
A1. Аксиома присваивания: { Ro } x := Е { R } Неформальное объяснение аксиомы: так как x после выполнения будет содержать… Аксиома присваивания будет иметь вид:{RxЕ} x := Е {R}.Begin
r := r - y; q := q + 1
end;
выдать(q,r);
Сформулируем постусловие
R: (r < y) AND (x = y*q + r)
Нужно доказать, что
{y > 0 AND x/y} S {(r < y) AND (x = y*q + r )}.
Доказательство.
1. Очевидно, что Q => x = x + y * 0.
2. Применим аксиому A1 к оператору r := x, тогда получим { x = x + y * 0 } r := x { x = r + y * 0 }
3. Аналогично, применяя A1 к оператору q := 0, получим: { x = r + y * 0 } q := 0 { x = r + y*q }
4. Применяя правило A3 к результатам пунктов 1 и 2, получим { Q } r := x { x = r + y * 0 }
5. Применяя правило A4 к результатам пунктов 4 и 3, получим { Q } r := x; q := 0 { x = r + y*q }
6. Выполним равносильное преобразование x = r + y * q AND y £ r => x = (r - y) + y*(q + 1)
7. Применяя правило A1 к оператору r:= r - y, получим {x = (r - y) + y*( q + 1)} r:= r - y {x = r+ y*(q+1)}
8. Для оператора q := q + 1 аналогично получим { x = r + y*(q + 1) } q := q + 1 { x = r + y*q }
Применяя правило A4 к результатам пунктов 7 и 8, получим
{ x = (r - y) + y*( q + 1) } r := r - y; q := q + 1 { x = r + y*q }
Применяя правило A2 к результатам пунктов 6 и 9, получим
{ x = r + y*q AND y £ r } r := r - y; q := q + 1 { x = r + y*q }
Применяя правило A8 к результату пункта 10, получим
{x = r + y*q } while y £ r do begin r := r - y; q := q + 1 end { NOT (y <= r) AND (x = r + y*q) }
Утверждение x = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.
Применяя правило A4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать,
{ Q } S { NOT (y £ r) AND (x = r + y*q) }
Осталось доказать, что выполнение программы заканчивается.
Доказывать будем от противного, т.е. предположим, что программа не заканчивается. Тогда должна существовать бесконечная последовательность значений r и q, удовлетворяющая условиям
1) y £ r;
2) r, q Î Nat.
Но значение r на каждом шаге цикла уменьшается на положительную величину: r := r - y (y > 0). Значит, последовательность значений r и q является конечной, т.е. найдется такое значение r, для которого не будет выполняться условие y £ r и циклический процесс завершится.
Теоретические модели вычислительных процессов
Взаимодействующие последовательные процессы
Такой подход обладает целым рядом преимуществ. Во-первых, он позволяет избежать многих традиционных для параллельного программирования проблем,… Во-вторых, он включает в себя в виде частных случаев модели структурного… В-третьих, он является надежной основой для избежания таких ошибок, как расходимость, тупики, зацикливание.Параллельные процессы
3.2.1. Взаимодействие Объединяя два процесса для совместного исполнения, как правило, хотят, чтобы… 3.2.1.1. ЗаконыРазделяемые ресурсы
Обозначение (m://S) мы использовали для именованного подчиненного процесса (m:R), единственной обязанностью которого является удовлетворение потребностей главного процесса S. Предположим теперь, что S состоит из двух параллельных процессов (P || Q) и они оба нуждаются в услугах одного и того же подчиненного процесса (m :R). К сожалению, P и Q не могут взаимодействовать с R по одним и тем же каналам, потому что тогда эти каналы должны содержаться в алфавитах обоих процессов, и, значит, согласно определению оператора ||, взаимодействия с (m : R) могут происходить, только когда P и Q одновременно посылают одно и то же сообщение, что далеко не соответствует желаемому результату. Нам же требуется своего рода чередование взаимодействий между P и (m:R) с взаимодействиями между Q и (m:R). В этом случае (m:R) служит как ресурс, разделяемый P и Q; каждый из них использует его независимо, и их взаимодействия с ним чередуются.
Когда все процессы-пользователи известны заранее, можно организовать работу так, чтобы каждый процесс-пользователь имел свой набор каналов для взаимодействий с совместно используемым ресурсом. Эта техника применялась в задаче об обедающих философах: каждая вилка совместно использовалась всеми пятью. Общий метод разделения ресурсов дает множественная пометка, которая является эффективным средством создания достаточного числа каналов для независимого взаимодействия с каждым процессом-пользователем. Отдельные взаимодействия по этим каналам произвольно чередуются. Однако при таком методе необходимо знать заранее имена всех процессов-пользователей, и поэтому он не подходит для подчиненного процесса, предназначенного для обслуживания главного процесса, который разбивается на произвольное число параллельных подпроцессов.
3.4.1. Поочередное использование
Проблему, вызванную использованием комбинирующего оператора ||, можно избежать, используя параллелизм в форме чередования (P
Q). Здесь P и Q имеют одинаковые алфавиты, а их взаимодействия с совместно используемыми внешними процессами произвольно чередуются. Пример 3.25. Совместно используемая подпрограмма: удв : УДВ // (P
Q). Здесь и P, и Q могут содержать вызов подчиненного процесса (удв.лев!v → удв.прав?х → ПРОПУСК), где ПРОПУСК – процесс, который ничего не делает, но благополучно завершается. Пример 3.26. Совместно используемое алфавитно-цифровое печатающее устройство: АЦПУ = занят → µХ.(лев?s → h!s → X | свободен → АЦПУ) Здесь h – канал, соединяющий АЦПУ с аппаратной частью устройства. После наступления события занят АЦПУ копирует в аппаратную часть последовательно поступающие по левому каналу строки, пока сигнал свободен не приведет его в исходное состояние, в котором он доступен для использования другими процессами. Этот процесс используется как разделяемый ресурс: ацпу: АЦПУ // … (P
Q)… Внутри P или Q вывод последовательности строк, образующей файл, заключен между событиями ацпу.занят и ацпу.свободен: ацпу.занят → … ацпу.лев!”Вася” →… ацпу.лев!следстр → … ацпу.свободен 3.4.2. Общая память Цель этого раздела – привести ряд аргументов против использования общей памяти. Поведение систем параллельных процессов без труда реализуется на обыкновенной ЭВМ с хранимой программой с помощью режима разделения времени, при котором единственный процессор поочередно выполняет каждый из процессов, причем смена выполняемого процесса происходит по прерыванию, исходящему от некоторого внешнего или синхронизирующего устройства. При такой реализации легко позволить параллельным процессам совместно использовать общую память, выборка и загрузка которой осуществляется каждым процессом. Ячейка общей памяти – это разделяемая переменная: (счет : ПЕРЕМ // (счет.лев!0 → (P
Q))). Произвольное чередование присваиваний в ячейку общей памяти различными процессами является следствием многочисленных опасностей. Пример 3.27. Взаимное влияние. Разделяемая переменная счет используется для подсчета числа исполнений некоторого важного события. При каждом наступлении этого события соответствующий процесс Р или О пытается изменить значение счетчика парой взаимодействий счет.прав?х; счет. лев! (х + 1) К сожалению, эти два взаимодействия могут перемежаться аналогичной парой взаимодействий от другого процесса, в результате чего мы получим последовательность счет.прав?х → счет.прав?у → счет.лев!(у + 1) → счет.лев!(х+ 1) →... В итоге значение счетчика увеличится лишь на единицу, а не на два. Такого рода ошибки известны как взаимное влияние и часто допускаются при проектировании процессов, совместно использующих общую память. Кроме того, проявление такой ошибки недетерминировано; ее воспроизводимость очень ненадежна, и поэтому ее практически невозможно диагностировать обычными методами тестирования. Возможным решением этой проблемы может быть контроль за тем, чтобы смена процесса не происходила при совершении последовательности действий, нуждающихся в защите от чередования. Такая последовательность называется критическим участком. При реализации с одним процессором требуемое исключение обычно достигается запрещением всех прерываний на протяжении критического участка. Нежелательным эффектом такого решения является задержка ответа на прерывание; но хуже всего то, что оно оказывается полностью несостоятельным, как только к машине добавляется второй процессор. Рисунок 4.1. А, В, С – разделяемый ресурс, Р1 Р2 – процессы. Более приемлемое решение было предложено Э. Дейкстрой, которому принадлежит идея использования двоичных семафоров. Семафор можно описать как процесс, поочередно выполняющий действия с именами Р и V; СЕМ = (Р → V → СЕМ) Он описывается как совместно используемый ресурс (взаискл: СЕМ // ...). При условии, что все процессы подчиняются этой дисциплине, каждый из двух процессов не сможет влиять на изменение счетчика — произвести действие взаискл.V. Таким образом, критический участок, на котором происходит увеличение счетчика, должен иметь вид взаискл. Р → счет.прав?х → счет.лев!(х + 1) → взаискл.V → ... При условии, что все процессы подчиняются этой дисциплине, каждый из двух процессов не сможет влиять на изменение счетчика своим партнером. Но если какой-нибудь процесс пропустит Р или V или выполнит их в обратном порядке, результат будет непредсказуемым и может привести к катастрофической или (что, возможно, еще хуже) неуловимой ошибке. Избежать взаимного влияния гораздо более надежным способом можно, встроив необходимую защиту в саму конструкцию общей памяти, воспользовавшись знанием о предполагаемом способе ее использования. Если, например, переменная будет использоваться только как счетчик, то ее увеличение можно задать одной элементарной операцией счет.вверх, а соответствующий разделяемый ресурс определить как СТ0: счет:СТ0 //(...Р
Q..) На самом деле, есть все основания рекомендовать, чтобы каждый совместно используемый ресурс заранее проектировался для своих целей и, чтобы в разработке системы с элементами параллелизма универсальная память не использовалась совместно. Этот метод не только предупреждает серьезную опасность случайного взаимного влияния, но и позволяет получать конструкции, поддающиеся эффективной реализации на сетях распределенных процессорных элементов, а также на одно- и многопроцессорных ЭВМ с физически общей памятью. 3.4.3. Кратные ресурсы Выше мы описали, как некоторое число параллельных процессов с различным поведением могут совместно использовать один подчиненный процесс. Каждый процесс-пользователь соблюдает дисциплину чередования ввода и вывода или чередования сигналов занят/свободен с тем, чтобы в каждый момент времени разделяемым ресурсом пользовался не более чем один процесс. Такие ресурсы называют последовательно переиспользуемыми. В этом разделе вводятся массивы процессов, представляющие кратные ресурсы с одинаковым поведением; индексы в массиве обеспечивают тот факт, что каждый элемент достоверно взаимодействует только с использующим его процессом. Мы будем использовать индексы и операторы с индексами, смысл которых очевиден. Например: В последнем примере мы требуем, чтобы f была взаимно однозначной для того, чтобы выбор между альтернативами осуществлялся обстановкой. Пример 3.28. Повторно входимая подпрограмма Последовательно переиспользуемая общая подпрограмма может обслуживать вызывающие ее процессы только по одному. Если выполнение подпрограммы требует значительных вычислений, соответствующие задержки могут возникнуть и в вызывающем процессе. Если же для вычислений доступны несколько процессоров, нам ничто не мешает позволить нескольким экземплярам подпрограммы параллельно исполняться на различных процессорах. Подпрограмма, имеющая несколько параллельно работающих экземпляров, называется повторно входимой и определяется как массив параллельных процессов yдв: (УДВ)) //… Типичным вызовом этой подпрограммы будет (удв.3.лев!30 → удв.3.прав?у → ПРОПУСК) Присутствие индекса 3 гарантирует, что результат вызова получен от того же самого экземпляра удв, которому были посланы аргументы, даже несмотря на то, что в это же время некоторые другие параллельные процессы могут вызывать другие элементы массива, что приводит к чередованию сообщений типа удв.3.лев.30,...удв.2.лев.20,... удв.3.прав.60,... удв.2.прав.40,... Когда процесс вызывает повторно входимую подпрограмму, на самом деле не имеет значения, какой из элементов массива ответит на этот вызов; годится любой в данный момент свободный процесс. Поэтому вместо того, чтобы указывать конкретный индекс 2 или 3, вызывающий процесс должен делать произвольный выбор, используя конструкцию (удв.i.лев!30 → удв.i.прав?у → ПРОПУСК) При этом по-прежнему существенно требование, чтобы для передачи аргументов и (сразу после этого) получения результата использовался один и тот же индекс. Различают локальные вызовы процедуры, поскольку предполагается, что выполнение процедуры происходит на том же процессоре, что и выполнение вызывающего процесса, и дистанционные вызовы общей процедуры когда предполагает исполнение на отдельном, возможно, удаленном процессоре. Так как эффект дистанционного и локального вызова должен быть одинаковым, причины для использования именно дистанционного вызова могут быть только организационными или экономическими. Например, для хранения кода процедуры в секрете или для исполнения его на машине, имеющей какие-то специальные средства, слишком дорогие для установки их на той машине, на которой исполняются процессы-пользователи. Типичным примером таких дорогостоящих устройств могут служить внешние запоминающие устройства большой емкости — такие, как дисковая или доменная память. Пример 3.29. Общая внешняя память. Запоминающая среда разбита на В секторов, запись и чтение с которых могут производиться независимо. В каждом секторе может храниться один блок информации, которая поступает слева и выводится направо. К несчастью, запоминающая среда реализована по технологии разрушающего считывания, так что каждый блок может быть считан только один раз. Дополнительная память в целом представляет собой массив таких секторов с индексами, не превосходящими В: ДОППАМ = i: КОПИР Предполагается, что эта память используется как подчиненный процесс (доп: ДОППАМ //...). Внутри основного процесса доступ к этой памяти осуществляется взаимодействиями Доп.i.лев!блок →... доп.i.прав?у →,.. Дополнительная память может также совместно использоваться параллельными процессами. В этом случае действие (доп.i.лев!блок →...) одновременно займет произвольный свободный сектор с номером i и запишет в него значение блок. Аналогично, доп.1.прав?х за одно действие считает содержимое сектора i в х и освободит этот сектор для дальнейшего использования, вполне вероятно, уже другим процессом. Именно это упрощение и послужило истинной причиной использования КОПИР для моделирования каждого сектора. Конечно, успешное совместное использование этой дополнительной памяти требует от процессов-пользователей строжайшего соблюдения дисциплины. Процесс может совершить ввод информации с некоторого сектора, только если именно этот процесс последним выводил туда информацию, причем за каждым выводом рано или поздно должен последовать такой ввод. Несоблюдение этого порядка приводит к тупиковой ситуации или к еще худшим последствиям. 3.4.4. Планирование ресурсов Когда ограниченное число ресурсов разделено между большим числом потенциальных пользователей, всегда существует возможность того, что некоторым пользователям, стремящимся занять ресурс, приходится ждать, пока его освободит другой процесс. Если к моменту освобождения ресурса его хотят занять два или более процесса, выбор того, который из ожидающих процессов получит ресурс, во всех приводившихся примерах был недетерминированным. Само по себе это большого значения не имеет, но предположим, что к тому моменту, когда ресурс снова освободится, к множеству ожидающих присоединится еще один процесс. Поскольку выбор между ожидающими процессами по-прежнему недетерминирован, может случиться, что повезет именно вновь присоединившемуся процессу. Если ресурс сильно загружен, так может случиться снова и снова. В результате может оказаться, что некоторые процессы будут откладываться бесконечно или по крайней мере в течение полностью неопределенного времени. С этой проблемой, называемой бесконечным перехватом, мы уже знакомы (см. п. 3.2.3.5). Одним из решений проблемы является обеспечение того, чтобы все ресурсы были несильно загружены. Этого можно достигнуть либо введением дополнительных ресурсов, либо установлением высокой платы за предоставляемые услуги. Фактически это единственно приемлемые решения в случае постоянно загруженного ресурса. К сожалению, даже в среднем несильно загруженный ресурс достаточно часто оказывается сильно загруженным в течение длительных периодов (в часы пик). Иногда проблему удается сгладить введением дифференцированного тарифа в попытке регулирования спроса, но это не всегда помогает и даже не всегда удается. В течение таких пиков задержки процесса-пользователя в среднем неизбежны. Важно лишь следить за сообразностью и предсказуемостью таких задержек — вы, несомненно, предпочтете знать, что вас обслужат в течение часа, чем гадать, сколько еще придется ждать—одну минуту или целые сутки. Задача распределения ресурса между ожидающими пользователями известна как планирование ресурсов. Для успешного планирования необходимо знать, какие процессы в текущий момент ожидают получения ресурса. По этой причине получение ресурса отныне нельзя рассматривать как одно элементарное событие. Его необходимо разбить на два события: пожалуйста, осуществляющее запрос ресурса, спасибо, сопровождающее реальное получение ресурса. Период между пожалуйста и спасибо для каждого процесса является временем, в течение которого он ждет ресурс. Чтобы различать ожидающие процессы, каждое вхождение события пожалуйста, спасибо и свободен помечено отличным от других натуральным индексом. При каждом запросе ресурса процесс получает номер с помощью конструкции: (рес.i. пожалуйста; реc.i.спасибо;...; реc.i.свободен → ПРОПУСК.) Простым и эффективным способом планирования ресурса является назначение его процессу, ожидавшему дольше всех. Такая политика называется «первым пришел — первым, обслужен» (FСFS) или «первым пришел — первым ушел» (FIFO) и представляет собой принцип очереди, соблюдаемый, к примеру, пассажирами на автобусной остановке. В заведении же типа поликлиники, где посетители не могут; или не хотят выстраиваться в очередь, для достижения того же результата действует другой механизм. Регистратура выдает талоны со строго возрастающими последовательными номерами. При входе в поликлинику посетитель берет талон. Когда врач освободился, он вызывает посетителя, имеющего талон с наименьшим номером, но еще не принятого. Этот алгоритм, называемый алгоритмом поликлиники, более строго описан ниже. Мы будем предполагать, что одновременно могут обслуживаться до R посетителей, Пример 3.30. Алгоритм поликлиники. Нам потребуются три счетчика: р — посетители, сказавшие пожалуйста, t — посетители, сказавшие спасибо, r — посетители, освободившие свои ресурсы. Очевидно, что в любой момент времени r £ t £ р. Кроме того, р всегда будет номером, который получает очередной посетитель, приходящий в поликлинику, а t — номером очередного обслуживаемого посетителя; далее, р — t будет числом ожидающих посетителей, а R + r — t — числом ожидающих врачей. Вначале значения всех счетчиков равны нулю и могут быть вновь положены равными нулю в любой момент, когда их значения совпадают — например, вечером, после ухода последнего посетителя. Одной из основных задач алгоритма является обеспечение того, чтобы никогда не было одновременно свободного ресурса и ждущего посетителя; как только возникает такая ситуация, следующим событием должно стать спасибо посетителя, получающего ресурс. ПОЛИКЛИНИКА = B0,0,0 Вp,t,r =if 0 < r = t = рthen ПОЛИКЛИНИКА else if R+r – t > 0 AND р — t > 0 then t.спасибо → Вр,t+1,r еlse (р.пожалуйста → Вр+1,t, r | i.свободен → Вр,t,r+1)).
Программирование параллельных вычислений
Исполнение процессов типичной параллельной программы прерывается значительно чаще, чем процессов, работающих в последовательной среде, так как… В соответствии с возможностями параллельного компьютера процессы… Рассмотренные механизмы связи необязательно используются только непосредственно на соответствующих архитектурах. Так…Еnd
Строка 1 описывает монитор с именем счет.
2 описывает локальную для монитора общую переменную n. Она доступна только внутри самого монитора.
З - 5 описывают три процедуры и их тела. Звездочки обеспечивают вызов этих процедур из программы, использующей монитор.
6 Здесь начинается исполнение монитора.
7 Три жирные точки обозначают внутреннее предложение, соответствующее блоку, который будет использовать монитор.
8 При выходе из использующего блока печатается конечное значение n (если оно ненулевое).
Новый экземпляр этого монитора может быть описан локальным для блока Р:
instanсе ракетa: счет; Р
Внутри блока Р можно вызывать помеченные звездочками процедуры, используя команды
ракета.вверх;... ракета.вниз;. ..;, ifракета.приземлthen...
Непомеченная же процедура или такая переменная, как n, недостижимы из Р. Свойственное мониторам взаимное исключение позволяет вызывать процедуру монитора любому числу процессов внутри Р без взаимного влияния при изменении n. Заметим, что попытка вызвать ракета.вниз при n. = 0 будет отложена до тех пор, пока некоторый другой процесс внутри Р не вызовет ракета.вверх. Это гарантирует, что значение n никогда не станет отрицательным.
Неэффективность повторяющейся проверки входных условий привела к появлению мониторов с более сложной схемой явного ожидания и явной подачей сигнала о возобновлении ожидающего процесса. Эти схемы даже позволяют приостанавливаться процедурному вызову в процессе его исполнения под воздействием автоматически возникающего исключения до того момента, когда некоторый последующий вызов процедуры другим процессом подаст сигнал о возобновлении приостановленного процесса. Таким путем можно эффективно реализовать множество оригинальных способов планирования, которые реализуются программой-планировщиком.
Так как в мониторе ожидающих процессов может быть несколько, простой порядок обслуживания очереди состоящий в том, что освобождается процесс, ожидающий дольше всех, гарантирует, что ни один из обратившихся процессов не будет задержан на неопределенное время.
Модели параллельных вычислений
Из-за сложности параллельных компьютеров и их существенного отличия от традиционных однопроцессорных компьютеров нельзя просто воспользоваться… 3.6.1. Процесс/канал В этой модели программы состоят из одного или более процессов, распределенных по процессорам. Процессы выполняются…Сети Петри
Введение в сети Петри
Сети Петри это инструмент для математического моделирования и исследования сложных систем. Цель представления системы в виде сети Петри и последующего анализа этой сети состоит в получении важной информации о структуре и динамическом поведении моделируемой системы. Эта информация может использоваться для оценки моделируемой системы и выработки предложений по ее усовершенствованию. Впервые сети Петри предложил немецкий математик Карл Адам Петри.
Сети Петри предназначены для моделирования систем, которые состоят из множества взаимодействующих друг с другом компонент. При этом компонента сама может быть системой. Действиям различных компонент системы присущ параллелизм. Примерами таких систем могут служить вычислительные системы, в том числе и параллельные, компьютерные сети, программные системы, обеспечивающие их функционирование, а также экономические системы, системы управления дорожным движением, химические системы, и т. д.
В одном из подходов к проектированию и анализу систем сети Петри используются, как вспомогательный инструмент анализа. Здесь для построения системы используются общепринятые методы проектирования. Затем построенная система моделируется сетью Петри, и модель анализируется. Если в ходе анализа в проекте найдены изъяны, то с целью их устранения проект модифицируется. Модифицированный проект затем снова моделируется и анализируется. Этот цикл повторяется до тех пор, пока проводимый анализ не приведет к успеху.
Другой подход предполагает построение проекта сразу в виде сети Петри. Методы анализа применяются только для создания проекта, не содержащего ошибок. Затем сеть Петри преобразуется в реальную рабочую систему.
В первом случае необходима разработка методов моделирования систем сетями Петри, а во втором случае должны быть разработаны методы реализации сетей Петри системами.
Основные определения
Пусть мультимножество это множество, допускающее вхождение нескольких экземпляров одного и того же элемента. Сеть Петри N является четверкой N=(P,Т,I,O), где P = {p1, p2,..., pn} — конечное множество позиций, n ³ 0;Моделирование систем на основе сетей Петри
4.3.1. События и условия Представление системы сетью Петри основано на двух основополагающих понятиях:… Возникновение события в системе возможно, если выполняются определённые условия – предусловия события. Возникновение…Begin
if mod(Y,2)=0