진행 보장

많은 동시성 알고리즘은 wait-freedom, lock-freedom, obstruction-freedom 같은 논블로킹(non-blocking) 진행 보장(progress guarantee)을 제공해요. Lincheck는 obstruction-freedom 검증만 지원해요. 다만 lock-free 알고리즘과 wait-free 알고리즘도 obstruction-free이기 때문에, obstruction-freedom을 위반하면 더 강한 보장도 함께 위반한 게 돼요.

프로그램의 obstruction-freedom 보장을 검증하려면 checkObstructionFreedom 옵션을 사용해요:

@Test
fun modelCheckingTest() = ModelCheckingOptions()
    .checkObstructionFreedom()
    .check(this::class)

checkObstructionFreedom 옵션은 모델 체킹(model checking) 전략에서만 사용할 수 있어요. Lincheck는 다른 모든 스레드가 멈춰 있을 때 특정 스레드가 진행할 수 있는지 확인해서 obstruction-freedom을 검증해요. 만약 스레드 실행이 루프에서 멈추면, Lincheck는 active lock(활성 락)을 보고해요. 특정 함수가 의도적으로 블로킹이라면 @Operation(blocking = true)로 표시해서 오탐(false positive)을 막을 수 있어요.

출처: Progress guarantees

본문

예: ConcurrentHashMap의 obstruction-freedom 테스트

이 예제에서는 ConcurrentHashMap 구조의 put() 함수를 테스트해요.

ConcurrentHashMapTest.kt 파일을 만들어요.
ConcurrentHashMap용 테스트 클래스를 만들고, put() 함수와 checkObstructionFreedom() 옵션이 켜진 테스트 함수를 선언해요:

class ConcurrentHashMapTest {
    private val map = ConcurrentHashMap<Int, Int>()

    @Operation
    fun put(key: Int, value: Int) = map.put(key, value)

    @Test
    fun modelCheckingTest() = ModelCheckingOptions()
        .checkObstructionFreedom()
        .threads(2)
        .actorsPerThread(1)
        .check(this::class)
}

threads와 actorsPerThread 옵션은 가능한 실행 시나리오의 수를 줄이는 데 사용돼요. 이 옵션들은 테스트의 통과/실패 여부를 바꾸지 않지만, 테스트 시간을 크게 줄여줘요.

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

= The algorithm should be non-blocking, but an active lock is detected =
| --------------------- |
| Thread 1  | Thread 2  |
| --------------------- |
| put(1, 0) | put(1, 1) |
| --------------------- |

The following interleaving leads to the error:
| -------------------------------------------------------------------------------------------------------------- |
|                                          Thread 1                                          |     Thread 2      |
| -------------------------------------------------------------------------------------------------------------- |
| put(1, 0): <hung>                                                                          |                   |
|   map.put(1, 0)                                                                            |                   |
|     putVal(1, 0, false)                                                                    |                   |
|       spread(1): 1                                                                         |                   |
|       table ➜ null                                                                         |                   |
|       loop(1 iterations) at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1016)          |                   |
|         <iteration 1>                                                                      |                   |
|           initTable()                                                                      |                   |
|             loop(1 iterations) at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2293) |                   |
|             table ➜ null                                                                   |                   |
|             switch                                                                         |                   |
|                                                                                            | put(1, 1): <hung> |
| -------------------------------------------------------------------------------------------------------------- |

put() 함수 어노테이션에 blocking = true 옵션을 추가해요:

@Operation(blocking = true)
fun put(key: Int, value: Int) = map.put(key, value)

테스트를 다시 실행해요. 성공적으로 통과해야 해요.

예: ConcurrentSkipListMap의 obstruction-freedom 테스트

이 예제에서는 논블로킹 ConcurrentSkipListMap 구조의 put() 함수를 테스트해요.

ConcurrentSkipListMapTest.kt 파일을 만들어요.
ConcurrentSkipListMap용 테스트 클래스를 만들고, put() 함수와 checkObstructionFreedom() 옵션이 켜진 테스트 함수를 선언해요:

class ConcurrentSkipListMapTest {
    private val map = ConcurrentSkipListMap<Int, Int>()

    @Operation
    fun put(key: Int, value: Int) = map.put(key, value)

    @Test
    fun modelCheckingTest() = ModelCheckingOptions()
        .checkObstructionFreedom()
        .check(this::class)
}

테스트를 실행해요. 성공적으로 통과해야 해요.

더 알아보기

인자 생성 제약 구성하기 (Configuring argument generation constraints)
연산 실행 구성하기 (Configuring operation execution)
실행 결과 검증하기 (Validating execution results)