Skip to content

Register allocator correctness verifier#13229

Draft
danocmx wants to merge 97 commits intooracle:masterfrom
danocmx:feat/reg-alloc-verifier
Draft

Register allocator correctness verifier#13229
danocmx wants to merge 97 commits intooracle:masterfrom
danocmx:feat/reg-alloc-verifier

Conversation

@danocmx
Copy link
Copy Markdown

@danocmx danocmx commented Mar 27, 2026

Register allocation verifier, inspired by cranelift's regalloc checker. Works by saving symbols before allocation - variables, constants, registers and stack slots, then matches these to locations inserted by allocator(s) - registers and stack slots. Outputs of instructions then store these symbols to those locations in block's verification state. Spills, register moves and reloads move these around. Before any checking is done, initial allocation state (map of form location → symbol) is calculated for each block based on it's predecessors, when same location with different symbols meet, a conflict is created - can be resolved by writing to the location. Afterwards, checking is done for each block, we verify that symbols before allocation are stored at the locations inserted by allocator(s), taking into account reloads and spills that the allocator created.

Implemented as a phase (RegAllocVerifierPhase) that wraps around both register and stack allocator, collects symbol information before allocation and matches this information to instructions after allocation to create verifier IR that it then uses to update state allocation maps and to verify operands.

When a violation is detected by the verifier, a RAVException is thrown and if dumping is enabled a .rav.txt file is created in graal_dumps directory with the exception details and verifier IR.

Implemented as jdk.graal.compiler.lir.alloc.verifier package, modifies AllocationStage to insert the verification phase when enabled and also changes modifier to public for build method in LocationMarker to access it in the verifier package. No other modification to existing was needed, variable locations stripped by the allocator from label/jump instructions are recovered by finding their first usage in FromUsageGlobalResolver class to not mess with the existing register allocator code.

Some functionality tested in RegAllocVerifierTest, runs valid methods with the verifier, then injects faults and tests if the verifier can detect them. To be expanded.

New compiler flags:

  • EnableRAVerifier - enables the verification for the compilation
  • VerifyStackAllocator - verifies that stack allocator output together with register allocator
  • CollectReferences - uses LocationMarker class to collect GC reference sets before final code analysis stage to verify and invalidate old references

Other functionality

  • Handle rematerialised constants
  • Check kinds between original variables and current locations, as well as the allocation state at said location
  • Check kinds between moved values
  • Make sure callee-saved registers are recovered
  • Check correspondence to operand flags
  • Make sure alive location is not overwritten by the instruction as temp or output
  • Remove old references and check if location marked as reference actually stores one
  • Make sure LIR reference and JavaKind Object match

danocmx added 30 commits March 22, 2026 10:21
@oracle-contributor-agreement
Copy link
Copy Markdown

Thank you for your pull request and welcome to our community! To contribute, please sign the Oracle Contributor Agreement (OCA).
The following contributors of this PR have not signed the OCA:

To sign the OCA, please create an Oracle account and sign the OCA in Oracle's Contributor Agreement Application.

When signing the OCA, please provide your GitHub username. After signing the OCA and getting an OCA approval from Oracle, this PR will be automatically updated.

If you are an Oracle employee, please make sure that you are a member of the main Oracle GitHub organization, and your membership in this organization is public.

@oracle-contributor-agreement oracle-contributor-agreement bot added the OCA Required At least one contributor does not have an approved Oracle Contributor Agreement. label Mar 27, 2026
@danocmx
Copy link
Copy Markdown
Author

danocmx commented Mar 27, 2026

cc @d-kozak @gergo-

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

OCA Required At least one contributor does not have an approved Oracle Contributor Agreement.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant