PhaseII verified: Temporal logic and state machines

[rikosellic]

No description provided.

[rikosellic]

This is the first step of the effort to verify data structures in sync. VerusSync shows several limitations, so a new framework is required. Currently, I'm migrating temporal logic and state machine definitions from Anvil to see to what extent we can formally verify liveness properties of our TLA state machines. Connecting the state machine to Rust code is the next step.

This is orthogonal to the verification in mm.

[rikosellic]

I managed to prove the dead_and_alive_lock_free property of the abstract_lock defined in TLA+, which shows this approach is promising. I think it can be merged now. The later verification work of sync will be split into two parts. One starts from the spec and focuses on more liveness proofs, and the other starts from the executable code and focuses on the minimal safety requirement of exclusiveness. Let's see where they can be merged in the future.