Skip to main content

segment_cover_count

ostd::specs::mm::embedding

Function segment_cover_count 

Source 
pub open spec fn segment_cover_count(
    segments: Map<SegmentId, SegmentEntry>,
    paddr: Paddr,
) -> nat
Expand description
{
    segments
        .dom()
        .filter(|sid: SegmentId| {
            segments[sid].range.start <= paddr && paddr < segments[sid].range.end
        })
        .len()
}

Number of outstanding Segment handles covering the frame slot at paddr — i.e., #{ sid : segments[sid].range covers paddr }. This is the per-slot raw_count term contributed by segments (Design B: each segment holds one forgotten reference per frame in its range, so raw_count == segment_cover_count(segments, ...)). Intended to be called on page-aligned paddrs (e.g. via index_to_frame(idx)); segment ranges are themselves page- aligned so the resulting count is the same for any paddr within a given page.