From ae3ad4d8b7004f17376ee0a8bfae931788194b8b Mon Sep 17 00:00:00 2001 From: Xander Date: Tue, 8 Aug 2023 23:13:00 +0200 Subject: Final refactoring for opts: frames --- kernel/memory/frame.dats | 248 +++++++++++++++++++++++------------------------ kernel/memory/frame.sats | 45 ++++----- 2 files changed, 139 insertions(+), 154 deletions(-) (limited to 'kernel/memory') diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats index 8a9160b..2910de5 100644 --- a/kernel/memory/frame.dats +++ b/kernel/memory/frame.dats @@ -1,131 +1,121 @@ -(* #include "kernel/prelude/kernel_prelude.hats" *) -(**) +#include "kernel/prelude/kernel_prelude.hats" + #define ATS_DYNLOADFLAG 0 -(**) -(* staload "./frame.sats" *) -(* staload "kernel/bootinfo/multiboot.sats" *) -(* staload "lib/SATS/init.sats" *) -(**) -(* staload UN = "prelude/SATS/unsafe.sats" *) -(**) -(* assume frame_allocator = frame_allocator_t *) -(**) -(* implement containing_address(address): frame_t = *) -(* @{ *) -(* counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) *) -(* } *) -(**) -(* 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{k : agz}(bf : !boot_info_t @ k | b : ptr k, allocator : &frame_allocator_t) : void = let *) -(* val length = get_memory_mappings_n(bf | b) *) -(* val next_free_frame = allocator.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 *) -(* allocator.current_area := loop(bf | b, i2sz(0), length); *) -(**) -(* if (allocator.current_area.length > 1) then *) -(* let *) -(* val start_frame = containing_address(allocator.current_area.base_addr) *) -(* in *) -(* if (allocator.next_free_frame.num < start_frame.num) then *) -(* allocator.next_free_frame := start_frame *) -(* end *) -(* end *) -(**) -(* local *) -(**) -(* var allocator_static : frame_allocator_t? *) -(* prval () = opt_none allocator_static *) -(* var allocator = uninitialized(allocator_static) *) -(* val allocator_ref = ref_make_viewptr{initializable frame_allocator_t} (view@allocator | addr@allocator) *) -(**) -(* in *) -(**) -(* implement frame_allocator_init(kernel_start, kernel_end, multiboot_start, multiboot_end, b) : void = let *) -(* val allocator = @{ *) -(* next_free_frame = containing_address(the_null_ptr), *) -(* current_area = invalid_area, *) -(* kernel_start = containing_address(kernel_start), *) -(* kernel_end = containing_address(kernel_end), *) -(* multiboot_start = containing_address(multiboot_start), *) -(* multiboot_end = containing_address(multiboot_end) *) -(* } : frame_allocator_t *) -(* val (vbox pf | p) = ref_get_viewptr(allocator_ref) *) -(* in *) -(* if not p->initialized then let *) -(* prval () = opt_unnone p->obj *) -(* in *) -(* p->obj := allocator; *) -(* p->initialized := true; *) -(* (* choose_next_area(b.0 | b.2, !p); *) *) -(* let prval () = opt_some p->obj in end; *) -(* end *) -(* end *) -(**) -(* implement allocate_frame(bf | b) : frame_t = let *) -(* val (vbox pf | p) = ref_get_viewptr(allocator_ref) *) -(* in *) -(* if p->initialized then let *) -(* (* var allocator = p->obj *) *) -(* prval () = opt_unsome p->obj *) -(* in *) -(* (* if (allocator.current_area.type != 0u) then let *) *) -(* (* val area = allocator.current_area *) *) -(* (* val frame = @{ num = allocator.next_free_frame.num } *) *) -(* (**) *) -(* (* // last frame of current area *) *) -(* (* 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 *) *) -(* (* choose_next_area(bf | b, allocator); *) *) -(* (* let prval () = opt_some allocator in end; *) *) -(* (* allocate_frame(bf | b) *) *) -(* (* ) else if (frame.num >= allocator.kernel_start.num && frame.num <= allocator.kernel_end.num) then ( *) *) -(* (* // frame is used by kernel *) *) -(* (* allocator.next_free_frame := @{num = allocator.kernel_end.num + 1}; *) *) -(* (* let prval () = opt_some allocator in end; *) *) -(* (* allocate_frame(bf | b) *) *) -(* (* ) else if (frame.num >= allocator.multiboot_start.num && frame.num <= allocator.multiboot_end.num) then ( *) *) -(* (* // frame is used by multiboot info structure *) *) -(* (* allocator.next_free_frame := @{num = allocator.multiboot_end.num + 1}; *) *) -(* (* let prval () = opt_some allocator in end; *) *) -(* (* allocate_frame(bf | b) *) *) -(* (* ) else ( *) *) -(* (* // frame is unused, increment `next_free_frame` and return it *) *) -(* (* allocator.next_free_frame.num := succ(allocator.next_free_frame.num); *) *) -(* (* let prval () = opt_some allocator in end; *) *) -(* (* frame *) *) -(* (* ); *) *) -(* (* end *) *) -(* (* else *) *) -(* (* let prval () = opt_some allocator in end; *) *) -(* (* @{num = i2sz(0)} // No free frames left *) *) -(* let prval () = opt_some p->obj in end; *) -(* @{num = i2sz(0)} *) -(* end *) -(* else *) -(* @{num = i2sz(0)} // No free frames left *) -(* *) -(* end *) -(**) -(* end *) -(**) -(* implement deallocate_frame(p) : void = let *) -(* in *) -(* *) -(* end *) +staload BOOT = "kernel/bootinfo/multiboot.sats" + +staload "./frame.sats" +staload "lib/SATS/init.sats" +staload "lib/DATS/init.dats" + +staload UN = "prelude/SATS/unsafe.sats" + +fn containing_address{l:addr}(address : ptr l):<> frame_t = + @{ + counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) + } + +fn containing_area(area : $BOOT.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(allocator : &frame_allocator_t) : void = let + val length = g1ofg0($BOOT.get_memory_mappings_n()) + val next_free_frame = allocator.next_free_frame + fun loop {n,i : nat | i < n} .. ( i : size_t i, n : size_t n) : $BOOT.memory_area_t = let + val entry = $BOOT.get_memory_mapping(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 (succ(i),n) + else + entry //TODO: fix + end +in + if (length > 0) then //TODO: fix + allocator.current_area := loop(i2sz(0), length); + + if (allocator.current_area.length > 1) then + let + val start_frame = containing_address(allocator.current_area.base_addr) + in + if (allocator.next_free_frame.num < start_frame.num) then + allocator.next_free_frame := start_frame + end +end + +local + + // Private function + extern fn _allocate_frame(allocator: &frame_allocator_t): frame_t + +in + local + // Static variable + var _v : frame_allocator_t? + prval () = opt_none _v + var v = uninitialized(_v) + // Reference to allocator + val allocator_ref = ref_make_viewptr{initializable frame_allocator_t} (view@v | addr@v) + in + + implement init(kernel_start, kernel_end, multiboot_start, multiboot_end) = let + val allocator = @{ + next_free_frame = containing_address(the_null_ptr), + current_area = $BOOT.invalid_area, + kernel_start = containing_address(kernel_start), + kernel_end = containing_address(kernel_end), + multiboot_start = containing_address(multiboot_start), + multiboot_end = containing_address(multiboot_end) + } : frame_allocator_t + + implement initialize$fwork(v) = ( + v := allocator; + $effmask_ref(choose_next_area(v)); + let prval () = opt_some v in true end + ) + in + initialize(allocator_ref) + end + + implement allocate_frame(): frame_t = let + implement exec$fwork(v) = $effmask_ref(_allocate_frame(v)) + in + exec(allocator_ref) + end + + end + + implement _allocate_frame(allocator) : frame_t = + if (allocator.current_area.type != 0u) then + let + val area = allocator.current_area + val frame = @{ num = allocator.next_free_frame.num } + + // last frame of current area + 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 + choose_next_area(allocator); + _allocate_frame(allocator) + ) else if (frame.num >= allocator.kernel_start.num && frame.num <= allocator.kernel_end.num) then ( + // frame is used by kernel + allocator.next_free_frame := @{num = allocator.kernel_end.num + 1}; + _allocate_frame(allocator) + ) else if (frame.num >= allocator.multiboot_start.num && frame.num <= allocator.multiboot_end.num) then ( + // frame is used by multiboot info structure + allocator.next_free_frame := @{num = allocator.multiboot_end.num + 1}; + _allocate_frame(allocator) + ) else ( + // frame is unused, increment `next_free_frame` and return it + allocator.next_free_frame.num := succ(allocator.next_free_frame.num); + frame + ); + end + else + @{num = i2sz(0)} // No free frames left + + +end diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats index 0926e6c..6ace8f9 100644 --- a/kernel/memory/frame.sats +++ b/kernel/memory/frame.sats @@ -1,25 +1,20 @@ -(* #define PAGE_SIZE 4096 *) -(**) -(* staload "kernel/bootinfo/multiboot.sats" *) -(**) -(* typedef frame_t = @{ *) -(* num = size_t *) -(* } *) -(**) -(* typedef frame_allocator_t = @{ *) -(* next_free_frame = frame_t, *) -(* current_area = memory_area_t, *) -(* kernel_start = frame_t, *) -(* kernel_end = frame_t, *) -(* multiboot_start = frame_t, *) -(* multiboot_end = frame_t *) -(* } *) -(**) -(* vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l - void | ptr l) *) -(**) -(* abst@ype frame_allocator = frame_allocator_t *) -(**) -(* fn containing_address {l : addr} (address : ptr l) :<> frame_t *) -(* fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) : frame_t *) -(* fn deallocate_frame (p : !allocptr) : void *) -(* (* fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void *) *) +#define PAGE_SIZE 4096 + +staload "kernel/bootinfo/multiboot.sats" + +typedef frame_t = @{ + num = size_t +} + +typedef frame_allocator_t = @{ + next_free_frame = frame_t, + current_area = memory_area_t, + kernel_start = frame_t, + kernel_end = frame_t, + multiboot_start = frame_t, + multiboot_end = frame_t +} + +fn allocate_frame () : frame_t +fn deallocate_frame () : void +fn init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr) : void -- cgit v1.2.3