summaryrefslogtreecommitdiff
path: root/lib/cThread.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /lib/cThread.ml
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'lib/cThread.ml')
-rw-r--r--lib/cThread.ml41
1 files changed, 35 insertions, 6 deletions
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 55bb6fd6..2d1f10bf 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -22,7 +22,7 @@ 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|Unix.EINTR),_,_) ->
- while not (safe_wait_timed_read fd 1.0) do Thread.yield () done;
+ while not (safe_wait_timed_read fd 0.05) do Thread.yield () done;
loop ()
in
loop ()
@@ -43,6 +43,18 @@ let really_read_fd fd s off len =
i := !i + r
done
+let really_read_fd_2_oc fd oc len =
+ let i = ref 0 in
+ let size = 4096 in
+ let s = String.create size in
+ while !i < len do
+ let len = len - !i in
+ let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in
+ if r = 0 then raise End_of_file;
+ i := !i + r;
+ output oc s 0 r;
+ done
+
let thread_friendly_really_read ic s ~off ~len =
try
let fd = Unix.descr_of_in_channel ic in
@@ -68,9 +80,26 @@ let thread_friendly_input_value ic =
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
+ let desired_size = body_size + Marshal.header_size in
+ if desired_size <= Sys.max_string_length then begin
+ let msg = String.create desired_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
+ end else begin
+ (* Workaround for 32 bit systems and data > 16M *)
+ let name, oc =
+ Filename.open_temp_file ~mode:[Open_binary] "coq" "marshal" in
+ try
+ output oc header 0 Marshal.header_size;
+ really_read_fd_2_oc fd oc body_size;
+ close_out oc;
+ let ic = open_in_bin name in
+ let data = Marshal.from_channel ic in
+ close_in ic;
+ Sys.remove name;
+ data
+ with e -> Sys.remove name; raise e
+ end
+ with Unix.Unix_error _ | Sys_error _ -> raise End_of_file