DeNA Testing Blog

Make Testing Fun, Smart, and Delighting End-Users

Goによるロードテスト

はじめに

SWETグループGoチームの金子 (@theoden9014) です。

弊社が運営するライブコミュニケーションアプリであるPococha(ポコチャ)においてロードテストを実施する際、Go言語を利用して独自のロードテストツール開発しました。今回は、その知見を共有したいと思います。

20201201171506

この記事はDeNA Advent Calendar 2020の4日目の記事です。

本記事ではシステムをWebシステムと前提としていますのでご注意ください。

ロードテストとは (Load Testing)

JSTQBISTQBにおいては性能テスト (Performance Testing) の1つと定義されています。 性能テストとはシステムテストにおける非機能テストの1つです。 ロードテスト、耐久性テスト、ストレステスト等があり、それぞれ目的に応じて実施します。

ロードテストは、システムがユーザ負荷のピーク時でも継続して稼働できるか検証します。 サーバ等のインフラも含めて本番規模のシステム構築するケースが多く、非常にコストが掛かる検証です。 よって、システム導入時や大規模なシステム改修時など、要所要所で単発的に実施する事が多いです。

検証する観点はサービスの性質やシステムの特性によって違うので一般化することは難しいです。例えば、想定されるスパイクアクセスに耐えられるか、想定される同時アクセス数を捌く事ができるかのような観点で検証します。

ロードテストはパフォーマンスの目標値をまず最初に設定します。この目標値を満たすことができるかロードテストツール使って検証し、満たしていない場合はシステム全体でボトルネックとなっている箇所を特定し、そのボトルネックを改善します。

この検証、分析、改善のサイクルを目標値を満たすまで繰り返し行います。

ロードテストにおいてボトルネックの特定は最も重要な要素です。 ロードテストを実施する際にはロードテストツールのメトリクスでは不十分で、システムの可観測性を高めておく必要があります。 しかし、今回は記事の主旨がロードテストツール側にあるので、検証対象のシステムについての可観測性については割愛させていただきます。

ロードテストツールの選定

最初に設定した目標値を元に、具体的な負荷シナリオや変動させるパラメータの設計をします。

静的なリクエストを生成するにはapachebenchvegetaなどのツールがあります。 ロジックに基づいたリクエストパラメータの生成やURLの生成などの、動的なリクエストを生成するにはGatlingJMeterLocust等のツールがあります。

このようなロードテストツールは他にもいくつかあります。 しかし、どうしてもユースケースに合わなかったり、欲しい機能が存在しなかったりといったケースが発生することもあります。 そういった場合は既存ツールを拡張するか、独自でロードテストツールを開発することになります。

今回のロードテストの要件

今回は今後想定されるユーザ数のリクエストを問題なく捌けるか検証したかったので、重要機能においての特定ユースケースのロードテストを実施しました。 同時利用ユーザ数、APIエンドポイント毎の秒間実行回数を目標値として設定し、その他変動させる必要のあるパラメータの設計をしました。

今回は様々な要件がありましたがその中でも難しかったのは、キャッシュのヒット率を下げるためにユーザの行動に重み付けをした上でランダム性を持たせなければならない、というところでした。例えば、ライブ視聴中におけるユーザの行動を挙げると以下のようなパラメータです。

  • コメントやアイテムやいいねの送信、他ユーザへの拍手、等々の行動の選択
  • 送信するコメント内容、アイテムの種類、拍手する対象ユーザの選択

認証やライブ視聴中のKeepAliveなど他にも技術的な要件や課題がいくつかあり、既存のロードテストツールでそれらを実現しようとすると通常の機能だけでは難しいと判断し、今回は使い慣れているGo言語を使ってロードテストツールを独自で実装することにしました。

Goによるロードテストツールの実装

Goではgoroutineとchannelを利用することで並行処理をシンプルに記述できます。 今回は以下のようなアーキテクチャで開発しました。

20200930130505

全てのコードの解説は行えないので、今回はポイントとなるコンポーネントであるEvent (+EventGenerator) とDispatcherを抜粋してご紹介します。 EventGeneratorではリクエストパラメータにランダム性を担保させるようにし、Dispatcherではそれを実行するユーザにランダム性を担保させるようにしています。

まずEventについてです。 Eventは処理を行う単位としており、行いたい処理の種類によって構造体とそれを生成するための関数を定義していきます。

一定の間隔でランダムなパラメータの生成を行い、channelに対してEventを送信します。

import (
    "context"
    "time"
)

type Event interface {
    Emit(ctx context.Context, c *APIClient) error
    Name() string
}

type commentEvent struct {
    // イベント生成側と処理側で共有するパラメータをここに記述します
    text string
}

// イベントの処理内容、複数のAPIで整合性が必要な処理もここにまとめます
// ここでは認証などの必要な初期化処理を行ったAPIClient(ユーザ)を再利用したいので引数で渡せるようにしています
func (e *sendCommentEvent) Emit(ctx context.Context, c *APIClient) error {
    if err := c.LiveViewing.SendComment(ctx, e.text, e.toUserID); err != nil {
        return err
    }
    return nil
}

// トレーシングや統計情報を集計する際に別のイベントと区別する為のイベント名
func (e *sendCommentEvent) Name() string {
    return "request: send comment"
}

// 任意のユーザがコメントを送信するイベントを発生させます
func commentEventGen(ctx context.Context, d time.Duration) chan Event {
    // EventGenはd間隔でイベントを生成して戻り値のチャネルに対して送信します
    return EventGen(ctx, d, func(tm time.Time, ev chan Event) {
    // 今回は適当にイベント生成時の時間を生成しています
    // ランダム性のあるパラメータはここで担保できるようになります
        ev <- &commentEvent{
            text: tm.String(),
        }
    })
}

// EventGenはイベントを一定間隔で生成する為の関数を生成する為のヘルパー関数
// 第三引数の関数でパラメータを与えてEventを生成してチャネルに送信する処理を記述します
func EventGen(ctx context.Context, d time.Duration, f func(time.Time, chan Event)) chan Event {
    eventChan := make(chan Event)
    if d == 0 {
        return eventChan
    }

    go func() {
        ticker := time.NewTicker(d)
        defer ticker.Stop()

        for {
            select {
            case t := <-ticker.C:
                f(t, eventChan)
            case <-ctx.Done():
                close(eventChan)
                return
            }
        }
    }()

    return eventChan
}

次に、生成されたイベント毎のchannelを1つに集約し、各ワーカーに対して処理を委任していく役割であるDispatcherについてです。 このDispatcherは一番重要な箇所です。 様々な種類のEventを1つのchannelにまとめます。その1つのchannelを複数のワーカーが受信することによって偏りを持たせずに処理を行えるようになります。

1ワーカー1ユーザとなるようにしているので、これによって各ユーザが実行するイベントの種類にランダム性を持たせてることが可能になります。 今回は記事の尺の都合上、他コンポーネントについては割愛させていただくのでinterfaceとして定義しております。

import (
    "context"
    "sync"
)

type Worker interface {
    WaitEvent(context.Context) Event
    Process(context.Context, Event) error
    Close() error
}
type WorkerPool interface {
    Get() Worker
    Put(Worker)
}

type Dispatcher struct {
    mu     sync.RWMutex
    inputs []<-chan Event

    pool WorkerPool
}

// 処理するイベントのchannelをセットします
// 複数のchannelをセットすることが可能です
func (d *Dispatcher) In(ev chan Event) {
    d.mu.Lock()
    defer d.mu.Unlock()
    d.inputs = append(d.inputs, ev)
}

type WorkerFunc func(context.Context, Event) error

// これを利用してWorker追加時に、WorkerFuncのクロージャ内にAPIClientを閉じ込めることによって
// 1Worker---1APIClient--1User の紐付けを行うことができます。
func (d *Dispatcher) NewWorker(id string, f WorkerFunc, r <-chan Event) {
    w := &worker{
        id: id,
        f:  f,
        r:  r,
    }
    d.pool.Push(w)
}

// Startはchannelを繋ぎ合わせ、設定したWorkerを起動していくメソッドです
func (d *Dispatcher) Start(ctx context.Context) {
    // d.inputs のチャネルを1つのチャネルに集約していきます
    input := make(chan Event, len(d.inputs))
    for _, evc := range d.inputs {
        evc := evc
        go func(evc <-chan Event) {
            for {
                select {
                case ev := <-evc:
                    input <- ev
                case <-ctx.Done():
                    return
                }
            }
        }(evc)
    }

    // WorkerPoolからWorkerを取得して、
    // それぞれのWorkerをgoroutineでイベントループで起動していきます
    for w := d.pool.Get(); w != nil; w = d.pool.Get() {
        w := w
        go func() {
            defer w.Close()
            for {
                select {
                case ev := <-input:
                    if ev == nil { // closed Event channel
                        return
                    }
                    w.Process(ctx, ev)
                case <-ctx.Done():
                    return
                }
            }
        }()
    }
}

これらのコードを以下のように繋ぎ合わせることで、複数種類のイベントを、パラメータと実行するユーザにランダム性を持たせることができます。

// 第二引数でイベントの生成間隔を指定、
// それ以降の引数はGeneratorの生成アルゴリズムによって任意の値を指定
cChan := commentEventGen(ctx, 1/10*time.Second)
iChan := itemEventGen(ctx, 1/20*time.Second, itemIds...)
.
.
.
dispatcher := NewDispatcher()
dispatcher.In(cChan)
dispatcher.In(iChan)
.
.
.

// テスト用のユーザデータは予め用意しておいて読み込むようにしておきます
for _, user := range users {
    // クライアントの認証や、
    // その他細かいクライアント毎のセットアップ処理
    auth := NewDebugAuthenticator(user)
    // 今回はアプリケーションの負荷を確認したかったのでコネクションプールを共通化していますが、
    // インフラ側のテストも兼ねて共通化したくない場合は、
    // APIクライアント毎にコネクションプールを作った方が良いでしょう。
    client := NewAPIClient(baseURL, http.DefaultClient, auth)
    // 生成されたイベントはchannelを通じて、
    // クロージャの第二引数であるEventに渡ってきます
    dispatcher.NewWorker(user.Name, func(ctx context.Context, ev Event) error {
        return ev.Emit(ctx, client)
    })
}

dispatcher.Start(ctx)

ボトルネックの可視化

runtime/traceパッケージ

Goでは標準パッケージのruntime/traceを利用することでトレーシングを行うことができます。これを使うとランタイムレベルのトレースと、ユーザアノテーションを使ったトレーシングを行うことができます。 今回はユーザアノテーションを使ったトレーシングについてお話ししたいと思います。

ユーザアノテーションをするにはtrace.Tasktrace.Regionの2つを使って計測したい区間を自分で定義していきます。

trace.Taskはgoroutineを跨いで計測できます。 trace.Regionを使うとgoroutine内の細かいトレース情報を取得できます。しかし、計測範囲をgoroutine内に絞る必要があります。

トレーシングの実施方法

runtime/traceは常にトレーシングを行っているわけではなく、ランタイム内のトレーシングフラグが有効な際にトレーシングが行われます。 以下の2つの方法でトレーシングをフラグを有効にして結果を取得できます。

1つはテスト時にトレーシングを行う方法です。go test -trace=${OUTPUT_FILE}フラグを追加することで${OUTPUT_FILE}にトレース結果のファイルを生成できます。

もう1つはプログラム実行中にhttpハンドラー経由でトレーシングを行う方法です。net/http/pprofを空インポートをするとhttp.DefaultMuxにトレーシングとプロファイリングのエンドポイント用のハンドラーが追加されます。 http.ListenAndServe(":8080", nil) 等でHTTPサーバを立ち上げて:8080/debug/pprof/traceへアクセスするとデフォルトで30秒間、その間だけトレーシングを実施して結果を取得できます。

これらのトレース結果ファイルはgo tool trace ${OUTPUT_FILE} コマンドでWebUIから確認できます

ロードテストツールでの利用

今回はruntime/traceを利用してイベントの種類(今回はAPIエンドポイント)毎にRegionを定義しました。 go tool traceを使うとWebUIから以下のようにイベントの種類毎の処理時間分布を確認できるので、処理が遅くなるエンドポイントを特定できました。(以下の画像はサンプル用に用意したものです)

20201202210836

OpenCensusOpenTelemetryのような分散トレーシングを使っても良いとは思いますが、今回はオーバースペックだと判断したので利用はしませんでした。

参考までにですが、以下のようなMakefileを用意しておくと簡単にプロファイルとトレーシング結果を取得できます。

GO          := go
PPROF_URL   := http://localhost:6060/debug/pprof
DEBUG_TYPES := profile.pdf goroutine.pdf heap.pdf block.pdf mutex.pdf trace.out
DEBUGDIR    := ./debug

.PHONY: debug
debug: debug/clean $(DEBUG_FILES)

.PHONY: debug/clean
debug/clean:
    @rm -f $(DEBUGDIR)/*

$(DEBUGDIR)/%.pdf:
    $(GO) tool pprof -pdf -output $@ $(PPROF_URL)/$*?seconds=30

$(DEBUGDIR)/%.out:
    curl -fsL -o $@ $(PPROF_URL)/$*?seconds=30
    $(GO) tool trace $@

まとめ

これらによって、負荷を生成しつつAPIエンドポイント毎の処理時間の分布が簡単に確認できるようになり、ボトルネックとなっているAPIエンドポイントを特定できました。

このツールはiOSアプリのパフォーマンステストでも利用しているので、興味がある方はこちらの記事もご覧ください。

ご紹介したソースコードは実装の概要をご紹介する為に一部簡略化している箇所や書き換えている箇所がございますのでご注意ください。他にも、実際はgolang.org/x/time/rateを利用してトークンバケット方式でバースト制御して想定外のスパイク負荷を発生させないようにしたりといった様々な工夫をしておりますが今回は省略させて頂いております。

このようにGoを利用するとロードテストツールもシンプルに実装可能です。 みなさまがパフォーマンステストを行う際の選択肢の1つとして助けになると幸いです。

私事ではありますが、汎用化を目的としてパフォーマンステストフレームワークを趣味で開発しているので、もし興味がございましたらご覧ください。

https://github.com/theoden9014/evbundler

関連リンク

この記事を読んで「面白かった」「学びがあった」と思っていただけた方、よろしければTwitterやfacebook、はてなブックマークにてコメントをお願いします! また DeNA 公式 Twitter アカウント @DeNAxTech では、Blog記事だけでなく色々な勉強会での登壇資料も発信してます。ぜひフォローして下さい!

【改訂版】継続的にiOSアプリのパフォーマンスを計測する

はじめに

SWETグループiOSチームのkariad(@kariad_uu)です。

本記事はiOSDC 2020 Japanにて発表した「継続的にアプリのパフォーマンスを計測する」の内容を元にブログという形で改めて紹介する記事となります。 発表時のスライドは以下を参照ください。

iOSチームではiOSアプリのパフォーマンス計測に取り組んできました。 iOSアプリのパフォーマンス計測方法はたくさんありますが、中でもInstrumentsを利用したパフォーマンス計測とその自動化について紹介します。

なぜパフォーマンス計測が必要なのか?

取り組んだ計測方法についてご紹介する前にアプリにとってパフォーマンスとその計測がなぜ重要なのかという点を説明します。

起動に時間がかかる、読み込みに時間がかかるアプリは動作が遅くユーザにストレスを与えてしまいます。 短時間で熱くなってしまうアプリでは端末が熱くて持てなくなってしまうだけではなくバッテリーの消費量も大きくなってしまいます。 また場合によってはパフォーマンスが悪いことでアプリのクラッシュが引き起こされる可能性もあります。 こうした問題はアプリのユーザーの離脱を引き起こしてしまう可能性があります。

アプリのパフォーマンスについてAppleが以下のドキュメントを出しています。 https://developer.apple.com/documentation/xcode/improving_your_app_s_performance

このドキュメントによるとパフォーマンス改善のサイクルを回していくことが推奨されています。 改善のサイクルを回すことでパフォーマンスが、ユーザーが離脱してしまうほど悪化する前に発見、修正できます。

Instrumentsでパフォーマンスを計測する

InstrumentsはXCUITestに組み込んで自動的に計測するような自動化の仕組みはありません。 そのため自動化し、継続的にパフォーマンス計測をするためにはツールを組み合わせる必要があります。

Instrumentsを利用して今回の事例で計測する項目は、CPU使用率とThermal State(端末温度)です。1 以前アプリの性能が悪化した際に原因を調査したところ、CPU使用率が高くなることで端末温度が上昇し、クラッシュに繋がることが判明したからです。

そして今回SWETでは次のような構成で自動計測基盤を構築しました。

  • 最新のアプリ: Bitriseでビルド&resign
  • 実機: HeadSpin
  • 計測環境: Jenkins
  • アプリ操作用UIテストフレームワーク: XCUITest
  • 計測ツール: Instruments CLI
  • アプリに負荷をかけるツール: お手製
  • 計測結果確認手段: Slack

この構成での実行フローは次のようになります。

  1. Bitriseにてreleaseビルドでipaを作成
  2. ipaに対してdevelopment証明書でresign
  3. HeadSpinにipaを配布、dSYMをArtifactsとして保存
  4. BitriseからJenkins jobトリガーを実行
  5. Jenkinsで負荷生成ツールのDL、起動、HeadSpinへの接続等の準備
  6. 計測開始と完了
  7. 結果のtraceファイルをXCUITestを用いてSSの撮影とSlackへの投稿
  8. traceファイルなどをJenkinsのArtifactsとして保存

20200930210832

構成について

なぜこのような構成となったのか、注意するべきポイントとともに、実行フローに沿って説明していきます。

最新のアプリ

コードは毎日変更されます。パフォーマンスが悪化したことをいち早く知るため変更に追従した最新のアプリで計測する必要があります。場合によってはちょっと改善を試したブランチなどもありえます。 またInstrumentsでのデバッグ用にdSYMも必要となるためこれらを毎日ビルドをして用意する必要があります。 しかしただビルドをするだけではなく、Instrumentsで正しく計測できるためにはいくつかの条件を満たす必要もあります。

  1. コンパイラの最適化をreleaseビルドと同等にする。
  2. developmentのCertificateでsignする。

Xcodeのデフォルトの設定ではdebugビルドとreleaseビルドではコンパイラの最適化の設定が異なっています。 releaseビルドでは、開発中頻繁にビルドされるdebugビルドよりもアグレッシブな最適化が行われます。最適化の差異はパフォーマンス計測結果の差異に繋がるため2、実際にユーザーが利用するreleaseビルドと同等の最適化設定でビルドされたアプリを対象に計測する必要があります。

またInstrumentsで計測する際にはdevelopmentのCertificateでsignされている必要があり、distributionではエラーとなってしまいます。

これらをまとめると「releaseと同等の最適化設定を利用しながらdevelopmentのCertificateでsign」という条件になります。 これは一見矛盾しているようにも見えます。計測用のビルドのために設定を変える方法もありますが、今回は別の方法を採用することとしました。それがipaのresignです。

ipaのresignとは生成されたipaに対して、名前の通りsignし直すことができます。 今回の例だとreleaseビルドに対してdevelopmentのCertificateでresignします。 resignにはいくつか方法がありますが、今回はfastlaneのresignを利用することにしました。 fastlaneは次のように書くことで簡単にresignが実行できます。

    resign(
      ipa: ipa_path,
      signing_identity: "iPhone Developer: Xxxxxx Xxxxxxx(FFFFFFFFF)",
      provisioning_profile: {
        "com.swet.app" => provisioning_profile_path,
        "com.swet.app.notificationservice" => provisioning_profile_notification_path
      },
      display_name: "SWET Debug"
    )

これらのビルドは元々Bitriseを利用していたため、そのままBitriseで実施しています。 そして、Bitriseから作成したipaを計測端末に配布します。

実機

Thermal Stateを計測するためには実機での計測が必要となります。 しかし実機を自前で管理すると次のような理由からコストは高くなってしまいます。

  1. テストが走っているタイミングで他のテストが実行されないように排他制御の仕組みを持つ必要
  2. OSのバージョン管理が必要
  3. 物理的な設置が必要
  4. 現在のリモート環境において問題が発生した場合に出社が必要となる可能性がある

これらの問題点を解消するためにクラウド型のデバイスファームを利用するという選択肢があります。 クラウド型のデバイスファームはデータセンターなどに設置された実機を利用できるサービスです。その中の一部サービスではWebなどから実際の手元の実機と同じように操作できる機能が提供されています。クラウド型のデバイスファームの有名所ではAWS Device FarmやRemote Testkitなどがありますが、今回はHeadSpinというデバイスファームを利用することにしました。

HeadSpinを選択した理由はすでにSWETで契約済みであり、追加で費用がかからなかったという点が大きいです。 それ以外にもHeadSpinには以下のような便利な機能があるため利用しています。

  • Webから実際の画面を見ながら操作できる
  • Xcodeから直接Runできる
  • Wi-Fiだけではなく特定のSIMで4G回線での利用もできる
  • AppiumサーバーがHeadSpin側で用意されている
  • 端末単位の契約で他社と共有することがない

20200930154745

HeadSpinはAPIも充実しています。例えば次のようなものがあります。

  • ipaのインストールとアンインストール
  • デバイスのロック、アンロック
  • OSアップデートのポップアップを消す

Bitriseからのipa配布にもこのAPIを利用しています。 その他APIも今回の構成でいくつか利用しています。

計測環境

計測する環境については最大2時間を想定としていたことからBitriseは選択肢に入りませんでした。 (本ブログ執筆時点でBitriseの最大時間は90分) またCircleCIも弊社では契約していますが、Enterprise版を利用しており、macOSでの利用は弊社では利用できません。そうした状況からオンプレで汎用性のあるJenkinsが候補となりました。

Jenkinsを選択したことでJenkins自体の管理が必要になる、という課題が発生します。 しかしSWETにはCI/CDチームが管理しているJenkinsがあります。そのJenkinsに相乗りする形で新たに管理しなくてはいけない項目を増やさずに済みました。このJenkinsはXcodeの新しいバージョンが簡単にインストールできる仕組みなどそれ以外にも便利なしくみが揃っています。またJenkinsで躓いた場合相談できるメンバーが周りにいるという点もJenkinsを採用する上での心強いポイントでした。

そのCI/CDチームがCEDEC 2020で発表した内容がこちらです。 Jenkins周りが気になる方はぜひ御覧ください。

モバイルゲーム開発におけるJenkinsクラウド時代のJenkins構築と管理テクニック

アプリ操作用UIテストフレームワーク

計測のためには、UIテストフレームワークを介してアプリを計測対象画面まで遷移させます。 採用したUIテストフレームワークはXCUITestです。

しかし最初からXCUITestを利用していたわけではありませんでした。 最初はAppium x RSpec(Ruby)を利用していました。

ここでAppiumについて軽く説明します。 AppiumはオープンソースのUIテストフレームワークで様々な言語を利用して実装できます。 その特徴としてWebDriverを用いてアプリを操作します。

20200930210826

上図のとおりAppiumの実行にはAppiumサーバーが必要ですが、相性のよいことにHeadSpin自体がAppiumサーバーの実行環境を用意しています。そこで当初は、AppiumのほうがXCUITestより良い選択肢だと考えていました。

Appiumで起きた問題

Appiumを利用する上でいくつかの問題が発生しました。

  • HeadSpin上のAppiumサーバーを利用する場合Xcodeのバージョンを柔軟にコントロールできない
  • HeadSpin上のAppiumサーバーを利用する場合traceファイルの転送が必要となり転送先を用意する必要がある
  • 原因不明だがconnection errorが発生する

Instrumentsの実行はAppiumサーバーと同じ環境で実行されます。そのため今回の場合はHeadSpin側でInstrumentsも実行されることとなり、向こう側のXcodeのバージョンに依存することとなります。 またInstrumentsの計測結果であるtraceファイルの転送も必要となり、転送先を考える必要がありました。 これらを考慮したときにJenkins上でAppiumサーバーを持つことで、Xcodeのバージョンは簡単に切り替えることができ、traceファイルもJenkinsのArtifactsとして保存すれば良いだけとなることからJenkins側でAppiumサーバーを持つ形へと変更することとなりました。

最後の問題として、負荷をかけ続けた状態で一定時間経つとAppiumで新しいコマンドを実行した際にconnection errorが発生しました。 原因を調査しましたが、詳細はわかりませんでした。しかし前述の理由でAppiumサーバーをJenkinsで立てることになり、Appiumを使い続ける理由がほぼなくなっていたため、XCUITestの挙動を確認することにしました。 すると安定して動作したためXCUITestへ移行したというのが現在です。

アプリに負荷をかけるツール

アプリに負荷をかけ続けた状態でのパフォーマンスを計測することにしました。 そのため、SWETの他チーム(Goチーム)のメンバーと協力して負荷生成ツールを作成しました。 このツールをJenkins上で同時に実行しています。

計測ツール

計測ツールについては以下の理由からInstrumentsを利用することにしました。

  • すでにパフォーマンスが問題となっており、ユーザーへ届ける前に問題がないかを知る必要があった
  • 問題がある場合は素早くその原因を特定し解決したい
  • 一定時間の負荷をかけた状態での端末の温度とCPU使用率の変化を計測したい

これらを満たせるのが現時点ではInsturmentsしかありませんでした。

InstrumentsはXcodeの一部として提供されているツールです。 アプリのパフォーマンスを計測するだけではなく、どこの処理のパフォーマンスが悪いのかまで特定できます。 今回はその特定まで行いたいという動機がInstrumentsを採用した大きな理由の1つです

Instruments実行方法

InstrumentsはInstruments.appとInstruments CLIという2種類に分けることができます。 結果の確認はInstruments.appでしかできませんが、計測だけならばどちらでも可能です。 そのため、コマンド1つで実行できるInstruments CLIを利用しました。 Instruments CLIはAppiumからも利用できます。

計測結果確認手段

Instrumentsではtraceファイルから計測結果を定量的な数値で取得する方法がありません。 (実際にはある程度取れる外部ツールが存在したのですが、この時点では存在を知りませんでした) そのため、結果の確認にはtraceファイルをInstruments appで開き、GUIで確認する必要がありました。 しかし負荷をかけ続けての長時間の計測ともなるとファイルサイズが150〜200MBと大きく、Instruments appで開くまでに1分以上かかることもあります。これを毎回手動で結果確認をするのは面倒です。

その解決策としてInstruments appをXCUITestで操作してスクリーンショットを撮影、Slackに投稿させるという方法を取りました。 Thermal Stateは次のような画面で結果を確認できます。

20200930154923

state 説明
Nominal 平常時、問題がない状態
Fair 対応が必要なほどではないが熱くなり始めている
Serious 非常に熱く、アプリ自体にも影響が出始める
Critical 今すぐに冷やす必要がある

またこの各stateの開始時間と終了時間がThermal Stateのグラフを選択することで詳細な情報としてみることができます。

続いてCPU使用率についても実際のスクリーンショットをもとに説明していきます。

20200930155118

CPU使用率に関してはGUIでもとても数値が見づらいです。 CPU使用率の絶対値はグラフでしか確認できません。 しかもそのグラフでさえもグラフの天井へ張り付いたときの数値が固定ではなくその計測回の一番高い数値になります。そのため複数の計測結果のグラフを並べてもグラフだけではどちらのCPU使用率が高いかわかりません。グラフにマウスカーソルを合わせることで初めて具体的な数値がわかります。 またグラフを選択した際に表示される詳細情報では選択した時間での全体のCPU使用率を100%とした場合の具体的な処理毎の使用率内訳が表示されます。つまり全体の使用率の平均などを見ることはGUIでもできません。

これらのスクリーンショットを撮影してSlackに投稿していますが、Thermal Stateについては詳細から各stateの文字列も取得できるため、そこからCriticalに到達したら失敗させるといったことも可能になりました。 一方でCPU使用率についてはスクリーンショットを撮影していますが、それだけではわからずtraceファイルをInstruments appで見なくてはわからないままです。

20200930155209

パフォーマンス計測で注意するべきこと

これらを組み上げる間には手元で確かめたりと様々な試行錯誤を重ねました。その中でパフォーマンス計測していく上で注意する必要があると気がついた点があります。

端末の状態

計測は1パターンだけでなくいくつかのパターンで計測したい場合があります。 しかし連続して同じ端末で計測すると、前の計測で既にThermal Stateが上がりきった状態で計測を開始してしまうため正しい計測結果が得られません。 環境にもよりますが、端末が冷えて前回の影響を受けずに計測するためには30分~1時間の間隔を開ける必要があります。 この問題には私達も直面し、そこで取った対応として端末数を増やして、さらに次のような実行計画を組むことでなるべく時間のロスなく計測パターンに対応させました。

20201021194915

Thermal Stateなど、物理的に影響のある項目を計測する場合には前回の計測から間を空けて、影響を受けないようにすることが必要になります。

外部気温

空調などで完全に管理された空間で無い限り物理的な端末での端末温度の計測は外部気温の影響を受けます。 それにより冬では大丈夫でも夏にはとても熱くなってしまうということもありえます。 性能が悪化していなくてもユーザーからすると使いづらい状況になるため、パフォーマンスの改善したほうが良いでしょう。 また上記で連続して計測する際に端末が熱い状態で開始すると正しく計測できず、クールタイムが必要になると説明しました。このクールタイムも外部気温が高いほど端末は冷えにくくなるため同じ端末で連続して計測する際には注意が必要となります。

これからについて

まだまだ改善していきたいところやまだやれていないことがたくさんあります。 今後やっていきたいことには次のようなものがあります。

  • xctraceによる計測結果の確認
  • 計測項目の追加と結果確認方法の改善

xctrace

Xcode12からinstrumetsコマンド(Instruments CLI)がdeprecatedとなります。 代わりにxctraceというツールが追加されました。 このxctraceは基本的にはinstrumentsコマンドを置き換えたものになるのですが、新しい機能も追加されています。 その中で最も特徴的なものがXML形式でのデータのexportです。 これによりtraceファイルをInstruments appで開かずとも計測結果のデータを取得できるようになります。 実際にThermal Stateは詳細に表示されていた各stateの開始時間と終了時間がexportできるようになりました。 一方でCPU使用率についてはまだxctraceで取得できません。 これはそもそもグラフでしか表現されていないのが問題かもしれませんが、いつか対応されることを期待しています。

xctraceの使い方

ここでxctraceのexport機能について紹介したいと思います。 以前Xcode12についての記事を書いたのですが、その時点ではまだbeta版であり、なおかつxctraceに関するドキュメントがmanコマンド以外ほぼ存在しないという状態でした。 そのため詳細の紹介を控えたのですがめでたくXcode12がリリースされたため、私が試したexport機能について、私が理解した範囲で紹介します。 また予め断りを入れておきますが、manコマンド以外のドキュメントが無く手探りで試して得られた利用方法のため、正しくない可能性があります。ご了承ください。

xctraceにはrecord、import、export、list、helpの5つコマンドが存在します。 その中でもexportがxctraceから使えるようになったtraceファイルのデータをXMLで出力できるコマンドです。 exportコマンドは次のように使います。例としてTime ProfilerのTemplateで計測した結果を利用します。

いきなり詳細を出力する前に--tocでTOC(Table of contents、計測項目の一覧と思われるが明確な記載は無いので推測です)を出力します。

$ xcrun xctrace export --input xx.trace --toc 

すると次のようなXMLで表現された結果が得られます。

<?xml version="1.0"?>

<trace-toc>
    <run number="1">
        <info>
            <target>
                <device name="device name" uuid="udid"/>
            </target>
            <summary/>
        </info>
        <data>
            <table schema="tick"/>
            <table schema="device-thermal-state-intervals"/>
            <table target-pid="ALL" kdebug-match-rule="0" exclude-os-logs="0" schema="region-of-interest" signpost-code-map="&quot;&lt;null&gt;&quot;"/>
            <table schema="os-log" category="PointsOfInterest"/>
            <table target="ALL" schema="kdebug" codes="&quot;0x1,0x25&quot;"/>
            <table target="ALL" schema="kdebug" codes="&quot;0x2b,0xd8&quot;"/>
            <table target="ALL" schema="kdebug" codes="&quot;0x2b,0xdc&quot;"/>
            <table target="ALL" schema="kdebug" codes="&quot;0x1f,0x7&quot;"/>
            <table codes="&quot;0x2d,*&quot;" schema="kdebug" target="ALL" callstack="user"/>
            <table target="ALL" schema="kdebug" codes="&quot;0x2b,0x87&quot;"/>
            <table codes="&quot;0x31,0xca&quot;" schema="kdebug" target="ALL"/>
            <table category="InduceCondition" schema="os-signpost" subsystem="&quot;com.apple.ConditionInducer.LowSeverity&quot;"/>
            <table target-pid="ALL" kdebug-match-rule="0" exclude-os-logs="0" schema="roi-metadata" signpost-code-map="&quot;&lt;null&gt;&quot;"/>
            <table schema="life-cycle-period" target-pid="ALL"/>
            <table codes="&quot;0x2b,0x65&quot;" schema="kdebug"/>
            <table codes="&quot;0x1,0xa&quot;" schema="kdebug" callstack="user"/>
            <table schema="os-signpost" category="PointsOfInterest"/>
            <table schema="tick" frequency="1"/>
            <table codes="&quot;46,2&quot;" schema="kdebug" callstack="user"/>
            <table sample-rate-micro-seconds="1000" all-thread-states="NO" schema="time-sample" target="ALL" callstack="user"/>
            <table codes="&quot;0x21,0xa&quot;" schema="kdebug" callstack="user"/>
            <table schema="gcd-perf-event" target-pid="ALL"/>
            <table schema="os-signpost-arg" category="PointsOfInterest"/>
            <table target-pid="ALL" exclude-os-logs="0" schema="global-poi-layout" signpost-code-map="&quot;&lt;null&gt;&quot;" colorize-by-arg4="0"/>
            <table target-pid="ALL" kdebug-match-rule="0" schema="global-roi-layout" signpost-code-map="&quot;&lt;null&gt;&quot;" colorize-by-arg4="0"/>
            <table schema="os-log-arg" category="PointsOfInterest"/>
            <table target-pid="ALL" high-frequency-sampling="0" schema="time-profile" needs-kernel-callstack="0" record-waiting-threads="0"/>
            <table target-pid="ALL" schema="kdebug-signpost" signpost-code-map="&quot;&lt;null&gt;&quot;"/>
            <table schema="thread-name"/>
        </data>
    </run>
</trace-toc>

詳細を見るためにはこのTOC XMLの階層を--xpathオプションでたどる必要があります。 例えばこのTOCからThermal Stateの詳細を得るためのコマンドが次になります。

$ xcrun xctrace export --input xx.trace --xpath '/trace-toc/run[@number="1"]/data/table[@schema="device-thermal-state-intervals"]'

このコマンドを実行すると以下のような結果が得られます。

<?xml version="1.0"?>
<trace-query-result>
  <node xpath='//trace-toc[1]/run[1]/data[1]/table[2]'>
    <schema name="device-thermal-state-intervals">
      <col>
        <mnemonic>start</mnemonic>
        <name>Start</name>
        <engineering-type>start-time</engineering-type>
      </col>
      <col>
        <mnemonic>duration</mnemonic>
        <name>Duration</name>
        <engineering-type>duration</engineering-type>
      </col>
      <col>
        <mnemonic>end</mnemonic>
        <name>End</name>
        <engineering-type>start-time</engineering-type>
      </col>
      <col>
        <mnemonic>thermal-state</mnemonic>
        <name>Thermal State</name>
        <engineering-type>thermal-state</engineering-type>
      </col>
      <col>
        <mnemonic>track-label</mnemonic>
        <name>Track</name>
        <engineering-type>string</engineering-type>
      </col>
      <col>
        <mnemonic>is-induced</mnemonic>
        <name>Is Induced</name>
        <engineering-type>boolean</engineering-type>
      </col>
      <col>
        <mnemonic>narrative</mnemonic>
        <name>Narrative</name>
        <engineering-type>narrative</engineering-type>
      </col>
    </schema>
    <row>
      <start-time id="1" fmt="16:03.938.891">963938891916</start-time>
      <duration id="2" fmt="12.28 min">737085646124</duration>
      <start-time id="3" fmt="28:21.024.538">1701024538040</start-time>
      <thermal-state id="4" fmt="Serious">Serious</thermal-state>
      <string id="5" fmt="Current">Current</string>
      <boolean id="6" fmt="No">0</boolean>
      <narrative id="7" fmt="Serious thermal state">
        <thermal-state ref="4"/>
        <narrative-text id="8" fmt=" thermal state"> thermal state</narrative-text>
      </narrative>
    </row>
    <row>
      <start-time id="9" fmt="09:48.940.922">588940922875</start-time>
      <duration id="10" fmt="6.25 min">374997969041</duration>
      <start-time ref="1"/>
      <thermal-state id="11" fmt="Fair">Fair</thermal-state>
      <string ref="5"/>
      <boolean ref="6"/>
      <narrative id="12" fmt="Fair thermal state">
        <thermal-state ref="11"/>
        <narrative-text ref="8"/>
      </narrative>
    </row>
    <row>
      <start-time id="13" fmt="00:00.000.000">0</start-time>
      <duration id="14" fmt="9.82 min">588940922875</duration>
      <start-time ref="9"/>
      <thermal-state id="15" fmt="Nominal">Nominal</thermal-state>
      <string ref="5"/>
      <boolean ref="6"/>
      <narrative id="16" fmt="Nominal thermal state">
        <thermal-state ref="15"/>
        <narrative-text ref="8"/>
      </narrative>
    </row>
  </node>
</trace-query-result>

中身を見てみると、Thermal stateの変化について出力されています。 開始から9.82minがNominal、その直後から6.25minがFair、最後にSeriousが12.28min、あることがわかります。 これはInstruments.appのGUIでThermal stateを選択した際の詳細情報として表示されていたものと同等のものが出力されているように見えます。

例としてThermal stateで試しましたがschemaにある項目であればすべて表示可能です。しかしTime Profilerなどはとてつもない長さのXMLが出力されるなど、正直あまり使い勝手がいいとは言えない気はします。 まだ最初のリリースなのでこれからに期待したいところです。

他項目の計測と結果確認方法の改善

現在他項目の計測も進めています。 項目によってはInstrumentsではなく別の方法で計測するのですが、結果をBigQueryに格納し、DataStudioで閲覧できるように準備中です。 今回の計測についてもこのフォーマットに合わせて閲覧できると計測結果がまとめて確認できるようになるためデータの可視化というのを進めていきたいと考えています。 その他MetricKitなど実際のユーザ環境での計測も検討しています。

まとめ

SWETが取り組んだパフォーマンス計測についてiOSDC Japan 2020で発表した内容をもとに計測の一例を紹介しました。

すべてのアプリがThermal stateを見る必要があるかというと必ずしもそうではないかもしれません。 大切なのは自分のアプリがどんな課題を持ちうるか検討した上で早めにパフォーマンス計測の仕組みを導入しておくことです。

今回紹介した計測でもさらなる改善や異なる観点での計測も考えています。 これからもパフォーマンス計測についてSWETでは取り組んでいきますのでさらなる知見が溜まったらまたブログ等で発信していきたいと思います。

最後に今年のiOSDCではViewの表示、バッテリーなど他にもパフォーマンスに関する発表がありました。 他社がどのようにパフォーマンス計測に対して取り組んでいるかを知ることができ、とても有意義でした。 発表については聞いてくださった皆様ありがとうございます。 当日質問できなかった、このブログを読んで気になることができた等あれば片山までTwitterでぜひお気軽に聞いてください。


  1. InstrumentsはCPU使用率とThermal State以外にも様々な項目を計測可能です。

  2. パフォーマンスへの影響についてはWWDC2019「Getting Started with Instruments」のセッションでも述べられています。

形式手法でデータ構造を記述・検査してみよう:Alloy編

SWETの仕様分析サポートチーム所属のtakasek(@takasek)です。

仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています(形式手法 カテゴリーの記事一覧)。

当記事は、Kuniwak(@orga_chem)により社内開催されたAlloyガイダンスを元に再構成した記事です。よく知られたデータ構造であるStackを形式仕様記述しビジュアライズすることで、Alloyの使い方と利点を実感できます。Alloy未経験者でもステップバイステップで試せるように構成しました。是非、お手元にAlloyをインストールして読み進めてください。環境はAlloy 5.1.0を想定しています。

https://github.com/AlloyTools/org.alloytools.alloy/releases

Alloyとは

形式手法の言語およびツールです。システムの構造の制約や振る舞いを簡易に、しかし強力に記述できるようデザインされています。記述されたモデルは要素同士の関係グラフとして視覚化できるというのが特徴です。

もっとも単純なモデルを記述する

Alloyのエディタを起動したら、以下を記述してください。

sig A {}

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

sig はsignatureを意味し、atom(要素)の集合を示します。signatureはオブジェクト指向プログラミングのclassと書き方がなんとなく似ていますが、その実態はまったく異なるものなのでご注意ください。

Executeの結果

ExecuteボタンをクリックするとVisualizerが開きます。Visualizerでは、Nextボタンをクリックするたびにインスタンスが次々とグラフとして表示されます。インスタンスというのは、関係における変数を特定の値で束縛したものです。1

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

Aのatomが0, 1, 2, 3, 4個存在する例を確認できました。現実的には当然5個以上になることもありますが、個数が増えると探索コストが急激に増大するためAlloyは割り切ってデフォルトの探索範囲を少なくしています。それでもおおよその反例は見つかるだろうという前提を小スコープ仮説といいます2。もし無限のケースについて正しさを証明したい場合は、CoqやIsabelleに代表される定理証明支援系の技術が必要になります。

2シグネチャの関係を記述する

sigを2つに増やして、その関係を記述してみましょう。

sig A {
    b: B // 集合Aに属する各々のatomは、集合Bに属するただ1個のatomと関係を持つ
}

sig B {}

Executeの結果

抜粋すると…

関係 グラフ
Aの要素:0個
Bの要素:1個
Aの要素:1個
Bの要素:2個
Aの要素:2個
Bの要素:2個
Aの要素:2個
Bの要素:2個

最後の例があることは提示されて初めて気づく人も多いのではないでしょうか。このように、パターンを網羅的に目で見て確認できるのがAlloyの良いところです。

関係の多重度は、さまざまな形で表現可能です。

sig A {
    b: B, // 1個の要素への関係
    c: one C, // 1個の要素への関係(※省略はoneを意味する)
    d: lone D, // 0〜1個の要素への関係
    e: set E // 0個以上の要素への関係
    // 他にもあります
}

Stackを表現する

ここからが本題です。Stackをモデルとして記述していきましょう。見慣れた連結リストです。

sig Stack {
    value: univ,
    next: lone Stack
}

Stack というsignature、すなわち集合を定義しました。

Stackvaluenext という2つのフィールドを持つsignatureです。フィールド value は、Stackに属する各々のatomと、univに属するただ1個のatomとの関係を示します。フィールド next は、Stackに属する各々のatomと、Stackに属する0〜1個のatomとの関係を示します。なお、univは「あらゆるatomが属する集合」を意味しています。

(勘の良い方は、このモデリングに「おや?」と思われたかもしれません。後ほどその点にも触れますので、今はこのまま読み進めてください)

ここまで書けたら、Executeします。

ビジュアライズの結果を読み解く

結果を見る前に…

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

数値が変わるだけの同じような例が連続して出てきてキツいですね。よく見るとVisualizerのステータスバーに Run Default for 4 but 4 int, 4 seq expect 1 とあります。実はAlloyは、Executeの対象がない場合は暗黙的に以下のような出力命令が省略されているものと解釈しているようです(Alloy5現在)。

run{} for 4 but 4 int, 4 seq expect 1

for 以下は、Visualizerの表示要素数の範囲(スコープ)を示します。なお省略されたrunに任せず明示的に run {} と書いた場合には、 run{} for 4 but 4 int, 4 seq expect 1 よりも少量のインスタンスがビジュアライズされるようです。なぜそうなるのかは調査できていません。

ビジュアライズ結果を読み解く

run {} で再度Executeして、ビジュアライズされた関係グラフを読み解きましょう。最初のグラフはこれですが…

いきなり想定外のグラフです。Visualizer上の Stack のnextが自分自身になっています。データ構造としてStackは循環を許しません。

「Stackは循環しない」という不変条件を書く

Stackが循環しないことを示すためには「このモデルは常にこうなる」という制約を与える論理式(不変条件)を書く必要があります。sig 内の記述だけに着目すれば成立するインスタンスでも、与えられた制約に違反する場合はビジュアライズされません。

「nextは自分自身にはならない」ことを示す

ただし不変条件を正しく書けなかった場合、正常なはずのインスタンスも表示されなくなってしまい、かつそれに気づけないリスクがあります。人間は異常なものを見つけることは得意ですが、あるべき正常なものの欠損に気づくのは苦手です。まずは論理式が本当に過不足のない制約を表現しているかを確認すべきです。

そのために表明(assert)を使います。不変条件はモデルに対して強制的に適用される論理式ですが、表明は現状のモデル自体には影響を与えず「モデルの制約はそうなっているはず」を表現する論理式です。3

今回、Stackが循環しないことを示すには「nextは自分自身にはならない」論理式を書きます。

// 「すべてのStackについて、自身のnextの集合に、自身が含まれない」という表明
assert TestRecursion {
    all s: Stack | s not in s.next
}
// check命令は、表明に違反するインスタンスがないかを確認します
check TestRecursion

ツールバーから Execute > Check TestRecursion すると、コンソールに以下のようなメッセージが表示されました。

Executing "Check TestRecursion"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   483 vars. 72 primary vars. 827 clauses. 7ms.
   Counterexample found. Assertion is invalid. 3ms.

反例(counterexample)、すなわち現状のモデルの中で表明に違反するインスタンスが見つかりました。グラフとして確認できるので見てみましょう。

いいですね。「すべてのStackについて、自身のnextの集合に、自身が含まれない」の反例……すなわち「自分自身がnextになる」インスタンスだけが出力されています。表明をそのまま不変条件に昇格させれば「常にモデルがそれを満たす」という制約の記述になります。

記述全体は以下のようになります。不変条件の記述は fact です。

sig Stack {
    value: univ,
    next: lone Stack
}
fact NoRecursion {
    all s: Stack | s not in s.next
}

不変条件を加えたモデルが想定どおりか、runして確認していきましょう。

run {}

すると、気になるものが見つかりました。

あるStack自身の循環はなくなりましたが、 Stack0.nextStack1Stack1.nextStack0 という間接的な循環が残っています。

「nextを辿った先が自分自身にはならない」ことを示す

「nextは自分自身にはならない(s -(next)-> s)」ことは示しましたが、それだけでは足りなかったのです。 s -(next)-> ... -(next)-> s という関係を表現する必要があります。

そのためには推移閉包を使います。厳密な定義は置いといて、ざっくり言えば「関係Rについて s1 -(R)-> s2 s2 -(R)-> s3 が言えるとき s1 -(R)-> s3 も言える」という関係の集合が推移閉包です。Googleイメージ検索したら感覚は掴めると思います。Alloyには推移閉包オペレータがあり、 ^ をつけるだけで推移的関係を表現可能です。

……というのは本当でしょうか? 我々には確認の手段があります。Alloyの力を借りましょう。 fact NoRecursion はそのまま、表明を追加します。最初に書いたTestRecursionからの差分は、nextに推移閉包オペレータをつけただけです。

...
fact NoRecursion {
    all s: Stack | s not in s.next
}
assert TestRecursion {
    all s: Stack | s not in s.(^next)
}
// 似たようなIntの例が多すぎて邪魔なので、forでスコープを絞ってcheckします
check TestRecursion for 2 Int

再びツールバーから Execute > Check TestRecursion します。さっき見つけた双方向の矢印のパターンが反例として上がってくればしめしめです。どうでしょうか……

nextが双方向の矢印になる例だけが見つかりました。Stackの表示要素数が2個より多い場合の関係も検査してみましょう。

check TestRecursion for 2 Int, 4 Stack

3個のStackが循環参照している反例が見つかりました。いい感じです。

では、表明を不変条件に格上げします。

fact NoRecursion {
-    all s: Stack | s not in s.next
+    all s: Stack | s not in s.(^next)
}

含意の確認をする

ちょっと待ってください。本当にこの格上げは正しいのでしょうか。推移閉包によって「nextを辿った先が自分自身にはならない」ことを表現できました。しかし、これを満たすとき、今までの「nextは自分自身にはならない」も満たすかと言われると確証がありません。感覚的には間違っていないように思えますが、論理の力で保証したいところです。

つまり、論理式「『nextを辿った先が自分自身にはならない』ならば『nextは自分自身にはならない』」が正しいことを確認したいのです。

assert TestImplies {
    (all s: Stack | s not in s.(^next))
        implies (all s: Stack | s not in s.next)
}

implies は含意、つまり論理学の初歩で習う「AならばB」です。

check TestImplies をExecuteすると、コンソールに以下のメッセージが表示されました。

Executing "Check TestImplies"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   560 vars. 72 primary vars. 907 clauses. 16ms.
   No counterexample found. Assertion may be valid. 2ms.

反例が見つからないということは、「『nextを辿った先が自分自身にはならない』ならば『nextは自分自身にはならない』」は正しいようです。不変条件の格上げは適切だと自信を持てました。

valueの不変条件を書く

ここまでで、全体の記述は以下のようになっています。

sig Stack {
    value: univ,
    next: lone Stack
}
fact NoRecursion {
    all s: Stack | s not in s.(^next)
}

run {} for 1 Int

runの結果……

value周りにおかしな関係が見つかりました。「Stack0.nextStack1」「Stack1.nextStack1」など、あるStackのvalueがStackだったケースでは循環が生まれてしまうようです。

その原因は、valueの属する集合が univ すなわち「あらゆるatomの集合」になっているせいです。

どのように対処しましょうか。

  • valueフィールドとnextフィールドの関係を適切に記述する
  • 「valueはStackにならない」という仕様で逃げる

理想的なのは前者ですが割愛します。腕に自信のある方は正面突破してみましょう。今回は「valueはStackにならない」という仕様を導入して逃げることにします。より厳密な日本語で表現するなら「すべてのStackについて、自身と関係するvalueはStackではない」というべきでしょうか。

assert TestValue {
    // ここに「すべてのStackについて、自身と関係するvalueはStackではない」という論理式を書く
}

もしあなたが手元にAlloyをインストールして進めているなら、ちょうどいい練習問題なので自分で書いてみましょうか。すこしスペースを空けますね。

...

...

...

...

...

答え合わせです。 答えのひとつは、次のとおりです。

assert TestValue {
    all s1, s2: Stack | s1.value not in s2
}

check TestValue for 1 Int, 4 Stack で検査してみるといいでしょう。

論理式をリファクタする

実は all s1, s2: Stack | s1.value not in s2 はベストな解ではありません。よりシンプルに書くなら、

all s: Stack | s.value not in Stack

で十分です。

そういうことなら…と書き換える前に、一度立ち止まりましょう。プログラミングでもそうですが、リファクタリングでは修正前後に記述の意味が変化してしまってはいけません。論理の世界の言葉で言い換えると「修正前の論理式と修正後の論理式が同値である」ことを確かめたいです。

そこで、式変形前後での同値性の確認のテクニックを紹介します。手順は先述した含意の確認とよく似ています。

assert TestTrans {
    (all s1, s2: Stack | s1.value not in s2)
        iff (all s: Stack | s.value not in Stack)
}

iffif and only if の略で「Bのときに限りAが成り立つ。Aが成り立つのはそのときに限る」つまり必要十分条件を示します。そのような論理式は同値として扱えます。オペレータとして <=> と書くこともできます。

check TestTrans をExecuteすると、コンソールに以下のメッセージが表示されました。

Executing "Check TestTrans"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   1158 vars. 69 primary vars. 2196 clauses. 7ms.
   No counterexample found. Assertion may be valid. 3ms.

反例が見つからないということは、修正前後の論理式は同値だということです。より大きなスコープで反例が見つかる可能性を頭の片隅に常に置いておく必要がありますが、今回は大丈夫でしょう。自信を持って書き換えましょう。なお、もし反例があった場合にはVisualizerでグラフとして確認可能です。Alloyは便利ですね。

完成したモデルを確認

sig Stack {
    value: univ,
    next: lone Stack
}
fact NoRecursion {
    all s: Stack | s not in s.(^next)
}
fact NoRecursiveValue {
    all s: Stack | s.value not in Stack
}

この記述が適切なものか確認しましょう。

run {} for 1 Int, 4 Stack

よさそうです。

push, popの前後関係をpredで表現する

データ構造のStackに対しては、pushとpopという操作が可能です。その確認もしたいです。

Alloyの状態モデルではミュータブルな手続きを書くことはできません。かわりに操作前後の状態を別物(事前状態、事後状態)として扱います。事後状態は慣習的に ' をつけて表記します。

  • push前のStack = s
  • push後のStack = s' (読みはs-prime)

s になんらかの値をpushした状態」と「s'」が同値だと示す論理式を書けば、前後の関係が表現できます。

任意個数の変数から真理値(true/false)を導く論理式を述語(predicate)といいます。これまで書いてきた run {}{} も、実は述語です。このrun命令は、次のように分解できます。

pred P {} // 述語の宣言と定義
run P     // 定義した述語に対する出力命令

pushを表現したいなら、次のような三変数述語になります。なお改行はandを示します。

pred Push[s, s': Stack, x: univ] {
    s'.value = x
    s'.next = s
}

この述語を満たす関係を run Push for 1 Int, 4 Stack でビジュアライズすれば、push前後のStackの関係が読み取れます。

上図の表記は、以下を意味します。

  • $Push_sPush の変数の s
  • $Push_s'Push の変数の s'
  • $Push_xPush の変数の x

sx をpushした結果が s' になることが図示できていますね。

popについても同じように書けます。難しいところはないので特に説明しません。練習問題として試してみるとよいでしょう。

まとめ

AlloyでStackを記述・検査する一連の流れを通じて、Alloyの使い方を紹介しました。とっつきやすいツールですので、是非ご活用ください。

仕様が妥当なものか確認せずに、手続き的に複雑な仕様を作り上げてしまうことはよくあります。形式仕様記述を用いて仕様をシンプルに書き、ときにリファクタしながら研ぎ澄ませると、より安全で自信に満ちあふれた開発プロセスが手に入るかもしれません。

なお、本記事よりも高度な記述が知りたい場合は公式のlanguage referenceをご参照ください。 https://alloytools.org/download/alloy-language-reference.pdf

SWET視点でピックアップしたテストに関するWWDC 2020まとめ

お久しぶりです。 SWETグループの平田(@tarappo)と片山(@kariad_uu)です。

本稿では、先日オンラインでおこなわれたWWDC2020の中から、SWET視点で気になった次の2点について紹介したいと思います。

  • The suite life of testing
  • Instruments周り

これら以外にもテスト周りの追加としては待望の「Xcodeを用いたStoreKitのテスト」がありますが、本記事では割愛します。

本記事でアップしているXcodeの画像はXcode11.6でとった画像となります。 Xcode12では見た目が変わっている可能性があります。

The suite life of testing

まず、WWDC2020で公開された「The suite life of testing」について平田が紹介していきます。

WWDC2020では「The suite life of testing」として次の5つの動画が公開されています。

  • Handle interruptions and alerts in UI tests
  • Get your test results faster
  • XCTSkip your tests
  • Triage test failures with XCTIssue
  • Write tests to fail

これらの動画での説明はそれぞれがある程度関係をしていて、大きくまとめると「自動テストが失敗したときの対応」についての話がメインといえます。

そこで、ここでは1つ1つの動画の中身について説明するのではなく、これらの動画を簡潔にまとめて説明をします。 (なお「Handle interruptions and alerts in UI tests」についてはUIテスト時の割り込みやアラートをどのように対応するかの話なので今回は除外します)

自動テストは常に成功するわけでなく失敗もします。 この自動テストの失敗時の調査は、テストコードを維持し続けるために大事なことです。 しかし、調査にコストがかかりすぎてしまうのは問題です。

このコストがかかりすぎないように、動画内でも説明されているものとして、次の2つの観点で説明をしていきます。

  • フィードバックを早くする
  • フィードバックからの情報取得

フィードバックを早くする

自動テストからのフィードバックは早いことが望ましいです。 たとえば、CI/CDサービスで自動テストを動かしていて、いつまでたっても終わらないといったことが起きてしまうと結果を待ちきれなくなってしまいます。

その結果、自動テストを実行しないといったことにもつながってしまう恐れがあります。

次をおこなうことでフィードバックを早くできます。

  • テストの実行時間の制御
  • テストのスキップ
  • 並列実行

これらについて次に説明をしていきます。

テストの実行時間の制御

必要な理由

テストの実行時間がのびてしまう原因の1つとして、自動テストが想定の時間以上かかってしまうということがあります。

たとえば、テストのハングにより自動テストが終わらなかったとします。

その場合、CI/CDサービスの制限時間や実行している環境(デバイスファームなど)の制限時間により、テストが無理やり終了させられてしまうことになります。

そうすると、テストが無事に終了していないため自動テストの結果を得ることも出来ずに、なにが問題だったのかがわからなくなってしまいます。

Xcode11.4でテストの実行時間を制御できるようになりました。

この機能を利用することで、特定の時間以上がかかった場合にそのテストを失敗扱いにできます。

これにより、想定外の挙動をしてテストが終了せずに実行時間が長くなってしまうといったことを止めることができます。

制限時間の設定

本機能はTestPlansで下記画像にあるように「Test Timeouts」をONにすることで利用できるようになります。

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

テストの制限時間はデフォルトで10分が指定されています。 この値は、複数の方法で変更できます。

その際の優先度は次のとおりです。

  1. テストコード側で利用するexecutionTimeAllowance API
  2. テスト実行時に指定するxcodebuildのtimeallowanceオプション
  3. TestPlansの設定
  4. デフォルトの時間(10分)

これらの設定方法のうち、Xcode12から3にあるTestPlansからも値を設定できるようになりました。

これらの指定する値は、秒数で指定できますが注意が必要です。 たとえば、60秒未満を指定した場合は1分に切り上げられます。 100秒であれば、2分に切り上げられます。

この指定した時間以上に実行時間がかかった場合、Xcode上では次のようなエラーが表示されます。

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

この画像の例では制限時間を1分と指定していて、テストの実行時間がその時間を過ぎています。

なお、エラーが出たときの情報の詳細はXcode12からより詳細に出るようになったので、後述します。

テストのスキップ

必要な理由

自動テストを実装している中で、実行する環境に依存するようなテストを実装することもあります。

たとえば、ユニバーサルアプリでiPadのみで動くテストとか、特定のOSバージョン以上で動作するテストなどです。

これらはすべてテストの実行時にしか判断できない条件になります。 今まではXCTestではテストの結果は「成功」または「失敗」しかありませんでした。

そのため、実行環境によって動かないテストは求めている実行環境以外で動作したときに「成功」または「失敗」のどちらかになるようにするか、またはそのテスト自体を無効化するかといった選択肢しかありませんでした。

成功とすると、テストを実行していないのに問題ないという判定をすることになります。 失敗とすると、何も問題が発生していないのに落ちた原因をチェックするコストを使うことになります。

Xcode11.4からテストをスキップできるXCTSkipというAPIが追加されました。 これにより、特定の条件の際に自動テストをスキップできます。

XCTSkipを利用してテストのスキップ

このXCTSkipを利用することで、明示的にテストを特定条件の際にスキップできます。

例えば次のコード例のようにXCTSkipUnlessを利用することで、実行デバイスがiPadでなければテストをスキップできます。

func testSkipExample() throws {
    try XCTSkipUnless(UIDevice.current.userInterfaceIdiom == .pad, "iPad only")
    
    //なにかしらの処理
}

このようにテストをスキップさせた場合、Xcode上では次のように表示されます。 今までは「成功の緑」と「失敗の赤」だけでしたが、この「スキップのグレイ」が増えました。

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

また自動テストはCI/CDサービスで動かすと思います。 そのため、CLI上で動かしたときに生成されるテスト結果にもテストが成功・失敗の情報だけでなくスキップされた情報も必要になります。

利用できるテスト成果物として、Xcode11から追加されたResult Bundleがあります。 このResult Bundleは次のコマンドを用いることでJSONフォーマットとして情報を生成できます。

$ xcrun xcresulttool get \
  --path ResultBundle.xcresult \
  --format json

生成された情報の一部は次のようになります。 これを見るとわかりますが、testSkippedCount としてスキップの情報もあることがわかります。

  "metrics" : {
    "_type" : {
      "_name" : "ResultMetrics"
    },
    "errorCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "2"
    },
    "testsCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "3"
    },
    "testsFailedCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "1"
    },
    "testsSkippedCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "1"
    }
  }

このResult Bundleを活用することにより、CI/CDサービスで自動テストを実行した場合でも、テストの「成功」「失敗」「スキップ」といった情報を取得できます。

Result Bundleについては、以前本ブログで書いた記事を参考にしてもらえればと思います。

並列実行

必要な理由

並列実行は自動テストにおいてよくある実行時間の短縮の方法です。 テストを分割しておこなえるために、トータルとしての実行時間が短くできます。

XCTestにおいてもいろいろな方法で並列実行をおこなうことができますが、Xcode10からiOSシミュレーターの並列実行が容易にできるようになっています。

ただし、並列実行をすれば必ずしも実行時間が確実に短縮されるわけではありません。 ある特定のテストケースだけ実行時間が長いと、トータルの実行時間はそのテストケースに引っ張られてしまいます。

このXcode10から追加された並列実行の方法や注意点については、以前書いたSWETブログの記事を参考にしてください。

Xcode12における並列実行

Xcode11.4からxcodebuildコマンドを利用すると、iOS/tvOSの実機に対して並列実行を行うことができるようになりました。

これにより、iOSシミュレーター / iOS実機と並列実行をできるようになり、いろいろなパターンで自動テストを実行できるようになりました。

本機能による並列実行の注意点として、自動テストがどの端末に割り当てられるかは指定できません。 (XCTestでは実行するテスト/実行しないテストを指定できるので、どの端末にどのテストを指定するかを決めることによる並列実行もできますが、手動管理になるため大変です)

そのため、基本的には同一のデバイス・同一のOSバージョンで端末を用意しておくのが理想的です。

同じ端末を用意できずに、異なるデバイスやOSを使って自動テストの並列実行する場合は、デバイスやOSに依存するようなテストは実行しないのが望ましいです。

フィードバックからの情報取得

テストが常に成功するのであれば、テストからのフィードバックに付加的な情報はそこまで必要ないかもしれません。

しかし、テストは失敗するものです。 そのため、テストからのフィードバックで得られる情報は重要です。

フィードバックからの情報としては、次のような情報を得られることが重要になってきます。

  • どのように失敗したのか
  • なぜ失敗したのか
  • ソースコードのどこで失敗したのか

Xcode12ではテストの失敗時に上記のような情報をより分かりやすく提供してくれるようになっています。

ここでは次の3点について説明をしていきます。

  • テストの実行時間の制御(spindump)
  • アサーション
  • テスト失敗時の情報(XCTIssue)

テストの実行時間の制御(spindump)

テストの実行時間の制御によりテストが失敗した場合、どうして想定時間より長くかかったかを知る必要があります。

ハングした原因を推測することは難しいことが多いです。 Xcode12からテスト実行時間の制御によりテストが失敗した場合、テスト結果にspindumpが添付されるようになりました。

テスト結果のspindumpを開くことで、失敗したテストケース名があるはずです。 この情報をおうことで、最も多くの時間を費やしているメソッドを教えてくれます。

これにより、ハングした原因の調査の助けになります。

アサーション

テストが失敗した場合に、指定した期待する値と実際の値が異なっていたとして、それぞれの値がどのような意味を持つのかがわからないことがあります。

これがわかるようにアサーションメッセージを適切に使うことは重要です。 次のようにXCTAssertsではメッセージを設定できます。

XCTAssertEqual(expected, actual, "アサーションメッセージ")

このメッセージに適切な情報を含めておくことが重要です。 しかし、このメッセージに失敗したファイルパスを含める必要はありません。

Xcode12では失敗時の情報がより適切に表示されるようになりました。

例えば独自のアサーションメソッドを用意することがあると思います。 その場合、今までは次のようにテストケース側にアノテーションが付与されずに、実際に呼び出しているアサーションメソッド側にアノテーションが付与されます。

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

そのため、実際にどこでテストが失敗したのかがわかりづらいところがありました。 今までは、次のようにfileとlineを利用することで上記の画像の場所ではなく、テストケース側でアノテーションを表示できました。

func assertSample(file: StaticString = #file, line: UInt = #line) {
    XCTAssertTrue(false, file: file, line: line)
}

しかし、この対応でも問題は残ります。 この対応ではテストケース側にアノテーションが表示されます。 そのため、アサーションメソッド内のどのアサーションで失敗したかまではわかりません。

Xcode12ではこれらの問題が解決しています。

今回のような場合では、テストケース側にはグレイのアノテーションが表示され、アサーションメソッド側には赤いアノテーションが表示されるようになりました。

テスト失敗時の情報(XCTIssue)

Xcode12からテスト失敗時の情報が今までよりまとまっています。

今まではXCTestではテスト失敗時にrecordFailure APIを呼び出しています。 これは次にあるように4つの情報を保存しています。

func recordFailure(withDescription description: String, 
            inFile filePath: String, 
            atLine lineNumber: Int, 
            expected: Bool)

expectedはアサーションの失敗によってテストが失敗した場合はtrueで、例外の場合だとfalseになります。

Xcode12からはrecordFailureはdeprecatedになり、新しくrecord APIが追加され、このAPIが呼び出せるようになりました。

このAPIを見るとわかるように、今までのような値の渡し方ではなくXCTIssueにカプセル化されています。

そして、今までよりも複数の情報が追加されています。

これにより、自動テストを実行したXcode上や自動テストの成果物であるResult Bundleでテスト失敗時の情報がより細かく分かるようになりました。

このrecord APIはテストの失敗時に呼ばれるので、overrideしてカスタムなものを作ることもできます。

overrideできることで、情報を増やしたり絞ることもできます。 たとえば、Attachmentとしてログを別途追加するといったこともできます。

    override func record(_ issue: XCTIssue) {
        var issue = issue
        issue.add(XCTAttachment(string:  log))
        super.record(issue)
    }

Instruments

ここからは、片山がXcode12からのInstrumentsについて、業務でInstrumentsを利用している中で特に嬉しい変更について2つご紹介します。

xctraceの登場

今回Instrumentsにおいても大きな変更が入りました。 今までCLIから実行する際にはinstrumentsコマンドを用いていましたが、Xcode12でdeprecatedとなりました。 その代わりとしてxctraceコマンドが新たに追加されました。xctraceに新生したと同時に新たにできることが増えました。 そのxctraceで新たにできるようになったことで最も嬉しいと感じたのが、「Analysis Core Tables」のexportです。

Xcode11までのInstrumentsでは、計測した結果のtraceファイルを基本的にはInstruments App以外で見ることができませんでした。 そのため、計測した結果をGUIでチェックする必要がありました。 例えば端末温度を計測をした際はtraceファイルをInstrumentsで開いて、GUIを操作して問題ないかをチェックする必要があります。 (我々は、InstrumentsアプリをXCTestで動作させ、スクリーンショットやUI要素の情報を得ることで計測結果を簡易的に取得することをおこなっていました)

これらの計測結果のtraceファイルの内容をxctraceからXML形式でexportできるようになったため、exportしたXMLをパースして計測結果を機械的にチェックすることも可能になります。 毎日計測して結果を得たい場合にはとてもありがたい機能追加です。 細かい使い方についてはmanコマンドにしか詳細が無いのでぜひそちらを参照してみてください。

また、xctraceではかゆいところに手が届く変更も入りました。 instrumentsコマンドは以下のような少しだけ不便な部分がありました。

  • 選択できるtemplateの一覧をinstrumentsコマンドから見ることができない
  • 選択できる端末の一覧をinstrumentsコマンドから見ることができない

些細な問題かもしれませんが、ちょっとだけ不便なところがxctraceでは改善されました。 templateと端末の一覧をxctraceのコマンドから簡単に調べることができます。

xctraceについては当然まだベータ版であり、不具合と思われる報告もされています。 気になる方はApple Developer Forumで探してみてください。

保存 / 読み込み速度の改善

Instruments App本体でも少しうれしい改善がありました。 traceファイルは長時間計測するとサイズも大きくなっていき、保存/読み込みにかなりの時間が掛かっていました。 その問題となっていた保存/読み込みのパフォーマンスが次のように改善されました。

  • 保存時:最大40%高速化
  • 読み込み時:最大80%高速化

あくまで最大と書いてあり状況によって変化するため、私個人として試したところでは劇的に早くなったとは感じないが、少しは早くなったかなという感想です。 Resolvedの項目に記載されてるため、Appleとしても気にしていたと思われます。 今後のアップデートでも保存/読み込み速度の改善が継続的にされると嬉しいです。

おわりに

今回、WWDC2020の動画からSWET視点で選んで上述した2点について紹介しました。

WWDC2020の動画を聞いた感想として、すでにある機能が今まで以上により使いやすい形でまとめられ提供されるようになったと感じています。

また、まだXcode12がリリース前の関係で変わることもあるかと思いますし、伝えきれなかった情報もあります。 それらについては正式にリリースした時点で追加記事を書ければと思います。

参考資料

おまけ

SWETではテストに特化した勉強会としてTest Nightを定期的に開催しています。

昨今の状況もあり開催できていませんでしたが、オンラインでの開催をおこなう予定です。 それにともない、Test Nightとは別の「Test Online」というグループをconnpassで作成しています。

このグループでの勉強会を近日中にconnpassを公開するので、ぜひとも参加していただければと思います。

おまけ2

今回、Instruments周りについて紹介した理由としてパフォーマンス計測に力を入れて取り組んでいるというのがあります。

今までの取り組みについて、iOSDC Japan 2020で登壇予定ですのでぜひ視聴していただければと思います。

継続的にアプリのパフォーマンスを計測する by kariad | トーク | iOSDC Japan 2020 - fortee.jp

DroidKaigi 2020発表動画公開記念:RobolectricでUIテストを動かすのに必要なことのまとめ

こんにちは。SWETグループの外山(@sumio_tym)です。

先日、DroidKaigi 2020で発表予定だったセッション「Robolectricの限界を理解してUIテストを高速に実行しよう」 の動画がYouTubeのDroidKaigiチャンネルで公開されました。

新型コロナウイルスの影響でDroidKaigi 2020が中止になってしまったのは残念でしたが、 発表したかった内容を皆さんに伝えることができて、とても嬉しいです。

発表スライドはこちらです。

合わせてサンプルコードも公開していますので、よろしければご覧ください。

さて、本記事では「RobolectricでもUIテストを動かしてみたいけど・・・動画を見る時間がない!」という方に向けて、 ぜひ押さえておきたいポイントを厳選してお伝えします1

  • 試してみる前に知っておきたいポイント
  • テストがすぐ書ける環境を構築する
  • 工夫が必要なJetpackコンポーネント

なお「何故そうしなければならないのか」といった理由や背景についての解説は割愛しています。 その点に興味がある方は動画やスライドを参照してください。

試してみる前に知っておきたいポイント

Robolectric上でUIテストを動かそうとする前に、最低限知っておきたいポイントは次の3点です。

  • 最初はInstrumented Testで動かす
  • 動かないと分かっているのを避ける
  • ひとつの画面で完結するものから着手する

これらのポイントを事前に押さえておけば、大きな手戻りが発生するリスクを抑えられます。 「すぐに試してみたい!」という方もご一読ください。

ポイント1:最初はInstrumented Testで動かす

テストを高速に実行できるRobolectricですが、UIテスト実行における大きな弱点は「画面が無い」点です。 画面が無いため、テストコードが意図通り動作しているのか(=意図通りUIを操作しているのか)目視で確認できません。

そのため、同じテストコードをInstrumented Testでも動かせるようにしておきましょう。 Instrumented Testであれば、テストの動作状況を画面を見ながら確認できます。

特に、テストコードを書いている途中では、画面を目視しながらの動作確認は必須と言えます。 最初はInstrumented Testで動くようにテストを書き、その後にRobolectricでも動くようにしていく方法がおすすめです。 テストコードの具体的な配置方法については後で紹介します。

ポイント2:動かないと分かっているものを避ける

発表時点の調査で、Robolectricで意図通り動かないと分かっているものは次の通りです。

Robolectricで動かすUIテストでは、これらの操作は避けましょう。

ポイント3:ひとつの画面で完結するものから着手する

事前に動かない操作を知っていたとしても、テストを書き進めると意図せずそのような操作に直面してしまうことがあります。 そのリスクを避けるために、できるだけ操作するステップが少ないテストから書き始めましょう。 複数の画面をまたがるテストだと操作ステップが増えがちなので、ひとつの画面で完結するものから始めるのがおすすめです。

テストがすぐ書ける環境を構築する

事前に知っておきたいポイントを押さえたところで、テストがすぐ書ける環境を構築していきます。 既にプロダクトコードをAndroid Studioでビルドできる環境があることを前提とします。

ここで説明する手順に沿って構築すれば、次のすべてが揃った環境を入手できます。

  • IdlingResourceに対応するように筆者が改変したRobolectric
  • DataBindingの非同期処理を待ち合わせるDataBindingIdlingResource2
  • Architecture Componentのバックグラウンドスレッドを待ち合わせるTaskExecutorWithIdlingResourceRule
  • Instrumented TestとRobolectricが動作するLocal Testでテストコードを共有できるShared Test

手順1:必要なファイルをコピーする

サンプルコードをcloneし、次のディレクトリをご自身のプロジェクトにコピーします。 そのときに、コピー先も同じディレクトリ構成にしてください。 たとえばapp/src/test/java/androidxディレクトリは、 ご自身のプロジェクト側でもapp/src/test/java/androidxディレクトリとしてコピーしてください3

  • app/local-repo
  • app/src/test/resources
  • app/src/test/java/androidx
  • app/src/sharedTest/java/com/android/example/github/util
  • app/src/sharedTest/java/com/example/android/architecture/blueprints/todoapp/util

手順2:build.gradleに追記する

app/local-repoディレクトリを、Maven形式のリポジトリ参照先として追加します。 app/build.gradleに、次のように追記してください。

repositories {
    maven { url = file('local-repo') }
}

トップレベルのbuild.gradleに書くこともできます。 その場合はfile('app/local-repo')のように、local-repoディレクトリの相対パスが正しくなるように注意してください。

次に、Robolectricを使えるようにするためのandroid.testOptions.unitTests.includeAndroidResourcestrueにセットします。 app/build.gradleに、次のように追記してください

android {
    ...
    testOptions {
        unitTests.includeAndroidResources = true
        ...
    }
}

次に、Shared Testを置くapp/src/sharedTestディレクトリをInstrumented TestとLocal Test両方のソースセットに加えます。 app/build.gradleに、次のように追記してください。

android {
    ...
    sourceSets {
        androidTest {
            java.srcDirs += file('src/sharedTest/java')
        }
        test {
            java.srcDirs += file('src/sharedTest/java')
        }
    }
}

最後に、依存関係に必要なライブラリを追加します。 Robolectricはapp/local-repoのものを参照する必要があるので、バージョン表記を4.3.1-modifiedとしてください。 なお、このRobolectricはEspressoのIdlingResourceに対応するように筆者が改変したものです。詳しくはスライドの34〜57ページを参照してください。

dependencies {
    ...

    androidTestImplementation "androidx.test:core-ktx:1.2.0"
    androidTestImplementation "androidx.test.ext:junit-ktx:1.1.1"
    androidTestImplementation "androidx.test.espresso:espresso-contrib:3.2.0"
    androidTestImplementation "androidx.test.espresso.idling:idling-concurrent:3.2.0"
    androidTestImplementation "androidx.arch.core:core-testing:2.0.0"
   
    testImplementation "org.robolectric:robolectric:4.3.1-modified"
    testImplementation "androidx.test:core-ktx:1.2.0"
    testImplementation "androidx.test.ext:junit-ktx:1.1.1"
    testImplementation "androidx.test.espresso:espresso-contrib:3.2.0"
    testImplementation "androidx.test.espresso.idling:idling-concurrent:3.2.0"
    testImplementation "androidx.arch.core:core-testing:2.0.0"
}

これらのモジュールが提供する主な機能は次の通りです。

モジュール 主な提供機能
androidx.test:core-ktx Activityの起動を伴うテスト
androidx.test.ext:junit-ktx AndroidJUnit4
androidx.test.espresso:espresso-contrib Espresso
androidx.test.espresso.idling:idling-concurrent EspressoのIdling Resource
androidx.arch.core:core-testing Android Architecture Componentのテスト
org.robolectric:robolectric Robolectric

Robolectric以外のモジュールは、Local TestとInstrumented Testの両方で使うため、 androidTestImplementationtestImplementationで宣言します。 RobolectricはLocal Testだけで使いますので、testImplementationのみで宣言します。

手順3:テストクラスを用意する

テストクラスは、Instrumented Test向け・Local Test向けのものをそれぞれ用意します。 ここで紹介する内容をコピー&ペーストして、クラス名とテスト対象Activity名を置換すれば、すぐに使い始められます。

Instrumented Test向けのテストクラス

Instrumented Test向けの典型的なテストクラス定義は次の通りです。 このクラス定義をapp/src/androidTestに置いてください。

import androidx.test.espresso.IdlingRegistry
import androidx.test.ext.junit.rules.activityScenarioRule
import androidx.test.ext.junit.runners.AndroidJUnit4
import com.android.example.github.util.TaskExecutorWithIdlingResourceRule
import com.example.android.architecture.blueprints.todoapp.util.DataBindingIdlingResource
import com.example.android.architecture.blueprints.todoapp.util.monitorActivity
import org.junit.After
import org.junit.Before
import org.junit.Rule
import org.junit.Test
import org.junit.runner.RunWith

@RunWith(AndroidJUnit4::class)
class MyActivityTest {

    @get:Rule
    val activityScenarioRule = activityScenarioRule<MyActivity>()

    @get:Rule
    val taskExecutorWithIdlingResourceRule = TaskExecutorWithIdlingResourceRule()

    private val dataBindingIdlingResource = DataBindingIdlingResource() // ★

    @Before
    fun setUp() {
        val idlingRegistry = IdlingRegistry.getInstance() // ★
        dataBindingIdlingResource.monitorActivity(activityScenarioRule.scenario) // ★
        idlingRegistry.register(dataBindingIdlingResource) // ★
    }

    @After
    fun tearDown() {
        IdlingRegistry.getInstance().unregister(dataBindingIdlingResource) // ★
    }

    @Test
    fun myTest() {
        // app/src/sharedTest/java にあるテストコード共通部分を呼び出す
    }
}

これを雛形にすれば、AAC (Android Architecture Components)が使われたアプリのテストはだいたいカバーできると思います。 なお、★印を付けたdataBindingIdlingResourceに関係する処理は、Data Bindingを使っていない場合は不要です。

Local Test向けのテストクラス

次はLocal Testにおけるテストクラス定義です。 このクラス定義はapp/src/testに置いてください。

import androidx.test.espresso.IdlingRegistry
import androidx.test.ext.junit.rules.activityScenarioRule
import androidx.test.ext.junit.runners.AndroidJUnit4
import com.android.example.github.util.TaskExecutorWithIdlingResourceRule
import com.example.android.architecture.blueprints.todoapp.util.DataBindingIdlingResource
import com.example.android.architecture.blueprints.todoapp.util.monitorActivity
import org.junit.After
import org.junit.Before
import org.junit.Rule
import org.junit.Test
import org.junit.runner.RunWith
import org.robolectric.annotation.LooperMode

@RunWith(AndroidJUnit4::class)
@LooperMode(LooperMode.Mode.PAUSED)
class RobolectricMyActivityTest {

    @get:Rule
    val activityScenarioRule = activityScenarioRule<MyActivity>()

    @get:Rule
    val taskExecutorWithIdlingResourceRule = TaskExecutorWithIdlingResourceRule()

    private val dataBindingIdlingResource = DataBindingIdlingResource() // ★

    @Before
    fun setUp() {
        val idlingRegistry = IdlingRegistry.getInstance() // ★
        dataBindingIdlingResource.monitorActivity(activityScenarioRule.scenario) // ★
        idlingRegistry.register(dataBindingIdlingResource) // ★
    }

    @After
    fun tearDown() {
        IdlingRegistry.getInstance().unregister(dataBindingIdlingResource) // ★
    }

    @Test
    fun myTest() {
        // app/src/sharedTest/java にあるテストコード共通部分を呼び出す
    }
}

ほとんどInstrumented Testと同じですが、以下の点に注目してください。

  • テストクラス名がInstrumented Testのものと違う
    現状では、app/src/androidTestapp/src/testで同じ名前のクラスを定義するとAndroid Studio上でエラーになってしまいます(バージョン3.6.3で確認)。 エラーを無視してビルドはできるものの、IDE上でエラーのままコードを書いていくのは苦痛です。 テストクラス名は別の名前にすることを推奨します。
  • @LooperModeアノテーションが付いている
    Robolectricのタスクスケジューラの種類をPAUSEDにしています。 詳しく知りたい方はスライドの22〜26ページを参照してください。

こちらも、★印を付けたdataBindingIdlingResourceに関係する処理は、Data Bindingを使っていない場合は不要です。

手順4:Instrumented Test・Local Test両方から呼びだせるようにテストを書く

手順3で作成したテストクラスにおける、テストの種類とテスト実行時に呼び出されるテストメソッドの関係は次のようになります。

テストの種類 テスト実行時に呼び出されるテストメソッド
Instrumented Test MyActivityTestクラスのmyTestメソッド
Local Test RobolectricMyActivityTestクラスのmyTestメソッド

これら2つのmyTestメソッドに同じテストコードを書けば、両者から同じテストを実行できるようになります。 とはいえ、両方のメソッドに同じコードを書くとコードが重複しメンテナンス性の低下を招きます。 その事態を避けるために、テストコード本体はapp/src/sharedTestに配置し、 myTestメソッドからはテストコード本体を呼び出すだけにします。

例えば、app/src/sharedTestに配置したテストコード本体をdoMyTest()関数としましょう。

// app/src/sharedTestに配置する
fun doMyTest() {
    Espresso.onView(...).perform(click())
    Espresso.onView(...).check(isDisplayed())
    ...
}    

その場合2つのmyTestメソッドでは、コード重複をできるだけ抑えるためにdoMyTest()を呼び出すだけとします。

// app/src/androidTestに配置する
...
class MyActivityTest {
    ...
    @Test
    fun myTest() {
        doMyTest()
    }
}    
// app/src/testに配置する
...
class RobolectricMyActivityTest {
    ...
    @Test
    fun myTest() {
        doMyTest()
    }
}    

この例におけるdoMyTest()部分の設計パターンはPage Objectデザインパターンがおすすめです。 Page Objectデザインパターンの詳細については割愛しますが、本パターンを適用するとmyTestメソッドの本体は次のような感じになります。

fun myTest() {
    MyGardenPage
            .goPlantList()
            .showPlantDetail("Mango")
            .addToMyGarden()
            .goBackPlantList()
            .goMyGarden()
            .assertPlanted("Mango")
}

スッキリ見通しが良くなりますね。

Page Objectについて詳しく知りたい方は、 DeNA CodelabsでSWETが公開している 「Espressoの知識ゼロでも書ける!Android UIテストはじめの一歩」に挑戦してみてください。

補足:テストクラスも共通化する方法

ここで紹介した方法ではmyTestメソッド内のコード重複は避けられません。

その重複も回避したい場合、本記事で紹介した範囲であれば2つのテストクラスを共通化することもできます。

その場合はLocal Test向けのテストクラスだけをapp/src/sharedTestに置きます。 app/src/androidTestapp/src/testには対応するテストクラスは置かないでください。

そして、app/build.gradleにInstrumented Testの依存関係としてorg.robolectric:annotationsを追加します。

dependencies {
    ...
    androidTestImplementation "org.robolectric:annotations:4.3.1"
}

Robolectricのアノテーションの違いだけであれば、この方法でテストクラスを共通化できます。 ただし、筆者個人の意見としては、あまりこの方法はおすすめしません。 おすすめしない理由は、両者のテスト間で完全に同じコードを維持できない可能性が高いと考えるからです。

たとえば、RobolectricのShadowクラスを使いたくなる場合など、どうしても共通化できない部分がでてきたとします。 そうなった場合、共通化できない部分をapp/src/androidTestapp/src/testへ切り出すことになります。

// app/src/sharedTestに配置したコード
@Test
fun myTest() {
  ...
  doActionOnlyLocalTest() // Local Testでしか実行したくない処理
}

// app/src/testに配置したコード
fun doActionOnlyLocalTest() {
  // ここにLocal Testでしか実行したくない処理を書く
}

// app/src/androidTestに配置したコード
fun doActionOnlyLocalTest() {
  // 何も書かない
}

ところがこの方法を取ってしまうと、前述した 「app/src/androidTestapp/src/testで同じ名前のクラスを定義するとAndroid Studioでエラーになる」 というAndroid Studioの振舞いに抵触してしまいます。 エラーを無視してビルドはできるものの、現状ではおすすめするのが難しいです。

将来Android Studioの振舞いが改善されたら、この方法がベストな選択肢になると思います4

工夫が必要なJetpackコンポーネント

Jetpack Componentのうち、RoomWorkManagerでは更なる対応が必要です。 その対応方法を説明します。

Room

Roomを使うアプリのうち、RoomDatabase(のサブクラス)への参照をstaticなフィールド(Kotlinのcompanion objectなどを含む)に保持しているケースが問題になります。 問題となる理由は、Robolectricの次のような振舞いと相性が良くないからです。

  • テストごとに(ひとつのテストメソッド実行の度に)SQLiteのデータベースファイルが新規に作られる
  • テストをまたいでもstaticな変数は初期化されない

RoomDatabaseのインスタンスは、データベースファイルと一対一対応しているため、 データベースファイルが作り直されたときは改めてインスタンスを作り直す必要があります。 また、RoomDatabaseのインスタンスが変わるとDAOのインスタンスも変わってしまう点にも注意が必要です。

そのため、そのようなアプリをRobolectricでテストするときは、テストのセットアップ時に次の処理を行うようにしましょう。

  1. RoomクラスのdatabaseBuilderメソッドを使って、RoomDatabaseインスタンスを作り直す
  2. アプリ内で保持している古いRoomDatabaseへの参照を、作り直したインスタンスへの参照に更新する
  3. 同様に古いDAOインスタンスへの参照を、新しいRoomDatabaseから取得し直したDAOインスタンスへの参照に更新する

RoomDatabaseの初期化をアプリケーションクラスで行っている場合は、Robolectric用に別のアプリケーションクラスを用意するのが簡単です。 Robolectricではテストクラスに次のようなアノテーションを指定できます。

@Config(application = TestApplication::class)
class RobolectricMyActivityTest { ... }

これで、Robolectricはこのアノテーションで指定されたアプリケーションクラスを使って初期化するようになります。 この例ではTestApplicationクラスのonCreateメソッドが呼び出されるようになりますので、 そのonCreateメソッドの中でRoomDatabaseインスタンスを作り直すなどの処理をすると良いでしょう。 なお、Robolectricではアプリケーションクラスの初期化もテストごとに行われます。

テスト対象アプリによって事情が異なるため具体的なコード例は割愛しますが、 Android Sunflowerアプリの修正例をスライド70〜75ページに掲載していますので、あわせて参考にしてください。

WorkManager

WorkManagerのデフォルトの振舞いでは、未完了のWorkはアプリが終了しても消えることがありません。 次回アプリ起動時に再開されます。

そのようなWorkの特徴により、前回のテストで未完了だったWorkが次のテストで意図せず起動することがあります。 その事態を回避するためにはWorkManagerTestInitHelperを使います。具体的な手順を見ていきます。

まず、app/build.gradleにLocal Testの依存関係としてandroidx.work:work-testingを追加します。

dependencies {
    ...
    testImplementation "androidx.work:work-testing:2.3.1"
}

次に、app/src/test/AndroidManifest.xmlを次の内容で作成します。

<manifest xmlns:android="http://schemas.android.com/apk/res/android"
    xmlns:tools="http://schemas.android.com/tools">

    <application>
        <provider
            android:name="androidx.work.impl.WorkManagerInitializer"
            android:authorities="${applicationId}.workmanager-init"
            tools:node="remove" />
    </application>

</manifest>

既にファイルが存在する場合は<provider>部分を<application>タグの中に追記してください。

最後に、テストのセットアップフェーズで、次のようにWorkManagerを初期化します。 Roomのケースと同様にテスト用アプリケーションクラスのonCreateメソッドで初期化するのが良いと思います。

class TestApplication : Application() {
    override fun onCreate() {
        ...
        WorkManagerTestInitHelper.initializeTestWorkManager(this)
        ...
    }
}    

テスト用アプリケーションクラスを用意する場合は、忘れずにテストクラス側でアプリケーションクラスを指定するようにしましょう。

@Config(application = TestApplication::class)
class RobolectricMyActivityTest { ... }

この対応で、未完了だったWorkが起動することはなくなります。 また、起動したWorkが同期的に実行されるようにもなるので、UIテストの安定化に寄与するはずです。

おわりに

RobolectricでUIテストを動かすときのポイントを紹介しました。 これらを実践すれば、UIテストの大部分がRobolectricでも動作するようになっていることと思います。

是非、簡単なところから少しずつ書きはじめてみてみてください!


  1. この文脈における「UIテスト」は、EspressoのAPIを使ったテストとします

  2. このコードは孫FragmentにDataBindingが使われているケースをサポートしていませんでした。サンプルコードではその問題を修正しています

  3. 特にapp/src/test/java/androidx配下のクラスは、パッケージ名を変更すると動かなくなりますので注意してください。app/src/sharedTest配下のクラスについては、パッケージ名を変更した上で別のディレクトリに配置しても問題ありません

  4. 途中から違う事象について議論しているので確証はありませんが、Issue 140375151が関連するバグチケットのようです

ゼロから学んだ形式手法

2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek(@takasek)です。

仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています(形式手法 カテゴリーの記事一覧)。

この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。

形式手法を学ぶ前の認識と疑問

ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造(モデル)を与え、そのモデルを解決の機構に落とし込む行為といえます。 その興味の延長線上で、よりアカデミックな裏付けのあるアプローチが取れると聞いて興味を持って形式手法を学び始めた私ですが、形式手法の概要を知った段階での認識・疑問は次のようなものでした。

f:id:swet-blog:20200407164509j:plain

そもそも「形式」「形式手法」の正体が掴めていない

形式手法というのはテストよりも抽象的に、網羅的に問題を発見できるらしい。

なるほど、たしかにテストの7原則によれば「テストは欠陥があることは示せるが、欠陥がないことは示せない」。その弱点をカバーできるとしたら形式手法はすごい。ただ理屈がよくわからない。書かれていないものは書かれていないのだから見つけようがないのでは?

形式手法は数理論理学に基づいているという説明もある。わからない。普段のプログラムだってif文を書くぞ。何が違うんだ。形式化されているのが違う? なるほど……なるほど? そもそも形式化って何だ? プログラムのコードは機械が読むためのものだが、それは形式化じゃないのか? やっぱりわからない。普通のプログラミングと形式手法を隔てるものは何なんだ?

形式手法の分野の違いがわからず混乱する

形式手法の分野には主に「形式仕様記述」「モデル検査」「形式検証(定理証明)」があるらしい。

しかし字面から違いがよくわからない。形式仕様記述は記述するだけで検査や検証をしないのか? 仕様とモデルの違いは? 検査と証明・検証の違いは? 混乱する。しかも各分野の中にもツールがたくさんあるようだ。なんでそんなにたくさんあるんだ。統一してほしい。

数学をちゃんと学ぶ必要があるらしいが、本当か?

そりゃ何事も学ぶほうがいいのはわかる。たとえば仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blogには以下のような記述が登場する。

\exists LocalVariables. \exists LocalVariables'. PredLocal \land PredPromote

存在量化子というやつだ。なるほど。こういう概念が登場したときに数式が理解できないとたしかに困りそうだ。でも、そういうテクニックだけをピンポイントに使う形でカバーできないのだろうか?

これまで触れてきたプログラム言語の型付けでも、存在型(existential)や全称型(generics)が登場する。基礎から理論を理解できるならもちろん良いが、とりあえず表面だけでもなんとかごまかしごまかし使うことができている。

形式手法も実はごまかしでいける部分が存在するのでは? 要求レベルを上げていったらきりがないじゃないか。「学ばないと太刀打ちできない」というような言い回しは不当にハードルを上げているだけでは? それとも形式手法の場合には決定的に「数学を学ばないと太刀打ちできない」ような事情があるのだろうか?

実際どこまで役に立つのだろうか

正直、知的好奇心に駆られて転職しちゃったところがあり、実際にプロダクト開発の現場で汎用的に適用できるイメージは具体的に湧いていない。

「形式手法の実践ポータル」に事例がまとめられているが、大層なプロジェクトばかりだ。現状、普通の開発現場で形式手法が流行っている様子はない。ということは、適用範囲がけっこう限られるのでは? どれくらい汎用性のある技術なんだろうか?

今の理解

f:id:swet-blog:20200407164516j:plain

このような疑問を持ちながら3か月の学習と実践を重ねていった結果、現在は以下のような理解に辿り着きました。

「形式」は証明のためのスタートライン

私の当初の「プログラムのコードだって形式化されているのでは?」という疑問は正解です。普段プログラマが使うプログラム言語は形式言語です。利用可能な文字集合、文法のルールが規定されており、曖昧な構文を許さない言語です。

形式手法と普段のプログラムと違う点は数理論理学に基づく点だと言われます。だから網羅性があり、テストでは発見できないような欠陥も発見できる。……よくわかりませんね。何が違うのでしょうか。

実は誰でも同様のアイデアを昔習ったことがあるはずです。私も中学数学の復習をしたら分かりました。証明です。

三平方の定理を考えてみましょう。a,bの二辺と長さcの斜辺からなる直角三角形においてa2+b2=c2が成り立つという定理です。

f:id:swet-blog:20200407164522j:plain

この結果を確認したいとき、プログラマが慣れているユニットテストでは具体的なケースを列挙するしかありません。 {a:3, b:4, c:5} のとき成り立つ、 {a:5, b:12, c:13} のとき成り立つ……といったように。Property Based Testingであれば大量のランダムな入力を与えることも可能ですが、どこまでいっても有限個の試行の繰り返しです。

しかし証明なら、個別のケースではなく任意の無限の直角三角形について定理が成り立つことを示せます。中学数学の証明では、直角三角形の図に補助線を引くなどの作業を通じて、すでに明らかな定義を変形させて定理を導きました。

中高の数学の範囲を離れると、次のように言えます。無条件に正しいと見なせる命題を公理といいます。公理に繰り返し推論規則を適用していくと定理を導出できます。その論理の筋道をつけるのが証明です。

形式手法の話に戻ります。形式手法とは「このシステムは正しい」と言えるようにするための手法です1。言い換えると、命題「このシステムは正しい」を証明するのが形式手法のゴールです。そして数学的な意味で証明可能にするためには、漠然とした「正しい」を数理論理学の世界に持ち込まなくてはなりません。

自然言語で書かれたシステムの仕様には曖昧さがあり、機械的な推論規則の適用もできません。それでは証明などできません。形式言語を使って論理式として仕様を表現することが、形式手法のスタートラインです。

形式手法の分野は多岐にわたり、また横断的である

システムの正しさを証明するのが形式手法のゴールだと述べました。形式手法の分野の違いは、その筋道のつけかたの違いです。

形式手法の多くは次のような二側面を持ちます。

  • システムのある性質を表現する仕様を形式的に記述し、
  • なんらかのツールを通じて検査・検証にかけ、結果を出力する

この前者および後者のバリエーションがさまざまな形式手法の違いです。

まず対象のシステムとは何かを考えてみましょう。システムと一言で言っても、入力と出力が1対1で対応するシステムと、異常がない限り動き続けてイベントを待ち受けるシステムは別物です。複雑な内部状態と条件分岐を持つゲームも、独立動作し協調しあう分散システムも「システム」です。

システムの中でも、検証すべき性質はひとつではありません。性質に応じて出力の形は変わります。

  • 仕様を詳細な設計に落としたとき、不正な挙動が混入していないことを確認したい
  • システムを構成する複数のコンポーネントの関係について、可能なパターンをグラフィカルに図示したい
  • 具体的なシナリオに沿って、状態遷移をシミュレーションしたい
  • 並行システムの挙動を合成して、不具合が起こりうるケースを網羅的に検知したい
  • 複雑な証明の途中式を自動的に補完しながら巨大な証明を完成させたい

こういった異なる目的を、同一の手法・ツールでは達成できません。

形式化のベースとなる論理体系も一様ではありません。たとえばアルゴリズムが仕様を満たしていることを検証したければ、その事前条件・事後条件をHoare論理を使って記述します。システムの長いライフサイクルにおける性質を検査したいときには「いずれtrueになることがある」「常にtrueのまま」といった時相論理を使った表現を使うこともできます。他にも検証したい性質に応じて、門外漢には想像もつかないほど多様な論理体系が存在するようです。

ただし強力な表現ができるほどよいというわけではありません。必要十分な表現力があればよいのです。記述の自由度と解析の簡単さはトレードオフです。無用に記述が複雑すぎると理解しづらくなり、仕様記述に矛盾や不整合がないことの検証(verification)のみならず「その仕様は本当に問題の解決の形として妥当か」の確認(validation)に支障が出ます。またシステムの全状態をモデルとして表現して網羅探索するモデル検査では、詳細すぎるモデルは状態爆発により現実的な時間内での検査が難しくなります。重要なのは適切な抽象度での仕様記述・モデリングです。時には表現力を制限し簡単な記述を可能にしたDSL(ドメイン特化言語)が有効な解決策になります。

ソフトウェア工学の道具としての形式手法では、形式手法とは何かという問いに、次のような説明で答えています。

数理論理学に基づく言語ならびに証明技法などからなる基礎理論を持つことに加えて、設計手法、ドメイン知識、などが関係する総合的な技術2

形式手法と一言で言おうとしても輪郭が掴みづらいのは、そういった総合的な側面が影響しているのでしょう。

先述したとおり形式手法には「形式仕様記述」「モデル検査」「形式検証」があると言われますが、3つの分野を排他的なものとして考えると混乱します。モデル検査であろうと形式検証であろうと仕様記述は必要です。たとえば代表的な形式検証のツール(定理証明系)であるCoqの記述言語Gallinaも、明確に「仕様記述言語」だと説明されています3

今私たちが取り組んでいるプロジェクトでも、目的までのロードマップには3分野いずれの技術も必要になっており、いくつもの手法を組み合わせて活用しています。何かひとつのツールを触って理解した気になるのではなく、問題に対して適切な抽象度とツールを選ぶために見識を広げていかなければならないと思います。

形式手法にとって数学は基礎的な語彙である

形式手法のツールには、難しい理論を知らずとも扱えるようにデザインされているものもあります。たとえば当ブログのDeNA TechCon 2020の発表についての記事で述べたように、仕様分析サポートチームでは当初「視覚的なフィードバックを得られるので初学者に易しい」という理由でAlloyを採用しました。ツール上でフィードバックを得ながら試行錯誤していたらなんかうまいこと目的達成できた、という体験も悪くはないでしょう。

しかし形式手法に正面切って向き合うなら、表層だけ撫でる態度はむしろ効率を損ないます。先に述べたように、あるシステムの仕様を適切に記述し性質を検証・検査可能にするためには、どのみち形式仕様記述を避けて通れません。モデル検査は「ボタン一発の検証法4」とは呼ばれますが、そのモデリングのためには抽象化技術が必要ですし、検査結果を読むにあたっても論理学の理解がないとしばしば誤った解釈をしてしまうそうです。数理論理学は形式手法での読み書きを支える基礎的な語彙となります。

そして論理学は、概念の積み上げで成立しています。注意深く足を進めないとすぐ転んでしまいます。例をいくつかご覧に入れましょう。

述語という単語を耳にしたとき、論理学の素養がない人は「主語でない文節」と理解することが多いでしょう。すると論理学での「変数を含み、変数に具体的な値を代入することによって真偽が定まる叙述5」という理解ができなくなります。

当記事でも何度も言及している性質は、数理論理学の世界では「変数が1つの述語」です。あなたのイメージと合致していたでしょうか? この理解は普段の日本語やオブジェクト指向に慣れ親しんだプログラマからは距離があります。

ときには普段のプログラミングでの考え方が邪魔をすることすらあります。形式仕様記述にもいくつかのアプローチがありますが、私が現在取り組んでいる仕様記述は状態に注目するモデル規範と呼ばれる方法なので、その話をしましょう。

ここで状態というのは「局所状態の掛け合わせとして立ち現れた、システム全体のグローバルな状態」です。プログラマは普段、グローバルな状態は悪だと考えているものです。なるべく状態を局所に留め、モジュール内の状態は隠蔽するよう、半ば教条主義的に訓練されています。なのでグローバルな状態という存在を受け入れるには、私にとってはかなりの発想の転換が必要でした。

モデル規範の形式仕様記述では、すべての状態の集合から特定の状態を取り上げ、状態どうしの関係を記述することになります。この手順を飲み込むまでにも時間を要しました。普段プログラマは多かれ少なかれパフォーマンスを気にしながらコードを書いています。もし集合(Set)に数万の要素が入ると言われたら、ぎょっとしてアルゴリズムを考え直すことが多いでしょう。グローバルな状態の集合は、天文学的な要素数をものともしません6。そういうものを扱う数学的な発想に、私は最初大きく戸惑いました。

「すべての状態」があらかじめ存在しているという前提を受け入れると、パラダイムが大きく変わります。事前状態・事後状態の関係は pred hoge(s, s') のように記述します7。日頃プログラマとして慣らされているような「事前状態を具体的な引数として受け取り、加工して事後状態を返す」関数ではなく、時間経過を伴わない静的な記述だというのがポイントです8

このように形式手法を学ぶ中ではしばしば、日常用語と異なっていたり、これまでのプログラミングの延長で捉えられない概念に遭遇します。既存の枠組みに引き寄せて歪んだ理解に辿り着かないよう、注意深くならなければいけません。

定評のある数学の教科書はどれも、まず単純な定義から始め、定義済みの確かなものを積み上げると新たな概念が獲得されるように書かれています。私のような現場でのアドホックな学習で育ってきた人間は、基礎を積み上げていくアカデミックな手続きをおろそかにしがちです。最初から数学やってる人には丁寧な手続きが常識なのかもしれませんが、少なくとも私はそういう足腰が弱ってることを自覚しないとすべてが始まりませんでした。

問題を分割統治するのはプログラミングでも散々やってきたはずだし、場合分けして分割統治、各個撃破というのは中学高校の証明で習ってるはずなのに、大人になると忘れちゃうし身についてないんですよね。不思議ですね。

形式手法は役に立つ!

かつて形式手法は、システムのすべての性質を壮大な論理体系で表現し、厳密な仕様がそのまま動くプログラムへと詳細化される世界(Correctness by Construction)を夢見ていました。しかしそれは壮大すぎて難しく、今世紀に入ってからは実用性を意識する Formal method Light が主流となったそうです9

プログラマが日常的に頼っている型システムも「型システム入門」によれば「最も確立された軽量形式手法」10です。当初の私の認識「普通の開発現場で形式手法が流行っている様子はない」なんてとんでもない勘違いでした。もう当たり前のように、形式手法はソフトウェアエンジニアリングの世界に溶け込んでいるのでした。

デザイン電卓として

かつてモバイルアプリエンジニアとして携わった案件でも、今と同様の知識があれば形式手法の実践を検討しただろうと思える局面が何度かあります。

私があるとき設計・実装したのは、端末のオンメモリ・サーバ通信・永続化層・さらにアプリバージョンのアップデートといった複数の状態が非同期に絡み合う複雑な機能でした。人数と時間をかけて何度も仕様をチェックし設計しましたが、やはり多くの細かいミスが出ました。テストを書いても「本当にこれですべて確認できるのか」「テスト自体が間違っているのでは」という不安がつきまとい、実際その不安は大いに的中しました。転ばぬ先の杖として不正なデータを差し戻す処理を随所に入れたりもしましたが、本当にそれが必要なガードだったのか、もしくは無用に仕様を複雑にしただけなのかは今でも分かりません。

今の自分が当時に戻ったら、この案件に限って形式仕様記述してモデル検査にかけよう! と提案することでしょう。モデルが正しく振る舞うことを早期に検査できれば安心して開発を進めることができます。目的を絞ればそこまでの導入コストはかからず、十分ペイするはずです。

このように、大がかりにではなくアドホックな形で形式手法を用いるアプローチは「デザイン電卓」と形容されるそうです11。形式手法に対しての大仰なイメージを払拭してくれる素敵な表現だと思います。

f:id:swet-blog:20200407164529j:plain

仕様の妥当性確認として

メリットは、ツールによる正当性(correctness)の検査(verification)だけではありません。形式的に仕様記述すること自体が「その仕様は本当に問題の解決の形として妥当か」の確認(validation)となります。

普段のソフトウェア開発業務で仕様書を読み書きするとき、条件の不明瞭さや期待結果の曖昧さ、項目どうしのつながりに不安を覚えることはないでしょうか。私はありました。自然言語の表現力に絶望して、おもむろに擬似コードを書き始めることもありました。頭の中ではなんとなくうまくいきそうなのに、条件の漏れやブレによって適切な仕様化に失敗することはよくあります。そんなとき、形式言語は仕様の妥当性を厳密に確認するための、まさに言語として役立ちます。

先日のDeNA TechConでの発表では、この側面について詳細に解説しています。予備知識がなくともわかりやすい発表になっていますので、是非あわせてご覧ください。

DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました(録画・スライドあり) - DeNA Testing Blog

より積極的な適用として

ソフトウェア開発のプロセスは、ある入力を別の形へと変換して出力する作業の繰り返しといえます。変換の中で混入した誤りが、後で致命的なバグに成長します。形式手法を活用すれば、そんなときに前後の入出力、あるいは別の変換を経た複数の成果物が同じ意味だと保証できるのです。これは非常に汎用的かつ強力なアイデアです。一度習得した技術が開発プロセスの至る所で使えるというのは、夢が広がりますよね。

私たち仕様分析サポートチームはそのような考えのもと、積極的に形式手法の活用局面を探っています。

おまけの副産物

形式手法の土台には多くの数学的背景が横たわっています。これはコンピュータサイエンスの土台でもあります。つまり形式手法を学べば必然的に、プログラミングの深い理解にも繋がります。

たとえば契約による設計は「オブジェクト指向入門」12でバートランド・メイヤーが唱えた概念ですが、その由来がHoare論理にあるのだと理解できました。

また、私はSwiftコンパイラ好きが集まるわいわいswiftc - connpassというイベントが好きでよく顔を出しています。そこでは発表のたびに「SwiftコードのコンパイルにはAST→Sema→IR→…というフェーズがあって」という説明が頻出します。この説明も「単にそういう手続きだ」というだけでなく「統語論と意味論を分けているのだな」と理論上の納得を得られるようになりました。

いろいろな技術領域を闇雲につまみ食いしていた私にとっては、バラバラだった知識に連続性がもたらされ、とても良い学びの機会となっています。

まとめ

人間はいい加減な存在です。自然言語の世界はなんとなく動いているように見えても、あちこちに誤魔化しや綻びがあります。たとえば「または」が排他的選言両立的選言のどちらを示すかは文脈によるとか、「1日おき」の意味が曖昧だとか。でも我々は意識しないと曖昧さに気づけないものです。そんなあやふやな論理を扱う人間だから、一度日常の世界を離れて数理論理学の力を借りる必要があります。

形式手法は強力で信頼できる論理体系に支えられており、それでいて多種多様です。場合によっては親しみやすくもあり、思ったよりも汎用的な技術領域に感じられます。

そんな形式手法についての、今時点での理解について書き連ねてみました。私と同じように形式手法に対しての疑問を感じていた方への道しるべになれば幸いです。

今後もSWETでは形式手法の実用性を見極める研究を続け、アウトプットしていきます。よろしくお願いします。


  1. 「ソフトウェア工学の道具としての形式手法」 p2 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf

  2. 「ソフトウェア工学の道具としての形式手法」 p2 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf

  3. The Gallina specification language — Coq 8.11.0 documentation https://coq.inria.fr/refman/language/gallina-specification-language.html

  4. 「ソフトウェア工学の道具としての形式手法」 p12 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf

  5. 「ソフトウェア科学基礎」p12 https://www.amazon.co.jp/dp/4764903555

  6. 記述上無限を扱えるという話であって、網羅的にパスを辿るモデル検査時にはパフォーマンス考慮が必要なことはあります。

  7. 具体的な記述の感触を掴みたい方は、仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blogもご参照ください。

  8. 条件によっては「事前状態を引数として受け取り、加工して事後状態を返す」書き方に変換可能なことはあります。

  9. 「ソフトウェア工学の道具としての形式手法」 p4 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf

  10. 「型システム入門」p1 https://www.amazon.co.jp/dp/B07CBB69SS

  11. 「ソフトウェア工学の道具としての形式手法」 p13 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf

  12. 「オブジェクト指向入門 第2版 原則・コンセプト」 11章 https://www.amazon.co.jp/dp/4798111112

DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました(録画・スライドあり)

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

コロナウィルスの影響で当初予定していた2020年3月4日(水)のDeNA TechCon 2020は中止になってしまいましたが、「せっかく資料も作ったしどうしてもDeNAのチャレンジを紹介したいんだ!」ということで、先週2020年3月12日(木)に一部のセッションをライブ配信しました。

タイトルにもある通り、私もゲームの仕様に関するテーマでライブ発表をしましたが、本記事はそのフォローアップということで、スライド資料の補足情報といただいた質問への回答を記載します。

発表内容

タイトル

仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ

f:id:swet-blog:20200317150044p:plain:w120

セッション情報

https://techcon.dena.com/2020/session/10

資料

動画

https://youtu.be/eKU5HOAtJsw?t=498

登壇者

今回は2名での発表でした。

  • 鈴木穂高(@hoddy3190
    • スライドの1章から4章を説明
  • Kuniwakこと国分佑樹(@orga_chem
    • スライドの5章とまとめを説明

それぞれのプロフィールは、DeNA TechCon 2020のセッション情報ページをご覧ください。

各章の意図

章立てはスライドp4に記載しています。

2章「アプリゲーム運用の現場」では、アプリゲーム運用の現場ではどのような問題がどのような背景で起こるのか説明しています。 その後の3章「我々のチャレンジ」では、それを踏まえた上で問題解決に向けた我々のチャレンジを説明しています。 4章「形式仕様記述の紹介」・5章「具体例」では、チャレンジの技術的な手段として形式仕様記述の紹介をしています。

今回はアプリゲーム運用の現場の説明や、形式仕様記述をやろうと思った背景の説明に、40分の発表のうち約半分の時間を費やしました。2章から3章、4章の一部が該当します。 なぜそこまでの時間を費やしたのか。それは2019年8月末に行われたbuilderscon tokyo 2019の時も今回と似たような構成で発表したのですが、そのときの反省点からです。 builderscon tokyo 2019での発表の反応(togetter)も決して悪くはなかったとは思っていますが、中には形式仕様記述の必要性について疑問がぬぐえなかった方もおられたようです。builderscon tokyo 2019のときは発表時間が20分しかなかったことも大きいですが、形式仕様記述を試用するに至った背景を十分に説明しきれていなかった、というのが大きな反省点としてありました。解決したい問題があって初めて使う技術を選択できると思うので、形式仕様記述を試用するまでに至ったそのプロセスの共有はとても大事だろうということで厚く時間を割きました。

5章では具体例を用いてAlloyで形式仕様記述をどのように行うのかを説明しています。初めての方でもなるべく理解できるようにというのを前提に作りました。 ただAlloyは書き方、考え方が手続き型のプログラミングとは異なるので、多くの人にとって初見で理解するのは難しいということは承知していました。 なので、この章のメインテーマを「Alloyの書き方」ではなく、「いかに仕様の漏れを形式仕様記述で埋めていくか」にしました。 一方で形式仕様記述をやったことがある人にとっては面白みのないものになる懸念があったので、先んじて形式仕様記述のテクニックを紹介するブログ記事を公開し、発表内でそのリンクを紹介する形をとりました。

今回の発表に対するTwitter上の反応をtogetterにまとめました。肌感としては、builderscon tokyo 2019のときと比べ、「わかりやすかった」という反応が増えたように思います。暗黙知をできる限り潰し、伝えたいことを解釈の幅をおさえて伝えるということが前よりはできたのかもしれません。

質問・回答

本発表への質問とそれに対する回答です。ライブ中に答えた質問も含め、Twitterや社内Slackなどで目に入った質問はすべて取り上げています。 なお質問の文言は、意味がなるべく変わらないように整えた上で掲載しています。 本記事とライブ配信で回答内容に齟齬がある場合は、本記事を正とさせてください。

Twitterでの質問

こちらはスライドp46「無用な大規模化や無用な複雑化は避けるべきと考える」対する質問かと思われます。 おっしゃるとおり無用かどうかを事前に見極めるのは難しいだろうと考えています。 補足スライド内の記述ということもあり、この文言の意図としては「要求を満たす仕様の中で、もっと単純な選択もあるのにわざわざ複雑になるような仕様を選んでしまう必要はない」くらいのニュアンスで書いていました。 仕様にまつわる問題は、今回我々の取り上げた「仕様が書かれない問題」以外にも様々あることがわかっています。 本当に必要な仕様なのかどうかの結論づけをいかに行うかというのもそのひとつだと思います。 ただ残念ながら現時点で我々もこうすれば良いだろうという具体的な案を持ち合わせているわけではないです。

有向です。

こちらおそらくInitial Commitの説明の前に発言されたものかと思われます。 仕様作成者がInitial Commitの仕様に気づけておらず仕様書に明文化されていなかったが、Alloyで形式仕様記述をする過程を経てその仕様に気づけるという例をお見せしました。

仕様分析サポートチーム以外にどのような形で共有するかは現在検討中です。

おっしゃる通り、その問題は起きえます。 Alloyの場合は、小スコープ仮説(モデルの不具合のほとんどは小さい例で示せる)に基づき代表的な状態のみに絞って検査をしています。 また我々が考えている対策案としては、形式的に記述した仕様を定理証明ツールで使えるような形に変換することを考えています。

Alloyにはそういうexport機能はありませんが、export機能があるツールはいくつかありまして、例えばVDMToolsにはC++やJavaに変換する機能があるようです。

我々が初めて形式仕様記述したプロダクトはOyakataです。

当時は形式仕様記述がどのようなものなのかぼんやりとしたイメージしか持っていなかったので、Oyakataの仕様を形式記述する動機は「Oyakataに貢献する」よりも「技術を知る」の方が大きかったです(cf. builderscon tokyo 2019「形式手法を使って、発見しにくいバグを一網打尽にしよう」p33)。 VDM++、Event-Bなど調べましたが、視覚的なフィードバックの得られるAlloyが初学者にとって易しそうだという理由でこの時はAlloyを選びました。

ちなみに、スライドp88に、「現在はOyakataの形式仕様記述を終えアプリゲームに適用している」旨を書いていますが、アプリゲームの仕様記述にはAlloyを用いていません。Oyakataへの形式仕様記述を通して、Alloyのメリット・デメリットがある程度把握できた上での判断です。こちらに関してはまたいつかお話できればと思っています。

社内からの質問

アプリゲーム以外でも形式手法による開発効率アップは見込めるでしょうか?

はい、見込めます。というのも、形式手法を適用してバグの件数が大きく減ったという事例は欧米を中心に多く報告されていた(航空宇宙、鉄道、電力など高い信頼性が必要とされる分野での事例が多い)ので、それをアプリゲーム運用にうまく適用できないだろうかと考えました。 事例は形式手法の実践ポータルがよくまとまっていると思います。

形式手法のコスパ見極めはいつ完了しそうな見込みでしょうか?

アプリゲームには2019年の11月から適用をしていますが、1年以上はかかると思います。

仕様分析サポートチームは現在何人ですか?

4人(うちフルコミットは2人、あとの2人は兼業)です。4人で1つのプロダクトに形式仕様記述を適用しています。 ネットや書籍に情報が少なく、手探りなことが多いので、モブプロを活用しながら取り組んでいます。

昨年のDeNA TechCon 2019とのつながり

昨年のDeNA TechCon 2019でKuniwakが発表した「ある SWET エンジニアの開発プロセス改善最前線 / Story of a SWET Engineer」でも形式手法、形式仕様記述を用いた取り組みについて発表しました。 この時期は色々と種類がある形式手法の中でもモデル検査について調査していました(詳しくは、「ある SWET エンジニアの開発プロセス改善最前線 / Story of a SWET Engineer」のp87以降をご参照ください)。 しかし会社の課題は何なのか、適切なアプローチは何なのかを改めて整理すると、形式仕様記述の方が適切そうだという結論になり方針転換をしました。 そうした紆余曲折を経ながらも、現在ではOyakataをはじめ様々なプロダクトに適用するまでに至り、可能性を見極めています。 まだまだ先は長いですが、これからも継続してチャレンジしていきます。

さいごに

DeNA TechCon 2020のテーマは「Craftmanship」です。 問題解決のために私たちが技術を徹底的に磨きチャレンジを続けてきた様子を、会場にて直接皆様の前でお伝えできずに残念でしたが、 これからも定期的にSWET Blog等を通じて発信していきますのでよろしければご覧ください。

また、DeNA TechConをはじめ、DeNAエンジニアの登壇お知らせや彼らが書いたブログ記事等の紹介をTwitterアカウント(@DeNAxTech)にてお届けしています。ぜひフォローをお願いします!