Send Code Prover Analysis from Desktop to Locally Hosted Server

You can perform a Polyspace^® analysis locally on your desktop or offload the analysis to one or more dedicated servers. This topic shows a simple server-client configuration for offloading the Polyspace analysis. In this configuration, the same computer acts as a client that submits a Polyspace analysis and a server that runs the analysis.

You can extend this tutorial to more complex configurations. For full setup and workflow instructions, see related links below.

Note

The versions of Polyspace on the client and server machines must match.

Client-Server Workflow for Running Bug Finder Analysis

After the initial setup, you can submit a Polyspace analysis from a client desktop to a server. The client-server workflow happens in three steps. All three steps can be performed on the same computer or three different computers. This tutorial uses the same computer for the entire workflow.

Client node: You specify Polyspace analysis options and start the analysis on the client desktop. The initial phase of analysis till compilation runs on the desktop. After compilation, the analysis job is submitted to the server.
You require the Polyspace desktop product, Polyspace Bug Finder™ on the computer that acts as the client node.
Head node: The server consists of a head node and several worker nodes. The head node uses a job scheduler to manage submissions from multiple client desktops. The jobs are then distributed to the worker nodes as they become available.
You require the product MATLAB^® Parallel Server™ on the computer that acts as the head node.
Worker nodes: When a worker becomes available, the job scheduler assigns the analysis to the worker. The Polyspace analysis runs on the worker and the results are downloaded back to the client desktop for review.
You require the product MATLAB Parallel Server on the computers that act as worker nodes. You also require the Polyspace server products, Polyspace Bug Finder Server™ and Polyspace Code Prover™ Server, to run the analysis.

Flow diagram of a typical workflow for submitting analysis jobs from a client to a server.

Prerequisites

This tutorial uses the same computer as client and server. You must install the following on the computer:

Client-side product: Polyspace Bug Finder
Server-side products: MATLAB Parallel Server, Polyspace Bug Finder Server and Polyspace Code Prover Server.

For more information, see Install Products for Submitting Polyspace Analysis from Desktops to Remote Server.

You must know the host name of your computer. For instance, in Windows^®, open a command-line terminal and enter:

hostname

Configure and Start Server

Stop Previous Services

If you started the services of MATLAB Parallel Server previously, make sure that you have stopped all services. In particular, you might have to:

Check your temporary folder, for instance, C:\Windows\Temp in Windows, and remove the MDCE folder if it exists.
Stop all services explicitly. You do not require this step in Linux^®.
Open a command-line terminal. Navigate to matlabroot\toolbox\parallel\bin (using cd) and enter the following:
```
mjs uninstall -clean
```
Here, matlabroot is the MATLAB Parallel Server installation folder, for instance, C:\Program Files\MATLAB\R2024b.

If this is the first time you are starting the services, you do not have to do these steps.

Configure `mjs` Service Settings

Before starting services, you have to configure the mjs service settings. Navigate to matlabroot\toolbox\parallel\bin, where matlabroot is the MATLAB Parallel Server installation folder, for instance, C:\Program Files\MATLAB\R2024b. Modify these two files. To edit and save these files, you have to open your editor in administrator mode.

mjs_def.bat (Windows) or mjs_def.sh (Linux)
Read the instructions in the file and uncomment the lines as needed. At a minimum, you might have to uncomment these lines:
- Hostname:
```
REM set HOSTNAME=myHostName
```
  in Windows or
```
#HOSTNAME=`hostname -f`
```
  in Linux. Remove the REM or # and explicitly specify your computer host name.
- Security level:
```
REM set SECURITY_LEVEL=
```
  in Windows or
```
#SECURITY_LEVEL=""
```
  in Linux. Remove the REM or # and explicitly specify a security level.
Otherwise, you might see an error later when starting the job scheduler.
mjs_polyspace.conf
Modify and uncomment the line that refers to a Polyspace server product root. The line should refer to the release number and root folder of your Polyspace server product installation. For instance, if the R2024b release of Polyspace Code Prover Server is installed in the root folder C:\Program Files\Polyspace Server\R2024b, modify the line to:
```
POLYSPACE_SERVER_ROOT=C:\Program Files\Polyspace Server\R2024b
```
Otherwise, the MATLAB Parallel Server installation cannot locate the Polyspace Code Prover Server installation to run the analysis.

Start Services

Start the mjs services and assign the current computer as both the head node and a worker node.

Navigate to matlabroot\toolbox\parallel\bin, where matlabroot is the MATLAB Parallel Server installation folder, for instance, C:\Program Files\MATLAB\R2024b. Run these commands (directly at the command line or using scripts):

mjs install
mjs start
startjobmanager -name JobScheduler -remotehost hostname -v
startworker -jobmanagerhost hostname -jobmanager JobScheduler -remotehost hostname -v

Here, hostname is the host name of your computer. This is the host name that you specified in the file mjs_def.bat (Windows) or mjs_def.sh (Linux). Note that in Linux, you do not require the command mjs install.

Instead of the command line, you can also start the services from the Admin Center interface. See Install Products for Submitting Polyspace Analysis from Desktops to Remote Server.

For more information on the commands, see Configure Advanced Options for MATLAB Job Scheduler Integration (MATLAB Parallel Server).

Configure Client

Open the user interface of the desktop product, Polyspace Bug Finder (or Polyspace Code Prover). Navigate to polyspaceroot\polyspace\bin, where polyspaceroot is the Polyspace desktop product installation folder, for instance, C:\Program Files\Polyspace\R2024b and double-click the polyspace executable.

Select Tools > Preferences. On the Server configuration tab, enter the host name of your computer for Job scheduler host name.

Example server configuration in Polyspace Preferences.

You are now set up for the server-client workflow.

Send Analysis from Client to Server

Run Code Prover on the file example.c provided with your installation.

Before running these steps, to avoid entering full paths to the Polyspace executables, add the path polyspaceroot\polyspace\bin to the PATH environment variable on your operating system. Here polyspaceroot is the Polyspace desktop product installation folder, for instance, C:\Program Files\Polyspace\R2024b. To check if the path is already added, open a command line terminal and enter:

polyspace-code-prover -h

If the path to the command is already added, you see the full list of options.

Copy the file example.c and all header files from polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources to a folder with write permissions.
Open a command terminal. Navigate to the folder where you saved example.c and enter the following:
```
polyspace-code-prover -sources example.c -I . -main-generator -results-dir resultsFolder -batch -scheduler hostname
```
Here, hostname is the host name of your computer. To run a Bug Finder analysis, use polyspace-bug-finder instead of polyspace-code-prover. Note that you can run the polyspace-code-prover command with a Polyspace Bug Finder license only, provided you use the -batch option.
After compilation, the analysis is submitted to a server and returns a job ID.
See the status of the current job.
```
polyspace-jobs-manager listjobs -scheduler hostname
```
You can locate the current job using the job ID.
Once the job is completed, you can explicitly download the results.
```
polyspace-jobs-manager download -job jobID -results-folder . -scheduler hostname
```
Here, jobID is the job ID from the submission.

The results folder contains the downloaded results file (with extension .pscp). Open the results in the user interface of the desktop product, Polyspace Bug Finder.