Remote-Run Tutorial¶
This tutorial aims to provide basic understanding of how to start the fm-weck server and how to remotely run tasks on that server.
For a more detailed explanation of fm-weck and its main arguments, please refer to this tutorial.
Table of Contents¶
Client side¶
To start a run remotely, run fm-weck remote-run with the same arguments and options as the fm-weck run mode, as follows:
$ fm-weck remote-run --help
usage: fm-weck remote-run [-h] -p PROPERTY --host HOST [--timelimit TIMELIMIT] [--output-path OUTPUT_PATH] TOOL FILES [FILES ...]
positional arguments:
TOOL The tool to obtain the container from. Can be the form <tool>:<version>. The TOOL is either the name of a
bundled tool (c.f. fm-weck --list) or the path to an fm-tools YAML file.
FILES Files to pass to the tool.
options:
-h, --help show this help message and exit
-p PROPERTY, --property PROPERTY, --spec PROPERTY
Property that is forwarded to the fm-tool. Either a path to a property file or a property name from SV-
COMP or Test-Comp. Use fm-weck serve --list to view all properties that can be called by name.
--host HOST Specifies the IP address and the port of the server.
--timelimit TIMELIMIT
Specifies the maximum amount of time to wait for the server to finish a run, in seconds.
--output-path OUTPUT_PATH
Specifies the location where the incoming files from the server will be stored, relative to the current
working directory.
In addition to the usual arguments, the remote-run expects the host option, which represents the address of the server.
We can also get the results of the previously started run with the command fm-weck get-run, as follows:
$ fm-weck get-run --help
usage: fm-weck get-run [-h] --host HOST [--timelimit TIMELIMIT] [--output-path OUTPUT_PATH] RUN-ID
positional arguments:
RUN-ID The run ID for which to get the result.
options:
-h, --help show this help message and exit
--host HOST Specifies the IP address and the port of the server.
--timelimit TIMELIMIT
Specifies the maximum amount of time to wait for the server to finish a run, in seconds.
--output-path OUTPUT_PATH
Specifies the location where the incoming files from the server will be stored, relative to the current working directory.
Example client calls¶
A typical client call could look like this:
fm-weck remote-run cpachecker:2.3.1 --host localhost:50051 --property unreach-call ./c_program_example.c
This command makes a blocking call to the server and waits for the resulting files to be returned. The property and tool can either be names or paths to user defined files.
The command also returns the unique ID of the run to the stdout, which can be used with the fm-weck get-run command to get the run results.
This can be useful if the blocking call returns an empty value due to a time-out or an internal error.
It is also possible to specify how long the call will block until it returns, and the path where the server’s output files will be stored.
$ fm-weck remote-run cpachecker:2.3.1 --host localhost:50051 --property unreach-call ./c_program_example.c --timelimit 15 --output-path path/to/output
Establishing a connection to the server ...
Run ID: 12345
$
This command blocks the client for 15 seconds, then returns, regardless of whether the server finished execution. If the result is received, it stores the resulting files at path/to/output, relative to the current working directory.
If the 15 second time limit is reached before the server finishes the execution, the call returns without the result. In this case, the client can run the following command to try and retrieve the result of the run:
fm-weck get-run 12345 --host localhost:50051 --timelimit 5 --output-path path/to/output
Server side¶
Starting the server is straightforward:
$ fm-weck server --help
usage: fm-weck server [-h] --port PORT --listen IPADDR
options:
-h, --help show this help message and exit
--port PORT Specifies the port number on which the server will listen.
--listen IPADDR Specifies the IP address on which the server will listen.
Example of starting the server:
$ fm-weck server --port 50051 --listen localhost
INFO:fm_weck.grpc_service.server_utils:Server started, listening on 50051
|