Experiment: verification for dma module

[hiroki-chen]

This partially fulfills #344's goal but since RwArc is a runtime-checked object, we define most of the APIs on the RwLock*Guard which as a view method on it.

The most significant changes include the introduction of a new DMA mapping set infrastructure, enhanced specification and verification for untyped memory segment access, and a substantial redesign of the VmIo trait to unify and clarify read/write specifications. Additionally, the PR includes various code cleanups, import reorderings, and minor improvements to frame and segment APIs.

DMA Mapping Infrastructure

Basically introduced verified APIs for DMA operations.

Untyped Memory Segment Access

• Implemented verified reader and writer methods for Segment<M> where M: AnyUFrameMeta + OwnerOf, with detailed specification and proof blocks to ensure correct kernel-space access and invariants.

Virtual Memory I/O Trait Redesign

• Refactored the VmIo trait to unify and clarify read/write specifications, replacing multiple *_requires and *_ensures spec functions with read_spec and write_spec, and updating the method signatures for read and write to use VmWriter/VmReader and ownership tokens. This makes the contract for virtual memory I/O more explicit and verifiable.

I'm not sure if the usage of RwArc and some of the derived structs make sense so any comment or advice is strongly welcomed.

[rikosellic]

The this: RwLockReadGuard/RwLockWriteGuard arguments look a bit weird. Is it necessary to obtain the inner value to write preconditions?

[hiroki-chen]

I didn't used any RwLockWriteGuards, and all methods are read-only for now.

[hiroki-chen]

@rikosellic, btw, do we need to add functions that take &self and then forward them to RwLockReadGuard-based ones (currently no write guard needed)?

[rikosellic]

@hiroki-chen I’m not sure I fully understand your point. Do you mean converting &T to RwLockReadGuard<T>?

[hiroki-chen]

rting &T to RwLockReadGuard<T>?

Yes, the original function signature is &self but since it is runtime-checked it might not be very straightforward to see what properties we can offer in such functions.

Example:

fn foo(&self); // assume self has "RwArc<T>"

// becomes

fn foo(&RwLockReadGuard<T>)

so that we can put pre-conditions and post-conditions to the second one, which makes the verification more explicit.

The downside is that an extra wrapper might be needed – to be compatible with the original one.

[rikosellic]

I think this modification will change the code behaviour. The design of RwArc is exactly why we can not write obvious pre/post-conditions for &self. RwArc provides interior mutability that is shared through different threads. When you read something from a function taking &RwArc, you can not even ensure that when the function returns, the value you read is still the same as the value protected behind the atomic. This is different from having an RwLockReadGuard, which means you can always ensure the value will not change while that guard exists. This is determined by the design of concurrent objects; we can never directly know the inner value of the atomic when having a &RwArc. And the reason why RwLockReadGuard works is that we can extract and restore knowledge (i.e., ghost resources) that gives us information about the inner value when operating the atomic.

As for writing through &RwArc, it is the same. The best we can do is to use tokens, either provided by tokenized_state_machine or defined by our own ghost resources, to represent the transitions we can make to the inner value. But we can never ensure that when the function returns, the inner value is still in the state that the transition has just finished.

[hiroki-chen]

I think this modification will change the code behaviour. The design of RwArc is exactly why we can not write obvious pre/post-conditions for &self. RwArc provides interior mutability that is shared through different threads. When you read something from a function taking &RwArc, you can not even ensure that when the function returns, the value you read is still the same as the value protected behind the atomic. This is different from having an RwLockReadGuard, which means you can always ensure the value will not change while that guard exists. This is determined by the design of concurrent objects; we can never directly know the inner value of the atomic when having a &RwArc. And the reason why RwLockReadGuard works is that we can extract and restore knowledge (i.e., ghost resources) that gives us information about the inner value when operating the atomic.

As for writing through &RwArc, it is the same. The best we can do is to use tokens, either provided by tokenized_state_machine or defined by our own ghost resources, to represent the transitions we can make to the inner value. But we can never ensure that when the function returns, the inner value is still in the state that the transition has just finished.

You are correct regarding the concurrency limitations of &RwArc. However, my goal is to separate the synchronization layer from the functional logic.

Reasoning directly on RwArc only proves that an invariant is maintained, which can be opaque. By using the Guard as a proof token, we specify concrete transitions for the inner state so people can see what happens clearly. This allows us to implement a pattern where a public API f(&RwArc) acquires the lock and then delegates to a verified f_impl(&Guard) that possesses the necessary ghost resources to prove specific $S \to S'$ properties. This makes the contract for what is actually being done to the data much clearer.

[rikosellic]

Now I get your point！ I'm still thinking whether we can do this without spliting the function. When I used to prove system calls in uC/OS II, we are facing a simliar situation, where the kernel can be concurrently called by many system calls and is synchronized through a big lock, but they have a clear way to state what transition we will do to the inner invariant (which may be nondeterminisitic) through context refinement. I will get back to you with more details later and maybe we can think whether we can achieve this in Verus. Until then the splitting approach is accepatable.

[hiroki-chen]

Lol, finally made some progress on this

[hiroki-chen]

@SNoAnd, Sean, seems we need to have VmIoOwners or something for kernel-owned VM objects. For example, the dma module has VmIO which requires us to have VmIoOwners on both the reader and writer (kernel object <-> user object). And because we use Segment as the underlying memory storage which boils down to MetaSlots, it might be useful if we can somehow create IO permissions from, e.g., MetaSlotOwner?