tgoop.com/covalue/58
Last Update:
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
BY Covalue
Share with your friend now:
tgoop.com/covalue/58