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
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
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
5ccaf91f
Commit
5ccaf91f
authored
Apr 05, 2016
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
src/server/README.server: remove '//' at the beginning of lines
parent
92dd9a78
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
50 additions
and
50 deletions
+50
-50
src/server/README.server
src/server/README.server
+50
-50
No files found.
src/server/README.server
View file @
5ccaf91f
//
This is a VC server for Why3. It implements the following functionalities:
This is a VC server for Why3. It implements the following functionalities:
//
* wait for connections on a unix domain socket (unix) or named pipe
* wait for connections on a unix domain socket (unix) or named pipe
//
(windows) for clients
(windows) for clients
//
* clients can send requests for a process to spawn, including
* clients can send requests for a process to spawn, including
//
timeout/memory limit
timeout/memory limit
//
* server will send back a filename containing the output of the process,
* server will send back a filename containing the output of the process,
//
as well as the time taken and the exit code
as well as the time taken and the exit code
//
//
Command line options
Command line options
//
====================
====================
//
//
-j <n> the maximum number of processes to spawn in parallel
-j <n> the maximum number of processes to spawn in parallel
//
--socket the name of the socket or named pipe
--socket the name of the socket or named pipe
//
//
Protocol
Protocol
//
=========
=========
//
//
A client request is a single line which looks like this:
A client request is a single line which looks like this:
//
//
id;timeout;memlimit;cmd;arg1;arg2;...;argn
id;timeout;memlimit;cmd;arg1;arg2;...;argn
//
//
All items are separated by semicolons, and must not contain semicolons
All items are separated by semicolons, and must not contain semicolons
//
themselves (but may contain spaces). Their meaning is the following:
themselves (but may contain spaces). Their meaning is the following:
//
id - a (ideally) unique identifier which identifies the request
id - a (ideally) unique identifier which identifies the request
//
timeout - the allowed CPU time in seconds for this command;
timeout - the allowed CPU time in seconds for this command;
//
this must be number, 0 for unlimited
this must be number, 0 for unlimited
//
memlimit - the allowed consumed memory for this command
memlimit - the allowed consumed memory for this command
//
this must be number, 0 for unlimited
this must be number, 0 for unlimited
//
cmd - the name of the executable to run
cmd - the name of the executable to run
//
arg(i) - the commandline arguments of the command to run
arg(i) - the commandline arguments of the command to run
//
//
A server answer looks like this:
A server answer looks like this:
//
//
id;exitcode;time;timeout;file
id;exitcode;time;timeout;file
//
//
Their meaning is the following:
Their meaning is the following:
//
id - the identifier of the request to which this answer belongs
id - the identifier of the request to which this answer belongs
//
exitcode - the exitcode of the executed program
exitcode - the exitcode of the executed program
//
time - the time taken by the executed program
time - the time taken by the executed program
//
timeout - 0 for regular exit or crash, 1 for program interrupt through
timeout - 0 for regular exit or crash, 1 for program interrupt through
//
timeout
timeout
//
file - the path to a file which contains the stdout and stderr of the
file - the path to a file which contains the stdout and stderr of the
//
executed program
executed program
//
//
There are two separate implementations on linux and windows, but both are
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).
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
They are both essentially a single-threaded event loop, where the possible
//
events are incoming clients, read/write operations on sockets, and
events are incoming clients, read/write operations on sockets, and
//
terminating child processes. Lists of child processes and connected clients
terminating child processes. Lists of child processes and connected clients
//
are maintained.
are maintained.
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