diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 4 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 5 | ||||
| -rw-r--r-- | kernel/main.dats | 26 | ||||
| -rw-r--r-- | kernel/memory/frame.dats | 121 | ||||
| -rw-r--r-- | kernel/memory/frame.sats | 8 |
5 files changed, 95 insertions, 69 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 4df903e..9eee595 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -45,7 +45,7 @@ end end -extern castfn ui2sz (n : uint) : [n : nat] size_t n +extern castfn ui2sz (n : uint) :<> [n : nat] size_t n //------------Memory------------------------ @@ -59,7 +59,7 @@ end // TODO: here use optional datatype (fix runtime alloc) implement get_memory_mapping(pf | p,n) = ( - assertloc(n < get_memory_mappings_n(pf | p)); + (* assertloc(n < get_memory_mappings_n(pf | p)); *) $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p->memory_map.entries,n)) ) diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index 684286b..1a2e6db 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -1,4 +1,3 @@ - typedef tag_t = @{ type = uint32, // Identifier of tag size = [n : nat | n >= 8] uint n // Size of tag (not including padding) @@ -50,8 +49,8 @@ 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 {l : agz} (pf : !boot_info_t@l | p : ptr l) : [n:nat] size_t n -fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) : memory_area_t +fn get_memory_mappings_n {l : agz} (pf : !boot_info_t@l | p : ptr l) :<> [n:nat] size_t n +fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) :<> memory_area_t fn print_memory_mappings (p : !bootptr) : void // Print all available memory area's fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n diff --git a/kernel/main.dats b/kernel/main.dats index 48bff24..dadcd2d 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -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(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 *) extern fun breakpoint() :void = "mac#" @@ -43,19 +43,19 @@ implement entry(p) = let val bootptr = boot_info_init(p) val (kernel_start,kernel_end) = get_kernel_ranges(bootptr) val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr) - val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr) + (* val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr) *) in print_memory_mappings(bootptr); print_elf_headers(bootptr); 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(allocptr,bootptr); *) + (* let *) + (* val frame = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) *) + (* in *) + (* println!(frame.num) *) + (* end; *) // Initialize interrupt table idt_init(); @@ -68,7 +68,7 @@ in let prval () = bootptr.1(bootptr.0) - prval () = allocptr.1(allocptr.0) + (* prval () = allocptr.1(allocptr.0) *) in end diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats index b1d86af..fad0420 100644 --- a/kernel/memory/frame.dats +++ b/kernel/memory/frame.dats @@ -4,22 +4,25 @@ 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 = + +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))) +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{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let +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 = p->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 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 @@ -32,26 +35,27 @@ fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k end in if (length > 0) then //TODO: fix - p->current_area := loop(bf | b, i2sz(0), length); + allocator.current_area := loop(bf | b, i2sz(0), length); - if (p->current_area.length > 1) then + if (allocator.current_area.length > 1) then let - val start_frame = containing_address(p->current_area.base_addr) + val start_frame = containing_address(allocator.current_area.base_addr) in - if (p->next_free_frame.num < start_frame.num) then - p->next_free_frame := start_frame + if (allocator.next_free_frame.num < start_frame.num) then + allocator.next_free_frame := start_frame end end local -var frame_allocator : frame_allocator_t +var allocator_static : frame_allocator_t? +prval () = opt_none allocator_static +var allocator = empty<frame_allocator_t>(allocator_static) +val allocator_ref = ref_make_viewptr{enablable frame_allocator_t} (view@allocator | addr@allocator) in - implement frame_allocator_init(kernel_start, kernel_end, multiboot_start, multiboot_end, b) : allocptr = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (frame_allocator_t@l) // takeout proof UNSAFE: - prval (pf, fpf) = __assert (addr@frame_allocator) + 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, @@ -59,48 +63,69 @@ in 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 - frame_allocator := allocator; - choose_next_area(pf,b.0 | addr@frame_allocator, b.2); - (pf, fpf | addr@frame_allocator) + if not p->enabled then let + prval () = opt_unnone p->obj + in + p->obj := allocator; + p->enabled := true; + (* choose_next_area(b.0 | b.2, !p); *) + let prval () = opt_some p->obj in end; + end end -end - -implement allocate_frame(pf , bf | p,b) : frame_t = - if (p->current_area.type != 0u) 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_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(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 +implement allocate_frame(bf | b) : frame_t = let + val (vbox pf | p) = ref_get_viewptr(allocator_ref) + in + if p->enabled 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 diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats index d965567..0de5056 100644 --- a/kernel/memory/frame.sats +++ b/kernel/memory/frame.sats @@ -17,7 +17,9 @@ typedef frame_allocator_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 +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) : allocptr +fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void |