Exponenta Banner

Отправка анализа Code Prover с рабочего стола на локально размещенный сервер

Можно выполнить Polyspace® анализ локально на рабочем столе или разгрузка анализа на один или несколько выделенных серверов. В этом разделе показано простое строение сервера с клиентом для разгрузки анализа Polyspace. В этом строении тот же компьютер действует как клиент, который отправляет анализ Polyspace и сервер, который запускает анализ.

Это руководство можно распространить на более сложные строения. Полные инструкции по настройке и рабочему процессу см. в соответствующих ссылках ниже.

Рабочий процесс Клиент-сервер для выполнения анализа Bug Finder

После первоначальной настройки можно отправить анализ Polyspace с рабочего стола клиента на сервер. Рабочий процесс клиент-сервер выполняется в три этапа. Все три шага могут быть выполнены на одном и том же компьютере или на трех разных компьютерах. Это руководство использует тот же компьютер для всего рабочего процесса.

  1. Узел клиента: Вы задаете опции анализа Polyspace и запускаете анализ на рабочем столе клиента. Начальная фаза анализа до компиляции выполняется на рабочем столе. После компиляции задание анализа отправляется на сервер.

    Вам требуется десктопный продукт Polyspace, Polyspace Bug Finder™ на компьютере, который выступает в качестве клиентского узла.

  2. Главный узел: Сервер состоит из головного узла и нескольких рабочих узлов. Главный узел использует планировщик заданий для управления отправками с нескольких клиентских рабочих столов. Затем задания распределяются между рабочими узлами по мере их доступности.

    Вам требуется продукт MATLAB® Parallel Server™ на компьютере, который выступает в качестве головного узла.

  3. Узлы рабочих процессов: Когда рабочий процесс становится доступным, планировщик заданий присваивает рабочий процесс анализу. Анализ Polyspace выполняется на рабочем столе, и результаты загружаются обратно на рабочий стол клиента для проверки.

    Требуется продукт MATLAB Parallel Server на компьютерах, которые выступают в качестве рабочих узлов. Для выполнения анализа также требуются серверные продукты Polyspace, Polyspace Bug Finder Server™ и Polyspace Code Prover™ Server.

См. также раздел Установка продуктов для отправки анализа Polyspace с рабочих столов на удаленный сервер.

Необходимые условия

Это руководство использует тот же компьютер, что и клиент и сервер. Необходимо установить на компьютере следующее:

  • Клиентский продукт: Polyspace Bug Finder

  • Серверные продукты: MATLAB Parallel Server, Polyspace Bug Finder Server и Polyspace Code Prover Server.

Дополнительные сведения см. в разделе Установка продуктов для отправки анализа Polyspace с рабочих столов на удаленный сервер.

Необходимо знать имя хоста компьютера. Например, в Windows®, откройте терминал командной строки и введите:

hostname

Настройка и запуск сервера

Остановить предыдущие службы

Если службы MATLAB Parallel Server были запущены ранее, убедитесь, что все службы остановлены. В частности, вам, возможно, придется:

  • Проверьте свою временную папку, например C:\Windows\Temp в Windows и удалить MDCE папка, если она существует.

  • Явная остановка всех служб.

    Откройте терминал командной строки. Переход к matlabroot\ toolbox\parallel\bin (использование cd) и введите следующее:

    mjs uninstall -clean

    Здесь, matlabroot - папка установки MATLAB Parallel Server, например C:\Program Files\MATLAB\R2021a.

Если вы впервые запускаете сервисы, вам не нужно делать эти шаги.

Сконфигурируйте mjs Настройки сервиса

Перед запуском служб необходимо сконфигурировать mjs параметры сервиса. Переход к matlabroot\ toolbox\parallel\bin, где matlabroot - папка установки MATLAB Parallel Server, например C:\Program Files\MATLAB\R2021a. Измените эти два файла. Чтобы отредактировать и сохранить эти файлы, вы должны открыть свой редактор в режиме администратора.

  • 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. Эта линия должен ссылаться на номер релиза и корневую папку установки серверного продукта Polyspace. Например, если R2021a релиз Polyspace Code Prover Server установлена в корневой папке C:\Program Files\Polyspace Server\R2021a, измените линию на:

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

    В противном случае установка MATLAB Parallel Server не может найти установку Polyspace Code Prover Server, чтобы запустить анализ.

Запуск служб

Запустите mjs и назначить текущий компьютер как головной узел, так и рабочий узел.

Переход к matlabroot\ toolbox\parallel\bin, где matlabroot - папка установки MATLAB Parallel Server, например C:\Program Files\MATLAB\R2021a. Запустите эти команды (непосредственно в командной строке или с помощью скриптов):

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).

Вместо командной строки также можно запустить сервисы из интерфейса Admin Center. Для отправки анализа Polyspace с рабочих столов на удаленный сервер см. раздел Установка продуктов.

Дополнительные сведения о командах см. в разделе Настройка дополнительных опций для интегрирования планировщика заданий MATLAB (MATLAB Parallel Server).

Настройка клиента

Откройте пользовательский интерфейс десктопного продукта Polyspace Bug Finder (или Polyspace Code Prover). Переход к polyspaceroot\ polyspace\bin, где polyspaceroot является папкой установки продукта Polyspace для рабочего стола, например C:\Program Files\Polyspace\R2021a и дважды кликните polyspace исполняемый файл.

Выберите Tools > Preferences. На вкладке Server configuration введите имя хоста компьютера для Job scheduler host name.

Теперь вы настроены для рабочего процесса клиент-сервер.

Отправка анализа с клиента на сервер

Запустите Код Prover на файл example.c обеспечивается вашей установкой.

Прежде чем выполнять эти шаги, чтобы избежать ввода полных путей к исполняемым файлам Polyspace, добавьте путь polyspaceroot\ polyspace\bin на PATH окружение в операционной системе. Вот polyspaceroot является папкой установки продукта Polyspace для рабочего стола, например C:\Program Files\Polyspace\R2021a. Чтобы проверить, добавлен ли уже путь, откройте клемму командной строки и введите:

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-bug-finder вместо polyspace-code-prover. Обратите внимание, что можно запустить polyspace-code-prover команда только с лицензией Polyspace Bug Finder при условии, что вы используете -batch опция.

    После компиляции анализ отправляется на сервер и возвращает идентификатор задания.

  3. См. состояние текущего задания.

    polyspace-jobs-manager listjobs -scheduler hostname

    Вы можете найти текущее задание с помощью идентификатора задания.

  4. После выполнения задания можно явно загрузить результаты.

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

    Здесь, jobID - идентификатор задания из отправки.

Папка результатов содержит загруженный файл результатов (с расширением .pscp). Откройте результаты в пользовательском интерфейсе десктопного продукта Polyspace Bug Finder.

Похожие темы

Документация Polyspace Code Prover

Поддержка