모델 체킹(Model checking)

모델 체킹(Model checking)

모델 체킹 전략으로 코드를 테스트할 때, Lincheck는 공유 메모리 접근 지점(read와 write)이나 동기화 지점(락 획득·해제, park/unpark, wait/notify 등)에 명시적인 스레드 전환 명령을 삽입합니다. 이 접근 방식을 통해 Lincheck는 프로그램의 실행 스케줄을 통제하며 탐색하고, 잘못된 결과를 유발하는 스케줄을 찾아낼 수 있어요.

모델 체킹으로 동시성 코드를 테스트할 때 Lincheck는 실행 스케줄 탐색이 다음 속성을 갖도록 보장합니다:

• 결정적(Deterministic). 입력 데이터가 변하지 않았다면 모델 체킹 테스트를 매번 호출해도 같은 결과가 반환됩니다.
• 제한적(Bounded). 각 테스트는 제한된 수의 실행 스케줄만 탐색합니다. 가능한 실행 스케줄의 수는 프로그램 크기에 따라 기하급수적으로 늘어나는데, 모두 항상 탐색하면 테스트 시간이 크게 늘어나게 됩니다. invocationsPerIteration 값을 변경해 이 한도를 조정할 수 있어요.

스트레스 테스트와 비교하면, 모델 체킹은 Lincheck가 실행 트레이스를 수집할 수 있게 해 주고 실패한 테스트에 대해 버그 재현을 보장합니다. 더 자세한 비교는 테스트 전략 문서의 표를 참고해 주세요.

출처: Model checking

본문

결정적 탐색

Lincheck의 모델 체킹은 입력 데이터와 실행 스케줄이 같다면 테스트 중인 코드가 같은 결과를 만들어야 한다고 요구합니다. 모델 체킹의 결정적 실행 덕분에 Lincheck는 실행 트레이스를 수집하고 실패한 테스트의 버그 재현을 보장할 수 있습니다. 즉, 결정적이지 않은(non-deterministic) 코드가 있으면 모델 체킹이 제대로 작동하지 못하게 됩니다.

실행이 결정적이지 않은 결과를 만들어 내면 Lincheck는 오류를 보고합니다:

Non-determinism found. Probably caused by non-deterministic code (WeakHashMap, Object.hashCode, etc).
== Reporting the first execution without execution trace ==
= Invalid execution results =
| -------- |
| Thread 1 |
| -------- |
| inc(): 2 |
| -------- |

== Reporting the second execution ==
= Invalid execution results =
| -------- |
| Thread 1 |
| -------- |
| inc(): 3 |
| -------- |

비결정성의 근원 중 일부는 Lincheck가 제어하고, 다른 것들은 사용이 제한되거나 예상치 못한 테스트 실패를 일으킬 수 있습니다.

제어되는 비결정성의 근원

모델 체킹 전략으로 테스트를 실행할 때 Lincheck는 다음과 같은 비결정성의 근원을 제어합니다:

• 스레드 전환. 스레드 전환을 JVM에 맡기는 대신, Lincheck는 공유 메모리 접근 지점(read와 write)이나 동기화 지점(락 획득·해제, park/unpark, wait/notify 등)에 명시적인 스레드 전환 명령을 삽입합니다.

• 난수 생성기. Lincheck는 난수 시드(seed)를 고정합니다.

• 아이덴티티 해시 코드(identity hash codes). Lincheck는 객체의 아이덴티티 해시 코드를 고정합니다.

• 시간 API 호출. Lincheck는 시간 API 호출을 가로채 결정적 결과를 반환합니다.

• 최상위 레벨 및 companion object 프로퍼티. 모델 체킹 테스트에서 Lincheck는 (전역 변수에 해당하는 Kotlin의) 최상위 레벨 var 프로퍼티와 companion object 프로퍼티의 값을 호출 사이에 재설정합니다:

  @TestMethodOrder(MethodOrderer.OrderAnnotation::class)
  class VariableResetTest {
      companion object {
          private var atomicInt = AtomicInteger(0)
      }
  
      @Test
      @Order(1)
      fun modelCheckingTest() = Lincheck.runConcurrentTest {
          val t1 = thread { atomicInt.getAndIncrement() }
          val t2 = thread { atomicInt.getAndIncrement() }
  
          t1.join()
          t2.join()
  
          check(atomicInt.get() == 2)
      }
  
      @Test
      @Order(2)
      fun resetAfterModelCheckingTest() {
          // Verify `atomicInt` has been reset to 0 after `modelCheckingTest()`
          check(atomicInt.get() == 0)
      }
  
      @Test
      @Order(3)
      fun regularIncTest() {
          atomicInt.getAndIncrement()
          check(atomicInt.get() == 1)
      }
  
      @Test
      @Order(4)
      fun valuePersistsAfterRegularIncTest() {
          // Verify `atomicInt` still holds 1 after `regularIncTest()`
          check(atomicInt.get() == 1)
      }
  }
  

제어되지 않는 비결정성의 근원

Lincheck는 일부 비결정성의 근원은 제어하지만 전부는 아닙니다. Lincheck가 제어할 수 없는 방식으로 비결정적 코드를 사용하면, 코드의 해당 부분에서 Lincheck를 사용하지 못하거나 해결 방법(workaround)이 필요합니다.

각 제어되지 않는 비결정성의 근원은 전용 섹션에서 자세히 설명합니다:

• 스레드 로컬 변수
• 약한 참조(Weak references)
• I/O API 호출

제한적 탐색

동시성 코드를 테스트할 때 Lincheck는 각 실행 시나리오를 여러 번 실행합니다. 각 시나리오 호출에서 프로그램의 서로 다른 실행 스케줄이 탐색됩니다. 가능한 실행 스케줄의 수는 프로그램 크기에 따라 기하급수적으로 늘어나기 때문에, 테스트 시간을 줄이기 위해 단일 실행 시나리오 테스트의 호출 횟수는 제한됩니다. 모든 실행 스케줄을 탐색하는 데 필요한 호출 횟수가 지정된 한도를 초과하면 Lincheck는 탐색을 중단합니다.

Lincheck가 모든 실행 스케줄을 분석하지 못할 때는 논리적으로 다른 스케줄들을 고르게 분석하려고 시도합니다:

• Lincheck는 먼저 선점적(preemptive) 스레드 전환이 하나 있는 모든 스케줄을 탐색하고, 그다음 두 개 있는 스케줄을 탐색하는 식으로 진행합니다.
• 다음으로 탐색할 스케줄을 고를 때 Lincheck는 새로운 위치에 스레드 전환이 있는 스케줄에 우선순위를 둡니다.

예제: 스레드 전환이 하나 있는 스케줄

두 스레드 시나리오에서 Lincheck가 선점적 스레드 전환이 하나 있는 실행 스케줄을 어떻게 모델링하는지 살펴보겠습니다:

Lincheck는 첫 번째 스레드에 스레드 전환이 있는 스케줄을 모델링하는 것부터 시작하므로, 다음으로 모델링되는 스케줄은 두 번째 스레드에 스레드 전환이 있을 가능성이 높습니다. 이 과정은 Lincheck가 탐색한 스케줄의 한도에 도달하거나 모든 가능한 스케줄을 다 소진할 때까지 계속됩니다.

알려진 제한 사항과 해결 방법

모델 체킹 전략에는 다음과 같은 알려진 제한 사항이 있습니다.

완화된(relaxed) Java 메모리 모델

모델 체킹은 Lincheck가 실행에 대해 순차 일관성(sequentially consistent) 메모리 모델을 가정해야 합니다.

Java에서 사용하는 완화된 메모리 모델은 명령어 재정렬(reordering), 메모리 캐시 동작 등과 관련된 버그를 일으킬 수 있습니다. 모델 체킹으로는 Lincheck가 이러한 효과를 시뮬레이션하거나 관련 버그를 잡을 수 없습니다.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

대부분의 동시성 버그는 순차 일관성 메모리 모델을 가정해도 찾을 수 있습니다. 하지만 Lincheck는 저수준 효과로 인한 일부 버그를 놓칠 수 있어요. 예를 들어 @Volatile 수식어가 빠지면 스토어 버퍼(store buffer)나 컴파일러 재정렬로 인한 버그가 발생할 수 있는데, 이는 Lincheck의 모델 체커로는 잡을 수 없습니다:

class RelaxedMemoryModelTest {
    var x = 0 // Not @Volatile
    var y = 0 // Not @Volatile

    @Test
    fun modelCheckingTest() = Lincheck.runConcurrentTest {
        thread {
            x = 1
            y = 1
        }
        thread {
            if (y == 1 && x == 0) {
                // Code in this block might be executed on real hardware because of
                // store buffer and compiler reordering.
                // Lincheck cannot model this behavior with model checking.
                error("Unreachable under sequential consistency")
            }
        }
    }
}

해결 방법

순차 일관성 메모리 모델을 가정하지 않고 동시성 코드를 테스트하고 싶다면, Lincheck는 동시성 데이터 구조를 위한 스트레스 테스트 전략을 제공합니다.

시나리오 밖에서 생성된 스레드

Lincheck는 동시성 시나리오 안에서 생성된 스레드만 추적할 수 있습니다. 코루틴에서 기본 디스패처를 사용하거나 Java의 ForkJoinPool과 함께 공통 스레드 풀을 사용하는 것처럼, 외부에서 생성된 스레드에서 발생하는 버그는 놓칠 수 있습니다.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

해결 방법

고정 크기 스레드 풀(fixed thread pool)을 사용해 보세요:

• 로컬 코루틴 디스패처로 사용하거나
• ForkJoinPool이 사용하는 공통 스레드 풀 대신 사용합니다.

이렇게 하면 Lincheck가 동시성 시나리오에서 스레드의 수명 주기와 활동을 추적할 수 있다는 것을 보장할 수 있습니다:

class FixedThreadPoolDispatcherTest {
    @Test
    fun test() = Lincheck.runConcurrentTest {
        val dispatcher = Executors.newFixedThreadPool(nThreads).asCoroutineDispatcher()
        dispatcher.use {
            runBlocking(dispatcher) {
                val counter = AtomicInteger(0)
                val coro = launch {
                    while (isActive) { counter.getAndIncrement() }
                }
                coro.cancel()
                coro.join()
            }
        }
    }
}

class FixedThreadPoolExecutorServiceTest {
    @Test
    fun test() = Lincheck.runConcurrentTest {
        val executorService = Executors.newFixedThreadPool(nThreads)
        try {
            val counter = AtomicInteger(0)
            val task = Runnable { counter.getAndIncrement() }
            val future1 = executorService.submit(task)
            val future2 = executorService.submit(task)
            future1.get()
            future2.get()
        } finally {
            executorService.shutdown()
        }
    }
}

스레드 로컬 변수

Lincheck는 (최상위 레벨 var 프로퍼티와 companion object 프로퍼티와는 달리) 같은 시나리오의 여러 호출 동안 스레드 로컬 변수를 재설정하지 않습니다. 이로 인해 같은 테스트의 실행 사이에 불일치가 생깁니다.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

예제:

class ThreadLocalVariableTest {
    @Test
    fun modelCheckingTest() = Lincheck.runConcurrentTest {
        var counter = getLocalCounter()
        var t = thread { counter.getAndIncrement() }
        t.join()
        check(counter.get() == 1)
    }

    private fun getLocalCounter() = localCounter.get()
}

// Using ThreadLocal to create a variable leads to a failed test
private val localCounter: ThreadLocal<AtomicInteger> = ThreadLocal.withInitial {
    AtomicInteger(0)
}

이 테스트는 시나리오 호출 사이에 카운터 값이 누적되기 때문에 오류로 실패합니다:

| ---------------------------------------------------------------------------------------- |
|                   Main Thread                   |                Thread 1                |
| ---------------------------------------------------------------------------------------- |
| getLocalCounter(): AtomicInteger#1              |                                        |
| thread(block = Lambda#1): Thread#1              |                                        |
| switch (reason: waiting for Thread 1 to finish) |                                        |
|                                                 | run()                                  |
|                                                 |   counter ➜ AtomicInteger#1            |
|                                                 |   AtomicInteger#1.getAndIncrement(): 2 |
| Thread#1.join()                                 |                                        |
| counter.element ➜ AtomicInteger#1               |                                        |
| AtomicInteger#1.get(): 3                        |                                        |
| ---------------------------------------------------------------------------------------- |

해결 방법

스레드 ID를 키로 사용하는 ConcurrentHashMap에 값을 저장하여 스레드 로컬 변수를 직접(manually) 만들 수 있습니다:

class ThreadLocalVariableWorkaroundTest {
    var threadLocalCounters = ConcurrentHashMap<Long, AtomicInteger>()

    @Test
    fun modelCheckingTest() = Lincheck.runConcurrentTest {
        var counter = getLocalCounter()
        var t = thread { counter.getAndIncrement() }
        t.join()
        check(counter.get() == 1)
    }

    private fun getLocalCounter() = threadLocalCounters.computeIfAbsent(Thread.currentThread().id) {
        AtomicInteger(0)
    }
}

threadLocalCounters는 최상위 레벨 var 프로퍼티이므로 Lincheck가 호출 사이에 재설정해 누적 문제를 피할 수 있습니다.

약한 참조(Weak references)

Lincheck는 약한 참조로만 참조되는 객체를 가비지 컬렉터가 언제 제거할지 제어하지 않습니다. 이런 객체에 get()을 호출하면 비결정적인 결과가 나옵니다. 약한 참조를 사용해도 테스트가 성공적으로 통과할 수는 있지만, Lincheck가 같은 테스트 실행 사이의 불일치를 발견하면 비결정성 오류를 발생시킵니다.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

시간 API 호출

Lincheck는 같은 테스트 실행 사이의 불일치를 방지하기 위해 java.lang.System.nanoTime()과 java.lang.System.currentTimeMillis() 호출을 미리 정의된 상수를 항상 반환하는 방식으로 시뮬레이션합니다.

이 접근 방식은 타임아웃, 경과 시간 비교, 속도 제한(rate-limiting) 또는 경과 시간에 의존하는 다른 로직을 제대로 시뮬레이션하지 못할 수 있습니다.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

I/O API 호출

Lincheck는 같은 테스트 실행 사이의 불일치를 방지하기 위해 파일과 소켓에 대한 작업을 포함한 I/O API 호출을 지원하지 않습니다.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

I/O API를 호출하면 java.lang.IllegalStateException이 발생합니다:

class FilesCreateTempFileTest {
    @Operation
    fun operation(): List<String> = List(10) {
        val tempFile = Files.createTempFile("test-prefix", ".txt")
        require(Files.exists(tempFile)) { "File was not created: $tempFile" }
        tempFile.toString()
    }

    // The test fails with the following error message:
    // "java.lang.IllegalStateException: File operations are not supported in Lincheck"
    @Test
    fun modelChecking() = ModelCheckingOptions().check(this::class)
}

가상 스레드(Virtual threads)

가상 스레드 지원은 검증되지 않았으며 보장되지 않습니다. 지원이 검증될 때까지는 모델 체킹이 필요한 시나리오에서 플랫폼 스레드(platform threads) 사용을 고려해 보세요.

관련 이슈에 투표하고 진행 상황을 GitHub에서 추적해 보세요.

더 알아보기

• 모델 체킹으로 임의의 동시성 코드를 테스트해 보세요.
• 모델 체킹을 사용해 동시성 데이터 구조를 테스트해 보세요.
• Lincheck 테스트 전략을 구성해 보세요.
• 모델 체킹과 스트레스 테스트를 비교해 보세요.
• 결과 검증 및 확인
• Kotlin Multiplatform 프로젝트에서 Lincheck