Incomplete trace

[bbrockbernd]

Hi! When testing my (faulty) concurrent hash map implementation I found that LinCheck sometimes gives incomplete traces. In the following example there are two screen shots of two steps in the trace. There are no steps (or events) in between the two however the state diagram changes significantly.

Screenshots of the trace and diagrams

Step 1	Step 2

Lincheck test (Inheritance here is important, otherwise it'll cover different scenarios that do not detect a bug.)

package reproLackingTrace

import org.jetbrains.kotlinx.lincheck.LoggingLevel
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
import org.junit.Test

abstract class MyLinCheckTestB {

    @Test
    fun modelCheckingTest() = ModelCheckingOptions()
        .iterations(300)
        .invocationsPerIteration(10_000)
        .actorsBefore(1)
        .threads(3)
        .actorsPerThread(3)
        .actorsAfter(0)
        .checkObstructionFreedom(true)
        .sequentialSpecification(SequentialHashTableIntIntA::class.java)
        .logLevel(LoggingLevel.INFO)
        .check(this::class.java)

}

class MyLinCheckTestsBImpl: MyLinCheckTestB() {
    
    private val map = BlaBlaMap<Int, Int>(2)
    @Operation
    fun get(k: Int): Int? = map.get(k)

    @Operation
    fun put(k: Int, v: Int): Int? = map.put(k, v)

    @Operation
    fun remove(k: Int): Int? = map.remove(k)
}

class SequentialHashTableIntIntB {
    private val map = HashMap<Int, Int>()

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

    fun get(key: Int): Int? = map.get(key)

    fun remove(key: Int): Int? = map.remove(key)
}

Datastructure under test

@file:Suppress("UNCHECKED_CAST")

package reproLackingTrace

import java.util.concurrent.atomic.*
import kotlin.math.absoluteValue

class BlaBlaMap<K : Any, V : Any>(initialCapacity: Int) {
    private val table = AtomicReference(Table(initialCapacity))

    fun put(key: K, value: V): V? {
        return table.get().put(key, value)
    }

    fun get(key: K): V? {
        return table.get().get(key)
    }

    fun remove(key: K): V? {
        return table.get().remove(key)
    }

    data class Fixed(val value: Any)

    inner class Table(val capacity: Int) {

        val keys = AtomicReferenceArray<Any?>(capacity)
        val values = AtomicReferenceArray<Any?>(capacity)
        val nextTable = AtomicReference<Table?>(null)

        fun put(key: K, value: V): V? {
            var index = index(key)
            repeat(MAX_PROBES) {
                while (true) {
                    val curKey = keys[index]
                    when (curKey) {
                        null -> {
                            if (!keys.compareAndSet(index, null, key)) continue
                            if (!values.compareAndSet(index, null, value)) continue
                            return null
                        }
                        key -> {
                            while (true) {
                                val currentValue = values[index]
                                if (currentValue == MOVED) {
                                    return resize { tab ->
                                        tab.put(key, value)
                                    } as V?
                                }
                                if (currentValue is Fixed) {
                                    return resize { tab ->
                                        tab.put(key, value)
                                    } as V?
                                }
                                if (!values.compareAndSet(index, currentValue, value)) continue
                                return currentValue as V?
                            }
                        }
                    }
                    index = (index + 1) % capacity
                    break
                }
            }
            resize()
            return this@BlaBlaMap.put(key, value)
        }

        fun get(key: K): V? {
            var index = index(key)
            repeat(MAX_PROBES) {
                val curKey = keys[index]
                when (curKey) {
                    key -> {
                        val curValue = values[index]
                        if (curValue == MOVED) {
                            resize()
                            return table.get()!!.get(key)
                        }
                        if (curValue is Fixed) {
                            return curValue.value as V?
                        }
                        return values[index] as V?
                    }
                    null -> {
                        return null
                    }
                }
                index = (index + 1) % capacity
            }
            return null
        }

        fun remove(key: K): V? {
            var index = index(key)
            repeat(MAX_PROBES) {
                val curKey = keys[index]
                when (curKey) {
                    key -> {
                        while (true) {
                            val curValue = values[index]
                            if (curValue == MOVED) {
                                return resize { tab ->
                                    tab.remove(key)
                                } as V?
                            }
                            if (curValue is Fixed) {
                                return resize { tab ->
                                    tab.remove(key)
                                } as V?
                            }
                            if (!values.compareAndSet(index, curValue, null)) continue
                            return curValue as V?
                        }
                    }
                    null -> {
                        return null
                    }
                }
                index = (index + 1) % capacity
            }
            return null
        }

        fun resize(doAfter: (Table) -> Any? = { null }): Any? {
            nextTable.compareAndSet(null, Table(capacity * 2))
            val next = nextTable.get()!!

            for (i in 0 ..< capacity) {
                while (true) {
                    val curKey = keys[i]
                    val curValue = values[i]

                    // if already moved continue
                    if (curValue == MOVED) break

                    // if empty or removed -> MOVED
                    if (curValue == null) {
                        if (!values.compareAndSet(i, null, MOVED)) continue
                        break
                    }

                    // if fixed -> put value and set MOVED
                    if (curValue is Fixed) {
                        // Set value in new table
                        next.put(curKey as K, curValue.value as V)

                        // Set value to moved in this table
                        if (!values.compareAndSet(i, curValue, MOVED)) continue
                        break
                    }

                    // if normal value -> fix
                    values.compareAndSet(i, curValue, Fixed(curValue))
                }
            }

            val resultAfter = doAfter(next)

            //Update table reference
            while (true) {
                val currentTable = table.get()
                if (currentTable.capacity >= nextTable.get()!!.capacity) break
                table.compareAndSet(currentTable, nextTable.get())
            }

            return resultAfter

        }

        private fun index(key: Any) = ((key.hashCode() * MAGIC) % capacity).absoluteValue
    }
}

private const val MAGIC = -0x61c88647 // golden ratio 
private const val MAX_PROBES = 2
private val NEEDS_REHASH = Any()
private val MOVED = Any()

[ndkoval]

@bbrockbernd could you please also provide the trace from the console output?

[bbrockbernd]

Sure thing

Detailed trace:
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
|                                        Thread 1                                         | Thread 2 |                                        Thread 3                                         |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| put(-1, -1): null                                                                       |          |                                                                                         |
|   map.put(-1,-1): null at MyLinCheckTestsBImpl.put(MyLinCheckTestB.kt:33)               |          |                                                                                         |
|     table.get(): Table#1 at BlaBlaMap.put(BlaBlaMap.kt:12)                              |          |                                                                                         |
|   result: null                                                                          |          |                                                                                         |
| put(1, 1): null                                                                         |          |                                                                                         |
|   map.put(1,1): null at MyLinCheckTestsBImpl.put(MyLinCheckTestB.kt:33)                 |          |                                                                                         |
|     table.get(): Table#1 at BlaBlaMap.put(BlaBlaMap.kt:12)                              |          |                                                                                         |
|   result: null                                                                          |          |                                                                                         |
| put(0, -1): null                                                                        |          |                                                                                         |
|   map.put(0,-1): null at MyLinCheckTestsBImpl.put(MyLinCheckTestB.kt:33)                |          |                                                                                         |
|     table.get(): Table#1 at BlaBlaMap.put(BlaBlaMap.kt:12)                              |          |                                                                                         |
|     Table#1.put(0,-1): null at BlaBlaMap.put(BlaBlaMap.kt:12)                           |          |                                                                                         |
|       MyLinCheckTestsBImpl#1.map.table.get(): Table#2 at BlaBlaMap.put(BlaBlaMap.kt:12) |          |                                                                                         |
|   result: null                                                                          |          |                                                                                         |
| put(-2, -3): null                                                                       |          |                                                                                         |
|   map.put(-2,-3): null at MyLinCheckTestsBImpl.put(MyLinCheckTestB.kt:33)               |          |                                                                                         |
|     table.get(): Table#2 at BlaBlaMap.put(BlaBlaMap.kt:12)                              |          |                                                                                         |
|   result: null                                                                          |          |                                                                                         |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
|                                                                                         |          | put(2, 4): null                                                                         |
|                                                                                         |          |   map.put(2,4): null at MyLinCheckTestsBImpl.put(MyLinCheckTestB.kt:33)                 |
|                                                                                         |          |     table.get(): Table#2 at BlaBlaMap.put(BlaBlaMap.kt:12)                              |
|                                                                                         |          |     switch                                                                              |
| remove(1): null                                                                         |          |                                                                                         |
|   map.remove(1): null at MyLinCheckTestsBImpl.remove(MyLinCheckTestB.kt:36)             |          |                                                                                         |
|     table.get(): Table#3 at BlaBlaMap.remove(BlaBlaMap.kt:20)                           |          |                                                                                         |
|   result: null                                                                          |          |                                                                                         |
|                                                                                         |          |     Table#2.put(2,4): null at BlaBlaMap.put(BlaBlaMap.kt:12)                            |
|                                                                                         |          |       MyLinCheckTestsBImpl#1.map.table.get(): Table#3 at BlaBlaMap.put(BlaBlaMap.kt:12) |
|                                                                                         |          |       MyLinCheckTestsBImpl#1.map.table.get(): Table#3 at BlaBlaMap.put(BlaBlaMap.kt:12) |
|                                                                                         |          |   result: null                                                                          |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |

[eupp]

Hi @bbrockbernd !
This could be the expected behavior or indeed a bug in Lincheck.

Lincheck does not actually add all the events into the trace (i.e. all variable reads/writes).
In some cases, as an optimization, it can skip accesses to some objects, if it can deduce the object is "local" and never escapes its thread.

Could you please re-check, if it is the case here, or if Lincheck incorrectly classified some object as "local"?

[bbrockbernd]

Hi @eupp, I believe the object is not local since it is shared among threads.

Also, if an object is classified as local (and for my understanding, unimportant for the lincheck test) shouldn't it be excluded from the lincheck state diagram?

Another example shows a significant change in state when switching from one thread to the other. However, with this trace it is unclear to me what exactly happened:

before switch	after switch