ostd/mm/frame/
linked_list.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Enabling linked lists of frames without heap allocation.
3//!
4//! This module leverages the customizability of the metadata system (see
5//! [super::meta]) to allow any type of frame to be used in a linked list.
6use vstd::prelude::*;
7
8use vstd::atomic::PermissionU64;
9use vstd::seq_lib::*;
10use vstd::simple_pptr::*;
11
12use vstd_extra::cast_ptr::*;
13use vstd_extra::ownership::*;
14use vstd_extra::ptr_extra::*;
15
16use crate::mm::frame::meta::mapping::frame_to_meta;
17use crate::mm::frame::meta::REF_COUNT_UNUSED;
18use crate::mm::frame::UniqueFrame;
19use crate::mm::{Paddr, PagingLevel, Vaddr};
20use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
21use crate::specs::mm::frame::linked_list::linked_list_owners::*;
22use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, Metadata};
23use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
24use crate::specs::mm::frame::unique::UniqueFrameOwner;
25
26use core::borrow::BorrowMut;
27use core::{
28    ops::{Deref, DerefMut},
29    ptr::NonNull,
30    sync::atomic::{AtomicU64, Ordering},
31};
32
33use crate::specs::*;
34
35use crate::mm::frame::meta::mapping::{frame_to_index, meta_addr, meta_to_frame};
36use crate::mm::frame::meta::{get_slot, has_safe_slot, AnyFrameMeta, MetaSlot};
37
38verus! {
39
40/// A link in the linked list.
41pub struct Link<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
42    pub next: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
43    pub prev: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
44    pub meta: M,
45}
46
47/// A linked list of frames.
48///
49/// Two key features that [`LinkedList`] is different from
50/// [`alloc::collections::LinkedList`] is that:
51///  1. It is intrusive, meaning that the links are part of the frame metadata.
52///     This allows the linked list to be used without heap allocation. But it
53///     disallows a frame to be in multiple linked lists at the same time.
54///  2. The linked list exclusively own the frames, meaning that it takes
55///     unique pointers [`UniqueFrame`]. And other bodies cannot
56///     [`from_in_use`] a frame that is inside a linked list.
57///  3. We also allow creating cursors at a specific frame, allowing $O(1)$
58///     removal without iterating through the list at a cost of some checks.
59/// # Verified Properties
60/// ## Verification Design
61/// The linked list is abstractly represented by a [`LinkedListOwner`]:
62/// ```rust
63/// tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
64///     pub list: Seq<LinkOwner>,
65///     pub perms: Map<int, vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<Link<M>>>>,
66///     pub list_id: u64,
67/// }
68/// ```
69/// ## Invariant
70/// The linked list uniquely owns the raw frames that it contains, so they cannot be used by other
71/// data structures. The frame metadata field `in_list` is equal to `list_id` for all links in the list.
72/// ```rust
73///    pub open spec fn inv_at(self, i: int) -> bool {
74///        &&& self.perms.contains_key(i)
75///        &&& self.perms[i].addr() == self.list[i].paddr
76///        &&& self.perms[i].is_init()
77///        &&& self.perms[i].value().wf(self.list[i])
78///        &&& i == 0 <==> self.perms[i].mem_contents().value().prev is None
79///        &&& i == self.list.len() - 1 <==> self.perms[i].value().next is None
80///        &&& 0 < i ==> self.perms[i].value().prev is Some && self.perms[i].value().prev.unwrap()
81///            == self.perms[i - 1].pptr()
82///        &&& i < self.list.len() - 1 ==> self.perms[i].value().next is Some
83///            && self.perms[i].value().next.unwrap() == self.perms[i + 1].pptr()
84///        &&& self.list[i].inv()
85///        &&& self.list[i].in_list == self.list_id
86///    }
87///
88///    pub open spec fn inv(self) -> bool {
89///        forall|i: int| 0 <= i < self.list.len() ==> self.inv_at(i)
90///    }
91/// ```
92/// ## Safety
93/// A given linked list can only have one cursor at a time, so there are no data races.
94/// The `prev` and `next` fields of the metadata for each link always points to valid
95/// links in the list, so the structure is memory safe (will not read or write invalid memory).
96pub struct LinkedList<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
97    pub front: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
98    pub back: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
99    /// The number of frames in the list.
100    pub size: usize,
101    /// A lazily initialized ID, used to check whether a frame is in the list.
102    /// 0 means uninitialized.
103    pub list_id: u64,
104}
105
106/// A cursor that can mutate the linked list links.
107///
108/// The cursor points to either a frame or the "ghost" non-element. It points
109/// to the "ghost" non-element when the cursor surpasses the back of the list.
110pub struct CursorMut<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
111    pub list: PPtr<LinkedList<M>>,
112    pub current: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
113}
114
115impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
116    /// Creates a new linked list.
117    pub const fn new() -> Self {
118        Self { front: None, back: None, size: 0, list_id: 0 }
119    }
120}
121
122impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Default for LinkedList<M> {
123    fn default() -> Self {
124        Self::new()
125    }
126}
127
128// SAFETY: Only the pointers are not `Send` and `Sync`. But our interfaces
129// enforces that only with `&mut` references can we access with the pointers.
130//unsafe impl<M> Send for LinkedList<M> where Link<M>: AnyFrameMeta {}
131//unsafe impl<M> Sync for LinkedList<M> where Link<M>: AnyFrameMeta {}
132#[verus_verify]
133impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
134    /// Gets the number of frames in the linked list.
135    #[verus_spec(s =>
136        with
137            Tracked(owner): Tracked<LinkedListOwner<M>>,
138        requires
139            self.wf(owner),
140            owner.inv(),
141        ensures
142            s == self.model(owner).list.len(),
143    )]
144    pub fn size(&self) -> usize
145    {
146        proof {
147            LinkedListOwner::<M>::view_preserves_len(owner.list);
148        }
149        self.size
150    }
151
152    /// Tells if the linked list is empty.
153    #[verus_spec(b =>
154        with
155            Tracked(owner): Tracked<LinkedListOwner<M>>,
156        requires
157            self.wf(owner),
158            owner.inv(),
159        ensures
160            b ==> self.size == 0 && self.front is None && self.back is None,
161            !b ==> self.size > 0 && self.front is Some && self.back is Some,
162    )]
163    pub fn is_empty(&self) -> bool
164    {
165        let is_empty = self.size == 0;
166        is_empty
167    }
168
169    /// Pushes a frame to the front of the linked list.
170    /// # Verified Properties
171    /// ## Preconditions
172    /// The list must be well-formed, with the pointers to its links' metadata slots
173    /// matching the tracked permission objects. The new frame must be active, so that it is
174    /// valid to call `into_raw` on it inside of `insert_before`.
175    /// ## Postconditions
176    /// The new frame is inserted at the front of the list, and the cursor is moved to the new frame.
177    /// The list invariants are preserved.
178    /// ## Safety
179    /// See [`insert_before`] for the safety guarantees.
180    #[verus_spec(
181        with
182            Tracked(regions): Tracked<&mut MetaRegionOwners>,
183            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
184            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
185            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
186        requires
187            perm.pptr() == ptr,
188            perm.is_init(),
189            perm.mem_contents().value().wf(*old(owner)),
190            old(owner).inv(),
191            old(owner).list_id != 0,
192            old(frame_own).inv(),
193            old(frame_own).global_inv(*old(regions)),
194            frame.wf(*old(frame_own)),
195            old(frame_own).frame_link_inv(),
196            old(owner).list.len() < usize::MAX,
197            old(regions).inv(),
198            old(regions).slots.contains_key(old(frame_own).slot_index),
199            old(regions).slot_owners[old(frame_own).slot_index].inner_perms.in_list.is_for(
200                old(regions).slots[old(frame_own).slot_index].value().in_list,
201            ),
202        ensures
203            owner.inv(),
204            owner.list == old(owner).list.insert(0, frame_own.meta_own),
205            owner.list_id == old(owner).list_id,
206            frame_own.meta_own.paddr == old(frame_own).meta_own.paddr,
207            frame_own.meta_own.in_list == old(owner).list_id,
208    )]
209    pub fn push_front(ptr: PPtr<Self>, frame: UniqueFrame<Link<M>>) {
210        let ll = ptr.borrow(Tracked(&perm));
211        let current = ll.front;
212        let tracked mut cursor_own = CursorOwner::front_owner(*owner, perm);
213        let mut cursor = CursorMut { list: ptr, current };
214
215        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
216        cursor.insert_before(frame);
217
218        proof {
219            *owner = cursor_own.list_own;
220        }
221    }
222
223    /// Pops a frame from the front of the linked list.
224    /// # Verified Properties
225    /// ## Preconditions
226    /// The list must be well-formed, with the pointers to its links' metadata slots
227    /// matching the tracked permission objects. The list must be non-empty, so that the
228    /// current frame is valid.
229    /// ## Postconditions
230    /// The front frame is removed from the list, and the cursor is moved to the next frame.
231    /// The list invariants are preserved.
232    /// ## Safety
233    /// See [`take_current`] for the safety guarantees.
234    #[verus_spec(r =>
235        with
236            Tracked(regions): Tracked<&mut MetaRegionOwners>,
237            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
238            Tracked(owner): Tracked<LinkedListOwner<M>>,
239            Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
240        requires
241            old(regions).inv(),
242            perm.pptr() == ptr,
243            perm.is_init(),
244            perm.value().wf(owner),
245            owner.inv(),
246            old(regions).slots.contains_key(frame_to_index(owner.list[0].paddr)),
247        ensures
248            owner.list.len() == 0 ==> r.is_none(),
249            r.is_some() ==> r.unwrap().0.model(r.unwrap().1@).meta == owner.list[0]@,
250            r.is_some() ==> r.unwrap().1@.frame_link_inv(),
251    )]
252    pub fn pop_front(ptr: PPtr<Self>) -> Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)> {
253        assert(owner.list.len() > 0 ==> owner.inv_at(0));
254
255        proof_with!(Tracked(owner), Tracked(perm) => Tracked(cursor_own));
256        let cursor = Self::cursor_front_mut(ptr);
257        let mut cursor = cursor;
258        let tracked mut cursor_own = cursor_own;
259
260        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own))]
261        cursor.take_current()
262    }
263
264    /// Pushes a frame to the back of the linked list.
265    /// # Verified Properties
266    /// ## Preconditions
267    /// The list must be well-formed, with the pointers to its links' metadata slots
268    /// matching the tracked permission objects. The new frame must be active, so that it is
269    /// valid to call `into_raw` on it inside of `insert_before`.
270    /// ## Postconditions
271    /// - The new frame is inserted at the back of the list, and the cursor is moved to the new frame.
272    /// - The list invariants are preserved.
273    /// ## Safety
274    /// See [`insert_before`] for the safety guarantees.
275    #[verus_spec(
276        with
277            Tracked(regions): Tracked<&mut MetaRegionOwners>,
278            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
279            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
280            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
281        requires
282            perm.pptr() == ptr,
283            perm.is_init(),
284            perm.mem_contents().value().wf(*old(owner)),
285            old(owner).inv(),
286            old(owner).list_id != 0,
287            old(frame_own).inv(),
288            old(frame_own).global_inv(*old(regions)),
289            frame.wf(*old(frame_own)),
290            old(frame_own).frame_link_inv(),
291            old(owner).list.len() < usize::MAX,
292            old(regions).inv(),
293            old(regions).slots.contains_key(old(frame_own).slot_index),
294            old(regions).slot_owners[old(frame_own).slot_index].inner_perms.in_list.is_for(
295                old(regions).slots[old(frame_own).slot_index].value().in_list,
296            ),
297        ensures
298            owner.inv(),
299            old(owner).list.len() > 0 ==> owner.list == old(owner).list.insert(
300                old(owner).list.len() as int - 1, frame_own.meta_own),
301            old(owner).list.len() == 0 ==> owner.list == old(owner).list.insert(
302                0, frame_own.meta_own),
303            owner.list_id == old(owner).list_id,
304            frame_own.meta_own.paddr == old(frame_own).meta_own.paddr,
305            frame_own.meta_own.in_list == old(owner).list_id,
306    )]
307    pub fn push_back(ptr: PPtr<Self>, frame: UniqueFrame<Link<M>>) {
308        let ll = ptr.borrow(Tracked(&perm));
309        let current = ll.back;
310        let tracked mut cursor_own = CursorOwner::back_owner(*owner, perm);
311        let mut cursor = CursorMut { list: ptr, current };
312
313        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
314        cursor.insert_before(frame);
315
316        proof {
317            *owner = cursor_own.list_own;
318        }
319    }
320
321    /// Pops a frame from the back of the linked list.
322    /// # Verified Properties
323    /// ## Preconditions
324    /// - The list must be well-formed, with the pointers to its links' metadata slots
325    /// matching the tracked permission objects.
326    /// - The list must be non-empty, so that the
327    /// current frame is valid.
328    /// ## Postconditions
329    /// - The back frame is removed from the list, and the cursor is moved to the "ghost" non-element.
330    /// - The list invariants are preserved.
331    /// ## Safety
332    /// See [`take_current`] for the safety guarantees.
333    #[verus_spec(r =>
334        with
335            Tracked(regions): Tracked<&mut MetaRegionOwners>,
336            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
337            Tracked(owner): Tracked<LinkedListOwner<M>>,
338            Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
339        requires
340            old(regions).inv(),
341            perm.pptr() == ptr,
342            perm.is_init(),
343            perm.mem_contents().value().wf(owner),
344            owner.inv(),
345            old(regions).slots.contains_key(frame_to_index(owner.list[owner.list.len() - 1].paddr)),
346        ensures
347            owner.list.len() == 0 ==> r.is_none(),
348            r.is_some() ==> r.unwrap().0.model(r.unwrap().1@).meta == owner.list[owner.list.len() - 1]@,
349            r.is_some() ==> r.unwrap().1@.frame_link_inv(),
350    )]
351    pub fn pop_back(ptr: PPtr<Self>) -> Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)> {
352        assert(owner.list.len() > 0 ==> owner.inv_at(owner.list.len() - 1));
353
354        #[verus_spec(with Tracked(owner), Tracked(perm))]
355        let (cursor, cursor_own) = Self::cursor_back_mut(ptr);
356        let mut cursor = cursor;
357        let mut cursor_own = cursor_own;
358
359        #[verus_spec(with Tracked(regions), Tracked(cursor_own.borrow_mut()))]
360        cursor.take_current()
361    }
362
363    /// Tells if a frame is in the list.
364    /// # Verified Properties
365    /// ## Preconditions
366    /// - The list must be well-formed, with the pointers to its links' metadata slots
367    /// matching the tracked permission objects.
368    /// - The frame must be a valid, active frame.
369    /// ## Postconditions
370    /// The function returns `true` if the frame is in the list, `false` otherwise.
371    /// ## Safety
372    /// - `lazy_get_id` uses atomic memory accesses, so there are no data races.
373    /// - We assume that the ID allocator has an available ID if the list previously didn't have one,
374    /// but the consequence if that is not the case is a failsafe panic.
375    /// - Everything else conforms to the safe interface.
376    #[verus_spec(r =>
377        with
378            Tracked(regions): Tracked<&mut MetaRegionOwners>,
379            Tracked(slot_own): Tracked<&MetaSlotOwner>,
380            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
381        requires
382            slot_own.inv(),
383            old(regions).inv(),
384            old(regions).slots.contains_key(frame_to_index(frame)),
385            old(regions).slots[frame_to_index(frame)].is_init(),
386            old(regions).slot_owners.contains_key(frame_to_index(frame)),
387            old(regions).slot_owners[frame_to_index(frame)].inner_perms.in_list.is_for(
388                old(regions).slots[frame_to_index(frame)].mem_contents().value().in_list,
389            ),
390        ensures
391            old(owner).list_id != 0 ==> *owner == *old(owner),
392    )]
393    pub fn contains(ptr: PPtr<Self>, frame: Paddr) -> bool {
394        let Ok(slot_ptr) = get_slot(frame) else {
395            return false;
396        };
397
398        let tracked mut slot_perm = regions.slots.tracked_remove(frame_to_index(frame));
399        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(frame));
400
401        let slot = slot_ptr.take(Tracked(&mut slot_perm));
402
403        let tracked mut inner_perms = slot_own.take_inner_perms();
404
405        let in_list = slot.in_list.load(Tracked(&mut inner_perms.in_list));
406        slot_ptr.put(Tracked(&mut slot_perm), slot);
407
408        proof {
409            slot_own.sync_inner(&inner_perms);
410            regions.slot_owners.tracked_insert(frame_to_index(frame), slot_own);
411            regions.slots.tracked_insert(frame_to_index(frame), slot_perm);
412        }
413
414        in_list == #[verus_spec(with Tracked(owner))]
415        Self::lazy_get_id(ptr)
416    }
417
418    /// Gets a cursor at the specified frame if the frame is in the list.
419    ///
420    /// This method fails if the frame is not in the list.
421    /// # Verified Properties
422    /// ## Preconditions
423    /// - The list must be well-formed, with the pointers to its links' metadata slots
424    /// matching the tracked permission objects.
425    /// - The frame should be raw (because it is owned by the list)
426    /// ## Postconditions
427    /// - This functions post-conditions are incomplete due to refactoring of the permission model.
428    /// When complete, it will guarantee that the cursor is well-formed and points to the matching
429    /// element in the list.
430    /// ## Safety
431    /// - `lazy_get_id` uses atomic memory accesses, so there are no data races.
432    /// - We assume that the ID allocator has an available ID if the list previously didn't have one,
433    /// but the consequence if that is not the case is a failsafe panic.
434    /// - Everything else conforms to the safe interface.
435    #[verus_spec(r =>
436        with
437            Tracked(regions): Tracked<&mut MetaRegionOwners>,
438            Tracked(owner): Tracked<LinkedListOwner<M>>,
439            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
440            -> cursor_owner: Tracked<Option<CursorOwner<M>>>,
441        requires
442            old(regions).inv(),
443        ensures
444//            has_safe_slot(frame) && owner.list_id != 0 ==> r is Some,
445            !has_safe_slot(frame) ==> r is None,
446    )]
447    #[verifier::external_body]
448    pub fn cursor_mut_at(ptr: PPtr<Self>, frame: Paddr) -> Option<CursorMut<M>>
449    {
450        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(frame));
451        let tracked mut inner_perms = slot_own.take_inner_perms();
452
453        if let Ok(slot_ptr) = get_slot(frame) {
454            let slot = slot_ptr.borrow(Tracked(&regions.slots[frame_to_index(frame)]));
455
456            let in_list = slot.in_list.load(Tracked(&mut inner_perms.in_list));
457
458            let contains = in_list == #[verus_spec(with Tracked(&owner))]
459            Self::lazy_get_id(ptr);
460
461            #[verus_spec(with Tracked(&regions.slots[frame_to_index(frame)]))]
462            let meta_ptr = slot.as_meta_ptr::<Link<M>>();
463
464            if contains {
465                proof {
466                    slot_own.sync_inner(&inner_perms);
467                    regions.slot_owners.tracked_insert(frame_to_index(frame), slot_own);
468                }
469
470                let ghost link = owner.list.filter(|link: LinkOwner| link.paddr == frame).first();
471                let ghost index = owner.list.index_of(link);
472                let tracked cursor_owner = CursorOwner::cursor_mut_at_owner(owner, perm, index);
473
474                proof_with!(|= Tracked(Some(cursor_owner)));
475                Some(CursorMut { list: ptr, current: Some(MetadataAsLink::cast_from_metadata(meta_ptr)) })
476            } else {
477                proof {
478                    slot_own.sync_inner(&inner_perms);
479                    regions.slot_owners.tracked_insert(frame_to_index(frame), slot_own);
480                }
481
482                proof_with!(|= Tracked(None));
483                None
484            }
485        } else {
486            assert(!has_safe_slot(frame));
487            proof_with!(|= Tracked(None));
488            None
489        }
490    }
491
492    /// Gets a cursor at the front that can mutate the linked list links.
493    ///
494    /// If the list is empty, the cursor points to the "ghost" non-element.
495    /// # Verified Properties
496    /// ## Preconditions
497    /// - The list must be well-formed, with the pointers to its links' metadata slots
498    /// matching the tracked permission objects.
499    /// ## Postconditions
500    /// - The cursor is well-formed, with the pointers to its links' metadata slots
501    /// matching the tracked permission objects. The list invariants are preserved.
502    /// - See [`CursorOwner::front_owner_spec`] for the precise specification.
503    /// ## Safety
504    /// - This function only uses the list permission, so there are no illegal memory accesses.
505    /// - No data races are possible.
506    #[verus_spec(r =>
507        with
508            Tracked(owner): Tracked<LinkedListOwner<M>>,
509            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
510                    -> r_perm: Tracked<CursorOwner<M>>,
511        requires
512            perm.pptr() == ptr,
513            perm.is_init(),
514            perm.mem_contents().value().wf(owner),
515            owner.inv(),
516        ensures
517            r.wf(r_perm@),
518            r_perm@.inv(),
519            r_perm@ == CursorOwner::front_owner_spec(owner, perm),
520    )]
521    pub fn cursor_front_mut(ptr: PPtr<Self>) -> CursorMut<M> {
522        let ll = ptr.borrow(Tracked(&perm));
523        let current = ll.front;
524
525        proof_with!(|= Tracked(CursorOwner::front_owner(owner, perm)));
526        CursorMut { list: ptr, current }
527    }
528
529    /// Gets a cursor at the back that can mutate the linked list links.
530    ///
531    /// If the list is empty, the cursor points to the "ghost" non-element.
532    /// # Verified Properties
533    /// ## Preconditions
534    /// - The list must be well-formed, with the pointers to its links' metadata slots
535    /// matching the tracked permission objects.
536    /// ## Postconditions
537    /// - The cursor is well-formed, with the pointers to its links' metadata slots
538    /// matching the tracked permission objects. The list invariants are preserved.
539    /// See [`CursorOwner::back_owner_spec`] for the precise specification.
540    /// ## Safety
541    /// - This function only uses the list permission, so there are no illegal memory accesses.
542    /// - No data races are possible.
543    #[verus_spec(
544        with
545            Tracked(owner): Tracked<LinkedListOwner<M>>,
546            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>
547    )]
548    pub fn cursor_back_mut(ptr: PPtr<Self>) -> (res: (CursorMut<M>, Tracked<CursorOwner<M>>))
549        requires
550            perm.pptr() == ptr,
551            perm.is_init(),
552            perm.mem_contents().value().wf(owner),
553            owner.inv(),
554        ensures
555            res.0.wf(res.1@),
556            res.1@.inv(),
557            res.1@ == CursorOwner::back_owner_spec(owner, perm),
558    {
559        let ll = ptr.borrow(Tracked(&perm));
560        let current = ll.back;
561
562        (CursorMut { list: ptr, current }, Tracked(CursorOwner::back_owner(owner, perm)))
563    }
564
565    /// Gets a cursor at the "ghost" non-element that can mutate the linked list links.
566    #[verus_spec(
567        with Tracked(owner): Tracked<&mut LinkedListOwner<M>>
568    )]
569    fn cursor_at_ghost_mut(ptr: PPtr<Self>) -> CursorMut<M> {
570        CursorMut { list: ptr, current: None }
571    }
572
573    /// # Verification Assumption
574    /// We assume that there is an available ID for `lazy_get_id` to return.
575    /// This is safe because it will panic if the ID allocator is exhausted.
576    #[verifier::external_body]
577    #[verus_spec(
578        with Tracked(owner): Tracked<& LinkedListOwner<M>>
579    )]
580    fn lazy_get_id(ptr: PPtr<Self>) -> (id: u64)
581        ensures
582            owner.list_id != 0 ==> id == owner.list_id,
583    {
584        unimplemented!()/*        // FIXME: Self-incrementing IDs may overflow, while `core::pin::Pin`
585        // is not compatible with locks. Think about a better solution.
586        static LIST_ID_ALLOCATOR: AtomicU64 = AtomicU64::new(1);
587        const MAX_LIST_ID: u64 = i64::MAX as u64;
588
589        if self.list_id == 0 {
590            let id = LIST_ID_ALLOCATOR.fetch_add(1, Ordering::Relaxed);
591            if id >= MAX_LIST_ID {
592//                log::error!("The frame list ID allocator has exhausted.");
593//                abort();
594                unimplemented!()
595            }
596            self.list_id = id;
597            id
598        } else {
599            self.list_id
600        }*/
601
602    }
603}
604
605impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<M> {
606    /// Moves the cursor to the next frame towards the back.
607    ///
608    /// If the cursor is pointing to the "ghost" non-element then this will
609    /// move it to the first element of the [`LinkedList`]. If it is pointing
610    /// to the last element of the LinkedList then this will move it to the
611    /// "ghost" non-element.
612    #[verus_spec(
613        with Tracked(owner): Tracked<CursorOwner<M>>
614    )]
615    pub fn move_next(&mut self)
616        requires
617            owner.inv(),
618            old(self).wf(owner),
619        ensures
620            self.model(owner.move_next_owner_spec()) == old(self).model(owner).move_next_spec(),
621            owner.move_next_owner_spec().inv(),
622            self.wf(owner.move_next_owner_spec()),
623    {
624        let ghost old_self = *self;
625
626        proof {
627            if self.current is Some {
628                assert(owner.list_own.inv_at(owner.index));
629            }
630            if owner.index < owner.length() - 1 {
631                assert(owner.list_own.inv_at(owner.index + 1));
632                owner.list_own.perms[owner.index + 1].pptr_implies_addr();
633            }
634        }
635
636        self.current = match self.current {
637            // SAFETY: The cursor is pointing to a valid element.
638            Some(current) => {
639                let current_md = MetadataAsLink::cast_to_metadata(current);
640                borrow_field!(current_md => metadata.next, owner.list_own.perms.tracked_borrow(owner.index))
641            },
642            None => borrow_field!(self.list => front, &owner.list_perm),
643        };
644
645        proof {
646            LinkedListOwner::<M>::view_preserves_len(owner.list_own.list);
647            assert(self.model(owner.move_next_owner_spec()).fore == old_self.model(owner).move_next_spec().fore);
648            assert(self.model(owner.move_next_owner_spec()).rear == old_self.model(owner).move_next_spec().rear);
649        }
650    }
651
652    /// Moves the cursor to the previous frame towards the front.
653    ///
654    /// If the cursor is pointing to the "ghost" non-element then this will
655    /// move it to the last element of the [`LinkedList`]. If it is pointing
656    /// to the first element of the LinkedList then this will move it to the
657    /// "ghost" non-element.
658    #[verus_spec(
659        with Tracked(owner): Tracked<CursorOwner<M>>
660    )]
661    pub fn move_prev(&mut self)
662        requires
663            owner.inv(),
664            old(self).wf(owner),
665        ensures
666            self.model(owner.move_prev_owner_spec()) == old(self).model(owner).move_prev_spec(),
667            owner.move_prev_owner_spec().inv(),
668            self.wf(owner.move_prev_owner_spec()),
669    {
670        let ghost old_self = *self;
671
672        proof {
673            if self.current is Some {
674                assert(owner.list_own.inv_at(owner.index));
675            }
676            if 0 < owner.index {
677                assert(owner.list_own.inv_at(owner.index - 1));
678                owner.list_own.perms[owner.index - 1].pptr_implies_addr();
679            }
680        }
681
682        self.current = match self.current {
683            // SAFETY: The cursor is pointing to a valid element.
684            Some(current) => {
685                let current_md = MetadataAsLink::cast_to_metadata(current);
686                borrow_field!(current_md => metadata.prev, owner.list_own.perms.tracked_borrow(owner.index))
687            },
688            None => borrow_field!(self.list => back, &owner.list_perm),
689        };
690
691        proof {
692            LinkedListOwner::<M>::view_preserves_len(owner.list_own.list);
693
694            if owner@.list_model.list.len() > 0 {
695                if owner@.fore.len() > 0 {
696                    assert(self.model(owner.move_prev_owner_spec()).fore == old_self.model(
697                        owner,
698                    ).move_prev_spec().fore);
699                    assert(self.model(owner.move_prev_owner_spec()).rear == old_self.model(
700                        owner,
701                    ).move_prev_spec().rear);
702                    if owner@.rear.len() > 0 {
703                        assert(owner.list_own.inv_at(owner.index));
704                    }
705                } else {
706                    assert(owner.list_own.inv_at(owner.index));
707                    assert(self.model(owner.move_prev_owner_spec()).rear == old_self.model(
708                        owner,
709                    ).move_prev_spec().rear);
710                    assert(owner@.rear == owner@.list_model.list);
711                }
712            }
713        }
714    }
715
716    /*
717    /// Gets the mutable reference to the current frame's metadata.
718    pub fn current_meta(&mut self) -> Option<&mut M> {
719        self.current.map(|current| {
720            // SAFETY: `&mut self` ensures we have exclusive access to the
721            // frame metadata.
722            let link_mut = unsafe { &mut *current.as_ptr() };
723            // We should not allow `&mut Link<M>` to modify the original links,
724            // which would break the linked list. So we just return the
725            // inner metadata `M`.
726            &mut link_mut.meta
727        })
728    }
729    */
730
731    /// Takes the current pointing frame out of the linked list.
732    ///
733    /// If successful, the frame is returned and the cursor is moved to the
734    /// next frame. If the cursor is pointing to the back of the list then it
735    /// is moved to the "ghost" non-element.
736    /// # Verified Properties
737    /// ## Preconditions
738    /// The cursor must be well-formed, with the pointers to its links' metadata slots
739    /// matching the tracked permission objects. The list must be non-empty, so that the
740    /// current frame is valid.
741    /// ## Postconditions
742    /// The current frame is removed from the list, and the cursor is moved to the next frame.
743    /// The list invariants are preserved.
744    /// ## Safety
745    /// This function calls `from_raw` on the frame, but we guarantee that the frame is forgotten
746    /// if it is in the list. So, double-free will not occur. All loads and stores are through track
747    /// tracked permissions, so there are no illegal memory accesses. No data races are possible.
748    #[verus_spec(
749        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
750            Tracked(owner) : Tracked<&mut CursorOwner<M>>
751    )]
752    pub fn take_current(&mut self) -> (res: Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)>)
753        requires
754            old(self).wf(*old(owner)),
755            old(owner).inv(),
756            old(regions).inv(),
757            old(owner).length() > 0 ==> old(regions).slot_owners.contains_key(
758                frame_to_index(old(self).current.unwrap().addr()),
759            ),
760        ensures
761            old(owner).length() == 0 ==> res.is_none(),
762            res.is_some() ==> res.unwrap().0.model(res.unwrap().1@).meta == old(
763                owner,
764            ).list_own.list[old(owner).index]@,
765            res.is_some() ==> self.model(*owner) == old(self).model(*old(owner)).remove(),
766            res.is_some() ==> res.unwrap().1@.frame_link_inv(),
767    {
768        let ghost owner0 = *owner;
769
770        let current = self.current?;
771
772        assert(owner.list_own.inv_at(owner.index));
773        assert(owner.index > 0 ==> owner.list_own.inv_at(owner.index - 1));
774        assert(owner.index < owner.length() - 1 ==> owner.list_own.inv_at(owner.index + 1));
775
776        let meta_ptr = current.addr();
777        let paddr = meta_to_frame(meta_ptr);
778
779        let tracked cur_perm = owner.list_own.perms.tracked_remove(owner.index);
780        let tracked mut cur_own = owner.list_own.list.tracked_remove(owner.index);
781
782        #[verus_spec(with Tracked(regions), Tracked(cur_perm), Tracked(cur_own))]
783        let (frame, frame_own) = UniqueFrame::<Link<M>>::from_raw(paddr);
784        let mut frame = frame;
785        let tracked mut frame_own = frame_own.get();
786
787        let next_ptr = frame.meta().next;
788
789        #[verus_spec(with Tracked(&frame_own))]
790        let frame_meta = frame.meta_mut();
791
792        let opt_prev_link = borrow_field!(frame_meta => metadata.prev, &frame_own.meta_perm);
793
794        if let Some(prev_link) = opt_prev_link {
795            let prev = MetadataAsLink::cast_to_metadata(prev_link);
796            // SAFETY: We own the previous node by `&mut self` and the node is
797            // initialized.
798            update_field!(prev => metadata.next <- next_ptr; owner.list_own.perms, owner.index-1);
799
800            assert(owner.index > 0);
801        } else {
802            update_field!(self.list => front <- next_ptr; owner.list_perm);
803        }
804
805        let prev_ptr = frame.meta().prev;
806
807        #[verus_spec(with Tracked(&frame_own))]
808        let frame_meta = frame.meta_mut();
809        let opt_next_link = frame_meta.borrow(Tracked(&frame_own.meta_perm)).metadata.next;
810
811        if let Some(next_link) = opt_next_link {
812            let next = MetadataAsLink::cast_to_metadata(next_link);
813            // SAFETY: We own the next node by `&mut self` and the node is
814            // initialized.
815            update_field!(next => metadata.prev <- prev_ptr; owner.list_own.perms, owner.index+1);
816
817            self.current = Some(next_link);
818        } else {
819            update_field!(self.list => back <- prev_ptr; owner.list_perm);
820
821            self.current = None;
822        }
823
824        #[verus_spec(with Tracked(&frame_own))]
825        let frame_meta = frame.meta_mut();
826
827        update_field!(frame_meta => metadata.next <- None; frame_own.meta_perm);
828        update_field!(frame_meta => metadata.prev <- None; frame_own.meta_perm);
829
830        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(paddr));
831
832        #[verus_spec(with Tracked(&frame_own.meta_perm.points_to))]
833        let slot = frame.slot();
834        let tracked mut inner_perms = frame_own.meta_perm.inner_perms;
835        slot.in_list.store(Tracked(&mut inner_perms.in_list), 0);
836        proof { frame_own.meta_perm.inner_perms = inner_perms; }
837
838        proof {
839            regions.slot_owners.tracked_insert(frame_to_index(paddr), slot_own);
840        }
841
842        update_field!(self.list => size -= 1; owner.list_perm);
843
844        proof {
845            owner0.remove_owner_spec_implies_model_spec(*owner);
846        }
847        Some((frame, Tracked(frame_own)))
848    }
849
850    /// Inserts a frame before the current frame.
851    ///
852    /// If the cursor is pointing at the "ghost" non-element then the new
853    /// element is inserted at the back of the [`LinkedList`].
854    /// # Verified Properties
855    /// ## Preconditions
856    /// The cursor must be well-formed, with the pointers to its links' metadata slots matching the tracked permission objects.
857    /// - The new frame must be active, so that it is valid to call `into_raw` on it.
858    /// ## Postconditions
859    /// - The new frame is inserted into the list, immediately before the current index.
860    /// - The list invariants are preserved.
861    /// ## Safety
862    /// - This function calls `into_raw` on the frame, so the caller must ensure that the frame is active and
863    /// has not been forgotten already to avoid a memory leak. If the caller attempts to insert a forgotten frame,
864    /// the invariant around `into_raw` and `from_raw` will be violated. But, it is the safe failure case in that
865    /// it will not cause a double-free. (Note: we should be able to move this requirement into the `UniqueFrame` invariants.)
866    #[verus_spec(
867        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
868            Tracked(owner): Tracked<&mut CursorOwner<M>>,
869            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>
870    )]
871    pub fn insert_before(&mut self, mut frame: UniqueFrame<Link<M>>)
872        requires
873            old(self).wf(*old(owner)),
874            old(owner).inv(),
875            old(owner).list_own.list_id != 0,
876            old(frame_own).inv(),
877            old(frame_own).global_inv(*old(regions)),
878            frame.wf(*old(frame_own)),
879            old(owner).length() < usize::MAX,
880            old(regions).inv(),
881            old(regions).slots.contains_key(old(frame_own).slot_index),
882            old(regions).slot_owners[old(frame_own).slot_index].inner_perms.in_list.is_for(
883                old(regions).slots[old(frame_own).slot_index].value().in_list,
884            ),
885            old(frame_own).meta_perm.addr() == frame.ptr.addr(),
886            old(frame_own).frame_link_inv(),
887        ensures
888            self.model(*owner) == old(self).model(*old(owner)).insert(frame_own.meta_own@),
889            self.wf(*owner),
890            owner.inv(),
891            owner.list_own.list == old(owner).list_own.list.insert(old(owner).index, frame_own.meta_own),
892            owner.list_own.list_id == old(owner).list_own.list_id,
893            frame_own.meta_own.paddr == old(frame_own).meta_own.paddr,
894            frame_own.meta_own.in_list == old(owner).list_own.list_id,
895    {
896        let ghost owner0 = *owner;
897
898        assert(meta_addr(frame_own.slot_index) == frame.ptr.addr());
899        assert(regions.slot_owners.contains_key(frame_own.slot_index));
900        let tracked slot_own = regions.slot_owners.tracked_borrow(frame_own.slot_index);
901
902        #[verus_spec(with Tracked(frame_own))]
903        let frame_ptr = frame.meta_mut();
904        assert(frame_ptr.addr() == frame.ptr.addr());
905
906        let frame_ptr_as_link = MetadataAsLink::cast_from_metadata(frame_ptr);
907
908        if let Some(current) = self.current {
909            let current_md = MetadataAsLink::cast_to_metadata(current);
910
911            assert(owner.list_own.inv_at(owner.index));
912            assert(owner.index > 0 ==> owner.list_own.inv_at(owner.index - 1));
913            assert(owner.index < owner.length() - 1 ==> owner.list_own.inv_at(owner.index + 1));
914
915            // SAFETY: We own the current node by `&mut self` and the node is initialized.
916            let tracked mut cur_perm = owner.list_own.perms.tracked_remove(owner.index);
917            let opt_prev_link : Option<ReprPtr<MetaSlot, MetadataAsLink<M>>> =
918                borrow_field!(current_md => metadata.prev, &cur_perm);
919            proof {
920                owner.list_own.perms.tracked_insert(owner.index, cur_perm);
921            }
922
923            if let Some(prev_link) = opt_prev_link {
924                let prev = MetadataAsLink::cast_to_metadata(prev_link);
925
926                // SAFETY: We own the previous node by `&mut self` and the node is initialized.
927                update_field!(prev => metadata.next <- Some(frame_ptr_as_link); owner.list_own.perms, owner.index-1);
928
929                update_field!(frame_ptr => metadata.prev <- Some(prev_link); frame_own.meta_perm);
930                update_field!(frame_ptr => metadata.next <- Some(current); frame_own.meta_perm);
931
932                update_field!(current_md => metadata.prev <- Some(frame_ptr_as_link); owner.list_own.perms, owner.index);
933            } else {
934                update_field!(frame_ptr => metadata.next <- Some(current); frame_own.meta_perm);
935
936                update_field!(current_md => metadata.prev <- Some(frame_ptr_as_link); owner.list_own.perms, owner.index);
937
938                update_field!(self.list => front <- Some(frame_ptr_as_link); owner.list_perm);
939            }
940        } else {
941            assert(0 < owner.length() ==> owner.list_own.inv_at(owner.index - 1));
942
943            if let Some(back) = borrow_field!(self.list => back, &owner.list_perm) {
944                let back_md = MetadataAsLink::cast_to_metadata(back);
945
946                assert(owner.index == owner.length());
947
948                // SAFETY: We have ownership of the links via `&mut self`.
949                //                    debug_assert!(back.as_mut().next.is_none());
950                update_field!(back_md => metadata.next <- Some(frame_ptr_as_link); owner.list_own.perms, owner.length()-1);
951
952                update_field!(frame_ptr => metadata.prev <- Some(back); frame_own.meta_perm);
953
954                update_field!(self.list => back <- Some(frame_ptr_as_link); owner.list_perm);
955            } else {
956                //                debug_assert_eq!(self.list.front, None);
957                update_field!(self.list => front <- Some(frame_ptr_as_link); owner.list_perm);
958                update_field!(self.list => back <- Some(frame_ptr_as_link); owner.list_perm);
959            }
960        }
961
962        assert(regions.slot_owners.contains_key(frame_to_index(meta_to_frame(frame.ptr.addr()))));
963        let tracked mut slot_own = regions.slot_owners.tracked_remove(
964            frame_to_index(meta_to_frame(frame.ptr.addr())),
965        );
966
967        #[verus_spec(with Tracked(&mut owner.list_own))]
968        let list_id = LinkedList::<M>::lazy_get_id(self.list);
969
970        let tracked mut inner_perms;
971        proof {
972            inner_perms = frame_own.meta_perm.take_inner_perms();
973        }
974        #[verus_spec(with Tracked(&frame_own.meta_perm.points_to))]
975        let slot = frame.slot();
976        slot.in_list.store(Tracked(&mut inner_perms.in_list), list_id);
977        proof { frame_own.meta_perm.put_inner_perms(inner_perms); }
978
979        proof {
980            // The store only changed in_list.value(); ref_count is unchanged.
981            // From global_inv: ref_count != REF_COUNT_UNUSED && ref_count != 0.
982            // So slot_own.inv() holds after the store.
983            assert(frame_own.slot_index == frame_to_index(meta_to_frame(frame.ptr.addr())));
984            assert(slot_own.inner_perms.ref_count.value() != REF_COUNT_UNUSED);
985            assert(slot_own.inner_perms.ref_count.value() != 0);
986            assert(slot_own.inv());
987
988            regions.slot_owners.tracked_insert(frame_to_index(meta_to_frame(frame.ptr.addr())), slot_own)
989        }
990
991        assert(regions.inv()) by {
992            // slot_owners only changed at frame_own.slot_index.
993            // For all other keys, the invariant is preserved from old(regions).inv().
994            // For the modified key, we proved slot_own.inv() above.
995            assert(forall|i: usize| #[trigger]
996                regions.slots.contains_key(i) ==>
997                    regions.slots[i].value().wf(regions.slot_owners[i]));
998        };
999
1000        // Forget the frame to transfer the ownership to the list.
1001        #[verus_spec(with Tracked(frame_own), Tracked(regions))]
1002        let _ = frame.into_raw();
1003
1004        update_field!(self.list => size += 1; owner.list_perm);
1005
1006        proof {
1007            CursorOwner::<M>::list_insert(owner, &mut frame_own.meta_own, &frame_own.meta_perm);
1008
1009            assert(forall|i: int| 0 <= i < owner.index - 1 ==> owner0.list_own.inv_at(i) ==> owner.list_own.inv_at(i)) by {};
1010            assert(forall|i: int| owner.index <= i < owner.length() ==> owner0.list_own.inv_at(i - 1) == owner.list_own.inv_at(i)) by {};
1011            assert(owner.list_own.inv_at(owner0.index as int));
1012
1013            assert(owner.list_own.list == owner0.list_own.list.insert(owner0.index, frame_own.meta_own));
1014            owner0.insert_owner_spec_implies_model_spec(frame_own.meta_own, *owner);
1015        }
1016    }
1017
1018    /// Provides a reference to the linked list.
1019    pub fn as_list(&self) -> PPtr<LinkedList<M>> {
1020        self.list
1021    }
1022}
1023
1024/*impl Drop for LinkedList
1025{
1026
1027    #[verifier::external_body]
1028    fn drop(&mut self) {
1029        unimplemented!()
1030//        let mut cursor = self.cursor_front_mut();
1031//        while cursor.take_current().is_some() {}
1032    }
1033}*/
1034
1035/*
1036impl Deref for Link {
1037    type Target = FrameMeta;
1038
1039
1040    fn deref(&self) -> &Self::Target {
1041        &self.meta
1042    }
1043}
1044
1045impl DerefMut for Link {
1046
1047    fn deref_mut(&mut self) -> &mut Self::Target {
1048        &mut self.meta
1049    }
1050}
1051*/
1052
1053impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Link<M> {
1054    /// Creates a new linked list metadata.
1055    pub const fn new(meta: M) -> Self {
1056        Self { next: None, prev: None, meta }
1057    }
1058}
1059
1060// SAFETY: If `M::on_drop` reads the page using the provided `VmReader`,
1061// the safety is upheld by the one who implements `AnyFrameMeta` for `M`.
1062/*unsafe impl<M> AnyFrameMeta for Link<M>
1063where
1064    M: AnyFrameMeta,
1065{
1066    fn on_drop(&mut self, reader: &mut crate::mm::VmReader<crate::mm::Infallible>) {
1067        self.meta.on_drop(reader);
1068    }
1069
1070    fn is_untyped(&self) -> bool {
1071        self.meta.is_untyped()
1072    }
1073}
1074*/
1075} // verus!
ostd/mm/frame/linked_list.rs

ostd/mm/frame/
linked_list.rs
