Commit 95c207d1 authored by Johannes Kanig's avatar Johannes Kanig Committed by Sylvain Dailler
Browse files

P613-010 fix crashes of gnatwhy3 connecting to why3server

On windows, when the why3server has accepted a client on the server
socket, it continues to use that socket for the client communication. A
new socket is created so that new clients can connect. However, there
may be a little time between accepting the client and creating the new
socket, where the connection of another client will be refused. This
resulted in crashes.

We now simply prepare more than one server socket, so that several
clients can connect at the same time. More precisely, we create as many
sockets as gnatwhy3 processes will be run in parallel.

Concretely, we replace the previous server_socket and server_key
variables by arrays, whose length is determined by the "parallel"
option. The code which manipulated these variables needs to be adapted
to know which of the sockets to manipulate.

* server-win.c
(shutdown_with_msg): close all handles
(create_server_socket): new integer argument which specifies the cell to
   store the new server socket in
(accept_client): new integer argument which specifies on which of the
   server sockets the connection was accepted. Used to create a new
   socket in that cell using create_server_socket.
(init): create an array of sockets instead of just one
(get_server_num): new function to determine the socket which got the
  new client
(main): use get_server_num to know if it was a server socket that had an
   event, and which one. Call accept_client with the result.

Change-Id: I5f7ff1b30c9340d897b75085ade61b2d79f87167
(cherry picked from commit f2cbded5da7a3fcbebb61ee98b8e6c8d9c1d2227)
parent 3081b1a9
......@@ -39,6 +39,7 @@
#define READOP 0
#define WRITEOP 1
// constants to distinguish between events from sockets and processes
#define SOCKET 0
#define PROCESS 1
......@@ -69,10 +70,16 @@ typedef struct {
char* outfile;
} t_proc, *pproc;
pserver server_socket = NULL;
int server_key = 0;
plist clients = NULL;
plist processes = NULL;
// 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
// allocated to arrays of equal length, holding the socket handle and the
// "key" (used for IO Completion Port) for each socket instance.
pserver* server_socket;
int* server_key;
plist clients;
plist processes;
char current_dir[MAX_PATH];
int gen_key = 1;
......@@ -95,9 +102,9 @@ int key_of_ms_key(ULONG_PTR ms) {
void init();
char* socket_name = NULL;
char* socket_name;
HANDLE completion_port = NULL;
HANDLE completion_port;
void shutdown_with_msg(char* msg);
......@@ -106,8 +113,10 @@ void shutdown_with_msg(char* msg) {
if (completion_port != NULL) {
CloseHandle (completion_port);
if (server_socket != NULL) {
CloseHandle (server_socket->handle);
for (int i = 0; i < parallel; i++) {
if (server_socket[i] != NULL) {
CloseHandle (server_socket[i]->handle);
if (clients != NULL) {
for (int i = 0; i < list_length(clients); i++) {
......@@ -168,7 +177,9 @@ void try_write(pclient client) {
void create_server_socket () {
// create a server socket and store it in the ith component of the
// server_socket array
void create_server_socket (int socket_num) {
pserver server;
int key = keygen();
server = (pserver) malloc(sizeof(t_server));
......@@ -190,8 +201,8 @@ void create_server_socket () {
add_to_completion_port(server->handle, to_ms_key(key, SOCKET));
ZeroMemory(&server->connect, sizeof(OVERLAPPED));
server->connect.hEvent = CreateEvent(NULL, FALSE, TRUE, NULL);
server_socket = server;
server_key = key;
server_socket[socket_num] = server;
server_key[socket_num] = key;
if (!ConnectNamedPipe(server->handle, (LPOVERLAPPED) &server->connect)) {
DWORD err = GetLastError();
if (err == ERROR_IO_PENDING) {
......@@ -468,15 +479,18 @@ void do_read(pclient client) {
(LPOVERLAPPED) &client->read);
void accept_client(int key) {
// the server socket with [key] and whose handle is stored in the [socket_num]
// component of the server_socket array, has received a client request. Handle
// it and create a new server socket instance for this socket number
void accept_client(int key, int socket_num) {
pclient client = (pclient) malloc(sizeof(t_client));
client->handle = server_socket->handle;
client->handle = server_socket[socket_num]->handle;
client->readbuf = init_readbuf(BUFSIZE);
client->writebuf = init_writebuf(16);
init_connect_data(&(client->read), READOP);
init_connect_data(&(client->write), WRITEOP);
list_append(clients, key, (void*)client);
......@@ -623,8 +637,23 @@ void init() {
clients = init_list(16);
processes = init_list(16);
server_socket = (pserver*) malloc(parallel * sizeof(pserver));
server_key = (int*) malloc(parallel * sizeof(int));
for (int i = 0; i < parallel; i++) {
// If the key in argument corresponds to a server socket, return the server
// socket number, else return -1.
int get_server_num (int key) {
for (int i=0; i < parallel; i++) {
if (server_key[i] == key)
return i;
return -1;
int main(int argc, char **argv) {
......@@ -632,6 +661,7 @@ int main(int argc, char **argv) {
ULONG_PTR mskey;
int key;
int kind;
int server_num;
p_conn_data conn;
BOOL res;
......@@ -655,13 +685,14 @@ int main(int argc, char **argv) {
key = key_of_ms_key(mskey);
kind = kind_of_ms_key(mskey);
server_num = get_server_num(key);
switch (kind) {
case SOCKET:
if (key == server_key) {
if (server_num != -1) {
if (!res && GetLastError () != ERROR_PIPE_CONNECTED) {
shutdown_with_msg("error connecting client");
} else {
accept_client(key, server_num);
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