aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-07-21 18:02:54 +0200
committerXander <xander@biltopia.org>2023-07-21 18:02:54 +0200
commit9226c8bb581c363a552998663704c483f35f6aae (patch)
tree857a7c8119b5df93d3340f8acd317b06fd254d84
parent589e17e4faf369857fd916cbe699bc72c193b9a3 (diff)
downloadats-os-9226c8bb581c363a552998663704c483f35f6aae.tar.xz
ats-os-9226c8bb581c363a552998663704c483f35f6aae.zip
Working on frame allocation
-rw-r--r--Makefile2
-rw-r--r--kernel/bootinfo/multiboot.dats4
-rw-r--r--kernel/bootinfo/multiboot.sats10
-rw-r--r--kernel/main.dats1
-rw-r--r--kernel/memory/frame.dats57
-rw-r--r--kernel/memory/frame.sats25
6 files changed, 91 insertions, 8 deletions
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<memory_map_t>(p);
+ boot_p->memory_map := $UN.ptr0_get<memory_areas_t>(p);
boot_p->memory_map.entries := ptr_add<uint32>(p,4)
)
| 9u => (
@@ -60,7 +60,7 @@ end
implement get_memory_mapping(p,n) = (
assertloc(n < get_memory_mappings_n(p));
- $UN.ptr0_get<memory_entry_t>(ptr_add<memory_entry_t>(p.2->memory_map.entries,n))
+ $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(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 -<lin,prf> 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<uint8>(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 -<lin,prf> 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