결과 검증과 유효성 확인

결과 검증과 유효성 확인

동시성 데이터 구조를 위해 생성된 시나리오를 실행한 뒤, Lincheck는 결과를 지정된 검증 모델(예: 선형화 가능성, linearizability)과 대조해 검증하고, 선택적으로 데이터 구조의 최종 상태를 사용자가 제공한 검증 함수와 대조해 확인해요.

출처: Results verification and validation

본문

검증 (Verification)

검증 과정에서 Lincheck는 동시성 시나리오의 연산들을 순차 실행했을 때 동시 실행과 같은 결과를 내는 순차 실행을 찾으려 해요. 검증 모델에 따라 순차 실행에 추가 제약이 있을 수 있어요. 검증 속성과 일치하는 순차 실행이 관찰된 결과를 만들 수 없다면, Lincheck는 오류를 보고해요.

순차 명세 (Sequential specification)

기본적으로 검증 과정에서 Lincheck는 동시성 데이터 구조의 연산을 사용해 순차 실행을 구성해요. 일치하는 연산을 가진 순차 데이터 구조를 지정하면 다음을 할 수 있어요:

  • 동시성 데이터 구조가 순차 데이터 구조와 같은 결과를 내는지 확인해요. 일반적으로 단일 스레드 구현은 스레드 안전 구현보다 단순해서, 정확성을 훨씬 쉽게 검증할 수 있어요(예: HashMap과 ConcurrentHashMap, LinkedList와 ConcurrentLinkedQueue). 두 버전의 실행 결과를 비교하면, 더 복잡한 동시성 구조가 단일 스레드 환경의 단순한 구조와 비슷하게 동작하는지 확인할 수 있어요.
  • 순차 정확성과 동시성 안전성을 한 번의 테스트로 검증해요.

데이터 구조의 순차 버전을 지정하려면:

  1. Lincheck가 테스트하는 모든 동시 함수의 순차 버전을 가진 데이터 구조를 구현해요.
  2. sequentialSpecification() 옵션으로 데이터 구조를 지정해요:
@Test
fun stressTest() = StressOptions()
    .sequentialSpecification(SequentialQueue::class.java)
    .check(this::class)

단일 스레드 LinkedList를 ConcurrentLinkedQueue의 순차 명세로 사용하는 Lincheck 테스트 예시는 다음과 같아요:

class ConcurrentLinkedQueueTest {
    private val s = ConcurrentLinkedQueue<Int>()

    @Operation
    fun add(value: Int) = s.add(value)

    @Operation
    fun poll(): Int? = s.poll()

    @Test
    fun stressTest() = StressOptions()
        .sequentialSpecification(SequentialQueue::class.java)
        .check(this::class)
}

class SequentialQueue {
    private val s = LinkedList<Int>()

    fun add(x: Int) = s.add(x)
    fun poll(): Int? = s.poll()
}

검증 모델 (Verification models)

기본적으로 Lincheck는 동시 실행 결과를 선형화 가능성(linearizability) 모델에 대조해 검증해요. 다른 검증 모델을 적용하려면 verifier 옵션을 사용해요:

@Test
fun customVerifierTest() = ModelCheckingOptions()
    .verifier(SerializabilityVerifier::class.java)
    .check(this::class.java)

Lincheck는 다음 검증기(verifier) 클래스를 제공해요:

  • LinearizabilityVerifier – 기본 옵션이에요. 동시 실행에서 연산 간의 "happens-before" 관계를 보존하는 순차 실행이 존재하면 동시 실행은 유효해요.
  • QuiescentConsistencyVerifier – quiescent consistency(정지 일관성) 모델을 사용해요. linearizability 모델과 비슷하게 동작하지만, @QuiescentConsistent로 표시된 연산에는 "happens-before" 제약이 적용되지 않아요:
@Operation
@QuiescentConsistent
fun someOperation() = { ... }

QuiescentConsistencyVerifier는 실제 quiescent 지점을 추적하지 않아요. 따라서 이 검증기는 quiescent 지점 경계를 가로질러 발생하는 버그를 놓칠 수 있어요.

  • SerializabilityVerifier – serializability(직렬화 가능성) 모델을 사용해요. "happens-before" 제약과 무관하게, 동시 실행과 같은 결과를 내는 어떤 순차 실행(아무 순서든)이 존재하면 동시 실행은 유효해요. 동시 연산의 상대적 순서가 중요하지 않은 구조에 사용할 수 있어요.
serializability와 linearizability 비교하기

두 모델의 차이를 이해하려면, 데이터 구조가 serializable하지만 linearizable하지 않은 경우를 살펴봐요:

  1. 다음 데이터 구조를 생각해 봐요:
class ConcurrentQueue {
    private val elements: MutableList<Int> = ArrayList()

    fun put(x: Int) = synchronized(this) {
        elements += x
    }

    fun poll(): Int? = synchronized(this) {
        if (elements.isEmpty()) return null
        elements.shuffle()
        elements.removeAt(0)
    }
}

이 동시성 구조는 잘못 동작해요. 일반적인 큐처럼 요소를 저장하지만, 반환할 때는 무작위로 돌려줘요.

  1. 요소를 제대로 저장하고 반환하는 큐의 순차 버전을 구현해요:
class CorrectSequentialQueue {
    private val elements: MutableList<Int> = ArrayList()

    fun put(x: Int) {
        elements += x
    }

    fun poll(): Int? = if (elements.isEmpty()) null else elements.removeAt(0)
}
  1. 테스트 클래스를 만들고 put()과 poll() 연산을 선언해요:
@Param(name = "value", gen = IntGen::class, conf = "1:2")
class ConcurrentQueueTest {
    private val q = ConcurrentQueue()

    @Operation
    fun put(@Param(name = "value") x: Int) = q.put(x)

    @Operation
    fun poll(): Int? = q.poll()
}
  1. serializability 테스트를 선언하고 실행해요:
@Test
fun serializabilityTest() = ModelCheckingOptions()
    .actorsBefore(0)
    .actorsAfter(0)
    .actorsPerThread(2)
    .threads(2)
    // Use the `SerializabilityVerifier`
    .verifier(SerializabilityVerifier::class.java)
    // Specify the sequential version of the structure
    .sequentialSpecification(CorrectSequentialQueue::class.java)
    .check(this::class.java)

성공적으로 통과해야 해요.

  1. linearizability 테스트를 선언하고 실행해요:
@Test
fun linearizabilityTest() = ModelCheckingOptions()
    .actorsBefore(0)
    .actorsAfter(0)
    .actorsPerThread(2)
    .threads(2)
    // Show the full failed scenario
    .minimizeFailedScenario(false)
    // Specify the sequential version of the structure
    .sequentialSpecification(CorrectSequentialQueue::class.java)
    .check(this::class.java)

다음 보고서와 함께 테스트가 실패해야 해요:

| -------------------- |
| Thread 1  | Thread 2 |
| -------------------- |
|           | put(2)   |
|           | put(1)   |
| put(3)    |          |
| poll(): 1 |          |
| -------------------- |
  1. 결과를 분석해요. serializability 테스트가 통과했기 때문에, poll(): 1을 만들어내는 SequentialQueue 연산의 어떤 순차 순서가 존재해요. 하지만 linearizability는 연산 순서를 더 제한해요. 동시 실행에서 연산 A가 연산 B가 시작되기 전에 끝났다면, 순차 실행에서도 A가 B보다 먼저 실행돼야 해요. Lincheck는 검증 중에 put() 연산을 재정렬할 수 없기 때문에, linearizability 제약을 따르는 순차 실행을 찾지 못해요. 그 결과 테스트가 실패해요.

유효성 확인 (Validation)

기본적으로 Lincheck는 생성된 시나리오를 실행한 뒤 동시성 데이터 구조의 상태를 검증하지 않아요. 최종 상태를 확인하려면 테스트 클래스의 검증 함수에 @Validate 어노테이션을 사용해요:

@Validate
fun validate() {
    // Check some property of the data structure
    // Throw an exception if the check is violated
    check(storage.size >= 2) { "Size must be at least 2, but was ${storage.size}" }
}

검증 함수는 다음 조건을 충족해야 해요:

  • 인수를 받지 않아야 해요.
  • 데이터 구조가 잘못된 상태에 있으면 예외를 던져야 해요.

더 알아보기

  • 인자 생성 제약 구성하기 (Configuring argument generation constraints)
  • 연산 실행 구성하기 (Configuring operation execution)
  • 논블로킹 진행 보장 확인하기 (Checking for non-blocking progress guarantees)