Skip to content

Prove tlb flush functions - #677

Draft
DID-Lab-SZU wants to merge 3 commits into
asterinas:mainfrom
DID-Lab-SZU:prove/tlb-flush-functions
Draft

Prove tlb flush functions#677
DID-Lab-SZU wants to merge 3 commits into
asterinas:mainfrom
DID-Lab-SZU:prove/tlb-flush-functions

Conversation

@DID-Lab-SZU

Copy link
Copy Markdown
Collaborator

No description provided.

@Marsman1996 Marsman1996 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

I'm not sure, too many exec code modifications

Comment thread ostd/src/mm/tlb.rs Outdated
Comment thread ostd/src/mm/tlb.rs Outdated
Comment thread ostd/src/mm/tlb.rs Outdated
Comment thread ostd/src/mm/tlb.rs Outdated
Comment thread ostd/src/mm/tlb.rs Outdated
@DID-Lab-SZU
DID-Lab-SZU requested a review from Marsman1996 July 31, 2026 07:00
@Marsman1996 Marsman1996 added the AI-assist AI-aided proof or generation label Jul 31, 2026

@Marsman1996 Marsman1996 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

From fa2a3b8 we can see that KVerus now still let the exec code modification passes without human review, which we shall think of a better method to guard the exec code...

@hiroki-chen

Copy link
Copy Markdown
Collaborator

This should be closed because:

  1. The TLB is CPU-local and should be explicitly modeled after CPU core model has been stablized.
  2. The TLB module has no spec at all so the verification itself is at most vacuous.

@rikosellic I don't think this PR should be merged right now. Perhaps this is part of the phase III content?

@hiroki-chen

Copy link
Copy Markdown
Collaborator

This will also interfere with page table designs because old mappings will likely need to reconcile with the latest modifications, for example.

@hiroki-chen
hiroki-chen marked this pull request as draft July 31, 2026 14:42
@rikosellic

Copy link
Copy Markdown
Collaborator

Yeah we should discuss this later.

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

Labels

AI-assist AI-aided proof or generation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants