From 2c765fac4a49273f2db7e20a860ad4e773d720f2 Mon Sep 17 00:00:00 2001 From: Michael Litvinov <81708672+litvinovmitch11@users.noreply.github.com> Date: Sun, 18 Oct 2026 00:17:27 +0300 Subject: [PATCH 1/9] Add base interfaces (#2) --- README.md | 1 + docs/solver-profiling.md | 58 ++++++ ksmt-profiling/build.gradle.kts | 19 ++ .../io/ksmt/profiling/KSolverProfile.kt | 179 ++++++++++++++++++ .../io/ksmt/profiling/KSolverProfiler.kt | 47 +++++ settings.gradle.kts | 1 + 6 files changed, 305 insertions(+) create mode 100644 docs/solver-profiling.md create mode 100644 ksmt-profiling/build.gradle.kts create mode 100644 ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfile.kt create mode 100644 ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfiler.kt diff --git a/README.md b/README.md index 55af96a2b..540b5a236 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,7 @@ Get the most out of SMT solving with KSMT features: * Utilities to [simplify and transform](#utilities-to-simplify-and-transform-expressions) your expressions * Switching between solvers and support for [portfolio mode](#using-multiple-solvers--portfolio-mode-) * Running solvers in a [separate process](#running-solvers-in-separate-processes) to reduce timeout-related crashes +* Observation-only contracts for profiling incremental solver workloads through the optional [`ksmt-profiling`](docs/solver-profiling.md) module * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml) diff --git a/docs/solver-profiling.md b/docs/solver-profiling.md new file mode 100644 index 000000000..4d1c4e361 --- /dev/null +++ b/docs/solver-profiling.md @@ -0,0 +1,58 @@ +# Solver workload profiling contracts + +The optional `ksmt-profiling` module defines an observation-only, interface +boundary for incremental solver workloads. It does not contain a profiler +implementation, configuration recommender, model training, configuration +search, ONNX Runtime, or a model. + +## Profile model + +`KSolverProfile` describes one solver session from profiler construction +through the corresponding solver `close` call. A snapshot may be taken while +the session is still active: + +- stable profile/run identifiers and session state; +- solver name, version, and attributes; +- native-default or unknown base configuration plus observed overrides; +- ordered solver events timed with `kotlin.time.Duration`; +- asserted KSMT formulas and per-check assumptions; +- `push` and `pop` operations needed to reconstruct the active formula; +- check timeout and status, plus explicit access to a backend-specific reason + for `UNKNOWN`; +- active and total assertion counts, task context, and failures. + +Failed solver calls are retained because a profile is an observation and must +not silently rewrite workload history. They are not configurations to tune. +Result-access events explicitly reference the check that produced the accessed +result when such a check exists. + +Configuration values are observational data only. The initial snapshot is +needed to determine whether a workload can be reproduced from native defaults; +it is not a recommendation. KSMT does not define patch +application, recommendation decisions, or a tuner lifecycle. + +Expressions stay as in-memory `KExpr` objects. Serializing formulas +or producing consumer-specific feature tensors is intentionally outside the +KSMT contract. + +## Extension point + +`KSolverProfilerFactory` wraps an existing solver using explicit session IDs, +solver metadata, initial configuration, attributes, and an event limit. +`KSolverProfiler` extends `KSolver` and specifies the future +transparent decorator. It exposes a structurally independent `snapshot` and +optional application task context. Recording may continue after a snapshot, +but the returned collections must remain stable. Profiling must not turn a +successful delegate call into a failure. KSMT does not yet provide an +implementation. + +The event limit bounds retained AST references. A profile retains the ordered +event prefix up to that limit, continues forwarding every solver call, and +increments `droppedEventCount` for each later event. Session state and observed +duration continue to advance. Consumers must treat `isTruncated` profiles as +ineligible for exact replay. + +Consumers may use a profile for diagnostics, benchmarking, or external tuning, +but those policies and their output types belong to the consumer. In +particular, cvc5 option whitelists, configuration patches, feature projection, +ONNX adapters, decoding, and fallback do not belong in KSMT. diff --git a/ksmt-profiling/build.gradle.kts b/ksmt-profiling/build.gradle.kts new file mode 100644 index 000000000..64f9a945e --- /dev/null +++ b/ksmt-profiling/build.gradle.kts @@ -0,0 +1,19 @@ +plugins { + id("io.ksmt.ksmt-base") +} + +dependencies { + api(project(":ksmt-core")) +} + +publishing { + publications { + create("maven") { + from(components["java"]) + + addKsmtPom() + addSourcesAndJavadoc(project) + signKsmtPublication(project) + } + } +} diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfile.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfile.kt new file mode 100644 index 000000000..3bc94e930 --- /dev/null +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfile.kt @@ -0,0 +1,179 @@ +package io.ksmt.profiling + +import io.ksmt.expr.KExpr +import io.ksmt.solver.KSolverStatus +import io.ksmt.sort.KBoolSort +import java.time.Instant +import kotlin.time.Duration + +/** Identifies the solver implementation whose workload was observed. */ +data class KSolverDescriptor( + val name: String, + val version: String? = null, + val attributes: Map = emptyMap(), +) + +/** + * Application-defined context attached to solver calls made for one logical unit of work. + * + * A task does not affect solver behavior. It lets consumers group calls by an application + * concept such as a symbolic state, method, request, or fork without adding that concept to the + * generic KSMT API. + */ +data class KSolverTask( + val id: String, + val kind: String? = null, + val attributes: Map = emptyMap(), +) + +/** Describes what configuration existed when the profiled solver session was created. */ +enum class KSolverConfigurationBase { + /** Native defaults of the solver version declared in [KSolverDescriptor]. */ + SOLVER_DEFAULTS, + + /** The complete base configuration cannot be reconstructed. */ + UNKNOWN, +} + +/** An observed solver configuration value. It has no application or merge semantics. */ +sealed class KSolverConfigurationValue { + data class BoolValue(val value: Boolean) : KSolverConfigurationValue() + data class IntValue(val value: Int) : KSolverConfigurationValue() + data class StringValue(val value: String) : KSolverConfigurationValue() + data class DoubleValue(val value: Double) : KSolverConfigurationValue() +} + +/** Native defaults or an unknown base, followed by the explicit overrides observed by KSMT. */ +data class KSolverConfigurationSnapshot( + val base: KSolverConfigurationBase, + val overrides: Map = emptyMap(), +) + +/** Whether the observed solver call returned normally or threw. */ +enum class KSolverCallOutcome { + SUCCESS, + FAILURE, +} + +/** Timing, state, task, and failure metadata shared by every recorded solver event. */ +data class KSolverCallMetadata( + val sequenceNumber: Long, + val startedAfterSession: Duration, + val duration: Duration, + val outcome: KSolverCallOutcome, + val task: KSolverTask?, + val stackDepth: Int, + val activeAssertionCount: Long, + val totalAssertionCount: Long, + val failureType: String? = null, + val failureMessage: String? = null, +) + +/** One ordered operation in an incremental solver session. */ +sealed interface KSolverProfileEvent { + val metadata: KSolverCallMetadata +} + +/** An inspectable configuration change. Null overrides denote an opaque backend-specific change. */ +data class KSolverConfigureEvent( + val overrides: Map?, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +/** A formula added by one single-expression solver call. */ +data class KSolverAssertEvent( + val expression: KExpr, + val tracked: Boolean, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +/** Formulas added by one bulk solver call. */ +data class KSolverAssertBatchEvent( + val expressions: List>, + val tracked: Boolean, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +data class KSolverPushEvent( + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +data class KSolverPopEvent( + val levels: UInt, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +/** + * A satisfiability check over the active assertion stack and optional assumptions. + * + * The active formula can be reconstructed by replaying assertion and scope events up to this + * event. [assumptions] are used only for this check. [status] is null when the call failed before + * returning a solver status. + */ +data class KSolverCheckEvent( + val checkId: Long, + val assumptions: List> = emptyList(), + val timeout: Duration = Duration.INFINITE, + val status: KSolverStatus? = null, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +enum class KSolverResultAccessKind { + MODEL, + UNSAT_CORE, + REASON_OF_UNKNOWN, +} + +/** Access to a result associated with [checkId], or null when no check could be associated. */ +data class KSolverResultAccessEvent( + val kind: KSolverResultAccessKind, + val checkId: Long?, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +enum class KSolverLifecycleEventKind { + INTERRUPT, + CLOSE, +} + +data class KSolverLifecycleEvent( + val kind: KSolverLifecycleEventKind, + override val metadata: KSolverCallMetadata, +) : KSolverProfileEvent + +/** Whether the observed solver session can still receive calls. */ +enum class KSolverProfileState { + ACTIVE, + CLOSED, + CLOSE_FAILED, +} + +/** + * In-memory snapshot of one solver session, from profiler construction through solver close. + * + * Expressions remain KSMT AST objects. Persistence and consumer-specific feature tensors are + * outside this contract and belong to profile consumers. Implementations of [KSolverProfiler] + * must return snapshots whose collection structure cannot change when recording continues. + */ +data class KSolverProfile( + val schemaVersion: String, + val profileId: String, + val runId: String, + val parentProfileId: String? = null, + val state: KSolverProfileState, + val solver: KSolverDescriptor, + val startedAt: Instant, + val observedDuration: Duration, + val initialConfiguration: KSolverConfigurationSnapshot, + val eventLimit: Int, + val events: List, + val droppedEventCount: Long, + val attributes: Map = emptyMap(), +) { + val isTruncated: Boolean + get() = droppedEventCount != 0L + + companion object { + const val CURRENT_SCHEMA_VERSION = "ksmt-solver-profile-v0" + } +} diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfiler.kt new file mode 100644 index 000000000..2c323cf04 --- /dev/null +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KSolverProfiler.kt @@ -0,0 +1,47 @@ +package io.ksmt.profiling + +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration + +/** Immutable construction data for one bounded profiling decorator. */ +data class KSolverProfilerRequest( + val profileId: String, + val runId: String, + val parentProfileId: String? = null, + val solver: KSolverDescriptor, + val initialConfiguration: KSolverConfigurationSnapshot, + val maxRecordedEvents: Int, + val attributes: Map = emptyMap(), +) + +/** Creates transparent profiling decorators without exposing an implementation constructor. */ +interface KSolverProfilerFactory { + fun wrap( + delegate: KSolver, + request: KSolverProfilerRequest, + ): KSolverProfiler +} + +/** + * Contract for a transparent [KSolver] decorator that observes one solver session. + * + * KSMT currently defines this boundary but does not provide an implementation. A future + * implementation must preserve delegate behavior, retain asserted expressions and assumptions, + * report calls in execution order, and never turn a successful delegate call into a failure + * because recording or snapshot construction failed. + */ +interface KSolverProfiler : KSolver { + /** + * Returns a structurally independent snapshot of the observations recorded so far. + * + * Recording may continue after the snapshot is returned, but its collections must not change. + */ + fun snapshot(): KSolverProfile + + /** + * Attaches observational application context to calls made by [block]. + * + * Nested blocks use the innermost task and restore the previous task even when [block] throws. + */ + fun withTask(task: KSolverTask, block: KSolverProfiler.() -> T): T +} diff --git a/settings.gradle.kts b/settings.gradle.kts index 19ee79b05..136d4c148 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -1,5 +1,6 @@ rootProject.name = "ksmt" include("ksmt-core") +include("ksmt-profiling") include("ksmt-z3") include("ksmt-z3:ksmt-z3-core") From 45d5fd0a1de17f14454a09ab464eeeddc6a201fb Mon Sep 17 00:00:00 2001 From: Michael Litvinov Date: Fri, 16 Oct 2026 14:04:42 +0300 Subject: [PATCH 2/9] good random search (cherry picked from commit 51c4c193253fbf25f697149fbfdf9ce3ae44ac5b) --- .../profiling/KRecordingSolverProfiler.kt | 360 ++++++++++++++++++ .../profiling/KRecordingSolverProfilerTest.kt | 187 +++++++++ 2 files changed, 547 insertions(+) create mode 100644 ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt create mode 100644 ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerTest.kt diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt new file mode 100644 index 000000000..f39e2db52 --- /dev/null +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt @@ -0,0 +1,360 @@ +package io.ksmt.profiling + +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.sort.KBoolSort +import java.time.Instant +import java.util.concurrent.atomic.AtomicLong +import java.util.UUID +import kotlin.time.Duration +import kotlin.time.Duration.Companion.nanoseconds + +/** + * Transparent in-memory [KSolver] decorator. + * + * The decorator never serializes expressions and never invokes solver operations that the caller + * did not request. Result-access events refer to the last successfully completed check without + * calling any additional solver operation. + */ +@Suppress("LongParameterList") +class KRecordingSolverProfiler( + private val delegate: KSolver, + private val solver: KSolverDescriptor, + private val profileId: String = UUID.randomUUID().toString(), + private val runId: String = UUID.randomUUID().toString(), + private val parentProfileId: String? = null, + private val initialConfiguration: KSolverConfigurationSnapshot = + KSolverConfigurationSnapshot(KSolverConfigurationBase.UNKNOWN), + private val profileAttributes: Map = emptyMap(), + private val maxRecordedEvents: Int = DEFAULT_MAX_RECORDED_EVENTS, +) : KSolverProfiler { + private val startedAt = Instant.now() + private val startedAtNanos = System.nanoTime() + private val nextSequenceNumber = AtomicLong() + private val nextCheckId = AtomicLong() + private val eventsLock = Any() + private val events = arrayListOf() + private val assertionCountsByScope = arrayListOf(0L) + private val currentTask = ThreadLocal() + + private var totalAssertionCount = 0L + private var droppedEventCount = 0L + private var lastSuccessfulCheckId: Long? = null + private var state = KSolverProfileState.ACTIVE + + init { + require(maxRecordedEvents > 0) { "Maximum recorded event count must be positive" } + } + + override fun snapshot(): KSolverProfile = synchronized(eventsLock) { + KSolverProfile( + schemaVersion = KSolverProfile.CURRENT_SCHEMA_VERSION, + profileId = profileId, + runId = runId, + parentProfileId = parentProfileId, + state = state, + solver = solver.copy(attributes = solver.attributes.toMap()), + startedAt = startedAt, + observedDuration = elapsedDuration(System.nanoTime()), + initialConfiguration = + initialConfiguration.copy(overrides = initialConfiguration.overrides.toMap()), + eventLimit = maxRecordedEvents, + events = events.sortedBy { it.metadata.sequenceNumber }.toList(), + droppedEventCount = droppedEventCount, + attributes = profileAttributes.toMap(), + ) + } + + override fun withTask(task: KSolverTask, block: KSolverProfiler.() -> T): T { + val previousTask = currentTask.get() + currentTask.set(task) + return try { + this.block() + } finally { + currentTask.set(previousTask) + } + } + + override fun configure(configurator: Config.() -> Unit) { + recordUnitCall( + event = { metadata -> KSolverConfigureEvent(overrides = null, metadata) }, + ) { + delegate.configure(configurator) + } + } + + override fun assert(expr: KExpr) { + recordUnitCall( + onSuccess = { addAssertions(1) }, + event = { metadata -> KSolverAssertEvent(expr, tracked = false, metadata) }, + ) { + delegate.assert(expr) + } + } + + override fun assert(exprs: List>) { + recordUnitCall( + onSuccess = { addAssertions(exprs.size) }, + event = { metadata -> KSolverAssertBatchEvent(exprs.toList(), tracked = false, metadata) }, + ) { + delegate.assert(exprs) + } + } + + override fun assertAndTrack(expr: KExpr) { + recordUnitCall( + onSuccess = { addAssertions(1) }, + event = { metadata -> KSolverAssertEvent(expr, tracked = true, metadata) }, + ) { + delegate.assertAndTrack(expr) + } + } + + override fun assertAndTrack(exprs: List>) { + recordUnitCall( + onSuccess = { addAssertions(exprs.size) }, + event = { metadata -> KSolverAssertBatchEvent(exprs.toList(), tracked = true, metadata) }, + ) { + delegate.assertAndTrack(exprs) + } + } + + override fun push() { + recordUnitCall( + onSuccess = { assertionCountsByScope.add(0L) }, + event = { metadata -> KSolverPushEvent(metadata) }, + ) { + delegate.push() + } + } + + override fun pop(n: UInt) { + recordUnitCall( + onSuccess = { + val removedScopeCount = minOf(n.toLong(), assertionCountsByScope.lastIndex.toLong()).toInt() + repeat(removedScopeCount) { + assertionCountsByScope.removeAt(assertionCountsByScope.lastIndex) + } + }, + event = { metadata -> KSolverPopEvent(n, metadata) }, + ) { + delegate.pop(n) + } + } + + override fun check(timeout: Duration): KSolverStatus { + val checkId = nextCheckId.getAndIncrement() + return recordResultCall( + onSuccess = { lastSuccessfulCheckId = checkId }, + onFailure = { lastSuccessfulCheckId = null }, + event = { status, metadata -> + KSolverCheckEvent( + checkId = checkId, + timeout = timeout, + status = status, + metadata = metadata, + ) + }, + ) { + delegate.check(timeout) + } + } + + override fun checkWithAssumptions( + assumptions: List>, + timeout: Duration, + ): KSolverStatus { + val checkId = nextCheckId.getAndIncrement() + return recordResultCall( + onSuccess = { lastSuccessfulCheckId = checkId }, + onFailure = { lastSuccessfulCheckId = null }, + event = { status, metadata -> + KSolverCheckEvent( + checkId = checkId, + assumptions = assumptions.toList(), + timeout = timeout, + status = status, + metadata = metadata, + ) + }, + ) { + delegate.checkWithAssumptions(assumptions, timeout) + } + } + + override fun model(): KModel = + recordResultCall( + event = { _, metadata -> + KSolverResultAccessEvent(KSolverResultAccessKind.MODEL, lastSuccessfulCheckId, metadata) + }, + ) { + delegate.model() + } + + override fun unsatCore(): List> = + recordResultCall( + event = { _, metadata -> + KSolverResultAccessEvent(KSolverResultAccessKind.UNSAT_CORE, lastSuccessfulCheckId, metadata) + }, + ) { + delegate.unsatCore() + } + + override fun reasonOfUnknown(): String = + recordResultCall( + event = { _, metadata -> + KSolverResultAccessEvent( + KSolverResultAccessKind.REASON_OF_UNKNOWN, + lastSuccessfulCheckId, + metadata, + ) + }, + ) { + delegate.reasonOfUnknown() + } + + override fun interrupt() { + recordUnitCall( + event = { metadata -> KSolverLifecycleEvent(KSolverLifecycleEventKind.INTERRUPT, metadata) }, + ) { + delegate.interrupt() + } + } + + override fun close() { + recordUnitCall( + onSuccess = { state = KSolverProfileState.CLOSED }, + onFailure = { state = KSolverProfileState.CLOSE_FAILED }, + event = { metadata -> KSolverLifecycleEvent(KSolverLifecycleEventKind.CLOSE, metadata) }, + ) { + delegate.close() + } + } + + private fun addAssertions(count: Int) { + val countAsLong = count.toLong() + assertionCountsByScope[assertionCountsByScope.lastIndex] += countAsLong + totalAssertionCount += countAsLong + } + + private inline fun recordUnitCall( + crossinline onSuccess: () -> Unit = {}, + crossinline onFailure: (Throwable) -> Unit = {}, + crossinline event: (KSolverCallMetadata) -> KSolverProfileEvent, + block: () -> Unit, + ) { + recordResultCall( + onSuccess = { onSuccess() }, + onFailure = onFailure, + event = { _, metadata -> event(metadata) }, + block = block, + ) + } + + @Suppress("TooGenericExceptionCaught") + private inline fun recordResultCall( + crossinline onSuccess: (T) -> Unit = {}, + crossinline onFailure: (Throwable) -> Unit = {}, + crossinline event: (T?, KSolverCallMetadata) -> KSolverProfileEvent, + block: () -> T, + ): T { + val call = beginCall() + val result = try { + block() + } catch (error: Throwable) { + runCatching { + synchronized(eventsLock) { + onFailure(error) + addEvent( + event( + null, + call.metadata( + outcome = KSolverCallOutcome.FAILURE, + failureType = error.javaClass.name, + failureMessage = error.message, + ), + ), + ) + } + } + throw error + } + + runCatching { + synchronized(eventsLock) { + onSuccess(result) + addEvent(event(result, call.metadata(KSolverCallOutcome.SUCCESS))) + } + } + return result + } + + private fun beginCall(): ProfiledCall = + ProfiledCall( + sequenceNumber = nextSequenceNumber.getAndIncrement(), + startedAtNanos = System.nanoTime(), + task = currentTask.get()?.let { it.copy(attributes = it.attributes.toMap()) }, + ) + + private fun ProfiledCall.metadata( + outcome: KSolverCallOutcome, + failureType: String? = null, + failureMessage: String? = null, + ): KSolverCallMetadata { + val finishedAtNanos = System.nanoTime() + return KSolverCallMetadata( + sequenceNumber = sequenceNumber, + startedAfterSession = elapsedDuration(startedAtNanos), + duration = (finishedAtNanos - startedAtNanos).coerceAtLeast(0).nanoseconds, + outcome = outcome, + task = task, + stackDepth = assertionCountsByScope.lastIndex, + activeAssertionCount = assertionCountsByScope.sum(), + totalAssertionCount = totalAssertionCount, + failureType = failureType, + failureMessage = failureMessage, + ) + } + + private fun elapsedDuration(now: Long): Duration = + (now - startedAtNanos).coerceAtLeast(0).nanoseconds + + private fun addEvent(event: KSolverProfileEvent) { + if (events.size < maxRecordedEvents) { + events += event + } else { + droppedEventCount++ + } + } + + private data class ProfiledCall( + val sequenceNumber: Long, + val startedAtNanos: Long, + val task: KSolverTask?, + ) + + companion object { + const val DEFAULT_MAX_RECORDED_EVENTS = 1_000_000 + } +} + +/** Reference factory for the experimental in-memory profiler implementation. */ +object KRecordingSolverProfilerFactory : KSolverProfilerFactory { + override fun wrap( + delegate: KSolver, + request: KSolverProfilerRequest, + ): KSolverProfiler = + KRecordingSolverProfiler( + delegate = delegate, + solver = request.solver, + profileId = request.profileId, + runId = request.runId, + parentProfileId = request.parentProfileId, + initialConfiguration = request.initialConfiguration, + profileAttributes = request.attributes, + maxRecordedEvents = request.maxRecordedEvents, + ) +} diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerTest.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerTest.kt new file mode 100644 index 000000000..84287b246 --- /dev/null +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerTest.kt @@ -0,0 +1,187 @@ +package io.ksmt.profiling + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KTheory +import io.ksmt.solver.model.KModelImpl +import io.ksmt.sort.KBoolSort +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertIs +import kotlin.test.assertSame +import kotlin.time.Duration + +class KRecordingSolverProfilerTest { + private val ctx = KContext() + + @Test + fun `records an incremental session without replacing bulk delegate calls`() { + val delegate = RecordingSolver(ctx) + val profiler = profiler(delegate) + val expressions = listOf(ctx.mkTrue(), ctx.mkFalse()) + + profiler.withTask(KSolverTask("fork-7", kind = "tsa-fork")) { + push() + assert(expressions) + checkWithAssumptions(listOf(ctx.mkTrue()), Duration.INFINITE) + pop() + } + + val profile = profiler.snapshot() + assertEquals(1, delegate.bulkAssertionCalls) + assertEquals(4, profile.events.size) + assertEquals(KSolverProfile.CURRENT_SCHEMA_VERSION, profile.schemaVersion) + + assertIs(profile.events[0]) + val assertion = assertIs(profile.events[1]) + assertSame(expressions[0], assertion.expressions[0]) + assertEquals(2, assertion.metadata.activeAssertionCount) + assertEquals(1, assertion.metadata.stackDepth) + assertEquals("fork-7", assertion.metadata.task?.id) + + val check = assertIs(profile.events[2]) + assertEquals(0, check.checkId) + assertEquals(KSolverStatus.UNKNOWN, check.status) + assertEquals(1, check.assumptions.size) + + val pop = assertIs(profile.events[3]) + assertEquals(0, pop.metadata.activeAssertionCount) + assertEquals(0, pop.metadata.stackDepth) + assertEquals(2, pop.metadata.totalAssertionCount) + } + + @Test + fun `links unknown reason access to the preceding check`() { + val profiler = profiler(RecordingSolver(ctx)) + + profiler.check() + assertEquals("test unknown", profiler.reasonOfUnknown()) + val events = profiler.snapshot().events + val check = events[0] as KSolverCheckEvent + val access = events[1] as KSolverResultAccessEvent + assertEquals(KSolverResultAccessKind.REASON_OF_UNKNOWN, access.kind) + assertEquals(check.checkId, access.checkId) + } + + @Test + fun `records failures and rethrows the same exception`() { + val failure = IllegalStateException("delegate failure") + val delegate = RecordingSolver(ctx, checkFailure = failure) + val profiler = profiler(delegate) + + val actual = assertFailsWith { profiler.check() } + assertSame(failure, actual) + + val event = assertIs(profiler.snapshot().events.single()) + assertEquals(KSolverCallOutcome.FAILURE, event.metadata.outcome) + assertEquals(IllegalStateException::class.java.name, event.metadata.failureType) + assertEquals(null, event.status) + } + + @Test + fun `bounds retained events and reports truncation`() { + val profiler = + KRecordingSolverProfiler( + delegate = RecordingSolver(ctx), + solver = KSolverDescriptor("test"), + maxRecordedEvents = 1, + ) + + profiler.push() + profiler.pop() + + val profile = profiler.snapshot() + assertEquals(1, profile.events.size) + assertEquals(1, profile.eventLimit) + assertEquals(1, profile.droppedEventCount) + assertEquals(true, profile.isTruncated) + } + + @Test + fun `preserves and records empty batches and zero-level pop`() { + val delegate = RecordingSolver(ctx) + val profiler = profiler(delegate) + + profiler.assert(emptyList()) + profiler.pop(0u) + + val events = profiler.snapshot().events + assertEquals(1, delegate.bulkAssertionCalls) + assertEquals(emptyList(), (events[0] as KSolverAssertBatchEvent).expressions) + assertEquals(0u, (events[1] as KSolverPopEvent).levels) + } + + @Test + fun `links profile identity and records successful close`() { + val profiler = + KRecordingSolverProfiler( + delegate = RecordingSolver(ctx), + solver = KSolverDescriptor("test"), + profileId = "profile-0", + runId = "run-0", + parentProfileId = "parent-0", + ) + + assertEquals(KSolverProfileState.ACTIVE, profiler.snapshot().state) + profiler.close() + + val profile = profiler.snapshot() + assertEquals("profile-0", profile.profileId) + assertEquals("run-0", profile.runId) + assertEquals("parent-0", profile.parentProfileId) + assertEquals(KSolverProfileState.CLOSED, profile.state) + } + + private fun profiler(delegate: RecordingSolver) = + KRecordingSolverProfiler( + delegate = delegate, + solver = KSolverDescriptor("test", version = "v0"), + ) + + private class TestConfiguration : KSolverConfiguration { + override fun setBoolParameter(param: String, value: Boolean) = Unit + override fun setIntParameter(param: String, value: Int) = Unit + override fun setStringParameter(param: String, value: String) = Unit + override fun setDoubleParameter(param: String, value: Double) = Unit + override fun optimizeForTheories(theories: Set?, quantifiersAllowed: Boolean) = Unit + } + + private class RecordingSolver( + private val ctx: KContext, + private val checkFailure: Throwable? = null, + ) : KSolver { + var bulkAssertionCalls = 0 + + override fun configure(configurator: TestConfiguration.() -> Unit) = TestConfiguration().configurator() + override fun assert(expr: KExpr) = Unit + + override fun assert(exprs: List>) { + bulkAssertionCalls++ + } + + override fun assertAndTrack(expr: KExpr) = Unit + override fun push() = Unit + override fun pop(n: UInt) = Unit + + override fun check(timeout: Duration): KSolverStatus { + checkFailure?.let { throw it } + return KSolverStatus.UNKNOWN + } + + override fun checkWithAssumptions( + assumptions: List>, + timeout: Duration, + ): KSolverStatus = KSolverStatus.UNKNOWN + + override fun model(): KModel = KModelImpl(ctx, emptyMap(), emptyMap()) + override fun unsatCore(): List> = emptyList() + override fun reasonOfUnknown(): String = "test unknown" + override fun interrupt() = Unit + override fun close() = Unit + } +} From fbcb3688c7f9fddc1b1888a49cf217f7400bb67e Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Mon, 19 Oct 2026 20:43:00 +0300 Subject: [PATCH 3/9] Record profiler events in strict sequence order Number and store every call under one lock, keep interrupt outside it, track active assertions in a counter. Add concurrency tests. --- .../profiling/KRecordingSolverProfiler.kt | 116 +++++---- ...KRecordingSolverProfilerConcurrencyTest.kt | 225 ++++++++++++++++++ 2 files changed, 298 insertions(+), 43 deletions(-) create mode 100644 ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt index f39e2db52..4b491a765 100644 --- a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt @@ -7,7 +7,6 @@ import io.ksmt.solver.KSolverConfiguration import io.ksmt.solver.KSolverStatus import io.ksmt.sort.KBoolSort import java.time.Instant -import java.util.concurrent.atomic.AtomicLong import java.util.UUID import kotlin.time.Duration import kotlin.time.Duration.Companion.nanoseconds @@ -18,6 +17,15 @@ import kotlin.time.Duration.Companion.nanoseconds * The decorator never serializes expressions and never invokes solver operations that the caller * did not request. Result-access events refer to the last successfully completed check without * calling any additional solver operation. + * + * Ordering guarantees: + * - Every solver call except [interrupt] holds [eventsLock] from the moment its sequence number is + * assigned until its event is stored. Calls from several threads therefore run one after another + * and events are stored in sequence order. When the event limit is reached, the retained events + * are an exact prefix of the call history. + * - [interrupt] forwards to the delegate without waiting for the lock, so it can stop a check that + * is running in another thread. Its event is numbered and stored after that check has finished. + * - [snapshot] waits for a running solver call to finish. */ @Suppress("LongParameterList") class KRecordingSolverProfiler( @@ -33,13 +41,15 @@ class KRecordingSolverProfiler( ) : KSolverProfiler { private val startedAt = Instant.now() private val startedAtNanos = System.nanoTime() - private val nextSequenceNumber = AtomicLong() - private val nextCheckId = AtomicLong() private val eventsLock = Any() - private val events = arrayListOf() - private val assertionCountsByScope = arrayListOf(0L) private val currentTask = ThreadLocal() + // Everything below is guarded by [eventsLock]. + private val events = arrayListOf() + private val assertionCountsByScope = arrayListOf(0L) + private var nextSequenceNumber = 0L + private var nextCheckId = 0L + private var activeAssertionCount = 0L private var totalAssertionCount = 0L private var droppedEventCount = 0L private var lastSuccessfulCheckId: Long? = null @@ -62,7 +72,7 @@ class KRecordingSolverProfiler( initialConfiguration = initialConfiguration.copy(overrides = initialConfiguration.overrides.toMap()), eventLimit = maxRecordedEvents, - events = events.sortedBy { it.metadata.sequenceNumber }.toList(), + events = events.toList(), droppedEventCount = droppedEventCount, attributes = profileAttributes.toMap(), ) @@ -133,21 +143,16 @@ class KRecordingSolverProfiler( override fun pop(n: UInt) { recordUnitCall( - onSuccess = { - val removedScopeCount = minOf(n.toLong(), assertionCountsByScope.lastIndex.toLong()).toInt() - repeat(removedScopeCount) { - assertionCountsByScope.removeAt(assertionCountsByScope.lastIndex) - } - }, + onSuccess = { removeScopes(n) }, event = { metadata -> KSolverPopEvent(n, metadata) }, ) { delegate.pop(n) } } - override fun check(timeout: Duration): KSolverStatus { - val checkId = nextCheckId.getAndIncrement() - return recordResultCall( + override fun check(timeout: Duration): KSolverStatus = synchronized(eventsLock) { + val checkId = nextCheckId++ + recordResultCall( onSuccess = { lastSuccessfulCheckId = checkId }, onFailure = { lastSuccessfulCheckId = null }, event = { status, metadata -> @@ -166,9 +171,9 @@ class KRecordingSolverProfiler( override fun checkWithAssumptions( assumptions: List>, timeout: Duration, - ): KSolverStatus { - val checkId = nextCheckId.getAndIncrement() - return recordResultCall( + ): KSolverStatus = synchronized(eventsLock) { + val checkId = nextCheckId++ + recordResultCall( onSuccess = { lastSuccessfulCheckId = checkId }, onFailure = { lastSuccessfulCheckId = null }, event = { status, metadata -> @@ -216,12 +221,30 @@ class KRecordingSolverProfiler( delegate.reasonOfUnknown() } + /** + * Forwards to the delegate without taking [eventsLock], so it can stop a check that is running + * in another thread. The event is numbered and stored after the delegate call returns. + */ override fun interrupt() { - recordUnitCall( - event = { metadata -> KSolverLifecycleEvent(KSolverLifecycleEventKind.INTERRUPT, metadata) }, - ) { - delegate.interrupt() + val startedAtNanos = System.nanoTime() + val task = currentTaskSnapshot() + val failure = runCatching { delegate.interrupt() }.exceptionOrNull() + synchronized(eventsLock) { + val call = ProfiledCall(nextSequenceNumber++, startedAtNanos, task) + runCatching { + addEvent( + KSolverLifecycleEvent( + KSolverLifecycleEventKind.INTERRUPT, + call.metadata( + outcome = if (failure == null) KSolverCallOutcome.SUCCESS else KSolverCallOutcome.FAILURE, + failureType = failure?.javaClass?.name, + failureMessage = failure?.message, + ), + ), + ) + } } + if (failure != null) throw failure } override fun close() { @@ -237,9 +260,17 @@ class KRecordingSolverProfiler( private fun addAssertions(count: Int) { val countAsLong = count.toLong() assertionCountsByScope[assertionCountsByScope.lastIndex] += countAsLong + activeAssertionCount += countAsLong totalAssertionCount += countAsLong } + private fun removeScopes(n: UInt) { + val removedScopeCount = minOf(n.toLong(), assertionCountsByScope.lastIndex.toLong()).toInt() + repeat(removedScopeCount) { + activeAssertionCount -= assertionCountsByScope.removeAt(assertionCountsByScope.lastIndex) + } + } + private inline fun recordUnitCall( crossinline onSuccess: () -> Unit = {}, crossinline onFailure: (Throwable) -> Unit = {}, @@ -260,45 +291,44 @@ class KRecordingSolverProfiler( crossinline onFailure: (Throwable) -> Unit = {}, crossinline event: (T?, KSolverCallMetadata) -> KSolverProfileEvent, block: () -> T, - ): T { + ): T = synchronized(eventsLock) { val call = beginCall() val result = try { block() } catch (error: Throwable) { runCatching { - synchronized(eventsLock) { - onFailure(error) - addEvent( - event( - null, - call.metadata( - outcome = KSolverCallOutcome.FAILURE, - failureType = error.javaClass.name, - failureMessage = error.message, - ), + onFailure(error) + addEvent( + event( + null, + call.metadata( + outcome = KSolverCallOutcome.FAILURE, + failureType = error.javaClass.name, + failureMessage = error.message, ), - ) - } + ), + ) } throw error } runCatching { - synchronized(eventsLock) { - onSuccess(result) - addEvent(event(result, call.metadata(KSolverCallOutcome.SUCCESS))) - } + onSuccess(result) + addEvent(event(result, call.metadata(KSolverCallOutcome.SUCCESS))) } - return result + result } private fun beginCall(): ProfiledCall = ProfiledCall( - sequenceNumber = nextSequenceNumber.getAndIncrement(), + sequenceNumber = nextSequenceNumber++, startedAtNanos = System.nanoTime(), - task = currentTask.get()?.let { it.copy(attributes = it.attributes.toMap()) }, + task = currentTaskSnapshot(), ) + private fun currentTaskSnapshot(): KSolverTask? = + currentTask.get()?.let { it.copy(attributes = it.attributes.toMap()) } + private fun ProfiledCall.metadata( outcome: KSolverCallOutcome, failureType: String? = null, @@ -312,7 +342,7 @@ class KRecordingSolverProfiler( outcome = outcome, task = task, stackDepth = assertionCountsByScope.lastIndex, - activeAssertionCount = assertionCountsByScope.sum(), + activeAssertionCount = activeAssertionCount, totalAssertionCount = totalAssertionCount, failureType = failureType, failureMessage = failureMessage, diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt new file mode 100644 index 000000000..ae878a55d --- /dev/null +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt @@ -0,0 +1,225 @@ +package io.ksmt.profiling + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KTheory +import io.ksmt.solver.model.KModelImpl +import io.ksmt.sort.KBoolSort +import java.util.concurrent.CountDownLatch +import java.util.concurrent.TimeUnit +import kotlin.concurrent.thread +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertIs +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class KRecordingSolverProfilerConcurrencyTest { + private val ctx = KContext() + + @Test + fun `events from several threads are stored in sequence order`() { + val profiler = profiler(StubSolver(ctx)) + val threadCount = 8 + val callsPerThread = 200 + + val threads = (0 until threadCount).map { + thread { + repeat(callsPerThread) { + profiler.push() + profiler.assert(ctx.mkTrue()) + profiler.pop() + } + } + } + threads.forEach { it.join() } + + val events = profiler.snapshot().events + assertEquals(threadCount * callsPerThread * 3, events.size) + events.forEachIndexed { index, event -> + assertEquals(index.toLong(), event.metadata.sequenceNumber) + } + assertEquals(threadCount * callsPerThread.toLong(), events.last().metadata.totalAssertionCount) + } + + @Test + fun `event limit keeps an exact prefix under concurrency`() { + val profiler = KRecordingSolverProfiler( + delegate = StubSolver(ctx), + solver = KSolverDescriptor("test"), + maxRecordedEvents = 50, + ) + + (0 until 4).map { thread { repeat(100) { profiler.push() } } }.forEach { it.join() } + + val profile = profiler.snapshot() + assertEquals(50, profile.events.size) + assertEquals(350L, profile.droppedEventCount) + profile.events.forEachIndexed { index, event -> + assertEquals(index.toLong(), event.metadata.sequenceNumber) + } + } + + @Test + fun `interrupt is forwarded while another thread is inside check`() { + val delegate = BlockingCheckSolver(ctx) + val profiler = profiler(delegate) + + val checker = thread { profiler.check() } + assertTrue(delegate.checkStarted.await(5, TimeUnit.SECONDS)) + + // The check holds the profiler lock; interrupt must still reach the delegate. + profiler.interrupt() + checker.join(5_000) + + assertTrue(delegate.interrupted) + val events = profiler.snapshot().events + assertEquals(2, events.size) + assertIs(events[0]) + val interrupt = assertIs(events[1]) + assertEquals(KSolverLifecycleEventKind.INTERRUPT, interrupt.kind) + assertEquals(1L, interrupt.metadata.sequenceNumber) + } + + @Test + fun `failed close marks an active profile`() { + val failure = IllegalStateException("close failure") + val profiler = profiler(StubSolver(ctx, closeFailure = failure)) + + val actual = assertFailsWith { profiler.close() } + + assertEquals(failure, actual) + assertEquals(KSolverProfileState.CLOSE_FAILED, profiler.snapshot().state) + } + + @Test + fun `active assertion count follows push assert and pop`() { + val profiler = profiler(StubSolver(ctx)) + + profiler.assert(ctx.mkTrue()) + profiler.push() + profiler.assert(listOf(ctx.mkTrue(), ctx.mkFalse())) + profiler.push() + profiler.assertAndTrack(ctx.mkTrue()) + profiler.pop(2u) + + val metadata = profiler.snapshot().events.map { it.metadata } + assertEquals(listOf(1L, 1L, 3L, 3L, 4L, 1L), metadata.map { it.activeAssertionCount }) + assertEquals(listOf(0, 1, 1, 2, 2, 0), metadata.map { it.stackDepth }) + assertEquals(4L, metadata.last().totalAssertionCount) + } + + @Test + fun `nested tasks restore the previous task even after an exception`() { + val profiler = profiler(StubSolver(ctx)) + val outer = KSolverTask("outer") + val inner = KSolverTask("inner") + + profiler.withTask(outer) { + push() + runCatching { + withTask(inner) { + push() + error("boom") + } + } + push() + } + profiler.push() + + val tasks = profiler.snapshot().events.map { it.metadata.task?.id } + assertEquals(listOf("outer", "inner", "outer", null), tasks) + } + + @Test + fun `assumption checks and tracked asserts are recorded`() { + val profiler = profiler(StubSolver(ctx)) + val assumption = ctx.mkTrue() + + profiler.assertAndTrack(ctx.mkTrue()) + val status = profiler.checkWithAssumptions(listOf(assumption)) + profiler.unsatCore() + + val events = profiler.snapshot().events + assertEquals(KSolverStatus.SAT, status) + assertEquals(true, assertIs(events[0]).tracked) + val check = assertIs(events[1]) + assertEquals(listOf(assumption), check.assumptions) + val access = assertIs(events[2]) + assertEquals(KSolverResultAccessKind.UNSAT_CORE, access.kind) + assertEquals(check.checkId, access.checkId) + } + + @Test + fun `result access before any check has no check id`() { + val profiler = profiler(StubSolver(ctx)) + + profiler.reasonOfUnknown() + + val access = assertIs(profiler.snapshot().events.single()) + assertNull(access.checkId) + } + + private fun profiler(delegate: KSolver) = + KRecordingSolverProfiler(delegate = delegate, solver = KSolverDescriptor("test")) + + private class TestConfiguration : KSolverConfiguration { + override fun setBoolParameter(param: String, value: Boolean) = Unit + override fun setIntParameter(param: String, value: Int) = Unit + override fun setStringParameter(param: String, value: String) = Unit + override fun setDoubleParameter(param: String, value: Double) = Unit + override fun optimizeForTheories(theories: Set?, quantifiersAllowed: Boolean) = Unit + } + + private open class StubSolver( + private val ctx: KContext, + private val closeFailure: Throwable? = null, + ) : KSolver { + override fun configure(configurator: TestConfiguration.() -> Unit) = TestConfiguration().configurator() + override fun assert(expr: KExpr) = Unit + override fun assertAndTrack(expr: KExpr) = Unit + override fun push() = Unit + override fun pop(n: UInt) = Unit + override fun check(timeout: Duration): KSolverStatus = KSolverStatus.SAT + + override fun checkWithAssumptions( + assumptions: List>, + timeout: Duration, + ): KSolverStatus = KSolverStatus.SAT + + override fun model(): KModel = KModelImpl(ctx, emptyMap(), emptyMap()) + override fun unsatCore(): List> = emptyList() + override fun reasonOfUnknown(): String = "stub" + override fun interrupt() = Unit + + override fun close() { + closeFailure?.let { throw it } + } + } + + /** A solver whose check blocks until it is interrupted. */ + private class BlockingCheckSolver(ctx: KContext) : StubSolver(ctx) { + val checkStarted = CountDownLatch(1) + private val interruptedLatch = CountDownLatch(1) + + @Volatile + var interrupted = false + + override fun check(timeout: Duration): KSolverStatus { + checkStarted.countDown() + interruptedLatch.await(5, TimeUnit.SECONDS) + return KSolverStatus.UNKNOWN + } + + override fun interrupt() { + interrupted = true + interruptedLatch.countDown() + } + } +} From 8cb7e05c5b38ee5b85775d1a2617349582437c8e Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Tue, 20 Oct 2026 23:06:00 +0300 Subject: [PATCH 4/9] Stop observed duration on close and narrow recording errors A repeated close keeps the closed state. Recording steps swallow only Exception, not Error. Add close and exception tests and restore SimpleProfilerTest. --- .../profiling/KRecordingSolverProfiler.kt | 57 +++++++++-- ...KRecordingSolverProfilerConcurrencyTest.kt | 46 ++++++++- .../io/ksmt/profiling/SimpleProfilerTest.kt | 95 +++++++++++++++++++ 3 files changed, 187 insertions(+), 11 deletions(-) create mode 100644 ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt index 4b491a765..4e6fba4ca 100644 --- a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt @@ -26,6 +26,12 @@ import kotlin.time.Duration.Companion.nanoseconds * - [interrupt] forwards to the delegate without waiting for the lock, so it can stop a check that * is running in another thread. Its event is numbered and stored after that check has finished. * - [snapshot] waits for a running solver call to finish. + * + * The observed duration stops growing once a [close] call has finished. A repeated [close] never + * turns a closed profile into a failed one. + * + * Recording problems ([Exception]s thrown while building or storing an event) are ignored and + * never change what the caller of the solver sees. */ @Suppress("LongParameterList") class KRecordingSolverProfiler( @@ -54,6 +60,7 @@ class KRecordingSolverProfiler( private var droppedEventCount = 0L private var lastSuccessfulCheckId: Long? = null private var state = KSolverProfileState.ACTIVE + private var closedAtNanos: Long? = null init { require(maxRecordedEvents > 0) { "Maximum recorded event count must be positive" } @@ -68,7 +75,7 @@ class KRecordingSolverProfiler( state = state, solver = solver.copy(attributes = solver.attributes.toMap()), startedAt = startedAt, - observedDuration = elapsedDuration(System.nanoTime()), + observedDuration = elapsedSinceStart(closedAtNanos ?: System.nanoTime()), initialConfiguration = initialConfiguration.copy(overrides = initialConfiguration.overrides.toMap()), eventLimit = maxRecordedEvents, @@ -151,6 +158,8 @@ class KRecordingSolverProfiler( } override fun check(timeout: Duration): KSolverStatus = synchronized(eventsLock) { + // The lock is entered again inside recordResultCall (allowed for the same thread). Taking it + // here makes checkId and the sequence number come from the same critical section. val checkId = nextCheckId++ recordResultCall( onSuccess = { lastSuccessfulCheckId = checkId }, @@ -230,8 +239,9 @@ class KRecordingSolverProfiler( val task = currentTaskSnapshot() val failure = runCatching { delegate.interrupt() }.exceptionOrNull() synchronized(eventsLock) { + // Unlike other calls, the number is assigned after the delegate call returns. val call = ProfiledCall(nextSequenceNumber++, startedAtNanos, task) - runCatching { + recordSafely { addEvent( KSolverLifecycleEvent( KSolverLifecycleEventKind.INTERRUPT, @@ -249,14 +259,26 @@ class KRecordingSolverProfiler( override fun close() { recordUnitCall( - onSuccess = { state = KSolverProfileState.CLOSED }, - onFailure = { state = KSolverProfileState.CLOSE_FAILED }, + onSuccess = { markClosed(KSolverProfileState.CLOSED) }, + onFailure = { markClosed(KSolverProfileState.CLOSE_FAILED) }, event = { metadata -> KSolverLifecycleEvent(KSolverLifecycleEventKind.CLOSE, metadata) }, ) { delegate.close() } } + /** + * A successful close always wins. A failed close only marks a session that is still active, + * so a later repeated close cannot turn [KSolverProfileState.CLOSED] into a failure. + * The observed duration stops at the first finished close. + */ + private fun markClosed(newState: KSolverProfileState) { + if (newState == KSolverProfileState.CLOSED || state == KSolverProfileState.ACTIVE) { + state = newState + } + if (closedAtNanos == null) closedAtNanos = System.nanoTime() + } + private fun addAssertions(count: Int) { val countAsLong = count.toLong() assertionCountsByScope[assertionCountsByScope.lastIndex] += countAsLong @@ -296,7 +318,7 @@ class KRecordingSolverProfiler( val result = try { block() } catch (error: Throwable) { - runCatching { + recordSafely { onFailure(error) addEvent( event( @@ -312,13 +334,29 @@ class KRecordingSolverProfiler( throw error } - runCatching { + recordSafely { onSuccess(result) addEvent(event(result, call.metadata(KSolverCallOutcome.SUCCESS))) } result } + /** + * Runs a recording step and drops its [Exception] so profiling never changes the outcome of + * a delegate call. [Error]s such as OutOfMemoryError are not recording problems and propagate. + */ + @Suppress("TooGenericExceptionCaught", "SwallowedException") + private inline fun recordSafely(step: () -> Unit) { + try { + step() + } catch (_: Exception) { + // Intentionally ignored, see the function documentation. + } + } + + /** + * Gives a number, remembers the start time and the current task + */ private fun beginCall(): ProfiledCall = ProfiledCall( sequenceNumber = nextSequenceNumber++, @@ -337,7 +375,7 @@ class KRecordingSolverProfiler( val finishedAtNanos = System.nanoTime() return KSolverCallMetadata( sequenceNumber = sequenceNumber, - startedAfterSession = elapsedDuration(startedAtNanos), + startedAfterSession = elapsedSinceStart(startedAtNanos), duration = (finishedAtNanos - startedAtNanos).coerceAtLeast(0).nanoseconds, outcome = outcome, task = task, @@ -349,8 +387,9 @@ class KRecordingSolverProfiler( ) } - private fun elapsedDuration(now: Long): Duration = - (now - startedAtNanos).coerceAtLeast(0).nanoseconds + /** Time between the profiler creation and [nowNanos], a value of [System.nanoTime]. */ + private fun elapsedSinceStart(nowNanos: Long): Duration = + (nowNanos - startedAtNanos).coerceAtLeast(0).nanoseconds private fun addEvent(event: KSolverProfileEvent) { if (events.size < maxRecordedEvents) { diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt index ae878a55d..ff7e9a864 100644 --- a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt @@ -17,6 +17,7 @@ import kotlin.test.assertEquals import kotlin.test.assertFailsWith import kotlin.test.assertIs import kotlin.test.assertNull +import kotlin.test.assertSame import kotlin.test.assertTrue import kotlin.time.Duration @@ -87,6 +88,43 @@ class KRecordingSolverProfilerConcurrencyTest { assertEquals(1L, interrupt.metadata.sequenceNumber) } + @Test + fun `observed duration stops growing after close`() { + val profiler = profiler(StubSolver(ctx)) + + profiler.close() + val first = profiler.snapshot().observedDuration + Thread.sleep(50) + val second = profiler.snapshot().observedDuration + + assertEquals(first, second) + } + + @Test + fun `second close keeps the closed state`() { + val profiler = profiler(StubSolver(ctx)) + + profiler.close() + profiler.close() + + val profile = profiler.snapshot() + assertEquals(KSolverProfileState.CLOSED, profile.state) + assertEquals(2, profile.events.size) + } + + @Test + fun `delegate exception is rethrown as the same object and recorded`() { + val failure = IllegalStateException("check failure") + val profiler = profiler(StubSolver(ctx, checkFailure = failure)) + + val actual = assertFailsWith { profiler.check() } + + assertSame(failure, actual) + val check = assertIs(profiler.snapshot().events.single()) + assertEquals(KSolverCallOutcome.FAILURE, check.metadata.outcome) + assertEquals(IllegalStateException::class.java.name, check.metadata.failureType) + } + @Test fun `failed close marks an active profile`() { val failure = IllegalStateException("close failure") @@ -123,7 +161,7 @@ class KRecordingSolverProfilerConcurrencyTest { profiler.withTask(outer) { push() - runCatching { + runCatching { withTask(inner) { push() error("boom") @@ -180,13 +218,17 @@ class KRecordingSolverProfilerConcurrencyTest { private open class StubSolver( private val ctx: KContext, private val closeFailure: Throwable? = null, + private val checkFailure: Throwable? = null, ) : KSolver { override fun configure(configurator: TestConfiguration.() -> Unit) = TestConfiguration().configurator() override fun assert(expr: KExpr) = Unit override fun assertAndTrack(expr: KExpr) = Unit override fun push() = Unit override fun pop(n: UInt) = Unit - override fun check(timeout: Duration): KSolverStatus = KSolverStatus.SAT + override fun check(timeout: Duration): KSolverStatus { + checkFailure?.let { throw it } + return KSolverStatus.SAT + } override fun checkWithAssumptions( assumptions: List>, diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt new file mode 100644 index 000000000..b397a904d --- /dev/null +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt @@ -0,0 +1,95 @@ +package io.ksmt.profiling + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KTheory +import io.ksmt.solver.model.KModelImpl +import io.ksmt.sort.KBoolSort +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.time.Duration + +class SimpleProfilerTest { + + @Test + fun `profile contains push assert check pop in call order`() { + val ctx = KContext() + + val fakeSolver = FakeSolver(ctx) + + val profiler = KRecordingSolverProfiler( + delegate = fakeSolver, + solver = KSolverDescriptor(name = "fake"), + ) + + val formula = ctx.mkTrue() + + profiler.push() + profiler.assert(formula) + val status = profiler.check() + profiler.pop() + + assertEquals(KSolverStatus.SAT, status) + + val profile = profiler.snapshot() + + assertEquals(4, profile.events.size) + + // The first event is push. + val push = assertIs(profile.events[0]) + assertEquals(0L, push.metadata.sequenceNumber) + assertEquals(1, push.metadata.stackDepth) + + // The second event is assert and it holds our formula. + val assertEvent = assertIs(profile.events[1]) + assertEquals(formula, assertEvent.expression) + assertEquals(1L, assertEvent.metadata.activeAssertionCount) + + // The third event is check and it holds the solver answer. + val check = assertIs(profile.events[2]) + assertEquals(KSolverStatus.SAT, check.status) + assertEquals(KSolverCallOutcome.SUCCESS, check.metadata.outcome) + + // The fourth event is pop: no scopes are left and the constraint is gone. + val pop = assertIs(profile.events[3]) + assertEquals(0, pop.metadata.stackDepth) + assertEquals(0L, pop.metadata.activeAssertionCount) + + // But one constraint was added during the whole session. + assertEquals(1L, pop.metadata.totalAssertionCount) + } + + // A minimal real KSolverConfiguration + private class FakeConfiguration : KSolverConfiguration { + override fun setBoolParameter(param: String, value: Boolean) = Unit + override fun setIntParameter(param: String, value: Int) = Unit + override fun setStringParameter(param: String, value: String) = Unit + override fun setDoubleParameter(param: String, value: Double) = Unit + override fun optimizeForTheories(theories: Set?, quantifiersAllowed: Boolean) = Unit + } + + // A fake solver: all methods are empty and check always returns SAT. + private class FakeSolver(private val ctx: KContext) : KSolver { + override fun configure(configurator: FakeConfiguration.() -> Unit) = FakeConfiguration().configurator() + override fun assert(expr: KExpr) = Unit + override fun assertAndTrack(expr: KExpr) = Unit + override fun push() = Unit + override fun pop(n: UInt) = Unit + override fun check(timeout: Duration): KSolverStatus = KSolverStatus.SAT + override fun checkWithAssumptions( + assumptions: List>, + timeout: Duration, + ): KSolverStatus = KSolverStatus.SAT + + override fun model(): KModel = KModelImpl(ctx, emptyMap(), emptyMap()) + override fun unsatCore(): List> = emptyList() + override fun reasonOfUnknown(): String = "" + override fun interrupt() = Unit + override fun close() = Unit + } +} From 6b6cc1bf9cd64dd677dc11199c13bc3de5ce64dc Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Wed, 21 Oct 2026 14:51:00 +0300 Subject: [PATCH 5/9] Extract assertion stack and event log from the recording profiler No behavior change. The helpers have no locks and stay guarded by the profiler lock. --- .../profiling/KRecordingSolverProfiler.kt | 119 ++++++++++++------ 1 file changed, 81 insertions(+), 38 deletions(-) diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt index 4e6fba4ca..3d2d53d53 100644 --- a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt @@ -50,14 +50,11 @@ class KRecordingSolverProfiler( private val eventsLock = Any() private val currentTask = ThreadLocal() - // Everything below is guarded by [eventsLock]. - private val events = arrayListOf() - private val assertionCountsByScope = arrayListOf(0L) + // Everything below is guarded by [eventsLock]. The helper objects have no locks of their own. + private val eventLog = EventLog(maxRecordedEvents) + private val assertionStack = AssertionStack() private var nextSequenceNumber = 0L private var nextCheckId = 0L - private var activeAssertionCount = 0L - private var totalAssertionCount = 0L - private var droppedEventCount = 0L private var lastSuccessfulCheckId: Long? = null private var state = KSolverProfileState.ACTIVE private var closedAtNanos: Long? = null @@ -79,8 +76,8 @@ class KRecordingSolverProfiler( initialConfiguration = initialConfiguration.copy(overrides = initialConfiguration.overrides.toMap()), eventLimit = maxRecordedEvents, - events = events.toList(), - droppedEventCount = droppedEventCount, + events = eventLog.toList(), + droppedEventCount = eventLog.droppedCount, attributes = profileAttributes.toMap(), ) } @@ -105,7 +102,7 @@ class KRecordingSolverProfiler( override fun assert(expr: KExpr) { recordUnitCall( - onSuccess = { addAssertions(1) }, + onSuccess = { assertionStack.add(1) }, event = { metadata -> KSolverAssertEvent(expr, tracked = false, metadata) }, ) { delegate.assert(expr) @@ -114,7 +111,7 @@ class KRecordingSolverProfiler( override fun assert(exprs: List>) { recordUnitCall( - onSuccess = { addAssertions(exprs.size) }, + onSuccess = { assertionStack.add(exprs.size) }, event = { metadata -> KSolverAssertBatchEvent(exprs.toList(), tracked = false, metadata) }, ) { delegate.assert(exprs) @@ -123,7 +120,7 @@ class KRecordingSolverProfiler( override fun assertAndTrack(expr: KExpr) { recordUnitCall( - onSuccess = { addAssertions(1) }, + onSuccess = { assertionStack.add(1) }, event = { metadata -> KSolverAssertEvent(expr, tracked = true, metadata) }, ) { delegate.assertAndTrack(expr) @@ -132,7 +129,7 @@ class KRecordingSolverProfiler( override fun assertAndTrack(exprs: List>) { recordUnitCall( - onSuccess = { addAssertions(exprs.size) }, + onSuccess = { assertionStack.add(exprs.size) }, event = { metadata -> KSolverAssertBatchEvent(exprs.toList(), tracked = true, metadata) }, ) { delegate.assertAndTrack(exprs) @@ -141,7 +138,7 @@ class KRecordingSolverProfiler( override fun push() { recordUnitCall( - onSuccess = { assertionCountsByScope.add(0L) }, + onSuccess = { assertionStack.push() }, event = { metadata -> KSolverPushEvent(metadata) }, ) { delegate.push() @@ -150,7 +147,7 @@ class KRecordingSolverProfiler( override fun pop(n: UInt) { recordUnitCall( - onSuccess = { removeScopes(n) }, + onSuccess = { assertionStack.pop(n) }, event = { metadata -> KSolverPopEvent(n, metadata) }, ) { delegate.pop(n) @@ -279,20 +276,6 @@ class KRecordingSolverProfiler( if (closedAtNanos == null) closedAtNanos = System.nanoTime() } - private fun addAssertions(count: Int) { - val countAsLong = count.toLong() - assertionCountsByScope[assertionCountsByScope.lastIndex] += countAsLong - activeAssertionCount += countAsLong - totalAssertionCount += countAsLong - } - - private fun removeScopes(n: UInt) { - val removedScopeCount = minOf(n.toLong(), assertionCountsByScope.lastIndex.toLong()).toInt() - repeat(removedScopeCount) { - activeAssertionCount -= assertionCountsByScope.removeAt(assertionCountsByScope.lastIndex) - } - } - private inline fun recordUnitCall( crossinline onSuccess: () -> Unit = {}, crossinline onFailure: (Throwable) -> Unit = {}, @@ -379,9 +362,9 @@ class KRecordingSolverProfiler( duration = (finishedAtNanos - startedAtNanos).coerceAtLeast(0).nanoseconds, outcome = outcome, task = task, - stackDepth = assertionCountsByScope.lastIndex, - activeAssertionCount = activeAssertionCount, - totalAssertionCount = totalAssertionCount, + stackDepth = assertionStack.depth, + activeAssertionCount = assertionStack.active, + totalAssertionCount = assertionStack.total, failureType = failureType, failureMessage = failureMessage, ) @@ -391,13 +374,7 @@ class KRecordingSolverProfiler( private fun elapsedSinceStart(nowNanos: Long): Duration = (nowNanos - startedAtNanos).coerceAtLeast(0).nanoseconds - private fun addEvent(event: KSolverProfileEvent) { - if (events.size < maxRecordedEvents) { - events += event - } else { - droppedEventCount++ - } - } + private fun addEvent(event: KSolverProfileEvent) = eventLog.add(event) private data class ProfiledCall( val sequenceNumber: Long, @@ -405,6 +382,72 @@ class KRecordingSolverProfiler( val task: KSolverTask?, ) + /** + * Bounded list of events. Once [limit] events are stored, later events are only counted, + * so the stored events are always an exact prefix of the call history. + * Not thread-safe: the owner guards it with its own lock. + */ + private class EventLog(private val limit: Int) { + private val events = arrayListOf() + + /** Number of events that did not fit into the limit. */ + var droppedCount = 0L + private set + + fun add(event: KSolverProfileEvent) { + if (events.size < limit) { + events += event + } else { + droppedCount++ + } + } + + /** Returns a copy, so later [add] calls do not change it. */ + fun toList(): List = events.toList() + } + + /** + * Assertion counters that mirror the push/pop stack of the solver. + * + * The first element of [countsByScope] belongs to the base level, so [depth] is the number of + * open scopes. [active] always equals the sum of [countsByScope]. [total] only grows. + * Not thread-safe: the owner guards it with its own lock. + */ + private class AssertionStack { + private val countsByScope = arrayListOf(0L) + + /** Number of open scopes (zero when only the base level exists). */ + val depth: Int get() = countsByScope.lastIndex + + /** Assertions that are still in effect. */ + var active = 0L + private set + + /** Assertions added since the session started, including already removed ones. */ + var total = 0L + private set + + fun push() { + countsByScope += 0L + } + + /** Counts [count] assertions in the innermost scope. */ + fun add(count: Int) { + val countAsLong = count.toLong() + countsByScope[countsByScope.lastIndex] += countAsLong + active += countAsLong + total += countAsLong + } + + /** Removes up to [n] scopes; the base level is never removed. */ + fun pop(n: UInt) { + val removedScopeCount = minOf(n.toLong(), countsByScope.lastIndex.toLong()).toInt() + repeat(removedScopeCount) { + active -= countsByScope.removeAt(countsByScope.lastIndex) + } + } + } + companion object { const val DEFAULT_MAX_RECORDED_EVENTS = 1_000_000 } From 000e14692f59a62c58bfcc4addc59c74eae1207f Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Wed, 21 Oct 2026 15:48:00 +0300 Subject: [PATCH 6/9] Document opaque configure events and test them --- .../ksmt/profiling/KRecordingSolverProfiler.kt | 7 +++++++ .../io/ksmt/profiling/SimpleProfilerTest.kt | 17 +++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt index 3d2d53d53..9b9908e67 100644 --- a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt @@ -92,6 +92,13 @@ class KRecordingSolverProfiler( } } + /** + * Forwards the configuration change and records it as an opaque event (`overrides = null`): + * the [configurator] lambda cannot be inspected without a solver-specific wrapper. + * + * Options that must be visible to profile consumers (for example the ones applied to a fresh + * solver before any assertion) belong to [initialConfiguration]. + */ override fun configure(configurator: Config.() -> Unit) { recordUnitCall( event = { metadata -> KSolverConfigureEvent(overrides = null, metadata) }, diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt index b397a904d..b0e79e9ed 100644 --- a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/SimpleProfilerTest.kt @@ -63,6 +63,23 @@ class SimpleProfilerTest { // But one constraint was added during the whole session. assertEquals(1L, pop.metadata.totalAssertionCount) } + @Test + fun `configure is forwarded and recorded as opaque event`() { + val profiler = KRecordingSolverProfiler( + delegate = FakeSolver(KContext()), + solver = KSolverDescriptor(name = "fake"), + ) + var configuratorCalled = false + + profiler.configure { configuratorCalled = true } + + assertEquals(true, configuratorCalled) + val event = assertIs(profiler.snapshot().events.single()) + assertEquals(null, event.overrides) + assertEquals(KSolverCallOutcome.SUCCESS, event.metadata.outcome) + } + + // A minimal real KSolverConfiguration private class FakeConfiguration : KSolverConfiguration { From 3d43b85783ccec991ae3bedc3a0cdb1126f89874 Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Thu, 22 Oct 2026 22:05:59 +0300 Subject: [PATCH 7/9] Add opt-in profiler overhead benchmark on cvc5 --- ksmt-profiling/build.gradle.kts | 4 + .../profiling/ProfilerOverheadBenchmark.kt | 144 ++++++++++++++++++ 2 files changed, 148 insertions(+) create mode 100644 ksmt-profiling/src/test/kotlin/io/ksmt/profiling/ProfilerOverheadBenchmark.kt diff --git a/ksmt-profiling/build.gradle.kts b/ksmt-profiling/build.gradle.kts index 64f9a945e..fe816be7e 100644 --- a/ksmt-profiling/build.gradle.kts +++ b/ksmt-profiling/build.gradle.kts @@ -4,6 +4,10 @@ plugins { dependencies { api(project(":ksmt-core")) + + // cvc5 is the primary real solver; it is used only by the opt-in overhead benchmark. + testImplementation(project(":ksmt-cvc5:ksmt-cvc5-core")) + testImplementation(project(":ksmt-cvc5:ksmt-cvc5-native")) } publishing { diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/ProfilerOverheadBenchmark.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/ProfilerOverheadBenchmark.kt new file mode 100644 index 000000000..245fb51d0 --- /dev/null +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/ProfilerOverheadBenchmark.kt @@ -0,0 +1,144 @@ +package io.ksmt.profiling + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.cvc5.KCvc5Solver +import io.ksmt.sort.KBoolSort +import io.ksmt.utils.mkConst +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.condition.EnabledIfEnvironmentVariable +import java.util.Locale +import kotlin.math.sqrt + +/** + * Opt-in measurement of the profiler overhead on a real cvc5 solver. It is skipped by default; + * run it with the environment variable `KSMT_PROFILING_BENCHMARK=true`, for example: + * `$env:KSMT_PROFILING_BENCHMARK='true'; gradlew :ksmt-profiling:test --tests "*ProfilerOverheadBenchmark*" -i` + * + * The results are printed to the console. The numbers are synthetic and are not a replacement + * for measurements on a real workload. + */ +@EnabledIfEnvironmentVariable(named = "KSMT_PROFILING_BENCHMARK", matches = "true") +class ProfilerOverheadBenchmark { + + @Test + fun `time overhead on incremental workloads`() { + println("=== Time overhead (cvc5, ms per run; lower is better) ===") + report("light: push/assert/pop x$LIGHT_CYCLES", withCheck = false, cycles = LIGHT_CYCLES) + report("heavier: push/assert/check/pop x$CHECK_CYCLES", withCheck = true, cycles = CHECK_CYCLES) + } + + @Test + fun `memory held by recorded events`() { + println("=== Memory held by the event log (shared formulas, cvc5) ===") + for (cycles in listOf(10_000, 100_000)) { + val ctx = KContext() + val formula = ctx.boolSort.mkConst("b") + val profiler = profiled(ctx, maxEvents = Int.MAX_VALUE) + val before = usedMemory() + runWorkload(profiler, formula, formula, cycles, withCheck = false) + val snapshot = profiler.snapshot() + val after = usedMemory() + val perEvent = (after - before).toDouble() / snapshot.events.size + println( + String.format( + Locale.ROOT, "events=%d, retained=%.1f MB, ~%.0f bytes/event (includes the snapshot copy)", + snapshot.events.size, (after - before) / MEGABYTE, perEvent, + ), + ) + profiler.close() + check(snapshot.events.isNotEmpty()) + } + } + + private fun report(title: String, withCheck: Boolean, cycles: Int) { + val bare = measure { ctx, formula, assumption -> runWorkload(KCvc5Solver(ctx), formula, assumption, cycles, withCheck) } + val recorded = measure { ctx, formula, assumption -> + runWorkload(profiled(ctx, maxEvents = 1_000_000), formula, assumption, cycles, withCheck) + } + val limited = measure { ctx, formula, assumption -> + runWorkload(profiled(ctx, maxEvents = 10), formula, assumption, cycles, withCheck) + } + println(title) + println(" bare ${bare.format()}") + println(" profiled ${recorded.format()} (x${ratio(recorded, bare)})") + println(" profiled, limit 10 ${limited.format()} (x${ratio(limited, bare)})") + } + + private fun ratio(a: Stats, b: Stats): String = String.format(Locale.ROOT, "%.2f", a.median / b.median) + + private fun profiled(ctx: KContext, maxEvents: Int): KRecordingSolverProfiler<*> = + KRecordingSolverProfiler( + delegate = KCvc5Solver(ctx), + solver = KSolverDescriptor(name = "cvc5"), + maxRecordedEvents = maxEvents, + ) + + private fun measure(run: (KContext, KExpr, KExpr) -> Unit): Stats { + val samples = ArrayList() + repeat(WARMUP + RUNS) { index -> + val ctx = KContext() + val formula = ctx.boolSort.mkConst("a") + val assumption = ctx.boolSort.mkConst("b") + val start = System.nanoTime() + run(ctx, formula, assumption) + if (index >= WARMUP) samples += (System.nanoTime() - start) / NANOS_PER_MILLI + } + return Stats.of(samples) + } + + private fun runWorkload( + solver: KSolver, + formula: KExpr, + other: KExpr, + cycles: Int, + withCheck: Boolean, + ) { + solver.use { + solver.assert(formula) + repeat(cycles) { + solver.push() + solver.assert(other) + if (withCheck) solver.check() + solver.pop() + } + } + } + + private fun usedMemory(): Long { + repeat(GC_ROUNDS) { System.gc() } + val runtime = Runtime.getRuntime() + return runtime.totalMemory() - runtime.freeMemory() + } + + private class Stats(val median: Double, val mean: Double, val stdDev: Double) { + fun format(): String = + String.format(Locale.ROOT, "median=%8.2f mean=%8.2f stdDev=%7.2f", median, mean, stdDev) + + companion object { + fun of(samples: List): Stats { + val sorted = samples.sorted() + val mean = sorted.average() + val variance = if (sorted.size > 1) sorted.sumOf { (it - mean) * (it - mean) } / (sorted.size - 1) else 0.0 + val median = if (sorted.size % 2 == 1) { + sorted[sorted.size / 2] + } else { + (sorted[sorted.size / 2 - 1] + sorted[sorted.size / 2]) / 2 + } + return Stats(median, mean, sqrt(variance)) + } + } + } + + private companion object { + const val LIGHT_CYCLES = 20_000 + const val CHECK_CYCLES = 2_000 + const val WARMUP = 3 + const val RUNS = 7 + const val GC_ROUNDS = 3 + const val NANOS_PER_MILLI = 1_000_000.0 + const val MEGABYTE = 1024.0 * 1024.0 + } +} From bcc31b2af1601257fd9c313cbe554fb4d2b16501 Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Thu, 22 Oct 2026 22:18:57 +0300 Subject: [PATCH 8/9] Keep result accesses linked to the last check across assert and pop --- .../ksmt/profiling/KRecordingSolverProfiler.kt | 3 +++ .../KRecordingSolverProfilerConcurrencyTest.kt | 17 +++++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt index 9b9908e67..32f2112f9 100644 --- a/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt +++ b/ksmt-profiling/src/main/kotlin/io/ksmt/profiling/KRecordingSolverProfiler.kt @@ -55,6 +55,9 @@ class KRecordingSolverProfiler( private val assertionStack = AssertionStack() private var nextSequenceNumber = 0L private var nextCheckId = 0L + + // Deliberately not reset by assert/push/pop: backends such as cvc5 keep the previous result + // readable until the next check, so result accesses stay linked to the last successful check. private var lastSuccessfulCheckId: Long? = null private var state = KSolverProfileState.ACTIVE private var closedAtNanos: Long? = null diff --git a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt index ff7e9a864..13f8ac8d1 100644 --- a/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt +++ b/ksmt-profiling/src/test/kotlin/io/ksmt/profiling/KRecordingSolverProfilerConcurrencyTest.kt @@ -203,6 +203,23 @@ class KRecordingSolverProfilerConcurrencyTest { val access = assertIs(profiler.snapshot().events.single()) assertNull(access.checkId) } + @Test + fun `result access after assert and pop stays linked to the last successful check`() { + val profiler = profiler(StubSolver(ctx)) + + profiler.push() + profiler.check() + profiler.assert(ctx.mkTrue()) + profiler.pop(1u) + profiler.reasonOfUnknown() + + val events = profiler.snapshot().events + val check = events.filterIsInstance().single() + val access = events.filterIsInstance().single() + assertEquals(check.checkId, access.checkId) + } + + private fun profiler(delegate: KSolver) = KRecordingSolverProfiler(delegate = delegate, solver = KSolverDescriptor("test")) From 7754e7430bd5f82a87adf34b57142743871961d0 Mon Sep 17 00:00:00 2001 From: Daniil Varezkin Date: Thu, 22 Oct 2026 23:13:15 +0300 Subject: [PATCH 9/9] Add ksmt-profiling README with build and run instructions --- ksmt-profiling/README.md | 115 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 ksmt-profiling/README.md diff --git a/ksmt-profiling/README.md b/ksmt-profiling/README.md new file mode 100644 index 000000000..3bd78e624 --- /dev/null +++ b/ksmt-profiling/README.md @@ -0,0 +1,115 @@ +# ksmt-profiling + +Solver-agnostic profiling for KSMT. The module records the chronology of calls made to a +`KSolver` (`configure`, `assert`, `push`, `pop`, `check`, `model`, `unsatCore`, ...) and exposes it +as an immutable `KSolverProfile`. + +`KRecordingSolverProfiler` is the implementation. It wraps any `KSolver` and does not depend on a +specific solver. cvc5 is the primary target. + +## Requirements + +- JDK 17 (the version the module was built and tested with). +- No separate Gradle installation: use the `gradlew` wrapper from the repository root. +- Internet access on the first build to download dependencies. +- No cvc5 build is needed. The cvc5 jar and native libraries are stored in `ksmt-cvc5/dist`. + See [`ksmt-cvc5/dist/build.md`](../ksmt-cvc5/dist/build.md) for their origin. + +Make sure `JAVA_HOME` points to JDK 17. Run all commands from the repository root. + +| OS | Wrapper | +| --- | --- | +| Linux / macOS | `./gradlew` | +| Windows (PowerShell) | `.\gradlew.bat` | + +The examples below use `./gradlew`. + +## Build and test + +```bash +# Compile the module +./gradlew :ksmt-profiling:build + +# Unit tests and static analysis +./gradlew :ksmt-profiling:test :ksmt-profiling:detekt +``` + +Expected result: `BUILD SUCCESSFUL`, 20 unit tests pass, 2 benchmark tests are skipped. + +Test reports are written to `ksmt-profiling/build/test-results/test/`. If Gradle reports +`UP-TO-DATE` and does not run the tests again, add `:ksmt-profiling:cleanTest` before +`:ksmt-profiling:test`. + +## Usage + +```kotlin +val solver = KCvc5Solver(ctx) +val profiler = KRecordingSolverProfiler( + delegate = solver, + solver = KSolverDescriptor(name = "cvc5"), + maxRecordedEvents = 1_000_000, +) + +profiler.push() +profiler.assert(formula) +profiler.check() +profiler.pop(1u) + +val profile = profiler.snapshot() // immutable chronology of the calls +profiler.close() +``` + +Use the profiler as a regular `KSolver`. Notes: + +- Exceptions thrown by the wrapped solver are rethrown as the same object and are recorded in the + profile. +- `configure` is recorded as an opaque event (`overrides = null`) because the contents of the + lambda cannot be inspected. Options that must be visible in the profile should be passed through + `KSolverProfilerRequest.initialConfiguration`. +- Events are stored in strict order. When `maxRecordedEvents` is reached, the profile keeps the + first events and reports that it was truncated. +- `interrupt()` can be called from another thread while `check` is running. +- `model`, `unsatCore` and `reasonOfUnknown` accesses are linked to the last successful check. + +## Overhead benchmark + +`ProfilerOverheadBenchmark` compares a bare cvc5 solver with the same solver under the profiler +and estimates memory per recorded event. It is **disabled by default** so that it does not slow +down regular test runs. Enable it with the environment variable `KSMT_PROFILING_BENCHMARK=true`. + +```bash +# Linux / macOS +KSMT_PROFILING_BENCHMARK=true ./gradlew :ksmt-profiling:cleanTest :ksmt-profiling:test \ + --tests "*ProfilerOverheadBenchmark*" +``` + +```powershell +# Windows (PowerShell) +$env:KSMT_PROFILING_BENCHMARK = 'true' +.\gradlew.bat :ksmt-profiling:cleanTest :ksmt-profiling:test --tests "*ProfilerOverheadBenchmark*" +Remove-Item Env:KSMT_PROFILING_BENCHMARK # do not leave it enabled +``` + +Gradle does not print the test output by default. Add `-i` or read the `system-out` section of +`ksmt-profiling/build/test-results/test/TEST-io.ksmt.profiling.ProfilerOverheadBenchmark.xml`. + +Reference numbers from one development machine (synthetic workload on cvc5, median of 7 runs): + +| Workload | Without profiler | With profiler | +| --- | --- | --- | +| 20 000 x `push/assert/pop` | 41.9 ms | 51.1 ms (x1.22) | +| 2 000 x `push/assert/check/pop` | 94.6 ms | 109.1 ms (x1.15, high variance) | + +Memory: about 100 bytes per recorded event. Absolute numbers depend on the machine, so compare the +two configurations only within a single run. The workload is synthetic and does not replace a +measurement on real TSA workloads. + +## Known limitations + +- The overhead was not measured on real TSA workloads or with several threads. +- Serialization of `KSolverProfile` is outside of KSMT. + +## Troubleshooting + +- **Gradle fails with a Java version error.** Check `JAVA_HOME` and `java -version`: JDK 17. +- **The benchmark runs on every test run.** `KSMT_PROFILING_BENCHMARK` is still set in your shell.