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

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

Можно расширить этот пример к более комплексным настройкам. Для полной настройки и инструкций по рабочему процессу, смотрите ссылки по теме ниже.

Рабочий процесс клиент-сервер для рабочего анализа средства поиска ошибки

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

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

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

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

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

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

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

См. также продукты Установки для Представления Анализа 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\R2020a.

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

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

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

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

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

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

Запустите сервисы

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

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

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\R2020a и дважды кликните polyspace исполняемый файл.

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

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

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

Запустите Программу автоматического доказательства Кода на файле example.c предоставленный вашу установку.

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

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

    После компиляции анализ представлен серверу и возвращает 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.

Похожие темы