PhaseII verified: Temporal logic and state machines (#213)

* MutexSpec init

* MutexSpec init

* Fix mutex spec

* Use state_machine to characterize state predicates

* Complete state machine definition

* temporal logic init

* Make `temporal_logic` compile

* Add a test

* Simplify stable def

* Add TLA rules

* Add some broadcasts

* Use ext_euqal for Execution

* Use broadcast to simplify proofs

* Simplify rules

* fmt

* Simplify rules

* Add a public broadcast group

* Finish updating TLA rules

* Migrate state_machine

* Add mutex state machine

* Add TLA-style transitions

* add pub use

* Merge temporal logic and state machine into vstd_extra to avoid compilation bugs

* fmt

* fmt

* Model abstract lock

* Prove the first TLA lemma

* Add mutual_exclusion_lemma

* Prove lemma_pc_stack_match in an ugly way

* Update abstract_lock.rs

* Minor

* refactor code

* Refactor code

* Add two proofs

* Fix crate name

* Update abstract_lock.rs

* Add rules and macros

* prove: 1 admit in lemma_not_locked_iff_not_in_cs

* prove: 2 `admit`s in `vstd_extra/rules`

* Minor

* Prove a set_prop_mutual_exclusion lemma

* Add handy macros

* prove: 6 `admit`s but modify a spec

* Revert "prove: 6 `admit`s but modify a spec"

This reverts commit 0901c02.

* fix false spec identified by kverus

* prove: 6 `admit`s in ostd sync spec

* Simplify kverus code

* Revert "Simplify kverus code"

This reverts commit da21deb.

* Revert "prove: 6 `admit`s in ostd sync spec"

This reverts commit 97a0fd0.

* Manually prove the first admit

* Prove mutual_exclusion

* Add a liveness lemma

* fmt

* Fix wrong spec

* Simplify rules

* Prove a new rule

* Fix some macros

* fmt

* Add TLA rules

* prove: `implies_tla_exists_by_witness` and `leads_to_tla_exists_by_witness`

* simplify proof

* Make rule names more clear

* Fully prove a liveness property

* Add a locked case

* prove: lift_state_exists_leads_to_intro

* prove: lemma_pc_stack_match_statdead_and_alive_lock_freee_pred_case_locked

* Simplify AI proofs

* Make SpinLock compile

* Prove dead and alive lock free

* Minor

---------

Co-authored-by: Marsman1996 <lqliuyuwei@outlook.com>

Author: rikosellic

Cargo.lock

@@ -44,9 +44,9 @@ pub mod logger;*/
 pub mod mm;
 /*pub mod panic;
 pub mod prelude;
-pub mod smp;
+pub mod smp;*/
 pub mod sync;
-pub mod task;
+/* pub mod task;
 pub mod timer;
 pub mod trap;
 pub mod user;*/

ostd/src/lib.rs

@@ -1,14 +1,14 @@
 // SPDX-License-Identifier: MPL-2.0
 //! Useful synchronization primitives.
-mod guard;
-mod mutex;
-mod rcu;
-mod rwarc;
-mod rwlock;
-mod rwmutex;
+//mod guard;
+//mod mutex;
+//mod rcu;
+//mod rwarc;
+//mod rwlock;
+//mod rwmutex;
 mod spin;
-mod wait;
-
+//mod wait;
+/* 
 pub(crate) use self::rcu::finish_grace_period;
 pub use self::{
     guard::{GuardTransfer, LocalIrqDisabled, PreemptDisabled, SpinGuardian, WriteIrqDisabled},
@@ -29,4 +29,4 @@ pub use self::{
 
 pub(crate) fn init() {
     rcu::init();
-}
+}*/

ostd/src/sync/mod.rs

@@ -1,4 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
+use vstd::prelude::*;
+use vstd::cell::{self, PCell};
+
 use alloc::sync::Arc;
 use core::{
     cell::UnsafeCell,
@@ -8,8 +11,8 @@ use core::{
     sync::atomic::{AtomicBool, Ordering},
 };
 
-use super::{guard::SpinGuardian, LocalIrqDisabled, PreemptDisabled};
-use crate::task::atomic_mode::AsAtomicModeGuard;
+//use super::{guard::SpinGuardian, LocalIrqDisabled, PreemptDisabled};
+//use crate::task::atomic_mode::AsAtomicModeGuard;
 
 /// A spin lock.
 ///
@@ -27,32 +30,41 @@ use crate::task::atomic_mode::AsAtomicModeGuard;
 ///
 /// [`disable_irq`]: Self::disable_irq
 #[repr(transparent)]
-pub struct SpinLock<T: ?Sized, G = PreemptDisabled> {
+#[verus_verify]
+//pub struct SpinLock<T: ?Sized, G = PreemptDisabled> {
+pub struct SpinLock<T,G> {
     phantom: PhantomData<G>,
     /// Only the last field of a struct may have a dynamically sized type.
     /// That's why SpinLockInner is put in the last field.
     inner: SpinLockInner<T>,
 }
 
-struct SpinLockInner<T: ?Sized> {
+#[verus_verify]
+struct SpinLockInner<T> {
     lock: AtomicBool,
-    val: UnsafeCell<T>,
+    //val: UnsafeCell<T>,
+    val: PCell<T>,
 }
 
+verus!{
+#[verus_verify]
 impl<T, G> SpinLock<T, G> {
     /// Creates a new spin lock.
     pub const fn new(val: T) -> Self {
+        let (val, Tracked(perm)) = PCell::new(val);
         let lock_inner = SpinLockInner {
             lock: AtomicBool::new(false),
-            val: UnsafeCell::new(val),
+            //val: UnsafeCell::new(val),
+            val: val,
         };
         Self {
             phantom: PhantomData,
             inner: lock_inner,
         }
     }
 }
-
+}
+/* 
 impl<T: ?Sized> SpinLock<T, PreemptDisabled> {
     /// Converts the guard behavior from disabling preemption to disabling IRQs.
     pub fn disable_irq(&self) -> &SpinLock<T, LocalIrqDisabled> {
@@ -156,14 +168,14 @@ pub struct SpinLockGuard_<T: ?Sized, R: Deref<Target = SpinLock<T, G>>, G: SpinG
     guard: G::Guard,
     lock: R,
 }
-
+/* 
 impl<T: ?Sized, R: Deref<Target = SpinLock<T, G>>, G: SpinGuardian> AsAtomicModeGuard
     for SpinLockGuard_<T, R, G>
 {
     fn as_atomic_mode_guard(&self) -> &dyn crate::task::atomic_mode::InAtomicMode {
         self.guard.as_atomic_mode_guard()
     }
-}
+}*/
 
 impl<T: ?Sized, R: Deref<Target = SpinLock<T, G>>, G: SpinGuardian> Deref
     for SpinLockGuard_<T, R, G>
@@ -210,3 +222,4 @@ unsafe impl<T: ?Sized + Sync, R: Deref<Target = SpinLock<T, G>> + Sync, G: SpinG
     for SpinLockGuard_<T, R, G>
 {
 }
+*/

ostd/src/sync/spin.rs

@@ -25,4 +25,4 @@ check_lifetime = true
 [dependencies]
 vstd = { workspace = true, optional = true }
 vstd_extra = { path = "../../vstd_extra" }
-aster_common = { path = "../../aster_common" }
+aster_common = { path = "../../aster_common" }

specs/ostd/Cargo.toml

@@ -1,7 +1,9 @@
+#![allow(non_snake_case)]
 mod linked_list_specs;
 mod meta_specs;
 mod page_table_cursor_specs;
 mod memory_region_specs;
+mod sync;
 mod page_table_node_specs;
 
 pub use linked_list_specs::*;