[WIP] Merge rcu version (#193)

* Add `SpinGuardGhostInner`

* Fix minor

* Temp progress

* Trivial merge

Author: Xungan2

lock-protocol/src/exec/mod.rs

@@ -1,7 +1,6 @@
-mod rcu;
-mod rw;
+// mod rcu;
+// mod rw;
 // mod test_map;
-
 use vstd::{invariant, prelude::*};
 use core::num;
 use std::collections::HashMap;

lock-protocol/src/exec/rcu/cpu.rs

@@ -1,7 +1,7 @@
 use vstd::prelude::*;
 
 use crate::spec::{common::*, utils::*, rcu::*};
-use super::{common::*, types::*};
+use super::common::*;
 
 verus! {
 

lock-protocol/src/exec/rcu/cursor/locking.rs

@@ -8,7 +8,7 @@ use vstd_extra::ghost_tree::Node;
 use vstd_extra::manually_drop::*;
 
 use crate::spec::{common::*, utils::*, rcu::*};
-use super::super::{common::*, types::*, cpu::*};
+use super::super::{common::*, cpu::*};
 use super::super::{frame::meta::*, page_table::*};
 use super::super::node::{
     PageTableNode, PageTableNodeRef, PageTableGuard,
@@ -167,8 +167,8 @@ pub(super) fn lock_range<'rcu>(
             subtree_root_opt->Some_0.wf(),
             subtree_root_opt->Some_0.inst().cpu_num() == GLOBAL_CPU_NUM,
             subtree_root_opt->Some_0.inst_id() == pt.inst@.id(),
-            subtree_root_opt->Some_0.guard->Some_0.stray_perm@.value() == false,
-            subtree_root_opt->Some_0.guard->Some_0.in_protocol@ == true,
+            subtree_root_opt->Some_0.guard->Some_0.stray_perm().value() == false,
+            subtree_root_opt->Some_0.guard->Some_0.in_protocol() == true,
             // TODO
             m.inv(),
             m.inst_id() == pt.inst@.id(),
@@ -216,9 +216,10 @@ pub(super) fn lock_range<'rcu>(
     )
 }
 
-pub fn unlock_range(cursor: &mut Cursor<'_>, m: Tracked<LockProtocolModel>) -> (res: Tracked<
-    LockProtocolModel,
->)
+pub fn unlock_range(
+    cursor: &mut Cursor<'_>, 
+    m: Tracked<LockProtocolModel>
+) -> (res: Tracked<LockProtocolModel>)
     requires
         old(cursor).wf(),
         m@.inv(),
@@ -314,8 +315,8 @@ fn try_traverse_and_lock_subtree_root<'rcu>(
             &&& res.0->Some_0.wf()
             &&& res.0->Some_0.inst().cpu_num() == GLOBAL_CPU_NUM
             &&& res.0->Some_0.inst_id() == pt.inst@.id()
-            &&& res.0->Some_0.guard->Some_0.stray_perm@.value() == false
-            &&& res.0->Some_0.guard->Some_0.in_protocol@ == true
+            &&& res.0->Some_0.guard->Some_0.stray_perm().value() == false
+            &&& res.0->Some_0.guard->Some_0.in_protocol() == true
             &&& res.1@.inv()
             &&& res.1@.inst_id() == pt.inst@.id()
             &&& res.1@.state() is Locking
@@ -346,7 +347,7 @@ fn try_traverse_and_lock_subtree_root<'rcu>(
                 &&& cur_node_guard->Some_0.inst_id() == pt.inst@.id()
                 &&& cur_node_guard->Some_0.nid() == cur_nid
                 &&& cur_node_guard->Some_0.inner.deref().level_spec() == cur_level
-                &&& cur_node_guard->Some_0.guard->Some_0.in_protocol@ == false
+                &&& cur_node_guard->Some_0.guard->Some_0.in_protocol() == false
             },
         ensures
             1 <= cur_level <= MAX_NR_LEVELS,
@@ -360,7 +361,7 @@ fn try_traverse_and_lock_subtree_root<'rcu>(
                 &&& cur_node_guard->Some_0.inst_id() == pt.inst@.id()
                 &&& cur_node_guard->Some_0.nid() == cur_nid
                 &&& cur_node_guard->Some_0.inner.deref().level_spec() == cur_level
-                &&& cur_node_guard->Some_0.guard->Some_0.in_protocol@ == false
+                &&& cur_node_guard->Some_0.guard->Some_0.in_protocol() == false
             },
         decreases cur_level,
     {
@@ -469,7 +470,7 @@ fn try_traverse_and_lock_subtree_root<'rcu>(
             m.token = new_token.1.get();
         }
         pt_guard.put_node_token(Tracked(new_node_token));
-        pt_guard.update_in_protocol(Ghost(true));
+        pt_guard.update_in_protocol(Tracked(true));
     }
     (Some(pt_guard), Tracked(m))
 }
@@ -487,26 +488,29 @@ fn dfs_acquire_lock(
     // cur_node_va: Vaddr,
     // va_range: Range<Vaddr>,
     m: Tracked<LockProtocolModel>,
-) -> (res: Tracked<LockProtocolModel>)
+    forgot_guards: Tracked<SubTreeForgotGuard>,
+) -> (res: (Tracked<LockProtocolModel>, Tracked<SubTreeForgotGuard>))
     requires
         cur_node.wf(),
-        cur_node.guard->Some_0.stray_perm@.value() == false,
-        cur_node.guard->Some_0.in_protocol@ == true,
+        cur_node.guard->Some_0.stray_perm().value() == false,
+        cur_node.guard->Some_0.in_protocol() == true,
         m@.inv(),
         m@.inst_id() == cur_node.inst_id(),
         m@.state() is Locking,
         m@.cur_node() == cur_node.nid() + 1,
         m@.node_is_locked(cur_node.nid()),
     ensures
-        res@.inv(),
-        res@.inst_id() == cur_node.inst_id(),
-        res@.state() is Locking,
-        res@.sub_tree_rt() == m@.sub_tree_rt(),
-        res@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid()),
+        res.0@.inv(),
+        res.0@.inst_id() == cur_node.inst_id(),
+        res.0@.state() is Locking,
+        res.0@.sub_tree_rt() == m@.sub_tree_rt(),
+        res.0@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid()),
     decreases cur_node.deref().deref().level_spec(),
 {
     broadcast use crate::spec::utils::group_node_helper_lemmas;
 
+    let tracked mut forgot_guards = forgot_guards.get();
+
     let cur_level = cur_node.deref().deref().level();
     if cur_level == 1 {
         assert(m@.cur_node() == NodeHelper::next_outside_subtree(cur_node.nid())) by {
@@ -531,8 +535,8 @@ fn dfs_acquire_lock(
         invariant
             0 <= i <= 512,
             cur_node.wf(),
-            cur_node.guard->Some_0.stray_perm@.value() == false,
-            cur_node.guard->Some_0.in_protocol@ == true,
+            cur_node.guard->Some_0.stray_perm().value() == false,
+            cur_node.guard->Some_0.in_protocol() == true,
             cur_node.deref().deref().level_spec() > 1,
             NodeHelper::is_not_leaf(cur_node.nid()),
             m.inv(),
@@ -560,7 +564,7 @@ fn dfs_acquire_lock(
                     cur_node.tracked_borrow_guard().tracked_borrow_pte_token();
                 assert(pa_pte_array_token.value().is_alive(entry.idx as nat));
                 assert(pa_pte_array_token.value().get_paddr(entry.idx as nat)
-                    == cur_node.guard->Some_0.perms@.inner.value()[entry.idx as int].inner.paddr());
+                    == cur_node.guard->Some_0.perms().inner.value()[entry.idx as int].inner.paddr());
                 assert(NodeHelper::in_subtree_range(m.sub_tree_rt(), pt.nid@)) by {
                     assert(NodeHelper::in_subtree_range(m.sub_tree_rt(), cur_node.nid()));
                 }
@@ -574,13 +578,19 @@ fn dfs_acquire_lock(
                 // let va_start = va_range.start.max(child_node_va);
                 // let va_end = va_range.end.min(child_node_va_end);
                 // dfs_acquire_lock(guard, &mut pt_guard, child_node_va, va_start..va_end);
-                assert(pt_guard.guard->Some_0.stray_perm@.value() == false);
+                assert(pt_guard.guard->Some_0.stray_perm().value() == false);
                 let res = dfs_acquire_lock(guard, &pt_guard, Tracked(m));
                 proof {
                     m = res.get();
                 }
+                // Forget the page table guard.
+                assert(pt_guard.guard is Some);
+                let tracked guard = pt_guard.guard.tracked_unwrap()
+                let tracked forgot_guard = guard.inner.get();
+                proof {
+                    forgot_guards.tracked_put(pt.nid@, forgot_guard);
+                }
                 let _ = ManuallyDrop::new(pt_guard);
-
             },
             ChildRef::Frame(_, _, _) => unreached(),
             ChildRef::None => {
@@ -589,7 +599,7 @@ fn dfs_acquire_lock(
                 proof {
                     let ghost nid = NodeHelper::get_child(cur_node.nid(), i as nat);
                     let tracked pte_token: &PteArrayToken =
-                        cur_node.guard.tracked_borrow().pte_token.borrow().tracked_borrow();
+                        cur_node.guard.tracked_borrow().tracked_borrow_pte_token();
                     assert(pte_token.value().is_void(i as nat));
                     assert(NodeHelper::in_subtree_range(m.sub_tree_rt(), nid)) by {
                         NodeHelper::lemma_in_subtree_is_child_in_subtree(
@@ -660,7 +670,7 @@ fn dfs_acquire_lock(
         i += 1;
     }
 
-    Tracked(m)
+    (Tracked(m), Tracked(forgot_guards))
 }
 
 /// Releases the locks for the given range in the sub-tree rooted at the node.
@@ -679,8 +689,8 @@ fn dfs_release_lock<'rcu>(
 ) -> (res: Tracked<LockProtocolModel>)
     requires
         cur_node.wf(),
-        cur_node.guard->Some_0.stray_perm@.value() == false,
-        cur_node.guard->Some_0.in_protocol@ == true,
+        cur_node.guard->Some_0.stray_perm().value() == false,
+        cur_node.guard->Some_0.in_protocol() == true,
         m@.inv(),
         m@.inst_id() == cur_node.inst_id(),
         m@.state() is Locking,
@@ -724,8 +734,8 @@ fn dfs_release_lock<'rcu>(
         invariant
             0 <= i <= 512,
             cur_node.wf(),
-            cur_node.guard->Some_0.stray_perm@.value() == false,
-            cur_node.guard->Some_0.in_protocol@ == true,
+            cur_node.guard->Some_0.stray_perm().value() == false,
+            cur_node.guard->Some_0.in_protocol() == true,
             m.inv(),
             m.inst_id() == cur_node.inst_id(),
             m.state() is Locking,
@@ -807,7 +817,7 @@ fn dfs_release_lock<'rcu>(
                 proof {
                     let ghost nid = NodeHelper::get_child(cur_node.nid(), i as nat);
                     let tracked pte_token: &PteArrayToken =
-                        cur_node.guard.tracked_borrow().pte_token.borrow().tracked_borrow();
+                        cur_node.guard.tracked_borrow().tracked_borrow_pte_token();
                     assert(m.cur_node() == NodeHelper::next_outside_subtree(nid)) by {
                         if i + 1 < 512 {
                             assert(m.cur_node() == NodeHelper::get_child(

lock-protocol/src/exec/rcu/cursor/mod.rs

@@ -5,8 +5,7 @@ use std::{marker::PhantomData, ops::Range};
 use vstd::prelude::*;
 
 use crate::spec::{common::*, utils::*, rcu::*};
-use super::{common::*, types::*, cpu::*};
-use super::page_table::PageTable;
+use super::{common::*, cpu::*};
 use super::node::PageTableGuard;
 use crate::mm::page_table::cursor::MAX_NR_LEVELS;
 use crate::task::DisabledPreemptGuard;

lock-protocol/src/exec/rcu/node/entry.rs

@@ -32,7 +32,7 @@ impl<C: PageTableConfig> Entry<C> {
     pub open spec fn wf(&self, node: PageTableGuard<C>) -> bool {
         &&& self.pte.wf_with_node(*(node.deref().deref()), self.idx as nat)
         &&& 0 <= self.idx < 512
-        &&& node.guard is Some ==> node.guard->Some_0.perms@.relate_pte(self.pte, self.idx as nat)
+        &&& node.guard is Some ==> node.guard->Some_0.perms().relate_pte(self.pte, self.idx as nat)
     }
 
     pub open spec fn nid(&self, node: PageTableGuard<C>) -> NodeId {
@@ -91,14 +91,14 @@ impl<C: PageTableConfig> Entry<C> {
             new_child.wf_with_node(old(self).idx as nat, *old(node)),
             !(new_child is PageTable),
             old(node).wf(),
-            old(node).guard->Some_0.stray_perm@.value() == false,
+            old(node).guard->Some_0.stray_perm().value() == false,
         ensures
             self.wf(*node),
             new_child.wf_into_pte(self.pte),
             self.idx == old(self).idx,
             if res is PageTable {
                 &&& node.wf_except(self.idx as nat)
-                &&& node.guard->Some_0.pte_token@->Some_0.value().is_alive(self.idx as nat)
+                &&& node.guard->Some_0.view_pte_token().value().is_alive(self.idx as nat)
             } else {
                 node.wf()
             },
@@ -128,24 +128,24 @@ impl<C: PageTableConfig> Entry<C> {
             old(self).wf(*old(node)),
             old(node).wf(),
             NodeHelper::is_not_leaf(old(node).nid()),
-            old(node).guard->Some_0.stray_perm@.value() == false,
-            old(node).guard->Some_0.in_protocol@ == false,
+            old(node).guard->Some_0.stray_perm().value() == false,
+            old(node).guard->Some_0.in_protocol() == false,
         ensures
             self.wf(*node),
             self.idx == old(self).idx,
             node.wf(),
             node.inst_id() == old(node).inst_id(),
             node.nid() == old(node).nid(),
             node.inner.deref().level_spec() == old(node).inner.deref().level_spec(),
-            node.guard->Some_0.in_protocol == old(node).guard->Some_0.in_protocol,
+            node.guard->Some_0.in_protocol() == old(node).guard->Some_0.in_protocol(),
             !(old(self).is_none() && old(node).inner.deref().level_spec() > 1) <==> res is None,
             res is Some ==> {
                 &&& res->Some_0.wf()
                 &&& res->Some_0.inst_id() == node.inst_id()
                 &&& res->Some_0.nid() == NodeHelper::get_child(node.nid(), self.idx as nat)
                 &&& res->Some_0.inner.deref().level_spec() + 1 == node.inner.deref().level_spec()
-                &&& res->Some_0.guard->Some_0.stray_perm@.value() == false
-                &&& res->Some_0.guard->Some_0.in_protocol@ == false
+                &&& res->Some_0.guard->Some_0.stray_perm().value() == false
+                &&& res->Some_0.guard->Some_0.in_protocol() == false
             },
     {
         broadcast use group_node_helper_lemmas;
@@ -156,8 +156,9 @@ impl<C: PageTableConfig> Entry<C> {
         let level = node.inner.deref().level();
         let ghost cur_nid = self.nid(*node);
         let mut lock_guard = node.guard.take().unwrap();
-        let tracked node_token = lock_guard.node_token.get().tracked_unwrap();
-        let tracked pte_token = lock_guard.pte_token.get().tracked_unwrap();
+        let tracked mut lock_guard_inner = lock_guard.inner.get();
+        let tracked node_token = lock_guard_inner.node_token.tracked_unwrap();
+        let tracked pte_token = lock_guard_inner.pte_token.tracked_unwrap();
         assert(node_token.value() is LockedOutside);
         assert(pte_token.value().is_void(self.idx as nat));
         assert(cur_nid != NodeHelper::root_id()) by {
@@ -181,8 +182,11 @@ impl<C: PageTableConfig> Entry<C> {
         );
         let new_page = RcuDrop::new(res.0);
         let tracked pte_token = res.1.get();
-        lock_guard.node_token = Tracked(Some(node_token));
-        lock_guard.pte_token = Tracked(Some(pte_token));
+        proof {
+            lock_guard_inner.node_token = Some(node_token);
+            lock_guard_inner.pte_token = Some(pte_token);
+        }
+        lock_guard.inner = Tracked(lock_guard_inner);
         node.guard = Some(lock_guard);
         let paddr = new_page.start_paddr();