Парадокс предусловий
Только что обнаруженная ситуация может обеспокоить, поскольку, на первый взгляд, она показывает несостоятельность в параллельном контексте ключевой методологии проектирования по контракту. Для очереди при последовательных вычислениях у нас были полностью определены спецификации взаимных обязательств и преимуществ (аналогично стекам в лекции 11 курса "Основы объектно-ориентированного программирования"):
| Клиент | (Выполнить предусловие:) Вызывать put(x) только для непустой очереди | (Из постусловия:) Получить обновленную, непустую очередь с добавленным x |
| Поставщик | (Выполнить постусловие:) Обновить очередь, добавив x и обеспечив выполнение not empty | (Из постусловия:) Обработка защищена предположением о том, что очередь неполна |
Неявно за такими контрактами стоит принцип "отсутствия скрытых условий": предусловие является единственным требованием, которое должен выполнить клиент, чтобы получить результат. Если вы вызываете put с неполной очередью на входе, то вам предоставляется результат этой подпрограммы, удовлетворяющий ее постусловию.
Но в параллельном контексте при наличии сепаратных поставщиков, таких как BOUNDED_BUFFER, дела клиента складываются весьма плачевно: как бы мы не старались ублажить поставщика, обеспечивая выполнение требуемого им предусловия, мы никогда не можем быть уверены в том, что его пожелания удовлетворены! Однако выполнение предусловия необходимо для корректной работы поставщика. Например, вполне вероятно, что тело подпрограммы put из класса BOUNDED_QUEUE (то же, что и в классе BOUNDED_BUFFER) не будет работать, если не гарантирована ложность условия full.
Подведем итоги: поставщики не могут выполнять свою работу без гарантии выполнения предусловий, а клиенты не способны обеспечить выполнение этих предусловий для сепаратных аргументов. Это можно назвать парадоксом параллельных предусловий.
|
Имеется аналогичный парадокс постусловий: при возврате из сепаратного вызова put нельзя быть уверенным, что для клиента выполнено условие not empty и другие постусловия. Эти свойства имеют место сразу после завершения подпрограммы, но другой клиент может их нарушить прежде, чем вызывающий клиент продолжит работу. Поскольку проблема является более серьезной для предусловий, определяющих корректную работу поставщиков, то они и будут рассматриваться. |
Эти парадоксы возникают только для сепаратных формальных аргументов. Если аргумент не сепаратный, например, является значением развернутого типа, то можно продолжать рассчитывать на обычные свойства утверждений. Но это слабое утешение.
Хотя это еще не до конца осознано в литературе, парадокс параллельных предусловий является одним из центральных пунктов в конструировании параллельного ОО-ПО, а безрезультативность попыток сохранения обычной семантики утверждений является одним из главных факторов, отличающих параллельные вычисления от их последовательных вариантов.
|
Парадокс предусловий может также возникнуть и в ситуациях, когда обычно не думают о параллельности, например при доступе к файлу. Это изучается в упражнении У12.6. |
