https://vk.com/msumathprogx05 — в группе VK есть видеозаписи вводных спецкурсов по системам типов в языках программирования: (отправьте заявку и напишите мне).
http://seminar.s2s.msu.ru/students — направления работы нашей исследовательской группы.
На этой странице кратко представлены варианты направлений для курсовых и дипломных работ, которые можно вести под моим руководством на кафедре вычислительной математики.
Область исследований — приложение математических методов (в первую очередь — математической логики) программированию.
Цель — разработка надёжных программ.
«Система типов это гибко управляемый синтаксический метод доказательства отсутствия в программе определенных видов поведения при помощи классификации выражений языка по разновидностям вычисляемых ими значений.» (перефразируя Б. Пирса — «Типы в языках программирования»)
Суперкомпиляция — метод анализа и преобразования программ, в ходе которого:
Самое точное описание поведения программы даёт не описание типов:
int main(int argc, char *argv[argc])
а её исходный код:
{
if (argc == 2) {
printf("Hello, %s!", argv[1]);
return 0;
} else {
printf("Not enough arguments!");
return 1;
}
}
Подход к анализу программ: определяем аппроксимацию входных данных. С помощью суперкомпиляции проверяем адекватность аппроксимации и уточняем поведение программы:
main(1, неизвестный_параметр) ⇒ { printf("Hello, %s!", неизвестный_параметр[1]); return 0; }
main(0, неизвестный_параметр) ⇒ { printf("Not enough arguments!"); return 1; }
Проблемы: комбинаторный взрыв; условия завершимости программы (проблема останова).
Современные языки программирования (Rust) предотвращают ошибки при работе с памятью с помощью системы типов.
Большая часть фундамента современного программного обеспечения (ядро операционной системы, системные библиотеки) написано на языке C.
Можно ли использовать анализ на основе суперкомпиляции для реализации анализа, аналогичного языку Rust, хотя бы для некоторых (адаптированных) программ на языке C.
Пример задачи для погружения в предметную область: расширение языка C в виде биекции на уровне синтаксиса.
Аналог clang modules на основе pkg-config:
#include <pthreads.h>; gcc -lpthread ↔ #import pthreads
Uniform function call syntax и импровизированные пространства имён на основе префиксов:
result = pthread_join(my_thread, &return_value)
↔
#alias pthread_ (join, ...)
result = my_thread.join(&return_value)
Биективное преобразование: открываем файл на языке C; редактируем его в «красивом» виде с модулями и UFCS; сохраняем обратно в C и получаем читаемый текст программы с минимальными необходимыми модификациями. Таким образом, расширение получается не отдельным языком, а способом представления и редактирования существующего кода.
Typed Assembly Language (G. Morrisett, 1998): язык ассемблера с продвинутой системой типов (System F).
К блокам кода на ассемблере добавляется описание системы типов — требования к содержимому регистров на момент входа в блок. Авторы не дошли до описания требований к содержанию памяти и эффектов системных вызовов.
На практике: reverse engineering — анализ программ, исходный код которых недоступен.
Forth — простой конкатенативный расширяемый язык программирования (советский независимый вариант с ВМК: язык ДССП). Особенности:
На практике: анализ самомодифицируемых программ, поиск уязвимостей в программах.
Исчисление конструкций (λ-исчисление с зависимыми типами) — формальная система, которая используется для описания свойств программ.
Исчисление конструкций используется в качестве базовой модели для систем автоматизированного доказательства теорем. Например, французская система Coq была использована для повторения доказательства теоремы о четырёх красках.
Задача разработки системы автоматизированного доказательства теорем на основе суперкомпиляции может быть поставлена для оценки выразительности системы типов.
Некоторые исследователи и практики программирования говорят о том, что компилятор — это база данных правил преобразования кода (хотя в отечественной терминологии правильнее было бы сказать «база знаний»). Есть несколько докладов с такими тезисами (например, Martin Odersky: Compilers Are (In-Memory) Databases, 2016 Scala World Keynote]), и попытки использовать эту точку зрения для ускорения работы компиляторов (Queries: demand-driven compilation, Rust Compiler Development Guide).
Для проверки гипотезы о том, что представление в виде базы данных является удобным для компилятора (т.е., например, сокращает объём и сложность кода по сравнению с классическими реализациями, не теряя при этом существенно в производительности, или получая при этом новые возможности) можно начать с реализации ассемблера (с прицелом на backend компилятора в будущем) в терминах реляционной модели.
В качестве стартовой точки нужно, с одной стороны, взять код одной из доступных реализаций ассемблера (NASM, FASM, VASM - с осторожностью, не свободный код, GAS - скорее всего, непонятный код) или backend компилятора (LLVM - скорее всего, большой и непонятный код, так что можно начать с QBE), и, с другой стороны, реализовать свой вариант ассемблера в терминах реляционной модели (например, на SQLite + Python) со следующей архитектурой.
В отдельной базе данных “Architecture definition” хранится описание системы команд процессора. Как минимум, там должны быть следующие сущности:
Что нужно сделать:
Кроме научных исследований, наш коллектив разрабатывает информационно-аналитическую систему «ИСТИНА»: https://istina.msu.ru/. Сейчас эта система работает в режиме «облака»: система существует в единственном экземпляре, и данные о научных результатах всех организаций, подключенных к ней, хранятся в центре обработки данных оператора системы. Такой «облачный» вариант удобен для верификации данных в системе. Однако по целому ряду других критериев — масштабируемость, контроль над данными, применимость системы в «закрытых» организациях, возможность доработки под нужды каждой из организаций — удобнее другая модель, в которой система разбита на большое количество равноправных независимых узлов, взаимодействующих на основе открытых протоколов. Такая модель называется децентрализованной.
На этом направлении есть как задачи, предполагающие большой объём программирования:
так и задачи, требующие создания новых математических моделей для решения вопросов доверия в децентрализованной системе:
Заметка про архитектуру децентрализованной наукометрической системы