Skip to content
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ abstract class ManagedOptions<OPT : Options<OPT, CTEST>, CTEST : CTestConfigurat
protected var checkObstructionFreedom = DEFAULT_CHECK_OBSTRUCTION_FREEDOM
protected var hangingDetectionThreshold = DEFAULT_HANGING_DETECTION_THRESHOLD
protected val guarantees: MutableList<ManagedStrategyGuarantee> = ArrayList(DEFAULT_GUARANTEES)
internal var stdLibAnalysisEnabled: Boolean = true
internal var stdLibAnalysisEnabled: Boolean = false

/**
* Use the specified number of scenario invocations to study interleavings in each iteration.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@ private fun SingleThreadedTable<TraceNode>.compressSuspendImpl() = compressNodes
if (it.tracePoint is CodeLocationTracePoint) {
(it.tracePoint as CodeLocationTracePoint).codeLocation = singleChild.tracePoint.codeLocation
}
it.decrementCallDepthOfTree()
newNode.addChild(it)
}
newNode
Expand Down Expand Up @@ -110,7 +109,6 @@ private fun combineNodes(parent: CallNode, child: CallNode): TraceNode {
check(parent.tracePoint.thrownException == child.tracePoint.thrownException)

val newNode = parent.copy()
child.decrementCallDepthOfTree()
child.children.forEach { newNode.addChild(it) }
return newNode
}
Expand All @@ -128,7 +126,6 @@ private fun SingleThreadedTable<TraceNode>.compressSyntheticFieldAccess() = comp
if (point is ReadTracePoint) point.codeLocation = node.tracePoint.codeLocation
if (point is WriteTracePoint) point.codeLocation = node.tracePoint.codeLocation

singleChild.decrementCallDepthOfTree()
singleChild
}

Expand Down Expand Up @@ -162,10 +159,7 @@ private fun SingleThreadedTable<TraceNode>.compressUserThreadRun() = compressNod
if (!isUserThreadStart(node.tracePoint, child.tracePoint)) return@compressNodes node

val newNode = node.copy()
node.children.getOrNull(0)?.children?.forEach {
it.decrementCallDepthOfTree()
newNode.addChild(it)
}
node.children.getOrNull(0)?.children?.forEach { newNode.addChild(it) }
newNode
}

Expand All @@ -189,27 +183,35 @@ private fun SingleThreadedTable<TraceNode>.compressThreadStart() = compressNodes
newNode
}

internal fun SingleThreadedTable<TraceNode>.collapseLibraries(analysisProfile: AnalysisProfile) = compressNodes { node ->
/**
* Collapses library code that should be hidden according to [analysisProfile].
* A [verbose] collapsed graph keeps the paths of hidden calls up to non hidden code visible.
*/
internal fun SingleThreadedTable<TraceNode>.collapseLibraries(analysisProfile: AnalysisProfile, verbose: Boolean) = compressNodes { node ->
// if should not be hidden
if (node !is CallNode || !analysisProfile.shouldBeHidden(node)) return@compressNodes node

// if cannot be hidden (due to switch point)
if (node.containsDescendant { it is EventNode && it.tracePoint is SwitchEventTracePoint })
if (verbose && node.containsDescendant(::isNonHideableNode))
return@compressNodes node

val newNode = node.copy()
findSubTreesToBeShown(node, analysisProfile).forEach { newNode.addChild(it) }
findSubTreesAndEventsToBeShown(node, analysisProfile).forEach { newNode.addChild(it) }
return@compressNodes newNode
}

private fun isNonHideableNode(traceNode: TraceNode) =
traceNode is EventNode && (traceNode.tracePoint is SwitchEventTracePoint || traceNode.tracePoint is ParkTracePoint)

/**
* Finds descendants that should not be hidden.
* But not descendants of descendants, aka the roots of all subtrees that should be shown in the trace.
*/
private fun findSubTreesToBeShown(node: TraceNode, analysisProfile: AnalysisProfile): List<TraceNode> {
private fun findSubTreesAndEventsToBeShown(node: TraceNode, analysisProfile: AnalysisProfile): List<TraceNode> {
if (node is EventNode && node.tracePoint is SwitchEventTracePoint || node.tracePoint is ParkTracePoint) return listOf(node)
if (node !is CallNode) return emptyList()
if (!analysisProfile.shouldBeHidden(node)) return listOf(node)
return node.children.map { findSubTreesToBeShown(it, analysisProfile) }.flatten()
return node.children.map { findSubTreesAndEventsToBeShown(it, analysisProfile) }.flatten()
}

private fun SingleThreadedTable<TraceNode>.compressNodes(compressionRule: (TraceNode) -> TraceNode) = map {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ internal class VerboseTraceFlattenPolicy : TraceFlattenPolicy {

// Check if result node should be added
if (descendants.size > 1 && returnedValue is ReturnedValueResult.ActorResult && returnedValue.showAtEndOfActor) {
return descendants + ResultNode(currentNode.callDepth + 1, returnedValue, descendants.last().eventNumber, currentNode.tracePoint)
return descendants + ResultNode(currentNode.callDepth + 1, returnedValue, currentNode.lastEventNumberOfDescendants, currentNode.tracePoint)
}

return descendants
Expand Down Expand Up @@ -114,7 +114,7 @@ internal class ShortTraceFlattenPolicy : TraceFlattenPolicy {

// Check if result node should be added
val nodesToReturn = if (descendants.size > 1 && returnedValue is ReturnedValueResult.ActorResult && returnedValue.showAtEndOfActor) {
descendants + ResultNode(currentNode.callDepth + 1, returnedValue, descendants.last().eventNumber, currentNode.tracePoint)
descendants + ResultNode(currentNode.callDepth + 1, returnedValue, currentNode.lastEventNumberOfDescendants, currentNode.tracePoint)
// Or thread start root nodes
} else if (descendants.size == 1 && descendants.contains(currentNode) && currentNode.tracePoint.isThreadStart) {
descendants + currentNode.children
Expand Down Expand Up @@ -158,7 +158,10 @@ internal fun TraceNode.flattenNodes(policy: TraceFlattenPolicy): List<TraceNode>
}

internal fun SingleThreadedTable<TraceNode>.flattenNodes(flattenPolicy: TraceFlattenPolicy): SingleThreadedTable<TraceNode> =
map { section -> section.flatMap { traceNode -> traceNode.flattenNodes(flattenPolicy) } }
map { section ->
section.forEach { it.setCallDepthOfTree(0) }
section.flatMap { traceNode -> traceNode.flattenNodes(flattenPolicy) }
}

//for idea plugin
internal fun SingleThreadedTable<TraceNode>.extractPreExpandedNodes(flattenPolicy: TraceFlattenPolicy): List<TraceNode> =
Expand Down
22 changes: 18 additions & 4 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/trace/TraceNodes.kt
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
package org.jetbrains.kotlinx.lincheck.trace

import kotlin.collections.plus
import kotlin.math.max

/**
* Represents a single node in the hierarchical trace structure.
Expand All @@ -34,6 +35,9 @@ internal abstract class TraceNode(var callDepth: Int, val eventNumber: Int, open
var parent: TraceNode? = null
private set

var lastEventNumberOfDescendants = eventNumber
private set

// Am i last event. Check at parents and all ancestors
val isLast: Boolean get() {
if (parent == null) return true
Expand All @@ -43,14 +47,15 @@ internal abstract class TraceNode(var callDepth: Int, val eventNumber: Int, open
fun addChild(node: TraceNode) {
_children.add(node)
node.parent = this
setLastEventNumber(node.lastEventNumberOfDescendants)
}

abstract override fun toString(): String

// Shifts stackTrace to the left
fun decrementCallDepthOfTree() {
callDepth--
children.forEach { it.decrementCallDepthOfTree() }
// Sets call depth of this (sub)tree
fun setCallDepthOfTree(depth: Int) {
callDepth = depth
children.forEach { it.setCallDepthOfTree(depth + 1) }
}

fun lastOrNull(predicate: (TraceNode) -> Boolean): TraceNode? {
Expand Down Expand Up @@ -83,6 +88,12 @@ internal abstract class TraceNode(var callDepth: Int, val eventNumber: Int, open
* Shallow copy without children
*/
abstract fun copy(): TraceNode

// sets the last event number of descendants, is called whenever a child is added
protected fun setLastEventNumber(lastEventNumber: Int) {
lastEventNumberOfDescendants = max(lastEventNumber, lastEventNumberOfDescendants)
parent?.setLastEventNumber(lastEventNumberOfDescendants)
}
}

internal class EventNode(
Expand All @@ -92,6 +103,7 @@ internal class EventNode(
): TraceNode(callDepth, eventNumber, tracePoint) {
override fun toString(): String = tracePoint.toString()
override fun copy(): TraceNode = EventNode(callDepth, tracePoint, eventNumber)
.also { it.setLastEventNumber(lastEventNumberOfDescendants) }
}

internal class CallNode(
Expand All @@ -104,6 +116,7 @@ internal class CallNode(

override fun toString(): String = tracePoint.toString()
override fun copy(): TraceNode = CallNode(callDepth, tracePoint, eventNumber)
.also { it.setLastEventNumber(lastEventNumberOfDescendants) }

internal fun createResultNodeForEmptyActor() =
ResultNode(callDepth + 1, tracePoint.returnedValue as ReturnedValueResult.ActorResult, eventNumber, tracePoint)
Expand All @@ -114,6 +127,7 @@ internal class ResultNode(callDepth: Int, val actorResult: ReturnedValueResult.A
: TraceNode(callDepth, eventNumber, tracePoint) {
override fun toString(): String = "result: ${actorResult.resultRepresentation}"
override fun copy(): TraceNode = ResultNode(callDepth, actorResult, eventNumber, tracePoint)
.also { it.setLastEventNumber(lastEventNumberOfDescendants) }
}

// (stable) Sort on eventNumber
Expand Down
15 changes: 10 additions & 5 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/trace/TraceReporter.kt
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ import org.jetbrains.kotlinx.lincheck.execution.*
import org.jetbrains.kotlinx.lincheck.runner.ExecutionPart
import org.jetbrains.kotlinx.lincheck.strategy.*
import org.jetbrains.kotlinx.lincheck.strategy.ValidationFailure
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingCTestConfiguration
import kotlin.math.max

internal typealias SingleThreadedTable<T> = List<SingleThreadedSection<T>>
Expand Down Expand Up @@ -62,15 +61,22 @@ internal class TraceReporter(
// Optimizes trace by combining trace points for synthetic field accesses etc..
val compressedTraceGraph = traceGraph
.compressTrace()
.collapseLibraries(failure.analysisProfile)

graph = if (isGeneralPurposeModelCheckingScenario(failure.scenario)) removeGPMCLambda(compressedTraceGraph) else compressedTraceGraph
}

fun appendTrace(stringBuilder: StringBuilder) = with(stringBuilder) {
// Turn graph into chronological sequence of calls and events, for verbose and simple trace.
val flattenedShort: SingleThreadedTable<TraceNode> = graph.flattenNodes(ShortTraceFlattenPolicy()).reorder()
val flattenedVerbose: SingleThreadedTable<TraceNode> = graph.flattenNodes(VerboseTraceFlattenPolicy()).reorder()
val flattenedShort: SingleThreadedTable<TraceNode> = graph
.collapseLibraries(failure.analysisProfile, verbose = false)
.flattenNodes(ShortTraceFlattenPolicy())
.reorder()

val flattenedVerbose: SingleThreadedTable<TraceNode> = graph
.collapseLibraries(failure.analysisProfile, verbose = true)
.flattenNodes(VerboseTraceFlattenPolicy())
.reorder()

appendTraceTable(TRACE_TITLE, flattenedShort)
appendLine()

Expand Down Expand Up @@ -133,7 +139,6 @@ private fun removeGPMCLambda(graph: SingleThreadedTable<TraceNode>): SingleThrea
val first = section.first()
if (first !is CallNode) return@map section
if (first.children.isEmpty()) return@map listOf(first.createResultNodeForEmptyActor())
first.decrementCallDepthOfTree()
if (first.children.firstOrNull() is CallNode) (first.children.first() as CallNode).tracePoint.returnedValue = first.tracePoint.returnedValue
first.children + section.drop(1)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -295,8 +295,13 @@ internal class AnalysisProfile(val analyzeStdLib: Boolean) {
isJavaExecutorService(className) && methodName == "submit" -> AnalysisSectionType.SILENT_PROPAGATING
isJavaExecutorService(className) -> AnalysisSectionType.SILENT
className.startsWith("java.util.concurrent.locks.AbstractQueuedSynchronizer") -> AnalysisSectionType.SILENT

// This DS is non linearizable
className.startsWith("java.util.concurrent.ConcurrentLinkedDeque") -> AnalysisSectionType.NORMAL
className.startsWith("java.util.concurrent.atomic") -> AnalysisSectionType.NORMAL
className.startsWith("java.util.concurrent.locks") -> AnalysisSectionType.NORMAL
!analyzeStdLib && className.startsWith("java.util.concurrent.") -> AnalysisSectionType.SILENT
className == "java.util.concurrent.FutureTask" -> AnalysisSectionType.SILENT
isConcurrentCollectionsLibrary(className) && !analyzeStdLib -> AnalysisSectionType.SILENT

else -> AnalysisSectionType.NORMAL
}
Expand All @@ -311,7 +316,7 @@ internal class AnalysisProfile(val analyzeStdLib: Boolean) {
*/
@Suppress("UNUSED_PARAMETER") // methodName is here for uniformity and might become useful in the future
fun shouldBeHidden(className: String, methodName: String): Boolean =
!analyzeStdLib && (isConcurrentCollectionsLibrary(className) || isCollectionsLibrary(className))
!analyzeStdLib && (isCollectionsLibrary(className) || className.startsWith("java.util.concurrent."))
}

internal fun isCollectionsLibrary(className: String) = className in setOf(
Expand Down Expand Up @@ -355,39 +360,6 @@ internal fun isCollectionsLibrary(className: String) = className in setOf(
"java.util.TreeMap",
)

internal fun isConcurrentCollectionsLibrary(className: String) = className in setOf(
// Interfaces
"java.util.concurrent.BlockingDeque",
"java.util.concurrent.BlockingQueue",
"java.util.concurrent.TransferQueue",
"java.util.concurrent.ConcurrentMap",
"java.util.concurrent.ConcurrentNavigableMap",

// Concrete implementations
// Concurrent collections
"java.util.concurrent.ConcurrentHashMap",
"java.util.concurrent.ConcurrentLinkedDeque",
"java.util.concurrent.ConcurrentLinkedQueue",
"java.util.concurrent.ConcurrentSkipListMap",
"java.util.concurrent.ConcurrentSkipListSet",

// Blocking queues
"java.util.concurrent.ArrayBlockingQueue",
"java.util.concurrent.LinkedBlockingDeque",
"java.util.concurrent.LinkedBlockingQueue",
"java.util.concurrent.DelayQueue",
"java.util.concurrent.PriorityBlockingQueue",
"java.util.concurrent.SynchronousQueue",
"java.util.concurrent.LinkedTransferQueue",

// Copy-on-write collections
"java.util.concurrent.CopyOnWriteArrayList",
"java.util.concurrent.CopyOnWriteArraySet",

// Inner class view
"java.util.concurrent.ConcurrentHashMap\$KeySetView"
)

private fun isJavaExecutorService(className: String) =
className.startsWith("java.util.concurrent.AbstractExecutorService") ||
className.startsWith("java.util.concurrent.ThreadPoolExecutor") ||
Expand Down
Loading