Вместо того, чтобы запустить анализ Polyspace® вашего локального рабочего стола, можно отправить анализ в удаленный кластер. Можно использовать специализированный кластер для рабочего Polyspace к свободному память на локальном рабочем столе.
Эта тема показывает, как использовать Windows® или скрипты Linux®, чтобы отправить анализ в удаленный кластер и загрузить результаты на ваш рабочий стол после анализа.
Чтобы разгрузить анализ от пользовательского интерфейса Polyspace, смотрите, Отправляют Анализ Polyspace с Рабочего стола на Удаленные серверы.
Для простого примера, который идет через все шаги для разгрузки анализа Polyspace, смотрите, Отправляют Анализ Программы автоматического доказательства Кода с Рабочего стола на Локально Размещенный Сервер. В примере тот же компьютер действует как клиент и сервер.
После начальной настройки можно представить анализ Polyspace с клиентского рабочего стола на сервер. Рабочий процесс клиент-сервер происходит на трех шагах. Все три шага могут быть выполнены на том же компьютере или трех различных компьютерах.
Клиентский узел: Вы задаете опции анализа Polyspace и запускаете анализ клиентского рабочего стола. Начальная фаза анализа до компиляции работает на рабочем столе. После компиляции аналитическое задание представлено серверу.
Вы требуете десктопного решения Polyspace, Polyspace Bug Finder™ на компьютере, который действует как клиентский узел.
Главный узел: сервер состоит из главного узла и нескольких узлов рабочего. Главный узел использует планировщик задания, чтобы справиться с представлениями с нескольких клиентских рабочих столов. Задания затем распределяются узлам рабочего, когда они становятся доступными.
Вы требуете продукта MATLAB® Parallel Server™ на компьютере, который действует как главный узел.
Узлы рабочего: Когда рабочий становится доступным, планировщик задания присваивает анализ рабочему. Анализ Polyspace работает на рабочем, и результаты загружаются назад на клиентский рабочий стол для анализа.
Вы требуете продукта MATLAB Parallel Server на компьютерах, которые действуют как узлы рабочего. Вы также требуете, чтобы серверные продукты Polyspace, Polyspace Bug Finder Server™ и/или Сервер Polyspace Code Prover™ запустили анализ.
Прежде чем вы запустите удаленный анализ при помощи скриптов, необходимо настроить связь между рабочим столом и удаленным сервером. Смотрите продукты Установки для Представления Анализа Polyspace с Рабочих столов на Удаленный сервер.
Чтобы запустить удаленный анализ, используйте эту команду:
polyspaceroot\polyspace\bin\polyspace-code-prover -batch -scheduler NodeHost|MJSName@NodeHost [options] [-mjs-username name]
polyspacerootC:\Program Files\Polyspace\R2021a.
NodeHost
MJSName
Если вы настраиваете связи с кластером от пользовательского интерфейса Polyspace, можно определить NodeHostMJSNameMJSName и NodeHost.
Если вы используете startjobmanager команда, чтобы запустить Планировщик Задания MATLAB, MJSName-name. Для получения дополнительной информации смотрите, Конфигурируют Расширенные настройки для Интегрирования Планировщика Задания MATLAB (MATLAB Parallel Server).
options
-sources-list-file: Задайте текстовый файл с одним именем исходного файла на строку.
-options-file: Задайте текстовый файл с одной опцией на строку.
-results-dir: Задайте папку загрузки для хранения результатов после анализа.
Для полного списка опций смотрите Опции анализа в Polyspace Code Prover. В качестве альтернативы вы можете:
Запустите анализ в пользовательском интерфейсе и остановке после компиляции. Можно получить текстовые файлы и скрипты для выполнения анализа в командной строке. Смотрите Конфигурируют Опции анализа Polyspace в Пользовательском интерфейсе и Генерируют Скрипты.
Введите polyspace-codeprover -h. Список доступных параметров с кратким описанием отображен.
Установите свой курсор на каждую опцию на панели Configuration в пользовательском интерфейсе Polyspace. Нажмите кнопку More Help для получения информации о синтаксисе опции и когда опция будет требоваться.
name
Анализ выполняется локально на вашем рабочем столе в конец фазы компиляции. После компиляции программное обеспечение представляет аналитическое задание кластеру и обеспечивает ID задания. Можно также считать ID из файла ID.txt в папке результатов. Чтобы контролировать ваш анализ, используйте polyspace-jobs-manager команда с ID задания.
Если аналитические остановки после того, как компиляция и вы должны перезапустить анализ, чтобы не повторно выполнять фазу компиляции, используйте опцию -submit-job-from-previous-compilation-results.
Чтобы справиться с несколькими удаленными исследованиями, используйте опцию -batch. Например:
polyspaceroot\polyspace\bin\polyspace-jobs-manager action -scheduler schedulerName
Run Bug Finder or Code Prover analysis on a remote cluster (-batch). Здесь:
polyspaceroot
schedulerName
Имя компьютера, который размещает главный узел вашего кластера MATLAB Parallel Server (NodeHost).
Имя Планировщика Задания MATLAB на главном хосте узла (MJSName@NodeHost
Имя профиля кластера MATLAB (ClusterProfile
Для получения дополнительной информации о кластерах, смотрите, Обнаруживают Кластеры и Профили Кластера Использования (Parallel Computing Toolbox)
Если вы не задаете планировщик задания, polyspace-job-manager использует планировщик, заданный в настройках Polyspace. Чтобы видеть имя планировщика, выберите Tools> Preferences. На вкладке Server Configuration смотрите Job scheduler host name.
action
listjobs:
Сгенерируйте список заданий Polyspace на планировщике. Для каждого задания программное обеспечение производит эту информацию:
ID — Верификация или аналитический идентификатор.
AUTHOR — Имя пользователя, который представил задание.
APPLICATION — Имя Продукта polyspace, например, Polyspace Code Prover или Polyspace Bug Finder.
LOCAL_RESULTS_DIR — Папка результатов на локальном компьютере, заданном через вкладку Tools> Preferences> Server Configuration.
WORKER — Локальный компьютер, от которого было представлено задание.
STATUS — Состояние задания, например, running и completed.
DATE — Дата, в которую было представлено задание.
LANG — Язык представленного исходного кода.
download -job
ID
-results-folder
FolderPath:
Загрузите результаты анализа с заданным ID к папке, заданной FolderPath.
Когда аналитическое задание ставится в очередь на сервере, команда polyspace-code-prover возвращает ID задания. Кроме того, файл ID.txt в результатах папка содержит ID задания в этом формате:
job_id;server_name:project_name version_number
92;localhost:Demo 1.0.Если вы не используете -results-folder опция, загрузки программного обеспечения результат к папке, которую вы задали когда стартовый анализ, с помощью -results-dir опция.
После загрузки результатов используйте пользовательский интерфейс Polyspace, чтобы просмотреть результаты.
getlog - задание :ID
Открытый журнал для задания с заданным ID.
удалите - задание :ID
Удалите задание с заданным ID.
продвиньте - задание :ID
Продвиньте задание с заданным ID в очереди.
понизьте в должности - задание ID
Понизьте в должности задание с заданным ID в очереди.
В Windows, чтобы не вводить команды каждый раз, можно сохранить команды в пакетном файле. В Linux можно повторно запустить анализ при помощи сценария оболочки. Создать пакетный файл для рабочего анализа:
Сохраните свои опции анализа в файле listofoptions.txt. Смотрите -options-file.
Создайте файл launcher.bat в текстовом редакторе как Блокнот.
В файле введите эти команды:
echo off set POLYSPACE_PATH=polyspaceroot\polyspace\bin set RESULTS_PATH=C:\Results set OPTIONS_FILE=C:\Options\listofoptions.txt "%POLYSPACE_PATH%\polyspace-code-prover.exe" -batch -scheduler localhost -results-dir %RESULTS_PATH% -options-file %OPTIONS_FILE% pause
polyspaceroot папка установки Polyspace. localhost
Замените определения этих переменных в файле:
POLYSPACE_PATH: Введите фактическое местоположение .exe файл.
RESULTS_PATH: Введите путь к папке. Файлы, сгенерированные во время компиляции, сохраняются в папке.
OPTIONS_FILE: Введите путь к файлу listofoptions.txt.
Дважды кликните launcher.bat запускать анализ.
Совет
Если при запуске анализ Polyspace, Windows .bat или Linux .sh файл сгенерирован. Файл находится в .settings подпапка в вашей папке результатов. Вместо того, чтобы писать скрипт с нуля, можно повторно запустить анализ с помощью этого файла.
Run Bug Finder or Code Prover analysis on a remote cluster (-batch)