DeNA Testing Blog

Make Testing Fun, Smart, and Delighting End-Users

Unityプロジェクト向けオートパイロットフレームワークの作りかた

SWETグループの長谷川(@nowsprinting)です。

開発者自身の手によるUnityプロジェクトの品質向上にはさまざまなアプローチがあります。 当ブログでもこれまでに、 ユニットテスト静的解析 といった、コーディング段階でC#コードの品質(特に内部品質)を高めるアプローチを紹介してきました。

本記事では少し目線を変えて、ゲームがほぼ組み上がった状態でのゲームプレイを自動化する、オートパイロットによる検証アプローチを紹介します。

オートパイロットによる検証の位置付けと目的

ゲームが組み上がった状態とは、ゲームを構成するC#コードや3Dモデルなどのアセットファイルを組み合わせた、結合度の高い状態を指します。 結合度を突き詰めると、IL2CPPビルドしてスタンドアロンプレイヤー(モバイル端末やコンソール機)で実施するテストになりますが、今回は結合度を上げすぎず、実行環境はUnityエディターの再生モードを使用します。

このアプローチのメリットは、エンジニア(プログラマー)個々が書いたコード間の連動や、アセットやマスターデータのバリデーションをすり抜けてしまった問題をQA工程に入る手前で検知できることです。 またユニットテストに比べてゲーム本体のテスタビリティ*1に影響されにくく、ユニットテストが困難なプロジェクトにも比較的低コストで導入できます。

しかし厳密な検証まで行なうのは難しく、たとえばシナリオに沿った操作をした結果の画面表示内容まで細かく検証しようとすると、テスト実装コストが高くなってしまいます。 自動テスト導入時には見逃されがちですが、運用をはじめてからはゲーム本体の仕様変更に追随していくメンテナンスコストが大きくのしかかります。このコストが払えないとせっかくの自動テストもすぐに使いものにならなくなります。

ここで妥当な検証方法として次の2つがあげられます。

  1. モンキーテストによる、クラッシュや進行不能バグの検出
  2. 少数のシナリオテストによる、主要な画面遷移の確認

それぞれ長所・短所がありますので、続いて説明していきます。

モンキーテスト

モンキーテストとは、お猿さんが操作するかのように無作為にゲームをプレイするテストです。ユーザーが行う操作をカバーさえできれば、シナリオの作成やメンテナンスは不要です。

ただし無作為な操作ですので、その操作の結果が意図したものかといった検証まではできません。 期待できるのは、クラッシュや進行不能といった、クリティカルではあるものの、まれな不具合に限られます。

また、たとえばゲーム開始時に接続するサーバ選択では常に特定のサーバを選択させる、チュートリアルには時間をかけずスキップするといった、完全ランダムではない振る舞いが求められるケースもあります。

シナリオテスト

シナリオテストとは、シナリオやユースケースにそってゲームをプレイし、設定されたゴール(たとえばデッキ編成の完了)に行き着くことができるかを検証するテストです。 主に「主要な機能を完遂できること*2」や「開発者・QA担当者ともめったに触らない機能が壊れていないこと」の確認を目的に、少数の簡易なシナリオを実行します。 画面遷移の途中でのクラッシュや進行不能のほか、想定されたボタンが表示されない、もしくはタップできないといった問題も検知できます。

なお、ここではシナリオのゴール判定は画面遷移されたこと、くらいの簡易な検証を想定しています。 詳細な検証(たとえば変更したデッキの戦闘力の数値が期待値と一致するか)も可能ではありますが、シナリオの作成・メンテナンスコストが増大します。それはユニットテストなどで担保するようにすべきです。

しかし少数・簡易なものに絞っても、操作シナリオをコード化していくコストはかかります。 開発中には画面遷移にも頻繁に変更が入りますし、運用に入ってもイベントや機能追加に対応するメンテナンスは続きます。

Anjin

DeNA内で開発・導入を進めているフレームワークAnjin(あんじん)*3は、モンキーテストとシナリオテストを組み合わせることによって双方のデメリットを補い、低コストでオートパイロットを運用できることを目指しています。

Unityの画面単位であるSceneごとに特定の操作を行なうAgentを割り当てておき、アクティブなSceneの切り替えに応じて動的にAgentを切り替えて動作します。 Agentは拡張できるようになっており、たとえばインゲームの操作を行なうAgentはゲームタイトルごとに個別に実装して組み込むことができます。

Sceneの切り替わりイベントは、UnityのSceneManagerに次のようにリスナを登録して受け取ることができます。

SceneManager.activeSceneChanged += _dispatcher.DispatchByScene;

このイベントを受け取るActionには、切り替え前後のSceneが引数で渡されます。 これを用いて、次のように切り替え後のScene(next)に対応するAgent(存在しない場合はFallbackに指定されているAgent)を起動しています。

public void DispatchByScene(Scene current, Scene next)
{
  var agent = GetAssignedAgent(next);
  if (agent == null)
  {
    agent = GetFallbackAgent();
  }

  var agentName = agent.GetType().Name;
  var gameObject = new GameObject(agentName);
  var token = gameObject.GetCancellationTokenOnDestroy();

  agent.Logger = _logger;
  agent.Random = _randomFactory.CreateRandom();
  agent.Run(token).Forget();

  // snip
}

Agentには、専用のロガーのほか、擬似乱数シードを与えています。 疑似乱数シードを生成する_randomFactoryの生成時に与えるシード値は、オートパイロットの設定で固定できるようになっており、同じシード値を指定することでモンキーテストのランダムな操作を再現できるようにしています*4

代表的なAgentの設定と実装

たとえばスマートフォン向けのゲームで、次のようなScene構成のものを例とします。

  • タイトル画面
  • ホーム画面・各種機能(アウトゲーム)
  • バトル画面(インゲーム)

タイトル画面には、接続サーバなど決まったものを選択する必要があるためシナリオ操作を行なうAgentを割り当てます。

ホーム画面には、ログインボーナスを受け取り、主要な機能を巡回するシナリオを実行した後、モンキーテストを行なうAgentを割り当てます。

バトル画面には、ゲームタイトル固有の自動操作を行なうAgentを割り当てます。 オートパイロットの目的から、これもモンキーテストもしくはすぐにリタイアしてアウトゲームに戻る振る舞いを想定しています。

Anjinでは、これを次のようにScriptableObjectに設定します*5

この例で用いているAgentは汎用的なもので、Anjinにビルトインされています。 続いて、代表的なビルトインAgentを紹介します。

アウトゲームのモンキーAgent

uGUI Monkey Agentは、Canvas上のUIコンポーネントをランダム操作するAgentです。 生存時間と、操作と操作の間の遅延時間を設定できるようにしています。

このAgentは、UnityEngine.UI.Selectable.allSelectablesArrayを利用して操作対象候補となるUIコンポーネントをリストアップ、Raycasterによるヒットテストを経て実際にプレイヤーが操作可能なUIコンポーネントを絞り込み、操作候補としています。 この中から擬似乱数によって操作するUIコンポーネントを抽選し、タップなどの操作を行ないます。 一般にモバイルアプリのモンキーテストではランダムな座標をタップしていく方式が取られますが、効率を考えてUIコンポーネント単位で操作するようにしています。

なお、広告表示や他のアプリを起動するボタンなどの操作させたくないオブジェクトに対しては、あらかじめIgnoreUGUIMonkeyというアノテーションコンポーネントをアタッチすることで操作対象外とする仕組みにしています。

アウトゲームのプレイバックAgent

uGUI Playback Agentは、UIコンポーネントをシナリオにそって操作するAgentです。 Recorded Jsonには、Automated QAパッケージ(com.unity.automated-testing)を使ってUI操作を記録したJSONファイルを指定します。

Automated QAパッケージのRecorded Playback機能は、Unityエディター上で実際のゲームUIをマウスで操作したシナリオをJSONファイルに記録・再生するものです。 Anjinで使用するテストシナリオ作成は、このレコーディング機能を利用してコーディングレスで行ないます。

実行時は、次のようにAutomated QAパッケージの公開されているAPIを使用してJSONファイルに記録されたUI操作を再生させています。

using Unity.AutomatedQA;
using Unity.RecordedPlayback;

// snip

private static IEnumerator Play(TextAsset recordingJson)
{
  RecordedPlaybackPersistentData.SetRecordingMode(RecordingMode.Playback);
  RecordedPlaybackPersistentData.SetRecordingData(recordingJson.text);

  CentralAutomationController.Instance.Reset();
  CentralAutomationController.Instance.AddAutomator<RecordedPlaybackAutomator>(
    new RecordedPlaybackAutomatorConfig { loadEntryScene = false });
  CentralAutomationController.Instance.Run();

  while (!CentralAutomationController.Instance.IsAutomationComplete())
  {
    yield return null;
  }
}

コンポジットAgent

Serial Composite Agentは、登録された複数のAgentを逐次実行するAgentです。Composite Agentを入れ子にもできます。

この例では、ホーム画面ではまずログインボーナスを受け取る操作、続いて機能Fooの操作、機能Barの操作、機能Bazの操作を行なうシナリオを実行します。 そして規定のシナリオが終わったら、残り時間はモンキーテストを実行する設定になっています。

このAgentは、シナリオとランダム操作を組み合わせられるというだけでなく、シナリオを細かく区切ることで仕様変更の影響によるメンテナンス範囲を最小限にとどめることにも役立ちます。

ゲームタイトル固有Agentの実装

ゲームタイトル固有のAgentを作る場合は、AbstractAgentクラスを継承してRunメソッドをオーバーライドします。 たとえば、指定された秒数待機するAgentは次のように実装できます。

[CreateAssetMenu(fileName = "New WaitAgent", menuName = "Anjin/Wait Agent", order = 20)]
public class WaitAgent : AbstractAgent
{
  public long lifespanSec = 0L;

  public override async UniTask Run(CancellationToken token)
  {
    if (lifespanSec > 0)
    {
      await UniTask.Delay(TimeSpan.FromSeconds(lifespanSec), cancellationToken: token);
    }
    else
    {
      await UniTask.Delay(-1, cancellationToken: token); // 無期限に待機する場合は -1
    }
  }
}

Agent内では、AbstractAgentクラスに定義されているLoggerおよびRandomが使用できます。

その他の機能

レポーティング

Anjinの実行中にErrorExceptionが発生した場合など、スクリーンショットを撮影してSlack通知するようになっています。 エラーなく操作を完遂した場合の通知は、Anjinを実行するGitHub ActionsやJenkinsのジョブで行ないます。

ログ監視

Anjinは、Unityのログに流れるゲームタイトルのログを監視し、あらかじめ設定された条件にマッチするログメッセージをエラーとして扱います。

Unityのログは、次のようにリスナを登録して受け取ることができます。

Application.logMessageReceived += _logMessageHandler.HandleLog;

このイベントを受け取るActionは次のように実装しています。

public async void HandleLog(string logString, string stackTrace, LogType type)
{
  if (IsIgnoreMessage(logString, stackTrace, type))
  {
    return;  // 報告・停止トリガでないログメッセージであればなにもしない
  }

  await UniTask.SwitchToMainThread();
  await PostToSlack(logString, stackTrace, type);  // Slack通知

  var autopilot = Object.FindObjectOfType<Autopilot>();
  if (autopilot != null)
  {
    autopilot.Terminate(Autopilot.ExitCode.UnCatchExceptions);  // Anjin停止処理
  }
}

IsIgnoreMessage()では、設定ファイルにしたがってそのログメッセージをエラー扱いするかどうかを判定しています。 設定には、AssertWarningをエラー扱いするか、また、ログメッセージに特定の文字列が含まれている場合は既知の問題として無視するといったことを定義できます。

今後の展望

Anjinはこれまでに、ゲームタイトル開発終盤に導入し、ナイトリービルドがQAに渡る前のスモークテスト*6で一定の成果を上げています。 この用途では、主要な画面遷移をパスできるというシナリオテストが中心でした。

現在は、より早い開発段階からモンキーテストをメインとして投入し、ゲーム内に埋め込まれたAssertを踏ませることで未知の不具合を早期発見できないかの検証を進めています。

We are hiring

SWETグループでは、このようなUnityプロジェクトに対する品質向上アプローチも行っています。 興味を持たれた方は、ぜひ採用情報を確認ください!

*1:テスト容易性とも呼ばれます。テスト対象への入力の与えやすさ・出力の観測しやすさなど、テストコードによるテストを可能にするためにはプロダクトコード側の品質もそれなりに要求されます。これが低いと、テストを書くコストがとても高くなります

*2:テストを実行するタイミングにもよりますが、QAによる検証作業を止めてしまう問題を事前にみつける目的を持ちます

*3:航海士(パイロット)の古語で、戦国時代の日本に漂着したイングランド人ウィリアム・アダムスの日本名(三浦按針)にもなっています

*4:ただしゲーム本体にもランダム要素がある場合、そちらのシードを固定できる機構も必要です

*5:Anjinでは、ゲームタイトル固有の拡張が必要な部分を除き、オートパイロットの設定はすべてUnityエディター上で完結するようになっています

*6:機械の電源を入れたときに煙を吹かないかを見るような簡素なテスト

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で働きたいエンジニアを絶賛募集中です。ぜひ採用ページをご覧ください!