Repository navigation
Execute the architecture review: allocator seam, one syntax surface, sealed ADT - #77
Merged
Merged
Conversation
TxnVar.of and TxnVarMap.of demanded a full STM[F] runtime to bump one counter, while STM.scala imports the model back — a package cycle that made two data types compile-depend on the whole cake. TxnIdAllocator now names the one capability they actually use; STM[F] extends it, so every existing caller resolves unchanged by subtyping, and the member is private[stm], so no allocator can exist outside the library. TxnVarMap holds the capability for its lifetime rather than taking it at construction: getRuntimeId mints existential key ids at run time, and those must come from the same global counter that numbers the entities, or key ids could alias entity ids in the footprint algebra. TxnIdAllocatorSpec pins the seam from both sides: the model builds against a stub counter with no scheduler standing up, and the ids so minted stay distinct across kinds, stable per key, and parented by their map.
Every transaction verb existed twice: once in the syntax package and once as implicit classes inside STM[F], reachable only via import stm._ on an instance. The inner copies were a strict subset — no setF/modifyF/handleErrorWithF — and the two surfaces had already drifted once, which is the maintenance shape that produced the drift in the first place. One definition per operation now. The sole consumer in the repository was one white-box test line, which now calls the private[stm] constructors it already lives amongst.
TxnAdt was an unsealed trait in its own file while its twelve cases lived path-dependent inside TxnAdtContext — so a case the interpreters had no arm for compiled clean anywhere in the library. The trait now sits sealed at the top of the file its cases live in: a rogue case is a compile error, which retires UnhandledAdtSpec (its rogue no longer compiles — the property it pinned is enforced by the compiler). The raising defaults stay. The exhaustiveness checker cannot verify matches over path-dependent case members — with the defaults dropped it rejects both walkers, listing all twelve arms as missing — so the default provides the totality the checker cannot see and turns a future in-file case without interpreter arms into a failed commit rather than a silently skipped operation. The interpreter file's blanket @nowarn annotations narrow to the three unit-cast expressions they were always for, so nothing broader is suppressed.
The implementation model — free monad, two interpreters, footprint scheduling, the commit protocol, two id spaces — lived scattered across one README bullet, the STM scaladoc, and the middle of a 735-line verification document. docs/architecture.md now narrates the moving parts in the order a transaction moves through them, linking to specs/README.md for every proof rather than restating verdicts, so it adds no second source of truth to drift.
Two documents and an archive justify a front door; one archived plan did not.
The review's negative-compilation probe for a home-made TxnIdAllocator failed, and chasing the failure found two real things. First, scalatest's assertTypeError never runs refchecks, so "object creation impossible" — the error the trait design leaned on — is invisible to it. Second, and worse, the trait was genuinely forgeable: a usercode anonymous subclass with a same-named val satisfies an invisible private[stm] abstract member, instantiates, and mints entity ids from its own counter — proved live before the fix. Aliased ids across counters are exactly how conflict detection silently breaks. TxnIdAllocator is now an abstract class whose constructor is private to the library, riding into STM through AsyncImplicits (the one superclass slot). Constructor access is checked at the subclassing site, at typer — outside implementation is a compile error the probes can see, and three of them now pin it, including the exact forgery shape. Also from the review round: the architecture doc no longer claims an in-file armless ADT case is a compile error (it is a loudly failed commit — the exhaustiveness checker cannot verify path-dependent matches), the CHANGELOG and the sealed-hierarchy comment name the ADT's own file rather than "alongside the interpreters", the interpreter section distinguishes fresh submissions (both walks) from re-runs (log walk only), and the README operations table carries the current factory signatures.
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
1 participant
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.
Stacked on #76 — review that first; GitHub retargets this to main when #76 merges and its branch is deleted. Binary-breaking items ride the open 0.15 window (MiMa is vacuous until the first 0.15.x tag; do not tag v0.15.0 before both PRs merge).
Summary
TxnVar.of/TxnVarMap.ofbound on a newTxnIdAllocator[F]capability instead of the fullSTM[F]cake (anSTM[F]is one, so user code resolves unchanged). The map holds the capability for its lifetime — its key-registry mints ids at run time.TxnIdAllocatorSpecpins the model building against a stub with no scheduler.valsatisfies an invisibleprivate[stm]abstract member and minted entity ids from a user counter (proved before the fix; aliased ids silently break conflict detection). It is now an abstract class with a library-private constructor, and threePublicApiSpecprobes pin the seal, including the exact forgery shape.STM[F]inner ops classes are deleted;bengal.stm.syntax.all._(a strict superset) is the single surface. Migration forimport stm._users is the one-line import swap; README already taught only syntax.all.TxnAdt: a rogue ADT case anywhere outside the ADT's own file is now a compile error, closing the unhandled-operation soundness hole structurally. The interpreters keep raising defaults — the exhaustiveness checker cannot verify path-dependent matches (rejects all twelve arms with the defaults dropped, both compilers) — and the blanket@nowarns narrowed to the three unit-cast expressions they were always for.No protocol behaviour changes: no scheduler or commit logic is touched; the spec suite holds (17 anchors, 12 pinned expectations).
Test plan
GITHUB_ACTIONS=true sbt scalafmtCheckAll scalafmtSbtCheck headerCheckAll 'scalafixAll --check' +test— 273/273 both compilers, fatal warnings onmimaReportBinaryIssues,doc,benchmarks/Jmh/compile./specs/verify_anchors.sh(17),./specs/expectations.sh --list(12)