Автоматизация параллельного программирования затрагивает различные этапы в разработке параллельной программы, начиная от профилирования исходной программы, ее преобразования и приведения к виду, допускающему эффективное распараллеливание, и заканчивая построением параллельной версии программы и ее последующей оптимизацией. Немалое значение имеет выбор целевой модели параллельного программирования, с одной стороны, позволяющей задействовать разнообразие существующих на данный момент аппаратных ресурсов, а с другой, упрощающей разработку автоматизированных средств и позволяющей пользователю изучить решения, принимаемые системой автоматизированного распараллеливания. Система SAPFOR (System FOR Automated Parallelization) объединяет различные подходы, направленные на автоматизацию программирования, и позволяет пользователю принимать активное участие в процесс распараллеливания программ. Кроме того, распараллеливание выполняется в модели DVMH, позволяющей разрабатывать эффективные параллельные программы для гетерогенных вычислительных кластеров.

В настоящей статье рассмотрен подход к автоматизированному распараллеливанию программ, реализованный в системе SAPFOR. Отдельное внимание уделено архитектуре системы и реализации подсистемы интерактивного взаимодействия с пользователем. Рассмотрено применение интерактивной оболочки в процессе распараллеливания и приведены результаты распараллеливания некоторых программ из набора NAS Parallel Benchmarks 3.3.1 c ручным распараллеливанием, выполненным с помощью OpenCL.

Построение расписания – это распределение дискретного множества событий в заданном временном интервале, с соблюдением заданных ограничений. Целью работы является описание математической модели автоматизации процесса составления расписания в образовательном учреждении. Рассмотрены также подходы к составлению оптимального расписания. В исследуемых задачах используется большое количество первоначальной исходной информации, различающейся по своему составу, и содержится большое количество требований, которые должны быть обязательно учтены. Поэтому составление расписания относится к классу NP-полных задач целочисленного программирования, который подразумевает, что с ростом числа значений заданных переменных сложность решения будет расти экспоненциально. Отметим, что качество сформированного расписания занятий напрямую влияет на эффективность учебного процесса вуза.

Описан процесс формирования расписания занятий: на первом этапе нужно сформировать начальное расписание на основе имеющихся студенческого контингента и преподавателей, учебных аудиторий, а также ряда дополнительных ограничений; на втором этапе происходит оптимизация первоначального расписания; на третьем этапе допускается корректировка полученного расписания сотрудниками вуза.

Представлен опыт верификации реализаций сервера криптографического протокола TLS версии 1.3. TLS – широко распространенный криптографический протокол, предназначенный для создания защищенных каналов передачи данных и обеспечивающий необходимую для этого функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. Новая версия протокола TLS 1.3 была представлена в августе 2018 года и имеет ряд существенных отличий по сравнению с предыдущей версией 1.2. Ряд разработчиков протокола TLS уже включил поддержку последней версии в свои реализации. Данные обстоятельства делают актуальным проведение исследований в области верификации и безопасности реализаций новой версии протокола TLS. В работе использован новый тестовый набор для верификации реализаций протокола TLS 1.3 на соответствие спецификациям интернета, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает часть дополнительной функциональности и необязательных расширений протокола.

Для тестирования реализаций на соответствие формальным спецификациям применена технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы с помощью передачи некорректных данных. В поток обмена протокола, создаваемый в соответствии со спецификацией, вносятся некоторые изменения: либо изменяются значения полей сообщений, сформированных на основе разработанной модели протокола, либо изменяется порядок сообщений в потоке обмена. Модель протокола позволяет вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствии с заданной программой. На данный момент было обнаружено несколько отклонений реализаций от спецификации.

Представленный подход доказал свою эффективность в нескольких наших проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок.

Представлен опыт верификации реализаций клиента криптографического протокола TLS версии 1.3. TLS сегодня является одним из наиболее востребованных криптографических протоколов, предназначенных для создания защищенных каналов передачи данных. Протокол обеспечивает необходимую для своих задач функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. В новой версии протокола TLS 1.3 была существенно переработана архитектура, устранен ряд недостатков предыдущих версий, выявленных как при разработке реализаций, так и в процессе их эксплуатации.

В работе использован новый тестовый набор для верификации реализаций клиента протокола TLS 1.3 на соответствие спецификациям интернет, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Для тестирования реализаций на соответствие формальным спецификациям применена технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы (завершение из-за фатальной ошибки, «подвисание», ошибки доступа к памяти) с помощью передачи некорректных данных, такие ситуации часто остаются за рамками требований спецификаций. В сообщения, сформированные на основе разработанной модели протокола, вносятся какие-либо изменения. Модель протокола дает возможность вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствие с заданной программой. Представленный подход доказал свою эффективность в нескольких наших проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает реализации клиентской части протокола.

Метаданные научных публикаций используются для построения каталогов, определения цитируемости публикаций и решения других задач. Автоматизация извлечения метаданных из PDF-файлов позволяет ускорить выполнение обозначенных задач, а от качества извлеченных данных зависит возможность их дальнейшего использования. Проанализированы существующие программные решения, в итоге отобраны три: GROBID, CERMINE, ScientificPdfParser. Предложена методика сравнения этих программных решений распознавания текстов научных публикаций по качеству извлечения метаданных. На основе методики проведен эксперимент по извлечению четырех типов метаданных (название, аннотация, дата публикации, имена авторов). Для сравнения программных решений использован набор из 112457 публикаций с разбиением на 23 предметные области, сформированный на основе данных Semantic Scholar. Приведен пример выбора эффективного программного решения извлечения метаданных в условиях заданных приоритетов для предметных областей и типов метаданных с использованием взвешенной суммы. Определено, что для приведенного примера CERMINE показывает эффективность на 10,5% выше, чем GROBID, и на 9,6% выше, чем ScientificPdfParser.