From 9226c8bb581c363a552998663704c483f35f6aae Mon Sep 17 00:00:00 2001 From: Xander Date: Fri, 21 Jul 2023 18:02:54 +0200 Subject: Working on frame allocation --- Makefile | 2 +- kernel/bootinfo/multiboot.dats | 4 +-- kernel/bootinfo/multiboot.sats | 10 ++++---- kernel/main.dats | 1 + kernel/memory/frame.dats | 57 ++++++++++++++++++++++++++++++++++++++++++ kernel/memory/frame.sats | 25 ++++++++++++++++++ 6 files changed, 91 insertions(+), 8 deletions(-) create mode 100644 kernel/memory/frame.dats create mode 100644 kernel/memory/frame.sats diff --git a/Makefile b/Makefile index f56a430..a4c3247 100644 --- a/Makefile +++ b/Makefile @@ -22,7 +22,7 @@ CLFAGS_ATS := CFLAGS_ATS += -D_ATS_CCOMP_RUNTIME_NONE_ CFLAGS_ATS += -D_ATS_CCOMP_EXCEPTION_NONE_ -CFLAGS=-ffreestanding -mcmodel=large -mno-red-zone -mgeneral-regs-only -m64 -fpack-struct -fno-stack-protector +CFLAGS=-ffreestanding -mcmodel=large -mno-red-zone -mgeneral-regs-only -m64 -fpack-struct -fno-stack-protector -nostdlib .PHONY: all clean run iso diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 742c7ed..6ea7b00 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -23,7 +23,7 @@ implement boot_info_init (p : Ptr1) = let in case+ type of | 6u => ( - boot_p->memory_map := $UN.ptr0_get(p); + boot_p->memory_map := $UN.ptr0_get(p); boot_p->memory_map.entries := ptr_add(p,4) ) | 9u => ( @@ -60,7 +60,7 @@ end implement get_memory_mapping(p,n) = ( assertloc(n < get_memory_mappings_n(p)); - $UN.ptr0_get(ptr_add(p.2->memory_map.entries,n)) + $UN.ptr0_get(ptr_add(p.2->memory_map.entries,n)) ) implement print_memory_mappings(p) = let diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index 0d89040..3909fdd 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -4,15 +4,15 @@ typedef tag_t = @{ size = [n : nat | n >= 8] uint n // Size of tag (not including padding) } -typedef memory_entry_t = @{ +typedef memory_area_t = @{ base_addr = Ptr1, // Start of physical address - length = uint64, // Size of memory region in bytes + length = [n : nat | n > 0 ] size_t n , // Size of memory region in bytes (64 bits) type = uint, // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information, // 4: reserved memory (preserved on hibernation), Other: reserved area reserved = uint 0 } -typedef memory_map_t = @{ +typedef memory_areas_t = @{ tag = tag_t, entry_size = [n : nat | n > 0 && n % 8 == 0] uint n, entry_version = uint, @@ -42,7 +42,7 @@ typedef elf64_shdr_t = @{ typedef boot_info_t = @{ total_size = uint, // total size of boot information - memory_map = memory_map_t, + memory_map = memory_areas_t, elf_tag = elf_tag_t } @@ -51,7 +51,7 @@ vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l - void | p fun boot_info_init(p : Ptr1) : bootptr fn get_memory_mappings_n (p : !bootptr) : [n:nat] size_t n -fn get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t +fn get_memory_mapping (p : !bootptr, n : size_t) : memory_area_t fn print_memory_mappings (p : !bootptr) : void fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n diff --git a/kernel/main.dats b/kernel/main.dats index 2a89603..94955ee 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -14,6 +14,7 @@ staload UN = "prelude/SATS/unsafe.sats" } %} + extern castfn char_arr2string {n:nat} (arr : &(@[char][n])) : string n extern fun breakpoint() :void = "mac#" diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats new file mode 100644 index 0000000..26ff412 --- /dev/null +++ b/kernel/memory/frame.dats @@ -0,0 +1,57 @@ +#include "kernel/prelude/kernel_prelude.hats" + +#define ATS_DYNLOADFLAG 0 + +staload "./frame.sats" +staload "kernel/bootinfo/multiboot.sats" + +staload UN = "prelude/SATS/unsafe.sats" + +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 + +in + +end + +implement allocate_frame(pf , bf | p,b) : frame_t = + if (p->current_area.length > 1) 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))) + in + if (frame.num > last_frame_area.num) then ( + // all frames of current area are used, switch to next area + choose_next_area(pf, bf | p,b); + allocate_frame(pf,bf | p,b) + ) else if (frame.num > p->kernel_start.num && frame.num <= p->kernel_end.num) then ( + // frame is used by kernel + p->next_free_frame := @{num = p->kernel_end.num + 1}; + allocate_frame(pf,bf | p,b) + ) else if (frame.num > p->multiboot_start.num && frame.num <= p->multiboot_end.num) then ( + // frame is used by multiboot info structure + p->next_free_frame := @{num = p->multiboot_end.num + 1}; + allocate_frame(pf,bf | p,b) + ) else ( + // frame is unused, increment `next_free_frame` and return it + p->next_free_frame.num := succ(p->next_free_frame.num); + frame + ); + end + else + @{num = i2sz(0)} // No free frames left + + + +implement deallocate_frame(p) : void = let + +in + +end + diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats new file mode 100644 index 0000000..441b85a --- /dev/null +++ b/kernel/memory/frame.sats @@ -0,0 +1,25 @@ +#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, + num_areas = size_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) + +fn containing_address {l : addr} (address : ptr l) : frame_t + +fn allocate_frame {l : agz}{k : agz} (pf : !frame_allocator_t @ l >> frame_allocator_t @ l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : frame_t + +fn deallocate_frame (p : !allocptr) : void -- cgit v1.2.3