メインコンテンツ

このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

デスクトップからローカルでホストされているサーバーへの Code Prover 解析の送信

Polyspace® 解析をデスクトップでローカルに実行したり、解析の負荷を 1 台以上の専用サーバーに移したりできます。このトピックでは、Polyspace 解析の負荷を移すための単純なサーバー/クライアント構成について説明します。この構成では、同じコンピューターが、Polyspace 解析を送信するクライアントおよび解析を実行するサーバーとして機能します。

このチュートリアルは、より複雑な構成に拡張できます。完全な設定とワークフローの手順については、下記の関連リンクを参照してください。

メモ

クライアント マシンとサーバー マシンの Polyspace のバージョンは一致している必要があります。

Bug Finder 解析を実行するためのクライアント/サーバー ワークフロー

初期設定の後、Polyspace 解析をクライアント デスクトップからサーバーに送信できます。クライアント/サーバー ワークフローは 3 つのステップで行われます。3 つのステップすべてが同じコンピューターで実行されるか、3 つの異なるコンピューターで実行されます。このチュートリアルでは、ワークフロー全体に対して同じコンピューターを使用します。

  1. クライアント ノード:Polyspace 解析オプションを指定し、クライアント デスクトップで解析を開始します。コンパイルまでの解析の初期フェーズは、デスクトップ上で実行されます。コンパイル後、解析ジョブはサーバーに送信されます。

    クライアント ノードとして機能するコンピューター上に Polyspace デスクトップ製品 Polyspace Bug Finder™ が必要です。

  2. ヘッド ノード:サーバーはヘッド ノードと複数のワーカー ノードで構成されています。ヘッド ノードは、ジョブ スケジューラを使用して複数のクライアント デスクトップからの送信を管理します。ジョブはワーカー ノードが使用可能になると、ワーカー ノードに分散されます。

    ヘッド ノードとして機能するコンピューター上に製品 MATLAB® Parallel Server™ が必要です。

  3. ワーカー ノード:ワーカーが使用可能になると、ジョブ スケジューラが解析をそのワーカーに割り当てます。Polyspace 解析はワーカーで実行され、結果はレビューのために元のクライアント デスクトップにダウンロードされます。

    ワーカー ノードとして機能するコンピューター上に製品 MATLAB Parallel Server が必要です。解析を実行するには、Polyspace サーバー製品 Polyspace Bug Finder Server™ および Polyspace Code Prover™ Server も必要です。

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

Install Products for Submitting Polyspace Analysis from Desktops to Remote Serverも参照してください。

前提条件

このチュートリアルでは、クライアントおよびサーバーとして同じコンピューターを使用します。コンピューターに以下をインストールしなければなりません。

  • クライアント側製品: Polyspace Bug Finder

  • サーバー側製品: MATLAB Parallel ServerPolyspace Bug Finder Server、および Polyspace Code Prover Server

詳細は、Install Products for Submitting Polyspace Analysis from Desktops to Remote Serverを参照してください。

コンピューターのホスト名を知っておかなければなりません。たとえば、Windows® では、コマンド ライン ターミナルを開いて、次のように入力します。

hostname

サーバーの構成と起動

以前のサービスの停止

あらかじめ MATLAB Parallel Server のサービスを開始していた場合、すべてのサービスを停止していることを確認します。特に、以下を行う必要がある可能性があります。

  • Windows の C:\Windows\Temp などの一時フォルダーをチェックして、MDCE フォルダーが存在する場合は削除。

  • すべてのサービスを明示的に停止。Linux® ではこの手順は不要。

    コマンド ライン ターミナルを開きます。(cd を使用して) matlabroot\toolbox\parallel\bin に移動し、以下を入力します。

    mjs uninstall -clean
    ここで、matlabrootMATLAB Parallel Server インストール フォルダーです。たとえば、C:\Program Files\MATLAB\R2025a です。

初めてサービスを開始する場合は、これらの手順を実行する必要はありません。

mjs サービス設定の構成

サービスを開始する前に、mjs サービス設定を構成しなければなりません。matlabroot\toolbox\parallel\bin に移動します。ここで matlabrootMATLAB Parallel Server インストール フォルダーです。たとえば、C:\Program Files\MATLAB\R2025a です。以下の 2 つのファイルを変更します。これらのファイルを編集して保存するには、エディターを管理者モードで開かなければなりません。

  • mjs_def.bat (Windows) または mjs_def.sh (Linux)

    ファイル内の説明を読み、必要に応じて行のコメントを解除します。少なくとも、以下の行のコメントは解除しなければならない場合があります。

    • ホスト名:

      REM set HOSTNAME=myHostName
      (Windows の場合) または
      #HOSTNAME=`hostname -f`
      (Linux の場合)。REM または # を削除し、コンピューターのホスト名を明示的に指定します。

    • セキュリティ レベル:

      REM set SECURITY_LEVEL=
      (Windows の場合) または
      #SECURITY_LEVEL=""
      (Linux の場合)。REM または # を削除し、セキュリティ レベルを明示的に指定します。

    そうしない場合、後でジョブ スケジューラを開始する際にエラーが発生する可能性があります。

  • mjs_polyspace.conf

    Polyspace Server 製品のルートを参照する行を変更し、コメントを解除します。この行は、Polyspace サーバー製品インストールのリリース番号とルート フォルダーを参照する必要があります。たとえば、Polyspace Code Prover ServerR2025a リリースがルート フォルダー C:\Program Files\Polyspace Server\R2025a にインストールされている場合は、この行を次のように変更します。

    POLYSPACE_SERVER_ROOT=C:\Program Files\Polyspace Server\R2025a
    

    そうしない場合、MATLAB Parallel Server インストールは、解析を実行する Polyspace Code Prover Server インストールを見つけることができません。

サービスの開始

mjs サービスを開始し、現在のコンピューターをヘッド ノードとワーカー ノードの両方として割り当てます。

matlabroot\toolbox\parallel\bin に移動します。ここで matlabrootMATLAB Parallel Server インストール フォルダーです。たとえば、C:\Program Files\MATLAB\R2025a です。以下のコマンドを (コマンド ラインで直接またはスクリプトを使用して) 実行します。

mjs install
mjs start
startjobmanager -name JobScheduler -remotehost hostname -v
startworker -jobmanagerhost hostname -jobmanager JobScheduler -remotehost hostname -v
ここで、hostname はコンピューターのホスト名です。これは、ファイル mjs_def.bat (Windows) または mjs_def.sh (Linux) で指定したホスト名です。Linux の場合は、コマンド mjs install は不要であることに注意してください。

コマンド ラインの代わりに、管理センター インターフェイスからサービスを開始することもできます。Install Products for Submitting Polyspace Analysis from Desktops to Remote Serverを参照してください。

コマンドの詳細は、MATLAB ジョブ スケジューラを統合するための詳細オプションの設定 (MATLAB Parallel Server)を参照してください。

クライアントの設定

デスクトップ製品 Polyspace Bug Finder (または Polyspace Code Prover) のインターフェイスを開きます。polyspaceroot\polyspace\bin に移動します。ここで polyspaceroot は Polyspace デスクトップ製品のインストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2025a です。実行可能ファイル polyspace をダブルクリックします。

[ツール][基本設定] を選択します。[サーバー設定] タブで、[ジョブ スケジューラのホスト名] にコンピューターのホスト名を入力します。

Example server configuration in Polyspace Preferences.

これでサーバー/クライアント ワークフローの設定が完了しました。

クライアントからサーバーへの解析の送信

インストールで提供されるファイル example.c に対して Code Prover を実行します。

以下の手順を実行する前に、Polyspace の実行可能ファイルへの絶対パスを入力しなくてもよいように、パス polyspaceroot\polyspace\bin をオペレーティング システムの環境変数 PATH に追加します。ここで、polyspaceroot は Polyspace デスクトップ製品のインストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2025a です。パスが既に追加されているかどうかをチェックするには、コマンド ライン ターミナルを開いて、次のように入力します。

polyspace-code-prover -h
コマンドへのパスが既に追加されている場合、すべてのオプションのリストが表示されます。

  1. ファイル example.c およびすべてのヘッダー ファイルを、polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources から書き込み権限のあるフォルダーにコピーします。

  2. コマンド ターミナルを開きます。example.c を保存したフォルダーに移動し、以下を入力します。

    polyspace-code-prover -sources example.c -I . -main-generator -results-dir resultsFolder -batch -scheduler hostname
    ここで、hostname はコンピューターのホスト名です。Bug Finder 解析を実行する場合は、polyspace-code-prover の代わりに polyspace-bug-finder を使用します。polyspace-code-prover コマンドは、-batch オプションを使用する場合、Polyspace Bug Finder ライセンスのみで実行できます。

    コンパイル後、解析はサーバーに送信され、ジョブ ID を返します。

  3. 現在のジョブのステータスを確認します。

    polyspace-jobs-manager listjobs -scheduler hostname
    ジョブ ID を使用して現在のジョブを見つけることができます。

  4. ジョブが完了したら、明示的に結果をダウンロードできます。

    polyspace-jobs-manager download -job jobID -results-folder . -scheduler hostname

    ここで、jobID は送信時に得られたジョブ ID です。

結果フォルダーには、ダウンロードされた結果ファイル (拡張子 .pscp) が格納されます。デスクトップ製品 Polyspace Bug Finder のユーザー インターフェイスで結果を開きます。

参考

トピック