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

riscv aspec: rename kernelBase to kernelELFBase and update address space layout comment

This commit is contained in:
Victor Phan 2019-10-25 12:13:54 +11:00 committed by Gerwin Klein
parent 0661581e44
commit 453233faad
1 changed files with 56 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -27,45 +27,59 @@ abbreviation (input) "toPAddr \<equiv> id"
abbreviation (input) "fromPAddr \<equiv> id"
(* Address space layout:
The top half of the address space is reserved for the kernel. This means that 256 top level
entries are for the user, and 256 are for the kernel. This will be further split into the
'regular' kernel window, which contains mappings to physical memory, a small (1GiB) higher
kernel image window that we use for running the actual kernel from and a top 1GiB window for
kernel device mappings. This means that between PPTR_BASE and
KERNEL_BASE there are 254 entries remaining, which represents how much physical memory
can be used.
+-----------------------------+ 2^64
| Kernel Devices |
+-------------------PPTR_KDEV-+ 2^64 - 1GiB
| Kernel ELF |
+-----------------KERNEL_BASE-+ --+ 2^64 - 2GiB
| | |
| | |
| | |
| PSpace | |
| (direct kernel mappings) | +----+
| | | |
| | | |
| | | |
| | |
+-------------------PPTR_BASE-+ --+ 2^64 - 2^c
| | +-------------------------+
| | | | |
| Invalid | | | |
| (not canonical) | | | not |
| | | | kernel |
| | | | addressable |
+-----------------------------+ 2^c | | |
| | | | |
| | | | |
| | | +- --------------------------+ PADDR_TOP =
| | | | | | KERNEL_BASE - PPTR_BASE
| | | | | |
| | | | | |
| User | | | | |
| | | | | |
| | +------+ +-------------------------+ PADDR_LOAD + 1GiB
| | kernel | | Kernel ELF |
| | addressable | +-------------------------+ PADDR_LOAD
| | | | |
| | | | |
+-----------------------------+ 0 +- +-------------------------+ 0 PADDR_BASE
Almost all of the top 256 kernel entries will contain 1GiB page mappings. The only 2 entries
that contain a 2nd level PageTable consisting of 2MiB page entries is the entry
for the 1GiB Kernel ELF region and the 1GiB region corresponding to the physical memory
of the kernel ELF in the kernel window. The same 2nd level PageTable is used and so both
entries refer to the same 1GiB of physical memory.
This means that the 1GiB kernel ELF mapping will correspond to physical memory with a 1GiB
alignment.
virtual address space physical address space
+-----------------------------+ 2^64
| Kernel Devices |
-> +-------------------PPTR_KDEV-+ 2^64 - 1GiB
| | Kernel ELF |
----| +-------------KERNEL_ELF_BASE-+ --+ 2^64 - 2GiB + (PADDR_LOAD % 1GiB)
| | | |
| -> +-----------------KERNEL_BASE-+ --+ 2^64 - 2GiB
Shared 1GiB| | | |
table entry| | PSpace | |
| | (direct kernel mappings) | +----+
------>| | | |
| | | |
+-------------------PPTR_BASE-+ --+ 2^64 - 2^c
| | | +-------------------------+
| | | | |
| | | | |
| Invalid | | | |
| | | | not |
| | | | kernel |
| | | | addressable |
+-----------------------------+ 2^c | | |
| | | | |
| | | | |
| | | +- --------------------------+ PADDR_TOP =
| | | | | | KERNEL_BASE - PPTR_BASE
| | | | | |
| | | | | |
| User | | | | |
| | | | | |
| | +------+ +-------------------------+ PADDR_HIGH_TOP =
| | kernel | | Kernel ELF | (PPTR_KDEV - KERNEL_ELF_BASE + PADDR_LOAD)
| | addressable | +-------------------------+ PADDR_LOAD
| | | | |
| | | | |
+-----------------------------+ 0 +- +-------------------------+ 0 PADDR_BASE
virtual address space physical address space
c = one less than number of bits the page tables can translate
@ -78,12 +92,12 @@ definition canonical_bit :: nat
where
"canonical_bit = 38"
definition kernelBase :: word64
definition kernelELFBase :: word64
where
"kernelBase = - (1 << 31) + 0x4000000" (* 2^64 - 2 GiB + 2^26 *)
"kernelELFBase = - (1 << 31) + 0x4000000" (* 2^64 - 2 GiB + 2^26 *)
lemma "kernelBase = 0xFFFFFFFF84000000" (* Sanity check with C *)
by (simp add: kernelBase_def)
lemma "kernelELFBase = 0xFFFFFFFF84000000" (* Sanity check with C *)
by (simp add: kernelELFBase_def)
definition paddrLoad :: word64
where
@ -91,7 +105,7 @@ definition paddrLoad :: word64
definition kernelBaseOffset :: word64
where
"kernelBaseOffset = kernelBase - paddrLoad"
"kernelBaseOffset = kernelELFBase - paddrLoad"
definition pptrBase :: word64
where