diff options
Diffstat (limited to 'kernel/memory')
| -rw-r--r-- | kernel/memory/frame.dats | 121 | ||||
| -rw-r--r-- | kernel/memory/frame.sats | 8 |
2 files changed, 78 insertions, 51 deletions
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 |