adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

riscv platform: removed unused region in address space diagram 

co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2019-01-07 16:31:47 +11:00 committed by Rafal Kolanski
parent 78e57e2d90
commit ac9ff925ce
1 changed files with 7 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
spec/machine/RISCV64/Platform.thy
View File

@ -34,19 +34,19 @@ abbreviation (input) "fromPAddr \<equiv> id"
| Kernel ELF |
+-----------------KERNEL_BASE-+ --+ 2^64 - 2GiB
| | |
| | |
| | |
| PSpace | |
| (direct kernel mappings) | +----+
| | | |
| | | |
+-------------------PPTR_BASE-+ --+ |
| | |
| User | |
| |
+-----------------------------+ 2^64 - 2^c +-------------------------+
| | | |
| | | |
| | |
+-------------------PPTR_BASE-+ --+ 2^64 - 2^c
| | +-------------------------+
| | | | |
| Invalid | | | |
| | | | not |
| (not canonical) | | | not |
| | | | kernel |
| | | | addressable |
+-----------------------------+ 2^c | | |
@ -72,8 +72,6 @@ c = one less than number of bits the page tables can translate
= sign extension bit for canonical addresses
(= 47 on x64, 38 on RISCV64 sv39, 47 on RISCV64 sv48)
On RISCV, PPTR_BASE is 2^64 - 2^c, i.e. there is no user region at the top.
*)
definition canonical_bit :: nat