https://www.cs.tau.ac.il/~shanir/progress.pdf Herlihy, Shavit, [2011] "On the nature of progress"

Ранее упоминалось, что упор для железнодорожной верификации делается на автоматизированных методах, что соответствует таким направлениям ФМ, как model checking и abstract interpetation. Посмотрим по довольно свежей статье-опроснику Beek et al, [2019] "Adopting Formal Methods in an Industrial Setting: The Railways Case", где и как они применяются.

Заметно, что большая часть усилий идёт на верификацию interlocking систем - это объясняется спецификой темы. Как видно уже из названия таких статей, как
Fantechi, Haxthausen, [2018] "Safety Interlocking as a Distributed Mutual Exclusion Problem", проблематику разрешения конфликтующих маршрутов сводят к уже существующим способам верификации многопоточных/распределенных систем. Т.е., рельсы и составы мыслятся как физический эквивалент потоков исполнения, где аналоги thread interference и race condition приводят к весьма печальным и зрелищным последствиям.

Самым же популярным инструментом, точнее семейством инструментов, выглядит уже упоминавшийся B-method - набор языков спецификации и модел-чекеров, разработка которых началась ещё в 80е в Англии и Франции. Из моделей можно экстрагировать код (в основном, кажется на Ada) - этот процесс называют refinement. B-method широко использовался французами в таких проектах как беспилотная 14я ветка парижского метро и автоматизированные шаттлы в аэропорту Шарль де Голь. По итогам проектов сложился некоторый консенсус по поводу надежности B-моделей, благодаря чему их теперь используют как низкоуровневый формализм, в который транслируют другие модели - например, сети Петри в
Sun, [2016] "Model based system engineering for safety of railway critical systems". Используются и другие инструменты проверки моделей, в частности, NuSMV и Promela/SPIN: https://github.com/jankofron/abz18-casestudy-spin.

В отличие от модел-чекинга, часто используемого для работы со спецификациями, абстрактная интерпретация используется для статического анализа кода. Для safety-critical систем таким кодом часто является C, получаемый из более высокоуровневой программы на датафлоу-языке типа Lustre, которая в свою очередь экстрагируется из Simulink-подобных диаграмм. Пример одновременного использования всех этих инструментов вместе с модел-чекингом можно увидеть в Ferrari et al, [2013] "The Metrô Rio case study". Также об этом рассказывает Xavier Leroy в своей наградной лекции 2016 года "In search of software perfection".

#railway

https://dalila.sip.ucm.es/isr2021/slides/Bruscoli.pdf Bruscoli, [2021] "An Introduction to the Deep Inference Methodology in Proof Theory"

В современной текстовой речи часто в ироническом смысле используются эрративы (нарочитые искажения синтаксиса а-ля "падонкафская речь") и анаколуфы (то же для грамматики, например закосы под "одесситский говор" со всякими "не делайте мне нервы"). Последний приём (также называемый "солецизм") использовался ещё древними греками. Интересно, что у них же было третье понятие для искажений семантики - т.е., ситуаций, ныне описываемые мемами типа "I don't think it means what you think it means" - так вот греки называли это варваризмом.

https://www.connectedpapers.com/

Визуализатор графа связности для научных статей

Написал заметку по статье о верифицированной императивной кодогенерации из полиэдральной модели: https://www.tg-me.com/plcomp/83

https://code.gouv.fr/ поисковик по опенсорсу французских государственных агентств

психиатр: булевалентности не существует, она не может тебе навредить
булевалентность:

Lemma bvalence (a b : bool) : (a <-> b) <-> a == b.
Proof.
case: a; case: b=>//; split=>//.
- by case=>/(_ isT).
by case=>_ /(_ isT).
Qed.

новый зулип по конструктивной математике: https://constructive-maths.zulipchat.com/

Майк Шульман анонсировал серию докладов "Towards Third-Generation HOTT" 14, 21 и 28 апреля: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Имеется в виду что первое поколение это "книжный HoTT", а второе - кубические теории. Аббревиатура гипотетического третьего поколения это сокращение от "Higher Observational Type Theory".

Доклады, увы, отменили.

Майкл Шульман выступит на другом семинаре: https://groups.google.com/g/homotopytypetheory/c/m3hQAKtypJs

(уже в PLT календаре 😊)

Нашел два интересных обзорных эссе о теории доменов в прошлогоднем бюллетене от британской группы по формальным методам BCS-FACS:

* Monahan, [2021] "Domain Theory - Revisited"
* Winskel, [2021] "Domain theory and interaction"

Первое эссе за авторством Монахана даёт обзор мотивации, контекста появления и основных идей теории доменов. Рассказывается о преодолении недоверия к нетипизированному лямбда-исчислению, поиске способов масштабирования и подходов к спецификации программ, о необходимости работы с частичными (из-за общей рекурсии) функциями.

Ключевая идея теории доменов - функции ЛИ соответствуют математическим функциям над особыми множествами (собственно, доменами, которые моделируют типы), упорядоченными по количеству содержащейся в них абстрактной информации, причем функции сохраняют этот порядок. Подобная структура функций позволяет конструировать неподвижные точки для них и таким образом моделировать рекурсию как предел нарабатывающего информацию процесса. Так впервые был выстроен топологический взгляд на вычисления, и информатика (точнее, теория языков программирования) оказалась полноценной математической теорией, а не просто "двиганием битов", что в свою очередь дало толчок развитию теорий типов и формальных семантик.

Эссе Винскеля более техническое и фокусируется на теме конкурентных и взаимодействующих вычислений. Начинается оно с введения в историю ТД с точки зрения её создателей, упоминает о создании LCF/PCF и ML, затем переходит к классическим проблемам ТД - работа с нондетерминизмом, проблема полной абстракции (конструкции в модели, для которых не существует синтаксиса). Пытаясь решить эти проблемы, теория доменов (и денотационная семантика в целом) перешла к созданию интерактивных моделей, в дальнейшем оформившихся в виде игровой семантики. С другой стороны, из-за проблем при работе с конкурентными программами, часть исследователей переключилась на алгебры процессов CCS/CSP с синхронизацией. Тем временем продолжение работ в рамках теории порядков привело к созданию понятия структуры событий (формализацию которых на Coq, кстати, можно найти тут).

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

Выложили записи всех трёх частей "Towards third generation HOTT":

* Part 1: Basic syntax (slides)
* Part 2: Symmetries and semicartesian cubes (slides)
* Part 3: Univalent universes (slides)

Андрей Бауэр выложил черновик лекций по реализуемости:

http://www.andrej.com/zapiski/MGS-2022/notes-on-realizability.pdf Bauer, [2022] "Notes on realizability"

Реализуемость можно понимать как более слабую/обобщенную версию соответствия Карри-Говарда, т.е. идеи о том что логические доказательства можно интерпретировать как программы - в случае реализуемости не обязательно тотальные или даже типизированные.

Shavit, [2011] "Data structures in the multicore age"

Относительно известная научно-популярная статья десятилетней давности одного из корифеев конкаренси о будущем многопоточного (библиотечного) программирования.

Начинается с мотивации законом Амдала о ботлнеке параллельных вычислений. Упоминает, что корректность в многопоточном сеттинге распадается на два аспекта: safety (относительно модели согласованности, например линеаризуемости) и liveness (условия прогресса - lock-free/wait-free и более экзотические). Также изменяются инструменты работы с complexity - добавляется модель stalls, нужно внимательно следить за contention. Делается предсказание, что развитие алгоритмов и структур данных пойдет по пути ослабления гарантий (кажется, спустя 10+ лет это до сих пор довольно нишевые вещи).

Основное время статья описывает в качестве примера процесс "ослабления" многопоточного стека на жаве, проходя несколько фаз:

1. стек под спинлоком - линеаризуем, не параллелен (deadlock-free), забивает шину из-за бесконтрольных спинов (обычно решается backoff-схемами)
2. lock-free стек - специализирует лок до CASа на голове стека
3. elimination backoff stack - убирает последовательный ботлнек, получая т.н. "дуальную" структуру - т.е. позволяя тредам оставлять "антиданные" (заявки) и передавать элементы напрямую без записи в стек, по прежнему линеаризуем
4. elimination tree - дуальность плохо работает в случае пакетов однотипных операций, поэтому можно ослабить согласованность до quiescent модели (иллюзия линейности только в периоды бездействия), разбив стек на несколько параллельных и прикрыв их балансировщиками
5. stack pool - в конечном счете проблемой является сама последовательная логика стека, поэтому дальнейшего роста быстродействия можно добиться, убрав балансирующую машинерию и превратив стек в тщательно подогнанную под архитектуру слабоупорядоченную структуру, которой, по мнению автора, должно хватать для большинства приложений

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

#concurrency

Papayannopoulos, [2020] "Unrealistic Models for Realistic Computations: How Idealisations Help Represent Mathematical Structures and Found Scientific Computing"

Научные вычисления (scientific computing / computational science), т.е. общие техники для всех вычислительных ветвей эмпирических наук, можно разделить на символьные и численные методы, в статье идёт речь о последних. Т.к. численные методы работают с непрерывными значениями (действительными/комплексными числами и их обобщениями), появляются вопросы сходимости, устойчивости и вычислимости алгоритмов над плавающей арифметикой (в частности проблема накопления ошибок округления). Для изучения этих вопросов нужен математический фреймворк вычислений над несчетными множествами, из наиболее популярных это BSS model (aka Real-RAM) и computable analysis (aka Type Two Effectivity), причем друг с другом они несовместимы. Статья посвящена разбору этих двух подходов.

CA/TTE - более фундаментальная и "низкоуровневая" теория, это разновидность матанализа, где сохраняется классическая теория, но дополнительно учитываются вычислительные представления объектов через бесконечные аппроксимации. Как правило, это делается через работу с некоторыми разновидностями машин Тюринга (с оракулом или более сложной машинерией репрезентаций). Её появление можно отследить к трудам Бореля, Банаха и Тюринга 1910-30х годов, где рассматривались вычислимые подмножества R (эта идея получила развитие в Марковской школе конструктивизма/синтетической вычислимости). Более поздние подходы ("Хагенская школа") перешли к рассмотрению всего R (ключевая идея TTE). В этой модели вычислимые функции должны быть непрерывными - как следствие, мы теряем возможность полноценно использовать "точечные" функции сравнения и округления (ср. https://twitter.com/andrejbauer/status/1400172747930718209).

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

Какой же фреймворк предпочтителен? BSS менее реалистична и хуже подходит для работы с ошибками округления и плохо обусловленными функциями, но тем не менее довольно популярна - она моделирует устойчивые алгоритмы (т.е. не вносит собственных ошибок) и позволяет работать с оценкой их сложности. Также BSS ближе к алгоритмам плавающей арифметики в том, что имеет фиксированную стоимость операций (в отличии от CA, где стоимость зависит от входа). С другой стороны, CA подходит для более глубоких вопросов вычислимости (в т.ч., например, квантовой) и работы с "плохо ведущими себя" функциями, но создает больше проблем при анализе стоимости и работе с хорошо изученными численными алгоритмами.

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

#realnumbers

Bornat, [2009] "Separation logic and concurrency"

Программирование это комбинация механических вычислений и формальной логики. Как правило, каждый новый формализм используется программистами для увеличения объема выразимых программ, а не корректности (насчет баланса между выразительностью и непротиворечивостью см также например https://twitter.com/aspiwack/status/1394012829464866819). Многопоточные вычисления - самая сложная разновидность программирования, и тут, как всегда, теория информатики одновременно и плетется за практикой, и обгоняет её.

Фундаментальная проблема конкаренси - синхронизация процессов, обменивающихся информацией, сама по себе является обменом информацией, т.е. мы как бы заперты внутри этой игры. Дейкстра предложил использовать примитивы синхронизации для структурирования параллельных программ, и задача корректности разделилась на проблемы верности того, что происходит при успешной синхронизации (обычно формулируемые как safety) и верности самой синхронизации (часто выражающиеся в форме liveness-свойств).

Конкурентная сепарационная логика (CSL) классически занимается safety, т.е. частичной корректностью многопоточной программы относительно спецификации и модели консистентности. Её предшественник это в первую очередь метод Owicki-Gries 70х - расширение аксиоматической логики Хоара на программы с примитивами параллельной композиции и синхронизации, основанное на доказательствах non-interference. Метод OG популяризировал идеи ресурсных инвариантов и вспомогательных (ghost) переменных. В 80х Cliff Jones доработал метод OG до rely-guarantee, добавив два одноименных условия к пред- и постусловиям. Одно из слабых мест обоих методов - работа с алиасингом, т.е. тем фактом, что одна ячейка памяти может индексироваться разными символьными выражениями. Для решения этой проблемы и была придумана сепарационная логика - параллельная ветка развития логики Хоара, где под "сепарацией" понимается двухместный предикат над ячейками, гарантирующий неравенство их адресов. Это позволяет иметь т.н. frame-правило (терминология, кстати, заимствована из ИИ), позволяющее отбрасывать "нерелевантные" логические условия, т.е. работать только с тем состоянием, которое напрямую затрагивается рассматриваемой частью программы.

Как и метод OG, CSL добавляет примитивы параллельной композиции и критических секций вида with r when B do C (для которых подразумевается наличие более низкоуровневой имплементации). r - так называемый ресурс, для каждого из которых в логике вводится свой инвариант (также идея OG). Статья показывает пример доказательств для программ с семафорами, далее переходит к механизму permissions, нужному для отслеживания read-only вспомогательных переменных (существуют альтернативы этому механизму - subjective auxiliary state в FCSL и ghost objects/higher-order ghost code в Iris). Далее демонстрируется доказательство для readers-writer lock (запрет на гонку между чтением и записью) на семафорах, с использованием ghost ticket трюка.

Последняя секция посвящена доказательству для неблокирующего алгоритма 4-slot авторства Hugo Simpson - алгоритм реализует wait-free single-reader single-writer atomic register. Доказательство выполнено "а-ля моделчекинг", с явным перечислением состояний в инварианте. Было бы неплохо иметь алгоритмическую теорию ресурсов, которую мы могли бы использовать в компиляторах, говорит нам статья, и завершается оптимизмом насчет грядущей инкоропорации идей rely-guarantee и темпоральной логики в CSL.

#concurrency

https://github.com/thery/FlocqLecture

Упражнения на работу с действительными числами и плавучкой в Coq с библиотекой Flocq - неравенства, режимы округления, форматы, лемма Стербенца, IEEE754.

#realnumbers