Безопасность памяти на основе типов без ручного управления памятью или сборки мусора во время выполнения?

Допустим, мы хотели создать типичный, чисто функциональный язык программирования, такой как Haskell или Idris, который предназначен для системного программирования без сборки мусора и не имеет времени выполнения (или, по крайней мере, не более, чем «среды выполнения» C и Rust). То, что может работать более или менее на голом металле.

Каковы некоторые параметры статической безопасности памяти, которые не требуют ручного управления памятью или сборки мусора во время выполнения, и как можно решить проблему, используя систему типов чистого функционала, подобного Haskell или Idris?

Грубо говоря, есть две основные стратегии безопасного ручного управления памятью.

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

   Это то, что делает Rust (он использует систему аффинных типов). Если вы интересуетесь теорией в стиле Rust, одна из лучших статей для чтения - L3 Ахмеда и его коллег: линейный язык с локациями . Кроме того, упомянутое Дамиано Мазза исчисление LFPL также является линейным, имеет полный язык, полученный из него на языке RAML .

   Если вы заинтересованы в верификации в стиле Idris, вам следует взглянуть на язык ATS Xi et al., Который является языком стиля Rust / L3 с поддержкой проверки на основе индексированных типов в стиле Haskell, только сделав доказательство нерелевантным и линейным, чтобы дать больше контроль над производительностью.

   Еще более агрессивно зависимый подход - это язык F-star, разработанный в Microsoft Research, который является полностью зависимой теорией типов. Этот язык имеет монадический интерфейс с предварительными и постусловиями в духе теории типов Hoare Наневского и др. (Или даже моего собственного Интегрирования линейных и зависимых типов ) и имеет определенное подмножество, которое может быть скомпилировано в низкоуровневый код C - на самом деле, они уже отправили проверенный криптографический код как часть Firefox!

   Чтобы было ясно, ни F-star, ни HTT не являются линейно типизированными языками, но индексный язык для их монад обычно основан на логике разделения Рейнольда и О'Хирна , которая является субструктурной логикой, связанной с линейной логикой, которая имела большой успех как язык утверждений для логики Hoare для указательных программ.

2. Второй подход заключается в том, чтобы просто указать, что делает сборка (или какой-либо низкоуровневый IR, который вы хотите), а затем использовать некую форму линейной логики или логики разделения, чтобы напрямую рассуждать о ее поведении в помощнике по проверке. По сути, вы можете использовать корректор или язык с зависимой типизацией в качестве очень интересного макроассемблера, который генерирует только правильные программы.

   Дженсен и др. Высокоуровневая логика разделения для низкоуровневого кода является особенно чистым примером этого - она ​​создает логику разделения для сборки x86! Тем не менее, есть много проектов в этом направлении, таких как Проверенный программный инструментарий в Принстоне и проект CertiKOS в Йельском университете.

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

Линейные типы и логика разделения великолепны, но могут потребовать немного усилий программиста. Написание безопасного связного списка в Rust может быть довольно трудным, например.

Но есть альтернатива, которая требует гораздо меньших усилий программиста, хотя и с менее строгими гарантиями. (Довольно старый) поток работы - гарантировать безопасность памяти, используя (как правило, стек) областей. Используя вывод области, компилятор может статически решить, в какую область следует поместить часть выделенных данных, и освободить область, когда она выходит из области видимости.

Вывод области доказуемо безопасен (не может освободить доступную память) и требует минимального вмешательства программиста, но он не является «полным» (то есть он все еще может утечь память, хотя определенно намного лучше, чем «ничего не делать»), поэтому обычно он объединяется с GC на практике. MLtonКомпилятор ML Kit использует регионы для устранения большинства вызовов GC, но у него все еще есть GC, потому что в противном случае он все равно будет пропускать память. По словам некоторых из первых пионеров в области, логический вывод региона не был изобретен для этой цели (я думаю, что это было сделано для автоматического распараллеливания); но оказалось, что его можно использовать и для управления памятью.

В качестве отправной точки я бы сказал, что Маддс Тофте и Жан-Пьер Талпин написали статью «Внедрение типизированного λ-исчисления при вызове по значению с использованием стека регионов». Для большего количества работ по выводу региона, посмотрите другие работы М. Тофте и Ж.-П. Талпин, некоторые из работ Пьера Жувело, а также серия работ Грека Моррисетта, Майка Хикса и Дэна Гроссмана о Циклоне.

Тривиальная схема для «голых железных» систем - просто запретить все выделения памяти во время выполнения. Помните, что даже для malloc/freeпары C требуется библиотека времени выполнения. Но даже когда все объекты определены во время компиляции, они могут быть определены типобезопасным способом.

Главная проблема здесь - фикция неизменяемых значений на чисто функциональных языках, которые создаются во время работы программы. Реальные аппаратные средства (и, конечно, системы с «голым железом») полагаются на изменяемую оперативную память, которой мало. Во время выполнения реализации функционального языка на практике динамически выделяется ОЗУ по мере создания новых «неизменяемых» значений, а сборщик мусора собирает их, когда «неизменяемое» значение больше не требуется.

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