Модуль Condition

Условные переменные.

Условные переменные полезны, когда несколько потоков хотят получить доступ к общей структуре данных, защищенной мьютексом (блокировкой взаимного исключения).

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

Например, при реализации структуры данных «очередь», если поток, желающий извлечь элемент, обнаруживает, что очередь пуста, он ожидает, пока очередь не станет непустой. Поток, добавляющий элемент в очередь, подает сигнал о том, что очередь стала непустой. Для этого используется условная переменная. Этот канал связи передает информацию о том, что свойство «очередь непуста» истинно или, точнее, может быть истинным. (Ниже объясняется, почему получатель сигнала не может быть уверен, что это свойство выполняется.)

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

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

Условные переменные представляют собой эффективную альтернативу активному ожиданию. Когда требуется дождаться, пока свойство P станет истинным, вместо написания цикла активного ожидания:

     Mutex.lock m;
     while not P do
       Mutex.unlock m; Mutex.lock m
     done;
     <update the data structure>;
     Mutex.unlock m
   

в теле цикла используют Condition.wait, как показано ниже:

     Mutex.lock m;
     while not P do
       Condition.wait c m
     done;
     <update the data structure>;
     Mutex.unlock m
   

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

С условной переменной c связан ровно один мьютекс m. Эта связь неявная: мьютекс m не передается явно в качестве аргумента функции Condition.create. Программист должен знать, какой мьютекс m связан с каждой условной переменной c.

С одним мьютексом m могут быть связаны несколько условных переменных. В примере с ограниченной очередью одна условная переменная используется для обозначения того, что очередь непуста, а другая — для обозначения того, что очередь заполнена не полностью.

С условной переменной c следует связывать ровно одно логическое свойство P. Примеры таких свойств: «очередь непуста» и «очередь заполнена не полностью». Программист должен отслеживать соответствующее свойство P для каждой условной переменной. Сигнал по условной переменной c отправляется, чтобы указать, что свойство P истинно или может быть истинным. Однако поток, разбуженный на стороне получателя, не может предполагать, что P истинно; после завершения вызова Condition.wait необходимо явно проверить, истинно ли P. Этому есть несколько причин. Одна из них заключается в том, что в промежутке между отправкой сигнала и его получением ожидающим потоком, после чего этот поток получает процессорное время, другой поток может получить мьютекс m и изменить структуру данных D, сделав свойство P ложным. Другая причина — возможность ложных пробуждений: ожидающий поток может быть разбужен, даже если сигнал не отправлялся.

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

     type 'a safe_queue =
       { queue : 'a Queue.t; mutex : Mutex.t; nonempty : Condition.t }

     let create () =
       { queue = Queue.create(); mutex = Mutex.create();
         nonempty = Condition.create() }

     let add v q =
       Mutex.lock q.mutex;
       let was_empty = Queue.is_empty q.queue in
       Queue.add v q.queue;
       if was_empty then Condition.broadcast q.nonempty;
       Mutex.unlock q.mutex

     let take q =
       Mutex.lock q.mutex;
       while Queue.is_empty q.queue do Condition.wait q.nonempty q.mutex done;
       let v = Queue.take q.queue in (* cannot fail since queue is nonempty *)
       Mutex.unlock q.mutex;
       v
   

Поскольку вызов Condition.broadcast выполняется внутри критической секции, при каждом снятии блокировки с мьютекса выполняется следующее свойство: если очередь непуста, то ни один поток не ожидает, или, другими словами, если какой-либо поток ожидает, то очередь должна быть пуста. Это желательное свойство: если поток, пытающийся выполнить операцию take, может оставаться приостановленным, несмотря на то что очередь непуста, это приведет к проблемной ситуации, известной как взаимная блокировка.