diff options
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 8 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 6 | ||||
| -rw-r--r-- | kernel/main.dats | 29 | ||||
| -rw-r--r-- | kernel/memory/frame.dats | 248 | ||||
| -rw-r--r-- | kernel/memory/frame.sats | 45 |
5 files changed, 160 insertions, 176 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index ff10c40..518962d 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -9,7 +9,7 @@ staload UN = "prelude/SATS/unsafe.sats" local - // Private function + // Private functions extern castfn ui2sz (n : uint) :<> [n : nat] size_t n extern fn _get_memory_mappings_n(boot_info: !boot_info_t):<> [n:nat] size_t n extern fn _get_memory_mapping(boot_info: !boot_info_t,n : size_t):<> memory_area_t @@ -54,7 +54,7 @@ in if (type != 0u) then loop(boot_info,ptr_add<uint8>(p, next)) else - unsafe_init(boot_info) + unsafe_init(boot_info) //UNSAFE: end implement initialize$fwork<boot_info_t>(v) = ( @@ -73,13 +73,13 @@ in implement get_memory_mappings_n() = let implement exec$fwork<boot_info_t><size_t>(v) = _get_memory_mappings_n(v) in - exec<boot_info_t><size_t>(bootinfo_ref) + $effmask_wrt(exec<boot_info_t><size_t>(bootinfo_ref)) end implement get_memory_mapping(n) = let implement exec$fwork<boot_info_t><memory_area_t>(v) = _get_memory_mapping(v,n) in - exec<boot_info_t><memory_area_t>(bootinfo_ref) + $effmask_wrt(exec<boot_info_t><memory_area_t>(bootinfo_ref)) end implement print_memory_mappings() = let diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index 16be379..2dfa205 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -55,9 +55,9 @@ macdef invalid_area = @{ fun init(p : Ptr1) :void -fn get_memory_mappings_n () : size_t -fn get_memory_mapping (n : size_t) : memory_area_t -fn print_memory_mappings () : void // Print all available memory area's +fn get_memory_mappings_n () :<!ref> size_t +fn get_memory_mapping (n : size_t) :<!ref> memory_area_t +fn print_memory_mappings () :<!ref,!wrt> void // Print all available memory area's fn get_elf_headers_n () : size_t fn get_elf_header (n : size_t) : elf64_shdr_t diff --git a/kernel/main.dats b/kernel/main.dats index 96cfdda..bbac122 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -2,7 +2,7 @@ staload "kernel/interrupts/idt.sats" staload BOOT = "kernel/bootinfo/multiboot.sats" -staload "kernel/memory/frame.sats" +staload FRAME = "kernel/memory/frame.sats" staload "lib/SATS/writer.sats" %{^ @@ -25,11 +25,11 @@ in i2sz(0) end -(* fn test(allocptr : !allocptr, bootptr : !bootptr) : void = let *) -(* fun loop(i : int) : void = if (i < 160) then( let val _ = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) in end; loop(succ(i))) *) -(* in *) -(* loop(0) *) -(* end *) +fn test() : void = let + fun loop(i : int) : void = if (i < 160) then( let val _ = $FRAME.allocate_frame() in end; loop(succ(i))) +in + loop(0) +end extern fun breakpoint() :void = "mac#" @@ -39,21 +39,20 @@ extern fun entry(p : Ptr1) : void = "ext#" implement entry(p) = let val () = $BOOT.init(p); val (kernel_start,kernel_end) = $BOOT.get_kernel_ranges() - (* val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr) *) - (* val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr) *) + val (multiboot_start,multiboot_end) = $BOOT.get_multiboot_ranges() + val () = $FRAME.init(kernel_start,kernel_end,multiboot_start,multiboot_end); in - // Initialize boot info struct $BOOT.print_memory_mappings(); $BOOT.print_elf_headers(); println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); - (* test(allocptr,bootptr); *) - (* let *) - (* val frame = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) *) - (* in *) - (* println!(frame.num) *) - (* end; *) + test(); + let + val frame = $FRAME.allocate_frame() + in + println!(frame.num) + end; // Initialize interrupt table idt_init(); 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 |