DeNA Testing Blog

Make Testing Fun, Smart, and Delighting End-Users

Gradle Managed Devicesでテストを動かしてみよう

こんにちは。SWETのAndroidチームに所属している外山(@sumio_tym)です。 SWET AndroidチームではAndroidのプロダクトに対して自動テストのサポートをしています。

はじめに

先日開催されたDroidKaigi 2022で「Gradle Managed Virtual Devicesで変化するエミュレータ活用術」というタイトルで登壇しました。

本セッションの動画もYouTubeのDroidKaigiチャンネルに公開されていますので、合わせて参考にしてください。

さて、本記事では、上記セッションの内容から開発PC上でGradle Managed Devices (GMD)を試すのに必要な部分だけを抜粋して紹介していきます。 本記事を読むだけで手っ取り早くGMDを試せるように構成してありますので参考にしてみてください。

Gradle Managed Devices (GMD)とは

Gradle Managed Device(GMD)とは、Gradle Managed Virtual Devicesとも呼ばれる機能で、Android Gradle Plugin 7.3より本格的に導入されました。 本機能を使うと、build.gradleに使いたいエミュレータの情報を書くだけで、Gradleタスクひとつ(コマンドひとつ)で次の一連の工程を実行できるようになります。

  1. build.gradleで指定されたエミュレータ種別に合うAVD(Android Virtual Device)を作成する
    (すでにあれば再利用する)
  2. 作成したAVDでエミュレータを起動する
  3. 起動したエミュレータ上でテスト(Instrumented Test)を実行する
  4. テスト実行が終わったら、インストールしたアプリ(apk)を削除する
  5. 起動したエミュレータを終了する
  6. テスト結果レポートや実行ログを保存する

build.gradleの記載内容だけでテストを実行するエミュレータの環境が定まり、コマンドひとつで実行できることから、次のようなメリットが得られます。

  • 開発者が手動で(Android Studioを操作して)AVDを作成しなくてよい
  • テスト実行時におけるエミュレータの環境差異をなくせる
    • エミュレータを使ったテストのCI上での実行が簡単にできる

GMDのセットアップとタスクの実行

GMDを使うための手順は次のような流れになります。順を追って説明します。

  1. 利用するAGP(Android Gradle Plugin)のバージョンをGMD対応版にする
  2. build.gradleにテストを実行したいAVD(エミュレータの種別など)を定義する
  3. GMD上でテストを走らせるGradleタスクを実行する

Android Gradle Pluginのバージョン指定

前述のとおり、GMDに本格対応したバージョン7.3.0以降を使うようにしてください(本原稿執筆時点では7.3.1が最新の安定バージョンです)。

buildscript {
  ...
  dependencies {
    classpath "com.android.tools.build:gradle:7.3.1"
    ...
  }
}

テストを実行したいAVDの定義

モジュールレベルのbuild.gradleapp/build.gradleなど)に次の形式で定義します。

android {
  testOptions {
    managedDevices {
      devices {
        pixel5api33 (ManagedVirtualDevice) { //・・・(1)
          device = "Pixel 5"                 //・・・(2)
          apiLevel = 33                      //・・・(3)
          systemImageSource = "google"       //・・・(4)
          require64Bit = false               //・・・(5)
        }
      }
    }
  }
}

それぞれの指定の意味は次のとおりです
(番号は上記ビルド定義ファイル中のコメントと対応しています)

  • (1) pixel5api33: デバイス(AVD)を一意に識別する名前を指定します。適当な名前を付けてください
  • (2) device: Device Profileを指定します。 Android StudioのDevice Manager>Create deviceで表示されるデバイス名から選択してください
  • (3) apiLevel: 起動したいエミュレータのAPI Levelを指定します
  • (4) systemImageSource: 利用するシステムイメージの種別を指定します。後述します
  • (5) require64Bit: 64ビットのABIを強制的に使うか否かを指定します。通常はfalseで問題ありません

systemImageSourceで指定できるシステムイメージの種別は次のとおりです。

従前のシステムイメージ ATD
無印(AOSP) aosp aosp-atd
Google APIs google google-atd
Google Play google_apis_playstore N/A

表の右カラムに記載されているATD(Automated Test Device)は、Instrumented Test用途に最適化された軽量版のシステムイメージで、本原稿執筆時点ではAPI Level 30と31で利用可能です。 ATDではハードウェアレンダリングが無効化され、さらにテストで使わなさそうなアプリやサービスが削除・無効化されています。 削除・無効化されている機能の一覧は公式ドキュメントを参照してください。これらの機能なしでテストが動きそうであればATDを試してみるのもよいと思います。

Gradleタスクの実行

GMD上でテストを走らせるGradleタスクは次の形式になっています

{デバイス名}{ビルドバリアント}AndroidTest

たとえば、デバイス名pixel5api33に対して、debugビルドバリアント(フレーバー未定義でビルドタイプがdebugの場合)のテストを走らせたい場合は、次のコマンドでテストを実行できます。

./gradlew pixel5api33DebugAndroidTest

テストの結果レポートやログは次のディレクトリに保存されます。

  • app/build/outputs/androidTest-results/managedDevice/flavors/{フレーバー名}/{デバイス名}/
    • JUnit互換のテスト結果XML
    • ログ(logcatや、AGPが内部で実行したadbなどのコマンドログ)
  • app/build/reports/androidTests/managedDevice/flavors/{フレーバー名}/{デバイス名}/
    • HTML形式のテスト結果レポート

知っておくと便利なテクニック

GMDは、コマンド1つでエミュレータ上でのテストの実行を完結してくれる反面、運用上使いにくいと感じる場面もあります。 たとえば、次のような場面です。

  • テスト実行中の画面が見えない
  • テストが終わるとapkがアンインストールされてしまうため、テスト実行中に作られたファイルも消えてしまう
  • Android Studioでじっくりデバッグできない

これらの問題解決の助けになるテクニックを3つ紹介します。 この3つのテクニックを知っておくと、GMDを試すときの動作確認が格段にやりやすくなります。是非お試しください。

テスト実行中に画面を表示する--enable-display

GMDによるテスト実行タスクに--enable-displayオプションを付けると、テスト実行中にエミュレータの画面が表示されます。 テスト失敗時に画面の状態を目視したいときなどに便利です。

./gradlew pixel5api33DebugAndroidTest --enable-display

なお、軽量版システムイメージであるATDでは、本オプションを付けても真っ黒な画面しか表示されません。ご注意ください。

テスト終了時にファイルをpullするadditionalTestOutputDir

Test Instrumentation Runnerに渡せるadditionalTestOutputDir引数にディレクトリを指定すると、 テスト終了時にそのディレクトリ内のファイルをpullさせることができます。

android {
  defaultConfig {
    testInstrumentationRunnerArgument(
        "additionalTestOutputDir",
        "/sdcard/Android/media/com.example.gmd/result"
    )
  }
}

テストが終了するときに、この例ではエミュレータのディレクトリ/sdcard/Android/media/com.example.gmd/result内のファイルを開発PCに取り出します。

取り出されたファイルはapp/build/outputs/managed_device_android_test_additional_output(AGPのバージョン8.0以上ではapp/build/intermediates/managed_device_android_test_additional_output)ディレクトリに保存されます。 テスト実行中に保存したスクリーンショットファイルやログファイルを取り出したいときなどに便利です。

なお、Scoped Storageが有効なOSのバージョンでは、本オプションに指定できるディレクトリのパスに制限があります。 /sdcard/Android/media/{アプリケーションID}/のような、アプリから書き込めて、かつadb pullできるディレクトリを指定するようにしてください。 その条件を満たさないパスに保存したファイルは本オプションを指定しても取り出せません。

GMDで使われるAVDでエミュレータを起動できるANDROID_AVD_HOME環境変数

GMDによるテストで使われるAVD(Android Virtual Device)は隠されており、Android StudioのDevice Managerからは確認できません。 そのため、GMDで使われるのと同じAVDのエミュレータに対してAndroid Studioからテストするには、コマンドラインを使って事前に対象のエミュレータを起動しておく必要があります。

これから説明する方法でエミュレータの起動さえできてしまえば、普段どおりAndroid Studioからアプリのインストール・デバッグ実行・テストの実行などが行えます。 この方法でテストが十分安定して動くことを確認してから、最終確認としてGMDでテストを実行するようにすると、あまり手戻りすることなくテストを書き進められます。

GMDで使われるAVDが表示されない理由は、デフォルトの場所($HOME/.android/avd)にAVDが保存されていないからです。 Android Gradle Plugin 7.3以上であれば、GMDで使われるAVDは次のディレクトリに保存されています。

$HOME/.android/avd/gradle-managed

このディレクトリを環境変数ANDROID_AVD_HOMEに指定してemulatorコマンドを実行すると、GMDで使われるAVDのエミュレータを起動できます。

まず目的のAVD名を特定するところから始めます。 GMDで使われているAVDの一覧を表示するには次のコマンドを実行してください。 emulatorコマンドは($ANDROID_HOME/toolsではなく)$ANDROID_HOME/emulatorディレクトリにあるものを使ってください。

env ANDROID_AVD_HOME=$HOME/.android/avd/gradle-managed $ANDROID_HOME/emulator/emulator -list-avds

dev33_google_x86_64_Pixel_5 のような、APIレベル・システムイメージ・ABI・Device Profileを組み合わせたAVD名の一覧が表示されますので、目的のAVDをみつけてください。

目的のAVDをみつけたら、次のコマンドでエミュレータを起動できます。

env ANDROID_AVD_HOME=$HOME/.android/avd/gradle-managed $ANDROID_HOME/emulator/emulator -avd {AVDの名前}

直前にGMDでテストを実行している場合は別の手段を取ることもできます。GMDの実行ログを活用する方法です。 エミュレータを起動したときの実行ログは次のファイルに保存されています。

app/build/outputs/androidTest-results/managedDevice/flavors/{フレーバー名}/{デバイス名}/emulator.1.ok.txt

このファイルを開くと次のような内容になっているはずです。

EXECUTING: /usr/local/share/android-sdk/emulator/emulator @dev33_google_apis_x86_64_Pixel_5 -no-window -no-audio -gpu auto-no-window -read-only -no-boot-anim -id :app:pixel5api33googleDebugAndroidTest
CURRENT_WORKING_DIRECTORY: (略)
START_TIME: 2022-10-04 22:26:40.754
START_TIME-NANOS: 2022-10-04 22:26:40.754965000
ENVIRONMENT:
(略)
ANDROID_AVD_HOME=/Users/sumio.toyama/.android/avd/gradle-managed
*****************************************
STDOUT/STDERR BELOW
===================
INFO    | Android emulator version 31.3.10.0 (build_id 8807927) (CL:N/A)
(略)
===================
END_TIME: 2022-10-04 22:28:27.392
END_TIME-NANOS: 2022-10-04 22:28:27.392521000
DURATION: 106637ms
EXIT CODE: 0

ENVIRONMENT欄に書かれているANDROID_AVD_HOME環境変数を指定しつつ、EXECUTING欄に書かれているコマンドを実行すると目的のエミュレータを起動できます。

ただし、このファイルに記載されているコマンドラインオプションのままだとエミュレータの画面が表示されないため、-no-windowオプションは外して起動してください。 起動したエミュレータを操作した後の状態を永続化したいときは-read-onlyオプションも外す必要があります。

両方のオプションを外した場合、このemulator.1.okの例だと目的のAVDでエミュレータを起動するコマンドは次のようになります。

env ANDROID_AVD_HOME=/Users/sumio.toyama/.android/avd/gradle-managed \
    /usr/local/share/android-sdk/emulator/emulator @dev33_google_apis_x86_64_Pixel_5 \
    -no-audio -gpu auto-no-window -no-boot-anim -id :app:pixel5api33googleDebugAndroidTest

まとめ

DroidKaigi 2022で発表した「Gradle Managed Virtual Devicesで変化するエミュレータ活用術」の内容から、 開発PC上でGradle Managed Devices(GMD)を試すのに必要な部分を抜粋して紹介しました。

DroidKaigi 2022のセッションでは、ここで触れられていない次の内容についても説明しています。 より深くGMDに触れてみたい方は、是非そちらもご覧ください。

  • GMDの使い方
    • 複数のデバイスをまとめてテストできるデバイスグループの使い方
  • Tips
    • デバイスの言語を(日本語などの)英語以外の言語に変更してからテストを実行する
    • build.gradleでは設定できない項目(ストレージ容量など)を変更する
    • テストを録画する
    • GMDで使うエミュレータが不安定になったときにCold Bootする
    • GMDで使うエミュレータをキッティングする
    • 複数のデバイスをまとめてテストすると動作が不安定になる場合の回避策
  • テストの種類別GMD活用シーン
    • Robolectricが必要なLocal Testの移行
    • UIテスト
    • スクリーンショットテスト
  • CI環境で動かすときのポイント

個人的には、今回の登壇は久しぶりのオフライン登壇でした。 久しぶりの雰囲気に緊張しつつも、聴きに来て下さった皆さんの様子を見ながら話すことの楽しさを改めて実感しました。 このような機会を提供して下さったDroidKaigi 2022スタッフをはじめ、関係者のみなさんに感謝いたします。

宣伝

この記事を読んで「面白かった」「学びがあった」と思っていただけた方、よろしければTwitterやfacebook、はてなブックマークにてコメントをお願いします。

また DeNA 公式 Twitter アカウント @DeNAxTech では、Blog記事だけでなく色々な勉強会での登壇資料も発信してます。ぜひフォローして下さい!

Lintを使う人、作ってみたい人、問題解決の引き出しを増やしたい人のための勉強会Lint Nightを開催します!

SWETグループのLint大好きマンKuniwakです。2022/11/18にオフライン・オンライン同時開催の勉強会「Lint Night #1」を開催します!

Lint Nightはプログラミング言語不問でLintに関するトピックを取り扱う勉強会です。ここでLintとはソースコードや文書を静的に解析して問題をみつけるツールのことです。ただ、どこまでをLintとするかには幅があるようです。

さて、Lintの面白いところはソースコードや文書を入力データとして扱うプログラムであることです。ソースコードを入力データとするプログラムといえばコンパイラやインタプリタがあげられますがいずれも実装がかなり大変です。しかしLintはそこまでではありません!実は手軽に実装できるんです(Lintの作り方については次のスライドをご覧ください)。

しかもそれでいてコードレビューを一部自動化できて実用的ですし、ソースコードや文書を入力とするプログラムは応用の幅も広い!

実際に私は業務で何度もLintの関連技術で問題を解決してきました。たとえば、巨大なCSSをバグ0でCSS→Less移行した時にもLintの技術を応用しましたし、C#で作られたアプリケーションのバグを分析するための大規模データ収集にもLintの技術を応用しました。ソースコードや文書を入力データとして扱うプログラムはこのように応用が広いのです。

この話はいくらでも続けられるのでこの辺りで切り上げますが、まさにこのようなLintの話を言語不問でできる勉強会があったらいいなと思いLint Nightを企画しました。

Lintを使ったことがある人、Lintを作ってみたい人、なんでもいいから問題解決の引き出しを増やしたい人、ぜひご参加ください!Lint NightはLintに興味のあるすべての方のための勉強会です。

初回の発表者は、Rubyの代表的なLintであるRuboCopのcore teamメンバーである@koicさんと、textlintの開発者である@azu_reさんです。

twitter.com twitter.com

それでは11/18のLint Night #1でお会いしましょう!

lintnight.connpass.com

夜開催のiOS Test Onlineを開催しました!

SWETグループのKuniwakです。2022/10/28にiOS Test Onlineを開催しました!

さて、今回の発表の録画とスライドを紹介していきます。

録画

YouTubeにパネルディスカッションを除く発表をアップロードしました。パネルディスカッションはリアルタイムにしか聞けないコンテンツにしたいので、次回以降ぜひリアルタイムにご参加ください!

聴衆の反応

iOS Test Online でわいわいしている人たちにtweetをまとめました。

発表スライド紹介

@orga_chem「実践 9つのメモリリークどう見つける?」

@the_uhooi「新規アプリの単体テスト戦略」

@treastrain「Bitrise Pipelines に移行して、クレジットを節約しながら並列でビルド・テストを回す」

次回開催の発表募集!

発表内容は、たとえば「テストはじめて書いてみたよ」や「このテストツール便利だったよ」あるいは「私がテストを書かない理由」でも大歓迎です!発表したい方は次のGoogle Formからご応募ください!なお、開催日は発表者が集まれる日で調整する予定です。

iOS Test Online発表応募フォーム

過去の発表資料を参考にしたい方は次の過去の発表資料をご覧になるとよいでしょう:

皆様からの発表のご応募お待ちしております!

macOSのCopy-on-Write機能を使ってディスクを節約した話

こんにちは、SWETでCI/CDチームの前田( @mad_p )です。 SWETではCI/CDチームの一員として、Jenkins運用のサポートや、CI/CD回りのノウハウ蓄積・研究をしています。

はじめに

先日開催されましたCEDEC 2022にて、Gitリポジトリの肥大化に対応した事例を発表しました。これはそのフォローアップ記事となります。以前に出した記事の続編でもあります。

発表資料は次の場所に置いていますので、参照してみてください。

Gitリポジトリの肥大化問題

前提となっている課題をおさらいしておきます。 Gitリポジトリは、コミットを重ねることで大きくなっていきます。 大きくなると、クローンにかかる時間や、クローン後の.gitを保存するためのディスク容量が多く必要になります。 その結果、CIの実行時間・CIマシンのディスク不足などの心配事が増えます。 特にディスク不足に関しては、.gitの容量とチェックアウトしたファイルの容量のダブルでディスク消費が増えるので注意が必要です。

Jenkinsマシン上では、同一のリポジトリをジョブ別の複数フォルダにクローンすることになります。 多くのジョブで活用されるリポジトリは、ディスク容量不足の原因となりやすいです。 今回の事例で節約対象としたJenkinsマシンでは、20か所以上にクローンされているリポジトリもあります。

今回紹介する事例について

今回紹介する事例の背景を少し説明したいと思います。 対象のJenkinsマシンは、あるモバイルゲームタイトルのCIを支えているものです。

そのゲームはリリースから数年経っていて、 毎月のイベントごとにアプリ更新とキャラクターの追加があります。 この月次のリリースに対応して、ソースコードやアセットのブランチを管理しています。

プロジェクト内の大きなリポジトリのトップ4はこんな感じです(クローン後の.gitの容量)。

  • アセット(22GB)
  • アセットバンドル(LFS利用、16GB)1
  • アセットソース(15GB)
  • アプリ(3.4GB)

一番大きいアセットリポジトリを使ったジョブが一番種類が多く、 大きさ×ジョブ数で、ディスクを多く必要とします。

Jenkinsマシンはオンプレ・クラウド合わせて15台くらいで運用しています。 macノードが、慢性的なディスク容量不足に悩まされていて、 ここをなんとかしたいというのが動機です。

すでに紹介した対応方法と効果

前回のブログ記事で説明した方法を使って節約できた容量を紹介します。 ある1台のmacノードでの成果を調べてみました。

リファレンスを活用したクローンでは、.gitの、ディスク容量とダウンロード時間を節約できました。

リファレンスの活用

よく使うリポジトリの上位5つくらいを、リファレンスとして使うためのミラーとして用意しておきます。 定期的にフェッチするようにして、ある程度最新の状態になるように保っています。 Jenkinsのジョブでクローンするとき、 ミラーをリファレンスとして使うようにオプションを設定します。 これによって、20個以上の.gitをひとつにまとめることができました。

リファレンス設定のファイルを数えて調べたところ、 容量×参照数で、820GB程度の必要量を60GBにまとめることができています。 元々シャロークローンで足りていた部分もあると思うので、 実質の節約量は引き算した760GBとはいかず半分くらいかもしれません。 思っていたよりたくさん節約していたことがわかりました。

LFSローカルストレージの共有化では、 .git/lfsのディスク容量とダウンロード時間を節約できています。

LFSローカルストレージ共有

こちらは、現状での節約量を調べるのは難しかったので、 導入当時の記録を調べました。 複数フォルダの合計で90GB程度だったものが、まとめて20GBになったとありました。

copy-on-write機能を使ってディスクを節約した事例

それでは、本題のcopy-on-write活用について説明しましょう。

次の問題: チェックアウトしたファイルの容量が大きい

.gitの容量問題が解決したのですが、まだディスク残量が厳しい状況でした。 次の要因としては、チェックアウトしたワーキングツリーの容量が大きそうです。

どんなデータがJenkinsマシンのディスク内で容量を使っているかを調査してみました。 その結果、ジョブ内で参照するアセットデータが大きいとわかりました。 特に、キャラクターのモデルやモーションのデータが大きいです。 スパースチェックアウトが使えないかな、と思いましたが、 キャラクターデータを部分的に扱うジョブというのはなく、 うまくいかなさそうです。 サウンドデータもリポジトリ容量は大きいですが、 ジョブは少なくディスク容量としてはそれほど気にならないです。 すべてのジョブがリードオンリーとは限らない使い方、ということもわかりました。

容量を使っているのは、キャラクターやモーションのデータということがわかりました。 アセットリポジトリからチェックアウトしたフォルダツリーには、 ファイルが4万個くらい入っていて、25GBくらいの容量になります。 これがジョブごとに別の場所にあり、全部で20組くらい、 合計すると500GB程度になっています。

多くのデータが重複している状態

このように多数のコピーを持っているのは、Jenkinsマシンのうち、 macノードだけということもわかりました。 macOS特有の機能を使ってもいいから、なんとかしたいという思いがありました。

同一内容のファイルがたくさんコピーされているなら、まとめることができそうです。 macOSのAPFSというファイルシステムには、 同一内容のファイルのディスク領域だけを共有する機能があります。 copy-on-write動作をするので、リードオンリーと限らない場合でも使えそうです。

同一のディスクブロックをまとめられたら、 全体がこの図のようにできると思います。 これが理想の形です。

データ重複を減らした理想形

モデル/モーションデータの性質

ここで、対象となるモデル/モーションのデータがどんな性質を持っているかを考えてみます。

モデルとモーションは、開発が進むにつれて、 新規キャラクターのデータが追加されます。 一方で、すでに登場しているキャラクターのデータが修正されたり モーションが追加されることは、ゼロではないにしても、それほど多くはありません。 先に述べたように、これらのデータは月次リリースに対応してブランチ管理されています。 登場済みのキャラクターは、ブランチを切りかえても内容が変わらないことがほとんどです。

ジョブでは、このブランチ名をパラメーターとして処理を行うことが多いです。 毎月、その月のリリースのブランチだけを処理するわけではなく、 何か月か先のブランチに対してもCIを行っています。 このため、ジョブは実行するたびに別のブランチをチェックアウトしています。 具体的にどのファイルが上書きされるのかを予見することは難しいです。

UNIXのリンク機能

同一内容のファイルがたくさんあるときに、まとめるテクニックとして、 UNIXで古来から使われていた方法にリンクというものがあります。 macOSもUNIXの一種なので同じものが使えます。

ハードリンク、シンボリックリンクという2種類があり、 いずれも、データがリードオンリーの場合によく使われてきました。 macOSのcopy-on-write機能と比較するために、ちょっと復習してみます。

今回の用途をふまえて、次の2点に注意して比較してみましょう。

  • 書きかえたときに、共有されている他のファイルに変更が反映されるか
  • Gitにコミット、Gitからチェックアウトしたときにどうなるか

リンクの説明をするために、ファイルシステム内のデータ構造についてみてみましょう。 UNIXやLinux、macOSのファイルシステムは、だいたいこんな風になっています。

inodeの仕組み

ファイルの実体は「inode」というデータ構造で管理されています。 ファイルのメタデータとディスクブロックの番号がここに記録されています。 実際のファイルひとつにinodeひとつが対応している感じです。

ファイルの内容は複数のブロックに分割して保存されています。 そのブロックの番号がinodeに記録されています。 じゃあファイル名はどこにあるんだ、というと、ディレクトリに入っています。 ディレクトリも実はファイルの一種です。 内容がファイル名とinode番号の対応表になっています。

ハードリンクは、ひとつのinodeに複数のファイル名をつける機能です。 ln コマンドで作ることができます。

ハードリンクの仕組み

ひとつのファイルに2つの名前があるという状態になります。 片方を書きかえるともう一方にも変更が反映されます。 むしろ、反映されることを狙いたい場合に使われる方法です。

Gitは、「このファイルとこのファイルがハードリンクされている」というのを調べないので、 コミットしたりチェックアウトしたりすると、別のファイルとして扱われます。

シンボリックリンクは、 ln コマンドに -s オプションをつけると作ることができます。

シンボリックリンクの仕組み

fileBのディスクブロックには「 fileA 」と書いてあって、 これをファイル名と見なしてfileAをさがし出し、 その内容をfileBの内容とする、という仕組みになっています。 片方を書きかえると、もう一方にも変更が反映されます。

Gitでは、シンボリックリンクを認識して、シンボリックリンクとしてコミットします。 チェックアウトするとシンボリックリンクとして作成されます。

以上の2つのリンク方式は、片方を書きかえるともう一方にも反映されるので、 今回対象とするJenkinsのジョブのように、 不用意に変更が反映されると困るという使い方には適していません。

macOSのcopy-on-write機能

macOSにある、copy-on-write機能の仕組みは、 これらのハードリンク、シンボリックリンクと比べてみると、理解しやすいです。

cp コマンドに -c オプションをつけると、この方法でファイルをコピーできます。

copy-on-writeで複製した状態

新しくinodeが作られ、ファイルの所有者やタイムスタンプなどは、独立して管理されます。 inodeから指しているディスク領域だけが、fileAとfileBで共有されます。

書きかえは片方にだけ反映されます。 ディスク領域を共有しているファイルの片方を書きかえると、 書き込みが発生した部分だけに、新たにディスクブロックが割り当てられます。

copy-on-writeの動作

図では、fileAの末尾に「 hoge 」と追記した状態を表わしています。 fileAとfileBで共有していたディスクブロックのうち、 末尾に対応するブロックだけが新しいブロックにコピーされて、 hoge が追記されます。

この動作は、「write」するときに「copy」するので、 「copy-on-write」と呼ばれています。 この新しいブロックは、fileAからだけ参照されます。 結果として、fileAとfileBは別の内容のファイルになりますが、 内容が同じ部分ではディスク領域を共有している、ということになります。

このような動作は、今回の用途にはぴったりです。

予備実験、効果見積り

copy-on-writeの仕組みを使って、ディスクの節約はできそうでしょうか?

別のディレクトリにクローンした、同じ内容のファイルをまとめたとして、 次のチェックアウトで上書きされて、別のディスク領域に戻ってしまわないでしょうか? ブランチを切りかえても内容が変わらない場合、 ディスク領域の共有が維持されることを期待します。

また、copy-on-writeで領域をまとめるとき、 どれとどれが同一内容のファイルであるか特定できるでしょうか? フォルダツリーが同じ構造をしていれば、 同じファイル名のもの同士を対応させて調べられます。 前述した、リファレンス用にミラーしているフォルダを使って、 ツリー同士を比較できそうです。

節約できそうか調べるため、予備実験と効果見積りをしました。 ブランチを切りかえてチェックアウトしてみて、 更新のないファイルが上書きされるか調べました。 ls コマンドに -i オプションをつけると、inode番号を表示できます。 inode番号とタイムスタンプを調べると、上書きされないことがわかりました。

たくさんコピーがあると言いましたが、 どれくらい同一内容のファイルがあるのかも調べて、 効果の見積りをしました。 ミラーとジョブのツリーをつき合わせて内容を比較しました。 100万個くらいあるファイルのうち97%程度が、 対応するミラーのファイルと同一内容であり、 全体としては500GB程度を節約できそうだ、ということがわかりました。

また、この調査だけで10時間以上がかかってしまいました。 ディスク領域をまとめる処理を一度に全部やろうとすると、 24時間で終わらなさそう、現実的でない、ということもわかりました。

copy-on-writeにどんなリスクがあるのかもこの時点で検討しています。

  • duなどのファイル容量調査ツールでは、別のinodeは別のディスク領域を使っていると計算される
    • 「duで測定したディレクトリごとのディスク容量の合計」と「dfで見たディスク容量」が一致しなくなる
    • copy-on-write活用によってどれくらいの節約になったか、効果測定が難しい
      • 2つのファイルが共有しているかは、後述のapfs-clone-checkerで調べられる
  • 領域共有が解除されるような操作によって急にディスク領域が必要になる
    • ディスクの残り容量が十分にあると思っていたら、急にディスクフルになってしまう可能性がなくはない
    • バックアップは正常に取れるが、リストアしようとしたらディスクに入り切らないという可能性もある

実装

予備実験の結果をふまえて、ディスク領域を共有するジョブを作成しました。 20個あるツリーのうち、1日に2個ずつ選んで処理します。 10日間で全ツリーに対して1回ずつ処理が終わり、 その後はまた最初から処理される、ということを狙っています。

ミラーにあるツリーを比較元として、ファイル内容が同一であるか調べます。 内容が同じで、かつ共有処理がまだされていなければ、 ミラーのファイルを cp -c して、処理対象のファイルの代わりに置きます。 これをたくさんのツリーに対して順に行えば、 「ミラーのディスク領域を共有したツリー」が増えていって、 いつか全部のディスク領域が共有できるというわけです。 どれくらいのファイルを処理したか、統計情報も出力するようにしました。

「2つのファイルが、すでにディスク領域を共有しているかどうか」は、 調べられるツールがあったので、これを使っています。

試験運用

このように作ったジョブを、1か月程度運用してみた結果です。 ディスク領域が共有できているのは、96万ファイル中39万ファイル、約200GB(40%程度)、ということがわかりました。

未共有 共有済 共有不可 合計
ファイル数 513,539 388,005 59,176 960,720
容量(GB) 273.28 201.60 11.22 486.10

予備実験のときの見積りの半分くらいしか効果が出ていないです。これはなぜなんでしょう?

トラブルシューティング

効果が出ない理由として2つを予想しました。

  • ジョブの中で、予備的に一度消してから、チェックアウトし直している
  • 別ブランチをチェックアウトするときに書きかえられているファイルが多い

これを調べるために、ファイルが書きかえられた瞬間を見張りました。 1分に1回、lsコマンドでファイルのタイムスタンプを表示します。 ファイルが書きかわった時刻が分かるので、 そのときに実行されていたJenkinsジョブと、 ジョブの中のどのコマンドだったかを調べました。

こうやって調べた結果、わかったことを元に対策していきます。

予備的なクリア

「予備的に全クリア」しているジョブはなさそうでした。

ブランチを削除するツール

ひとつ原因がわかったのは、「ブランチを削除するツール」が悪さをしていたことです。 ブランチを消すとき、現在のワーキングツリーがそのブランチにいると、 git branch コマンドが、エラーになってしまいます。 これを回避するために、 「とりあえずmasterブランチを1回チェックアウトする」という動作をしていました。 このmasterブランチがとても古く、 多くのファイルが上書きされていました。

対策は簡単です。 masterをチェックアウトする代わりに、 git checkout --detach HEAD というコマンドを実行すればよいです。 タグをチェックアウトしたときと同様の状態になり、安全にブランチを削除できます。

アプリビルド

別の原因として、アプリビルドのジョブがありました。 アプリは、チュートリアルで必要なアセットのみを選んでビルドする必要があります。 必要ないアセットは、いったんチェックアウトした後、削除する処理になっていました。 対策として、このジョブはディスク領域の共有をあきらめて処理対象から外しました。

git reset --hard の挙動

もうひとつ面白かった原因は、ワーキングツリーをブランチの内容に合わせるため、 git reset --hard コマンドを使っていたことでした。 cp -c したファイルと置きかえた直後に git reset すると、 内容が同一かどうか調べず、常に上書きされてしまうことがわかりました。 git checkout では、内容が同一の場合には上書きされません。

対策としては、一度 git status を行っておけば、 git reset しても上書きされないことがわかりました。2

その他の工夫

そのほかに、ツリーを単位として、処理済みかどうかを素早く予想する方法を思いついたので、 日次のジョブに工夫を入れました。 古くから存在していて、更新されそうもないキャラのモデルファイルをひとつ選びます。 処理対象ツリーごとに、このファイルが共有処理済みかどうか調べます。 共有されていなければ、そのツリー全体がおそらく未処理なので、優先して処理します。 このファイルが共有済みであれば、ツリー全体はおそらく処理済みですが、確実とはいえないので、 低優先度ながら処理するようにしました。

結果

このような改善をして、運用をさらに1か月続けた結果です。

未共有 共有済 共有不可 合計
ファイル数 81,236 773,185 15,440 869,861
容量(GB) 43.67 412.63 8.21 464.51

87万ファイル中の 77万ファイル約400GB(88%) のディスク領域を節約できました。 対策の中で処理対象から外したジョブもあるので、 見積り段階と比べると分母も減っています。

下のグラフは、効果の大きかった4台のマシンの空き容量監視画面です。

ディスク使用量の変化

導入前、200GB程度だった空き容量が、 試験運用のときは400GB程度、 改善後は500GB程度になっているのがわかります。 他の要因もあるので、 400GB空き容量が増えた、とはいきませんでしたが、 copy-on-writeの効果としては十分な節約ができたと思います。

当初の状態と比べてみましょう。

多くのデータが重複している状態

これが、こうなりました。

節約後の実際の状態

理想形との違いは、未処理のツリーが、10%くらいは常にありそう、ということです。

まとめ

Jenkinsのmacノード上で、チェックアウトしたデータの容量が多く、慢性的なディスク不足に悩んでいました。 容量の大きいデータを特定し、その性質を調べました。 copy-on-write機能が使えそうだと思いついて、 本当に使えるのか、予備実験をして効果を見積りました。 実装して試験運用すると、効果がいまいちでした。 その原因をさぐって対策した結果、見積りに近い効果が得られました。 gitコマンドの動作の違いなどがわかって面白かったです。

前回のブログで紹介した工夫と、今回紹介したブログの工夫を合わせて、 .gitの容量とチェックアウトしたファイルの容量の両面から、ディスク節約を行えました。

copy-on-write機能は、大きなフォルダ全体のコピーを素早く作りたいときなどにも役立ちます。 たとえば、自分の開発用マシン上で、すでにクローン済みのフォルダとは別にもうひとつクローンしたい場合に使えます。 ワーキングツリーと.gitをまとめて全部 cp -ac cloned_folder cloned_folder2 のようにコピーすると、 時間とディスク容量の両方を節約できます。 JenkinsやGitを使わない場合でも、便利な場面が多いと思います。 ぜひ活用してみてください。

宣伝

この記事を読んで「面白かった」「学びがあった」と思っていただけた方、よろしければTwitterやfacebook、はてなブックマークにてコメントをお願いします。

また DeNA 公式 Twitter アカウント @DeNAxTech では、Blog記事だけでなく色々な勉強会での登壇資料も発信してます。ぜひフォローして下さい!


  1. LFSについては前回の記事のLFS (Large File Storage) の活用の項で解説しています

  2. git statusで作成したインデックス情報とファイルの状態が異なる場合、git checkoutではファイルの内容が変わっているのか調べてくれるのに対し、git resetでは調べてくれないようです。インデックスにどんな情報が入っているかは、GitHubブログのこの記事の「Phase 1: refresh_index」の項に解説があります。inode番号も入っていますね。

夜開催のiOS Test Onlineを開催します!登壇者募集!

SWETグループのKuniwakです。iOSコミュニティの皆様にとってはお久しぶりです!

早速本題ですが、夜開催のiOS Test Onlineを始めます!iOS Test Onlineは、iOS Test NightやiOS Test TeaTimeと同じくiOSアプリのユニットテストやUIテスト、継続的インテグレーション(CI)などiOSアプリのテストにまつわる技術的な発表の場です。

「iOS Test 〜」系勉強会が多すぎる!と思った方向けに説明すると、それぞれのイベントは開催時間帯と開催形態で分かれているだけで発表内容や発表ボリュームは変わりません。

イベント 開催時間帯 開催形態
iOS Test Online オンライン
iOS Test Night オフライン
iOS Test TeaTime オンライン

さて、このiOS Test Onlineについて発表者を募集します!

もう一度言います。

iOS Test Onlineについて発表者を募集します!

発表内容は、たとえば「テストはじめて書いてみたよ」や「このテストツール便利だったよ」あるいは「私がテストを書かない理由」でも大歓迎です!発表したい方は次のGoogle Formからご応募ください!なお、開催日は発表者が集まれる日で調整する予定です。

iOS Test Online発表応募フォーム

過去の発表資料を参考にしたい方は次の過去の発表資料をご覧になるとよいでしょう:

皆様からの発表のご応募お待ちしております!

Isabelle/Isar勉強会を社内で開催しました

こんにちは、SWETグループの鈴木穂高(@hoddy3190)です。

SWETグループのメンバー向けにIsabelle/Isar勉強会を開催しました。本記事では、勉強会の概要の紹介と、勉強会の資料の公開をします。

もしよろしければご活用ください。

Isabelleとは

Isabelleは、定理証明支援ツールの1つです。 数学の授業で証明を解く時、暗記した定義や定義を引き出して仮定や結論をみて試行錯誤しながら適用して解いていっていたと思います。Isabelleを使うと、利用できる定理を提示してくれたり、自動で定理を適用して証明を進めてくれたり、誤った証明を指摘してくれたりします。

Isabelleの大きな特徴として強力な自動証明が挙げられます。自動証明機能の典型例であるSledgehammerは、証明したい論理式を与えれば自動で定理を適用して証明を解き進めてくれます。 公理系も選択可能です。よく使われるのはHOLですが、他にもFOLやZFなどを扱えます。 Isabelleの実績として、オペレーティングシステムの機能に関する証明に使われました。1

Isabelleには証明の記述方法が2種類あります。apply-scriptsとIsarです。 今回の勉強会で用いているのはIsarです。Isarは今何を証明しているのかを宣言して証明を書くためapply-scriptsより読みやすいという特徴があります。

業務でのIsabelleの用途

仕様と実装に正当性関係が成り立つことを証明するのに使えます。 仕様と実装の正当性関係とは、実装が仕様を満たしているかどうかの関係のことを言います。

私はSWETグループにて仕様の欠陥をなるべく早くみつける取り組みにチャレンジしています。 詳細はこちらの記事の「発表内容」のスライド資料または動画をご覧いただければと思いますが、簡単にいうと仕様を形式仕様記述するというアプローチで取り組んでいます。

正当性関係が成り立っていることは論理式で表せますので、仕様と実装が形式的に書かれていれば、実装が仕様を満たしているかをIsabelleのような定理証明支援ツールを使って証明ができます。私はOCamlで記述した仕様と実装をIsabelleが読める形にトランスパイルして、正当性関係が成り立つことを証明しました。

Isabelle/Isar勉強会の概要

正当性関係が成り立っているとはどういうことなのかは、Isabelleを使って証明を進めることで理解が深まります。 さらには証明の手順が分かると、正当性関係が成り立つことを証明されるのを見越して、仕様はこう書けばよい、仕様に対して実装はこう書けばよいといった勘所も養われます。 このようなメリットのため、SWET内でIsabelle/Isarを学ぶための勉強会を開催しました。

勉強会は毎週1時間リモートミーティングで開催しました。 参加メンバーの人数は5,6人です。 参加メンバー全員がIsabelleをapply-scriptsで使ったことがある方でした。 実はこの勉強会よりも前に、Isabelleの基本的な使い方や、仕様と実装をIsabelleで記述し正当性関係に関する証明のやり方を学ぶ別の勉強会があり全員そこの参加者でした。 ただ本資料はIsabelle初学者でも分かるように作っています。

1時間の勉強会の内容は、座学と練習問題です。 座学では毎回私が資料をベースに説明をし参加メンバーと質疑応答を行います。 その後用意してある練習問題を参加メンバーに解いてもらいます。 毎回平均して30分ほど座学、残り30分ほどは演習問題を解く時間でした。 時間内に解ききれなかった練習問題は可能であれば別途各自で時間をみつけて次回の勉強会までに解いてもらうようにしました。 勉強会は合計7回開催しました。

参加メンバーからのフィードバックとして次のようなものが得られました:

  • 簡単な定理から徐々に証明していく形だったので、以前の勉強会に付いていけてなくても何とかなったのが良かったです。
  • apply-scriptsのほうが慣れている分楽な気がします。一方、apply-scriptsは確かにIsabelleを動かさないと何をしているのかがわからないですが、Isarだと読むだけでわかりそうでそこはよさそうに思います。

Isabelle/Isar勉強会の資料と練習問題

Isabelleの特徴は先に述べたとおり強力な自動証明ですが、今回の練習問題では自動証明は極力使わないよう解答してもらいました。 基本的な定理を理解した上で、定理を使って少しずつゴールをrefineしていくことがIsabelle/Isarに慣れるためには必須だと思ったからです。 ですから、もし練習問題を解く際は極力自動証明を使わないことをお勧めします。

さいごに

実際に業務で出てくる論理式に対して、今回は初学者向けということもあり例題や練習問題はシンプルです。 焦らず少しずつできることを増やしていってもらえればよいと思います。 本資料や練習問題に興味を持ってくださる方がいたら嬉しいです。

それから、SWETで働きたいエンジニアを絶賛募集中です。ぜひ採用ページをご覧ください!

時間を加味したモデリング

こんにちは、SWETの鈴木穂高(@hoddy3190)です。

現在SWETチームにて仕様の欠陥をなるべく早くみつける取り組みにチャレンジしています。 欠陥をみつけるタイミングが早ければ早いほど、開発中の手戻りに伴うコストを抑えられます。 たとえば、仕様作成フェーズ、実装フェーズ、QAフェーズの順で開発が進んでいくときに、仕様の欠陥が実装フェーズやQAフェーズでみつかると実装やQAのやり直しを引き起こしかねません。 そうした大きな手戻りを抑えるために仕様の欠陥をなるべく仕様作成フェーズでみつけることを目指します。

対象領域に出てくる要素をモデリングすることは、仕様に潜む欠陥を開発の早い段階でみつけるための、有効な手段のひとつです。 要素には、開発者がこれから作るシステムや、そのシステムのユーザー、そのシステムと直接的または間接的に相互作用する外部のシステムが含まれます。 単に図を書くというモデリングの他に、プログラムのように動くモデルを作るという方法もあります。動くモデルを作るとモデリングする過程での気づきや、モデルを動かしてみた時の気づきが後工程での手戻りを減らすことにつながります。

以前私が書いた「仕様記述テクニック『Promotion』の紹介」ではAlloyを使っていましたが、 本記事ではプログラミング言語OCamlをモデリング言語として使って時間を加味したモデルを記述する方法を紹介します。 多くのモデリング対象の振る舞いは時間が関係するため、モデルの記述で時間を扱えると表現の幅が広がります。 なお、OCamlの説明はしません。

OCamlでのモデリング

今回はプロセスをモデリングします。プロセスは対象領域の要素の振る舞いを指す用語として用います。 モデリングのやり方はさまざまあります。今回は対象のプロセスをプロセスが取りうる状態と遷移で表現します。 プロセスの型は次のようにします:

type ('ev, 'ch, 'state) process =
  'state -> (('ev, 'ch, 'state) trans) list

process型で求められる状態の型は次のようにします:

type state =
  | State_A
  | State_B of int

状態変数はコンストラクタの引数を使って表現します。

遷移ラベルには、イベント同期、受信、τを用意します。ここでτという遷移ラベルのついた遷移は、プロセス内部で自動的に遷移します。 遷移の型は次のようにします:

type ('ev, 'ch, 'state) trans =
  | Tau of 'state
  | Ev of ('ev * 'state)
  | Recv of ('ch * ('state, 'ev) guard * ('ev -> 'state))

コンストラクタTauはτを表します。 コンストラクタEvはイベント同期を表します。イベント同期は、チャネルを通じて値をやりとりします。 コンストラクタRecvは受信を表します。受信は、チャネルを通じて値を受け取ります。受信の場合、事後状態は受信した値によって決まります。ガードを満たすかどうかも受信した値によって決まります。 受信によって起きるイベントは、受信した値を使ってイベント同期で表します。

trans型で求められるイベントの型は次のようにします:

type ev =
  | Event_A
  | Ch1 of int

イベント型に呼応してチャネル型を定義します。イベントが属するコンストラクタを表すための型です。 OCamlでは引数をとるコンストラクタそのものを値として使うことができないので、このような構成にしています。 trans型で求められるチャネルの型は次のようにします:

type ch =
  | Ch_Ch1
  | Ch_Ch2

ここまでを踏まえて次の状態遷移図で表されるATMをモデリングしてみましょう。

f:id:swet-blog:20220404134852p:plain

ATMの振る舞いは、カードを受け取り(in)、PINナンバーを受け取り(pin)、PINナンバーをチェックし(check)、引き出す額を受け取り(req)、額分のお金を出し(dispense)、カードを出します(out)。

これをモデリングすると次のようになります:

let atm_process : (ev, ch, atm_state) process = fun s ->
  match s with
  | A_S1 vals ->
      [
        (* in?c *)
        Recv
          ( Ch_In,
            (fun _ _ -> true),
            fun ev ->
              let vals' = make_vals'_1 vals ev in
              A_S2 vals' );
      ]
  | A_S2 vals ->
      [
        (* pin?p *)
        Recv
          ( Ch_Pin,
            (fun _ _ -> true),
            fun ev ->
              let vals' = make_vals'_2 vals ev in
              A_S3 vals' );
      ]
  | A_S3 vals ->
      let vals' = make_vals'_3 vals in
      [ (* check *) Ev (Check, A_S4 vals') ]
  | A_S4 vals ->
      [
        (* req?n *)
        Recv
          ( Ch_Req,
            (fun _ _ -> true),
            fun ev ->
              let vals' = make_vals'_4 vals ev in
              A_S5 vals' );
      ]
  | A_S5 vals ->
      let vals' = make_vals'_5 vals in
      [ (* dispense!n *) Ev (Dispense vals.req, A_S6 vals') ]
  | A_S6 vals ->
      let vals' = make_vals'_6 vals in
      [ (* out!c *) Ev (Out (get_card vals), A_S1 vals') ]

時間遷移の追加

次に、物理的な時間経過を表現できるように表現の枠組みを拡大します。ここでは時間オートマトンという理論にある考え方を使います。 時間オートマトンにおける状態は、ロケーションと時間代入関数の組で表現します。 ロケーションは、今まで「状態」と呼んでいたものです。時間代入関数はクロック変数と時間をマッピングしたものです。クロックは経過した時間を表します。 遷移には2種類あり、あるロケーションから別のロケーションに遷移する離散遷移と、時間経過による時間遷移があります。

時間を表す型を用意します:

type datetime = int

クロック変数の型を用意します:

type clock = T

時間制約式は、時間に関する条件を表した式です。ある時刻までに遷移するといった遷移の条件や、ある時刻を越えてこの状態に留まることはできないといった状態が満たすべき条件を表すのに用いられます。時間制約式は次のようにします:

type ('clock) cons =
  | True
  | Eq of 'clock * datetime
  | Le of 'clock * datetime
  | Ge of 'clock * datetime
  | Lt of 'clock * datetime
  | Gt of 'clock * datetime
  | Not of 'clock cons
  | Or of 'clock cons * 'clock cons
  | And of 'clock cons * 'clock cons

時間代入関数は次のようにします:

type 'clock v = ('clock, datetime) Hashtbl.t

時間代入関数は時間遷移や、クロック変数のリセットを伴う離散遷移で更新されます。

不変述語は状態が満たす時間制約です。不変述語は次のようにします:

type ('state, 'clock) inv = 'state -> ('clock cons)

遷移に時間制約を与えられるようにしたいので、遷移する際に満たすべき時間制約とリセット対象のクロック変数を指定できるようプロセスの型を次のように変更します:

type ('ev, 'ch, 'state, 'clock) process =
  'state ->
  'clock v ->
  ( 'clock cons * (* 遷移する際に満たすべき時間制約式 *)
    'clock list * (* リセットするクロック変数 *)
    ('ev, 'ch, 'state, 'clock) trans ) list

遷移も合わせて変更します:

type ('ev, 'ch, 'state, 'clock) trans =
  | Tau of 'state
  | Ev of ('ev * 'state)
  | Recv of ('ch * ('state, 'clock, 'ev) guard * ('ev -> 'state))

ATMの例(モデリング)

ここまでを踏まえてさきほどのATMの振る舞いに変更を加えたものをモデリングしてみましょう。

f:id:swet-blog:20220324180050p:plain

pinの受け取りに時間が30かかる場合はカードを出す振る舞いを加えました。 これをモデリングすると次のようになります:

let atm_process (ev, ch, atm_state, clock) process = fun s v ->
  match s with
  | A_S1 vals ->
      [
        ( True,
          [ T ],
          (* in?c *)
          Recv
            ( Ch_In,
              (fun _ _ _ -> true),
              fun ev ->
                let vals' = make_vals'_1 vals ev in
                A_S2 vals' ) );
      ]
  | A_S2 vals ->
      [
        ( Lt (T, 30),
          [],
          (* pin?p *)
          Recv
            ( Ch_Pin,
              (fun _ _ _ -> true),
              fun ev ->
                let vals' = make_vals'_2 vals ev in
                A_S3 vals' ) );
        (Eq (T, 30), [], Ev (Out (get_card vals), A_S1 vals));
      ]
  | A_S3 vals ->
      let vals' = make_vals'_3 vals in
      [ (True, [], (* check *) Ev (Check, A_S4 vals')) ]
  | A_S4 vals ->
      [
        ( True,
          [],
          (* req?n *)
          Recv
            ( Ch_Req,
              (fun _ _ _ -> true),
              fun ev ->
                let vals' = make_vals'_4 vals ev in
                A_S5 vals' ) );
      ]
  | A_S5 vals ->
      let vals' = make_vals'_5 vals in
      [ (True, [], (* dispense!n *) Ev (Dispense vals.req, A_S6 vals')) ]
  | A_S6 vals ->
      let vals' = make_vals'_6 vals in
      [ (True, [], (* out!c *) Ev (Out (get_card vals), A_S1 vals')) ]

モデリングしたプロセスをエンジンを使ってREPL上で動かしてみます。 エンジンは、どのイベントが起こるとどの状態になるのかを可視化します。 ひとつ前の状態に戻ったり、遷移の履歴をダンプしたりもできます。 不変述語を満たしているかのチェックもエンジン側で行っています。

f:id:swet-blog:20220324180234g:plain

メニュー[0]を選ぶと時間遷移をします。 メニュー[1]を選ぶとたどってきた状態とイベントをダンプします。 メニュー[2]を選ぶとひとつ前の状態に戻ります(undo)。 メニュー[3]を選ぶとundoで戻った操作をやり直します(redo)。 メニュー[4]以降を選ぶと離散遷移をします。

状態遷移図を見ながら意図どおりに動いているかチェックします。 上の図では、初期状態A_S1から、メニュー[4]を選択していき、A_S2、A_S3、A_S4、A_S5、A_S6、A_S1と遷移することを確認しています。 その後、A_S1からA_S2に遷移し、メニュー[0]を選択して時間を30進めた後、A_S1に遷移することを確認しています。

並行合成

一般にシステムはユーザーや外部ソフトウェアなどと相互作用をもちます。 しかし、相互作用をもつ複数の要素から構成されるシステムを欠陥なく設計し実装することは難しいものです。 複数の要素から構成されるシステムをモデリングして開発の早い段階で先のように動かしてみることは、手戻りを減らすことに寄与することが期待されます。

システムを動かすためには、まず相互作用する複数のプロセスをそれぞれモデリングします。そしてそれらを合成します。合成は、複数の振る舞いを組み合わせてできたシステムの振る舞いを決定します。 並行合成は、合成する2つのプロセスそれぞれで発生する遷移のうち、同期させたい遷移を指定して合成します。指定された遷移以外の遷移は独立して起こります。

2つのプロセスを受け取り、並行合成したプロセスを返す関数の型を次のように決めます:

val composit:
  ?sync_set_by_ch:('ch -> bool) ->
  ?eq_ev:('ev -> 'ev -> bool) ->
  ('ev, 'ch, 'p_state, 'clock) process (* プロセスP *) ->
  ('ev, 'ch, 'q_state, 'clock) process (* プロセスQ *) ->
  ('ev -> 'ch) (* 対応チャネル取得関数 *) -> 
  ('ev, 'ch, 'p_state * 'q_state, 'clock) process

プロセスPとプロセスQは合成対象のプロセスです。合成されたプロセスがとりうる状態は、プロセスPがとりうる状態とプロセスQがとりうる状態の組になります。合成されたプロセスがとりうる状態はp_stateとq_stateのタプルで表現します。 対応チャネル取得関数は、与えられたイベントが属するチャネルを返します。 sync_set_by_chで同期イベント集合を表現します。同期イベント集合には、合成する2つのプロセスの相互作用に関係するイベントを指定します。たとえば2つのプロセス間でチャネルを通じて値を送受信する場合、値のやりとりをするイベントを指定します。チャネルを受け取ってtrueを返す場合、そのチャネルに属するイベントはすべて同期イベント集合に含まれることを意味します。 eq_evは受け取った2つのイベント同期を比較し等しいかどうかを判定する関数です。2つのイベント同期が同期イベント集合に含まれているとき同期するのかどうかを判定するのに使います。

ATMの例(並行合成)

さきほどのATMのモデルは変えずに、新たにユーザーの振る舞いをモデリングして、ATMと並行合成します。

ユーザーの振る舞いを次のように定めます: f:id:swet-blog:20220324180131p:plain

さきほどのcomposit関数を用いてATMの振る舞いとユーザーの振る舞いを並行合成したものを動かしてみます。 同期イベント集合は次のようにします:

let sync_set_by_ch ch =
match ch with
| Ch_In -> true
| Ch_Pin -> true
| Ch_Req -> true
| Ch_Dispense -> true
| Ch_Out -> true
| _ -> false

ユーザーとATMを合成した振る舞いの状態遷移図は次のようになります: f:id:swet-blog:20220324180045p:plain

初期状態を(U_S1, A_S1)にして動かしてみます。

f:id:swet-blog:20220324182633g:plain

まとめ

調べたい部分に限定したモデリングは実システムの実装よりもずっと小さなコストでできますから、実装が終わって調べていた振る舞いを、仕様作成の段階で調べることができます。 ここで誤りをみつけることができれば手戻り避けることができるので、開発時間を大きく短縮できます。 動くモデルを作って動かせば、仕様書を読んだだけだと気づけなかった仕様の欠陥にも気づくことが期待できます。 また設計上の選択についてさまざまな可能性を実験的に調べるといったことも可能になります。そうすることでよりよいプロダクトやサービスを開発できる可能性が高まると考えています。

参考