На днях мне захотелось узнать, чем занимается создатель Python Гвидо ван Россум, и поэтому я прочитал несколько его последних статей в блоге. Я не был уверен, чего ожидать: может быть, самодовольства по поводу того, что Python, по некоторым данным, стал самым популярным языком программирования в мире? Или, возможно, разглагольствования о людях, жалующихся на переход на Python 3 — то, что я счастливо пропустил, поскольку последний раз писал строчку о Python несколько лет назад. Вместо этого я с удивлением наткнулся на свою любимую тему: параллелизм.
Самая последняя статья, описывающая трудности Python BDL с реализацией семафора, используемого в asyncio, привлекла мое внимание и вдохновила меня на выполнение собственного небольшого упражнения TLA+: моделирование семафора Гвидо.
Проблема
Следуя метафоре об очередях в очень эксклюзивный ресторан быстрого питания в Силиконовой долине — возможно, намекая на столовые различных технологических компаний, где Python BDL нашел работу на протяжении многих лет, — Гвидо покорно отмечает: Оказывается, что реализация примитивов синхронизации сложна. Это, добавляет он, стало неожиданностью, потому что в asyncio одновременно может выполняться только одна задача, а переключение задач происходит только при ожидании —отличное наблюдение о том, что сложность параллелизм не относится к параллельному выполнению как таковому.
Возможно, иронично, что Гвидо, гражданин Нидерландов, боролся со своей реализацией семафора целых 62 года после того, как Эдсгер Дейкстра — еще один голландец — изобрел программный эквивалент железнодорожного сигнала.
Семафор используется для управления доступом к (набору) ресурсов, совместно используемых одновременно выполняющимися процессами (вы можете заменить «процесс» на любую единицу параллелизма). Он управляет счетчиком, изначально установленным равным количеству доступных ресурсов. Этот счетчик уменьшается при получении общего ресурса процессом и увеличивается при повторном освобождении этого ресурса. Процесс, пытающийся получить ресурс, когда он недоступен (когда счетчик равен нулю), добавляется в очередь до тех пор, пока он не станет доступным.
Хотя некоторые трудности, описанные в статье Гвидо, по-видимому, относятся к основанной на фьючерсах среде выполнения asyncio (нотация await не упрощает рассуждения о параллелизме), BDL признает его «борьбу за визуализацию состояния семафора». В частности, Гвидо упоминает, что «ошибка справедливости возникла из-за того, что acquire() использовала ярлык, когда уровень семафора (количество открытых таблиц) отличен от нуля. Он не должен этого делать, когда в очереди еще есть фьючерсы».
Статья завершается несколькими математическими определениями и инвариантами, которые БДЛ придумал в конце концов и которые, по-видимому, поддержали его рассуждения, предоставив план фактической реализации.
Это была бы прекрасная возможность использовать TLA+; Итак, мы сделаем это здесь в качестве своего рода мысленного эксперимента.
Решение
Использование TLA+ не предназначено, как вы иногда читаете, для формальной проверки кода. Скорее, это формальная проверка идей в вашей голове и предоставление документации по ним, которой можно поделиться с другими людьми. Ничто не будет напрямую связывать спецификацию TLA+ с кодом, написанным для ее реализации; ничего, кроме, надеюсь, более ясного размышления о параллельном аспекте проектирования системы — а это уже довольно много.
Ниже следует спецификация в полном объеме; мы рассмотрим каждую часть одну за другой после.
Установка
EXTENDS Naturals, Sequences VARIABLES level, clients, queue CONSTANT UpperBound, ClientId
В самом верху спецификации мы импортируем модули и объявляем переменные и константы. Переменные — это то, что может быть изменено работающей моделью, а константы — это то, что нужно определить в средстве проверки модели TLC перед его запуском.
ClientStatus == {"Acquired", "Released", "Waiting", "Cancelled"}
Init == /\ level = UpperBound
/\ clients = [fut \in ClientId |-> "Released" ]
/\ queue = << >>
TypeInvariant == /\ level >= 0
/\ clients \in [ClientId -> ClientStatus]
/\ queue \in Seq(ClientId)
/\ level =< UpperBound
/\ Len(queue) =< UpperBound
Следующая часть спецификации представляет его настройку. Сначала мы объявляем своего рода тип, набор ClientStatus, представляющий различные состояния, в которых может находиться клиент семафора:
Acquired— это когда клиент успешно получил семафор.Released— это состояние после освобождения полученного семафора, а также состояние, в котором мы инициализируем всех клиентов в модели.Waitingпредставляет клиента, который не смог получить семафор и был добавлен в очередь.Cancelled— это клиент, который был добавлен в очередь, а затем решил, что ему больше не нужно получать семафор.
Затем мы определяем оператор Init, который представляет собой инициализацию спецификации. Там мы устанавливаем queue в пустую очередь, устанавливаем счетчик семафора (называемый здесь level) на верхнюю границу, определенную моделью, и инициализируем всех клиентов в состояние Released. Обратите внимание, что clients является функцией от ClientId до ClientStatus , которую вы можете представить как карту; или, на языке Python, словарь.
TypeInvariant представляет инвариант, который должен выполняться для всех состояний модели.
Далее следуют операторы спецификации. Каждый из них представляет условный переход состояния, и они могут чередоваться в любом порядке, соответствующем установленным условиям. Обратите внимание, что операторы не выполняются параллельно друг другу — в соответствии с приведенным выше наблюдением, что проблемы, возникающие при работе с параллелизмом, сами по себе не связаны с параллелизмом — они будут выполняться последовательно.
Acquire(id) == /\ Len(queue) = 0
/\ clients[id] = "Released"
/\ level > 0
/\ level' = level - 1
/\ clients' = [clients EXCEPT ![id] = "Acquired"]
/\ UNCHANGED <<queue>>
Release(id) == /\ level' = level + 1
/\ clients[id] = "Acquired"
/\ clients' = [clients EXCEPT ![id] = "Released"]
/\ UNCHANGED <<queue>>
AddWaiter(id) == /\ level = 0
/\ clients[id] = "Released"
/\ clients' = [clients EXCEPT ![id] = "Waiting"]
/\ queue' = Append(queue, id)
/\ UNCHANGED <<level>>
CancelWaiter(id) == /\ clients[id] = "Waiting"
/\ clients' = [clients EXCEPT ![id] = "Cancelled"]
/\ UNCHANGED <<level, queue>>
Каждый из первых четырех операторов принимает ClientId и выполняет несколько шагов для этого идентификатора. Шаги с использованием заштрихованной переменной, например queue’ , представляют собой изменение этой переменной, а не заштрихованные - скорее условия оператора.
Например, в Acquire(id) есть условие, что очередь пуста, что покрывает ошибку справедливости, упомянутую Гвидо, когда клиенты повторно получали семафор, даже если в очереди стояли другие.
AddWaiter(id) — это оператор, который при нулевом уровне добавляет клиента в очередь. Далее мы рассмотрим два оператора, которые удаляют клиентов из очереди.
AcquireNext == LET id == Head(queue)
IN /\ Len(queue) > 0
/\ level > 0
/\ level' = level - 1
/\ clients[id] = "Waiting"
/\ queue' = Tail(queue)
/\ clients' = [clients EXCEPT ![id] = "Acquired"]
RemoveCancelled == LET id == Head(queue)
IN /\ Len(queue) > 0
/\ clients[id] = "Cancelled"
/\ queue' = Tail(queue)
/\ clients' = [clients EXCEPT ![id] = "Released"]
/\ UNCHANGED <<level>>
Пока клиент находится в очереди, он может перейти из состояния Waiting в состояние Cancelled посредством CancelWaiter(id). Из этого следует, что всякий раз, когда level возвращается выше нуля и в очереди есть клиенты, модель будет удалять первого из очереди, либо запустив AcquireNext, который увидит, что клиент получает семафор, либо запустив RemoveCancelled, который вернет клиента в исходное состояние Released.
Следующий оператор, Next, определяет так называемый «следующий шаг» спецификации: на каждом шаге работающей модели «вызывается» Next.
Next == \/ \E id \in ClientId:
\/ Acquire(id)
\/ AddWaiter(id)
\/ Release(id)
\/ CancelWaiter(id)
\/ AcquireNext
\/ RemoveCancelled
Сказанное выше можно примерно перевести на английский язык следующим образом: при заданном наборе клиентов на каждом шаге модели должен быть либо клиент, для которого мы можем запустить один из операторов, принимающих идентификатор, либо мы должны иметь возможность для запуска одного из двух шагов, которые удаляют клиента из очереди.
Я оставлю обсуждение Spec и Theorem отличной книге по TLA+.
Константы, как и инвариант, нужно пробивать вручную в программе проверки модели TLC; скриншот того, как это выглядит, прикреплен ниже.
И это все, ребята; теперь у нас есть модель нашего семафора, которая, по крайней мере мне кажется, позволяет легко рассуждать о переходах состояний одного из них. Интересно, что бы сказал об этом Гвидо…
