aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/frame.dats
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-07-28 21:38:35 +0200
committerXander <xander@biltopia.org>2023-07-28 21:38:35 +0200
commitb78762c92afee705e618f29f89897db8b45df3dd (patch)
tree90833dc90cd3b58ee84d19357fb1d945d40823ec /kernel/memory/frame.dats
parentc6ad352a25b6b1d45e56090ccc0432d123b043bc (diff)
downloadats-os-b78762c92afee705e618f29f89897db8b45df3dd.tar.xz
ats-os-b78762c92afee705e618f29f89897db8b45df3dd.zip
optional implementation of multboot 1
Diffstat (limited to 'kernel/memory/frame.dats')
-rw-r--r--kernel/memory/frame.dats258
1 files changed, 129 insertions, 129 deletions
diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats
index 5a950ad..8a9160b 100644
--- a/kernel/memory/frame.dats
+++ b/kernel/memory/frame.dats
@@ -1,131 +1,131 @@
-#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<uint8>(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) :<!wrt> 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} .<n-i>. (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<frame_allocator_t>(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 "./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<uint8>(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) :<!wrt> 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} .<n-i>. (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<frame_allocator_t>(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 *)