Основы многопоточного и распределенного программирования

       

Свойства безопасности и живучести


Свойство программы — это ее атрибут, истинный для любой возможной истории выполне­ния (см. раздел 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) — программа работает, но процессы не про­двигаются. Активный тупик — это активно ожидающий аналог взаимоблокировки (клинча). Отсутствие активного тупика, как и отсутствие клинча, является свойством безопасности. Плохим считается состояние, в котором все процессы зациклены, но не выполняется ни одно из условий (окончания) задержки. С другой стороны, продвижение любого из процессов яв­ляется свойством живучести. Хорошим в этом случае является то, что цикл активного ожида­ния отдельного процесса когда-нибудь завершится.

Содержание раздела