From 1de689b269f2699cbabe1415fe06b7c0d455db50 Mon Sep 17 00:00:00 2001 From: Uuu Date: Thu, 30 Jul 2026 13:52:49 +0800 Subject: [PATCH 1/2] Prove TLB flush functions in ostd/src/mm/tlb.rs --- ostd/src/mm/tlb.rs | 62 ++++++++++++++++++++++++++++++++++------------ 1 file changed, 46 insertions(+), 16 deletions(-) diff --git a/ostd/src/mm/tlb.rs b/ostd/src/mm/tlb.rs index 75f18dec7..ba3853d03 100644 --- a/ostd/src/mm/tlb.rs +++ b/ostd/src/mm/tlb.rs @@ -40,8 +40,10 @@ pub struct TlbFlusher<'a /*, G: PinCurrentCpu*/ > { } } // verus! +verus! { + #[verus_verify] -impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { +impl<'a /*, G: PinCurrentCpu*/ > TlbFlusher<'a /*, G*/ > { /// Creates a new TLB flusher with the specified CPUs to be flushed. /// /// The target CPUs should be a reference to an [`AtomicCpuSet`] that will @@ -49,7 +51,7 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { /// /// The flusher needs to stick to the current CPU. So please provide a /// guard that implements [`PinCurrentCpu`]. - pub fn new(target_cpus: &'a AtomicCpuSet /*, pin_current_guard: G*/) -> Self { + pub fn new(target_cpus: &'a AtomicCpuSet /*, pin_current_guard: G*/ ) -> Self { Self { target_cpus, have_unsynced_flush: CpuSet::new_empty(), @@ -65,13 +67,21 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { /// [`Self::dispatch_tlb_flush`] is called. #[verus_spec( with Tracked(model): Tracked<&mut TlbModel> + requires + old(model).inv(), ensures *final(model) == old(model).issue_tlb_flush(op), final(model).inv(), )] - #[verifier::external_body] pub fn issue_tlb_flush(&mut self, op: TlbFlushOp) { - self.ops_stack.push(op, None); + // Update the ghost TLB model to reflect the pending flush (proof), then + // record the operation on the executable ops stack. The proof consumes + // `op` (matching the `ensures`), so `push` records a clone. + let op_clone = op.clone(); + proof { + model.tracked_issue_tlb_flush(op); + } + self.ops_stack.push(op_clone, None); } /// Issues a TLB flush request that must happen before dropping the page. @@ -83,17 +93,25 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { /// method is designed to be used in such cases. #[verus_spec(r => with Tracked(model): Tracked<&mut TlbModel> + requires + old(model).inv(), ensures *final(model) == old(model).issue_tlb_flush(op), final(model).inv(), )] - #[verifier::external_body] pub fn issue_tlb_flush_with( &mut self, op: TlbFlushOp, drop_after_flush: Frame, ) { - self.ops_stack.push(op, Some(drop_after_flush)); + // Update the ghost TLB model to reflect the pending flush (proof), then + // record the operation on the executable ops stack. The proof consumes + // `op` (matching the `ensures`), so `push` records a clone. + let op_clone = op.clone(); + proof { + model.tracked_issue_tlb_flush(op); + } + self.ops_stack.push(op_clone, Some(drop_after_flush)); } /// Dispatches all the pending TLB flush requests. @@ -112,8 +130,8 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { final(model).inv(), )] pub fn dispatch_tlb_flush(&mut self) { - unimplemented!() /*let irq_guard = crate::trap::irq::disable_local(); - + unimplemented!()/*let irq_guard = crate::trap::irq::disable_local(); + if self.ops_stack.is_empty() { return; @@ -152,6 +170,7 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { } else { self.ops_stack.clear_without_flush(); }*/ + } /// Waits for all the previous TLB flush requests to be completed. @@ -171,7 +190,7 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { /// other's TLB coherence. #[verifier::external_body] pub fn sync_tlb_flush(&mut self) { - unimplemented!() /* + unimplemented!()/* assert!( irq::is_local_enabled(), "Waiting for remote flush with IRQs disabled" @@ -185,9 +204,11 @@ impl<'a /*, G: PinCurrentCpu*/> TlbFlusher<'a /*, G*/> { self.have_unsynced_flush = CpuSet::new_empty(); */ + } } +} // verus! verus! { /// The operation to flush TLB entries. @@ -217,11 +238,13 @@ impl TlbFlushOp { } - #[verifier::external_body] fn optimize_for_large_range(self) -> Self { match self { TlbFlushOp::Range(range) => { - if range.len() > FLUSH_ALL_RANGE_THRESHOLD { + // Equivalent to `range.len() > FLUSH_ALL_RANGE_THRESHOLD`: + // `Range::::len` is `end.checked_sub(start).unwrap_or(0)`, + // i.e. saturating subtraction (never panics on inverted ranges). + if range.end.saturating_sub(range.start) > FLUSH_ALL_RANGE_THRESHOLD { TlbFlushOp::All } else { TlbFlushOp::Range(range) @@ -288,12 +311,10 @@ impl OpsStack { } } - #[verifier::external_body] fn is_empty(&self) -> bool { !self.need_flush_all && self.size == 0 } - #[verifier::external_body] fn push(&mut self, op: TlbFlushOp, drop_after_flush: Option>) { if let Some(frame) = drop_after_flush { // self.page_keeper.push(frame); @@ -311,7 +332,11 @@ impl OpsStack { self.size += 1; } - #[verifier::external_body] + #[verus_spec( + requires + self.size <= FLUSH_ALL_OPS_THRESHOLD, + other.size <= FLUSH_ALL_OPS_THRESHOLD, + )] fn push_from(&mut self, other: &OpsStack) { // self.page_keeper.extend(other.page_keeper.iter().cloned()); if self.need_flush_all { @@ -322,7 +347,13 @@ impl OpsStack { self.size = 0; return; } - for i in 0..other.size { + let old_size = self.size; + for i in 0..other.size + invariant + self.size == old_size + i, + i <= other.size, + old_size + other.size <= FLUSH_ALL_OPS_THRESHOLD, + { self.ops[self.size] = other.ops[i].clone(); self.size += 1; } @@ -344,7 +375,6 @@ impl OpsStack { self.clear_without_flush(); } - #[verifier::external_body] fn clear_without_flush(&mut self) { self.need_flush_all = false; self.size = 0; From fa2a3b863da855c05dc47c690bb2b7f47c077d35 Mon Sep 17 00:00:00 2001 From: Je5s1e Date: Fri, 31 Jul 2026 15:00:10 +0800 Subject: [PATCH 2/2] Refine TLB flush proof ownership --- ostd/specs/mm/tlb.rs | 11 ++++++++--- ostd/src/mm/tlb.rs | 33 ++++++++------------------------- 2 files changed, 16 insertions(+), 28 deletions(-) diff --git a/ostd/specs/mm/tlb.rs b/ostd/specs/mm/tlb.rs index 3c0ef433f..513d14044 100644 --- a/ostd/specs/mm/tlb.rs +++ b/ostd/specs/mm/tlb.rs @@ -108,14 +108,19 @@ impl TlbModel { TlbModel { pending: self.pending.push(op), mappings: self.mappings } } - pub proof fn tracked_issue_tlb_flush(tracked &mut self, tracked op: TlbFlushOp) + pub proof fn tracked_issue_tlb_flush(tracked &mut self, tracked op: &TlbFlushOp) requires old(self).inv(), ensures - *final(self) == old(self).issue_tlb_flush(op), + *final(self) == old(self).issue_tlb_flush(*op), final(self).inv(), { - self.pending.tracked_push(op); + match op { + TlbFlushOp::All => self.pending.tracked_push(TlbFlushOp::All), + TlbFlushOp::Address(a) => self.pending.tracked_push(TlbFlushOp::Address(*a)), + TlbFlushOp::Range(r) => { self.pending.tracked_push(TlbFlushOp::Range(r.start..r.end)) + }, + } } pub open spec fn dispatch_tlb_flush_spec(self) -> Self { diff --git a/ostd/src/mm/tlb.rs b/ostd/src/mm/tlb.rs index ba3853d03..68f71c5da 100644 --- a/ostd/src/mm/tlb.rs +++ b/ostd/src/mm/tlb.rs @@ -39,9 +39,6 @@ pub struct TlbFlusher<'a /*, G: PinCurrentCpu*/ > { //_pin_current: G, } -} // verus! -verus! { - #[verus_verify] impl<'a /*, G: PinCurrentCpu*/ > TlbFlusher<'a /*, G*/ > { /// Creates a new TLB flusher with the specified CPUs to be flushed. @@ -74,14 +71,10 @@ impl<'a /*, G: PinCurrentCpu*/ > TlbFlusher<'a /*, G*/ > { final(model).inv(), )] pub fn issue_tlb_flush(&mut self, op: TlbFlushOp) { - // Update the ghost TLB model to reflect the pending flush (proof), then - // record the operation on the executable ops stack. The proof consumes - // `op` (matching the `ensures`), so `push` records a clone. - let op_clone = op.clone(); proof { - model.tracked_issue_tlb_flush(op); + model.tracked_issue_tlb_flush(&op); } - self.ops_stack.push(op_clone, None); + self.ops_stack.push(op, None); } /// Issues a TLB flush request that must happen before dropping the page. @@ -104,14 +97,10 @@ impl<'a /*, G: PinCurrentCpu*/ > TlbFlusher<'a /*, G*/ > { op: TlbFlushOp, drop_after_flush: Frame, ) { - // Update the ghost TLB model to reflect the pending flush (proof), then - // record the operation on the executable ops stack. The proof consumes - // `op` (matching the `ensures`), so `push` records a clone. - let op_clone = op.clone(); proof { - model.tracked_issue_tlb_flush(op); + model.tracked_issue_tlb_flush(&op); } - self.ops_stack.push(op_clone, Some(drop_after_flush)); + self.ops_stack.push(op, Some(drop_after_flush)); } /// Dispatches all the pending TLB flush requests. @@ -208,9 +197,6 @@ impl<'a /*, G: PinCurrentCpu*/ > TlbFlusher<'a /*, G*/ > { } } -} // verus! -verus! { - /// The operation to flush TLB entries. #[verifier::allow(autoderive_clone_without_spec)] #[derive(Debug, Clone, PartialEq, Eq)] @@ -241,10 +227,8 @@ impl TlbFlushOp { fn optimize_for_large_range(self) -> Self { match self { TlbFlushOp::Range(range) => { - // Equivalent to `range.len() > FLUSH_ALL_RANGE_THRESHOLD`: - // `Range::::len` is `end.checked_sub(start).unwrap_or(0)`, - // i.e. saturating subtraction (never panics on inverted ranges). - if range.end.saturating_sub(range.start) > FLUSH_ALL_RANGE_THRESHOLD { + if vstd_extra::external::range::range_usize_len(&range) + > FLUSH_ALL_RANGE_THRESHOLD { TlbFlushOp::All } else { TlbFlushOp::Range(range) @@ -347,12 +331,11 @@ impl OpsStack { self.size = 0; return; } - let old_size = self.size; for i in 0..other.size invariant - self.size == old_size + i, + self.size == old(self).size + i, i <= other.size, - old_size + other.size <= FLUSH_ALL_OPS_THRESHOLD, + old(self).size + other.size <= FLUSH_ALL_OPS_THRESHOLD, { self.ops[self.size] = other.ops[i].clone(); self.size += 1;