Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
6d8e3e59
Commit
6d8e3e59
authored
5 years ago
by
Loïc Correnson
Committed by
Michele Alberti
5 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[server] fix yielding and polling
parent
ed0bf472
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/server/main.ml
+43
-48
43 additions, 48 deletions
src/plugins/server/main.ml
with
43 additions
and
48 deletions
src/plugins/server/main.ml
+
43
−
48
View file @
6d8e3e59
...
...
@@ -77,7 +77,7 @@ type 'a message = {
(* Private API: *)
type
'
a
exec
=
{
type
'
a
process
=
{
id
:
'
a
;
request
:
string
;
data
:
json
;
...
...
@@ -91,11 +91,11 @@ type 'a server = {
pretty
:
Format
.
formatter
->
'
a
->
unit
;
equal
:
'
a
->
'
a
->
bool
;
fetch
:
unit
->
'
a
message
option
;
q_in
:
'
a
exec
Queue
.
t
;
q_in
:
'
a
process
Queue
.
t
;
q_out
:
'
a
response
Stack
.
t
;
mutable
daemon
:
Db
.
daemon
option
;
mutable
shutdown
:
bool
;
mutable
running
:
'
a
exec
option
;
mutable
running
:
'
a
process
option
;
}
exception
Killed
...
...
@@ -116,6 +116,9 @@ let pp_request pp fmt (r : _ request) =
else
Format
.
fprintf
fmt
"Request %s:%a"
request
pp
id
let
pp_process
pp
fmt
(
p
:
_
process
)
=
Format
.
fprintf
fmt
"Execute %s:%a"
p
.
request
pp
p
.
id
let
pp_response
pp
fmt
(
r
:
_
response
)
=
match
r
with
|
`Error
(
id
,
err
)
->
Format
.
fprintf
fmt
"Error %a: %s"
pp
id
err
...
...
@@ -132,35 +135,35 @@ let pp_response pp fmt (r : _ response) =
(* --- Request Handling --- *)
(* -------------------------------------------------------------------------- *)
let
execute
exe
c
:
_
response
=
let
run
pro
c
:
_
response
=
try
let
data
=
exe
c
.
handler
exe
c
.
data
in
`Data
(
exe
c
.
id
,
data
)
let
data
=
pro
c
.
handler
pro
c
.
data
in
`Data
(
pro
c
.
id
,
data
)
with
|
Killed
->
`Killed
exe
c
.
id
|
Data
.
InputError
msg
->
`Error
(
exe
c
.
id
,
msg
)
|
Killed
->
`Killed
pro
c
.
id
|
Data
.
InputError
msg
->
`Error
(
pro
c
.
id
,
msg
)
|
Sys
.
Break
as
exn
->
raise
exn
(* Silently pass the exception *)
|
exn
when
Cmdline
.
catch_at_toplevel
exn
->
Senv
.
warning
"[%s] Uncaught exception:@
\n
%s"
exec
.
request
(
Cmdline
.
protect
exn
)
;
`Error
(
exec
.
id
,
Printexc
.
to_string
exn
)
proc
.
request
(
Cmdline
.
protect
exn
)
;
`Error
(
proc
.
id
,
Printexc
.
to_string
exn
)
let
delayed
process
=
if
Senv
.
debug_atleast
1
then
Some
(
fun
d
->
Senv
.
debug
"No yield since %dms during %s"
d
process
)
else
None
let
execute_debug
server
yield
exec
=
Senv
.
debug
"Trigger %s:%a"
exec
.
request
server
.
pretty
exec
.
id
;
Db
.
with_progress
~
debounced
:
server
.
polling
?
on_delayed
:
(
delayed
exec
.
request
)
yield
execute
exec
let
reply_debug
server
resp
=
if
Senv
.
debug_atleast
1
then
Senv
.
debug
"%a"
(
pp_response
server
.
pretty
)
resp
;
let
execute
server
?
yield
proc
=
Senv
.
debug
"%a"
(
pp_process
server
.
pretty
)
proc
;
let
resp
=
match
yield
with
|
Some
yield
when
proc
.
yield
->
Db
.
with_progress
~
debounced
:
server
.
polling
?
on_delayed
:
(
delayed
proc
.
request
)
yield
run
proc
|
_
->
run
proc
in
Senv
.
debug
"%a"
(
pp_response
server
.
pretty
)
resp
;
Stack
.
push
resp
server
.
q_out
(* -------------------------------------------------------------------------- *)
...
...
@@ -185,26 +188,28 @@ let process_request (server : 'a server) (request : 'a request) : unit =
end
|
`Kill
id
->
begin
let
kill
=
kill_request
server
.
equal
id
in
Queue
.
iter
kill
server
.
q_in
;
option
kill
server
.
running
;
let
set_
kill
ed
=
kill_request
server
.
equal
id
in
Queue
.
iter
set_
kill
ed
server
.
q_in
;
option
set_
kill
ed
server
.
running
;
end
|
`Request
(
id
,
request
,
data
)
->
begin
match
find
request
with
|
None
->
reply_debug
server
(
`Rejected
id
)
|
None
->
Senv
.
debug
"Rejected %a"
server
.
pretty
id
;
Stack
.
push
(
`Rejected
id
)
server
.
q_out
|
Some
(
`GET
,
handler
)
->
let
exe
c
=
{
id
;
request
;
handler
;
data
;
let
pro
c
=
{
id
;
request
;
handler
;
data
;
yield
=
false
;
killed
=
false
}
in
reply_debug
server
(
execute
exec
)
execute
server
proc
;
|
Some
(
`SET
,
handler
)
->
let
exe
c
=
{
id
;
request
;
handler
;
data
;
let
pro
c
=
{
id
;
request
;
handler
;
data
;
yield
=
false
;
killed
=
false
}
in
Queue
.
push
exe
c
server
.
q_in
Queue
.
push
pro
c
server
.
q_in
|
Some
(
`EXEC
,
handler
)
->
let
exe
c
=
{
id
;
request
;
handler
;
data
;
let
pro
c
=
{
id
;
request
;
handler
;
data
;
yield
=
true
;
killed
=
false
}
in
Queue
.
push
exe
c
server
.
q_in
Queue
.
push
pro
c
server
.
q_in
end
(* -------------------------------------------------------------------------- *)
...
...
@@ -238,19 +243,14 @@ let do_yield server () =
(* --- One Step Process --- *)
(* -------------------------------------------------------------------------- *)
let
rec
fetch_exec
q
=
if
Queue
.
is_empty
q
then
None
else
let
e
=
Queue
.
pop
q
in
if
e
.
killed
then
fetch_exec
q
else
Some
e
let
process
server
=
match
fetch_exec
server
.
q_in
with
|
None
->
communicate
server
|
Some
exec
->
server
.
running
<-
Some
exec
;
if
Queue
.
is_empty
server
.
q_in
then
communicate
server
else
let
proc
=
Queue
.
pop
server
.
q_in
in
server
.
running
<-
Some
proc
;
try
reply_debug
server
(
execute
_debug
server
(
do_yield
server
)
exec
)
;
execute
server
~
yield
:
(
do_yield
server
)
proc
;
server
.
running
<-
None
;
true
with
exn
->
...
...
@@ -332,14 +332,9 @@ let run server =
foreground
server
;
signal
true
;
begin
try
let
idle
=
float_of_int
server
.
polling
/.
1000
.
0
in
while
not
server
.
shutdown
do
let
activity
=
process
server
in
if
not
activity
then
begin
Unix
.
sleepf
idle
;
Db
.
yield
()
;
end
if
not
activity
then
Db
.
sleep
server
.
polling
done
;
with
Sys
.
Break
->
()
(* Ctr+C, just leave the loop normally *)
end
;
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment