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::{UniqueFrame, UniqueFrameOwner};
18use crate::mm::{Paddr, PagingLevel, Vaddr};
19use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
20use crate::specs::mm::frame::linked_list::{CursorOwner, LinkedListOwner};
21use crate::specs::mm::frame::meta_owners::MetaSlotOwner;
22use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
23
24use core::borrow::BorrowMut;
25use core::{
26    ops::{Deref, DerefMut},
27    ptr::NonNull,
28    sync::atomic::{AtomicU64, Ordering},
29};
30
31use crate::specs::*;
32
33use crate::mm::frame::meta::mapping::{frame_to_index, meta_addr, meta_to_frame};
34use crate::mm::frame::meta::{get_slot, AnyFrameMeta, MetaSlot};
35
36verus! {
37
38#[rustc_has_incoherent_inherent_impls]
39pub struct Link<M: AnyFrameMeta + Repr<MetaSlot>> {
40    pub next: Option<ReprPtr<MetaSlot, Link<M>>>,
41    pub prev: Option<ReprPtr<MetaSlot, Link<M>>>,
42    pub meta: M,
43}
44
45/// A linked list of frames.
46///
47/// Two key features that [`LinkedList`] is different from
48/// [`alloc::collections::LinkedList`] is that:
49///  1. It is intrusive, meaning that the links are part of the frame metadata.
50///     This allows the linked list to be used without heap allocation. But it
51///     disallows a frame to be in multiple linked lists at the same time.
52///  2. The linked list exclusively own the frames, meaning that it takes
53///     unique pointers [`UniqueFrame`]. And other bodies cannot
54///     [`from_in_use`] a frame that is inside a linked list.
55///  3. We also allow creating cursors at a specific frame, allowing $O(1)$
56///     removal without iterating through the list at a cost of some checks.
57#[rustc_has_incoherent_inherent_impls]
58pub struct LinkedList<M: AnyFrameMeta + Repr<MetaSlot>> {
59    pub front: Option<ReprPtr<MetaSlot, Link<M>>>,
60    pub back: Option<ReprPtr<MetaSlot, Link<M>>>,
61    /// The number of frames in the list.
62    pub size: usize,
63    /// A lazily initialized ID, used to check whether a frame is in the list.
64    /// 0 means uninitialized.
65    pub list_id: u64,
66}
67
68/// A cursor that can mutate the linked list links.
69///
70/// The cursor points to either a frame or the "ghost" non-element. It points
71/// to the "ghost" non-element when the cursor surpasses the back of the list.
72#[rustc_has_incoherent_inherent_impls]
73pub struct CursorMut<M: AnyFrameMeta + Repr<MetaSlot>> {
74    pub list: PPtr<LinkedList<M>>,
75    pub current: Option<ReprPtr<MetaSlot, Link<M>>>,
76}
77
78impl<M: AnyFrameMeta + Repr<MetaSlot>> LinkedList<M> {
79    /// Creates a new linked list.
80    pub const fn new() -> Self {
81        Self { front: None, back: None, size: 0, list_id: 0 }
82    }
83}
84
85impl<M: AnyFrameMeta + Repr<MetaSlot>> Default for LinkedList<M> {
86    fn default() -> Self {
87        Self::new()
88    }
89}
90
91pub struct StoredLink {
92    pub next: Option<Paddr>,
93    pub prev: Option<Paddr>,
94    pub slot: MetaSlot,
95}
96
97impl<M: AnyFrameMeta + Repr<MetaSlot>> Repr<MetaSlot> for Link<M> {
98    uninterp spec fn wf(r: MetaSlot) -> bool;
99
100    uninterp spec fn to_repr_spec(self) -> MetaSlot;
101
102    #[verifier::external_body]
103    fn to_repr(self) -> MetaSlot {
104        unimplemented!()
105    }
106
107    uninterp spec fn from_repr_spec(r: MetaSlot) -> Self;
108
109    #[verifier::external_body]
110    fn from_repr(r: MetaSlot) -> Self {
111        unimplemented!()
112    }
113
114    #[verifier::external_body]
115    fn from_borrowed<'a>(r: &'a MetaSlot) -> &'a Self {
116        unimplemented!()
117    }
118
119    proof fn from_to_repr(self)
120        ensures
121            Self::from_repr(self.to_repr()) == self,
122    {
123        admit();
124    }
125
126    proof fn to_from_repr(r: MetaSlot)
127        ensures
128            Self::from_repr(r).to_repr() == r,
129    {
130        admit();
131    }
132
133    proof fn to_repr_wf(self)
134        ensures
135            <Self as Repr<MetaSlot>>::wf(self.to_repr()),
136    {
137        admit();
138    }
139}
140
141impl<M: AnyFrameMeta + Repr<MetaSlot>> AnyFrameMeta for Link<M> {
142    fn on_drop(&mut self) {
143    }
144
145    fn is_untyped(&self) -> bool {
146        false
147    }
148
149    uninterp spec fn vtable_ptr(&self) -> usize;
150}
151
152// SAFETY: Only the pointers are not `Send` and `Sync`. But our interfaces
153// enforces that only with `&mut` references can we access with the pointers.
154//unsafe impl<M> Send for LinkedList<M> where Link<M>: AnyFrameMeta {}
155//unsafe impl<M> Sync for LinkedList<M> where Link<M>: AnyFrameMeta {}
156#[verus_verify]
157impl<M: AnyFrameMeta + Repr<MetaSlot>> LinkedList<M> {
158    /// Gets the number of frames in the linked list.
159    #[rustc_allow_incoherent_impl]
160    #[verus_spec(s =>
161        with
162            Tracked(owner): Tracked<LinkedListOwner<M>>,
163        requires
164            self.wf(owner),
165            owner.inv(),
166        ensures
167            s == self.model(owner).list.len(),
168    )]
169    pub fn size(&self) -> usize
170    {
171        proof {
172            LinkedListOwner::<M>::view_preserves_len(owner.list);
173        }
174        self.size
175    }
176
177    /// Tells if the linked list is empty.
178    #[rustc_allow_incoherent_impl]
179    #[verus_spec(b =>
180        with
181            Tracked(owner): Tracked<LinkedListOwner<M>>,
182        requires
183            self.wf(owner),
184            owner.inv(),
185        ensures
186            b ==> self.size == 0 && self.front is None && self.back is None,
187            !b ==> self.size > 0 && self.front is Some && self.back is Some,
188    )]
189    pub fn is_empty(&self) -> bool
190    {
191        let is_empty = self.size == 0;
192        is_empty
193    }
194
195    /// Pushes a frame to the front of the linked list.
196    #[rustc_allow_incoherent_impl]
197    #[verus_spec(
198        with
199            Tracked(regions): Tracked<&mut MetaRegionOwners>,
200            Tracked(owner): Tracked<LinkedListOwner<M>>,
201            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
202            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
203        requires
204            perm.pptr() == ptr,
205            perm.is_init(),
206            perm.mem_contents().value().wf(owner),
207            owner.inv(),
208            owner.list_id != 0,
209            old(frame_own).inv(),
210            old(frame_own).global_inv(*old(regions)),
211            frame.wf(*old(frame_own)),
212            old(frame_own).frame_link_inv(),
213            owner.list.len() < usize::MAX,
214            old(regions).inv(),
215            old(regions).slots.contains_key(old(frame_own).slot_index),
216            old(regions).slot_owners[old(frame_own).slot_index].in_list.is_for(
217                old(regions).slots[old(frame_own).slot_index].value().in_list,
218            ),
219    )]
220    pub fn push_front(ptr: PPtr<Self>, frame: UniqueFrame<Link<M>>) {
221        proof_with!(Tracked(owner), Tracked(perm) => Tracked(cursor_own));
222        let cursor = Self::cursor_front_mut(ptr);
223        let mut cursor = cursor;
224        let tracked mut cursor_own = cursor_own;
225
226        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
227        cursor.insert_before(frame);
228    }
229
230    /// Pops a frame from the front of the linked list.
231    #[rustc_allow_incoherent_impl]
232    #[verus_spec(r =>
233        with
234            Tracked(regions): Tracked<&mut MetaRegionOwners>,
235            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
236            Tracked(owner): Tracked<LinkedListOwner<M>>,
237            Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
238        requires
239            old(regions).inv(),
240            perm.pptr() == ptr,
241            perm.is_init(),
242            perm.value().wf(owner),
243            owner.inv(),
244            old(regions).slots.contains_key(frame_to_index(owner.list[0].paddr)),
245    )]
246    #[verusfmt::skip]
247    pub fn pop_front(ptr: PPtr<Self>) -> Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)> {
248        assert(owner.list.len() > 0 ==> owner.inv_at(0));
249
250        proof_with!(Tracked(owner), Tracked(perm) => Tracked(cursor_own));
251        let cursor = Self::cursor_front_mut(ptr);
252        let mut cursor = cursor;
253        let tracked mut cursor_own = cursor_own;
254
255        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own))]
256        cursor.take_current()
257    }
258
259    /// Pushes a frame to the back of the linked list.
260    #[rustc_allow_incoherent_impl]
261    #[verus_spec(
262        with
263            Tracked(regions): Tracked<&mut MetaRegionOwners>,
264            Tracked(owner): Tracked<LinkedListOwner<M>>,
265            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
266            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
267        requires
268            perm.pptr() == ptr,
269            perm.is_init(),
270            perm.mem_contents().value().wf(owner),
271            owner.inv(),
272            owner.list_id != 0,
273            old(frame_own).inv(),
274            old(frame_own).global_inv(*old(regions)),
275            frame.wf(*old(frame_own)),
276            old(frame_own).frame_link_inv(),
277            owner.list.len() < usize::MAX,
278            old(regions).inv(),
279            old(regions).slots.contains_key(old(frame_own).slot_index),
280            old(regions).slot_owners[old(frame_own).slot_index].in_list.is_for(
281                old(regions).slots[old(frame_own).slot_index].value().in_list,
282            ),
283    )]
284    pub fn push_back(ptr: PPtr<Self>, frame: UniqueFrame<Link<M>>) {
285        #[verus_spec(with Tracked(owner), Tracked(perm))]
286        let (cursor, cursor_own) = Self::cursor_back_mut(ptr);
287        let mut cursor = cursor;
288        let mut cursor_own = cursor_own;
289
290        #[verus_spec(with Tracked(regions), Tracked(cursor_own.borrow_mut()), Tracked(frame_own))]
291        cursor.insert_before(frame);
292    }
293
294    /// Pops a frame from the back of the linked list.
295    #[rustc_allow_incoherent_impl]
296    #[verus_spec(r =>
297        with
298            Tracked(regions): Tracked<&mut MetaRegionOwners>,
299            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
300            Tracked(owner): Tracked<LinkedListOwner<M>>,
301            Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
302        requires
303            old(regions).inv(),
304            perm.pptr() == ptr,
305            perm.is_init(),
306            perm.mem_contents().value().wf(owner),
307            owner.inv(),
308            old(regions).slots.contains_key(frame_to_index(owner.list[owner.list.len() - 1].paddr)),
309
310    )]
311    pub fn pop_back(ptr: PPtr<Self>) -> Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)> {
312        assert(owner.list.len() > 0 ==> owner.inv_at(owner.list.len() - 1));
313
314        #[verus_spec(with Tracked(owner), Tracked(perm))]
315        let (cursor, cursor_own) = Self::cursor_back_mut(ptr);
316        let mut cursor = cursor;
317        let mut cursor_own = cursor_own;
318
319        #[verus_spec(with Tracked(regions), Tracked(cursor_own.borrow_mut()))]
320        cursor.take_current()
321    }
322
323    /// Tells if a frame is in the list.
324    #[rustc_allow_incoherent_impl]
325    #[verus_spec(r =>
326        with
327            Tracked(regions): Tracked<&mut MetaRegionOwners>,
328            Tracked(slot_own): Tracked<&MetaSlotOwner>,
329            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
330        requires
331            slot_own.inv(),
332            slot_own.self_addr == frame_to_meta(frame),
333            old(regions).inv(),
334            old(regions).slots.contains_key(frame_to_index(frame)),
335            old(regions).slots[frame_to_index(frame)].is_init(),
336            old(regions).slot_owners.contains_key(frame_to_index(frame)),
337            old(regions).slot_owners[frame_to_index(frame)].in_list.is_for(
338                old(regions).slots[frame_to_index(frame)].mem_contents().value().in_list,
339            ),
340    )]
341    pub fn contains(ptr: PPtr<Self>, frame: Paddr) -> bool {
342        let Ok(slot_ptr) = get_slot(frame, Tracked(slot_own)) else {
343            return false;
344        };
345
346        let tracked mut slot_perm = regions.slots.tracked_remove(frame_to_index(frame));
347        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(frame));
348
349        let slot = slot_ptr.take(Tracked(&mut slot_perm));
350        let in_list = slot.in_list.load(Tracked(&mut slot_own.in_list));
351        slot_ptr.put(Tracked(&mut slot_perm), slot);
352
353        proof {
354            regions.slot_owners.tracked_insert(frame_to_index(frame), slot_own);
355            regions.slots.tracked_insert(frame_to_index(frame), slot_perm);
356        }
357
358        in_list == #[verus_spec(with Tracked(owner))]
359        Self::lazy_get_id(ptr)
360    }
361
362    /// Gets a cursor at the specified frame if the frame is in the list.
363    ///
364    /// This method fail if [`Self::contains`] returns `false`.
365    #[rustc_allow_incoherent_impl]
366    #[verus_spec(r =>
367        with
368            Tracked(regions): Tracked<&mut MetaRegionOwners>,
369            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
370        requires
371            old(regions).inv(),
372            frame < MAX_PADDR(),
373            frame % PAGE_SIZE() == 0,
374            old(regions).slots.contains_key(frame_to_index(frame)),
375            old(regions).slots[frame_to_index(frame)].is_init(),
376            old(regions).slot_owners.contains_key(frame_to_index(frame)),
377            old(regions).slot_owners[frame_to_index(frame)].in_list.is_for(
378                old(regions).slots[frame_to_index(frame)].mem_contents().value().in_list,
379            ),
380    )]
381    pub fn cursor_mut_at(ptr: PPtr<Self>, frame: Paddr) -> Option<CursorMut<M>>
382    {
383        let tracked mut slot_perm = regions.slots.tracked_remove(frame_to_index(frame));
384        let tracked mut slot_own = regions.slot_owners.tracked_remove(frame_to_index(frame));
385
386        let Ok(slot_ptr) = get_slot(frame, Tracked(&slot_own)) else {
387            return None;
388        };
389
390        let slot = slot_ptr.borrow(Tracked(&slot_perm));
391        let in_list = slot.in_list.load(Tracked(&mut slot_own.in_list));
392        let contains = in_list == #[verus_spec(with Tracked(owner))]
393        Self::lazy_get_id(ptr);
394
395        #[verus_spec(with Tracked(&slot_perm))]
396        let meta_ptr = slot.as_meta_ptr::<Link<M>>();
397
398        let res = if contains {
399            Some(CursorMut { list: ptr, current: Some(meta_ptr) })
400        } else {
401            None
402        };
403
404        proof {
405            regions.slots.tracked_insert(frame_to_index(frame), slot_perm);
406            regions.slot_owners.tracked_insert(frame_to_index(frame), slot_own);
407        }
408
409        res
410    }
411
412    /// Gets a cursor at the front that can mutate the linked list links.
413    ///
414    /// If the list is empty, the cursor points to the "ghost" non-element.
415    #[rustc_allow_incoherent_impl]
416    #[verus_spec(r =>
417        with
418            Tracked(owner): Tracked<LinkedListOwner<M>>,
419            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
420                    -> r_perm: Tracked<CursorOwner<M>>,
421        requires
422            perm.pptr() == ptr,
423            perm.is_init(),
424            perm.mem_contents().value().wf(owner),
425            owner.inv(),
426        ensures
427            r.wf(r_perm@),
428            r_perm@.inv(),
429            r_perm@ == CursorOwner::front_owner_spec(owner, perm),
430    )]
431    pub fn cursor_front_mut(ptr: PPtr<Self>) -> CursorMut<M> {
432        let ll = ptr.borrow(Tracked(&perm));
433        let current = ll.front;
434
435        proof_with!(|= Tracked(CursorOwner::front_owner(owner, perm)));
436        CursorMut { list: ptr, current }
437    }
438
439    /// Gets a cursor at the back that can mutate the linked list links.
440    ///
441    /// If the list is empty, the cursor points to the "ghost" non-element.
442    #[rustc_allow_incoherent_impl]
443    #[verus_spec(
444        with
445            Tracked(owner): Tracked<LinkedListOwner<M>>,
446            Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>
447    )]
448    pub fn cursor_back_mut(ptr: PPtr<Self>) -> (res: (CursorMut<M>, Tracked<CursorOwner<M>>))
449        requires
450            perm.pptr() == ptr,
451            perm.is_init(),
452            perm.mem_contents().value().wf(owner),
453            owner.inv(),
454        ensures
455            res.0.wf(res.1@),
456            res.1@.inv(),
457            res.1@ == CursorOwner::back_owner_spec(owner, perm),
458    {
459        let ll = ptr.borrow(Tracked(&perm));
460        let current = ll.back;
461
462        (CursorMut { list: ptr, current }, Tracked(CursorOwner::back_owner(owner, perm)))
463    }
464
465    /// Gets a cursor at the "ghost" non-element that can mutate the linked list links.
466    #[rustc_allow_incoherent_impl]
467    #[verus_spec(
468        with Tracked(owner): Tracked<&mut LinkedListOwner<M>>
469    )]
470    fn cursor_at_ghost_mut(ptr: PPtr<Self>) -> CursorMut<M> {
471        CursorMut { list: ptr, current: None }
472    }
473
474    #[verifier::external_body]
475    #[rustc_allow_incoherent_impl]
476    #[verus_spec(
477        with Tracked(owner): Tracked<&mut LinkedListOwner<M>>
478    )]
479    fn lazy_get_id(ptr: PPtr<Self>) -> (id: u64)
480        ensures
481            old(owner).list_id != 0 ==> id == old(owner).list_id && *owner == *old(owner),
482    {
483        unimplemented!()/*        // FIXME: Self-incrementing IDs may overflow, while `core::pin::Pin`
484        // is not compatible with locks. Think about a better solution.
485        static LIST_ID_ALLOCATOR: AtomicU64 = AtomicU64::new(1);
486        const MAX_LIST_ID: u64 = i64::MAX as u64;
487
488        if self.list_id == 0 {
489            let id = LIST_ID_ALLOCATOR.fetch_add(1, Ordering::Relaxed);
490            if id >= MAX_LIST_ID {
491//                log::error!("The frame list ID allocator has exhausted.");
492//                abort();
493                unimplemented!()
494            }
495            self.list_id = id;
496            id
497        } else {
498            self.list_id
499        }*/
500
501    }
502}
503
504impl<M: AnyFrameMeta + Repr<MetaSlot>> CursorMut<M> {
505    /// Moves the cursor to the next frame towards the back.
506    ///
507    /// If the cursor is pointing to the "ghost" non-element then this will
508    /// move it to the first element of the [`LinkedList`]. If it is pointing
509    /// to the last element of the LinkedList then this will move it to the
510    /// "ghost" non-element.
511    #[rustc_allow_incoherent_impl]
512    #[verus_spec(
513        with Tracked(owner): Tracked<CursorOwner<M>>
514    )]
515    pub fn move_next(&mut self)
516        requires
517            owner.inv(),
518            old(self).wf(owner),
519        ensures
520            self.model(owner.move_next_owner_spec()) == old(self).model(owner).move_next_spec(),
521            owner.move_next_owner_spec().inv(),
522            self.wf(owner.move_next_owner_spec()),
523    {
524        let ghost old_self = *self;
525
526        proof {
527            if self.current is Some {
528                assert(owner.list_own.inv_at(owner.index));
529            }
530            if owner.index < owner.length() - 1 {
531                assert(owner.list_own.inv_at(owner.index + 1));
532                owner.list_own.perms[owner.index + 1].pptr_implies_addr();
533            }
534        }
535
536        self.current = match self.current {
537            // SAFETY: The cursor is pointing to a valid element.
538            Some(current) => *borrow_field!(& current => next, owner.list_own.perms.tracked_borrow(owner.index)),
539            None => borrow_field!(self.list => front, &owner.list_perm),
540        };
541
542        proof {
543            LinkedListOwner::<M>::view_preserves_len(owner.list_own.list);
544            assert(self.model(owner.move_next_owner_spec()).fore == old_self.model(owner).move_next_spec().fore);
545            assert(self.model(owner.move_next_owner_spec()).rear == old_self.model(owner).move_next_spec().rear);
546        }
547    }
548
549    /// Moves the cursor to the previous frame towards the front.
550    ///
551    /// If the cursor is pointing to the "ghost" non-element then this will
552    /// move it to the last element of the [`LinkedList`]. If it is pointing
553    /// to the first element of the LinkedList then this will move it to the
554    /// "ghost" non-element.
555    #[rustc_allow_incoherent_impl]
556    #[verus_spec(
557        with Tracked(owner): Tracked<CursorOwner<M>>
558    )]
559    pub fn move_prev(&mut self)
560        requires
561            owner.inv(),
562            old(self).wf(owner),
563        ensures
564            self.model(owner.move_prev_owner_spec()) == old(self).model(owner).move_prev_spec(),
565            owner.move_prev_owner_spec().inv(),
566            self.wf(owner.move_prev_owner_spec()),
567    {
568        let ghost old_self = *self;
569
570        proof {
571            if self.current is Some {
572                assert(owner.list_own.inv_at(owner.index));
573            }
574            if 0 < owner.index {
575                assert(owner.list_own.inv_at(owner.index - 1));
576                owner.list_own.perms[owner.index - 1].pptr_implies_addr();
577            }
578        }
579
580        self.current = match self.current {
581            // SAFETY: The cursor is pointing to a valid element.
582            Some(current) => *borrow_field!(& current => prev, owner.list_own.perms.tracked_borrow(owner.index)),
583            None => borrow_field!(self.list => back, &owner.list_perm),
584        };
585
586        proof {
587            LinkedListOwner::<M>::view_preserves_len(owner.list_own.list);
588
589            if owner@.list_model.list.len() > 0 {
590                if owner@.fore.len() > 0 {
591                    assert(self.model(owner.move_prev_owner_spec()).fore == old_self.model(
592                        owner,
593                    ).move_prev_spec().fore);
594                    assert(self.model(owner.move_prev_owner_spec()).rear == old_self.model(
595                        owner,
596                    ).move_prev_spec().rear);
597                    if owner@.rear.len() > 0 {
598                        assert(owner.list_own.inv_at(owner.index));
599                    }
600                } else {
601                    assert(owner.list_own.inv_at(owner.index));
602                    assert(self.model(owner.move_prev_owner_spec()).rear == old_self.model(
603                        owner,
604                    ).move_prev_spec().rear);
605                    assert(owner@.rear == owner@.list_model.list);
606                }
607            }
608        }
609    }
610
611    /*
612    /// Gets the mutable reference to the current frame's metadata.
613    pub fn current_meta(&mut self) -> Option<&mut M> {
614        self.current.map(|current| {
615            // SAFETY: `&mut self` ensures we have exclusive access to the
616            // frame metadata.
617            let link_mut = unsafe { &mut *current.as_ptr() };
618            // We should not allow `&mut Link<M>` to modify the original links,
619            // which would break the linked list. So we just return the
620            // inner metadata `M`.
621            &mut link_mut.meta
622        })
623    }
624    */
625    /// Takes the current pointing frame out of the linked list.
626    ///
627    /// If successful, the frame is returned and the cursor is moved to the
628    /// next frame. If the cursor is pointing to the back of the list then it
629    /// is moved to the "ghost" non-element.
630    #[rustc_allow_incoherent_impl]
631    #[verus_spec(
632        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
633            Tracked(owner) : Tracked<&mut CursorOwner<M>>
634    )]
635    pub fn take_current(&mut self) -> (res: Option<
636        (UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>),
637    >)
638        requires
639            old(self).wf(*old(owner)),
640            old(owner).inv(),
641            old(regions).inv(),
642            old(owner).length() > 0 ==> old(regions).slots.contains_key(
643                frame_to_index(old(self).current.unwrap().addr()),
644            ),
645        ensures
646            old(owner).length() == 0 ==> res.is_none(),
647            res.is_some() ==> res.unwrap().0.model(res.unwrap().1@).meta == old(
648                owner,
649            ).list_own.list[old(owner).index]@,
650            res.is_some() ==> self.model(*owner) == old(self).model(*old(owner)).remove(),
651            res.is_some() ==> res.unwrap().1@.frame_link_inv(),
652    {
653        let ghost owner0 = *owner;
654
655        let current = self.current?;
656
657        assert(owner.list_own.inv_at(owner.index));
658        assert(owner.index > 0 ==> owner.list_own.inv_at(owner.index - 1));
659        assert(owner.index < owner.length() - 1 ==> owner.list_own.inv_at(owner.index + 1));
660
661        let meta_ptr = current.addr();
662        let paddr = meta_to_frame(meta_ptr);
663
664        let tracked cur_perm = owner.list_own.perms.tracked_remove(owner.index);
665        let tracked mut cur_own = owner.list_own.list.tracked_remove(owner.index);
666
667        #[verus_spec(with Tracked(regions), Tracked(cur_perm), Tracked(cur_own))]
668        let (frame, frame_own) = UniqueFrame::<Link<M>>::from_raw(paddr);
669        let mut frame = frame;
670        let tracked mut frame_own = frame_own.get();
671
672        let next_ptr = frame.meta().next;
673
674        #[verus_spec(with Tracked(&regions.slots.tracked_borrow(frame_to_index(paddr))))]
675        let frame_meta = frame.meta_mut();
676
677        let opt_prev = borrow_field!(frame_meta => prev, &frame_own.meta_perm);
678
679        if let Some(prev) = opt_prev {
680            // SAFETY: We own the previous node by `&mut self` and the node is
681            // initialized.
682            update_field!(prev => next <- next_ptr; owner.list_own.perms, owner.index-1);
683
684            assert(owner.index > 0);
685            //            assume(owner.list_own.list == LinkedListOwner::update_next(owner0.list_own.list, owner.index-1, owner0.list_own.list[owner.index].next)); /*** KVerus: Help me prove ***/
686        } else {
687            update_field!(self.list => front <- next_ptr; owner.list_perm);
688        }
689
690        let prev_ptr = frame.meta().prev;
691
692        #[verus_spec(with Tracked(&regions.slots.tracked_borrow(frame_to_index(paddr))))]
693        let frame_meta = frame.meta_mut();
694        let opt_next = frame_meta.borrow(Tracked(&frame_own.meta_perm)).next;
695
696        if let Some(next) = opt_next {
697            // SAFETY: We own the next node by `&mut self` and the node is
698            // initialized.
699            update_field!(next => prev <- prev_ptr; owner.list_own.perms, owner.index+1);
700
701            self.current = Some(next);
702        } else {
703            update_field!(self.list => back <- prev_ptr; owner.list_perm);
704
705            self.current = None;
706        }
707
708        #[verus_spec(with Tracked(&regions.slots.tracked_borrow(frame_to_index(paddr))))]
709        let frame_meta = frame.meta_mut();
710
711        update_field!(frame_meta => next <- None; frame_own.meta_perm);
712        update_field!(frame_meta => prev <- None; frame_own.meta_perm);
713
714        //        frame.slot().in_list.store(0, Ordering::Relaxed);
715        //        frame.slot().in_list_store(0);
716
717        update_field!(self.list => size -= 1; owner.list_perm);
718
719        proof {
720            owner0.remove_owner_spec_implies_model_spec(*owner);
721        }
722        Some((frame, Tracked(frame_own)))
723    }
724
725    /// Inserts a frame before the current frame.
726    ///
727    /// If the cursor is pointing at the "ghost" non-element then the new
728    /// element is inserted at the back of the [`LinkedList`].
729    #[rustc_allow_incoherent_impl]
730    #[verus_spec(
731        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
732            Tracked(owner): Tracked<&mut CursorOwner<M>>,
733            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>
734    )]
735    #[verusfmt::skip]
736    pub fn insert_before(&mut self, mut frame: UniqueFrame<Link<M>>)
737        requires
738            old(self).wf(*old(owner)),
739            old(owner).inv(),
740            old(owner).list_own.list_id != 0,
741            old(frame_own).inv(),
742            old(frame_own).global_inv(*old(regions)),
743            frame.wf(*old(frame_own)),
744            old(owner).length() < usize::MAX,
745            old(regions).inv(),
746            old(regions).slots.contains_key(old(frame_own).slot_index),
747            old(regions).slot_owners[old(frame_own).slot_index].in_list.is_for(
748                old(regions).slots[old(frame_own).slot_index].value().in_list,
749            ),
750            old(frame_own).meta_perm.addr() == frame.ptr.addr(),
751            old(frame_own).frame_link_inv(),
752        ensures
753            self.model(*owner) == old(self).model(*old(owner)).insert(frame_own.meta_own@),
754            self.wf(*owner),
755            owner.inv(),
756    {
757        let ghost owner0 = *owner;
758        // The frame can't possibly be in any linked lists since the list will
759        // own the frame so there can't be any unique pointers to it.
760        assert(meta_addr(frame_own.slot_index) == frame.ptr.addr()) by { admit() };
761
762        assert(regions.slot_owners.contains_key(frame_own.slot_index));
763        let tracked slot_own = regions.slot_owners.tracked_borrow(frame_own.slot_index);
764
765        #[verus_spec(with Tracked(&regions.slots.tracked_borrow(frame_own.slot_index)))]
766        let frame_ptr = frame.meta_mut();
767        assert(frame_ptr.addr() == frame.ptr.addr());
768
769        if let Some(current) = self.current {
770            assert(owner.list_own.inv_at(owner.index));
771            assert(owner.index > 0 ==> owner.list_own.inv_at(owner.index - 1));
772            assert(owner.index < owner.length() - 1 ==> owner.list_own.inv_at(owner.index + 1));
773
774            // SAFETY: We own the current node by `&mut self` and the node is
775            // initialized.
776            let tracked mut cur_perm = owner.list_own.perms.tracked_remove(owner.index);
777            let opt_prev = borrow_field!(current => prev, &cur_perm);
778            proof {
779                owner.list_own.perms.tracked_insert(owner.index, cur_perm);
780            }
781
782            if let Some(prev) = opt_prev {
783                // SAFETY: We own the previous node by `&mut self` and the node
784                // is initialized.
785                update_field!(prev => next <- Some(frame_ptr); owner.list_own.perms, owner.index-1);
786
787                update_field!(frame_ptr => prev <- Some(prev); frame_own.meta_perm);
788                update_field!(frame_ptr => next <- Some(prev); frame_own.meta_perm);
789
790                update_field!(current => prev <- Some(frame_ptr); owner.list_own.perms, owner.index);
791            } else {
792                update_field!(frame_ptr => next <- Some(current); frame_own.meta_perm);
793
794                update_field!(current => prev <- Some(frame_ptr); owner.list_own.perms, owner.index);
795
796                update_field!(self.list => front <- Some(frame_ptr); owner.list_perm);
797            }
798        } else {
799            assert(0 < owner.length() ==> owner.list_own.inv_at(owner.index - 1));
800
801            if let Some(back) = borrow_field!(self.list => back, &owner.list_perm) {
802                assert(owner.index == owner.length());
803
804                // SAFETY: We have ownership of the links via `&mut self`.
805                //                    debug_assert!(back.as_mut().next.is_none());
806                update_field!(back => next <- Some(frame_ptr); owner.list_own.perms, owner.length()-1);
807
808                update_field!(frame_ptr => prev <- Some(back); frame_own.meta_perm);
809
810                update_field!(self.list => back <- Some(frame_ptr); owner.list_perm);
811            } else {
812                //                debug_assert_eq!(self.list.front, None);
813                update_field!(self.list => front <- Some(frame_ptr); owner.list_perm);
814                update_field!(self.list => back <- Some(frame_ptr); owner.list_perm);
815            }
816        }
817
818        #[verus_spec(with Tracked(&regions.slots.tracked_borrow(frame_own.slot_index)))]
819        let slot = frame.slot();
820
821        assert(regions.slot_owners.contains_key(frame_to_index(meta_to_frame(frame.ptr.addr()))));
822        let tracked mut slot_own = regions.slot_owners.tracked_remove(
823            frame_to_index(meta_to_frame(frame.ptr.addr())),
824        );
825
826        #[verusfmt::skip]
827        slot.in_list.store(
828            Tracked(&mut slot_own.in_list),
829            #[verus_spec(with Tracked(&mut owner.list_own))]
830            LinkedList::<M>::lazy_get_id(self.list)
831        );
832
833        proof {
834            regions.slot_owners.tracked_insert(
835                frame_to_index(meta_to_frame(frame.ptr.addr())),
836                slot_own
837            )
838        }
839
840        // Forget the frame to transfer the ownership to the list.
841        //        let _ = frame.into_raw();
842
843        update_field!(self.list => size += 1; owner.list_perm);
844
845        // TODO: these broke, figure out why (it's related to meta-frame conversions)
846        assert(forall|i: int| 0 <= i < owner.index - 1 ==> owner0.list_own.inv_at(i) ==> owner.list_own.inv_at(i)) by {};
847        assert(forall|i: int| owner.index <= i < owner.length() ==> owner0.list_own.inv_at(i - 1) == owner.list_own.inv_at(i)) by { admit() };
848
849        proof {
850            // TODO: likewise
851            assert(owner.list_own.list == owner0.list_own.list.insert(owner0.index, frame_own.meta_own)) by { admit() };
852            owner0.insert_owner_spec_implies_model_spec(frame_own.meta_own, *owner);
853        }
854    }
855
856    /// Provides a reference to the linked list.
857    #[rustc_allow_incoherent_impl]
858    pub fn as_list(&self) -> PPtr<LinkedList<M>> {
859        self.list
860    }
861}
862
863/*impl Drop for LinkedList
864{
865    #[rustc_allow_incoherent_impl]
866    #[verifier::external_body]
867    fn drop(&mut self) {
868        unimplemented!()
869//        let mut cursor = self.cursor_front_mut();
870//        while cursor.take_current().is_some() {}
871    }
872}*/
873
874/*
875impl Deref for Link {
876    type Target = FrameMeta;
877
878    #[rustc_allow_incoherent_impl]
879    fn deref(&self) -> &Self::Target {
880        &self.meta
881    }
882}
883
884impl DerefMut for Link {
885    #[rustc_allow_incoherent_impl]
886    fn deref_mut(&mut self) -> &mut Self::Target {
887        &mut self.meta
888    }
889}
890*/
891
892impl<M: AnyFrameMeta + Repr<MetaSlot>> Link<M> {
893    #[rustc_allow_incoherent_impl]
894    /// Creates a new linked list metadata.
895    pub const fn new(meta: M) -> Self {
896        Self { next: None, prev: None, meta }
897    }
898}
899
900// SAFETY: If `M::on_drop` reads the page using the provided `VmReader`,
901// the safety is upheld by the one who implements `AnyFrameMeta` for `M`.
902/*unsafe impl<M> AnyFrameMeta for Link<M>
903where
904    M: AnyFrameMeta,
905{
906    fn on_drop(&mut self, reader: &mut crate::mm::VmReader<crate::mm::Infallible>) {
907        self.meta.on_drop(reader);
908    }
909
910    fn is_untyped(&self) -> bool {
911        self.meta.is_untyped()
912    }
913}
914*/
915} // verus!
ostd/mm/frame/linked_list.rs

ostd/mm/frame/
linked_list.rs
