Состояние, действие, история и свойства
Состояние параллельной программы состоит из значений переменных программы в некоторый момент времени. Переменные могут быть явно определенными программистом или неявными (вроде программного счетчика каждого процесса), хранящими скрытую информацию о состоянии. Параллельная программа начинает выполнение в некотором исходном состоянии. Каждый процесс программы выполняется независимо, и по мере выполнения он проверяет и изменяет состояние программы.
Процесс выполняет последовательность операторов. Оператор, в свою очередь, реализуется последовательностью неделимых действий. Эти действия проверяют или изменяют со-
50 Часть 1. Программирование с разделяемыми переменными
стояние программы неделимым образом. Примерами неделимых действий являются непрерываемые машинные инструкции, которые загружают и сохраняют слова памяти.
Выполнение параллельной программы приводит к чередованию последовательностей неделимых действий, производимых каждым процессом. Конкретное выполнение каждой программы может быть рассмотрено как история s0—> s, —>... —>sn, где s0— начальное состояние. Переходы между состояниями осуществляются неделимыми действиями, изменяющими состояние. Историю также называют трассой последовательности состояний. Даже параллельное выполнение можно представить в виде линейной истории, поскольку параллельная реализация набора неделимых действий эквивалентна их выполнению в некотором последовательном порядке. Изменение состояния, вызванное неделимым действием, неразделимо, и, следовательно, на него не могут повлиять неделимые действия, производимые примерно в это же время.
Каждое выполнение параллельной программы порождает историю. Для всех, кроме самых тривиальных программ, число возможных историй громадно. Дело в том, что следующим в истории может стать неделимое действие любого процесса. Следовательно, существует много способов чередования действий, даже если выполнение программы всегда начинается в одном и том же исходном состоянии.
Кроме того, в каждом процессе обычно есть условные операторы, и, следовательно, возможны различные действия при различных изменениях в состоянии.
Цель синхронизации — исключить нежелаемые истории параллельной программы. Взаимное исключение состоит в комбинировании неделимых действий, реализуемых непосредственно аппаратным обеспечением в виде последовательностей действий, которые называются критическими секциями. Они должны быть неделимыми, т.е. их нельзя прервать действия-• ми других процессов, которые ссылаются на те же переменные. Синхронизация по условию (условная синхронизация) означает, что действие будет осуществлено, когда состояние будет удовлетворять заданному логическому условию. Обе формы синхронизации могут приостанавливать процессы, ограничивая набор последующих неделимых действий.
Свойством программы называется атрибут, который является истинным при любой возмож--ной истории программы и, следовательно, при всех ее выполнениях. Есть два типа свойств: безопасность и живучесть. Свойство безопасности заключается в том, что программа никогда не попадает в "плохое" состояние (при котором некоторые переменные могут иметь нежелательные значения). Свойство живучести означает, что программа в конце концов всегда попадает в "хорошее" состояние, т.е. состояние, в котором все переменные имеют желаемые значения.
Примером свойства безопасности является частичная корректность (правильность). Программа частично корректна (правильна), если правильно ее заключительное состояние (при условии, что программа завершается). Если программе не удается завершить выполнение, она может никогда не выдать правильный результат, но не существует такой истории, при которой программа завершается, не выдавая правильного результата. Завершимость — пример свойства живучести. Программа завершается, если завершается каждый цикл или вызов процедуры, т.е. длина каждой истории конечна. Тотальная (полная) корректность программы — это свойство, объединяющее частичную корректность и завершимость: программа полностью корректна, если она всегда завершается, выдавая при этом правильный результат.
Взаимное исключение — это пример свойства безопасности в параллельной программе. При плохом состоянии два процесса такой программы одновременно выполняют действия в разных критических секциях. Возможность в конце концов войти в критическую секцию — пример свойства живучести в параллельной программе. В хорошем состоянии каждый процесс выполняется в своей критической секции.
Как же демонстрировать, что данная программа обладает желаемым свойством? Обычный подход состоит в тестировании, или отладке. Его можно охарактеризовать фразой "запусти программу и посмотри, что получится". Это соответствует перебору некоторых возможных историй программы и проверке их приемлемости. Недостаток такой проверки состоит в том, что каждый тест касается только одной истории выполнения, а ограниченное число тестов вряд ли способно продемонстрировать отсутствие плохих историй.
Глава 2. Процессы и синхронизация 51
Второй подход— использование операторных рассуждений, которые можно назвать "исчерпывающий анализ случаев" (перебираются все возможные истории выполнения программы). Для этого анализируются способы чередования неделимых действий процессов. К сожалению, в параллельной программе число возможных историй обычно очень велико (поэтому метод "изнурителен"5). Предположим, что параллельная программа содержит п процессов и каждый из них выполняет последовательность из m неделимых действий. Тогда число различных историй программы составит (n-m) !/(m!n). Для программы из трех процессов, каждый из которых выполняет всего две неделимые операции, возможны 90 различных историй! (Числитель в формуле — это количество возможных перестановок из n-m действий. Но, поскольку каждый процесс выполняет последовательность действий, для него возможен только один порядок следования m действий; знаменатель отбрасывает все варианты с неправильным порядком следования.
Эта формула дает количество, равное числу способов перемешать п колод по m карт в каждой, при условии, что относительный порядок карт в каждой колоде сохраняется.)
Третий подход— применение утвердительных рассуждений (assertional reasoning); его можно назвать "абстрактный анализ". В этом методе формулы логики предикатов называются утверждениями и используются для описания наборов состояний — например, всех состояний, у которых х > 0. Неделимые действия рассматриваются как предикатные преобразователи, поскольку они меняют состояние программы, удовлетворяющее одному предикату, на состояние, удовлетворяющее другому. Преимуществом данного подхода является компактное представление состояний и их преобразований. Но еще важнее то, что он приводит к методу построения и анализа программ, согласно которому объем работы прямо пропорционален числу неделимых действий в программе.
Используем метод утверждений как инструмент построения и анализа решений многих нетривиальных задач. При разработке алгоритмов также будет применяться метод операторных рассуждений. Наконец, многие программы этой книги были протестированы. Однако в результате тестирования можно только обнаружить наличие ошибок, а не гарантировать их отсутствие. Кроме того, параллельные программы очень сложны в тестировании и отладке, поскольку, во-первых, трудно остановить сразу все процессы и проверить их состояние, и, во-вторых, в общем случае каждое выполнение программы приводит к новой истории.
