Модуль 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. Программисту нужно знать, для каждой условной переменной c, какой мьютекс m является ассоциированным.

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

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

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

     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, мог оставаться приостановленным, даже если очередь непуста, это была бы проблемная ситуация, известная как тупик.