Skip to content

Add eager transitions to x86 TSO operational model#88

Merged
tperami merged 6 commits intomainfrom
optimise-x86-operational
Mar 20, 2026
Merged

Add eager transitions to x86 TSO operational model#88
tperami merged 6 commits intomainfrom
optimise-x86-operational

Conversation

@s-prism
Copy link
Copy Markdown
Collaborator

@s-prism s-prism commented Mar 10, 2026

  • Add eager transitions to x86 TSO operational model
  • Determine the number of execution paths taken in each test

Copy link
Copy Markdown
Collaborator

@tperami tperami left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Few fixes here, and I'll look up how to do better fuel handling at the bottom

Comment thread ArchSemX86/OperationalX86TSO.v Outdated
Comment thread ArchSemX86/OperationalX86TSO.v Outdated
Comment thread ArchSemX86/OperationalX86TSO.v Outdated
Comment thread ArchSemX86/OperationalX86TSO.v Outdated
Comment thread ArchSemX86/OperationalX86TSO.v Outdated
Comment thread ArchSemX86/OperationalX86TSO.v
Comment thread ArchSemX86/OperationalX86TSO.v Outdated
Comment thread ArchSemX86/OperationalX86TSO.v Outdated
@s-prism s-prism force-pushed the optimise-x86-operational branch from 8fb1995 to 1c74670 Compare March 16, 2026 14:53
@tperami tperami force-pushed the optimise-x86-operational branch from 4a7ef64 to a48d2ad Compare March 16, 2026 17:18
- Split the eager and non-eager runner to avoid looking up the flag all
  the time
- Streamline termination checking to avoid high-order stuff
  (else_action)
- Put everything in same section to avoid passing term and isem around
- Put machine_state in the section and rename into mstate for conciseness
@tperami tperami force-pushed the optimise-x86-operational branch from a48d2ad to 3baa529 Compare March 16, 2026 17:18
@tperami tperami merged commit 3c786f5 into main Mar 20, 2026
1 check passed
@tperami tperami deleted the optimise-x86-operational branch March 20, 2026 17:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants