Weekly PR: ref_count TSM

[SNoAnd]

This PR includes the prototype VerusSync-style tokenized state machine for the ref_count field of each frame. Since we are planning on splitting up the 'inner' perms that are currently carried together in MetaRegionOwners, I modeled that behavior with a simplified TmpRegionOwners that can be replaced by the updated one. Then verified some simple approximations of our actual code with it. It all seems to work so far. Nothing touches the main project source.

The other main thread, types and layouts, ran into problems when I started porting it into Verus. I think it'll be pretty manageable but I ended up backing it out of this PR for now. Most of the work lives in VerusBelt anyway. Maybe I'll make a separate, branched PR for it and keep this one just for TSM stuff.

[rikosellic]

I'm wondering whether we do need a tokenized state machine for the reference-counting mechanism. The VerusSync-style tokenized state machine is just one kind of resource that can be stored in atomic_ghost. Verus uses it to verify their rwlock, but we managed to verify a more complicated rwlock purely with fractional permissions and without TSM. What do you think @SNoAnd @hiroki-chen?

[hiroki-chen]

AFAIK, this depends on the goal of the verification. TSM is convenient if the target being verified is myopic and self-contained so that its internal states solely interfact everything from within. For frames I'm afraid they might get entangled with other OS components and future extension is needed.

In this case the price we pay does not justify the architectural overhaul. Also It seems that PCM is a superset of TSM so switching to resource algebra doesn't hurt too much.

[SNoAnd]

@rikosellic, I tend to agree that the ref_count mechanism alone doesn't need to be its own TSM. My plan was to start there and expand to cover the frame module. Then, depending on the results of the TSM composition experiment, either compose that machine with a page_table machine or continue expanding one big TSM to cover the whole system.

@hiroki-chen, I think you're mostly thinking in terms of the latter approach, or are there other reasons that TSM is undesirable for a more dynamic codebase?

Experiments are now moved to a dedicated module, outside of specs. The pt_path_tsm.rs and pt_path_pcm.rs files compare the two approaches when mapping a frame, which in the TSM case involves separate state machines for page_table and ref_count. The PCM case ends up being slightly heavier to verify in these examples. I don't have a lot of experience with that technique though, so I wouldn't necessarily notice if the AI approached it inefficiently.

The best thing about the TSM in my book is that it naturally lends itself to a top-level theorem: all executions are modeled by this state machine, therefore all executions are defined, which is soundness. If we take the PCM approach I would want to write something resembling a state machine with it, just not using the TSM DSL.

[hiroki-chen]

@SNoAnd If you design a TSM the most of the states you are tracking are internally visible because TSM needs a "self-contained" design. If other kernel stuffs like the page table needs to manage the frame lifecycles on its own, the TSM might not work well in this case.