diff options
Diffstat (limited to 'kernel/memory/paging')
| -rw-r--r-- | kernel/memory/paging/entry.dats | 14 | ||||
| -rw-r--r-- | kernel/memory/paging/entry.sats | 4 | ||||
| -rw-r--r-- | kernel/memory/paging/page.dats | 117 | ||||
| -rw-r--r-- | kernel/memory/paging/page.sats | 18 | ||||
| -rw-r--r-- | kernel/memory/paging/table.dats | 44 | ||||
| -rw-r--r-- | kernel/memory/paging/table.sats | 9 |
6 files changed, 191 insertions, 15 deletions
diff --git a/kernel/memory/paging/entry.dats b/kernel/memory/paging/entry.dats index 7fa97b9..76d6c0c 100644 --- a/kernel/memory/paging/entry.dats +++ b/kernel/memory/paging/entry.dats @@ -13,8 +13,7 @@ assume entry_type = uint64 val zero = u2u64(0u) -fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let - implement array_foreach$fwork<entry_flag><entry_t>(f,k) = k := k lor $UN.cast{entry_t}(1 << (case+ f of +implement add_flag(entry,f) = entry lor $UN.cast{entry_t}(1 << (case+ f of | PRESENT() => 0 | WRITABLE() => 1 | USER_ACCESSIBLE() => 2 @@ -25,8 +24,11 @@ fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let | GLOBAL() => 8 | NO_EXECUTE() => 63 )) + +fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) :<> entry_t = let + implement array_foreach$fwork<entry_flag><entry_t>(f,k) = k := add_flag(k,f) var k = g0ofg1(u2u64(0u)) - val _ = array_foreach_env<entry_flag><entry_t>(arr,n,k) + val _ = $effmask_all(array_foreach_env<entry_flag><entry_t>(arr,n,k)) in k end @@ -35,7 +37,7 @@ implement is_unused(entry) = entry = zero implement set_unused(entry) = entry := zero implement contains_flag(entry,flag) = (flags2entry(flags,i2sz(1)) land entry) != zero where { - var flags = @[entry_flag](PRESENT) + var flags = @[entry_flag](flag) } implement pointed_frame(entry) = @@ -44,9 +46,9 @@ implement pointed_frame(entry) = else create_unvalid() -implement entry_set(entry,frame,flags,n) = let +implement create_entry(frame,flags,n) = let val x = Ptr0_to_u64($FRAME.start_address(frame)) in assertloc((x land u2u64(0xFFF0000000000FFFu)) = zero); - entry := (x lor flags2entry(flags,n)) + (x lor flags2entry(flags,n)) end diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats index 17a9f72..fc20a20 100644 --- a/kernel/memory/paging/entry.sats +++ b/kernel/memory/paging/entry.sats @@ -1,5 +1,6 @@ staload "kernel/memory/frame.sats" staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" abst@ype entry_type = uint64 typedef entry_t = entry_type @@ -22,4 +23,5 @@ fn set_unused(&entry_t) :<!wrt> void fn contains_flag(entry_t,entry_flag):<> bool fn pointed_frame(entry_t) : Valid frame_t -fn entry_set{n:nat}(&entry_t,frame_t,&(@[entry_flag][n]),size_t n) : void +fn add_flag(entry_t,entry_flag) : entry_t +fn create_entry{s:nat}(frame_t,&(@[entry_flag][s]),size_t s) : entry_t diff --git a/kernel/memory/paging/page.dats b/kernel/memory/paging/page.dats new file mode 100644 index 0000000..2880c18 --- /dev/null +++ b/kernel/memory/paging/page.dats @@ -0,0 +1,117 @@ +#define ATS_DYNLOADFLAG 0 + +#include "kernel/prelude/kernel_prelude.hats" + +staload "./page.sats" +staload FR = "kernel/memory/frame.sats" +staload "./table.sats" + +staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" + +datatype table_level = + | Level4 + | Level3 + | Level2 + | Level1 + +fn start_address(page : page_t) : size_t = page.num * $FR.PAGE_SIZE + +fn get_index(page: page_t,n : intLte(3)) = g1ofg0((page.num >> (27 - 9 * n)) land i2sz(511)) + +//NOTE: huge page handler not implemented +fn translate_page(page: page_t) : Valid $FR.frame_t = let + fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n) : Valid $FR.frame_t = let + staload "./entry.sats" + val index = get_index(page,count) + in + if index < ENTRY_COUNT then let + val v = next_table(table,index) + in + if is_valid(v) then let + val table_next = unwrap_valid(v) + in + if count < 2 then + loop(table_next,succ(count)) + else( + consume(table_next); + frame + ) where { + val index = get_index(page,count+1) + val frame = (if index < ENTRY_COUNT then pointed_frame(table_next[index]) else create_unvalid()) : Valid $FR.frame_t + } + end + else ( + destroy_unvalid(v); + println!("Unvalid table pointer encountered: ", count); + create_unvalid()) + end + else ( + consume(table); + println!("Table index too big"); + create_unvalid()) + end +in + loop(get_P4(),0) +end + +implement translate(virtual_addr) = let + val offset = Ptr0_to_sz(virtual_addr) % i2sz($FR.PAGE_SIZE) + val vframe = translate_page(containing_address(virtual_addr)) +in + if is_valid(vframe) then let + val frame = unwrap_valid(vframe) + in + create_valid (sz_to_Ptr0(frame.num * $FR.PAGE_SIZE + offset)) + end + else ( + destroy_unvalid(vframe); + create_unvalid(); + ) +end + +implement containing_address(address) = ( + assertloc(address < ulint_to_Ptr0(0x0000800000000000ul) || + address >= ulint_to_Ptr0(0xFFFF800000000000ul)); + @{num = Ptr0_to_sz(address) / i2sz($FR.PAGE_SIZE)} +) + +// TODO: implement and_then and or_else for valid (like in rust) +implement map_to{s}(page,frame,flags,size) = let + staload "./entry.sats" + fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n, flags: &(@[entry_flag][s])) : void = let + staload "lib/SATS/panic.sats" + val index = get_index(page,count) + val () = println!(index) + in + if index < ENTRY_COUNT then let + val v = next_table_create(table,index) + in + if is_valid(v) then let + val table_next = unwrap_valid(v) + in + if count < 2 then + loop(table_next,succ(count),flags) + else let + val index = get_index(page,count+1) + in + if index < ENTRY_COUNT then ( + assertloc(is_unused(table_next[index])); + table_next[index] := add_flag(create_entry(frame, flags,size),PRESENT); + ); + consume(table_next); + end + end + else ( + destroy_unvalid(v); + panic("Could not create table")) + end + else ( + consume(table); + println!("Table index too big")) + end +in + loop(get_P4(),0,flags) +end + +implement map(page,flags,size) = map_to(page,$FR.allocate_frame(),flags,size) diff --git a/kernel/memory/paging/page.sats b/kernel/memory/paging/page.sats new file mode 100644 index 0000000..1de50c6 --- /dev/null +++ b/kernel/memory/paging/page.sats @@ -0,0 +1,18 @@ +staload FRAME = "kernel/memory/frame.sats" + +staload "lib/SATS/valid.sats" +staload "./entry.sats" + +typedef vaddr = Ptr0 + +typedef page_t = @{ + num = size_t +} + +fn translate(vaddr) : Valid $FRAME.paddr + +fn containing_address(vaddr) : page_t + +fn map_to{n:nat}(page_t,$FRAME.frame_t,&(@[entry_flag][n]),size : size_t n): void + +fn map{n:nat}(page_t,&(@[entry_flag][n]),size : size_t n) : void diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats index e636c6c..d3bfe93 100644 --- a/kernel/memory/paging/table.dats +++ b/kernel/memory/paging/table.dats @@ -28,6 +28,16 @@ in create_unvalid() end +// Checks if next table exists and returns bool +fn next_table_exists{n:int|n < 3}(table: !table_t(n),index : sizeLt(ENTRY_COUNT)):<> bool = let + val vnext = next_table_address(table,index) +in + if is_valid(vnext) then + let val _ = unwrap_valid(vnext) in true end + else + (destroy_unvalid(vnext); false) +end + implement table_get_at(table,i) = let val entry = (table.3->[i]) : entry_t in @@ -36,7 +46,8 @@ end implement table_set_at(table,i,x) = table.3->[i] := x -implement set_zero(table) = let +// Set all the entries in the table to unused (zero) +fn set_zero(table: &Table_t):<!wrt> void = let fun loop{i:nat | i < ENTRY_COUNT}.<ENTRY_COUNT-i>.(i : size_t i,t : !Table_t):<!wrt> void = let in set_unused(t.3->[i]); @@ -54,6 +65,8 @@ local in + // TODO: define safe unique ownership for this table + // see https://os.phil-opp.com/page-tables/#safety-2 implement get_P4() = let val (pf,fpf | p) = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)) in @@ -76,7 +89,32 @@ in let val () = destroy_unvalid(next) in - create_unvalid() - end; + create_unvalid(); + end + end + + implement next_table_create(table,index) = let + staload "kernel/memory/frame.sats" + in + if ~next_table_exists(table,index) then ( + println!("not exists"); + assertloc(~contains_flag(table[index],HUGE_PAGE)); + table[index] := create_entry(allocate_frame(),flags,i2sz(2)) where { + var flags = @[entry_flag](PRESENT,WRITABLE) + }; + let + val vnext = next_table(table,index) + in + if is_valid(vnext) then + let var next = unwrap_valid(vnext) in (set_zero(next); create_valid(next)) end + else ( + destroy_unvalid(vnext); + create_unvalid() + ) + end + ) else + $UN.castvwtp0(next_table(table,index)) //This is safe end + end + diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats index 491b77e..6b8e188 100644 --- a/kernel/memory/paging/table.sats +++ b/kernel/memory/paging/table.sats @@ -17,11 +17,10 @@ fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t): overload [] with table_get_at overload [] with table_set_at -// Set all the entries in the table to unused (zero) -fn set_zero(&Table_t):<!wrt> void - castfn consume(Table_t): void -fun get_P4() : table_t 0 +fn get_P4() : table_t 0 + +fn next_table{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) -fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) +fn next_table_create{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) |