Repository navigation
Reduce executor per-round CPU (CDS archive, HttpURLConnection, no redundant class re-parse/check) - #96
Merged
Conversation
Records wall clock, thread and process CPU time at the phase boundaries of one executor run (agent init, premain, execution start/end, trace serialization, trace transfer, shutdown), class-load/instrumentation counters and the CPU time per JVM thread. Off unless the property is set. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
java.lang.instrument treats any non-null return value as a transformed class, so returning the unchanged input buffer made the JVM parse every class loaded after premain from its bytes again, also the JDK classes it would otherwise map from the CDS archive (about 1000 per executor run). The class bytes are the same as before. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Creating a java.net.http.HttpClient initialises an SSL context (reading the CA certificates), a selector thread and an executor and loads about 200 classes, which cost a large part of a short executor run's CPU time although the request is plain HTTP to localhost. Same request (POST, JSON body, Content-Type application/json) and same output line. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Every round starts a new executor JVM that loads, parses and verifies the same ~3000 classes (agent jar, JDK classes outside the default CDS archive). Round 0 now records the loaded classes, the archive is dumped before round 3 (about 1.6 s CPU, so short runs do not pay for it) and later rounds map the classes from it: about 0.26 s less CPU per round on MinePump (0.95 -> 0.69 s). CDS archives classes from leading jar entries of the class path only, so the class path gets a prefix of its jars plus the agent jar; this is done only if no file of a moved jar also exists in an entry before it, so every name resolves to the same file as before. Transformed classes are still parsed from the transformed bytes. Any failure falls back to running without the archive; --no-executor-cds turns it off. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ieval Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… is set Four transformers always wrote the instrumented class through CheckClassAdapter with data-flow checks, whatever the config said; only the separate verify step honoured instrumentation.checkClassAdapter. The checks only catch instrumentation bugs and cost about 0.06 s CPU per executor run. The writer is now wrapped under the same condition as the verify step (instrumentation.checkClassAdapter, default false, and instrumentation.checkClassAdapterClass). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
Author
|
Full campaign: 1713 SV-COMP jobs (300 s CPU, no SA, sv-comp.cfg, 15 GB / -Xmx12g), dev 209cc0e and
Attribution: the 20 runs that changed were re-run with each change switched off ( This PR: no verdict changes (with AppCDS: 128 runs left a 🤖 Generated with Claude Code |
This was referenced Oct 21, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Reduces the fixed CPU cost of each executor round (one JVM start per explored path) in sv-comp mode.
Changes
nullfor classes they do not change. java.lang.instrument treats any non-null return as "transformed", so the JVM re-parsed every class loaded afterpremain(incl. ~1000 JDK classes otherwise taken from CDS).HttpURLConnectioninstead ofHttpClient.HttpClient.newHttpClient()sets up a default SSLContext, a selector thread and ~200 classes (~0.2 s per round) for a plain-HTTP POST. Same request, same output.symbolic-explorer/svcomp/ExecutorCDS.py): round 0 writes a class list (-XX:DumpLoadedClassList), before round 3 the explorer runs a staticjava -Xshare:dump(no agent involved, ~1.5 s CPU), rounds >= 3 start with-XX:SharedArchiveFile. Runs with <= 3 rounds pay nothing; break-even is ~6 rounds.<jars of the cp> : <agent jar> : <original cp>because CDS refuses directory entries. This is only done if no moved jar's file name shadows an earlier entry, so every class/resource resolves to the same file; otherwise CDS is off for the run.java.class.pathdiffers as a side effect.-Xshare:auto).--no-executor-cds.<logdir>/swat-cds-*/and deleted at the end of a normal run (a killed run leaves it behind). If the log dir is on tmpfs it counts against the memory limit.-XX:ArchiveClassesAtExit) is not usable with a Java agent on JDK 17 (needs a diagnostic flag and crashes at dump).-Xshare:dumpis a standard JDK 17 feature.instrumentation.checkClassAdapteris set. Four transformers always wrote throughnew CheckClassAdapter(cw, true)(visit checks + data-flow analysis of every method), ignoring the flag that sv-comp.cfg sets to false. Behaviour differs only for invalid instrumented code, which is then no longer rejected while written (it hits the JVM verifier or ASM frame computation instead). NewCheckClassAdapterSwitchSpec.-Dswat.profile=<file>(de.uzl.its.swat.common.Profile; off = one static boolean check).Measured
CPU per round (user+sys of the JVM, 2 pinned cores, sv-comp.cfg,
-Xmx12g, stub explorer):(Last three rows measured before the CheckClassAdapter commit.) Rounds completed within 300 s CPU on 8 timeout tasks: +31% to +75%.
Verdicts: 64 non-timeout tasks from 15 families: 63/64 identical to dev (the other is a wall-timeout on both). 20 further tasks after the CheckClassAdapter change: 20/20 identical. Explorer unit tests pass; executor
test(common.*,instrument.*) andagentTestpass.Full-campaign numbers follow in a comment.
🤖 Generated with Claude Code