diff options
| -rw-r--r-- | lib/cThread.ml | 48 | ||||
| -rw-r--r-- | lib/cThread.mli | 21 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | lib/spawned.ml | 22 | ||||
| -rw-r--r-- | lib/spawned.mli | 4 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 6 |
6 files changed, 73 insertions, 29 deletions
diff --git a/lib/cThread.ml b/lib/cThread.ml new file mode 100644 index 000000000..a38c88d80 --- /dev/null +++ b/lib/cThread.ml @@ -0,0 +1,48 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +let prepare_in_channel_for_thread_friendly_io ic = + Unix.set_nonblock (Unix.descr_of_in_channel ic) + +let thread_friendly_read_fd fd s ~off ~len = + let rec loop () = + try Unix.read fd s off len + with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN),_,_) -> + while not (Thread.wait_timed_read fd 1.0) do Thread.yield () done; + loop () + in + loop () + +let thread_friendly_read ic s ~off ~len = + try + let fd = Unix.descr_of_in_channel ic in + thread_friendly_read_fd fd s ~off ~len + with Unix.Unix_error _ -> 0 + +let really_read_fd fd s off len = + let i = ref 0 in + while !i < len do + let off = off + !i in + let len = len - !i in + let r = thread_friendly_read_fd fd s ~off ~len in + if r = 0 then raise End_of_file; + i := !i + r + done + +let thread_friendly_input_value ic = + try + let fd = Unix.descr_of_in_channel ic in + let header = String.create Marshal.header_size in + really_read_fd fd header 0 Marshal.header_size; + let body_size = Marshal.data_size header 0 in + let msg = String.create (body_size + Marshal.header_size) in + String.blit header 0 msg 0 Marshal.header_size; + really_read_fd fd msg Marshal.header_size body_size; + Marshal.from_string msg 0 + with Unix.Unix_error _ -> raise End_of_file + diff --git a/lib/cThread.mli b/lib/cThread.mli new file mode 100644 index 000000000..6c635748e --- /dev/null +++ b/lib/cThread.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* As of OCaml 4.01.0 input_value and input do not quite work well + * with threads. The symptom is the following. Two threads, each + * of them blocked on a read (on different channels). One is not + * woken up even if data is available. When the other one gets data + * then the stuck one is eventually unblocked too. Unix.select with + * an unbounded wait has the same problem. *) + +(* Use only the following functions on the channel *) +val prepare_in_channel_for_thread_friendly_io : in_channel -> unit +val thread_friendly_input_value : in_channel -> 'a +val thread_friendly_read : + in_channel -> string -> off:int -> len:int -> int + diff --git a/lib/lib.mllib b/lib/lib.mllib index be15eca60..9ba1e15b9 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -8,6 +8,7 @@ Segmenttree Unicodetable Unicode System +CThread Spawn Spawned Trie diff --git a/lib/spawned.ml b/lib/spawned.ml index 29cf51769..9c304435b 100644 --- a/lib/spawned.ml +++ b/lib/spawned.ml @@ -83,25 +83,3 @@ let get_channels () = | None -> Errors.anomaly(Pp.str "init_channels not called") | Some(ic, oc) -> ic, oc -let prepare_in_channel_for_thread_friendly_blocking_input ic = - if Sys.os_type = "Win32" then Unix.set_nonblock (Unix.descr_of_in_channel ic) - else () - -let thread_friendly_blocking_input ic = - if Sys.os_type = "Win32" then - let open Unix in - let open Thread in - let fd = descr_of_in_channel ic in - let rec loop buf n = - try read fd buf 0 n - with - | Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN),_,_) -> - (* We wait for some data explicitly yielding each second *) - while not (wait_timed_read fd 1.0) do yield () done; - loop buf n - | Unix.Unix_error _ -> 0 - in - loop - else - (fun buf n -> Pervasives.input ic buf 0 n) - diff --git a/lib/spawned.mli b/lib/spawned.mli index bc5649a2f..18b88dc64 100644 --- a/lib/spawned.mli +++ b/lib/spawned.mli @@ -20,7 +20,3 @@ val init_channels : unit -> unit (* Once initialized, these are the channels to talk with our master *) val get_channels : unit -> in_channel * out_channel -(* In multi threaded environments on windows blocking calls do - prevent context switch. This seems a huge BUG, here a work around *) -val prepare_in_channel_for_thread_friendly_blocking_input : in_channel -> unit -val thread_friendly_blocking_input : in_channel -> string -> int -> int diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index e93d16720..af58f8eb2 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -397,9 +397,9 @@ let loop () = catch_break := false; let in_ch, out_ch = Spawned.get_channels () in let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in - Spawned.prepare_in_channel_for_thread_friendly_blocking_input in_ch; - let in_lb = - Lexing.from_function (Spawned.thread_friendly_blocking_input in_ch) in + CThread.prepare_in_channel_for_thread_friendly_io in_ch; + let in_lb = Lexing.from_function (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in set_logger (slave_logger xml_oc); |