20.10.2020 14:07:37 |
Автор: Оглавление:
- Cyclone
- C++, владение и псевдонимы
- Rust
- Midoris M#
- Pony
- Cone
- Резюме
В 2001 году Джим Тревор (AT&T Research) и Грег Моррисетт (Cornell) запустили совместный проект по разработке безопасного диалекта языка программирования C как развитие более ранних работ над Типизированным Ассемблером. После пяти лет напряженной работы и нескольких опубликованных научных работ, команда (в том числе Дэн Гроссман, Майкл Хикс, Ник Свами и другие) выпустила Cyclone 1.0. А затем разработчики занялись другими делами.
Мало кто слышал о Cyclone, и почти никто им не пользовался. И все же, когда вы бросаете правильный камень в подготовленный пруд, то вода еще долго продолжает расходиться кругами. Cyclone был большим, хорошо обработанным камнем; и пульсации его духа, а также те новшества, которые в нем были впервые выделены, продолжают распространяться нетривиальными способами.
Перед тем, как рассказать эту историю, предупреждаю: Инновации и влияние это сложный социальный процесс. Ничего нового не возникает в вакууме. Тысячи людей каждый год бросают в пруд новые интересные им камни, под влиянием ранее уже брошенных. Но ни одна статья не может охватить всю эту хаотическую рябь целиком.
Для того чтобы этот рассказ был целостным и удобочитаемым, я сосредоточусь на определенных темах: прогрессе в эволюции статической безопасности и применении линейности в управлении памятью с конкурентным доступом к ней, что выражено в нескольких выбранных мейнстримных ("императивных") языках программирования. Это означает, что тонны актуальных и важных подробностей во влиятельных академических языках и исследованиях останутся без должного внимания. Не позволяйте моим писательским недостаткам ввести вас в заблуждение ввиду упрощенного понимания причины и следствия. Вместо этого проявите любопытство, изучите исторические записи и оцените вклад столь многих первопроходцев.
Cyclone
В конце 20-го века системное программное обеспечение обычно создавалось с использованием С (или "до-современного" С++). Поскольку их семантика близко отражает способ использования CPU, эти языки генерируют экономичные, высокопроизводительные системы. Цена, которую платят за такую эффективность, это риск возникновения ошибок безопасности, таких как переполнения буфера, что делает наши критические системы уязвимыми для вредоносных субъектов.
Целью команды Cyclone было создание языка, совместимого с C, который был бы, по крайней мере, столь же быстрым и экономичным, но гораздо, гораздо более безопасным. Их понятие безопасности было радикальным для своего времени: небезопасные программы должны быть сложны в написании, невозможны для компиляции и паниковать, когда нарушения безопасности встречаются во время выполнения.
Уязвимости, подлежащие вымиранию, включали: переполнение буфера, разыменование нулевых указателей, use-after-free, висячие указатели, double free, атаки с использованием форматных строк printf, использование неинициализированных переменных, небезопасные приведения типов, неопределенные возвраты функций, goto на другую область видимости, и нетегированные union'ы.
Основное оружие для повышения безопасности (и универсальности) было выбрано в результате укрепления печально известной слабой системы типов C посредством умелого применения достижений техник из ML, Haskell, и опубликованных исследований, в частности:
- Алгебраические типы данных. Хотя C поддерживает сум-типы с помощью struct, использование union для сум-типов может быть небезопасным. Вместо этого, Cyclone вводит объединения фиксированного размера с тегами, типы данных переменного размера и сопоставление паттернов. Cyclone также поддерживает кортежи, позволяя функциям возвращать несколько значений.
- Кванторные типы. Cyclone поддерживает параметрический полиморфизм (генерики) для функций и типов. Несмотря на то, что эта функция ограничена для типов размером в слово и не может мономорфизоваться, она достаточна для поддержки коллекций с обобщенными (боксовыми) типами. Cyclone также поддерживает абстрактные, экзистенциальные типы, со схожими ограничениями. Подобно трейтам, они позволяют использовать метод-подобные функции для различных базовых типов.
- Управление памятью на базе регионов. В основу Cyclone была положена фундаментальная работа Тофте и Талпина про доказательства выведения регионов в середине 1990-х годов. Как реализовано в ML Kit (с Биркедалом и другими), анализ программы позволяет заменить использование сборки мусора (GC) памяти более быстрыми, вложенными регионами памяти (аренами). Сопутствующая работа Aiken применяется для арен и управления памятью с подсчетом ссылок для C. Команда Cyclone улучшила эти методы, заменив перекрестно-функциональные выкладки явными аннотациями регионов. Важно отметить, что они обогатили эту схему для поддержки неслыханного ранее разнообразия безопасных, автоматических стратегий управления памятью: регионы арен (включая арены первого класса), с подсчетом ссылок, трассировка GC (с использованием Boehm), и то, что они назвали уникальным (unique) регионом.
- Линейные/аффинные типы. Уникальный регион Cyclone является полезным приложением работы Жирара по линейной логике конца 1980-х годов, усовершенствованной позже Вадлером, а затем Уолкером. Гарантируя, что выделенная память всегда будет иметь только одного владельца (ссылку на него), мы получаем безопасное, детерминированное управление памятью без затрат на ведение бухгалтерского учета GC во время выполнения. Управление памятью с подсчетом ссылок также более эффективно в случае, если оно построено с использованием линейной логики. Тем не менее, линейная логика (и регионы) усложняет язык с точки зрения мув-семантики и кванторных типов, с чем команде Cyclone пришлось столкнуться.
Указатели потребовали большого объема работ, чтобы сделать их безопасными:
- Нулевые указатели. Циклон устранил так называемую "миллиард долларовую ошибку" Тони Хоара, предложив выбор. Вы можете определить указатели как ненуллабельные (например, int @x) и использовать их свободно и безопасно. Или, если вам все-таки нужен нуллабельный указатель, компилятор не даст вам его разыменовать до тех пор, пока вы сначала не покажете, что он не нулевой.
- Толстые и ограниченные указатели. Для защиты от переполнения буфера Cyclone предлагает "жирные" указатели (char ?), которые хранят точный размер данных вместе с указателем. Арифметика указателей разрешена, но любая попытка доступа к элементам за пределами границ приводит к ошибке во время выполнения. Ограниченные указатели предлагают схожие возможности несколько по-другому.
- Безопасные для памяти указатели. Для обеспечения доступа указателей только к действительным, живым данным, тип указателя может быть аннотирован регионом, из которого получен его объект в памяти. Эта аннотация гарантирует, что объект освобождается только по истечении срока действия последнего используемого указателя на этот объект. С помощью анализа потока данных также обеспечивается безопасность указателей на данные, выделенные на стеке.
- Полиморфные указатели. При таком большом количестве аннотаций типов для указателей, безопасность типов может заставить нас дублировать код (или использовать генерики) для каждого возможного варианта указателя, передаваемого в функции. Cyclone преодолел эту проблему удобства, поддерживая полиморфные типы указателей, которые совмещают самые разнообразные типы указателей.
Можно сказать больше о расширениях безопасности Cyclone (например, обработка исключений и явное присвоение), но я думаю, что вы поняли суть. Команда "Циклона" добросовестно и скрупулезно занималась поиском и минимизацией уязвимостей безопасности. Они даже проработали стратегию статического типа, чтобы сделать многопоточность безопасной, используя блокировки потоков и thread-local данные.
Примечательно, что все эти улучшения в области безопасности и универсальности были разработаны с учетом сохранения как можно большей обратной совместимости с C. По понятным причинам, они хотели сделать путь к безопасности как можно более безболезненным для существующих программистов на C. Их работы демонстрируют полезные примеры, когда код на C был портирован на Cyclone, с результатами бенчмарков, иллюстрирующими, что безопасность не обязательно влечет за собой резкое снижение производительности.
C++, владение и псевдонимы
Прежде чем двигаться вперед по временной шкале, я хочу противопоставить безопасное управление памятью Cyclone с C++. Управление памятью в C++ основано на двух ключевых возможностях, доступных до 1990 года: шаблоны (более универсальные и сложные, чем типичные генерики) и получение ресурса это инициализация (RAII). Используя RAII, программа может получить и использовать некоторый локальный к блоку ресурс, и ожидать, что компилятор автоматически уничтожит этот ресурс в конце этого блока. Однако RAII не работает с объектами, динамически выделяемыми с помощью new.
Для устранения возможности утечки из-за забытых delete, стандарт 1997 года представил auto_ptr, первый "умный" указатель. Эта шаблонная функция, действует как указатель, при этом RAII все еще уполномочен обеспечивать автоматическое удаление владеемого объекта. Еще лучше было то, что auto_ptr был линейно-подобен [1]: Только одна переменная принадлежала указанному ресурсу. Присвоение передает право собственности.
Тем не менее, auto_ptr имел фатальный изъян дизайна, ограничивая его полезность. В 2002 году, вдохновленный Эндрю Кёнигом из Bell Labs, Говард Хиннант написал "Предложение добавить семантику перемещения в C++". Ключевым мотивом стала производительность: неразрушающее копирование указателя намного дешевле, чем любое глубокое копирование. Результатом стандартного процесса стал unique_ptr, заменивший auto_ptr в техническом отчете 2005 года (TR1) и, в конечном итоге, в C++11. В том же стандарте был введен shared_ptr, умный указатель с подсчетом ссылок, основанный на практиках конца 1990-х годов.
Таким образом, к 2006 году различные тенденции привели к тому, что как Cyclone, так и C++ поддерживали одни и те же две формы автоматического управления памятью: с одиночным владением (линейное) и с подсчетом ссылок. При этом управление памятью Cyclone, основанное на регионах, было более универсальным (так как оно также поддерживало арены и трассирующий GC) и гораздо более безопасным.
Когда речь зашла о строгой безопасности памяти, команда Cyclone располагала более глубокой практикой и академическими исследованиями, для продвижения вперед. Кроме влияний, о которых я упоминал ранее, они опирались на типы псевдонимов (Smith and Walker, 2000, как реализовано в Typed Assembly Language), использование подсчета ссылок в Objective C, а также на влияющую Логику разделения (рус.ссылка) (Reynolds, O'Hearn, Pym, 2000-2002). Как говорит Грег Моррисетт: "Вклад Cyclone заключался в том, чтобы найти общий фреймворк, в который можно было бы вложить кучу разных вещей".
Обработка "заимствованных" ссылок иллюстрирует разрыв в безопасности между Cyclone и C++. Использование функции get() на умных указателях С++ возвращает псевдоним указателя. Так как Си++ их не отслеживает, чтобы гарантировать, безопасность псевдонимов для использования, не проблема ошибочно использовать указатель после того, как объект, на который он указывает, был освобожден.
В Cyclone также имеется возможность создать полиморфный указатель, заимствованный из любого регионального указателя. В отличие от C++, Cyclone тщательно отслеживает время жизни области видимости каждого заимствованного указателя, часто неявно. Сложный анализ на этапе компиляции времени жизни региона (включая субтипирование региона) делает невозможным для любого заимствованного указателя пережить время жизни его владельца. Таким образом, заимствованные указатели Cyclone всегда безопасны в использовании.
Rust
В 2006 году, в том же, когда команда Cyclone закрыла лавочку, Грейдон Хоар (в то время сотрудник Mozilla) начал работу над языком программирования Rust в качестве личного проекта. Три года спустя началось корпоративное спонсорство, финансирование и укомплектование кадрами, кульминацией которого стала стабильная версия 1.0 в 2015 году.
Если вы знаете Rust, моя краткая информация о безопасности и возможностях Cyclone должна звучать жутко знакомо. Rust это надежный, реально работающий язык системного программирования, обеспечивающий достижение практически всех целей Cyclone.
Rust ссылается на Cyclone, C++ и SML/OCaml в числе многих своих предшественников. Несколько членов основной команды, таких как Нико Мацакис, Аарон Турон и Дэйв Герман, также привнесли богатые академические исследования в свой выбор дизайна.
Rust так же безопасен, как и Cyclone, во всех тех же отношениях и часто использует в значительной степени схожие методы. Тем не менее, различия между языками легко обнаруживаются:
- Синтаксис Rust скорее привычный для C/C++, чем совместимый.
- Генерики и трейты более гибкие, схожие с языками ML-семейства. Их использование является ключевым для основных возможностей языка (например, Option, Result и "умные" обертки указателей, такие как Rc и Mutex).
- Borrowed References более универсальны, поддерживают такие функции, как статические мутексы (напр, &mut), нелексическое время жизни, использование заимствования для получения блокировок в области видимости, а также сахар с удалением явных указаний лайфтаймов. При этом интригующе отметить, что полиморфные переменные Cyclone `r (часто используемые в качестве региональных аннотаций) напоминают аннотацию времени жизни Rust 'а.
- Управление памятью. В связи с тем, что Rust принял владение как определяющую характеристику языка, его поддержка множественных стратегий управления памятью более ограничена, чем у Cyclone. Как и в случае с C++, техники однопользовательского владения (Box) и подсчета ссылок (Rc) являются доминирующими. Хотя и существуют пакеты Rust для трассирующего GC и арен, они ограничены по сравнению с поддержкой Cyclone для регионов, особенно в отношении безопасных арен первого класса.
- unsafe. Команда Rust мудро осознала, что им необходимо предложить лазейку, позволяющую программистам писать безопасную, производительную логику, которую компилятор не может проверить как безопасную. Ряд важных библиотек полагаются на эту существенную особенность.
Важно, что Rust пошел на полную линейность, выходя далеко за рамки управления памятью с одним владельцем. Создатели хотели бороться с фундаментальными проблемами, возникающими при предоставлении общего, изменяемого доступа к значениям.
В большинстве основных языков программы могут легко иметь множество ссылок на один и тот же объект, каждая из которых способна изменять (мутировать) его состояние. Это может вызвать проблемы. Отладка и сопровождение значительно сложнее, когда вы не знаете, где возникают изменения, особенно когда неожиданно нарушаются инварианты. Неограниченная общая мутируемость открывает двери к гонкам данных не только для многопоточных программ, но иногда и в однопоточном контексте. При правильном использовании блокировки (как и предполагалось в Cyclone) могут вылечить гонки данных, но часто они несут значительные затраты на пропускную способность.
Языки десятилетиями искали лучшие мутирующие решения с псевдонимами. Ограниченные типы Ada, restrict в C, строгие правила псевдонимов в C++, ограничения без псевдонимов для аргументов в Fortran, гибкая защита псевдонимов для Java, функциональные языковые ограничения мутируемости, академическая работа над дроблением прав и (опять-таки) логикой разделения.
Как оказалось, линейная логика это не просто ценная стратегия управления памятью. Она также является ценной стратегией и для псевдонимов и гонок данных. В 1992 году язык Clean ввел уникальные типы для обработки операций ввода-вывода и деструктивных обновлений. Более поздние языки, такие как ATS, Alms и Mezzo, исследовали эту идею по-разному. Команда Rust находилась в контакте с этими командами и в то же время была в курсе многочисленных исследований, проводимых в настоящее время.
Полученная в результате модель владения Rust в значительной степени основана на идее взаимного исключения, согласно которой либо имеется единственная мутирующая ссылка на объект, либо, допустимы множественные иммутабельные ссылки. Соблюдение этого ограничения устраняет ранее упомянутые проблемы и делает безопасным передачу изменяемых данных из одного потока в другой без блокировок. Экстенсивный подход Раста к бесстрашному параллелизму опирается не только на это, но этот аспект вносит важный вклад.
И, если вы действительно хотите иметь общий и мутируемый доступ, это тоже возможно, используя механизмы синхронизации, основанные на блокировках (например, Mutex) или даже безблокировочную, но несколько ограниченную Cell.
Midori M#
Midori это исследовательский/инкубационный проект компании Майкрософт, который длился с 2007 по 2014 год. Его целью было коммерческое внедрение Singularity, операционной системы, построенной на более надежном фундаменте, чем горы небезопасного Си и Си++ кода.
Для достижения своих целей, параллельности, безопасности и производительности команда создала новый диалект языка программирования C# под названием M#. Поздние возможности C#, такие как срезы и async/await, имели свое происхождение в M#. Несмотря на некоторое упорное стремление, они не пошли по стопам Cyclone (и Rust'а) в отношении управления памятью; M# остался языком со сборкой мусора (хотя и там были внесены значительные изменения).
Как и в случае с Cyclone и Rust, работа над Midori и M# была богато вдохновлена предшествующим творчеством и исследованиями: C++ const, анализ псевдонимов, линейные типы, монады, эффекты типов, регионы, логика разделения, типы уникальности, проверка моделей, современные C++, D, Go и Rust. Несколько человек из команды Midori знали о Cyclone. Колин Гордон, зная о работе Дэна Гроссмана над Cyclone, последовал за ним в Университет Вашингтона в качестве аспиранта/доктора, где сделал важный вклад в качестве стажера в команде Midori. Мануэль Фендрих, чья ранняя работа вдохновила его на "заимствование", взятое из Cyclone, внес ключевой вклад в проект Singularity. Дэвид Тардити, другой участник проекта Singularity/Midori, сейчас работает с Майклом Хиксом (команда Cyclone) и другими участниками проекта Microsoft'а Checked C, чьи цели перекликаются с целями Cyclone.
Команда Midori была так же сосредоточена на "трех китах безопасности", как и Cyclone и Rust. Они использовали аналогичные механизмы безопасности, такие как срезы (для решения проблемы выхода за границы), тегируемые union'ы и заимствованные ссылки. Они также тестировали в работе дополнительные механизмы, включая изолированные процессы, возможности объектов, контракты, работу с исключениями и возможности ссылок (Прим.пер.Это такой термин, со смыслом прав доступа).
Возможности ссылок M# обогащают полезность уникальных ссылок. M# помечает все ссылки одной из четырех безблокировочных ссылочных возможностей (квалификаторов прав доступа): изолированные, записываемые, неизменяемые и читаемые. Несмотря на то, что все они безопасны в гонке данных, каждая из них включает (и ограничивает) возможности своей ссылки по-разному. Ограничение, налагаемое isolated, линейность: может быть только одна.
При всех своих преимуществах уникальные (линейные) ссылки имеют существенное ограничение. Используя только уникальные ссылки, можно построить только иерархические (древовидные) структуры данных. Почти все циклические структуры данных должны допускать несколько ссылок на один и тот же объект, что недоступно с помощью уникальных ссылок. Это ограничение, а также деструктивные ограничения семантики перемещения надо держать в уме, расхваливая достоинства управления памятью с одним владельцем и уникальными ссылками.
В свете этого ограничения представьте себе, что мы имеем изолированную (уникальную) ссылку на некую циклическую структуру данных, реализованную внутренне с использованием псевдонимных ссылок. Безопасно ли перемещать всю эту структуру данных из одного потока в другой? Определенно да, если псевдонимы указывают на неизменяемые значения. Однако, если псевдонимические ссылки являются мутируемыми (writable), мы должны быть более осторожны. Перемещение безопасно только в том случае, если все изменяемые ссылки на каждый объект в этой структуре данных, по сути, перемещаются вместе. Если мы не можем гарантировать, что перемещаемая структура данных "внешне изолирована", мы подвергаемся опасности возникновения гонки данных, так как несколько потоков могут получить мутируемые ссылки на одни и те же объекты.
M# способен гарантировать внешнюю изоляцию во время компиляции, используя два механизма ссылочных возможностей. Первый в виде "сужения окна", при которой право доступа по какому-либо полю объекта может быть понижено на основании права доступа по ссылке, используемой для доступа к этому объекту. Например, иммутабельная ссылка на объект не может быть использована для изменения значения, на которое указывает поле-ссылка (указатель внутри) этого объекта, даже если тип этого поля мутабелен.
Вторым механизмом является способность M# навязывать (принуждать), а затем "восстанавливать" возможности. Восстановление позволяет временно сделать изолированную ссылку доступной для записи (или неизменяемой) для некоторой ограниченной области видимости, после чего можно безопасно восстановить ее исходное изолированное состояние. В то время как она является записываемой, мы можем мутировать и дополнять структуру данных, на которую указывает ссылка, дополнительными объектами. Чтобы сохранить внешнюю изоляцию, логика внутри области видимости восстановления ограничена таким образом, что она может использовать только immutable либо isolated ссылки, приходящие из-за пределов области видимости (и не записываемые или только для чтения).
Помимо возможности межпоточных перемещений мутируемых, циклических структур данных, механизм принуждения и восстановления M# обладает и другими преимуществами. Его также можно использовать для безопасного (и мутируемого) построения циклических структур данных, которые в конечном итоге переходят в неизменяемые. В конечном итоге, ссылочные возможности Midori безопасно дают многопоточным программам дополнительные преимущества в производительности и универсальности структур данных за счет использования уникальных ссылок.
Pony
В 2014-5 годах Сильван Клебш и его команда разработали и создали компилятор для актор-ориентированного языка Pony. Здесь было использовано слишком много взаимосвязанных идей, в том числе и наработки по актор-процессам из Erlang. Выбор дизайна еще раз продемонстрировал, что производительность и возможности не обязательно должны быть врагами с безопасностью.
Pony полон интересного функционала и архитектурных решений, таких как: актеры и поведение, неявная передача сообщений, интерфейсы против трейтов, а также необычный гибридный подход к сбору мусора, использующий как подсчет ссылок, так и трассировку. Как и M#, Pony поддерживает возможности объектов и ссылок. Pony усовершенствовал, обогатил и переименовал свой набор ссылочных возможностей, уточнив, что разрешено и что запрещено. Пони также дал возможность инстанцировать дженерики с уникальной ссылкой.
Cone
Несмотря на то, что у меня не было ролей в рассказанных до сих пор историях, они представляют для меня большой личный интерес, благодаря моей работе над языком Cone.
Два года назад я внимательно изучал язык Rust и Pony в надежде научиться инновационным стратегиям безопасного и эффективного управления памятью и параллелизмом. Я был в восторге от того, что я обнаружил, и в итоге задокументировал свои мысли о том, как расширить их методы для поэтапного управления памятью. В частности, я хочу объединить подход Rust к владению и заимствованию ссылок с ссылочными возможностями (разрешениями) Pony в поддержку более универсального, безопасного, производительного использования памяти.
В то время я понятия не имел, насколько актуальной была новаторская работа Cyclone до появления Rust and Pony. Это изменилось несколько месяцев назад, когда Аарон Вайс прислал мне ссылки на пару интересных академических статей. Одно вело к другому, и вскоре я погрузился в историю Cyclone и связанные с ним работы в мельчайших деталях.
Теперь я понимаю, что Cone преследует те же цели, что и Cyclone, не только с точки зрения безопасности, согласованности и производительности, но и с точки зрения универсальности управления памятью. Долгое время одной из моих целей было облегчить программисту выбор метода управления памятью между управлением ею с использованием единственного владельца, подсчётом ссылок, трассирующим GC, арен или пулов, чтобы это наилучшим образом отвечало требованиям программы к производительности и структуре данных. Теперь, вдохновившись Cyclone, добившегося этого 15 лет назад, я ищу возможность добавить к этому списку арены 1го класса. Я не менее благодарен за то, что смог использовать многие инновационные, усовершенствованные функции, впервые появившиеся в более поздних языках.
Резюме
В конце 1990 года Филипп Вадлер в работе "Линейные типы могут изменить мир!", заключил: "требуется больше практического опыта, прежде чем мы сможем оценить вероятность того, что линейные типы изменят мир". Так много языков дало нам этот практический опыт. И этот опыт, несомненно, меняет то, как мир программирования строит программы для обеспечения безопасности и производительности.
Теперь, когда языки, ориентированные на безопасность, производительность и линейность, становятся все более общепринятыми и успешными, мы все чаще видим, что существующие (и новые) языки приобретают схожие возможности. Язык программирования D планирует поддерживать владение и заимствование (Прим.пер.Уже вышло в релиз). Nim изучает нечто подобное (Прим.пер.Отложено, см.177), ссылаясь на документ Google/IBM, в котором большая часть технологии основана на Cyclone.
Я уверен, что на этом история не закончится. И я за это выражаю благодарность многим людям, включая команду Cyclone, которая так много сделала, запустив этот пробный шар.
Я благодарен Грегу Моррисету, Грейдону Хоару, Майклу Хиксу, Колину Гордону и Дэну Гроссману за их бесценные отзывы на более раннюю версию этой статьи, открывшие мне глаза на то, как много людей внесли свой вклад в основополагающие идеи, которые позволили создать эти языки.
Об авторе
Jonathan Goodwin 3D Веб евангелист. Автор языков программирования Cone и Acorn.
[1] С++ был не первым. Пятью годами ранее (1992), Linear Lisp продемонстрировал использование линейной логики в качестве решения для сбора мусора.
Категории: 
