Trivial merge

Author: Xungan2

lock-protocol/src/exec/mod.rs

@@ -1,5 +1,5 @@
-mod rcu;
-mod rw;
+// mod rcu;
+// mod rw;
 // mod test_map;
 
 use vstd::{invariant, prelude::*};

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

@@ -588,7 +588,7 @@ fn dfs_acquire_lock(
                 let tracked guard = pt_guard.guard.tracked_unwrap()
                 let tracked forgot_guard = guard.inner.get();
                 proof {
-                    forgot_guards.tracked_put(, forgot_guard);
+                    forgot_guards.tracked_put(pt.nid@, forgot_guard);
                 }
                 let _ = ManuallyDrop::new(pt_guard);
             },
@@ -670,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.

lock-protocol/src/mm/frame_concurrent/meta/mapping.rs

@@ -0,0 +1,44 @@
+use core::ops::Range;
+use core::mem::size_of;
+
+use vstd::prelude::*;
+
+use crate::mm::lock_protocol_utils::*;
+use super::MetaSlot;
+
+verus! {
+
+// global layout MetaSlot is size == 12, align == 12;
+pub uninterp spec fn frame_to_meta_spec(paddr: Paddr) -> Vaddr;
+
+/// Converts a physical address of a base frame to the virtual address of the metadata slot.
+#[inline(always)]
+#[verifier::when_used_as_spec(frame_to_meta_spec)]
+#[verifier::external_body]
+pub const fn frame_to_meta(paddr: Paddr) -> Vaddr
+    returns
+        frame_to_meta_spec(paddr),
+{
+    // let base = FRAME_METADATA_RANGE.start;
+    // let offset = paddr / PAGE_SIZE;
+    // base + offset * size_of::<MetaSlot>()
+    unimplemented!()
+}
+
+pub uninterp spec fn meta_to_frame_spec(vaddr: Vaddr) -> Paddr;
+
+/// Converts a virtual address of the metadata slot to the physical address of the frame.
+#[inline(always)]
+#[verifier::when_used_as_spec(meta_to_frame_spec)]
+#[verifier::external_body]
+pub const fn meta_to_frame(vaddr: Vaddr) -> Paddr
+    returns
+        meta_to_frame_spec(vaddr),
+{
+    // let base = FRAME_METADATA_RANGE.start;
+    // let offset = (vaddr - base) / size_of::<MetaSlot>();
+    // offset * PAGE_SIZE
+    unimplemented!()
+}
+
+} // verus!

lock-protocol/src/mm/frame_concurrent/meta/mod.rs

@@ -0,0 +1,95 @@
+pub mod mapping;
+
+use vstd::prelude::*;
+use vstd::raw_ptr::{PointsTo};
+
+use crate::spec::{common::*, utils::*, rcu::*};
+use crate::mm::lock_protocol_utils::*;
+use crate::mm::page_table::node_concurrent::PageTablePageMeta;
+use crate::mm::page_table::PageTableConfig;
+
+pub use mapping::*;
+
+verus! {
+
+pub enum MetaSlotType {
+    PageTablePageMeta,
+    Others,
+}
+
+struct_with_invariants! {
+    pub struct MetaSlot<C: PageTableConfig> {
+        pub usage: MetaSlotType,
+        pub inner: Option<PageTablePageMeta<C>>,
+    }
+
+    pub open spec fn wf(&self) -> bool {
+        predicate {
+            &&& self.usage is PageTablePageMeta <==> self.inner is Some
+            &&& self.inner is Some ==> self.inner->Some_0.wf()
+        }
+    }
+}
+
+impl<C: PageTableConfig> MetaSlot<C> {
+    pub open spec fn is_pt(&self) -> bool {
+        self.usage is PageTablePageMeta
+    }
+
+    pub open spec fn get_inner_pt_spec(&self) -> PageTablePageMeta<C>
+        recommends
+            self.is_pt(),
+    {
+        self.inner->Some_0
+    }
+
+    pub fn get_inner_pt(&self) -> (res: &PageTablePageMeta<C>)
+        requires
+            self.wf(),
+            self.is_pt(),
+        ensures
+            *res =~= self.get_inner_pt_spec(),
+    {
+        self.inner.as_ref().unwrap()
+    }
+}
+
+pub tracked struct MetaSlotPerm<C: PageTableConfig> {
+    pub inner: PointsTo<MetaSlot<C>>,
+    pub slot_idx: nat,
+}
+
+impl<C: PageTableConfig> MetaSlotPerm<C> {
+    pub open spec fn relate(&self, ptr: *const MetaSlot<C>) -> bool {
+        &&& self.inner.ptr() == ptr
+    }
+
+    pub open spec fn wf(&self) -> bool {
+        //&&& 0 <= self.slot_idx < meta_slot_array.len()
+        //&&& self.relate(meta_slot_array.vec[self.slot_idx as int])
+        &&& self.inner.is_init()
+        &&& self.inner.value().wf()
+        &&& self.inner.value().is_pt() ==> {
+            &&& self.frame_paddr() == meta_to_frame(self.meta_vaddr())
+            &&& frame_to_meta(self.frame_paddr()) == self.meta_vaddr()
+        }
+    }
+
+    pub open spec fn is_pt(&self) -> bool {
+        self.inner.value().is_pt()
+    }
+
+    pub open spec fn frame_paddr(&self) -> Paddr {
+        self.inner.value().get_inner_pt_spec().frame_paddr
+    }
+
+    pub open spec fn meta_vaddr(&self) -> Vaddr {
+        self.inner.ptr() as usize
+    }
+
+    pub open spec fn value(&self) -> MetaSlot<C> {
+        self.inner.value()
+    }
+}
+
+} // verus!

lock-protocol/src/mm/frame_concurrent/mod.rs

@@ -0,0 +1 @@
+pub mod meta;

lock-protocol/src/mm/lock_protocol_utils/common.rs

@@ -0,0 +1,169 @@
+use std::ops::Range;
+
+use vstd::prelude::*;
+use vstd::vstd::arithmetic::power2::*;
+use vstd::arithmetic::div_mod::*;
+use vstd::arithmetic::power2::*;
+use vstd::bits::*;
+
+use crate::helpers::bits::*;
+use crate::helpers::extern_const::*;
+use crate::spec::{common::*, utils::*};
+
+pub use super::configs::*;
+pub use crate::mm::{Paddr, Vaddr, PagingLevel};
+
+verus! {
+
+// pub const MAX_FRAME_NUM: u64 = 256;
+pub const INVALID_PADDR: Paddr = 0xffff_ffff_ffff_ffff;
+
+// extern_const!(
+// pub MAX_RC [MAX_RC_SPEC, CONST_MAX_RC]: u64 = 382);
+} // verus!
+verus! {
+
+// Maybe introduce a MAX_PADDR constant in the future.
+pub open spec fn valid_paddr(pa: Paddr) -> bool {
+    true
+}
+
+pub uninterp spec fn paddr_to_vaddr_spec(pa: Paddr) -> Vaddr;
+
+#[inline(always)]
+#[verifier::when_used_as_spec(paddr_to_vaddr_spec)]
+#[verifier::external_body]
+pub fn paddr_to_vaddr(pa: Paddr) -> (va: Vaddr)
+// requires
+// valid_paddr(pa),
+
+    ensures
+        va == paddr_to_vaddr_spec(pa),
+{
+    unimplemented!()
+}
+
+} // verus!
+verus! {
+
+pub open spec fn valid_vaddr(va: Vaddr) -> bool {
+    0 <= va < (1u64 << 48)
+}
+
+pub open spec fn valid_va_range(va: Range<Vaddr>) -> bool {
+    0 <= va.start <= va.end <= (1u64 << 48)
+}
+
+#[verifier::allow_in_spec]
+pub fn vaddr_is_aligned(va: Vaddr) -> (res: bool)
+    requires
+        valid_vaddr(va),
+    returns
+        (va & (low_bits_mask(12) as usize)) == 0,
+{
+    (va & low_bits_mask_usize(12)) == 0
+}
+
+pub open spec fn va_level_to_offset(va: Vaddr, level: PagingLevel) -> nat
+    recommends
+        valid_vaddr(va),
+        1 <= level <= 4,
+{
+    ((va >> (12 + (level - 1) * 9)) & low_bits_mask(9) as usize) as nat
+}
+
+pub fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize)
+    requires
+        valid_vaddr(va),
+        1 <= level <= 4,
+    ensures
+        valid_pte_offset(res as nat),
+    returns
+        va_level_to_offset(va, level) as usize,
+{
+    let offset = (va >> (12 + (level - 1) * 9)) & low_bits_mask_usize(9);
+
+    proof {
+        lemma2_to64();
+        let num = (va >> (12 + (level - 1) * 9));
+        assert((num & 511) < 512) by (bit_vector);
+    }
+
+    offset
+}
+
+pub open spec fn va_level_to_trace(va: Vaddr, level: PagingLevel) -> Seq<nat>
+    recommends
+        1 <= level <= 4,
+{
+    Seq::new((4 - level) as nat, |i| va_level_to_offset(va, (4 - i) as PagingLevel))
+}
+
+pub open spec fn va_level_to_nid(va: Vaddr, level: PagingLevel) -> NodeId {
+    NodeHelper::trace_to_nid(va_level_to_trace(va, level))
+}
+
+pub proof fn lemma_va_level_to_nid_inc(va: Vaddr, level: PagingLevel, nid: NodeId, idx: nat)
+    requires
+        valid_vaddr(va),
+        1 <= level < 4,
+        NodeHelper::valid_nid(nid),
+        nid == va_level_to_nid(va, (level + 1) as PagingLevel),
+        valid_pte_offset(idx),
+        idx == va_level_to_offset(va, (level + 1) as PagingLevel),
+    ensures
+        NodeHelper::get_child(nid, idx) == va_level_to_nid(va, level),
+{
+    broadcast use group_node_helper_lemmas;
+    // Establish the relationship between traces at consecutive levels
+
+    let trace_level_plus_1 = va_level_to_trace(va, (level + 1) as PagingLevel);
+    let trace_level = va_level_to_trace(va, level);
+
+    // Show that trace_level = trace_level_plus_1.push(idx)
+    assert(trace_level == trace_level_plus_1.push(idx));
+
+    // Now use the fact that nid = trace_to_nid(trace_level_plus_1)
+    // and get_child(nid, idx) = trace_to_nid(nid_to_trace(nid).push(idx))
+    assert(NodeHelper::nid_to_trace(nid) == trace_level_plus_1) by {
+        // First establish that trace_level_plus_1 is a valid trace
+        assert(NodeHelper::valid_trace(trace_level_plus_1)) by {
+            lemma_va_level_to_trace_valid(va, (level + 1) as PagingLevel);
+        };
+        NodeHelper::lemma_trace_to_nid_bijective();
+    };
+}
+
+pub proof fn lemma_va_level_to_offset_range(va: Vaddr, level: PagingLevel)
+    requires
+        1 <= level <= 4,
+    ensures
+        0 <= va_level_to_offset(va, level) < 512,
+{
+    let offset = va_level_to_offset(va, level);
+    assert(offset < 512) by {
+        assert(low_bits_mask(9) == 511) by {
+            lemma_low_bits_mask_values();
+        };
+        assert((va >> (12 + (level - 1) as usize * 9)) & 511 <= 511) by (bit_vector);
+    }
+}
+
+pub proof fn lemma_va_level_to_trace_valid(va: Vaddr, level: PagingLevel)
+    requires
+        1 <= level <= 4,
+    ensures
+        NodeHelper::valid_trace(va_level_to_trace(va, level)),
+    decreases 4 - level,
+{
+    if level < 4 {
+        lemma_va_level_to_trace_valid(va, (level + 1) as PagingLevel);
+        lemma_va_level_to_offset_range(va, (level + 1) as PagingLevel);
+        assert(va_level_to_trace(va, level) == va_level_to_trace(
+            va,
+            (level + 1) as PagingLevel,
+        ).push(va_level_to_offset(va, (level + 1) as PagingLevel)));
+    }
+}
+
+} // verus!

lock-protocol/src/mm/lock_protocol_utils/configs.rs

@@ -0,0 +1,17 @@
+use vstd::prelude::*;
+
+verus! {
+
+// Configurations
+// Cpu
+pub spec const GLOBAL_CPU_NUM: nat = 2;
+
+// Frame
+pub spec const GLOBAL_FRAME_NUM: nat = 1024;
+
+pub spec const FRAME_SIZE: nat = 4096;
+
+// Pte
+pub exec const PTE_NUM: usize = 512;
+
+} // verus!

lock-protocol/src/mm/lock_protocol_utils/mod.rs

@@ -0,0 +1,5 @@
+pub mod configs;
+pub mod common;
+
+pub use configs::*;
+pub use common::*;

lock-protocol/src/mm/mod.rs

@@ -2,6 +2,8 @@ pub mod frame;
 pub(crate) mod page_prop;
 pub mod page_table;
 pub mod vm_space;
+pub mod frame_concurrent;
+pub mod lock_protocol_utils;
 
 use std::ops::Range;