From 1d25d9783127c181f79732eb5c20c680444af414 Mon Sep 17 00:00:00 2001 From: Xander Date: Fri, 21 Jul 2023 21:36:54 +0200 Subject: Mainly refactoring --- kernel/memory/frame.dats | 57 +++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 54 insertions(+), 3 deletions(-) (limited to 'kernel/memory/frame.dats') diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats index 26ff412..8578e8f 100644 --- a/kernel/memory/frame.dats +++ b/kernel/memory/frame.dats @@ -2,6 +2,13 @@ #define ATS_DYNLOADFLAG 0 +macdef invalid_area = @{ + base_addr = the_null_ptr, + length = 1, + type = 0u, + reserved = 0 +} + staload "./frame.sats" staload "kernel/bootinfo/multiboot.sats" @@ -12,19 +19,63 @@ implement containing_address(address) : frame_t = counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) } -fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let +fn containing_area(area : memory_area_t) : frame_t = containing_address(ptr_add(area.base_addr,area.length - i2sz(1))) +//FIX: function doesn't handle no frames left +fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let + val length = get_memory_mappings_n(bf | b) + val next_free_frame = p->next_free_frame + fun loop {n,i : nat | i < n} {l : agz} .. (bf : !boot_info_t @ l | b : ptr l, i : size_t i, n : size_t n) : memory_area_t = let + val entry = get_memory_mapping(bf | b ,i) + val fr = containing_area(entry) + in + if (entry.type = 1 && fr.num >= next_free_frame.num) then + entry + else if (i < n-1) then + loop (bf | b,succ(i),n) + else + entry //TODO: fix + end in + if (length > 0) then //TODO: fix + p->current_area := loop(bf | b, i2sz(0), length); + if (p->current_area.length > 1) then + let + val start_frame = containing_address(p->current_area.base_addr) + in + if (p->next_free_frame.num < start_frame.num) then + p->next_free_frame := start_frame + end end +local + +var frame_allocator : frame_allocator_t + +in + + implement frame_allocator_init() : allocptr = let + extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (frame_allocator_t@l) // takeout proof UNSAFE: + prval (pf, fpf) = __assert (addr@frame_allocator) + val allocator = @{ + next_free_frame = containing_address(the_null_ptr), + current_area = invalid_area + } + in + + (pf, fpf | addr@frame_allocator) + end + +end + implement allocate_frame(pf , bf | p,b) : frame_t = - if (p->current_area.length > 1) then let + if (p->current_area.type != 0u) then let val area = p->current_area val frame = @{ num = p->next_free_frame.num } // last frame of current area - val last_frame_area = containing_address(ptr_add(area.base_addr,area.length - i2sz(1))) + val last_frame_area = containing_area(area) in if (frame.num > last_frame_area.num) then ( // all frames of current area are used, switch to next area -- cgit v1.2.3