Software Transactional Memory на Free-монадах27.03.2018 16:33

Осознав, что я давно не писал на Хабр ничего полезного о ФП и Haskell, и что имеется вполне отличный повод для технической статьи, — решил тряхнуть стариной. Речь в статье пойдет о Software Trasactional Memory (STM), которую мне удалось реализовать на Free-монадах при участии ADTs и MVars. И, в общем-то, Proof of Concept оказался крайне простым, в сравнении с «настоящим» STM. Давайте это обсудим.

Software Transactional Memory


STM — подход для программирования конкурентной модели данных. Конкурентность здесь в том, что разные части модели могут обновляться в разных потоках независимо друг от друга, а конфликты на общих ресурсах решаются с помощью транзакций. Транзакционность похожа на таковую в БД, но есть ряд различий. Допустим, вы захотели поменять часть данных в своем коде. Концептуально можно считать, что ваш код не пишет прямо в модель, а работает с копией той части, которая ему нужна. В конце движок STM открывает транзакцию и сначала проверяет, что интересующая вас часть модели никем не менялась. Не менялась? Хорошо, новые значения будут зафиксированы. Кто-то успел раньше вас? Это конфликт, будьте любезны, перезапустите ваши вычисления на новых данных. Схематично это можно представить так:

xdewc96wvwycaskfon4uhg4ytbg.png


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

Существуют разные вариации 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 -> error "Changing state from Thinking not implemented."
    Eating   -> do
      takeForks (tLeftFork, tRightFork)
      writeTVar tState Eating


Полную реализацию этого метода оставим в качестве упражнения, а сейчас рассмотрим последнее недостающее звено. Покамест мы просто описывали логику транзакционной модели, но никаких конкретных 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 транзакция либо будет зафиксирована в переданном контексте, либо будет откачена и перезапущена. Алгоритм такой:

  1. Получить уникальный идентификатор транзакции.
  2. Атомарно снять локальную копию с текущего контекста. Здесь происходит краткая блокировка контекста, делается это с помощью MVar, которая выступает как обычный mutex.
  3. Запустить интерпретацию сценария с локальной копией, дождаться результата.
  4. Если получена команда перезапуска вычисления, усыпить поток на некоторое время и перейти к пункту 1.
  5. Если получен результат, атомарно проверить конфликты локальной копии и контекста.
  6. Если конфликты найдены, усыпить поток на некоторое время и перейти к пункту 1.
  7. Если конфликтов нет, все также атомарно замержить локальную копию в контекст.
  8. Конец.


Контекст может измениться, пока данное вычисление что-то делает со своей локальной копией. Конфликт возникает, когда изменилась хотя бы одна 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, и если кто-нибудь собирается ее посетить, то можно обсудить эту тему подробнее.

© Habrahabr.ru