Try to use dyn InAtomicMode

[rikosellic]

No description provided.

[hiroki-chen]

This is curious, since some of the APIs declared now become:

    /// Queries the mapping at the given virtual address.
    ///
    /// Returns the mapped item at the page containing `addr`, or `None` if there is no mapping.
    ///
    /// ## Preconditions
    /// - The kernel virtual area invariant holds ([`inv`](Inv::inv)).
    /// - The address is within the virtual area's range.
    /// ## Postconditions
    /// - If there is a mapped item at the page containing the address ([`query_some_condition`]),
    /// it is returned ([`query_some_ensures`]).
    /// - If there is no mapping at that page, `None` is returned ([`query_none_ensures`]).
    #[verus_spec(r =>
        with Tracked(owner): Tracked<KVirtAreaOwner>,
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(guards): Tracked<&mut Guards<'static, KernelPtConfig>>,
            Ghost(root_guard): Ghost<PageTableGuard<'static, KernelPtConfig>>
            Tracked(guards): Tracked<&mut Guards<'_, KernelPtConfig>>,
            Ghost(root_guard): Ghost<PageTableGuard<'_, KernelPtConfig>>
        /* omit *./
    )]
    #[allow(private_interfaces)]
    pub fn query(&self, addr: Vaddr) -> Option<super::MappedItem> { ... }

So this means when you have a tracked guard you must ensure that it is statically available and should not be bound to any specific lifetime like 'rcu. However, since disabling preemption must be effective for only a specific timeframe (otherwise this would break the kernel's scheduling), this causes a serious lifetime issue. Apparently query should be not take a 'static guards as they should be only valid for a perioud of time.

[hiroki-chen]

Well then, specs for APIs associated guards are unsound... We'll need a fix first. I'd suggest doing:

#[verus_spec(r =>
        with Tracked(owner): Tracked<KVirtAreaOwner>,
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
//            Tracked(guards): Tracked<&mut Guards<'static, KernelPtConfig>>,
//            Ghost(root_guard): Ghost<PageTableGuard<'static, KernelPtConfig>>
            Tracked(guards): Tracked<&mut Guards<'_, KernelPtConfig>>, // just let Rust infer or bind to &'_ self
            Ghost(root_guard): Ghost<PageTableGuard<'_, KernelPtConfig>>
)]
pub fn query(&self, addr: Vaddr) -> Option<super::MappedItem> { ... }

For cursors, perhaps we'll need two lifetime markers?

pub struct Cursor<'rcu, 'guard, C: PageTableConfig> {
    /// The current path of the cursor.
    ///
    /// The level 1 page table lock guard is at index 0, and the level N page
    /// table lock guard is at index N - 1.
    pub path: [Option<PageTableGuard<'rcu, C>>; NR_LEVELS],
    /// The cursor should be used in a RCU read side critical section.
    pub rcu_guard: &'guard dyn InAtomicMode,
//....
}

Cursor is associated to its parent struct whose lifetime should be rcu and the atomic operation should occur as long as the preemption is disabled (i.e., rcu).

P.S.: --no-lifetime can be used as a trick to bypass this issue.

[rikosellic]

This is exactly what I'm worrying yesterday. I've done some experiments like 'rcu:'guard but failed. Anyway, I think we must find a sound way to do this, hacking with no-lifetime is not an acceptable solution for me.

[hiroki-chen]

This is exactly what I'm worrying yesterday. I've done some experiments like 'rcu:'guard but failed. Anyway, I think we must find a sound way to do this, hacking with no-lifetime is not an acceptable solution for me.

We can at least first replace '_ or explicit local lifetime for some of the tracked guards with 'static lifetimes. These may be easy to fix

[rikosellic]

I do not think we can pass &mut Guard as an argument. disable_preempt returns a local variable, whose lifetime is not relevant to the lifetime of Guard. Replacing static with _ does not help. The current approach works because disable_preempt returns a guard with a user-provided lifetime, but it is not the truth.

[hiroki-chen]

I do not think we can pass &mut Guard as an argument. disable_preempt returns a local variable, whose lifetime is not relevant to the lifetime of Guard. Replacing static with _ does not help. The current approach works because disable_preempt returns a guard with a user-provided lifetime, but it is not the truth.

Replacing static with _ allows Rust to deduce that it outlives &cursor but it does not have anything to do with the DisablePreemptGuard.