冬頃、SPINでPostgreSQLのレプリケーションツールのひとつであるpgpool-IIをモデル検証していたのを思い出したので、一部公開する。
replication-strictモードの挙動
手始めにv2.0で廃止されたreplication-strictモードの挙動をspinで調べてみる。
$ cat pgpool-v2.0-strict.pml /* * pgpool-II:replication-strictモードのモデル検証 * * Copyright (C) 2010 suzuki hironobu _@_ interdb.jp */ #define STRICT #define SERIALIZABLE /* * lock */ mtype {LOCKED, UNLOCKED}; mtype master_mutex = UNLOCKED; mtype slave_mutex = UNLOCKED; inline lock(m) {atomic{ (m == UNLOCKED) -> m = LOCKED}} inline unlock(m) {m = UNLOCKED} /* * chan */ mtype {UPDATE, COMMIT, ABORT, ACK}; mtype {OK, NG}; mtype {P0, P1, P_init}; chan to_master[2] = [0] of {mtype, mtype}; chan to_slave[2] = [0] of {mtype, mtype}; /* * data */ byte master_rowval = P_init; byte slave_rowval = P_init; /* * operations */ inline update (ch, m, rowval) { #ifdef SERIALIZABLE ch?UPDATE(x) -> if :: /* UNLOCKEDなら */ atomic { (m == UNLOCKED) -> m = LOCKED -> ch!ACK(OK) } :: /* LOCKEDなら */ else -> atomic { (m == UNLOCKED) /* UNLOCKEDまで wait */ -> m = LOCKED -> ch!ACK(NG) } fi; #else /* READ_COMMITTED */ ch?UPDATE(x) -> lock(m) -> ch!ACK(OK) #endif } inline commit (ch, m, rowval) { atomic { ch?COMMIT(x) -> rowval = x; unlock(m) -> ch!ACK(OK) } } inline abort (ch, m) { atomic { ch?ABORT(x) -> unlock(m) -> ch!ACK(OK); } } /* * watchdog */ bool pool_end[2]; proctype watchdog() { do :: (pool_end[0] == true && pool_end[1] == true) -> assert(master_rowval == slave_rowval); atomic { pool_end[0] = false; pool_end[1] = false; master_rowval = P_init; slave_rowval = P_init; } od } /* * PostgreSQL */ proctype master(int c) { local mtype x; do :: if :: update(to_master[c], master_mutex, master_rowval) :: commit(to_master[c], master_mutex, master_rowval) :: abort(to_master[c], master_mutex) fi od } proctype slave(int c) { local mtype x; do :: if :: update(to_slave[c], slave_mutex, slave_rowval) :: commit(to_slave[c], slave_mutex, slave_rowval) :: abort(to_slave[c], slave_mutex) fi od } /* * pgpool-II */ proctype pool(int p; mtype P) { local mtype pm, ps; do :: (pool_end[p] == false) -> #ifdef STRICT /* send query to master */ to_master[p]!UPDATE(P); /* wait for response */ to_master[p]?ACK(pm); /* send query to slave */ to_slave[p]!UPDATE(P); /* wait for response */ to_slave[p]?ACK(ps); #else /* send query */ to_master[p]!UPDATE(P); to_slave[p]!UPDATE(P); /* wait for response */ if :: to_master[p]?ACK(pm); to_slave[p]?ACK(ps); :: to_slave[p]?ACK(ps); to_master[p]?ACK(pm); fi; #endif if :: (pm == OK) -> to_master[p]!COMMIT(P); :: else -> to_master[p]!ABORT(P); fi; if :: (ps == OK) -> to_slave[p]!COMMIT(P); :: else -> to_slave[p]!ABORT(P); fi; to_master[p]?ACK(pm); to_slave[p]?ACK(ps); pool_end[p] = true; od } /* * init */ init { pool_end[0] = false; pool_end[1] = false; atomic { run watchdog(); run master(0); run master(1); run slave(0); run slave(1); run pool(0, P0); run pool(1, P1); } end:skip }
まずはreplication-strict=falseの挙動を調べる。
ソースの宣言部のSTRICTとSERIALIZABLEをふたつともコメントアウトする。
これでreplication-strict=false、トランザクション分離レベルはREAD_COMMITTEDになり、
2つのクライアントが同時に同じカラムをupdateする状況を調べる。
具体的には、マスタとスレーブのデータの不一致(watchdog内のassert)と
デッドロック(invalid end states)の可能性について、状態空間の全検索を行う。
/* #define STRICT */ /* #define SERIALIZABLE */
以下のコマンドを実行する。
$ spin -a pgpool-v2.0-strict.pml $ gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=128 -DSAFETY -DNOCLAIM -DXUSAFE -DNOFAIR pan.c $ ./pan -v -m10000 -w19 -c10
すると、以下の結果が得られる。"errors: 2"なのでなんらかのエラーを検出したということである。
pan:1: invalid end state (at depth 76) (Spin Version 5.2.5 -- 17 April 2010) + Partial Order Reduction Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 96 byte, depth reached 111, errors: 2 .... 略 ....
エラーの発生状況をシミュレートして出力する。まず最初のエラーは"-j0"で表示できる。
$ spin -p -v -g -s -r -t -j0 pgpool-v2.0-strict.pml .... 略 .... 77: proc 6 (pool) line 137 "pgpool-v2.0-strict.pml" Recv ACK,OK <- queue 1 (to_master[0]) 77: proc 6 (pool) line 137 "pgpool-v2.0-strict.pml" (state 4) [to_master[p]?ACK,pm] spin: trail ends after 77 steps #processes: 8 master_mutex = LOCKED slave_mutex = LOCKED master_rowval = 9 slave_rowval = 9 pool_end[0] = 0 pool_end[1] = 0 77: proc 7 (pool) line 138 "pgpool-v2.0-strict.pml" (state 7) 77: proc 6 (pool) line 137 "pgpool-v2.0-strict.pml" (state 5) 77: proc 5 (slave) line 100 "pgpool-v2.0-strict.pml" (state 23) 77: proc 4 (slave) line 19 "pgpool-v2.0-strict.pml" (state 5) 77: proc 3 (master) line 19 "pgpool-v2.0-strict.pml" (state 5) 77: proc 2 (master) line 89 "pgpool-v2.0-strict.pml" (state 23) 77: proc 1 (watchdog) line 74 "pgpool-v2.0-strict.pml" (state 8) 77: proc 0 (:init:) line 166 "pgpool-v2.0-strict.pml" (state 12) <valid end state> 8 processes created
ここで、シミュレーションが77ステップ進んだところで、master_mutexとslave_mutexが共に"LOCKED"となりデッドロック状態になったことがわかる。
ちなみに、spin自体はLOCK/UNLOCKを認識しているわけではなく、これ以上シミュレーションが進まないことを認識してその旨表示している。それをユーザである我々が"デッドロックである"と解釈するのである。
2つ目のエラーも同様に表示でき、やはりデッドロックを検出している(clientプロセスが2つあるのでエラー検出も対象的なのである)。
次はreplication-strict=trueの調査。ソースの"#define STRICT"からコメントアウトを外し、
同様の手順を実行する。
#define STRICT /* #define SERIALIZABLE */
以下が実行結果。今度は"errors: 0"。よってデータの不一致もデッドロックも起きないことがわかる。
.... 略 .... State-vector 96 byte, depth reached 111, errors: 0 .... 略 ....
SERIALIZABLEでの挙動
次にトランザクション分離レベルをREAD COMMITTEDからSERIALIZABLEにして検査する。
#define STRICT #define SERIALIZABLE
すると"errors: 4"になってしまう。
pan:1: assertion violated (master_rowval==slave_rowval) (at depth 111) (Spin Version 5.2.5 -- 17 April 2010) + Partial Order Reduction Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 96 byte, depth reached 355, errors: 4 .... 略 ....
出力をよく読むと、マスタとスレーブで値の不一致が起きている(assert(master_rowval==slave_rowval)が不成立する状態が検出された)。
pan:1: assertion violated (master_rowval==slave_rowval) (at depth 111)
pgpool-II:v.2.2の修正を反映
実は、上記の挙動はv2.2で修正されたバグを再現している。
トランザクションをシリアライズできないエラーが発生したときに、 すべてのDBノードのトランザクションをアボートするようにしました。 こうしないと、DBノードの間でデータの不整合が起きることがあります(Tatsuo)。 例を示します(Mはマスタ、Sはスレーブを示します)。 M:S1:BEGIN; M:S2:BEGIN; S:S1:BEGIN; S:S2:BEGIN; M:S1:SET TRANSACTION ISOLATION LEVEL SERIALIZABLE; M:S2:SET TRANSACTION ISOLATION LEVEL SERIALIZABLE; S:S1:SET TRANSACTION ISOLATION LEVEL SERIALIZABLE; S:S2:SET TRANSACTION ISOLATION LEVEL SERIALIZABLE; M:S1:UPDATE t1 SET i = i + 1; S:S1:UPDATE t1 SET i = i + 1; M:S2:UPDATE t1 SET i = i + 1; <-- blocked S:S1:COMMIT; M:S1:COMMIT; M:S2:ERROR: could not serialize access due to concurrent update S:S2:UPDATE t1 SET i = i + 1; <-- success in UPDATE and data becomes inconsistent!
新しいモデルのソースを以下に示す:
$ cat pgpool-v2.2-serializable.pml /* * pgpool-II:v.2.2で修正されたバグの再現と修正: * * Copyright (C) 2010 suzuki hironobu _@_ interdb.jp */ #define SERIALIZABLE #define OLD_VERSION /* * lock */ mtype {LOCKED, UNLOCKED}; mtype master_mutex = UNLOCKED; mtype slave_mutex = UNLOCKED; inline lock(m) {atomic{ (m == UNLOCKED) -> m = LOCKED}} inline unlock(m) {m = UNLOCKED} /* * chan */ mtype {UPDATE, COMMIT, ABORT, ACK}; mtype {OK, NG}; mtype {P0, P1, P_init}; chan to_master[2] = [0] of {mtype, mtype}; chan to_slave[2] = [0] of {mtype, mtype}; /* * data */ byte master_rowval = P_init; byte slave_rowval = P_init; /* * operations */ inline update (ch, m, rowval) { #ifdef SERIALIZABLE ch?UPDATE(x) -> if :: atomic { (m == UNLOCKED) -> m = LOCKED -> ch!ACK(OK) } :: else -> atomic { (m == UNLOCKED) -> m = LOCKED -> ch!ACK(NG) } fi; #else /* READ_COMMITTED */ ch?UPDATE(x) -> lock(m) -> ch!ACK(OK) #endif } inline commit (ch, m, rowval) { atomic { ch?COMMIT(x) -> rowval = x; unlock(m) -> ch!ACK(OK) } } inline abort (ch, m) { atomic { ch?ABORT(x) -> unlock(m) -> ch!ACK(OK); } } /* * watchdog */ bool pool_end[2]; proctype watchdog() { do :: (pool_end[0] == true && pool_end[1] == true) -> assert(master_rowval == slave_rowval); atomic { pool_end[0] = false; pool_end[1] = false; master_rowval = P_init; slave_rowval = P_init; } od } /* * PostgreSQL */ proctype master(int c) { local mtype x; do :: if :: update(to_master[c], master_mutex, master_rowval) :: commit(to_master[c], master_mutex, master_rowval) :: abort(to_master[c], master_mutex) fi od } proctype slave(int c) { local mtype x; do :: if :: update(to_slave[c], slave_mutex, slave_rowval) :: commit(to_slave[c], slave_mutex, slave_rowval) :: abort(to_slave[c], slave_mutex) fi od } /* * pgpool-II */ proctype pool(int p; mtype P) { local mtype pm, ps; do :: (pool_end[p] == false) -> /* send query to master */ to_master[p]!UPDATE(P); /* wait for response */ to_master[p]?ACK(pm); /* send query to slave */ to_slave[p]!UPDATE(P); /* wait for response */ to_slave[p]?ACK(ps); #ifdef OLD_VERSION if :: (pm == OK) -> to_master[p]!COMMIT(P); :: else -> to_master[p]!ABORT(P); fi; if :: (ps == OK) -> to_slave[p]!COMMIT(P); :: else -> to_slave[p]!ABORT(P); fi; to_master[p]?ACK(pm); to_slave[p]?ACK(ps); #else if :: (pm == NG || ps == NG); /* abort */ to_master[p]!ABORT(P0); to_master[p]?ACK(pm); to_slave[p]!ABORT(P0); to_slave[p]?ACK(ps); :: else -> to_master[p]!COMMIT(P0); to_master[p]?ACK(pm); to_slave[p]!COMMIT(P0); to_slave[p]?ACK(ps); fi; #endif pool_end[p] = true; od } /* * init */ init { pool_end[0] = false; pool_end[1] = false; atomic { run watchdog(); run master(0); run master(1); run slave(0); run slave(1); run pool(0, P0); run pool(1, P1); } end:skip }
ここで以下の条件でspinを実行する。
#define SERIALIZABLE /* #define OLD_VERSION */
$ spin -a pgpool-v2.2-serializable.pml $ gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=128 -DSAFETY -DNOCLAIM -DXUSAFE -DNOFAIR pan.c $ ./pan -v -m10000 -w19 -c10
実行結果は、めでたく"errors: 0"である。
(Spin Version 5.2.5 -- 17 April 2010) + Partial Order Reduction Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 96 byte, depth reached 205, errors: 0 .... 略 ....
今後
pgpoolのモデル化の主目的は:
- まだ隠れているバグの検出
- 障害時の挙動調査
で冬頃に始めていた。が、ちょっと時間を空けたら自分でもソースが読めなくなっている。
下記のように、非同期通信を前提とすると、STRICT=trueでもデッドロックやデータのズレが生じるモデルも作ったのだが、ソースがどこかに行ってしまった。
今後、pgpoolについては：
をやってみるつもりである。
さらにpgpoolだけでなく、PostgreSQLのSRやPostgres-XCなどクラスタリング関連のモデル検証を行うつもりである。というか、もともとSRやXCの分析を始めてしまったのでpgpoolのモデル化が中断してしまったのだが。
