diff options
| author | Pierre-Marie Pédrot | 2014-04-25 19:46:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 21:17:11 +0200 |
| commit | 8330f5cfd6a332df10fc806b0c0bdab6e0abe8e7 (patch) | |
| tree | 56ab646154a576454a1ee34ad1cc0a8c6e7a70fe /lib/tQueue.ml | |
| parent | 9e36fa1e7460d256a4f9f37571764f79050688e2 (diff) | |
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.
Diffstat (limited to 'lib/tQueue.ml')
| -rw-r--r-- | lib/tQueue.ml | 64 |
1 files changed, 0 insertions, 64 deletions
diff --git a/lib/tQueue.ml b/lib/tQueue.ml deleted file mode 100644 index 783c545fd0..0000000000 --- a/lib/tQueue.ml +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -type 'a t = { - queue: 'a Queue.t; - lock : Mutex.t; - cond : Condition.t; - mutable nwaiting : int; - cond_waiting : Condition.t; -} - -let create () = { - queue = Queue.create (); - lock = Mutex.create (); - cond = Condition.create (); - nwaiting = 0; - cond_waiting = Condition.create (); -} - -let pop ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) = - Mutex.lock m; - while Queue.is_empty q do - tq.nwaiting <- tq.nwaiting + 1; - Condition.signal cn; - Condition.wait c m; - tq.nwaiting <- tq.nwaiting - 1; - done; - let x = Queue.pop q in - Condition.signal c; - Condition.signal cn; - Mutex.unlock m; - x - -let push { queue = q; lock = m; cond = c } x = - Mutex.lock m; - Queue.push x q; - Condition.signal c; - Mutex.unlock m - -let wait_until_n_are_waiting_and_queue_empty j tq = - Mutex.lock tq.lock; - while not (Queue.is_empty tq.queue) || tq.nwaiting < j do - Condition.wait tq.cond_waiting tq.lock - done; - Mutex.unlock tq.lock - -let dump { queue; lock } = - let l = ref [] in - Mutex.lock lock; - while not (Queue.is_empty queue) do l := Queue.pop queue :: !l done; - Mutex.unlock lock; - List.rev !l - -let reorder tq rel = - Mutex.lock tq.lock; - let l = ref [] in - while not (Queue.is_empty tq.queue) do l := Queue.pop tq.queue :: !l done; - List.iter (fun x -> Queue.push x tq.queue) (List.sort rel !l); - Mutex.unlock tq.lock |
