昨日の記事「メイヤー代数やメイヤー加群はまだ整理不足」において、
双代数の条件を入れておいたのはトランザクションのためでした。トランザクションは、「更新オペレータをローカルでキューイングする」方式を前提とします。
と書きました。
ここで、トランザクションについてザッと説明しておきます。下の絵のような3つの方式について紹介して、僕の立場からのコメントを付けます。それぞれの方式を切り離した絵も後に再掲します。
詳細はともかく、絵の見方は:
- 時間は上から下の方向に経過します。
- Sは状態空間です。データベースの可能なすべての状態の集合と考えればいいでしょう。
- Vは状態の観測値の集合です。観測値は状態に関する部分的な情報を提供します。
- fは状態を変更する処理を行うプログラムです。
- Mは状態を更新するオペレータの集まり、モノイドとなります。
- 黒三角はデータのコピー(クローン)です。
- S→S×V という枝分かれは余作用(後述)です。
- S×M→S という合流は作用(後述)です。
- 他のシルシは後で説明します。
時間は上から下に流れますが、処理の前段と後段に分かれています。前段でfが処理を行なって、後段ではコミット(OKのとき)またはキャンセル(NGのとき)をします。後段では、OKかNGのどちらか一方のケースが実行されます。
コピー方式のトランザクション処理(?)
見出しに「(?)」が付いているのは、「トランザクション処理」って呼んでいいかどうかちょっと疑問だからです。コピー方式は原始的な方法で、処理を始める前に、状態のフルバックアップをとっておきます。黒三角はコピーでした。s∈S に対して s|→(s, s) と対応させるのがコピーです。コピーは ΔS:S→S×S とも書かれ、Sの対角写像と呼ばれることもあります。
コピーした状態の片一方にfが処理をします。fは f:S→S という写像です。f(s) = s' とすると、何もしてないほうのコピーとペアにして (s, s') というデータが出来ます。ここまでが前段です。
下向きの白三角はデータを捨てる操作を表します。処理が成功(OK)のときは、(s, s')|→s' (もとのsを捨てる)なので、コミットになります。処理が失敗(NG)なら、(s, s')|→s (処理したs'を捨てる)でキャンセルですね。
これは、対角写像Δと直積の射影 π1, π2 だけでトランザクションを組み立てています。原始的なゆえに汎用性があります。しかし、フルバックアップを作るのは重いのが欠点です。
キューイング方式のトランザクション処理
フルバックアップをとった上でfが状態を直接更新するのではなくて、fが状態を観測して、必要な更新をオペレータとして出力する方式があります。
Vは観測値の集合なので、図の枝分かれは、c:S→S×V という観測操作です。観測操作cを余作用(coaction)とも呼びます。観測は状態を変更することはないので、q:S→V という写像を使って、c(s) = (s, q(s)) と書くこともできます。このときのqは、メイヤーの意味のQueryです。
Mは更新オペレータの集合でした。x∈M に対して a(s, x) = s' と更新を実行する写像aを作用(action)と呼びます。a:S×M→S です。
処理が成功したら、更新オペレータ(Mの要素)による作用を実行し、処理が失敗なら更新オペレータを捨てます。fが直接的にSに影響を与えないで、いったん更新オペレータをキュー(待ち行列)に入れるので、これはキューイング方式と呼んでいいでしょう。実際には、fは複数の処理単位の順次結合 f = f1;f2; ... ;fn となるので、キューにオペレータを順次入れてって貯める感じになります。
アンドゥ方式のトランザクション処理
3つ目はアンドゥ方式です。アンドゥよりロールバックと呼ばれることが多いかな。
S、V、M はキューイング方式と同じ意味です。fは、処理の前段で、実際にSへの作用を実行してしまいます。その代わり、アンドゥの準備をします。白い小さな箱はアンドゥ・オペレータを作り出す操作で、u:V×M→M という形をしてます。uの出力が実際に作用を取り消すことは次の等式で示せます。aは作用、qはメイヤーのQueryです。
- s' = a(s, x) として、a(s', u(q(s), x)) = s
処理が成功したら、アンドゥ・オペレータ(Mの要素)を捨て、処理が失敗ならアンドゥ・オペレータを作用させて変更をもとに戻します。
fが複数の処理単位の順次結合 f = f1;f2; ... ;fn だと、実際の作用が何度も実行され、アンドゥ・オペレータも(キューイング方式と同様に)累積されます。
僕がキューイング方式を選ぶ状況とワケ
それぞれの方式に一長一短があるので、どれが良いという絶対的基準はありません。状況によりけりです。
状態空間Sがリモートのデータベースサーバーで実現されているような場合で、トランザクション処理への要求がさほどに厳しくないなら、キューイング方式が良いだろうと思います。
アンドゥ方式は、図を見ても分かるように複雑です。それと、処理の前段で実際に状態を変更してしまうのですよね。後でアンドゥは出来るわけですが、確実にアンドゥ出来ることを保証するには、DoとUndoの間に他の処理が割り込まないようにしなければいけません。つまり、トランザクションのあいだずっと状態空間を専有する必要があります。
キューイング方式では、トランザクションの最後で1回しか実際の変更を試みません。失敗か成功かは楽観的並行性制御により判断すればいいでしょう。アンドゥ方式に比べると処理も単純です。とはいえ、「メイヤー代数やメイヤー加群はまだ整理不足」で述べた同型が成立することがキューイング方式の前提です。トランザクション処理も、ある種の代数的な法則に支えられているのです。