Свойства безопасности и живучести
Свойство программы — это ее атрибут, истинный для любой возможной истории выполнения (см. раздел 2.1). Каждое интересующее нас свойство можно сформулировать как свойство безопасности или живучести. Свойство безопасности утверждает, что во время выполнения программы не происходит ничего плохого; свойство живучести утверждает, что в конечном счете происходит что-то хорошее. В последовательных программах основное свойство безопасности состоит в корректности заключительного состояния, а живучести — в завершимости про-
Глава 2 Процессы и синхронизация 73
граммы. Для параллельных программ эти свойства одинаково важны. Однако есть и другие интересные свойства безопасности и живучести, применимые к параллельным программам.
Два важных свойства безопасности параллельных программ — взаимные исключения и отсутствие взаимоблокировок (deadlock). Для взаимного исключения плохо, когда несколько процессов одновременно выполняют критические секции операторов. Для взаимоблокировки плохо, когда все процессы ожидают условий, которые никогда не выполнятся.
Вот примеры свойств живучести параллельных программ: процесс в конце концов войдет в критическую секцию, запрос на обработку будет принят, а сообщение достигнет места назначения. Свойства живучести зависят от стратегии планирования, которая определяет, какое из неделимых действий должно быть выполнено следующим.
В данном разделе представлены два метода обоснования свойств безопасности. Затем описаны различные типы стратегий планирования процессора и их влияние на свойства живучести.
2.8.1. Доказательство свойств безопасности
Каждое выполняемое программой действие основано на ее состоянии. Если программа не удовлетворяет свойству безопасности, должно существовать некоторое "плохое" состояние, не удовлетворяющее этому свойству. Например, если не удовлетворяется свойство взаимного исключения, то должно быть некоторое состояние, в котором два (или более) процесса одновременно находятся в своих критических секциях.
Или если процессы заблокировали друг друга (вошли в клинч), то должно быть состояние, в котором это происходит.
Эти замечания ведут к простому методу доказательства, что программа удовлетворяет свойству безопасности. Пусть предикат BAD описывает плохое состояние программы. Тогда программа удовлетворяет соответствующему свойству безопасности, если BAD ложен в каждом состоянии любой возможной истории выполнения программы. Чтобы по данной программе S показать, что предикат BAD не является истинным в любом состоянии, нужно доказать, что он ложен в начальном состоянии, во втором состоянии и т.д., причем состояние изменяется в результате выполнения неделимых действий.
Если программа не должна попадать в BAD-состояние, она всегда должна быть в GOOD-состоянии, где предикат GOOD эквивалентен -<BAD. Следовательно, эффективный способ обеспечить свойства безопасности — определить предикат BAD и его отрицание, чтобы получить GOOD, а затем проверить, является ли предикат GOOD глобальным инвариантом, т.е. предикатом, истинным в каждом состоянии программы. Чтобы сделать предикат глобальным инвариантом, можно использовать синхронизацию (как это уже было и еще не раз будет показано в дальнейших главах).
Вышеописанный метод является общим для доказательства свойств безопасности. Существует связанный с ним, но несколько более специализированный метод, также весьма полезный. Рассмотрим следующий фрагмент программы.
со # процесс 1
...; {pre(Sl)} SI; ...
// # процесс 2
. ..,- {pre(S2)> S2; ...
ос
Здесь есть два оператора, по одному в каждом процессе, и два связанных с ними предусловия (предикаты, истинные перед выполнением каждого оператора). Предположим, что эти предикаты не подвержены вмешательству, а их конъюнкция ложна:
pre(Sl) л pre(S2) == false
Это значит, что оба процесса одновременно не могут выполнять данные операторы, поскольку предикат, который ложен, не характеризует ни одного состояния программы (пустое множество состояний, если хотите).
Этот метод называется исключением конфигураций, поскольку
74 Часть 1. Программирование с разделяемыми переменными
он исключает конфигурации программы, в которых первый процесс находится в состоянии pre (S1), а второй в это же время — в состоянии pre (S2).
В качестве примера рассмотрим схему доказательства корректности программы копирования массива (см. листинг 2.3). Оператор await в каждом процессе может стать причиной задержки. Процессы заблокируют друг друга ("войдут в клинч"), если оба будут приостановлены и ни один не сможет продолжить работу. Процесс Producer приостанавливается, если он находится в операторе await, а условие (окончания) задержки ложно; в этом состоянии истинным является следующий предикат. PC ^р<п^р ' = с
Следовательно, когда приостановлен процесс Producer, истинно условие р > с. Аналогично приостанавливается процесс Consumer, если он находится в операторе await, а условие (окончания) задержки ложно; это состояние удовлетворяет такому предикату.
/Слс<плр<=с
Поскольку условия р > сир <= с не могут быть истинными одновременно, процессы не могут одновременно находиться в этих состояниях, т.е. взаимоблокировка возникнуть не может.
2.8.2. Стратегии планирования и справедливость
Большинство свойств живучести зависит от справедливости (fairness), связанной с гарантиями, что каждый процесс получает шанс на продолжение выполнения независимо от действий других процессов. Каждый процесс выполняет последовательность неделимых действий. Неделимое действие в процессе называется подходящим, или возможным (eligible), если оно является следующим неделимым действием в процессе, которое может быть выполнено. При наличии нескольких процессов существует несколько возможных неделимых действий. Стратегия планирования (scheduling policy) определяет, какое из них будет выполнено следующим. В этом разделе определены три степени справедливости, которые могут быть обеспечены стратегией планирования.
Напомним, что безусловное неделимое действие — это действие, не имеющее условия задержки. Рассмотрим следующую простую программу, в которой процессы выполняют безусловные неделимые действия.
bool continue = true; со while (continue); // continue = false; oc
Допустим, что стратегия планирования назначает процессор для процесса до тех пор, пока тот не завершится или не будет приостановлен (задержан). При одном процессоре данная программа не завершится, если вначале будет выполняться первый процесс. Однако, если второй процесс в конце концов получит право на выполнение, программа будет завершена. Данная ситуация отражена в следующем определении.
(2.6) Безусловная справедливость (unconditional fairness). Стратегия планирования безусловно справедлива, если любое подходящее безусловное неделимое действие в конце концов выполняется.
Для программы, приведенной выше, безусловно справедливой стратегией планирования на одном процессоре было бы циклическое (round-robin) выполнение, а на мультипроцессоре — синхронное.
Если программа содержит условные неделимые действия— операторы await с логическими условиями в, необходимо делать более сильные предположения, чтобы гарантировать продвижение процесса. Причина в том, что условное неделимое действие не может быть выполнено, пока условие в не станет истинным.
Глава 2. Процессы и синхронизация 75
(2.7) Справедливость в слабом смысле (weak fairness). Стратегия планирования справедлива в слабом смысле, если: 1) она безусловно справедлива, и 2) каждое подходящее условное неделимое действие в конце концов выполняется, если его условие становится и затем остается истинным, пока его видит процесс, выполняющий условное неделимое действие.
Таким образом, если действие (await (В) S;) является подходящим и условие В становится истинным, то в остается истинным по крайней мере до окончания выполнения условного неделимого действия.
Циклическая стратегия и стратегия квантования времени являются справедливыми в слабом смысле, если каждому процессу дается возможность выполнения. Причина в том, что любой приостановленный процесс в конце концов увидит, что условие (окончания) его задержки истинно.
Справедливости в слабом смысле, однако, недостаточно для гарантии, что любой подходящий оператор await в конце концов выполняется. Это связано с тем, что условие может изменить свое значение (от ложного к истинному и обратно к ложному), пока процесс приостановлен. В этом случае необходима более сильная стратегия планирования.
(2.8) Справедливость в сильном смысле (strong fairness). Стратегия планирования справедлива в сильном смысле, если: 1) она безусловно справедлива, и 2) любое подходящее условное неделимое действие в конце концов выполняется в предположении, что его условие бывает истинным бесконечно часто.
Условие бывает истинным бесконечно часто, если оно истинно бесконечное число раз в каждой истории (не завершающейся) программы. Чтобы стратегия планирования была справедливой в сильном смысле, действие должно выбираться для выполнения не только тогда, когда его условие ложно, но и когда оно истинно.
Чтобы увидеть различия между справедливостью в слабом и сильном смысле, рассмотрим следующую программу.
bool continue = true, try = false;
со while (continue) (try = true; try = false;}
// (await (try) continue = false;)
oc
При стратегии, справедливой в сильном смысле, эта программа в конце концов завершится, поскольку значение переменной try бесконечно часто истинно. Однако при стратегии планирования, справедливой в слабом смысле, программа может не завершиться, поскольку значение переменной try также бесконечно часто является ложным.
К сожалению, невозможно разработать стратегию планирования процессора, которая была бы и практичной, и справедливой в сильном смысле. Еще раз рассмотрим программу, приведенную выше. На одном процессоре диспетчер, чередующий действия двух процессов, будет справедливым в сильном смысле, поскольку второй процесс будет видеть состояние, в котором значение переменной try истинно.
Однако такой планировщик невозможно реализовать практически. Циклическое планирование и планирование с квантованием времени практичны, но в общем случае не являются справедливыми в сильном смысле, поскольку процессы выполняются в непредсказуемом порядке. Диспетчер мультипроцессора, выполняющего процессы параллельно, также практичен, но не является справедливым в сильном смысле. Причина в том, что второй процесс может проверять значение переменной try только тогда, когда оно ложно. Это, конечно, маловероятно, но теоретически возможно.
Для дальнейшего объяснения различных видов стратегий планирования вернемся к программе копирования массива в листингах 2.2 и 2.3. Как отмечалось выше, эта программа свободна от блокировок. Таким образом, программа будет завершена, поскольку каждый процесс регулярно получает возможность продвинуться в своем выполнении. Процесс будет продвигаться, поскольку стратегия справедлива в слабом смысле. Дело в том, что, когда один процесс делает истинным условие (окончания) задержки другого процесса, это условие остается истинным, пока другой процесс не будет продолжен и не изменит разделяемые переменные.
76 Часть 1. Программирование с разделяемыми переменными
Оба оператора await в программе копирования массива имеют вид (await (В) ;), а условие в ссылается только на одну переменную, изменяемую другим процессом. Следовательно, оба оператора await могут быть реализованы циклами активного ожидания. Например, (await (р == с) ;) в процессе Producer может быть реализован следующим оператором. while (р != с);
Программа завершится, если стратегия планирования безусловно справедлива, поскольку теперь нет условных неделимых действий и процессы чередуют доступ к разделяемому буферу. Однако в общем случае не верно, что безусловно справедливая стратегия планирования гарантирует завершение цикла активного ожидания. Причина в том, что при безусловно справедливой стратегии всегда может быть запланировано к выполнению неделимое действие, проверяющее условие цикла как раз тогда, когда оно истинно (как в приведенной выше программе).
Если все циклы активного ожидания программы зациклились навсегда, о программе говорят, что она вошла в активный тупик (livelock) — программа работает, но процессы не продвигаются. Активный тупик — это активно ожидающий аналог взаимоблокировки (клинча). Отсутствие активного тупика, как и отсутствие клинча, является свойством безопасности. Плохим считается состояние, в котором все процессы зациклены, но не выполняется ни одно из условий (окончания) задержки. С другой стороны, продвижение любого из процессов является свойством живучести. Хорошим в этом случае является то, что цикл активного ожидания отдельного процесса когда-нибудь завершится.
