フリーモナドのソフトウェアトランザクションメモリ

長い間、FPとHaskellについてHabrに有用なものを何も書いておらず、技術記事の完全に優れた理由があることに気づいたので、私は昔を振ることに決めました。 この記事では、ADT（代数データ型）とMVar（競合可変変数）を使用して、フリーモナドに実装したSoftware Trasactional Memory（STM）に焦点を当てます。 そして、一般に、概念実証は「実際の」STMと比較して非常にシンプルであることが判明しました。 それについて議論しましょう。

ソフトウェアトランザクションメモリ

STMは、競争力のあるデータモデルをプログラミングするためのアプローチです。 ここでの競争は、モデルのさまざまな部分が互いに独立して異なるスレッドで更新され、共有リソースの競合がトランザクションを使用して解決されることです。 トランザクションはデータベースのトランザクションと似ていますが、いくつかの違いがあります。 コード内のデータの一部を変更するとします。 概念的には、コードがモデルに直接書き込まれるのではなく、必要な部分のコピーで機能すると想定できます。 最後に、STMエンジンはトランザクションを開き、最初に関心のあるモデルの部分が誰によっても変更されていないことを確認します。 変更しませんでしたか？ さて、新しい値は修正されます。 あなたの前に誰かが管理しましたか？ これは競合です。新しいデータで計算を再開してください。 概略的には、これは次のように表すことができます。


ここで、アトミック操作はスレッドによって並列に実行されますが、モデルの可変部分へのアクセスをブロックするトランザクション内でのみコミットされます。

STMにはさまざまなバリエーションがありますが、有名な作品「Composable Memory Transactions」で提案されたものについて具体的にお話します。

• データモデルの概念とその上の計算は分離されています。
• コンピューティングはSTMモナドであり、FPパラダイムに完全に準拠して構成できます。
• 手動で計算を再開するという概念があります（再試行）。
• 最後に、Haskellの優れた実装がありますが、これは考慮しませんが、自分のインターフェイスのようなものに焦点を合わせます。

モデルには、任意のデータ構造を使用できます。 STMライブラリは、変数（ TVar ）、キュー（ TQueue ）、配列（ TArray ）など、さまざまなプリミティブを提供します。 トランザクション変数-TVar'i（ "クリッター"）-は、本格的な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] 

共有リソースは1つしかなく、哲学的なストリームが5つある場合、それらは順番にコミットする権利を受け取ります。 その結果、1人の哲学者だけが食事をし、他の4人が考え、次に別の人が食事をしますが、理論的には5つのフォークで2人が同時に食事をすることもできます。 したがって、最も期待される動作を提供する競合モデルを作成する必要があります。 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) 

プラグが解放され、正常に「取得」された場合、つまりtForkが上書きされた場合、関数はTrueを返します。 プラグがすでに動作している場合は、Falseになり、触れられません。 次に、いくつかのフォークについて考えます。 5つの状況があります。

• 両方とも無料です
• 忙しいまま（左隣）、右は無料
• 左が無料、右が忙しい（右隣）
• 両方とも忙しい（隣人）
• どちらも忙しい（哲学者による）

私たちは今、私たちの哲学者による両方の分岐の取り方を書きます：

 takeForks :: (TFork, TFork) -> STM Bool takeForks (tLeftFork, tRightFork) = do leftTaken <- takeFork tLeftFork rightTaken <- takeFork tRightFork pure (leftTaken && rightTaken) 

このコードでは、1つのプラグ（たとえば、左のプラグ）を使用できますが、別のプラグ（たとえば、隣人が占有していることが判明した右のプラグ）は使用できないことに気付くかもしれません。 もちろんこの場合、 takeForks関数はFalseを返しますが、1つのフォークがまだ哲学者の手中にあるという事実はどうでしょうか？ 彼は一人で食べることができないので、元に戻さなければならず、もうしばらく考え続けなければなりません。 その後、両方のフォークが無料になることを期待して、もう一度試すことができます。

しかし、STMの観点からの「プットバック」は、他の競合構造の観点からやや異なる方法で実装されます。 tLeftForkとtRightForkの両方の変数は、他の哲学者によって同じリソースに接続されていないローカルコピーであると想定できます。 したがって、プラグを「置く」ことはできませんが、失敗したことを計算に伝えることができます。 その場合、1つのフォークは共有リソースに書き込まれません-とにかく、 takeForkの呼び出しが成功しませんでした 。 これは非常に便利であり、Haskelian STM実装を他のものから区別するのは、現在のモナド計算の「キャンセル」操作です。 キャンセルするための特別な再試行方法があります。それを使用してtakeForksを書き換えましょう。

 takeForks :: (TFork, TFork) -> STM () takeForks (tLeftFork, tRightFork) = do leftTaken <- takeFork tLeftFork rightTaken <- takeFork tRightFork when (not leftTaken || not rightTaken) retry 

両方の分岐点が哲学者によって一度に取得された場合、計算は成功します。 それ以外の場合は、一定の間隔で何度も再起動します。 このバージョンでは、両方のリソースが正常にキャプチャされたかどうかを知る必要がないため、 Boolを返しません。 関数が実行され、計算をファイルしない場合、正常に実行されたことを意味します。

分岐点をとった後、たとえば哲学者を「食べる」状態にするなど、何か他のことをする必要があるでしょう。 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 

アトミックに：STM a-> IO aコンビネーターは、 STMモナドでアトミックに計算を実行します。 タイプから、競合モデルで動作する純粋な部分は、 IOモナドのクリーンでないコンピューティングから分離されていることがわかります。 STMコードは効果がありません。 より良い-まったくありません。そうしないと、再起動時にいくつかの奇妙な結果が得られます。たとえば、ファイルに書き込んだ場合、場合によっては偽のエントリを取得できますが、このエラーをキャッチするのは非常に困難です。 したがって、 STMモナドには純粋な計算しかなく、その実行はアトミック操作であると想定できますが、他の計算はブロックしません。 TVar newTVarIO :: a-> IO（TVar a）を作成する関数も汚れていますが、純粋なコンビネータnewTVar :: a-> STM（TVar a）を使用してSTM内で新しいTVarを作成することを妨げるものはありません。 必要なかっただけです。 気配りのある人は、フォークだけが共有リソースであり、哲学者自身の状態が便宜上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 

もちろん、ライブラリには、たとえばSTMの Alternative型クラスのインスタンスなど、他にも非常に多くの便利な構成要素がありますが、独立した学習のために残しましょう。

フリーモナドのSTM

適切に動作するSTMを実装することは難しいと考えられており、コンパイラーからのサポートがあれば良いです。 HaskellとClojureの実装は現時点で最高であり、他の言語ではSTMは現実的ではないと聞いています。 命令型言語で計算を再開し、効果を制御することができるモナドSTMは存在しないと想定できます。 しかし、これはすべて怠idleな推論であり、私は間違っているかもしれません。 残念ながら、他のエコシステムは言うまでもなく、 stm haskelライブラリーの内部すら理解できません。 それでも、インターフェイスの観点から見ると、マルチスレッド環境でコードがどのように動作するかは明らかです。 そして、インターフェース（サブジェクト指向言語）と予想される動作の仕様がある場合、これはすでに、フリーモナドを使用して独自のSTMを作成しようとするのに十分です。

だから、 無料のモナド 。 Freeモナド上に構築されたDSLには、次の特性があります。

• 一元的に構成可能な純粋なDSL、つまり本当に機能します。
• このようなDSLのコードには、サブジェクト領域に加えて余分なものは含まれません。つまり、読みやすく、理解しやすいということです。
• インターフェイスと実装は効果的に分離されています。
• いくつかの実装があり、実行時に置き換えることができます。

無料のモナドは非常に強力なツールであり、 Inversion of Controlを実装するための「正しい」純粋に機能的なアプローチと考えることができます。 私の考えでは、サブジェクト領域の問題は、Free-monadic DSLの助けを借りて解決することもできます。 このトピックは非常に広範囲であり、関数型プログラミングのソフトウェア設計とアーキテクチャの多くの問題に関係しているため、他の詳細は図から省きます。 好奇心people盛な人は、インターネット上の多数の情報源、または無料のモナドが特別な注意を払われている私の半本のFunctional Design and Architectureに目を向けることができます。

では、 stm-freeライブラリのコードを見てみましょう。

STMはトランザクションモデルを作成するためのサブジェクト指向言語であるため、クリーンで単調です。最小限のSTMの場合、無料DSLにはTVarを操作するための同じメソッドが含まれている必要があります。無料のモナド。 まず、TVarとは何かを判断します。

 type UStamp = Unique newtype TVarId = TVarId UStamp data TVar a = TVar TVarId 

「クリーチャー」を区別する必要があるため、各インスタンスは一意の値で識別されます。 ライブラリユーザーはこれを知る必要はありません。TVara型を使用することが期待されます。 このタイプの値を扱うことは、小さな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 Monadは何らかのeDSLの上に構築する必要があるということです。 最も簡単な設定方法は、可能なメソッドをADTコンストラクターの形式で定義することです。 エンドユーザーはこのタイプでは動作しませんが、これを使用して、何らかの効果のあるメソッドを解釈します。 明らかに、NewTVarメソッドは、「新しいTVarが作成され、結果として返される」という結果で解釈される必要があります。 しかし、たとえばデータベース、ログへの書き込み、または実際のSTMへの呼び出しなど、何か他のことを行うインタープリターを作成できます。

これらのコンストラクタには、解釈する必要があるすべての情報が含まれています。 NewTVarコンストラクターには、ユーザー定義の値aが含まれており、解釈時にこの値を新しいTVarに入れます。 しかし問題は、 NewTVarへの呼び出しごとにaが独自のものでなければならないことです 。 次のaにSTMFを記述した場合、いくつかのNewTVar呼び出しが結び付けられているすべてのコードに既に共通しています：

 data STMF next a where NewTVar :: a -> (TVar a -> next) -> STMF next 

しかし、これは無意味です。なぜなら、私たちはまだ任意の型にNewTVarを使用したいからです。 したがって、特定のメソッドのみのローカル可視性でaを削除します。

ご注意 実際、Proof of Conceptの作業を高速化するために、シリアル化できるようにaを入力するように制限されています（ aesonライブラリのToJSON / FromJSONクラスのインスタンス）。 実際、これらのさまざまなタイプのTVarをマップに保存する必要がありますが、 Typeable / Dynamic 、特にHListsを台無しにしたくありません。 実際のSTMでは、タイプaは関数でも、絶対に何でもかまいません。 また、この問題については後ほど対処します。

この次のフィールドはどのようなものですか？ ここでは、Free Monadからの要求に応じます。 彼女は現在のメソッドの継続をどこかに保存する必要があり、 次のフィールドは彼女に適していない-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) 

簡単勝利！ しかし、私たちが見逃したことがあります。 たとえば、 再試行の計算を中断する方法。 追加するのは簡単です：

 data STMF next where Retry :: STMF next instance Functor STMF where fmap g Retry = Retry retry :: STML () retry = liftF Retry 

私のライブラリには姉とわずかな違いがあります。 特に、ここの再試行メソッドはUnitを返しますが、任意の型aを返す必要があります。 これは基本的な制限ではなく、PoCの急速な発展の成果物であり、今後修正します。 それにもかかわらず、このコードでさえ、モナド自体を置き換えることを除いて、変更なしで残ります。

 takeForks :: (TFork, TFork) -> STML () takeForks (tLeftFork, tRightFork) = do leftTaken <- takeFork tLeftFork rightTaken <- takeFork tRightFork when (not leftTaken || not rightTaken) retry 

Monadic eDSLは基本実装に可能な限り似ていますが、STMLスクリプトの起動は異なります。 私のアトミックなコンビネーターは、基本実装とは異なり、追加の引数（計算がスピンするコンテキスト）を取ります。

 atomically :: Context -> STML a -> IO a 

コンテキストはユーザーデータをTVarの形式で保存するため、いくつかの異なるコンテキストを使用できます。 これは、たとえば、トランザクションモデルを分離する場合に役立ちます。これにより、相互に影響を与えません。 たとえば、あるモデルでは膨大な量のユーザーデータが作成され、別のモデルではTVarセットはまったく変更されません。 次に、コンテキストを分離して、2番目のモデルが「腫れている」隣人に起因する問題を経験しないようにすることは理にかなっています。 基本的な実装では、コンテキストはグローバルであり、これをどのように回避できるかはわかりません。

哲学者の起動コードは次のようになります。

 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 

解釈について少し

アトミックにスクリプトを実行するとどうなりますか？ 実際の環境に対するシナリオの解釈が始まります。 この時点でTVarの作成と変更が開始され、割り込み条件がチェックされ、トランザクションが転送されたコンテキストでコミットされるか、ロールバックされて再起動されるのがアトミックです 。 アルゴリズムは次のとおりです。

1. 一意のトランザクション識別子を取得します。
2. 現在のコンテキストからローカルコピーを原子的に削除します。 ここで短いコンテキストロックが発生します。これは、通常のミューテックスのように動作するMVarを使用して行われます。
3. ローカルコピーを使用してスクリプトの解釈を実行し、結果を待ちます。
4. 計算を再開するコマンドを受信した場合は、ストリームをしばらくスリープ状態にして、手順1に進みます。
5. 結果が得られたら、ローカルコピーとコンテキストの競合をアトミックにチェックします。
6. 競合が見つかった場合は、ストリームをしばらくスリープ状態にし、手順1に進みます。
7. 競合がなければ、すべてがローカルコピーをアトミックにコンテキストに凍結しています。
8. 終わり。

この計算がローカルコピーで何かをしている間に、コンテキストが変更される場合があります。 この計算に関係する少なくとも1つのTVarが変更されたときに、競合が発生します。 これは、各インスタンスに格納されている一意の識別子によって確認されます。 ただし、計算でTVarが使用されなかった場合、競合は発生しません。

私たちの実際の環境は、状態とIOモナドのスタックである特定のAtomicモナドによって表現されます。 状態として-すべてのTVarのローカルコピー：

 data AtomicRuntime = AtomicRuntime { ustamp :: UStamp , localTVars :: TVars } type Atomic a = StateT AtomicRuntime IO a 

このモナド内では、相互にネストされた2つの構造を解き、解釈します。 思い出すと、 Free型とSTMF型を使用して構築されるSTML型です。 Freeのタイプは、再帰的であるため、少し頭脳になります。 彼には2つのオプションがあります。

 data Free fa = Pure a | Free (f (Free fa)) 

解釈は単純なパターンマッチングになります。 インタープリターは、トランザクション全体の値、またはトランザクションを再開するコマンドを返します。

 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から作成されます。この関数は、ローカルで変更されたTVarのコンテキストからのグローバルコピーとの競合をチェックし、トランザクションを再開するかどうかを決定します。

 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 Monadを使用したアプローチは非常に柔軟であることがわかり、コードはご自身でわかるようにはるかに小さく、一般的に非常に簡単です。 また、これは、他の言語でのSTMの実装への道を開いているため、優れています。

たとえば、今、私はC ++でFree-monadic STMを移植していますが、これにはこの言語に特有の私自身の困難が伴います。 作業の結果に基づいて、4月C ++ロシア2018会議でレポートを作成し、誰かがそれを訪問する場合は、このトピックをより詳細に議論できます。