diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-25 19:46:30 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-25 21:17:11 +0200 |
commit | 8330f5cfd6a332df10fc806b0c0bdab6e0abe8e7 (patch) | |
tree | 56ab646154a576454a1ee34ad1cc0a8c6e7a70fe /stm/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 'stm/tQueue.ml')
-rw-r--r-- | stm/tQueue.ml | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/stm/tQueue.ml b/stm/tQueue.ml new file mode 100644 index 000000000..783c545fd --- /dev/null +++ b/stm/tQueue.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* 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 |