Repository navigation
Single-source the submission scaffold and align docs with the build - #76
Merged
Merged
Conversation
The scheduler spec and its absent-key config described pre-fix absent-key behaviour in the present tense, directly above the negative control that deliberately reproduces that behaviour — narration a maintainer could act on and destroy the control. Those claims are now past tense with the control named, matching the harness's own voice. Spec comments also carried three wrong mappings (retryMap is keyed by TxnId, not footprint; sweeps have three slots, not two; the park-time recheck is anyReadChangedSinceRead) and four fix-date parentheticals whose H-identifiers already carry the meaning. In the sources: repointed a dangling short-circuit rationale at the deleted aggregate dirty check, documented extractMap's structure-entry gate at its consumption site, corrected the @nowarn header (setter arms never cast — their match refines V = Unit), rewrote TxnVarMap's registration-timing note to match all three real paths, and stopped the scaladoc advertising `import stm._` as equivalent to `syntax.all._` (the F-variants exist only in the latter). syntax.all's commit and handleErrorWith now carry the full cancellation/retry contract users hover in an IDE. Removed an identity re-tupling in the two txnLog map-read arms: it read as a load-bearing GADT coercion but cross-compiles clean without it on both Scala versions. Test comments: dropped a copy-pasted value annotation, corrected a reader count, stripped process history from the TxnLogDirtySpec header while keeping its H1 pin, documented the soak's tag-offset constraint, fixed a debugging checklist's location pointer, and dropped the H6 co-label from a G2 calibration case (H6's demonstrated shape is G-single). Docs: linked SECURITY.md from README and CONTRIBUTING, repaired the README intro's garbled relative clause, fixed a rounding slip (+21.9%), updated the crossMapInsert comment to point at its published baseline, replaced QUALITY.md's dead artifact paths, and appended the current quality summary to QUALITY.md.
Two byte-identical overrides in TxnLogValid (raiseError, pure) shadowed their base defaults and invited silent divergence; the base raiseError is now the single implementation, its comment recast as the live error short-circuit it actually is. A single-use TxnResultFailure companion overload, an unreachable erratum match arm (TxnErratum is sealed and both cases are handled), a dead TLA+ operator (IsRetryTxn), and a dead oracle constant (InitTxn) are deleted outright. The fiber-per-trivial-op traversals follow the idFootprint precedent already measured in this file: whole-map reads and writes, the park-time staleness fold, the retry-queue wakes and removals, and the unsub cascade now traverse sequentially — every per-element effect is a non-blocking Ref/TrieMap access or a .start that spawns its own fiber, so ordering is unobservable and the fiber-spawn overhead goes. subscribeDownstreamDependency stops materializing the whole key set to answer one membership test. Safe upcasts written as asInstanceOf are now ascriptions, so the remaining casts all mark genuinely unchecked coercions. IdFootprint gains readOnly/writeOnly factories, replacing six positional literals whose read/write slots a typo could swap silently. Smaller idiom fixes: StateT.pure for hand-rolled pure StateT bodies, a shortCircuit helper for the duplicated analysis-pass handler, NoStackTrace on the short-circuit control-flow exception (matching its sibling), explicit tuples where auto-tupling was relied on, case-form destructuring, def over lazy val for constructor-field getters, and final on the top-level and object-nested case classes. final was reverted on the 11 trait-nested ADT cases: Scala 2.13's -Xlint outer-reference check rejects it there, fatal under -Werror. The benchmark keyspace is now derived (2 * Batch) instead of a silent 64 whose coupling to WindowB an edit to Batch alone would break. One duplicate test deleted (identical body, unobserved message string): the suite goes 269 -> 268 intentionally.
The two scheduler submit paths duplicated the load-bearing registration sequence; registerAndSweep now holds it once, so the TLA+-walked order (scan before self-insert, edges complete before the readiness test) is shared by construction and the paths differ only in how they direct an edge to an incompatible peer. Two protocol pins cover what no public API observes: the resubmission path's anti-starvation edge reversal, and commit failure on ADT cases the interpreters do not handle — their defaults now raise instead of silently no-oping, closing the unrecorded-footprint hole an unsealed TxnAdt leaves open. TxnLogValid walks its entries once per question instead of re-listing the map each time, commits sequentially per the measured idFootprint precedent, and raises its control-flow aborts as a dedicated NoStackTrace type. The API layer's pure setters and modifiers delegate to their F-variants, the compiler walkers collapse the triple-cloned keyed-write analysis into one helper, and TxnStateEntity drops the value member nothing used. CONTRIBUTING now names the variable that actually keys fatal warnings (GITHUB_ACTIONS, not CI — CI=true green-lights builds real CI fails), specs/README's writeSeq row states the owner order the code sorts by, and the benchmark tables carry the drift and mixed-protocol annotations their own methodology demands.
The comment claimed every write commit is a Ref.set or a locked map mutation, but the map-structure write entry is a reachable third case: it contributes a lock and a footprint id while committing as unit, because the per-key entries built alongside it carry the real writes.
QUALITY.md and .quality-accepted.jsonl are working logs of the review process, not project documentation — nothing in the repository, the docs, or CI references either. They stay as local files the tooling appends to; the repo front door keeps only the conventional OSS surface.
5 tasks done
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.
Summary
registerAndSweep) so both scheduler submit paths walk the TLA+-verified registration sequence by construction, differing only in edge direction; the fiber-per-peer scan becomes a sequential traverse (invisible to peers under the graph semaphore)ResubmissionEdgeSpec(the dirty path's anti-starvation edge reversal) andUnhandledAdtSpec(rogue-case commit failure)entriesval, two-set footprint fold, sequential per-entry commit per the measured precedent),NoStackTracecontrol-flow aborts, API-layer pure/F delegation, keyed-write analysis deduplication, and thewithRuntimeSynctest-harness consolidationGITHUB_ACTIONS, notCI), specs/README'swriteSeqrow states the owner order the code sorts by, benchmark tables carry drift and mixed-protocol annotations, README figures single-source to benchmarks/READMENo protocol behaviour changes: the scaffold extraction preserves the spec-walked ordering (scan before self-insert, edges complete before the readiness test), and the full spec suite holds — 12 pinned TLC expectations, 17 verified anchors, all 10 negative-control patches apply.
Test plan
GITHUB_ACTIONS=true sbt scalafmtCheckAll scalafmtSbtCheck headerCheckAll 'scalafixAll --check' +test— 271/271 both compilers, fatal warnings onmimaReportBinaryIssues,doc,benchmarks/Jmh/compile./specs/verify_anchors.sh(17 mapped),./specs/expectations.sh --list(12 declared)