模組 Condition

條件變數。

當多個執行緒想要存取受互斥鎖（一種互斥鎖定）保護的共享資料結構時，條件變數非常有用。

條件變數是一個溝通管道。在接收端，一個或多個執行緒可以表明它們希望等待某個屬性變為真。在傳送端，一個執行緒可以發出信號表示此屬性已變為真，從而喚醒一個（或多個）等待中的執行緒。

例如，在佇列資料結構的實作中，如果一個希望取出元素的執行緒發現佇列目前為空，則此執行緒會等待佇列變為非空。一個將元素插入佇列的執行緒會發出信號表示佇列已變為非空。條件變數用於此目的。此溝通管道傳達「佇列為非空」的屬性為真，或者更準確地說，可能為真的資訊。（我們將在下面解釋為什麼信號的接收者不能確定該屬性成立。）

繼續佇列的範例，假設佇列具有固定的最大容量，則希望插入元素的執行緒可能會發現佇列已滿。然後，此執行緒必須等待佇列變為非滿，而取出佇列元素的執行緒會發出信號表示佇列已變為非滿。另一個條件變數用於此目的。

簡而言之，條件變數 c 用於傳達關於由互斥鎖 m 保護的共享資料結構 D 的某個屬性 P 可能為真的資訊。

條件變數為忙碌等待提供了一種有效率的替代方案。當希望等待屬性 P 為真時，可以使用 Condition.wait 在迴圈主體中，而不是編寫忙碌等待迴圈：

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

如下所示：

     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 操作的執行緒即使佇列為非空也可以保持暫停，那將是一個有問題的情況，稱為死鎖。