Commit 28cd7354 authored by MARCHE Claude's avatar MARCHE Claude

VC server: adding a request to interrupt processes, in progress

parent 964d077e
This is a VC server for Why3. It implements the following functionalities:
* wait for connections on a unix domain socket (unix) or named pipe
(windows) for clients
* clients can send requests for a process to spawn, including
timeout/memory limit
* server will send back a filename containing the output of the process,
as well as the time taken and the exit code
timeout/memory limit. To process is not spawned immediately but put
in a queue od processes to be spawned. Process are spawned in
parallel up to some maximal number.
* when a process is spawned, server sends a message to the client of the form 'S;id' to inform it that process 'id' has started.
* when the process is terminated, either normally or by a ressource
limit reached, server sends back a detailed message containing the
output of the process, as well as the time taken and the exit code
* clients can also request to change the maximal number of process
that can run in parallel
* clients can also request to interrupt a process, killing it if it
already runs
Command line options
====================
......@@ -20,8 +35,11 @@ A client request is a single line which looks like this:
commandkind;payload
Where commandkind is a simple string and payload is a semicolon-separated
list. There are currently three possible commands. The first command looks
like this:
list. There are currently four possible commands.
1 Running a process
The first command looks like this:
run;id;timeout;memlimit;cmd;arg1;arg2;...;argn
......@@ -59,6 +77,8 @@ Their meaning is the following:
file - the path to a file which contains the stdout and stderr of the
executed program
2 Running a process on sdtin
The second command is very similar:
runstdin;id;timeout;memlimit;cmd;arg1;arg2;...;argn;filename
......@@ -68,6 +88,8 @@ difference that an extra filename is given as the last argument to the
command. This filename is not passed to the command as a commandline argument,
instead it is "piped" into the stdin of the command.
3 Changing the maximal number of processes run in parallel
The third commmand is like this:
parallel;num
......@@ -77,6 +99,14 @@ 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.
4 Interrupt a process
interrupt;id
will stop the process of the given id, killing it if it was already running
== notes ==
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
......
......@@ -24,7 +24,7 @@ typedef struct {
int capacity; // the capacity of the arrays key and data
} t_list, *plist;
// The idea is that each element in the list is a tuple (key, data), but it is
// simpler to hahve two separate arrays for that
// simpler to have two separate arrays for that
// return a list of initial capacity <capacity>
plist init_list(int capacity);
......
......@@ -70,8 +70,8 @@ prequest parse_request(char* str_req, int len, int key) {
if (semic == 0) {
return NULL;
}
// might be a 'parallel' command
if (semic == 1) {
// might be a 'parallel' or a 'interrupt' command
pos = copy_up_to_semicolon (str_req, pos, len, &tmp);
if (strncmp(tmp, "parallel", pos) == 0) {
free(tmp);
......@@ -81,6 +81,14 @@ prequest parse_request(char* str_req, int len, int key) {
parallel = parallel_arg;
}
}
if (strncmp(tmp, "interrupt", pos) == 0) {
free(tmp);
req = (prequest) malloc(sizeof(request));
req->key = key;
req->req_type = REQ_INTERRUPT;
pos = copy_up_to_semicolon(str_req, pos, len, &(req->id));
return req;
}
free(tmp);
return NULL;
}
......@@ -101,6 +109,7 @@ prequest parse_request(char* str_req, int len, int key) {
free(tmp);
req = (prequest) malloc(sizeof(request));
req->key = key;
req->req_type = REQ_RUN;
req->numargs = numargs;
req->usestdin = runstdin;
pos = copy_up_to_semicolon(str_req, pos, len, &(req->id));
......
......@@ -14,8 +14,11 @@
#include <stdbool.h>
typedef enum { REQ_RUN, REQ_INTERRUPT } request_type;
typedef struct {
int key;
request_type req_type;
char* id;
int timeout;
int memlimit;
......
......@@ -436,6 +436,8 @@ void handle_child_events() {
}
}
/*@ requires r != NULL && r->req_type == REQ_RUN;
@*/
void run_request (prequest r) {
char* outfile;
int out_descr;
......@@ -467,6 +469,20 @@ void run_request (prequest r) {
send_started_msg_to_client(client, r->id);
}
void remove_from_queue(pqueue p, char *id) {
// inefficient, but what else?
pqueue tmp = init_queue(p->capacity);
while (!queue_is_empty(p)) {
prequest r = queue_pop(p);
if (strcmp(r->id,id)) queue_push(tmp, r);
}
while (!queue_is_empty(tmp)) {
prequest r = queue_pop(tmp);
queue_push(p, r);
}
free_queue(tmp);
}
void handle_msg(pclient client, int key) {
prequest r;
char* buf;
......@@ -486,11 +502,22 @@ void handle_msg(pclient client, int key) {
break;
r = parse_request(buf + old, cur - old, key);
if (r) {
if (list_length(processes) < parallel) {
run_request(r);
switch (r->req_type) {
case REQ_RUN:
if (list_length(processes) < parallel) {
run_request(r);
free_request(r);
} else {
queue_push(queue, (void*) r);
}
break;
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
remove_from_queue(queue, r->id);
// kill all processes whose id is r->id;
// TODO kill_processes(processes, r->id);
free_request(r);
} else {
queue_push(queue, (void*) r);
break;
}
}
//skip newline
......
......@@ -451,11 +451,19 @@ void handle_msg(pclient client, int key) {
//the read buffer also contains the newline, skip it
r = parse_request(client->readbuf->data, client->readbuf->len - 1, key);
if (r) {
if (list_length(processes) < parallel) {
run_request(r);
free_request(r);
} else {
switch (r->req_type) {
case REQ_RUN:
if (list_length(processes) < parallel) {
run_request(r);
free_request(r);
} else {
queue_push(queue, (void*) r);
}
break;
case REQ_INTERRUPT:
// TODO: remove r from the queue if still there, or kill the process r->id;
free_request(r);
break;
}
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment