Covalue

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

www.group-telegram.com/sg/covalue.com/58

1.7K viewsedited  Jul 22, 2022 at 13:44

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