aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/memory')
-rw-r--r--kernel/memory/frame.dats248
-rw-r--r--kernel/memory/frame.sats45
2 files changed, 139 insertions, 154 deletions
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<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 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<uint8>(area.base_addr,area.length - i2sz(1)))
+
+//FIX: function doesn't handle no frames left
+fn choose_next_area(allocator : &frame_allocator_t) :<!wrt,!ref> 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} .<n-i>. ( i : size_t i, n : size_t n) :<!ref> $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):<!wrt,!ref> frame_t
+
+in
+ local
+ // Static variable
+ var _v : frame_allocator_t?
+ prval () = opt_none _v
+ var v = uninitialized<frame_allocator_t>(_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<frame_allocator_t>(v) = (
+ v := allocator;
+ $effmask_ref(choose_next_area(v));
+ let prval () = opt_some v in true end
+ )
+ in
+ initialize<frame_allocator_t>(allocator_ref)
+ end
+
+ implement allocate_frame(): frame_t = let
+ implement exec$fwork<frame_allocator_t><frame_t>(v) = $effmask_ref(_allocate_frame(v))
+ in
+ exec<frame_allocator_t><frame_t>(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 -<lin,prf> 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) :<!ref,!wrt> 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:13:08 +0000