diff --git a/ostd/specs/lib.rs b/ostd/specs/lib.rs
index f316bf901..223908e61 100644
--- a/ostd/specs/lib.rs
+++ b/ostd/specs/lib.rs
@@ -12,6 +12,3 @@ pub mod mm;
 #[allow(unused_parens)]
 #[allow(unused_braces)]
 mod sync;
-#[allow(unused_parens)]
-#[allow(unused_braces)]
-pub mod task;
diff --git a/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs b/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs
index ee5981381..b3bad4ba6 100644
--- a/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs
+++ b/ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs
@@ -8,7 +8,7 @@ use crate::specs::mm::frame::meta_owners::{is_mmio_paddr, REF_COUNT_MAX, REF_COU
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::cursor::owners::*;
 use crate::specs::mm::page_table::*;
-use crate::specs::task::InAtomicMode;
+use crate::task::atomic_mode::InAtomicMode;
 
 use core::ops::Range;
 
@@ -16,7 +16,7 @@ verus! {
 
 // ─── Cursor specs ─────────────────────────────────────────────────────────────
 
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> Cursor<'rcu, C> {
     pub open spec fn cursor_new_success_conditions(va: &Range<Vaddr>) -> bool {
         &&& va.start < va.end
         &&& va.start % C::BASE_PAGE_SIZE() == 0
@@ -129,7 +129,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
 
 // ─── CursorMut specs ──────────────────────────────────────────────────────────
 
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> CursorMut<'rcu, C> {
     // TODO: trace the `level >= guard_level` panic to its actual location in `pop_level`
     // (unwrap of None path entry). The lock treatment of the invariant has now been
     // fixed (`Cursor::wf` and `CursorOwner::nodes_locked` are gated on `guard_level`
diff --git a/ostd/specs/mm/page_table/cursor/owners.rs b/ostd/specs/mm/page_table/cursor/owners.rs
index 81d2c2641..77120604e 100644
--- a/ostd/specs/mm/page_table/cursor/owners.rs
+++ b/ostd/specs/mm/page_table/cursor/owners.rs
@@ -33,7 +33,7 @@ use crate::specs::mm::page_table::AbstractVaddr;
 use crate::specs::mm::page_table::Guards;
 use crate::specs::mm::page_table::Mapping;
 use crate::specs::mm::page_table::{nat_align_down, nat_align_up};
-use crate::specs::task::InAtomicMode;
+use crate::task::atomic_mode::InAtomicMode;
 
 verus! {
 
@@ -2523,7 +2523,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
     }
 }
 
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> Inv for Cursor<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> Inv for Cursor<'rcu, C> {
     open spec fn inv(self) -> bool {
         // `level <= NR_LEVELS + 1` (not `<= NR_LEVELS`), mirroring the
         // `guard_level + 1` slack below: it admits the transient "popped
@@ -2548,7 +2548,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Inv for Cursor<'rcu, C, A> {
     }
 }
 
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> OwnerOf for Cursor<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> OwnerOf for Cursor<'rcu, C> {
     type Owner = CursorOwner<'rcu, C>;
 
     open spec fn wf(self, owner: Self::Owner) -> bool {
@@ -2603,7 +2603,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> OwnerOf for Cursor<'rcu, C, A> {
     }
 }
 
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> ModelOf for Cursor<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> ModelOf for Cursor<'rcu, C> {
 
 }
 
diff --git a/ostd/specs/mm/vm_space.rs b/ostd/specs/mm/vm_space.rs
index 2a42363ae..e12eef3d3 100644
--- a/ostd/specs/mm/vm_space.rs
+++ b/ostd/specs/mm/vm_space.rs
@@ -10,6 +10,7 @@ use crate::mm::page_prop::PageProperty;
 use crate::mm::page_table::*;
 use crate::mm::vm_space::{Cursor, CursorMut, MappedItem, UserPtConfig, VmSpace};
 use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr, MAX_USERSPACE_VADDR};
+use crate::task::atomic_mode::InAtomicMode;
 use crate::specs::arch::mm::{current_page_table_paddr_spec, NR_LEVELS};
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::io::{VmIoMemView, VmIoOwner};
@@ -19,7 +20,6 @@ use crate::specs::mm::page_table::node::entry_owners::EntryOwner;
 use crate::specs::mm::page_table::{Guards, Mapping, OwnerSubtree, PageTableOwner, PageTableView};
 use crate::specs::mm::tlb::TlbModel;
 use crate::specs::mm::virt_mem::{FrameContents, MemView};
-use crate::specs::task::InAtomicMode;
 
 verus! {
 
@@ -694,7 +694,7 @@ impl<'a> VmSpace<'a> {
     }
 }
 
-impl<'rcu, A: InAtomicMode> Cursor<'rcu, A> {
+impl<'rcu> Cursor<'rcu> {
     pub open spec fn query_success_requires(self) -> bool {
         self.0.barrier_va.start <= self.0.va < self.0.barrier_va.end
     }
@@ -715,7 +715,7 @@ impl<'rcu, A: InAtomicMode> Cursor<'rcu, A> {
     }
 }
 
-impl<'a, A: InAtomicMode> CursorMut<'a, A> {
+impl<'a> CursorMut<'a> {
     pub open spec fn map_cursor_requires(
         self,
         cursor_owner: CursorOwner<'a, UserPtConfig>,
@@ -744,7 +744,7 @@ impl<'a, A: InAtomicMode> CursorMut<'a, A> {
         &&& self.pt_cursor.0.va + page_size(level) <= self.pt_cursor.0.barrier_va.end
         &&& entry_owner.inv()
         &&& self.pt_cursor.0.va % page_size(level) == 0
-        &&& crate::mm::page_table::CursorMut::<'a, UserPtConfig, A>::item_slot_in_regions(item, regions)
+        &&& crate::mm::page_table::CursorMut::<'a, UserPtConfig>::item_slot_in_regions(item, regions)
     }
 
     pub open spec fn map_item_ensures(
diff --git a/ostd/specs/task/mod.rs b/ostd/specs/task/mod.rs
deleted file mode 100644
index 91b631036..000000000
--- a/ostd/specs/task/mod.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-use vstd::prelude::*;
-
-verus! {
-
-    pub trait InAtomicMode {
-
-    }
-
-    /// A dummy type satisfying [`InAtomicMode`], used when the concrete
-    /// guard type is irrelevant (e.g. in `external_body` stubs).
-    pub struct AnyAtomicGuard;
-    impl InAtomicMode for AnyAtomicGuard {}
-
-} // verus!
diff --git a/ostd/src/mm/kspace/kvirt_area.rs b/ostd/src/mm/kspace/kvirt_area.rs
index 33f5274c4..f4af58c80 100644
--- a/ostd/src/mm/kspace/kvirt_area.rs
+++ b/ostd/src/mm/kspace/kvirt_area.rs
@@ -15,13 +15,15 @@ use super::{
     FRAME_METADATA_BASE_VADDR, KERNEL_BASE_VADDR, KERNEL_END_VADDR, KERNEL_PAGE_TABLE,
     VMALLOC_VADDR_RANGE,
 };
-use crate::mm::{
-    frame::{untyped::AnyUFrameMeta, Frame, Segment},
-    kspace::{KernelPtConfig, MappedItem},
-    largest_pages,
-    page_prop::PageProperty,
-    page_table::{is_valid_range_spec, page_size, Child, CursorMut, PageTable, PageTableConfig},
-    Paddr, Vaddr, PAGE_SIZE,
+use crate::{mm::{
+        frame::{untyped::AnyUFrameMeta, Frame, Segment},
+        kspace::{KernelPtConfig, MappedItem},
+        largest_pages,
+        page_prop::PageProperty,
+        page_table::{is_valid_range_spec, page_size, Child, CursorMut, PageTable, PageTableConfig},
+        Paddr, Vaddr, PAGE_SIZE,
+    },
+    task::disable_preempt,
 };
 
 use crate::mm::frame::DynFrame;
@@ -36,7 +38,7 @@ use crate::specs::mm::frame::meta_owners::{is_mmio_paddr, PageUsage, REF_COUNT_M
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::cursor::{CursorOwner, CursorView};
 use crate::specs::mm::page_table::*;
-use crate::specs::task::InAtomicMode;
+use crate::task::atomic_mode::InAtomicMode;
 
 //static KVIRT_AREA_ALLOCATOR: RangeAllocator = RangeAllocator::new(VMALLOC_VADDR_RANGE);
 
@@ -101,11 +103,6 @@ impl RangeAllocator {
     }
 }
 
-#[verifier::external_body]
-pub fn disable_preempt<'a, G: InAtomicMode + 'a>() -> &'a G {
-    unimplemented!()
-}
-
 exec static KVIRT_AREA_ALLOCATOR: RangeAllocator = RangeAllocator::new(VMALLOC_VADDR_RANGE);
 
 /// Total size (in bytes) of the pages `elems[from..to]`.
@@ -423,7 +420,7 @@ impl KVirtArea {
             self.range.start <= addr < self.range.end
     )]
     #[allow(private_interfaces)]
-    pub fn query<A: InAtomicMode + 'static>(&self, addr: Vaddr) -> Option<super::MappedItem> {
+    pub fn query(&self, addr: Vaddr) -> Option<super::MappedItem> {
         use align_ext::AlignExt;
         assert!(self.start() <= addr && self.end() > addr);
 
@@ -464,10 +461,10 @@ impl KVirtArea {
             proof_decl! { let tracked mut _kpt_owner: Option<&PageTableOwner<KernelPtConfig>> = None; }
             get_kernel_page_table(Tracked(&mut _kpt_owner), Tracked(regions), Tracked(guards))
         };
-        let preempt_guard = disable_preempt::<A>();
+        let preempt_guard = disable_preempt();
         let (mut cursor, Tracked(mut cursor_owner)) = (
         #[verus_spec(with Tracked(owner.pt_owner), Ghost(root_guard), Tracked(regions), Tracked(guards))]
-        page_table.cursor(preempt_guard, &vaddr)).unwrap();
+        page_table.cursor(&preempt_guard, &vaddr)).unwrap();
         proof {
             // Bridge `cursor_owner@.mappings` to `owner.cursor_view_at(addr).mappings`.
             // PageTable::cursor ensures `cursor_owner.as_page_table_owner() == owner.pt_owner`
@@ -601,7 +598,7 @@ impl KVirtArea {
             Tracked(guards): Tracked<&mut Guards<'a, KernelPtConfig>>
     )]
     #[allow(private_interfaces)]
-    pub fn map_frames<'a, A: InAtomicMode + 'a>(
+    pub fn map_frames<'a>(
         area_size: usize,
         map_offset: usize,
         frames: alloc::vec::Vec<DynFrame>,
@@ -629,7 +626,7 @@ impl KVirtArea {
             // with `rc > 0` in the current regions. The runtime invariant of `Frame<M>`
             // implies this; the caller is responsible for projecting it into spec form.
             forall|i: int|
-                0 <= i < frames.len() ==> CursorMut::<'a, KernelPtConfig, A>::item_slot_in_regions(
+                0 <= i < frames.len() ==> CursorMut::<'a, KernelPtConfig>::item_slot_in_regions(
                     MappedItem::Tracked(#[trigger] frames[i], prop),
                     *old(regions),
                 ),
@@ -671,10 +668,10 @@ impl KVirtArea {
                 }
             get_kernel_page_table(Tracked(&mut _kpt_owner), Tracked(regions), Tracked(guards))
         };
-        let preempt_guard = disable_preempt::<A>();
+        let preempt_guard = disable_preempt();
 
         #[verus_spec(with Tracked(owner.pt_owner), Ghost(root_guard), Tracked(regions), Tracked(guards))]
-        let cursor_res = page_table.cursor_mut(preempt_guard, &cursor_range);
+        let cursor_res = page_table.cursor_mut(&preempt_guard, &cursor_range);
 
         proof {
             // Discharge `assert!(cursor_res.is_ok())` via the may_panic chain:
@@ -686,10 +683,7 @@ impl KVirtArea {
             // ⟺ `map_offset >= area_size` ⟹ `bounds_panic_condition`
             // ⟹ `may_panic()` via the requires implication.
             if !cursor_res.is_ok() {
-                assert(!crate::mm::page_table::Cursor::<
-                    KernelPtConfig,
-                    A,
-                >::cursor_new_success_conditions(&cursor_range));
+                assert(!crate::mm::page_table::Cursor::<KernelPtConfig>::cursor_new_success_conditions(&cursor_range));
                 assert(map_offset >= area_size);
                 assert(Self::map_frames_bounds_panic_condition(
                     area_size,
@@ -738,11 +732,7 @@ impl KVirtArea {
                 // `cursor.map`'s effect on unrelated slots — see the focused assume in
                 // the loop body.)
                 forall|i: int|
-                    it.index() <= i < it.seq().len() ==> CursorMut::<
-                        'a,
-                        KernelPtConfig,
-                        A,
-                    >::item_slot_in_regions(
+                    it.index() <= i < it.seq().len() ==> CursorMut::<'a,KernelPtConfig>::item_slot_in_regions(
                         MappedItem::Tracked(#[trigger] it.seq()[i], prop),
                         *regions,
                     ),
@@ -854,7 +844,7 @@ impl KVirtArea {
             // `item_slot_in_regions` for the current item is delivered by the
             // loop invariant (instantiated at i = it.index()), itself established by
             // the function precondition.
-            assert(CursorMut::<'a, KernelPtConfig, A>::item_slot_in_regions(item, *regions));
+            assert(CursorMut::<'a, KernelPtConfig>::item_slot_in_regions(item, *regions));
             proof {
                 // Discharge `cursor.map`'s `map_panic_conditions ==>
                 // may_panic()` via the chain. Most disjuncts of
@@ -900,11 +890,7 @@ impl KVirtArea {
                 let cur_pa = KernelPtConfig::item_into_raw_spec(item).0;
                 let cur_pa_idx = frame_to_index_spec(cur_pa);
                 assert forall|i: int|
-                    (it.index() as int + 1) <= i < it.seq().len() implies CursorMut::<
-                    'a,
-                    KernelPtConfig,
-                    A,
-                >::item_slot_in_regions(
+                    (it.index() as int + 1) <= i < it.seq().len() implies CursorMut::<'a,KernelPtConfig>::item_slot_in_regions(
                     MappedItem::Tracked(#[trigger] it.seq()[i], prop),
                     *regions,
                 ) by {
@@ -917,7 +903,7 @@ impl KVirtArea {
                     // slots-monotonicity and the relevant ref_count fact at
                     // either branch (idx_i != cur_pa_idx via direct equality,
                     // idx_i == cur_pa_idx via mapped-idx > 0 preservation).
-                    assert(CursorMut::<'a, KernelPtConfig, A>::item_slot_in_regions(
+                    assert(CursorMut::<'a, KernelPtConfig>::item_slot_in_regions(
                         item_i,
                         regions_before_map,
                     ));
@@ -1047,7 +1033,7 @@ impl KVirtArea {
             Tracked(guards): Tracked<&mut Guards<'a, KernelPtConfig>>
     )]
     #[allow(private_interfaces)]
-    pub unsafe fn map_untracked_frames<A: InAtomicMode + 'a, 'a>(
+    pub unsafe fn map_untracked_frames<'a>(
         area_size: usize,
         map_offset: usize,
         pa_range: Range<Paddr>,
@@ -1105,10 +1091,7 @@ impl KVirtArea {
                     == 0);
                 assert(va_range.end % <KernelPtConfig as PagingConstsTrait>::BASE_PAGE_SIZE_spec()
                     == 0);
-                assert(crate::mm::page_table::Cursor::<
-                    KernelPtConfig,
-                    A,
-                >::cursor_new_success_conditions(&va_range));
+                assert(crate::mm::page_table::Cursor::<KernelPtConfig>::cursor_new_success_conditions(&va_range));
             }
 
             let page_table = {
@@ -1117,13 +1100,13 @@ impl KVirtArea {
                 }
                 get_kernel_page_table(Tracked(&mut _kpt_owner), Tracked(regions), Tracked(guards))
             };
-            let preempt_guard = disable_preempt::<A>();
+            let preempt_guard = disable_preempt();
 
             // Save regions state before cursor_mut so postcondition trigger can fire.
             let ghost pre_cursor_regions: MetaRegionOwners = *regions;
 
             #[verus_spec(with Tracked(owner.pt_owner), Ghost(root_guard), Tracked(regions), Tracked(guards))]
-            let cursor_res = page_table.cursor_mut(preempt_guard, &va_range);
+            let cursor_res = page_table.cursor_mut(&preempt_guard, &va_range);
 
             assert!(cursor_res.is_ok());
 
@@ -1239,7 +1222,7 @@ impl KVirtArea {
                     assert(regions.slots.contains_key(idx));
                     assert(regions.slot_owners[idx].inner_perms.ref_count.value()
                         != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED);
-                    assert(CursorMut::<'a, KernelPtConfig, A>::item_slot_in_regions(
+                    assert(CursorMut::<'a, KernelPtConfig>::item_slot_in_regions(
                         item,
                         *regions,
                     ));
diff --git a/ostd/src/mm/page_table/cursor/locking.rs b/ostd/src/mm/page_table/cursor/locking.rs
index 0f8b93a08..f5b323a2a 100644
--- a/ostd/src/mm/page_table/cursor/locking.rs
+++ b/ostd/src/mm/page_table/cursor/locking.rs
@@ -6,10 +6,13 @@ use vstd::prelude::*;
 
 use vstd_extra::ownership::*;
 
-use crate::mm::{
-    nr_subpage_per_huge, paddr_to_vaddr, page_table::*, Paddr, PagingConsts, PagingConstsTrait,
-    PagingLevel, Vaddr, NR_ENTRIES, NR_LEVELS, PAGE_SIZE,
+use crate::{
+    mm::{
+        nr_subpage_per_huge, paddr_to_vaddr, page_table::*, Paddr, PagingConsts, PagingConstsTrait,
+        PagingLevel, Vaddr, NR_ENTRIES, NR_LEVELS, PAGE_SIZE,},
+    task::atomic_mode::InAtomicMode,
 };
+use crate::task::DisabledPreemptGuard;
 
 use vstd_extra::array_ptr::*;
 
@@ -17,7 +20,6 @@ use crate::mm::page_table::*;
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::node::entry_owners::EntryOwner;
 use crate::specs::mm::page_table::node::Guards;
-use crate::specs::task::InAtomicMode;
 use vstd_extra::ghost_tree::TreePath;
 
 use align_ext::AlignExt;
@@ -104,15 +106,15 @@ pub assume_specification<Idx: Clone>[ Range::<Idx>::clone ](range: &Range<Idx>)
             ==> final(regions).slot_owners[idx].inner_perms.ref_count.value()
                     == old(regions).slot_owners[idx].inner_perms.ref_count.value(),
         // Frames that were item_not_mapped before remain so after locking.
-        forall|item: C::Item| #![trigger CursorMut::<C, A>::item_not_mapped(item, *old(regions))]
-            CursorMut::<C, A>::item_not_mapped(item, *old(regions)) ==>
-            CursorMut::<C, A>::item_not_mapped(item, *final(regions)),
+        forall|item: C::Item| #![trigger CursorMut::<C>::item_not_mapped(item, *old(regions))]
+            CursorMut::<C>::item_not_mapped(item, *old(regions)) ==>
+            CursorMut::<C>::item_not_mapped(item, *final(regions)),
 )]
-pub fn lock_range<'rcu, C: PageTableConfig, A: InAtomicMode>(
+pub fn lock_range<'rcu, C: PageTableConfig>(
     pt: &'rcu PageTable<C>,
-    guard: &'rcu A,
+    guard: &'rcu dyn InAtomicMode,
     va: &Range<Vaddr>,
-) -> (Cursor<'rcu, C, A>, Tracked<CursorOwner<'rcu, C>>) {
+) -> (Cursor<'rcu, C>, Tracked<CursorOwner<'rcu, C>>) {
     let ghost start_idx = AbstractVaddr::from_vaddr(va.start).index[NR_LEVELS as int - 1];
 
     let tracked mut cursor_own: CursorOwner<'rcu, C> = CursorOwner::tracked_new(
@@ -159,7 +161,7 @@ pub fn lock_range<'rcu, C: PageTableConfig, A: InAtomicMode>(
     path[guard_level as usize - 1] = Some(subtree_root);
 
     let res = (
-        Cursor::<'rcu, C, A> {
+        Cursor::<'rcu, C> {
             path,
             rcu_guard: guard,
             level: guard_level,
@@ -199,7 +201,7 @@ pub fn lock_range<'rcu, C: PageTableConfig, A: InAtomicMode>(
 }
 
 #[verifier::external_body]
-pub fn unlock_range<C: PageTableConfig, A: InAtomicMode>(cursor: &mut Cursor<'_, C, A>) {
+pub fn unlock_range<C: PageTableConfig>(cursor: &mut Cursor<'_, C>) {
     unimplemented!()/*    let end = cursor.guard_level as usize - 1;
     for i in (0..end) {
         if let Some(guard) = cursor.path[end - i].take() {
@@ -304,14 +306,14 @@ pub fn unlock_range<C: PageTableConfig, A: InAtomicMode>(cursor: &mut Cursor<'_,
         // the paddr range's slots either had non-UNUSED ref_count (preserved
         // per above) or UNUSED ref_count (and freshly-allocated PT nodes go
         // into OTHER slot indices, so frame paddrs' paths_in_pt stays empty).
-        forall|item: C::Item| #![trigger CursorMut::<C, A>::item_not_mapped(item, *old(regions))]
-            CursorMut::<C, A>::item_not_mapped(item, *old(regions)) ==>
-            CursorMut::<C, A>::item_not_mapped(item, *final(regions)),
+        forall|item: C::Item| #![trigger CursorMut::<C>::item_not_mapped(item, *old(regions))]
+            CursorMut::<C>::item_not_mapped(item, *old(regions)) ==>
+            CursorMut::<C>::item_not_mapped(item, *final(regions)),
 )]
 #[verifier::external_body]
-fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig, A: InAtomicMode>(
+fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig>(
     pt: &PageTable<C>,
-    guard: &'rcu A,
+    guard: &'rcu dyn InAtomicMode,
     va: &Range<Vaddr>,
 ) -> Option<PageTableGuard<'rcu, C>> {
     let mut cur_node_guard: Option<PageTableGuard<'rcu, C>> = None;
@@ -500,8 +502,8 @@ fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig, A: InAtomicMode>
         final(regions).slot_owners =~= old(regions).slot_owners,
 )]
 #[verifier::external_body]
-fn dfs_acquire_lock<'rcu, C: PageTableConfig, A: InAtomicMode>(
-    guard: &A,
+fn dfs_acquire_lock<'rcu, C: PageTableConfig>(
+    guard: & dyn InAtomicMode,
     cur_node: &mut PageTableGuard<'rcu, C>,
     cur_node_va: Vaddr,
     va_range: Range<Vaddr>,
@@ -629,8 +631,8 @@ unsafe fn dfs_release_lock<'rcu, C: PageTableConfig, A: InAtomicMode>(
         forall |addr: usize| addr != locked_addr && old(guards).lock_held(addr) ==> final(guards).lock_held(addr),
 )]
 #[verifier::external_body]
-pub fn dfs_mark_stray_and_unlock<'a, C: PageTableConfig, A: InAtomicMode>(
-    rcu_guard: &A,
+pub fn dfs_mark_stray_and_unlock<'a, C: PageTableConfig>(
+    rcu_guard: & dyn InAtomicMode,
     sub_tree: &PageTableGuard<'a, C>,
 ) -> usize {
     unimplemented!();
diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs
index 2234d869c..f90fd45d0 100644
--- a/ostd/src/mm/page_table/cursor/mod.rs
+++ b/ostd/src/mm/page_table/cursor/mod.rs
@@ -53,6 +53,7 @@ use crate::specs::mm::frame::meta_owners::{
 };
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::cursor::page_size_lemmas::*;
+use crate::task::DisabledPreemptGuard;
 
 use core::{fmt::Debug, marker::PhantomData, ops::Range};
 
@@ -60,7 +61,7 @@ use align_ext::AlignExt;
 
 use crate::{
     mm::{page_prop::PageProperty, page_table::is_valid_range},
-    specs::task::InAtomicMode,
+    task::atomic_mode::InAtomicMode,
 };
 
 use super::{
@@ -82,14 +83,14 @@ pub type PagesState<C> = (Range<Vaddr>, Option<<C as PageTableConfig>::Item>);
 ///
 /// A cursor is able to move to the next slot, to read page properties,
 /// and even to jump to a virtual address directly.
-pub struct Cursor<'rcu, C: PageTableConfig, A: InAtomicMode> {
+pub struct Cursor<'rcu, C: PageTableConfig> {
     /// The current path of the cursor.
     ///
     /// The level 1 page table lock guard is at index 0, and the level N page
     /// table lock guard is at index N - 1.
     pub path: [Option<PageTableGuard<'rcu, C>>; NR_LEVELS],
     /// The cursor should be used in a RCU read side critical section.
-    pub rcu_guard: &'rcu A,
+    pub rcu_guard: &'rcu dyn InAtomicMode,
     /// The level of the page table that the cursor currently points to.
     pub level: PagingLevel,
     /// The top-most level that the cursor is allowed to access.
@@ -109,9 +110,9 @@ pub struct Cursor<'rcu, C: PageTableConfig, A: InAtomicMode> {
 /// page table corresponding to the address range. A virtual address range
 /// in a page table can only be accessed by one cursor, regardless of the
 /// mutability of the cursor.
-pub struct CursorMut<'rcu, C: PageTableConfig, A: InAtomicMode>(pub Cursor<'rcu, C, A>);
+pub struct CursorMut<'rcu, C: PageTableConfig>(pub Cursor<'rcu, C>);
 
-impl<C: PageTableConfig, A: InAtomicMode> Iterator for Cursor<'_, C, A> {
+impl<C: PageTableConfig> Iterator for Cursor<'_, C> {
     type Item = PagesState<C>;
 
     #[verifier::external_body]
@@ -218,7 +219,7 @@ impl<C: PageTableConfig> PageTableFrag<C> {
 }
 
 #[verus_verify]
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> Cursor<'rcu, C> {
     #[verus_spec(
         with Tracked(regions): Tracked<&mut MetaRegionOwners>,
             Ghost(pa): Ghost<Paddr>)]
@@ -342,9 +343,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
                     >= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX
                 ==> final(regions).slot_owners[idx].inner_perms.ref_count.value()
                         == old(regions).slot_owners[idx].inner_perms.ref_count.value(),
-            forall|item: C::Item| #![trigger CursorMut::<C, A>::item_not_mapped(item, *old(regions))]
-                CursorMut::<C, A>::item_not_mapped(item, *old(regions)) ==>
-                CursorMut::<C, A>::item_not_mapped(item, *final(regions)),
+            forall|item: C::Item| #![trigger CursorMut::<C>::item_not_mapped(item, *old(regions))]
+                CursorMut::<C>::item_not_mapped(item, *old(regions)) ==>
+                CursorMut::<C>::item_not_mapped(item, *final(regions)),
             // Non-saturation preservation.
             (forall |i: usize| #![trigger old(regions).slot_owners[i]]
                 old(regions).slot_owners.contains_key(i)
@@ -360,7 +361,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
                 ==> final(regions).slot_owners[i].inner_perms.ref_count.value() + 1
                     < crate::specs::mm::frame::meta_owners::REF_COUNT_MAX),
     )]
-    pub fn new(pt: &'rcu PageTable<C>, guard: &'rcu A, va: &Range<Vaddr>) -> Result<
+    pub fn new(pt: &'rcu PageTable<C>, guard: &'rcu dyn InAtomicMode, va: &Range<Vaddr>) -> Result<
         (Self, Tracked<CursorOwner<'rcu, C>>),
         PageTableError,
     > {
@@ -2059,7 +2060,7 @@ impl<C: PageTableConfig> Drop for Cursor<'_, C> {
 */
 
 #[verus_verify]
-impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
+impl<'rcu, C: PageTableConfig> CursorMut<'rcu, C> {
     /// Creates a cursor claiming exclusive access over the given range.
     ///
     /// The cursor created will only be able to map, query or jump within the given
@@ -2075,7 +2076,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
             // Per-config tightening; see `Cursor::new`.
             va.end as int <= C::LOCKED_END_BOUND_spec(),
         ensures
-            Cursor::<C, A>::cursor_new_success_conditions(va) ==> {
+            Cursor::<C>::cursor_new_success_conditions(va) ==> {
                 &&& r is Ok
                 &&& r.unwrap().0.0.invariants(*r.unwrap().1, *final(regions), *final(guards))
                 &&& r.unwrap().1.in_locked_range()
@@ -2084,7 +2085,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                 &&& r.unwrap().0.0.va == va.start
                 &&& r.unwrap().0.0.barrier_va == *va
             },
-            !Cursor::<C, A>::cursor_new_success_conditions(va) ==> r is Err,
+            !Cursor::<C>::cursor_new_success_conditions(va) ==> r is Err,
             // cursor_mut only acquires locks on page-table node slots; it does not
             // set paths_in_pt for data-frame slots. Any frame that was item_not_mapped
             // before the call remains item_not_mapped after.
@@ -2100,7 +2101,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                 ==> final(regions).slot_owners[idx].paths_in_pt
                         == old(regions).slot_owners[idx].paths_in_pt,
     )]
-    pub fn new(pt: &'rcu PageTable<C>, guard: &'rcu A, va: &Range<Vaddr>) -> Result<
+    pub fn new(pt: &'rcu PageTable<C>, guard: &'rcu dyn InAtomicMode, va: &Range<Vaddr>) -> Result<
         (Self, Tracked<CursorOwner<'rcu, C>>),
         PageTableError,
     > {
@@ -2114,7 +2115,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                     // (from !conditions ==> Err, contrapositive gives Ok ==> conditions).
                     // Therefore the success-case ensures apply, giving us invariants.
                     assert(inner_cursor.invariants(*tracked_owner, *regions, *guards));
-                    assert(CursorMut::<C, A>(inner_cursor).0.invariants(
+                    assert(CursorMut::<C>(inner_cursor).0.invariants(
                         *tracked_owner,
                         *regions,
                         *guards,
@@ -2301,7 +2302,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
             final(owner)@ == old(owner)@,
             *final(regions) == *old(regions),
     )]
-    fn map_branch_pt(&mut self, pt: PageTableNodeRef<'rcu, C>, rcu_guard: &'rcu A) {
+    fn map_branch_pt(&mut self, pt: PageTableNodeRef<'rcu, C>, rcu_guard: &'rcu dyn InAtomicMode) {
         let ghost guards0 = *guards;
 
         let ghost level_key = owner.level as int - 1;
@@ -2371,7 +2372,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
             forall|idx: usize| #![trigger final(regions).slots.contains_key(idx)]
                 old(regions).slots.contains_key(idx) ==> final(regions).slots.contains_key(idx),
     )]
-    pub fn map_loop(&mut self, level: PagingLevel, rcu_guard: &'rcu A) {
+    pub fn map_loop(&mut self, level: PagingLevel, rcu_guard: &'rcu dyn InAtomicMode) {
         let ghost guard_level = self.0.guard_level;
         let ghost barrier_va = self.0.barrier_va;
         let ghost owner0 = *owner;
diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs
index 22e94fcc9..80503d514 100644
--- a/ostd/src/mm/page_table/mod.rs
+++ b/ostd/src/mm/page_table/mod.rs
@@ -26,10 +26,9 @@ use crate::specs::mm::page_table::*;
 use crate::specs::arch::mm::*;
 use crate::specs::arch::paging_consts::PagingConsts;
 use crate::specs::mm::page_table::cursor::*;
-use crate::specs::task::InAtomicMode;
 
 use crate::mm::frame::meta::mapping::frame_to_index;
-use crate::mm::kspace::kvirt_area::disable_preempt;
+use crate::task::{atomic_mode::InAtomicMode, disable_preempt};
 use crate::specs::arch::PageTableEntry;
 use crate::specs::mm::frame::meta_owners::MetaPerm;
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
@@ -1122,10 +1121,10 @@ impl PageTable<KernelPtConfig> {
         ensures
             final(regions).inv(),
     )]
-    pub(in crate::mm) fn create_user_page_table<G: InAtomicMode + 'static>(
+    pub(in crate::mm) fn create_user_page_table(
         &'static self,
     ) -> PageTable<UserPtConfig> {
-        let preempt_guard: &G = disable_preempt::<G>();
+        let preempt_guard= disable_preempt();
 
         proof_decl! {
             let tracked mut new_pt_owner: Option<PageTableOwner<UserPtConfig>> = None;
@@ -1188,14 +1187,14 @@ impl PageTable<KernelPtConfig> {
             #[verus_spec(with Tracked(regions), Tracked(root_perm))]
             let root_ref = self.root.borrow();
             #[verus_spec(with Tracked(root_owner), Tracked(guards_k))]
-            root_ref.lock(preempt_guard)
+            root_ref.lock(&preempt_guard)
         };
         let ghost regions_after_kroot_borrow: MetaRegionOwners = *regions;
-        let mut new_node: PageTableGuard<'static, UserPtConfig> = {
+        let mut new_node = {
             #[verus_spec(with Tracked(regions), Tracked(&new_node_owner.meta_perm))]
             let new_ref = new_root.borrow();
             #[verus_spec(with Tracked(&new_node_owner), Tracked(guards_u))]
-            new_ref.lock(preempt_guard)
+            new_ref.lock(&preempt_guard)
         };
         proof {
             // Each `borrow` adjusts raw_count to 1 at one slot index. For the kernel
@@ -1624,7 +1623,7 @@ impl<C: PageTableConfig> PageTable<C> {
             // Per-config tightening; see `Cursor::new`.
             va.end as int <= C::LOCKED_END_BOUND_spec(),
         ensures
-            Cursor::<C, G>::cursor_new_success_conditions(va) ==> {
+            Cursor::<C>::cursor_new_success_conditions(va) ==> {
                 &&& r is Ok
                 &&& r.unwrap().0.0.invariants(*r.unwrap().1, *final(regions), *final(guards))
                 &&& r.unwrap().1.in_locked_range()
@@ -1634,20 +1633,25 @@ impl<C: PageTableConfig> PageTable<C> {
                 &&& r.unwrap().0.0.va == va.start
                 &&& r.unwrap().0.0.barrier_va == *va
             },
-            !Cursor::<C, G>::cursor_new_success_conditions(va) ==> r is Err,
-            forall |item: C::Item| #![trigger CursorMut::<'rcu, C, G>::item_not_mapped(item, *old(regions))]
-                CursorMut::<'rcu, C, G>::item_not_mapped(item, *old(regions)) ==>
-                CursorMut::<'rcu, C, G>::item_not_mapped(item, *final(regions)),
+            !Cursor::<C>::cursor_new_success_conditions(va) ==> r is Err,
+            forall |item: C::Item| #![trigger CursorMut::<'rcu, C>::item_not_mapped(item, *old(regions))]
+                CursorMut::<'rcu, C>::item_not_mapped(item, *old(regions)) ==>
+                CursorMut::<'rcu, C>::item_not_mapped(item, *final(regions)),
             // cursor_mut only locks page-table node slots; paths_in_pt is unchanged for all slots.
             forall |idx: usize| #![auto]
                 (*final(regions)).slot_owners[idx].paths_in_pt == (*old(regions)).slot_owners[idx].paths_in_pt,
     )]
     #[verifier::external_body]
-    pub fn cursor_mut<'rcu, G: InAtomicMode>(
+    /* pub fn cursor_mut<'rcu, G: AsAtomicModeGuard>(
         &'rcu self,
         guard: &'rcu G,
         va: &Range<Vaddr>,
-    ) -> Result<(CursorMut<'rcu, C, G>, Tracked<CursorOwner<'rcu, C>>), PageTableError> {
+    ) -> Result<CursorMut<'rcu, C>, PageTableError>*/
+    pub fn cursor_mut<'rcu>(
+        &'rcu self,
+        guard: &'rcu dyn InAtomicMode,
+        va: &Range<Vaddr>,
+    ) -> Result<(CursorMut<'rcu, C>, Tracked<CursorOwner<'rcu, C>>), PageTableError> {
         #[verus_spec(with Tracked(owner), Ghost(root_guard), Tracked(regions), Tracked(guards))]
         CursorMut::new(self, guard, va)
     }
@@ -1667,7 +1671,7 @@ impl<C: PageTableConfig> PageTable<C> {
             // Per-config tightening; see `Cursor::new`.
             va.end as int <= C::LOCKED_END_BOUND_spec(),
         ensures
-            Cursor::<C, G>::cursor_new_success_conditions(va) ==> {
+            Cursor::<C>::cursor_new_success_conditions(va) ==> {
                 &&& r is Ok
                 &&& r.unwrap().0.invariants(*r.unwrap().1, *final(regions), *final(guards))
                 &&& r.unwrap().1.in_locked_range()
@@ -1678,7 +1682,7 @@ impl<C: PageTableConfig> PageTable<C> {
                 &&& r.unwrap().1@.as_page_table_owner() == owner
                 &&& r.unwrap().1@.continuations[3].path() == owner.0.value.path
             },
-            !Cursor::<C, G>::cursor_new_success_conditions(va) ==> r is Err,
+            !Cursor::<C>::cursor_new_success_conditions(va) ==> r is Err,
             forall|idx: usize| #![trigger final(regions).slot_owners[idx].paths_in_pt]
                 old(regions).slot_owners[idx].inner_perms.ref_count.value()
                     != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
@@ -1713,8 +1717,13 @@ impl<C: PageTableConfig> PageTable<C> {
                 ==> final(regions).slot_owners[idx].inner_perms.ref_count.value()
                         == old(regions).slot_owners[idx].inner_perms.ref_count.value(),
     )]
-    pub fn cursor<'rcu, G: InAtomicMode>(&'rcu self, guard: &'rcu G, va: &Range<Vaddr>) -> Result<
-        (Cursor<'rcu, C, G>, Tracked<CursorOwner<'rcu, C>>),
+    /* pub fn cursor<'rcu, G: AsAtomicModeGuard>(
+        &'rcu self,
+        guard: &'rcu G,
+        va: &Range<Vaddr>,
+    )*/
+    pub fn cursor<'rcu>(&'rcu self, guard: &'rcu dyn InAtomicMode, va: &Range<Vaddr>) -> Result<
+        (Cursor<'rcu, C>, Tracked<CursorOwner<'rcu, C>>),
         PageTableError,
     > {
         #[verus_spec(with Tracked(owner), Ghost(root_guard), Tracked(regions), Tracked(guards))]
diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs
index 342f926c0..6aa3a387e 100644
--- a/ostd/src/mm/page_table/node/entry.rs
+++ b/ostd/src/mm/page_table/node/entry.rs
@@ -16,7 +16,6 @@ use crate::specs::arch::paging_consts::PagingConsts;
 use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, REF_COUNT_UNUSED};
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::{PageTableOwner, INC_LEVELS};
-use crate::specs::task::InAtomicMode;
 
 use core::marker::PhantomData;
 use core::ops::Deref;
@@ -24,7 +23,7 @@ use core::ops::Deref;
 use crate::{
     mm::{nr_subpage_per_huge, page_prop::PageProperty},
     //    sync::RcuDrop,
-    //    task::atomic_mode::InAtomicMode,
+    task::atomic_mode::InAtomicMode,
 };
 
 use super::*;
@@ -587,7 +586,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
             forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
             forall |i: usize| old(guards).unlocked(i) && i != final(owner).value.node.unwrap().meta_perm.addr() ==> final(guards).unlocked(i),
     )]
-    pub(in crate::mm) fn alloc_if_none<A: InAtomicMode>(&mut self, guard: &'rcu A) -> (res: Option<
+    pub(in crate::mm) fn alloc_if_none(&mut self, guard: &'rcu dyn InAtomicMode) -> (res: Option<
         PageTableGuard<'rcu, C>,
     >) {
         let entry_is_present = self.pte.is_present();
@@ -806,7 +805,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
                     #[trigger] final(parent_owner).children_perm.value()[j]
                         == old(parent_owner).children_perm.value()[j],
     )]
-    pub(in crate::mm) fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A) -> (res:
+    pub(in crate::mm) fn split_if_mapped_huge(&mut self, guard: &'rcu dyn InAtomicMode) -> (res:
         Option<PageTableGuard<'rcu, C>>) {
         #[verus_spec(with Tracked(&parent_owner.meta_perm))]
         let level = self.node.level();
diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs
index 098e01dec..c61226a7d 100644
--- a/ostd/src/mm/page_table/node/mod.rs
+++ b/ostd/src/mm/page_table/node/mod.rs
@@ -32,6 +32,7 @@ mod child_specs;
 mod entry_specs;
 
 pub use crate::specs::mm::page_table::node::{entry_owners::*, owners::*};
+use crate::task::DisabledPreemptGuard;
 pub use child::*;
 pub use entry::*;
 
@@ -69,7 +70,7 @@ use crate::{
         //        FrameAllocOptions, Infallible,
         //        VmReader,
     },
-    specs::task::InAtomicMode,
+    task::atomic_mode::InAtomicMode,
 };
 
 verus! {
@@ -292,7 +293,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
             Self::locks_preserved_except(owner.meta_perm.addr(), *old(guards), *final(guards)),
             owner.relate_guard(res),
     )]
-    pub fn lock<'rcu, A: InAtomicMode>(self, _guard: &'rcu A) -> PageTableGuard<'rcu, C> where
+    pub fn lock<'rcu>(self, _guard: &'rcu dyn InAtomicMode) -> PageTableGuard<'rcu, C> where
         'a: 'rcu,
      {
         unimplemented!()
@@ -317,7 +318,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
             Self::locks_preserved_except(owner.meta_perm.addr(), *old(guards), *final(guards)),
             owner.relate_guard(res),
     )]
-    pub fn make_guard_unchecked<'rcu, A: InAtomicMode>(self, _guard: &'rcu A) -> PageTableGuard<
+    pub fn make_guard_unchecked<'rcu>(self, _guard: &'rcu dyn InAtomicMode) -> PageTableGuard<
         'rcu,
         C,
     > where 'a: 'rcu {
diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs
index 479ae5a78..8d24bf9e7 100644
--- a/ostd/src/mm/vm_space.rs
+++ b/ostd/src/mm/vm_space.rs
@@ -21,6 +21,7 @@ use crate::mm::frame::MetaSlot;
 use crate::mm::kspace::KernelPtConfig;
 use crate::mm::page_table::*;
 use crate::mm::page_table::{EntryOwner, PageTableFrag, PageTableGuard};
+use crate::task::atomic_mode::InAtomicMode;
 use crate::specs::arch::*;
 use crate::specs::mm::frame::mapping::meta_to_frame;
 use crate::specs::mm::frame::meta_owners::{MetaPerm, MetaSlotStorage, MetadataInnerPerms};
@@ -29,7 +30,6 @@ use crate::specs::mm::io::VmIoMemView;
 use crate::specs::mm::page_table::cursor::owners::CursorOwner;
 use crate::specs::mm::page_table::*;
 use crate::specs::mm::tlb::TlbModel;
-use crate::specs::task::InAtomicMode;
 use core::marker::PhantomData;
 use core::{ops::Range, sync::atomic::Ordering};
 use vstd_extra::ghost_tree::*;
@@ -200,7 +200,7 @@ impl<'a> VmSpace<'a> {
         }
         let pt = {
             #[verus_spec(with Tracked(kernel_owner), Tracked(regions), Tracked(guards_k), Tracked(guards_u))]
-            kpt.create_user_page_table::<crate::specs::task::AnyAtomicGuard>()
+            kpt.create_user_page_table()
         };
         Self { pt, cpus: AtomicCpuSet::new(CpuSet::new_empty()), _marker: PhantomData }
     }
@@ -230,7 +230,7 @@ impl<'a> VmSpace<'a> {
         requires
             owner.inv(),
         ensures
-            crate::mm::page_table::Cursor::<UserPtConfig, G>::cursor_new_success_conditions(va) ==> (r matches Ok(_) && cursor_owner@ matches Some(_)),
+            crate::mm::page_table::Cursor::<UserPtConfig>::cursor_new_success_conditions(va) ==> (r matches Ok(_) && cursor_owner@ matches Some(_)),
             // On the success branch, the returned cursor owner satisfies
             // its invariant. Follows from the underlying PT::cursor's
             // ensures: r is Ok ⇒ cursor_new_success_conditions (by
@@ -238,8 +238,13 @@ impl<'a> VmSpace<'a> {
             // hold ⇒ cursor_owner.inv().
             cursor_owner@ matches Some(c) ==> c.inv(),
     )]
-    pub fn cursor<G: InAtomicMode>(&'a self, guard: &'a G, va: &Range<Vaddr>) -> Result<
-        Cursor<'a, G>,
+    /* pub fn cursor<'rcu, G: AsAtomicModeGuard>(
+        &'rcu self,
+        guard: &'rcu G,
+        va: &Range<Vaddr>,
+    )*/
+    pub fn cursor(&'a self, guard: &'a dyn InAtomicMode, va: &Range<Vaddr>) -> Result<
+        Cursor<'a>,
     > {
         proof_decl! {
             let tracked mut out_owner: Option<CursorOwner<'a, UserPtConfig>>;
@@ -288,12 +293,17 @@ impl<'a> VmSpace<'a> {
         requires
             owner.inv(),
         ensures
-            crate::mm::page_table::Cursor::<UserPtConfig, G>::cursor_new_success_conditions(va) ==> (r matches Ok(_) && cursor_owner@ matches Some(_)),
+            crate::mm::page_table::Cursor::<UserPtConfig>::cursor_new_success_conditions(va) ==> (r matches Ok(_) && cursor_owner@ matches Some(_)),
             // See `cursor` above for the derivation.
             cursor_owner@ matches Some(c) ==> c.inv(),
     )]
-    pub fn cursor_mut<G: InAtomicMode>(&'a self, guard: &'a G, va: &Range<Vaddr>) -> Result<
-        CursorMut<'a, G>,
+    /*pub fn cursor_mut<'rcu, G: AsAtomicModeGuard>(
+        &'rcu self,
+        guard: &'rcu G,
+        va: &Range<Vaddr>,
+    ) -> Result<CursorMut<'rcu, C>, PageTableError> */
+    pub fn cursor_mut(&'a self, guard: &'a dyn InAtomicMode, va: &Range<Vaddr>) -> Result<
+        CursorMut<'a>,
     > {
         proof_decl! {
             let tracked mut out_owner: Option<CursorOwner<'a, UserPtConfig>>;
@@ -437,10 +447,10 @@ impl<'a> VmSpace<'a> {
 /// It exclusively owns a sub-tree of the page table, preventing others from
 /// reading or modifying the same sub-tree. Two read-only cursors can not be
 /// created from the same virtual address range either.
-pub struct Cursor<'a, A: InAtomicMode>(pub crate::mm::page_table::Cursor<'a, UserPtConfig, A>);
+pub struct Cursor<'a>(pub crate::mm::page_table::Cursor<'a, UserPtConfig>);
 
 #[verus_verify]
-impl<'rcu, A: InAtomicMode> Cursor<'rcu, A> {
+impl<'rcu> Cursor<'rcu> {
     /// Queries the mapping at the current virtual address.
     ///
     /// If the cursor is pointing to a valid virtual address that is locked,
@@ -597,15 +607,15 @@ impl<'rcu, A: InAtomicMode> Cursor<'rcu, A> {
 ///
 /// It exclusively owns a sub-tree of the page table, preventing others from
 /// reading or modifying the same sub-tree.
-pub struct CursorMut<'a, A: InAtomicMode> {
-    pub pt_cursor: crate::mm::page_table::CursorMut<'a, UserPtConfig, A>,
+pub struct CursorMut<'a> {
+    pub pt_cursor: crate::mm::page_table::CursorMut<'a, UserPtConfig>,
     // We have a read lock so the CPU set in the flusher is always a superset
     // of actual activated CPUs.
     pub flusher: TlbFlusher<'a  /*, DisabledPreemptGuard*/ >,
 }
 
 #[verus_verify]
-impl<'a, A: InAtomicMode> CursorMut<'a, A> {
+impl<'a> CursorMut<'a> {
     /// Queries the mapping at the current virtual address.
     ///
     /// This is the same as [`Cursor::query`].
diff --git a/ostd/src/sync/rcu/mod.rs b/ostd/src/sync/rcu/mod.rs
index 2df43a8ae..dbc6bfe71 100644
--- a/ostd/src/sync/rcu/mod.rs
+++ b/ostd/src/sync/rcu/mod.rs
@@ -32,7 +32,7 @@ use super::Once;
 
 use self::monitor::{RcuMonitor, RcuMonitorOwner, RcuMonitorPred};
 use crate::task::{
-    //atomic_mode::{AsAtomicModeGuard, InAtomicMode},
+    atomic_mode::{/*AsAtomicModeGuard,*/ InAtomicMode},
     disable_preempt,
     DisabledPreemptGuard,
 };
@@ -40,8 +40,6 @@ use crate::task::{
 mod monitor;
 pub mod non_null;
 
-use crate::specs::task::InAtomicMode;
-
 verus! {
 
 broadcast use vstd_extra::external::nonnull::group_nonull_axioms;
diff --git a/ostd/src/task/atomic_mode.rs b/ostd/src/task/atomic_mode.rs
index 4986747ca..52461723e 100644
--- a/ostd/src/task/atomic_mode.rs
+++ b/ostd/src/task/atomic_mode.rs
@@ -25,8 +25,10 @@
 //! 2. Switching to user space.
 //!
 //! This module provides API to detect such "sleep-like" actions.
-use core::sync::atomic::Ordering;
+use vstd::prelude::*;
 
+use core::sync::atomic::Ordering;
+/* 
 /// Marks a function as one that might sleep.
 ///
 /// This function will panic if it is executed in atomic mode.
@@ -43,7 +45,7 @@ pub fn might_sleep() {
         );
     }
 }
-
+*/
 /// A marker trait for guard types that enforce the atomic mode.
 ///
 /// Key kernel primitives such as `SpinLock` and `Rcu` rely on
@@ -58,8 +60,9 @@ pub fn might_sleep() {
 ///
 /// The implementer must ensure that the atomic mode is maintained while
 /// the guard type is alive.
-pub unsafe trait InAtomicMode: core::fmt::Debug {}
-
+#[verus_verify]
+pub unsafe trait InAtomicMode/* : core::fmt::Debug*/ {}
+/* 
 /// Abstracts any type from which one can obtain a reference to an atomic-mode guard.
 pub trait AsAtomicModeGuard {
     /// Returns a guard for the atomic mode.
@@ -77,3 +80,4 @@ impl AsAtomicModeGuard for dyn InAtomicMode + '_ {
         self
     }
 }
+*/
\ No newline at end of file
diff --git a/ostd/src/task/mod.rs b/ostd/src/task/mod.rs
index 305b6b3c5..bc6a26ecb 100644
--- a/ostd/src/task/mod.rs
+++ b/ostd/src/task/mod.rs
@@ -2,8 +2,8 @@
 //! Tasks are the unit of code execution.
 use vstd::prelude::*;
 
-/* pub mod atomic_mode;
-mod kernel_stack; */
+pub mod atomic_mode;
+/* mod kernel_stack; */
 mod preempt;
 // mod processor;
 pub mod scheduler;
diff --git a/ostd/src/task/preempt/guard.rs b/ostd/src/task/preempt/guard.rs
index 8e44ce12b..4a91d2bb7 100644
--- a/ostd/src/task/preempt/guard.rs
+++ b/ostd/src/task/preempt/guard.rs
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
 use vstd::prelude::*;
 
-use crate::{sync::GuardTransfer /*, task::atomic_mode::InAtomicMode*/};
+use crate::{sync::GuardTransfer, task::atomic_mode::InAtomicMode};
 
 /// A guard for disable preempt.
 #[verus_verify]
@@ -13,12 +13,14 @@ pub struct DisabledPreemptGuard {
     _private: (),
 }
 
-/* impl !Send for DisabledPreemptGuard {}
+impl !Send for DisabledPreemptGuard {}
 
 // SAFETY: The guard disables preemptions, which meets the second
 // sufficient condition for atomic mode.
+#[verifier::external]
 unsafe impl InAtomicMode for DisabledPreemptGuard {}
 
+/*
 impl DisabledPreemptGuard {
     fn new() -> Self {
         super::cpu_local::inc_guard_count();