Smaller epsilon towards determinism#125
Draft
cds-amal wants to merge 3 commits intoruntimeverification:masterfrom
Draft
Smaller epsilon towards determinism#125cds-amal wants to merge 3 commits intoruntimeverification:masterfrom
cds-amal wants to merge 3 commits intoruntimeverification:masterfrom
Conversation
…tput Output vectors (functions, types, allocs, spans) were sorted by rustc's interned indices (Ty.to_index(), AllocId.to_index()), which change between compiler runs. Replace these with content-based sort keys: type display strings for functions/types, a variant+content key for allocs, and location tuples for spans. Also sort uneval_consts (previously unsorted). For functions and types, the interned index is kept as a tiebreaker in case two distinct types produce the same display string. Regenerate golden files for the 3 tests affected by the new ordering.
The Makefile ran `cargo clippy` without flags, so clippy warnings that CI treats as errors (via `-Dwarnings`) passed locally but failed in CI.
Replace sort_by with sort_by_key(alloc_sort_key), which clippy further simplifies by passing the function directly without a closure wrapper.
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.
This PR replaces all index-based sort keys with content-derived ones, making the ordering of output vectors deterministic across runs. The one remaining source of cross-run non-determinism is
adt_def(see below for why that can't be fixed here).Context
For those unfamiliar: rustc stores types, allocations, and other values in central tables and refers to them by integer index. These indices are assigned in the order the compiler happens to intern items, which is not guaranteed to be the same between invocations. There are two independent reasons for this:
FxHashMapfor speed rather than the standard library'sRandomState-backedHashMap). Hash-map iteration order is not specified and depends on hash/table layout and insertion history. If the order of insertions varies (because upstream work completed in a different order, or because of platform or compiler version differences), then iterating the map and interning items in iteration order produces different interned indices.Either source alone is sufficient to produce different indices across runs.
The output vectors in
collect_smir()were sorted like this:These
.to_index()calls return those interned IDs. The original comment said "stabilise output (a bit)", which is honest about the fact that this was only partially working. Anduneval_consts(coming fromHashMap::into_iter()) wasn't sorted at all.The integration test harness worked around all of this with a jq normalization filter (
normalise-filter.jq) that strips unstable IDs and re-sorts by content before diffing. But the raw JSON output itself was not reproducible.What changed
All changes are in
src/printer.rs, in the sorting section ofcollect_smir(). Here's the new sort strategy for each vector:functionsTy.to_index()Tydisplay string (viaty_pretty)typesTy.to_index()Tydisplay string (viaty_pretty)allocsAllocId.to_index()spans(filename, lo_line, lo_col, hi_line, hi_col)uneval_constsitemsOrdimplAllocation sort keys deserve some detail. The new
alloc_sort_key()helper produces a content-derived string from eachAllocInfoby matching on theGlobalAllocvariant:Memory0_Memory_+ zero-padded byte length"0_Memory_00000000000000000032"Static1_Static_+ def name"1_Static_MY_STATIC"VTable2_VTable_+ type string"2_VTable_dyn Trait"Function3_Function_+ instance name"3_Function_foo::bar"The numeric prefix groups entries by variant kind. Byte length is zero-padded to 20 digits so that
32sorts before128lexicographically. (Span locations areusizevalues that compare numerically, so no padding is needed there.)Three golden test files were regenerated because their normalized output changed due to the new ordering. The jq normalization filter doesn't fully sort
TupleTypeandFunTypeentries, so those were sensitive to input order.Remaining non-determinism:
adt_defWe looked into stabilizing the
adt_deffield onEnumType/StructType/UnionTypeas well; it's another interned index that the jq filter strips for test normalization. Turns out it can't be dropped or replaced.The reason: downstream consumers need
adt_defas a cross-reference key to matchAggregateKind::Adt(adt_def, ...)in MIR bodies with the corresponding type metadata entry.AggregateKindserialization comes from stable_mir (we don't control it), so both sides of the join have to use the same key format. The index is consistent within a single JSON file; it's just not stable across runs.So
adt_defremains the one known source of cross-run non-determinism in the output, and the jq filter still needs to strip it for golden test comparison. A comment was added on the field explaining this constraint. If we ever get the ability to customizeAggregateKindserialization upstream, we could replace these indices with names, but that's a stable_mir change, not something we can do on our end. (See PR #64 for the full discussion.)On the
Tydisplay string tiebreakerTy's display impl goes throughty_pretty(), which callsto_string()on rustc's internalTy. For monomorphized types (all generics resolved, no lifetime parameters), this should be injective: distinct types produce distinct strings. But there's a theoretical concern: could two distinctTyvalues display identically? Perhaps some obscure lifetime or where-clause difference that gets elided in the display output.We weren't confident enough to rule this out entirely, so the interned index is used as a tiebreaker: content-based ordering for the common case, with the index preserving a consistent (within-run) ordering for any hypothetical ties. If a tie does occur, the ordering at the tie point would be non-deterministic across runs, but we haven't observed this in practice.
What this means in practice
If you run stable-mir-json twice on the same input file and diff the raw JSON (no jq filter), the only differences will be the interned index values themselves (
adt_def,alloc_id,Tykeys, etc.). The structural ordering of every output vector is now identical across runs. Before this change, even the order of types, functions, allocs, and spans could shuffle around.The jq normalization filter is still needed for golden tests (to strip those interned IDs), but the sort operations in it are now redundant; they just confirm what the source already guarantees.
Performance
The
format!("{}", ty)calls for sortingfunctionsandtypesallocate strings. This is fine; the vectors are small (one entry per unique type or function in the program), and this code runs once at the end after all collection is done.Test plan
cargo buildcompiles cleanlymake integration-testpasses (all 28 tests)assert_eq.rsand diffed the raw JSON: identical modulo interned index values (adt_defonly); all vector ordering matched exactly