From eb44670c0654cfaf29b8a8c76f6cedd360c9cd5d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 28 Mar 2022 16:41:40 +0200
Subject: [PATCH] [ivette] reducing polling & response latency
---
ivette/src/frama-c/server.ts | 2 +-
src/plugins/server/server_socket.ml | 30 ++++++++++++++++-------------
2 files changed, 18 insertions(+), 14 deletions(-)
diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts
index 8906457a681..4c8fd9181ee 100644
--- a/ivette/src/frama-c/server.ts
+++ b/ivette/src/frama-c/server.ts
@@ -121,7 +121,7 @@ const pending = new Map<string, PendingRequest>();
let process: ChildProcess | undefined;
/** Polling timeout when server is busy. */
-const pollingTimeout = 200;
+const pollingTimeout = 10;
let pollingTimer: NodeJS.Timeout | undefined;
/** Killing timeout and timer for server process hard kill. */
diff --git a/src/plugins/server/server_socket.ml b/src/plugins/server/server_socket.ml
index ad9fd893d89..32c00fa522e 100644
--- a/src/plugins/server/server_socket.ml
+++ b/src/plugins/server/server_socket.ml
@@ -67,19 +67,23 @@ let feed_bytes { sock ; rcv ; brcv } =
let send_bytes { sock ; snd ; bsnd } =
try
- (* snd buffer is only used locally *)
- let n = Buffer.length bsnd in
- if n > 0 then
- let s = Bytes.length snd in
- let w = min n s in
- Buffer.blit bsnd 0 snd 0 w ;
- let r = Unix.single_write sock snd 0 w in
- if r > 0 then
- (* TODO[LC]: inefficient move. Requires a ring-buffer. *)
- let rest = Buffer.sub bsnd r (n-r) in
- Buffer.reset bsnd ;
- Buffer.add_string bsnd rest
- with Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> ()
+ while true do
+ (* snd buffer is only used locally *)
+ let n = Buffer.length bsnd in
+ if n > 0 then
+ let s = Bytes.length snd in
+ let w = min n s in
+ Buffer.blit bsnd 0 snd 0 w ;
+ let r = Unix.single_write sock snd 0 w in
+ if r > 0 then
+ (* TODO[LC]: inefficient move. Requires a ring-buffer. *)
+ let rest = Buffer.sub bsnd r (n-r) in
+ Buffer.reset bsnd ;
+ Buffer.add_string bsnd rest
+ else raise Exit
+ else raise Exit
+ done
+ with Exit | Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> ()
(* -------------------------------------------------------------------------- *)
(* --- Data Chunks Encoding --- *)
--
GitLab