Семинары лаборатории языковых инструментов JetBrains Research

Лаборатория языковых инструментов — совместная инициатива JetBrains и математико-механического факультета СПбГУ.

Сотрудники лаборатории исследуют:

• формализацию и верификацию семантики языков программирования в контексте слабых моделей памяти;
• логическое и реляционное программирование;
• теорию формальных языков и ее применения;
• метапрограммирование, специализацию и частичные вычисления;
• формальную верификацию и применение SMT-решателей.

На еженедельных семинарах выступают как наши сотрудники и студенты, так и приглашенные докладчики. С недавних пор семинары записываются, их можно посмотреть на Youtube. В этом посте мы поделимся ссылками и описаниями прошедших встреч, а также расскажем, как не пропустить анонсы будущих мероприятий.



Прошедшие доклады:

Персистентная семантика файловой системы ext4 и верификация в ней

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

Первым шагом к решению этой проблемы является формализация файловых систем. В докладе мы рассмотрим Linux ext4 и её формальную модель, интегрированную с моделью памяти C/С++11. Кроме того, обсудим адаптацию алгоритма проверки моделей GenMC для верификации программ, работающих с файлами. В конце будут приведены примеры ошибок, которые удалось найти с помощью адаптированного GenMC в текстовых редакторах, таких как vim и nano.

Докладчик: Илья Кайсин

Ссылка

Реализация сжатия ссылок в кучу в GraalVM Native Image

В некоторых приложениях размер адресного пространства существенно превышает размер области памяти, на которую может ссылаться указатель. Сжатие ссылок позволяет уменьшить размер приложения и ускорить его выполнение и старт. Рассматриваются варианты реализации сжатых ссылок. Демонстрируется способ легкого введения сжатия ссылок в хорошо организованную реализацию языков программирования.

Докладчик: Олег Плисс

Ссылка

Слегка субкубический алгоритм для задачи поиска путей с контекстно-свободными ограничениями

Все мы так или иначе сталкиваемся с задачами, решаемыми за полиномиальное время. Но есть такие задачи, для которых кубическое или, например, квадратичное время работы является слишком неэффективным для использования на практике. Возникает вопрос, может ли конкретная задача быть решена немного быстрее, например, хотя бы за субкубическое (n^{3-e}) (или субквадратичное) время? Если нет, то как показать, что такое время работы оптимально?

В докладе будет рассмотрена одна из таких задач — задача поиска путей с контекстно-свободными ограничениями (CFL-reachability), к которой сводится большое количество задач анализа программ. Вопрос о существовании субкубического алгоритма для решения этой задачи является открытым уже более 30 лет. Оптимально ли классическое кубическое решение? Мы попробуем ответить на этот вопрос, используя инструменты современного направления теории сложности — fine-grained complexity. Также будет показано, как ускорить время решения на логарифмический фактор, получив тем самым "«слегка субкубический»" алгоритм для задачи CFL-reachability.

Докладчик: Екатерина Шеметова

Ссылка

Построение сертифицированных частичных вычислителей

Частичные вычисления позволяют улучшать производительность кода на основании частично известных данных или свойств использованных в программе операций, заданных, например, правилами переписывания термов. Реализация сертифицированных частичных вычислителей, работающих за адекватное время — нетривиальная задача сама по себе. Создавать их, используя как можно меньше несертифицированных компонент — еще сложнее. В докладе я расскажу про систему для создания таких частичных вычислителей, предложенную Джейсоном Гроссом. Система реализована на Coq, позволяет задавать свои правила перепивывания термов и способна специализировать библиотеки сертифицированного кода на Coq длиной в тысячи строк.

Докладчик: Екатерина Вербицкая

Ссылка

Проверка моделей в слабых моделях памяти

Проверка моделей — это метод автоматической формальной верификации программ. На сегодняшний день большинство инструментов для проверки моделей либо не учитывают эффекты, возникающие в слабых моделях памяти, либо работают только с некоторой фиксированной моделью. Среди этих инструментов выделяется GenMC, который не привязан к конкретной модели памяти. GenMC может работать с широким классом моделей (в который входят, например, модели RC11 и IMM). Тем не менее наиболее сложные и интересные модели (Promising, Weakestmo) не поддерживаются, так как эти в этих моделях не выполняются некоторые свойства, подразумеваемые GenMC. Кроме того, оказывается что и сами эти модели (Promising, Weakestmo), настолько «слабые», что какой-либо алгоритм их проверки может оказаться неприменимым на практике.

На семинаре мы рассмотрим алгоритм, лежащий в основе GenMC. Мы поговорим об ограничениях на входную модель памяти, которые накладывает GenMC и рассмотрим проблемы, возникающие при попытке осабить эти ограничения. Также будет предложена модифицированная версия модели Weakestmo, которая существенно упрощаёт алгоритм её проверки и в то же время сохраняет все желаемые свойства модели. В конце доклада будет приведён прототип усовершенствованного алгоритма GenMC, который добавляет поддержку модели Weakestmo.

Докладчик: Евгений Моисеенко

Ссылка

Логическое программирование высшего порядка

В докладе мы познакомимся с языком программирования λProlog. Объединяя логическое программирование с программированием высшего порядка, λProlog позволяет естественным образом поддерживать HOAS для описания языков, избавляя программиста от необходимости ручной работы со связываниями переменных. В случае с отношениями высшего порядка унификация является неразрешимой, однако существует некоторое подмножество языка, на котором унификацию всегда можно выполнить. Я расскажу про то, зачем нужно логическое программирование высшего порядка и как в нем реализовать унификацию.

Докладчик: Екатерина Вербицкая

Ссылка

Выразительная сила типов высшего порядка и недетерминизма

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

Докладчик: Даниил Березун

Ссылка

Переоснащение параллелизма для OCaml

Сейчас ведется работа на новой реализацией среды исполнения программ на языке OCaml, с улучшенной поддержкой параллелизма. В докладе будут рассмотрены выдвинутые требования и инженерные решения, которые были приняты, чтобы удовлетворить этим требованиям

Докладчик: Дмитрий Косарев

Ссылка

О представимости инвариантов программ с алгебраическими типами данных

Со времён появления логики Хоара принято выражать свойства и сертификаты корректности программ на языках первого порядка. Современные методы автоматического вывода индуктивных инвариантов программ ориентированы на представление инвариантов также в логике первого порядка. Хотя такие представления очень выразительны для некоторых теорий (LIA, LRA BV, теория массивов), они не позволяют выразить многие интересные свойства программ над алгебраическими типами данных (АТД).

В докладе будут рассмотрены три различных подхода к представлению индуктивных инвариантов программ над АТД: формулами первого порядка, древовидными автоматами и формулами первого порядка с ограничениями на размер. Мы сравним их выразительную мощность и увидим на простых примерах, что очень часто современные инструменты вывода инвариантов не будут завершаться по причине непредставимости инварианта в языке. Также мы рассмотрим, как автоматически выводить регулярные инварианты программ над АТД с помощью инструментов поиска конечных моделей. Будет представлено сравнение эффективности вывода регулярных инвариантов через построение конечных моделей с современными Хорн-решателями.

Докладчик: Юрий Костюков

Ссылка

Разработка компиляторов предметно-ориентированных языков для спецпроцессоров

В составе современных вычислительных систем все чаще используются аппаратные спецпроцессоры, программируемые на предметно-ориентированных языках. Популярность набирает подход compiler-in-the-loop, предполагающий совместную разработку спецпроцессора и компилятора. При этом традиционный инструментарий, GCC и LLVM, оказывается недостаточным для быстрой разработки оптимизирующих компиляторов, порождающих целевой код нетрадиционной, нерегулярной архитектуры со статическим параллелизмом операций.

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

Докладчик: Пётр Советов

Ссылка

Логика некорректности

Всем хорошо известна так называемая логика корректности Хоара, позволяющая формально доказать, что программа работает правильно. А что если мы захотим формально доказать, что в программе есть баг? Например, что программа упадет, если дать ей на вход очень большую строку, при этом не уточняя, какая именно это строка. Оказывается, процесс доказательства наличия бага в программе можно формализовать так же, как мы формализуем доказательство корректности с помощью логики Хоара, — используя «Логику Некорректности» В докладе мы поговорим про «Логику Некорректности»: обсудим ее связь с логикой корректности Хоара, посмотрим на ее натуральный вывод и семантику, отловим пару багов и, наконец, рассмотрим, как она связана с Динамической Логикой и Relation Algebra.

Докладчик: Владимир Гладштейн

Ссылка

Семантика рекурсивных типов с индексацией шагов исполнения

Стандартным подходом для задачи написания и проверки безопасности ненадежного кода является построение системы типов, выделяющей безопасные программы. При этом обосновывать корректность системы типов можно двумя принципиально разными путями: синтаксически (доказывая прогресс и сохранение типа напрямую по правилам типизации) и семантически (используя некоторую математическую модель для типов). Appel и McAllester предложили метод построения семантической модели на базе аппроксимаций результата исполнения программы для заданного числа шагов. В отличие от других известных конструкций, такая семантика не полагается на понятия из теории решеток или теории рекурсии, поэтому проста для формализации. В то же время, она позволяет описывать нетривиальные и полезные расширения, такие как рекурсивные типы.

В докладе на примере семантики с индексацией шагов исполнения мы рассмотрим семантический подход к доказательству типобезопасности и эквивалентности программ для лямбда-исчисления с рекурсивными типами и (возможно) более реалистичного языка инструкций машины фон Неймана.

Докладчик: Дима Розплохас

Ссылка

Ближайший доклад 2 ноября сделает Антон Трунов по теме “Неразличимые доказательства: по определению, но без аксиомы К”. Присоединяйтесь в 17:30 в Google Meet по ссылке.

Анонс семинара 2 ноября

Не секрет, что формализация математики, логики, языков программирования, а также верификация программ с использованием теории типов наталкивается на сложности работы с иерархией равенств в теории типов. Научный фольклор не случайно пестрит упоминаниями «геенны сетоидной». При этом, чем больше термов вычислительно равны, т.е. неразличимы в используемой формальной системе, тем проще с ней работать на практике — как в смысле сокращения ручного труда, так и увеличения производительности проверки типов, например, при использовании рефлексивных доказательств. В особенности это справедливо для термов, интерпретируемых как доказательства неразличимости высказываний. Однако, безыскусное внедрение неразличимости доказательств в теорию типов приводит либо к потере разрешимости проверки типов, либо к потере совместимости с другими расширениями базовой теории, такими как Унивалентность.

Первая часть доклада подготовит почву для освещения основной темы: в частности будет рассмотрена структура вселенных в системе интерактивных доказательств Coq. Во второй части пойдет речь об относительно недавно добавленной экспериментальной вселенной строгих высказываний SProp с неразличимыми по определению доказательствами. При этом сохраняются перечисленные выше желательные свойства и показывается неадекватность известного подхода одиночной элиминации во вселенной Prop для настоящей проблемы. Также будет показана связь SProp с другими вселенными на простых примерах.

Чтобы получать анонсы наших семинаров:

• вступите в Google группу,
• вступите в Vk группу лаборатории,
• или добавьте себе календарь семинаров.