aboutsummaryrefslogtreecommitdiff
path: root/lib/tQueue.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-04-25 19:46:30 +0200
committerPierre-Marie Pédrot2014-04-25 21:17:11 +0200
commit8330f5cfd6a332df10fc806b0c0bdab6e0abe8e7 (patch)
tree56ab646154a576454a1ee34ad1cc0a8c6e7a70fe /lib/tQueue.ml
parent9e36fa1e7460d256a4f9f37571764f79050688e2 (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.ml64
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