@hiroki-chen @Marsman1996 @SNoAnd According to the documentation, PageTableConfig::item_from_raw should restore the exact item that item_into_raw consumed. Unfortunately, KernelPtConfig failed to clear the AVAIL1 bit, which is used to indicate trackedness, violating the documented constraint and complicating verification.
As the PageTableConfig has been refactored in newer Asterinas versions, I propose changing this code to deal with AVAIL1 only in our codebase in #622 to make our verification smoother.
|
/// - if the provided raw form matches the item that was consumed by |
|
/// `item_into_raw`, `item_from_raw` restores the exact item that was |
|
/// consumed by `item_into_raw`. |
@hiroki-chen @Marsman1996 @SNoAnd According to the documentation,
PageTableConfig::item_from_rawshould restore the exact item thatitem_into_rawconsumed. Unfortunately,KernelPtConfigfailed to clear theAVAIL1bit, which is used to indicate trackedness, violating the documented constraint and complicating verification.As the
PageTableConfighas been refactored in newer Asterinas versions, I propose changing this code to deal withAVAIL1only in our codebase in #622 to make our verification smoother.vostd/ostd/src/mm/page_table/mod.rs
Lines 108 to 110 in f918b43