Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
121
Issues
121
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
b43ca104
Commit
b43ca104
authored
Apr 10, 2016
by
Johannes Kanig
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
implement setting of parallel option through server command
parent
d2d9a34f
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
56 additions
and
12 deletions
+56
-12
src/driver/prove_client.ml
src/driver/prove_client.ml
+6
-3
src/server/README.server
src/server/README.server
+23
-4
src/server/request.c
src/server/request.c
+24
-2
src/server/server-win.c
src/server/server-win.c
+3
-3
No files found.
src/driver/prove_client.ml
View file @
b43ca104
...
...
@@ -2,9 +2,6 @@ let standalone : bool ref = ref true
let
socket
:
Unix
.
file_descr
option
ref
=
ref
None
let
max_running_provers
:
int
ref
=
ref
1
let
set_max_running_provers
x
=
max_running_provers
:=
x
let
client_connect
socket_name
=
if
Sys
.
os_type
=
"Win32"
then
begin
let
name
=
"
\\\\
.
\\
pipe
\\
"
^
socket_name
in
...
...
@@ -90,9 +87,15 @@ let force_connect () =
connect
()
|
_
->
()
let
set_max_running_provers
x
=
max_running_provers
:=
x
;
if
!
socket
<>
None
then
send_request_string
(
"parallel;"
^
string_of_int
x
)
let
send_request
~
id
~
timelimit
~
memlimit
~
cmd
=
force_connect
()
;
let
buf
=
Buffer
.
create
128
in
Buffer
.
add_string
buf
"run;"
;
Buffer
.
add_string
buf
(
string_of_int
id
);
Buffer
.
add_char
buf
'
;
'
;
Buffer
.
add_string
buf
(
string_of_int
timelimit
);
...
...
src/server/README.server
View file @
b43ca104
...
...
@@ -17,10 +17,17 @@ Command line options
A client request is a single line which looks like this:
id;timeout;memlimit;cmd;arg1;arg2;...;argn
commandkind;payload
All items are separated by semicolons, and must not contain semicolons
themselves (but may contain spaces). Their meaning is the following:
Where commandkind is a simple string and payload is a semicolon-separated
list. There are currently only two possible commands. The first command looks
like this:
run;id;timeout;memlimit;cmd;arg1;arg2;...;argn
So the commandstring is "run". All items are separated by semicolons, and must
not contain semicolons themselves (but may contain spaces). Their meaning is
the following:
id - a (ideally) unique identifier which identifies the request
timeout - the allowed CPU time in seconds for this command;
this must be number, 0 for unlimited
...
...
@@ -29,7 +36,10 @@ themselves (but may contain spaces). Their meaning is the following:
cmd - the name of the executable to run
arg(i) - the commandline arguments of the command to run
A server answer looks like this:
The server does not acknowledge the receipt of this message. However, it will
run the executable with its arguments and time/memory limit. When the
executable has terminated, the server sends a message like this to the client
who sent the 'run' request:
id;exitcode;time;timeout;file
...
...
@@ -42,6 +52,15 @@ Their meaning is the following:
file - the path to a file which contains the stdout and stderr of the
executed program
The second commmand is like this:
parallel;num
So the commandstring is "parallel". 'num' is a number greater or equal to 1.
When this command is received, the server will allow to run up to 'num'
processes in parallel from now on. Later 'parallel' commands can increase or
decrease this number. There is no server answer to this command.
There are two separate implementations on linux and windows, but both are
very similar in structure and share some code (but should share much more).
They are both essentially a single-threaded event loop, where the possible
...
...
src/server/request.c
View file @
b43ca104
...
...
@@ -2,6 +2,7 @@
#include <stdlib.h>
#include <string.h>
#include "request.h"
#include "options.h"
//count the semicolons in <buf>, up to <len>
int
count_semicolons
(
char
*
buf
,
int
len
);
...
...
@@ -43,16 +44,37 @@ int copy_up_to_semicolon(char* buf, int begin, int len, char** result) {
}
prequest
parse_request
(
char
*
str_req
,
int
len
,
int
key
)
{
int
numargs
;
int
numargs
,
semic
,
parallel_arg
;
int
i
=
0
;
int
pos
=
0
;
prequest
req
;
char
*
tmp
;
numargs
=
count_semicolons
(
str_req
,
len
)
-
3
;
semic
=
count_semicolons
(
str_req
,
len
);
if
(
semic
==
0
)
{
return
NULL
;
}
// might be a 'parallel' command
if
(
semic
==
1
)
{
pos
=
copy_up_to_semicolon
(
str_req
,
pos
,
len
,
&
tmp
);
if
(
strncmp
(
tmp
,
"parallel"
,
pos
)
==
0
)
{
pos
=
copy_up_to_semicolon
(
str_req
,
pos
,
len
,
&
tmp
);
parallel_arg
=
atoi
(
tmp
);
if
(
parallel_arg
>=
1
)
{
parallel
=
parallel_arg
;
}
}
return
NULL
;
}
numargs
=
semic
-
4
;
if
(
numargs
<
0
)
{
return
NULL
;
}
pos
=
copy_up_to_semicolon
(
str_req
,
pos
,
len
,
&
tmp
);
if
(
strncmp
(
tmp
,
"run"
,
pos
)
!=
0
)
{
return
NULL
;
}
req
=
(
prequest
)
malloc
(
sizeof
(
request
));
req
->
key
=
key
;
req
->
numargs
=
numargs
;
...
...
src/server/server-win.c
View file @
b43ca104
...
...
@@ -443,7 +443,7 @@ void accept_client(int key) {
pclient
client
=
(
pclient
)
malloc
(
sizeof
(
t_client
));
client
->
handle
=
server_socket
->
handle
;
client
->
readbuf
=
init_readbuf
(
BUFSIZE
);
client
->
writebuf
=
init_writebuf
(
parallel
);
client
->
writebuf
=
init_writebuf
(
16
);
init_connect_data
(
&
(
client
->
read
),
READOP
);
init_connect_data
(
&
(
client
->
write
),
WRITEOP
);
free
(
server_socket
);
...
...
@@ -564,8 +564,8 @@ void init() {
strcat
(
socket_name
,
basename
);
queue
=
init_queue
(
100
);
clients
=
init_list
(
parallel
);
processes
=
init_list
(
parallel
);
clients
=
init_list
(
16
);
processes
=
init_list
(
16
);
init_logging
();
create_server_socket
();
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment