9.7. Свойства живости (осуществимости)

Эта категория свойств выражается общей формулой:

Эта формула означает, что для каждого допустимого вычисления, если , является изначально истинной, должна в конце концов также стать истинной. В отличие от свойств инвариантности, которые описывают только сохранение желаемых свойств при переходах от одного места к другому, свойства живости говорят о том, что некоторые события в конце концов должны осуществиться. Эта формула в определенном смысле формулирует цель, которая обязательно должна быть достигнута после некоторого, в общем случае неизвестного, числа тактов.

Заметим, что вследствие замкнутости оператора 0 относительно множества суффиксов допустимых вычислений приведенная формула, выражающая свойство живости, эквивалентна следующей:

9.7.1. Абсолютная корректность

Это свойство похоже на частичную корректность и имеет смысл только для программ с терминальными местами. Говорят, что программа абсолютно корректна, если для всех значений входных переменных х, удовлетворяющих ее окончание гарантировано и выходное значение у после окончания выполнения программы удовлетворяет Более того, пусть обозначает набор терминальных мест программы. Тогда абсолютная корректность выражается так:

Это означает, что если мы имеем допустимую выполняемую последовательность, начинающуюся в ситуации, определяемой местами и значениями в которой истинна, то далее для этой выполняемой

последовательности гарантированно будет иметь место ситуация, определяемая и удовлетворяющая

Пример. Программа вычисления факториала:

Пример. Программа подсчета вершин дерева:

Пример. Программа вычисления биноминальных коэффициентов:

9.7.2. Гарантированное осуществление

Свойства живости позволяют выразить причинно-следственную связь между любыми двумя событиями, возникающими в течение выполнения программы, а не только между началом и окончанием программы. Такая возможность особенно существенна, когда программа является циклической. Общий вид формулы, выражающей свойство гарантированного осуществления, следующий.

Эта формула означает, что если истинна в месте то в конце концов будет достигнуто место в котором истинна.

Пример. Для программы подсчета числа вершин в дереве утверждение гарантированного осуществления, которое служит основой для доказательства ее корректности, имеет вид

где с использованы в роли глобальных переменных, в то время как и С — локальные переменные. Это утверждение говорит о том, что нахождение в с непустым стеком гарантирует попадание в конце концов в одном из последующих тактов снова в При этом верхний элемент стека и будет уже взят и значение Сбудет увеличено на число вершин в этом верхнем элементе.

Следующие свойства живости имеют значение для параллельных программ, содержащих более одного процесса.

9.7.3. Доступность

Рассмотрим снова процесс, который имеет критическую секцию С. В предыдущем разделе при изучении свойства взаимного исключения было

показано, как установить защиту для такой секции от вмешательства со стороны других процессов. Продолжающим и дополняющим свойством к свойству взаимного исключения является свойство доступности, означающее следующее: если процесс желает войти в свою критическую секцию, он, в конечном счете, попадает туда, т.е. не будет неопределенно долго удерживаться механизмом зашиты. Очевидно, что защитный механизм является бесполезным, если он не позволяет в конце концов процессу войти в его критическую секцию.

Пусть — место перед критической секцией. Тот факт, что процесс находится в отражает намерение войти в критическую секцию. Пусть С является множеством мест в критической секции. Тогда выражение свойства доступности выглядит следующим образом:

Правильная конструкция критической секции должна гарантировать выполнение этих двух полезных свойств: взаимного исключения и доступности.

9.7.4. Беступиковость

Более общий класс свойств живости связан с возможностью осуществления продвижения процедуры вычисления любого процесса, находящегося в месте Здесь мы не ограничиваемся только местами, содержащими семафорные команды. Рассмотрим произвольное нетерминальное место в некотором процессе , т.е. Если вычисление процесса должно развиваться таким образом, что он обязательно должен покинуть место то он не может оставаться блокированным в вследствие ошибки диспетчера, который управляет выполнением процесса Р.. Это означает, что процесс Р., находясь в месте в котором истинна формула в месте должен его обязательно покинуть, в результате чего станет истинной формула в месте Следовательно, свойство беступиковости для любого места может быть выражено следующим образом:

или эквивалентной формулой

которая означает, что мы никогда не будем заблокированы в месте

Свойство беступиковости так же известно как свобода от индивидуального зависания, определяемого как ситуация, в которой некоторые процессы, которые не находятся в терминальных местах, не могут продвигаться (выполняться), несмотря на то, что программа в целом выполняется за счет продвижения других процессов. Заметим, что это более сильное требование,

чем отсутствие дедлока, поскольку считается, что программа не попала в дедлок до тех пор, пока хотя бы один процесс выполняется.

9.7.5. Отзывчивость

Очень важным классом программ, относящихся обычно к параллельным программам, являются операционные системы и такие программы реального времени, как системы резервирования билетов в авиации или другие системы баз данных, функционирующие в режиме on-line. Эти программы удобно рассматривать как непрерывные или циклические программы, работающие постоянно. Остановка выполнения этих программ обычно отражает ошибочные условия. Следовательно, эти программы работают не на получение конечного результата, а для результатов, производимых в течение их бесконечного выполнения. Таким образом, понятия абсолютной и частичной корректности здесь не применимы и должны быть заменены утверждениями, учитывающими непрерывное выполнение программ. Одним из важнейших свойств таких программ является отзывчивость.

Пример. Предположим, что программа, моделирующая операционную систему (диспетчер), обслуживает ряд программ (процессов) пользователей управляя распределением между ними ресурсов. Ресурсами могут быть жесткий диск, главная память и т.д. Пусть программы пользователей взаимодействуют с диспетчером, запрашивая ресурсы через булевы (пропозициональные) переменные Переменная устанавливается истинной пользователем программы чтобы сигнализировать о запросе ресурса. Переменная устанавливается истинной операционной системой С, сообщающей тем самым пользователю что он может взять ресурс. После использования ресурса пользователь возвращает ресурс обратно системе С, присваивая переменной ложное значение. Операционная система признает освобождение ресурса присвоением переменной ложного значения.

Итак, имеем

Утверждением о, означающим, что диспетчер справедливо реагирует на запросы потребителя, является

т.е. когда бы не стала истинной в конце концовбудет истинной. Заметим, что это утверждение не требует, чтобы становилась истинной, когда диспетчер находится в каком-либо определенном месте.

Подобным образом необходимо обеспечить подтверждение освобождения ресурса присвоением ложного значения:

Более того, система не сможет работать нормально, если не будет обеспечено должного взаимодействия между программами пользователей. Например, система не может обещать пользователю предоставления ресурса, если пользователь который в это время занимает его в конце концов его не освободит.

Следовательно, требуется, чтобы поведение пользователя удовлетворяло определенным требованиям с а именно:

Это утверждение говорит о том, что в случае предоставления потребителю ресурса этот ресурс в конце концов будет освобожден. К сформулированным утверждениям обычно добавляются утверждения, гарантирующие правильное непрерывное поведение С. Одним из таких утверждений является следующее:

означающее, что в любом такте диспетчер предоставляет ресурс самое большее одному потребителю. Оно относится к типу утверждений взаимного исключения.

Введем теперь утверждение корректного поведения диспетчера С в целом:

Корректное поведение, ожидаемое от пользователей имеет вид

Проблема доказательства правильного поведения диспетчера С может быть решена двумя различными путями.

В первом случае рассматривается параллельная программа, которая состоит из одного диспетчера С. Переменные рассматриваются как входные и выходные переменные этой программы. Значения переменных устанавливаются внешними пользователями Для этой программы необходимо доказать истинность формулы

задающей свойство отзывчивости. Смысл этой формулы состоит в том, что при условии непрерывно правильного поведения пользователей, формирующих внешнее воздействие в соответствии с формулой диспетчер С должен всегда вести себя соответствующим образом в соответствии с формулой правильного поведения

Во втором случае рассматривается параллельная программа Р, которая состоит из операционной системы С, работающей совместно с программами т.е.

Для каждого устанавливается модель, которая гарантирует выполнение условия с.. В упрошенном виде такую модель можно представить как следующую профамму пользователя Я при начальном значении Ложь:

Если полагать, что эта модель хорошо представляет реального потребителя в части его взаимодействия с то для гарантии корректного поведения программы необходимо доказать истинность формулы

также задающей свойство отзывчивости.

Таким образом, возможны две моделирующие ситуацию альтернативы: рассмотрение диспетчера в единственном числе и во взаимодействии с внешними пользователями посредством переменных или рассмотрение совокупной системы, состоящей из . В первом случае соответствующее поведение внешних по отношению к пользователей проверяется и обеспечивается отдельно посредством непрерывного сохранения значения Во втором случае поведение пользователей проверяется вместе с соответствующим поведением

Аналогичный анализ может быть распространен на другие ситуации, где необходимо обеспечивать взаимодействие с внешними устройствами и реагировать соответствующим образом на внешние сигналы.