Осознав, что я давно не писал на Хабр ничего полезного о ФП и Haskell, и что имеется вполне отличный повод для технической статьи, — решил тряхнуть стариной. Речь в статье пойдет о Software Trasactional Memory (STM), которую мне удалось реализовать на Free-монадах при участии ADTs (Algebraic Data Types) и MVars (конкурентные мутабельные переменные). И, в общем-то, Proof of Concept оказался крайне простым, в сравнении с «настоящим» STM. Давайте это обсудим.
STM — подход для программирования конкурентной модели данных. Конкурентность здесь в том, что разные части модели могут обновляться в разных потоках независимо друг от друга, а конфликты на общих ресурсах решаются с помощью транзакций. Транзакционность похожа на таковую в БД, но есть ряд различий. Допустим, вы захотели поменять часть данных в своем коде. Концептуально можно считать, что ваш код не пишет прямо в модель, а работает с копией той части, которая ему нужна. В конце движок STM открывает транзакцию и сначала проверяет, что интересующая вас часть модели никем не менялась. Не менялась? Хорошо, новые значения будут зафиксированы. Кто-то успел раньше вас? Это конфликт, будьте любезны, перезапустите ваши вычисления на новых данных. Схематично это можно представить так:
Здесь атомарные операции выполняются тредами параллельно, но коммитятся только внутри транзакций, блокирующих доступ к изменяемым частям модели.
Существуют разные вариации STM, но мы будем говорить конкретно о той, что предложена в знаменитом труде «Composable Memory Transactions», поскольку ее отличает ряд замечательных свойств:
Модель может быть какой угодно структурой данных. Вы можете преобразовать любую вашу обычную модель в транзакционную, для этого STM-библиотеки предоставляют различные примитивы: переменные (TVar), очереди (TQueue), массивы (TArray) и много других. Можно догадаться, что транзакционные переменные — TVar’и («твари») — уже минимально достаточны для полноценного STM, а все остальное выражается через них.
Рассмотрим, например, проблему обедающих философов. Мы можем представить вилки как общий ресурс, к которому нужно выстроить конкурентный доступ:
Эта модель наиболее простая: каждая вилка хранится в своей транзакционной переменной, и нужно с ними работать попарно: (fork1, fork2), (fork2, fork3), … (fork5, fork1). А вот такая структура работала бы хуже:
Потому что здесь всего один разделяемый ресурс, и если бы у нас были пять философствующих потоков, они бы получали право на коммит по очереди. В итоге, обедал бы только один философ, а четыре других бы размышляли, а в следующий раз обедал бы другой, но тоже один, хотя теоретически при пяти вилках обедать параллельно могут двое. Поэтому нужно составлять такую конкурентную модель, которая даст наиболее ожидаемое поведение. Вот как могло выглядеть вычисление в монаде STM для модели с раздельными вилками-тварями:
Функция возвращает True, если вилка была свободна, и ее успешно «взяли», то есть, перезаписали tFork. False будет, если вилка уже в деле, и ее нельзя трогать. Теперь рассмотрим пару вилок. Ситуаций может быть пять:
Напишем теперь взятие обеих вилок нашим философом:
Можно заметить, что код позволяет взять одну вилку (например, левую), но при этом не взять другую (например, правую, которая оказалась занята соседом). Функция takeForks, конечно, вернет False в этом случае, но как быть с тем, что одна вилка таки оказалась в руках нашего философа? Он не сможет есть одной, поэтому ее надо положить обратно, и продолжать размышлять еще какое-то время. После этого можно попробовать снова в надежде, что обе вилки окажутся свободными.
Но «положить назад» в терминах STM реализуется несколько иначе, чем в терминах других конкурентных структур. Мы можем считать, что обе переменные — tLeftFork и tRightFork — это локальные копии, которые не связаны с этим же ресурсом у других философов. Поэтому можно не «класть» вилку назад, а сказать вычислению, что оно провалено. Тогда наша одна взятая вилка не запишется в общие ресурсы, — все равно, что и не было успешного вызова takeFork. Это очень удобно, и именно операция «отмены» текущего монадического вычисления отличает реализацию хаскельного STM от других. Для отмены имеется специальный метод retry, давайте перепишем takeForks с его использованием:
Вычисление будет успешным, когда сразу обе вилки были взяты нашим философом. В противном случае, оно будет рестартовать снова и снова через какие-то промежутки времени. В этой версии мы не возвращаем Bool, потому что нам не потребуется знать, успешно ли захвачены оба ресурса. Если функция выполнилась и не зафейлила вычисление, — значит, успешно.
После взятия вилок нам, вероятно, нужно будет сделать что-то еще, например, перевести философа в состояние «Eating». Мы просто делаем это после вызова takeForks, а монада STM позаботится, чтобы состояния «тварей» были консистентны:
Полную реализацию этого метода оставим в качестве упражнения, а сейчас рассмотрим последнее недостающее звено. Покамест мы только описывали логику транзакционной модели, но никаких конкретных TVar мы еще не создали, и ничего не запустили выполняться. Давайте это сделаем:
Комбинатор atomically :: STM a -> IO a выполняет вычисление в монаде STM атомарно. Из типа видно, что чистая часть — работа с конкурентной моделью — отделена от нечистых вычислений в монаде IO. STM-код не должен иметь эффектов. Лучше — вообще никаких, иначе при перезапусках вы будете получать какие-то странные результаты, например, если вы писали в файл, то при некоторых ситуациях вы можете получить паразитные записи, а эту ошибку очень сложно отловить. Поэтому можно считать, что в монаде STM есть только чистые вычисления, а их исполнение — атомарная операция, которая, впрочем, не блокирует другие вычисления. Нечистыми также являются и функции для создания TVar newTVarIO :: a -> IO (TVar a), но ничто не мешает создавать новые TVar внутри STM с помощью чистого комбинатора newTVar :: a -> STM (TVar a). Нам это просто не понадобилось. Внимательные заметят, что разделяемым ресурсом здесь являются только вилки, а состояние самих философов обернуто в TVar лишь для удобства.
Подведем итог. Минимальная реализация STM должна содержать следующие функции по работе с TVar:
Выполнение вычислений:
Наконец, возможность перезапустить вычисление будет огромным плюсом:
Конечно, в библиотеках есть огромное количество других полезных конструкций, например, экземпляр класса типов Alternative для STM, но оставим это на самостоятельное изучение.
Реализация корректно работающей STM считается сложным делом, и лучше, если есть поддержка со стороны компилятора. Мне доводилось слышать, что реализации в Haskell и Clojure на сегодняшний момент лучшие, а в других языках STM не вполне настоящая. Можно предположить, что монадических STM с возможностью перезапуска вычислений и контролем эффектов нет ни в одном императивном языке. Но это все досужие рассуждения, и я могу оказаться неправ. К сожалению, я не разбираюсь во внутренностях даже хаскельной библиотеки stm, не говоря уж о прочих экосистемах. Тем не менее, с точки зрения интерфейса вполне понятно, как код должен вести себя в многопоточной среде. А если есть спецификация интерфейса (предметно-ориентированного языка) и ожидаемое поведение, этого уже достаточно, чтобы попробовать создать свою STM с помощью Free-монад.
Итак, Free-монады. Любой DSL, построенный на Free-монадах, будет иметь следующие характеристики:
Free-монады — очень мощный инструмент, и их можно считать «правильным», чисто функциональным подходом для реализации Inversion of Control. По моим ощущениям, любую задачу в предметной области можно также решить и с помощью Free-монадического DSL. Поскольку эта тема очень обширна и затрагивает многие вопросы дизайна и архитектуры ПО в функциональном программировании, я оставлю за скобками прочие подробности. Любопытствующие же могут обратиться к многочисленным источникам в Интернете или к моей полукниге «Functional Design and Architecture», где Free-монадам уделено особое внимание.
А сейчас давайте заглянем в код моей библиотеки stm-free.
Поскольку STM — это предметно-ориентированный язык для создания транзакционных моделей, он чистый и монадический, то можно предположить, что для минимальной STM, Free DSL должен содержать те же самые методы по работе с TVar, и они будут автоматически компонуемыми и чистыми в этой самой Free-монаде. Сначала определим, чем является TVar.
Нам нужно будет различать наших «тварей», поэтому каждый экземпляр будет идентифицироваться уникальным значением. Пользователю библиотеки это не нужно знать, он ожидаемо будет использовать тип TVar a. Работа со значениями этого типа — половина всего поведения нашей маленькой STM. Поэтому определим ADT с соответствующими методами:
И здесь нужно остановиться поподробнее.
Почему мы должны это делать? Суть в том, что Free-монада должна строиться поверх какого-то eDSL. Самый легкий способ его задать — это определить возможные методы в виде конструкторов ADT. Конечный пользователь не будет работать с этим типом, но мы будем использовать его для интерпретации методов с каким-нибудь эффектом. Очевидно, что метод NewTVar должен интерпретироваться с результатом «новая TVar создана и возвращена как результат». Но можно сделать такой интерпретатор, который будет делать что-то еще, например — писать в БД, в лог, или вовсе выполнять вызовы к настоящей STM.
Эти конструкторы содержат в себе всю необходимую информацию, чтобы быть интерпретированными. Конструктор NewTVar содержит некое пользовательское значение a, и при интерпретации мы положим это значение в новую TVar. Но проблема в том, что a должен быть своим для каждого вызова NewTVar. Если бы мы написали просто STMF next a, a уже был бы общим для всего кода, где завязаны несколько вызовов NewTVar:
Но это бессмысленно, потому что мы хотим все-таки использовать NewTVar для своих произвольных типов, и чтобы они при этом не толкались. Потому мы убираем a в локальную видимость только конкретного метода.
Более интересный вопрос, где же наконец наша кастомная монада для STM. Вот она:
Мы обернули тип STMF в тип Free, а с ним пришли все нужные нам монадические свойства. Осталось только создать ряд удобных монадических функций поверх наших голых методов языка STMF:
Как итог, мы уже можем оперировать транзакционной моделью в виде TVar’ов. По факту, можно взять пример с обедающими философами и нехитро заменить STM на STML:
Легкая победа! Но есть вещи, которые мы упустили. Например, метод для обрыва вычислений retry. Его несложно добавить:
В моей библиотеке есть незначительные отличия от более старшей сестры; в частности, метод retry здесь возвращает Unit, хотя должен возвращать произвольный тип a. Это не принципиальное ограничение, а артефакт быстрой разработки PoC, и в будущем я это исправлю. Тем не менее, даже этот код останется без переделок кроме замены самой монады:
Монадический eDSL максимально похож на базовую реализацию, а вот запуск STML сценариев отличается. Мой комбинатор atomically, в отличие от базовой реализации, принимает дополнительный аргумент — контекст, в котором будет крутиться вычисление.
В контексте хранятся пользовательские данные в виде TVar, поэтому можно иметь несколько разных контекстов. Это может быть полезным, например, для разделения транзакционных моделей, — чтобы они не влияли друг на друга. Скажем, в одной модели создается огромное количество пользовательских данных, а в другой модели набор TVar не меняется вовсе. Тогда имеет смысл разделить контексты, чтобы вторая модель при выполнении не испытывала проблем из-за «распухающей» соседки. В базовой же реализации контекст глобален, и я не очень представляю, как это можно обойти.
Код запуск философов теперь выглядит так:
Что происходит, когда мы запускаем сценарий на выполнение с помощью atomically? Начинается интерпретация сценария относительно реального окружения. Именно в этот момент начинают создаваться и изменяться TVar’ы, проверяться условия прерывания, и именно внутри atomically транзакция либо будет зафиксирована в переданном контексте, либо будет откачена и перезапущена. Алгоритм такой:
Контекст может измениться, пока данное вычисление что-то делает со своей локальной копией. Конфликт возникает, когда изменилась хотя бы одна TVar, задействованная в данном вычислении. Это будет видно по уникальному идентификатору, хранящемуся в каждом экземпляре. Но если вычисление никак не использовало TVar, конфликта не будет.
Пусть наше реальное окружение выражено некоей монадой Atomic, которая представляет собой стек из State и IO монад. В качестве состояния — локальная копия всех TVar:
Будем внутри этой монады раскручивать и интерпретировать две взаимно вложенные структуры: тип STML, который, как мы помним, строится с помощью типа Free, и тип STMF. Тип Free немного мозголомный, так как рекурсивный. У него есть два варианта:
Интерпретация делается простым pattern-matching. Интерпретатор возвращает либо значение всей транзакции, либо команду на перезапуск оной.
Функции newTVar', readTVar', writeTvar' работают с локальной копией транзакционных переменных, и могут их свободно изменять. Вызов runSTML делается из другой функции, runSTM, которая проверит локально измененные TVars на конфликты с глобальной копией из контекста, и решит, нужно ли перезапустить транзакцию.
Оставлю эту функцию без пояснений, а также не стану углубляться в детали, как реализована функция tryCommit. Не очень оптимально, если честно, но это уже тема для отдельной статьи.
В моей реализации есть ряд тонких моментов, которые мне еще нужно осознать. Все еще могут быть неочевидные баги, и нужно бы проверить больше кейсов «на адекватность поведения», да вот неясно, что же считать адекватным поведением STM. Но по крайней мере, никаких внешних отличий на задаче обедающих философов я не выявил, а значит, идея работает, и ее можно доводить до ума. В частности, можно сильно оптимизировать рантайм, сделать более умным решение конфликтов и снятие локальной копии. Подход с интерпретацией и Free-монадой получается весьма гибким, а кода, как вы сами можете убедиться, гораздо меньше, и он в целом, весьма прямолинейный. И это хорошо, потому что открывает еще путь для реализации STM в других языках.
Например, сейчас я портирую Free-монадный STM в C++, что сопряжено со своими, уникальными для этого языка, трудностями. По результатам работы я сделаю доклад на апрельской конференции C++ Russia 2018, и если кто-нибудь собирается ее посетить, то можно обсудить эту тему подробнее.
Software Transactional Memory
STM — подход для программирования конкурентной модели данных. Конкурентность здесь в том, что разные части модели могут обновляться в разных потоках независимо друг от друга, а конфликты на общих ресурсах решаются с помощью транзакций. Транзакционность похожа на таковую в БД, но есть ряд различий. Допустим, вы захотели поменять часть данных в своем коде. Концептуально можно считать, что ваш код не пишет прямо в модель, а работает с копией той части, которая ему нужна. В конце движок STM открывает транзакцию и сначала проверяет, что интересующая вас часть модели никем не менялась. Не менялась? Хорошо, новые значения будут зафиксированы. Кто-то успел раньше вас? Это конфликт, будьте любезны, перезапустите ваши вычисления на новых данных. Схематично это можно представить так:
Здесь атомарные операции выполняются тредами параллельно, но коммитятся только внутри транзакций, блокирующих доступ к изменяемым частям модели.
Существуют разные вариации STM, но мы будем говорить конкретно о той, что предложена в знаменитом труде «Composable Memory Transactions», поскольку ее отличает ряд замечательных свойств:
- разделены понятия модели данных и вычислений над ней;
- вычисления — это монада STM, и они компонуемы в полном соответствии с парадигмой ФП;
- имеется понятие ручного перезапуска вычисления (retry);
- наконец, есть отличная реализация для Haskell, которую, впрочем, я рассматривать не буду, а сфокусируюсь на своей, интерфейсно похожей.
Модель может быть какой угодно структурой данных. Вы можете преобразовать любую вашу обычную модель в транзакционную, для этого STM-библиотеки предоставляют различные примитивы: переменные (TVar), очереди (TQueue), массивы (TArray) и много других. Можно догадаться, что транзакционные переменные — TVar’и («твари») — уже минимально достаточны для полноценного STM, а все остальное выражается через них.
Рассмотрим, например, проблему обедающих философов. Мы можем представить вилки как общий ресурс, к которому нужно выстроить конкурентный доступ:
data ForkState = Free | Taken
type TFork = TVar ForkState
data Forks = Forks
{ fork1 :: TFork
, fork2 :: TFork
, fork3 :: TFork
, fork4 :: TFork
, fork5 :: TFork
}Эта модель наиболее простая: каждая вилка хранится в своей транзакционной переменной, и нужно с ними работать попарно: (fork1, fork2), (fork2, fork3), … (fork5, fork1). А вот такая структура работала бы хуже:
type Forks = TVar [ForkState]Потому что здесь всего один разделяемый ресурс, и если бы у нас были пять философствующих потоков, они бы получали право на коммит по очереди. В итоге, обедал бы только один философ, а четыре других бы размышляли, а в следующий раз обедал бы другой, но тоже один, хотя теоретически при пяти вилках обедать параллельно могут двое. Поэтому нужно составлять такую конкурентную модель, которая даст наиболее ожидаемое поведение. Вот как могло выглядеть вычисление в монаде STM для модели с раздельными вилками-тварями:
data ForkState = Free | Taken
type TFork = TVar ForkState
takeFork :: TFork -> STM Bool
takeFork tFork = do
forkState <- readTVar tFork
when (forkState == Free) (writeTVar tFork Taken)
pure (forkState == Free)Функция возвращает True, если вилка была свободна, и ее успешно «взяли», то есть, перезаписали tFork. False будет, если вилка уже в деле, и ее нельзя трогать. Теперь рассмотрим пару вилок. Ситуаций может быть пять:
- Обе свободны
- Левая занята (левым соседом), правая свободна
- Левая свободна, правая занята (правым соседом)
- Обе заняты (соседями)
- Обе заняты (нашим философом)
Напишем теперь взятие обеих вилок нашим философом:
takeForks :: (TFork, TFork) -> STM Bool
takeForks (tLeftFork, tRightFork) = do
leftTaken <- takeFork tLeftFork
rightTaken <- takeFork tRightFork
pure (leftTaken && rightTaken)Можно заметить, что код позволяет взять одну вилку (например, левую), но при этом не взять другую (например, правую, которая оказалась занята соседом). Функция takeForks, конечно, вернет False в этом случае, но как быть с тем, что одна вилка таки оказалась в руках нашего философа? Он не сможет есть одной, поэтому ее надо положить обратно, и продолжать размышлять еще какое-то время. После этого можно попробовать снова в надежде, что обе вилки окажутся свободными.
Но «положить назад» в терминах STM реализуется несколько иначе, чем в терминах других конкурентных структур. Мы можем считать, что обе переменные — tLeftFork и tRightFork — это локальные копии, которые не связаны с этим же ресурсом у других философов. Поэтому можно не «класть» вилку назад, а сказать вычислению, что оно провалено. Тогда наша одна взятая вилка не запишется в общие ресурсы, — все равно, что и не было успешного вызова takeFork. Это очень удобно, и именно операция «отмены» текущего монадического вычисления отличает реализацию хаскельного STM от других. Для отмены имеется специальный метод retry, давайте перепишем takeForks с его использованием:
takeForks :: (TFork, TFork) -> STM ()
takeForks (tLeftFork, tRightFork) = do
leftTaken <- takeFork tLeftFork
rightTaken <- takeFork tRightFork
when (not leftTaken || not rightTaken) retryВычисление будет успешным, когда сразу обе вилки были взяты нашим философом. В противном случае, оно будет рестартовать снова и снова через какие-то промежутки времени. В этой версии мы не возвращаем Bool, потому что нам не потребуется знать, успешно ли захвачены оба ресурса. Если функция выполнилась и не зафейлила вычисление, — значит, успешно.
После взятия вилок нам, вероятно, нужно будет сделать что-то еще, например, перевести философа в состояние «Eating». Мы просто делаем это после вызова takeForks, а монада STM позаботится, чтобы состояния «тварей» были консистентны:
data PhilosopherState = Thinking | Eating
data Philosopher = Philosopher
{ pState :: TVar PhilosopherState
, pLeftFork :: TFork
, pRrightFork :: TFork
}
changePhilosopherActivity :: Philosopher -> STM ()
changePhilosopherActivity (Philosopher tState tLeftFork tRightFork) = do
state <- readTVar tState
case state of
Thinking -> do
taken <- takeForks tFs
unless taken retry -- Do not need to put forks if any was taken!
writeTVar tAct Eating
pure Eating
Eating -> error "Changing state from Eating not implemented."Полную реализацию этого метода оставим в качестве упражнения, а сейчас рассмотрим последнее недостающее звено. Покамест мы только описывали логику транзакционной модели, но никаких конкретных TVar мы еще не создали, и ничего не запустили выполняться. Давайте это сделаем:
philosoperWorker :: Philosopher -> IO ()
philosoperWorker philosopher = do
atomically (changePhilosopherActivity philosopher)
threadDelay 5000
philosoperWorker philosopher
runPhilosophers :: IO ()
runPhilosophers = do
tState1 <- newTVarIO Thinking
tState2 <- newTVarIO Thinking
tFork1 <- newTVarIO Free
tFork2 <- newTVarIO Free
forkIO (philosoperWorker (Philosopher tState1 tFork1 tFork2))
forkIO (philosoperWorker (Philosopher tState2 tFork2 tFork1))
threadDelay 100000Комбинатор atomically :: STM a -> IO a выполняет вычисление в монаде STM атомарно. Из типа видно, что чистая часть — работа с конкурентной моделью — отделена от нечистых вычислений в монаде IO. STM-код не должен иметь эффектов. Лучше — вообще никаких, иначе при перезапусках вы будете получать какие-то странные результаты, например, если вы писали в файл, то при некоторых ситуациях вы можете получить паразитные записи, а эту ошибку очень сложно отловить. Поэтому можно считать, что в монаде STM есть только чистые вычисления, а их исполнение — атомарная операция, которая, впрочем, не блокирует другие вычисления. Нечистыми также являются и функции для создания TVar newTVarIO :: a -> IO (TVar a), но ничто не мешает создавать новые TVar внутри STM с помощью чистого комбинатора newTVar :: a -> STM (TVar a). Нам это просто не понадобилось. Внимательные заметят, что разделяемым ресурсом здесь являются только вилки, а состояние самих философов обернуто в TVar лишь для удобства.
Подведем итог. Минимальная реализация STM должна содержать следующие функции по работе с TVar:
newTVar :: a -> STM (TVar a)
readTVar :: TVar a -> STM a
writeTVar :: TVar a -> a -> STM ()Выполнение вычислений:
atomically :: STM a -> IO aНаконец, возможность перезапустить вычисление будет огромным плюсом:
retry :: STM aКонечно, в библиотеках есть огромное количество других полезных конструкций, например, экземпляр класса типов Alternative для STM, но оставим это на самостоятельное изучение.
STM на Free-монадах
Реализация корректно работающей STM считается сложным делом, и лучше, если есть поддержка со стороны компилятора. Мне доводилось слышать, что реализации в Haskell и Clojure на сегодняшний момент лучшие, а в других языках STM не вполне настоящая. Можно предположить, что монадических STM с возможностью перезапуска вычислений и контролем эффектов нет ни в одном императивном языке. Но это все досужие рассуждения, и я могу оказаться неправ. К сожалению, я не разбираюсь во внутренностях даже хаскельной библиотеки stm, не говоря уж о прочих экосистемах. Тем не менее, с точки зрения интерфейса вполне понятно, как код должен вести себя в многопоточной среде. А если есть спецификация интерфейса (предметно-ориентированного языка) и ожидаемое поведение, этого уже достаточно, чтобы попробовать создать свою STM с помощью Free-монад.
Итак, Free-монады. Любой DSL, построенный на Free-монадах, будет иметь следующие характеристики:
- Чистый DSL, компонуемый монадически, то есть, по-настоящему функционально;
- Код на таком DSL не будет содержать ничего лишнего, помимо предметной области, а значит, его легче читать и понимать;
- Интерфейс и имплементация эффективно разделены;
- Имплементаций может быть несколько, и их можно заменять в рантайме.
Free-монады — очень мощный инструмент, и их можно считать «правильным», чисто функциональным подходом для реализации Inversion of Control. По моим ощущениям, любую задачу в предметной области можно также решить и с помощью Free-монадического DSL. Поскольку эта тема очень обширна и затрагивает многие вопросы дизайна и архитектуры ПО в функциональном программировании, я оставлю за скобками прочие подробности. Любопытствующие же могут обратиться к многочисленным источникам в Интернете или к моей полукниге «Functional Design and Architecture», где Free-монадам уделено особое внимание.
А сейчас давайте заглянем в код моей библиотеки stm-free.
Поскольку STM — это предметно-ориентированный язык для создания транзакционных моделей, он чистый и монадический, то можно предположить, что для минимальной STM, Free DSL должен содержать те же самые методы по работе с TVar, и они будут автоматически компонуемыми и чистыми в этой самой Free-монаде. Сначала определим, чем является TVar.
type UStamp = Unique
newtype TVarId = TVarId UStamp
data TVar a = TVar TVarIdНам нужно будет различать наших «тварей», поэтому каждый экземпляр будет идентифицироваться уникальным значением. Пользователю библиотеки это не нужно знать, он ожидаемо будет использовать тип TVar a. Работа со значениями этого типа — половина всего поведения нашей маленькой STM. Поэтому определим ADT с соответствующими методами:
data STMF next where
NewTVar :: a -> (TVar a -> next) -> STMF next
WriteTVar :: TVar a -> a -> next -> STMF next
ReadTVar :: TVar a -> (a -> next) -> STMF nextИ здесь нужно остановиться поподробнее.
Почему мы должны это делать? Суть в том, что Free-монада должна строиться поверх какого-то eDSL. Самый легкий способ его задать — это определить возможные методы в виде конструкторов ADT. Конечный пользователь не будет работать с этим типом, но мы будем использовать его для интерпретации методов с каким-нибудь эффектом. Очевидно, что метод NewTVar должен интерпретироваться с результатом «новая TVar создана и возвращена как результат». Но можно сделать такой интерпретатор, который будет делать что-то еще, например — писать в БД, в лог, или вовсе выполнять вызовы к настоящей STM.
Эти конструкторы содержат в себе всю необходимую информацию, чтобы быть интерпретированными. Конструктор NewTVar содержит некое пользовательское значение a, и при интерпретации мы положим это значение в новую TVar. Но проблема в том, что a должен быть своим для каждого вызова NewTVar. Если бы мы написали просто STMF next a, a уже был бы общим для всего кода, где завязаны несколько вызовов NewTVar:
data STMF next a where
NewTVar :: a -> (TVar a -> next) -> STMF nextНо это бессмысленно, потому что мы хотим все-таки использовать NewTVar для своих произвольных типов, и чтобы они при этом не толкались. Потому мы убираем a в локальную видимость только конкретного метода.
Примечание. На самом деле, для ускорения работы над Proof of Concept, на тип a у меня наложено ограничение, чтобы он был сериализуем (экземпляр класса ToJSON / FromJSON из библиотеки aeson). Дело в том, что мне нужно будет хранить эти разнотиповые TVar’ы в мапе, но я не хочу возиться с Typeable / Dynamic или, тем более, с HLists. В реальных STM тип a может быть абсолютно любой, даже функции. Я тоже займусь этим вопросом как-нибудь позже.А что это за поле next такое? Здесь мы наступаем на требование со стороны Free-монады. Ей нужно где-то хранить продолжение текущего метода, причем просто поле next её не устраивает, — ADT должен быть функтором по этому полю. Так, метод NewTVar должен возвращать TVar a, и мы видим, что продолжение (TVar a -> next) как раз ждет нашу новую переменную на вход. С другой стороны, WriteTVar не возвращает ничего полезного, поэтому продолжение имеет тип next, — то есть, не ожидает ничего на вход. Сделать функтором тип STMF несложно:
instance Functor STMF where
fmap g (NewTVar a nextF) = NewTVar a (g . nextF)
fmap g (WriteTVar tvar a next ) = WriteTVar tvar a (g next)
fmap g (ReadTVar tvar nextF) = ReadTVar tvar (g . nextF)Более интересный вопрос, где же наконец наша кастомная монада для STM. Вот она:
type STML next = Free STMF nextМы обернули тип STMF в тип Free, а с ним пришли все нужные нам монадические свойства. Осталось только создать ряд удобных монадических функций поверх наших голых методов языка STMF:
newTVar :: ToJSON a => a -> STML (TVar a)
newTVar a = liftF (NewTVar a id)
writeTVar :: ToJSON a => TVar a -> a -> STML ()
writeTVar tvar a = liftF (WriteTVar tvar a ())
readTVar :: FromJSON a => TVar a -> STML a
readTVar tvar = liftF (ReadTVar tvar id)Как итог, мы уже можем оперировать транзакционной моделью в виде TVar’ов. По факту, можно взять пример с обедающими философами и нехитро заменить STM на STML:
data ForkState = Free | Taken
type TFork = TVar ForkState
takeFork :: TFork -> STML Bool
takeFork tFork = do
forkState <- readTVar tFork
when (forkState == Free) (writeTVar tFork Taken)
pure (forkState == Free)Легкая победа! Но есть вещи, которые мы упустили. Например, метод для обрыва вычислений retry. Его несложно добавить:
data STMF next where
Retry :: STMF next
instance Functor STMF where
fmap g Retry = Retry
retry :: STML ()
retry = liftF RetryВ моей библиотеке есть незначительные отличия от более старшей сестры; в частности, метод retry здесь возвращает Unit, хотя должен возвращать произвольный тип a. Это не принципиальное ограничение, а артефакт быстрой разработки PoC, и в будущем я это исправлю. Тем не менее, даже этот код останется без переделок кроме замены самой монады:
takeForks :: (TFork, TFork) -> STML ()
takeForks (tLeftFork, tRightFork) = do
leftTaken <- takeFork tLeftFork
rightTaken <- takeFork tRightFork
when (not leftTaken || not rightTaken) retryМонадический eDSL максимально похож на базовую реализацию, а вот запуск STML сценариев отличается. Мой комбинатор atomically, в отличие от базовой реализации, принимает дополнительный аргумент — контекст, в котором будет крутиться вычисление.
atomically :: Context -> STML a -> IO aВ контексте хранятся пользовательские данные в виде TVar, поэтому можно иметь несколько разных контекстов. Это может быть полезным, например, для разделения транзакционных моделей, — чтобы они не влияли друг на друга. Скажем, в одной модели создается огромное количество пользовательских данных, а в другой модели набор TVar не меняется вовсе. Тогда имеет смысл разделить контексты, чтобы вторая модель при выполнении не испытывала проблем из-за «распухающей» соседки. В базовой же реализации контекст глобален, и я не очень представляю, как это можно обойти.
Код запуск философов теперь выглядит так:
philosoperWorker :: Context -> Philosopher -> IO ()
philosoperWorker ctx philosopher = do
atomically ctx (changePhilosopherActivity philosopher)
threadDelay 5000
philosoperWorker ctx philosopher
runPhilosophers :: IO ()
runPhilosophers = do
ctx <- newContext -- Создание контекста.
tState1 <- newTVarIO ctx Thinking
tState2 <- newTVarIO ctx Thinking
tFork1 <- newTVarIO ctx Free
tFork2 <- newTVarIO ctx Free
forkIO (philosoperWorker ctx (Philosopher tState1 tFork1 tFork2))
forkIO (philosoperWorker ctx (Philosopher tState2 tFork2 tFork1))
threadDelay 100000Немного об интерпретации
Что происходит, когда мы запускаем сценарий на выполнение с помощью atomically? Начинается интерпретация сценария относительно реального окружения. Именно в этот момент начинают создаваться и изменяться TVar’ы, проверяться условия прерывания, и именно внутри atomically транзакция либо будет зафиксирована в переданном контексте, либо будет откачена и перезапущена. Алгоритм такой:
- Получить уникальный идентификатор транзакции.
- Атомарно снять локальную копию с текущего контекста. Здесь происходит краткая блокировка контекста, делается это с помощью MVar, которая выступает как обычный mutex.
- Запустить интерпретацию сценария с локальной копией, дождаться результата.
- Если получена команда перезапуска вычисления, усыпить поток на некоторое время и перейти к пункту 1.
- Если получен результат, атомарно проверить конфликты локальной копии и контекста.
- Если конфликты найдены, усыпить поток на некоторое время и перейти к пункту 1.
- Если конфликтов нет, все также атомарно замержить локальную копию в контекст.
- Конец.
Контекст может измениться, пока данное вычисление что-то делает со своей локальной копией. Конфликт возникает, когда изменилась хотя бы одна TVar, задействованная в данном вычислении. Это будет видно по уникальному идентификатору, хранящемуся в каждом экземпляре. Но если вычисление никак не использовало TVar, конфликта не будет.
Пусть наше реальное окружение выражено некоей монадой Atomic, которая представляет собой стек из State и IO монад. В качестве состояния — локальная копия всех TVar:
data AtomicRuntime = AtomicRuntime
{ ustamp :: UStamp
, localTVars :: TVars
}
type Atomic a = StateT AtomicRuntime IO aБудем внутри этой монады раскручивать и интерпретировать две взаимно вложенные структуры: тип STML, который, как мы помним, строится с помощью типа Free, и тип STMF. Тип Free немного мозголомный, так как рекурсивный. У него есть два варианта:
data Free f a
= Pure a
| Free (f (Free f a))Интерпретация делается простым pattern-matching. Интерпретатор возвращает либо значение всей транзакции, либо команду на перезапуск оной.
interpretStmf :: STMF a -> Atomic (Either RetryCmd a)
interpretStmf (NewTVar a nextF) = Right . nextF <$> newTVar' a
interpretStmf (ReadTVar tvar nextF) = Right . nextF <$> readTVar' tvar
interpretStmf (WriteTVar tvar a next) = const (Right next) <$> writeTVar' tvar a
interpretStmf Retry = pure $ Left RetryCmd
interpretStml :: STML a -> Atomic (Either RetryCmd a)
interpretStml (Pure a) = pure $ Right a
interpretStml (Free f) = do
eRes <- interpretStmf f
case eRes of
Left RetryCmd -> pure $ Left RetryCmd
Right res -> interpretStml res
runSTML :: STML a -> Atomic (Either RetryCmd a)
runSTML = interpretStml
Функции newTVar', readTVar', writeTvar' работают с локальной копией транзакционных переменных, и могут их свободно изменять. Вызов runSTML делается из другой функции, runSTM, которая проверит локально измененные TVars на конфликты с глобальной копией из контекста, и решит, нужно ли перезапустить транзакцию.
runSTM :: Int -> Context -> STML a -> IO a
runSTM delay ctx stml = do
(ustamp, snapshot) <- takeSnapshot ctx
(eRes, AtomicRuntime _ stagedTVars) <- runStateT (runSTML stml) (AtomicRuntime ustamp snapshot)
case eRes of
Left RetryCmd -> runSTM (delay * 2) ctx stml
Right res -> do
success <- tryCommit ctx ustamp stagedTVars
if success
then return res
else runSTM (delay * 2) ctx stmlОставлю эту функцию без пояснений, а также не стану углубляться в детали, как реализована функция tryCommit. Не очень оптимально, если честно, но это уже тема для отдельной статьи.
Заключение
В моей реализации есть ряд тонких моментов, которые мне еще нужно осознать. Все еще могут быть неочевидные баги, и нужно бы проверить больше кейсов «на адекватность поведения», да вот неясно, что же считать адекватным поведением STM. Но по крайней мере, никаких внешних отличий на задаче обедающих философов я не выявил, а значит, идея работает, и ее можно доводить до ума. В частности, можно сильно оптимизировать рантайм, сделать более умным решение конфликтов и снятие локальной копии. Подход с интерпретацией и Free-монадой получается весьма гибким, а кода, как вы сами можете убедиться, гораздо меньше, и он в целом, весьма прямолинейный. И это хорошо, потому что открывает еще путь для реализации STM в других языках.
Например, сейчас я портирую Free-монадный STM в C++, что сопряжено со своими, уникальными для этого языка, трудностями. По результатам работы я сделаю доклад на апрельской конференции C++ Russia 2018, и если кто-нибудь собирается ее посетить, то можно обсудить эту тему подробнее.
