1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

ユニークビジョン株式会社Advent Calendar 2024

Day 18

バグに遭遇したのでSPINを使って考えてみた

Last updated at Posted at 2024-12-24

先日、あるバグに遭遇しました。バグに遭遇することなど、プログラマをやっていれば日常茶飯事のことで、特筆するべきことでもないのですが、アドベントカレンダーの季節なので、せっかくなのでネタにしよう、と筆を取った次第です。

そのシステムはRailsで作られたアプリケーションで、ユーザからリクエストを受け、呼び出されたControllerがSidekiqにジョブを流し、バックグラウンドでタスクを複数実行していました。

  • タスクA
  • タスクB

タスクA内ではタスクBをさらにSidekiqへジョブを投入している(このタスクをタスクβと呼称します)、という作りになっていました。なお、この文章では、この作りが妥当なものなのか、という点については話題に上げません。ここで扱う内容は、こう作られていたらバグっていた、という事実のみです。

タスクBはシステム内の複数のリソースを集計し、集計結果を特定の場所に格納する、という処理を実行します。タスクAはタスクBの集計対象となるリソースを更新した後、タスクBを実行する、という流れです。

バグは、タスクAでリソースXが更新される状況が発生しているにも関わらず、リソースXが更新されないことがある、というものでした。

当初、Sidekiqが一つのコントローラ内から複数起動していたり、ローカル環境では再現しなかったりしたので、何か特別なことをしているのではないかと身構えながらコードを読んでいったのですが、バグの原因はタスクBが実行しているストアドファンクションと、タスクAとタスクBとが順々にに実行されると思った大昔の実装者の勘違いでした。

ストアドファンクションは次のような処理を実行していました。

  1. 起動時刻を変数に保存する
  2. リソースXを算出するために集計を行う
  3. 1で保存した変数が、リソースXの更新日時より古いか等しい場合、リソースXを2で算出した値を用いて更新し、新しかったならば、更新をしない。また、リソースXを更新する際に記録する更新日時は1の値とする

既に察しがついている方も多いでしょうが、ストアドファンクションの処理1、2、3、及びSidekiqから起動されるジョブ全般にわたって、処理がアトミックになることを保証している部分はありませんでした。よって、タスクAが起動し、その後タスクBが起動して、それが終了する前にタスクβが起動し、その状態でタスクBが終了すると、タスクAで行なったリソースXへの更新処理が、実行されないことがある、という状態が発生しえます。

タスクA起動 --> タスクB起動 --> タスクβ起動 --> タスクB終了 --> タスクβでリソースXが更新されずに終了

今回はせっかくなのでSPINを持ち出して簡単なモデル検証をし、このバグについて考えてみました。SPINやモデル検証については今回は記述しません。詳しいことはWikipediaの「SPINモデルチェッカ」の項に書いてありますし。

まずこの問題の本質的なことを抽出します。

SidekiqでタスクB、タスクAが起動云々、と書きましたが、モデス化する際には、平行にたくさん起動される、としてしまいました。Sidekiqへ放りこまれたジョブの実行順序など考えていられません。ようはたくさん一緒に起動したと考えればよいのです(暴論)。

次にストアドファンクションの部分です。1に起動時刻云々とありましたが、起動のタイミングで値をインクリメントする変数で代替しました。PROCNUMを2以上にした場合、複数のプロセスが同一の値を持つ状態になるケースは発生しますが、これは同一時刻に起動された、と考えればよいでしょう。その場合、双方で更新処理が実行されます。

2の集計処理ですが、これは別にどんな処理であろうと、リソースXが更新されるかどうかについては関係ないので無視します(あくまでも今回の問題では、です。タスクAとタスクBの実行開始時間が十分離れるような場合だと色々と影響が出てくると思います)。

最後のリソースXの更新については、これはインクリメントする変数を、別途用意した変数に代入するという行為で代替しました。

これらの事情を考慮し、Promelaで記述してみました。

#define PROCNUM 1

int count = 0
int current_count = 0

active [PROCNUM] proctype Updater()
{
  do
    :: count = count + 1 ->
      if
         :: (current_count < count) -> current_count = count; printf("%d\n", count);
         :: else -> assert(false); printf("error \n");
      fi
  od
}

まずPROCNUMは、同時に実行されているタスクBの数です。1の値を与えた場合、冒頭で開発環境では発生しない、と書きましたが、タスクが順序よく、終了を待って実行された状態を表現できると考えました。これをSPINで実行すると、ひたすらインクリメントされる数字が表示されます。よって、errorの方には流れていません。

PROCNUMの値を2以上にした場合、先程暴論と称した「たくさん」起動した状態(2であれば2で、たくさんという文字通りの状態を作りたいのであればこの数を増やせばよい)がつくれます。その結果は、elseへ処理が流れ、動作が停止します。spin -u100 "ファイル名.p"としたとしても、100まで実行する以前で処理が終了します。その際、終了のタイミングはランダムです。

これらによって、開発環境では発生しない(sidekiqのconcurrencyの設定値を低くしているので、結果的に順々に処理が実行されていると推測している)、本番環境では発生したり発生しなかったりする、という状況を再現することができました。ただ、かっこ書きをした推測もあるので、間違っている可能性もありますが、大きく外してはいないでしょう(多分)。

さて、このバグの修正方法を検討し、モデル化し、SPINを利用して検証するところまで行なってはじめて、このツールの使い方を記述した価値ある記事になりえるはずですが、そろそろ夜も遅くなってきたので、それはまたの機会にしたいと思います。

ではよいお年を。

1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?