Commit 07b60cd3 authored by Johannes Kanig's avatar Johannes Kanig Committed by Sylvain Dailler

R531-011 implement killing of tasks

The why3server supports the "interrupt" command which removes a task.
But until now, the server didn't actually kill any already running
processes. This is now implemented.

Background is that I plan some refactorings which may make use of the
"interrupt" command, so I want it to work properly.

This new code is untested on windows, because no client code actually
uses the interrupt command in SPARK. But I tested that it doesn't cause
regressions. It will be later tested by the new code I intend to write.

*server-unix.c
*server-win.c
(overall): outsource some little code to new proc unit
(handle_msg): actually kill processes

* proc.c - new file
(os_kill): new platform-dependent function to kill a process by pid
(init_process_list): new function to init the process list
(kill_processes): new function to kill processes from process list with
  a certain key
(free_process): release memory held by a process record

Change-Id: I7238578061c65883423f8ec538d79d9de3fb717b
(cherry picked from commit b17873a181ff56abda9d09bc8d10c29ba036c019)
parent 33810098
......@@ -603,7 +603,7 @@ clean::
##############
SERVER_MODULES := logging arraylist options queue readbuf request \
writebuf server-unix server-win
proc writebuf server-unix server-win
CPULIM_MODULES := cpulimit-unix cpulimit-win
......
#include <signal.h>
#include <stdlib.h>
#include <string.h>
#include "proc.h"
#include "options.h"
// global pointers are initialized with NULL by C semantics
plist processes;
// kill process using os specific routine
void os_kill(pproc p);
void os_kill(pproc p) {
#ifdef _WIN32
// arbitrarily chosen exit code
TerminateProcess(p->handle, ERROR_REQUEST_ABORTED);
#else
kill(p->id, SIGKILL);
#endif
}
void init_process_list () {
processes = init_list(parallel);
}
void kill_processes(char *id) {
for (int i = 0; i < processes->len; i++) {
if (!strcmp(((pproc)(processes->data[i]))->task_id, id)) {
os_kill((pproc)processes->data[i]);
}
}
}
void free_process(pproc proc) {
#ifdef _WIN32
CloseHandle(proc->handle);
CloseHandle(proc->job);
#endif
free(proc->outfile);
free(proc->task_id);
free(proc);
}
#ifndef PROC_H
#define PROC_H
#ifdef _WIN32
#include <windows.h>
#else
#include <sys/types.h>
#endif
#include "arraylist.h"
typedef struct {
#ifdef _WIN32
HANDLE handle;
HANDLE job;
#else
pid_t id;
#endif
int client_key;
char* task_id;
char* outfile;
} t_proc, *pproc;
extern plist processes;
// free memory and resources associated with the process p
void free_process(pproc p);
// kill all processes whose task_id is equal to id
void kill_processes(char *id);
// initialize global list of processes
void init_process_list();
#endif
......@@ -27,7 +27,6 @@
#include <poll.h>
#include <stddef.h>
#include <stdlib.h>
#include <string.h>
#include <signal.h>
#include <sys/time.h>
#include <sys/wait.h>
......@@ -41,6 +40,7 @@
#include "writebuf.h"
#include "options.h"
#include "logging.h"
#include "proc.h"
#define READ_ONCE 1024
......@@ -53,13 +53,6 @@ typedef struct {
int server_sock = -1;
typedef struct {
pid_t id;
int client_fd;
char* task_id;
char* outfile;
} t_proc, *pproc;
// the poll list is the list of file descriptors for which we monitor certain
// events.
struct pollfd* poll_list;
......@@ -67,7 +60,6 @@ int poll_num = 0;
int poll_len = 0;
// global pointers are initialized with NULL by C semantics
plist processes;
plist clients;
char *current_dir;
......@@ -269,7 +261,7 @@ void server_init_listening(char* socketname, int parallel) {
free(socketname_copy1);
free(socketname_copy2);
add_to_poll_list(server_sock, POLLIN);
processes = init_list(parallel);
init_process_list();
setup_child_pipe();
}
......@@ -421,12 +413,6 @@ void send_msg_to_client(pclient client,
queue_write(client, msgbuf);
}
void free_process(pproc proc) {
free(proc->outfile);
free(proc->task_id);
free(proc);
}
void handle_child_events() {
pproc child;
pclient client;
......@@ -455,7 +441,7 @@ void handle_child_events() {
}
child = (pproc) list_lookup(processes, pid);
list_remove(processes, pid);
client = (pclient) list_lookup(clients, child->client_fd);
client = (pclient) list_lookup(clients, child->client_key);
if (client != NULL) {
send_msg_to_client(client,
child->task_id,
......@@ -494,7 +480,7 @@ void run_request (prequest r) {
proc = (pproc) malloc(sizeof(t_proc));
proc->task_id = r->id;
proc->client_fd = r->key;
proc->client_key = r->key;
proc->id = id;
proc->outfile = outfile;
list_append(processes, id, (void*) proc);
......@@ -532,8 +518,7 @@ void handle_msg(pclient client, int key) {
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
remove_from_queue(r->id);
// kill all processes whose id is r->id;
// TODO kill_processes(processes, r->id);
kill_processes(r->id);
free_request(r);
break;
}
......
......@@ -32,6 +32,7 @@
#include "writebuf.h"
#include "arraylist.h"
#include "logging.h"
#include "proc.h"
#define READ_ONCE 1024
#define BUFSIZE 4096
......@@ -62,14 +63,6 @@ typedef struct {
pwritebuf writebuf;
} t_client, *pclient;
typedef struct {
HANDLE handle;
HANDLE job;
int client_key;
char* id;
char* outfile;
} t_proc, *pproc;
// AFAIU, there is no connection queue or something like that, so we need to
// create several socket instances to be able to process several clients that
// would connect almost at the same time. The two variables below will be
......@@ -79,7 +72,6 @@ pserver* server_socket;
int* server_key;
plist clients;
plist processes;
char current_dir[MAX_PATH];
int gen_key = 1;
......@@ -109,7 +101,6 @@ HANDLE completion_port;
void shutdown_with_msg(char* msg);
void shutdown_with_msg(char* msg) {
pproc proc;
if (completion_port != NULL) {
CloseHandle (completion_port);
}
......@@ -125,9 +116,7 @@ void shutdown_with_msg(char* msg) {
}
if (processes != NULL) {
for (int i = 0; i < list_length(processes); i++) {
proc = processes->data[i];
CloseHandle(proc->handle);
CloseHandle(proc->job);
free_process(processes->data[i]);
}
}
logging_shutdown(msg);
......@@ -430,7 +419,7 @@ void run_request (prequest r) {
proc = (pproc) malloc(sizeof(t_proc));
proc->handle = pi.hProcess;
proc->job = ghJob;
proc->id = r->id;
proc->task_id = r->id;
proc->client_key = r->key;
proc->outfile = outfile;
key = keygen();
......@@ -469,7 +458,10 @@ void handle_msg(pclient client, int key) {
break;
case REQ_INTERRUPT:
remove_from_queue(r->id);
// TODO: remove r from the queue if still there, or kill the process r->id;
kill_processes(r->id);
// no need to clean up the list of processes and free the memory for
// processes, this will be done when we get notified of the end of the
// child process
free_request(r);
break;
}
......@@ -502,14 +494,6 @@ void accept_client(int key, int socket_num) {
do_read(client);
}
void free_process(pproc proc) {
CloseHandle(proc->handle);
CloseHandle(proc->job);
free(proc->id);
free(proc->outfile);
free(proc);
}
void send_started_msg_to_client(pclient client,
char* id) {
char* msgbuf;
......@@ -621,7 +605,7 @@ void handle_child_event(pproc child, pclient client, int proc_key, DWORD event)
timeout = (exitcode == ERROR_NOT_ENOUGH_QUOTA) ||
(exitcode == STATUS_QUOTA_EXCEEDED);
send_msg_to_client(client,
child->id,
child->task_id,
exitcode,
cpu_time,
timeout,
......@@ -648,7 +632,7 @@ void init() {
init_request_queue();
clients = init_list(parallel);
processes = init_list(parallel);
init_process_list();
server_socket = (pserver*) malloc(parallel * sizeof(pserver));
server_key = (int*) malloc(parallel * sizeof(int));
......
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