Theory MMU
section ‹Memory Management Unit (MMU)›
theory MMU
imports Main RegistersOps Sparc_Types
begin
section ‹MMU Sizing›
text‹
We need some citation here for documentation about the MMU.
›
text‹The MMU uses the Address Space Identifiers (ASI) to control memory access.
ASI = 8, 10 are for user; ASI = 9, 11 are for supervisor.›
subsection "MMU Types"
type_synonym word_PTE_flags = word8
type_synonym word_length_PTE_flags = word_length8
subsection "MMU length values"
text‹Definitions for the length of the virtua address, page size,
virtual translation tables indexes, virtual address offset and Page protection flags›
definition length_entry_type :: "nat"
where "length_entry_type ≡ LENGTH(word_length_entry_type)"
definition length_phys_address:: "nat"
where "length_phys_address ≡ LENGTH(word_length_phys_address)"
definition length_virtua_address:: "nat"
where "length_virtua_address ≡ LENGTH(word_length_virtua_address)"
definition length_page:: "nat" where "length_page ≡ LENGTH(word_length_page)"
definition length_t1:: "nat" where "length_t1 ≡ LENGTH(word_length_t1)"
definition length_t2:: "nat" where "length_t2 ≡ LENGTH(word_length_t2)"
definition length_t3:: "nat" where "length_t3 ≡ LENGTH(word_length_t3)"
definition length_offset:: "nat" where "length_offset ≡ LENGTH(word_length_offset)"
definition length_PTE_flags :: "nat" where
"length_PTE_flags ≡ LENGTH(word_length_PTE_flags)"
subsection "MMU index values"
definition va_t1_index :: "nat" where "va_t1_index ≡ length_virtua_address - length_t1"
definition va_t2_index :: "nat" where "va_t2_index ≡ va_t1_index - length_t2"
definition va_t3_index :: "nat" where "va_t3_index ≡ va_t2_index - length_t3"
definition va_offset_index :: "nat" where "va_offset_index ≡ va_t3_index - length_offset"
definition pa_page_index :: "nat"
where "pa_page_index ≡ length_phys_address - length_page"
definition pa_offset_index :: "nat" where
"pa_offset_index ≡ pa_page_index -length_page"
section ‹MMU Definition›
record MMU_state =
registers :: "MMU_context"
text ‹The following functions access MMU registers via addresses.
See UT699LEON3FT manual page 35.›
definition mmu_reg_val:: "MMU_state ⇒ virtua_address ⇒ machine_word option"
where "mmu_reg_val mmu_state addr ≡
if addr = 0x000 then
Some ((registers mmu_state) CR)
else if addr = 0x100 then
Some ((registers mmu_state) CTP)
else if addr = 0x200 then
Some ((registers mmu_state) CNR)
else if addr = 0x300 then
Some ((registers mmu_state) FTSR)
else if addr = 0x400 then
Some ((registers mmu_state) FAR)
else None"
definition mmu_reg_mod:: "MMU_state ⇒ virtua_address ⇒ machine_word ⇒
MMU_state option" where
"mmu_reg_mod mmu_state addr w ≡
if addr = 0x000 then
Some (mmu_state⦇registers := (registers mmu_state)(CR := w)⦈)
else if addr = 0x100 then
Some (mmu_state⦇registers := (registers mmu_state)(CTP := w)⦈)
else if addr = 0x200 then
Some (mmu_state⦇registers := (registers mmu_state)(CNR := w)⦈)
else if addr = 0x300 then
Some (mmu_state⦇registers := (registers mmu_state)(FTSR := w)⦈)
else if addr = 0x400 then
Some (mmu_state⦇registers := (registers mmu_state)(FAR := w)⦈)
else None"
section ‹Virtual Memory›
subsection ‹MMU Auxiliary Definitions›
definition getCTPVal:: "MMU_state ⇒ machine_word"
where "getCTPVal mmu ≡ (registers mmu) CTP"
definition getCNRVal::"MMU_state ⇒ machine_word"
where "getCNRVal mmu ≡ (registers mmu) CNR"
text‹
The physical context table address is got from the ConText Pointer register (CTP) and the
Context Register (CNR) MMU registers.
The CTP is shifted to align it with
the physical address (36 bits) and we add the table index given on CNR.
CTP is right shifted 2 bits, cast to phys address and left shifted 6 bytes
to be aligned with the context register.
CNR is 2 bits left shifted for alignment with the context table.
›
definition compose_context_table_addr :: "machine_word ⇒machine_word
⇒ phys_address"
where
"compose_context_table_addr ctp cnr
≡ ((ucast (ctp >> 2)) << 6) + (ucast cnr << 2)"
subsection ‹Virtual Address Translation›
text‹Get the context table phys address from the MMU registers›
definition get_context_table_addr :: "MMU_state ⇒ phys_address"
where
"get_context_table_addr mmu
≡ compose_context_table_addr (getCTPVal mmu) (getCNRVal mmu)"
definition va_list_index :: "nat list" where
"va_list_index ≡ [va_t1_index,va_t2_index,va_t3_index,0]"
definition offset_index :: "nat list" where
"offset_index
≡ [ length_machine_word
, length_machine_word-length_t1
, length_machine_word-length_t1-length_t2
, length_machine_word-length_t1-length_t2-length_t3
]"
definition index_len_table :: "nat list" where "index_len_table ≡ [8,6,6,0]"
definition n_context_tables :: "nat" where "n_context_tables ≡ 3"
text ‹The following are basic physical memory read functions.
At this level we don't need the write memory yet.›
definition mem_context_val:: "asi_type ⇒ phys_address ⇒
mem_context ⇒ mem_val_type option"
where
"mem_context_val asi add m ≡
let asi8 = word_of_int 8;
r1 = m asi add
in
if r1 = None then
m asi8 add
else r1
"
context
includes bit_operations_syntax
begin
text ‹Given an ASI (word8), an address (word32) addr,
read the 32bit value from the memory addresses
starting from address addr' where addr' = addr
exception that the last two bits are 0's.
That is, read the data from
addr', addr'+1, addr'+2, addr'+3.›
definition mem_context_val_w32 :: "asi_type ⇒ phys_address ⇒
mem_context ⇒ word32 option"
where
"mem_context_val_w32 asi addr m ≡
let addr' = (AND) addr 0b111111111111111111111111111111111100;
addr0 = (OR) addr' 0b000000000000000000000000000000000000;
addr1 = (OR) addr' 0b000000000000000000000000000000000001;
addr2 = (OR) addr' 0b000000000000000000000000000000000010;
addr3 = (OR) addr' 0b000000000000000000000000000000000011;
r0 = mem_context_val asi addr0 m;
r1 = mem_context_val asi addr1 m;
r2 = mem_context_val asi addr2 m;
r3 = mem_context_val asi addr3 m
in
if r0 = None ∨ r1 = None ∨ r2 = None ∨ r3 = None then
None
else
let byte0 = case r0 of Some v ⇒ v;
byte1 = case r1 of Some v ⇒ v;
byte2 = case r2 of Some v ⇒ v;
byte3 = case r3 of Some v ⇒ v
in
Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24)
((ucast(byte1)) << 16))
((ucast(byte2)) << 8))
(ucast(byte3)))
"
text ‹
@{term "get_addr_from_table"} browses the page description tables
until it finds a PTE (bits==suc (suc 0).
If it is a PTE it aligns the 24 most significant bits of the entry
with the most significant bits of the phys address and or-ed with the offset,
which will vary depending on the entry level.
In the case we are looking at the last table level (level 3),
the offset is aligned to 0 otherwise it will be 2.
If the table entry is a PTD (bits== Suc 0),
the index is obtained from the virtual address depending on the current level and or-ed with the PTD.
›
function ptd_lookup:: "virtua_address ⇒ virtua_address ⇒
mem_context ⇒ nat ⇒ (phys_address × PTE_flags) option"
where "ptd_lookup va pt m lvl = (
if lvl > 3 then None
else
let thislvl_offset = (
if lvl = 1 then (ucast ((ucast (va >> 24))::word8))::word32
else if lvl = 2 then (ucast ((ucast (va >> 18))::word6))::word32
else (ucast ((ucast (va >> 12))::word6))::word32);
thislvl_addr = (OR) pt thislvl_offset;
thislvl_data = mem_context_val_w32 (word_of_int 9) (ucast thislvl_addr) m
in
case thislvl_data of
Some v ⇒ (
let et_val = (AND) v 0b00000000000000000000000000000011 in
if et_val = 0 then
None
else if et_val = 1 then
let ptp = (AND) v 0b11111111111111111111111111111100 in
ptd_lookup va ptp m (lvl+1)
else if et_val = 2 then
let ppn = (ucast (v >> 8))::word24;
va_offset = (ucast ((ucast va)::word12))::word36
in
Some (((OR) (((ucast ppn)::word36) << 12) va_offset),
((ucast v)::word8))
else
None
)
|None ⇒ None)
"
by pat_completeness auto
termination
by (relation "measure (λ (va, (pt, (m, lvl))). 4 - lvl)") auto
definition get_acc_flag:: "PTE_flags ⇒ word3" where
"get_acc_flag w8 ≡ (ucast (w8 >> 2))::word3"
definition mmu_readable:: "word3 ⇒ asi_type ⇒ bool" where
"mmu_readable f asi ≡
if uint asi ∈ {8, 10} then
if uint f ∈ {0,1,2,3,5} then True
else False
else if uint asi ∈ {9, 11} then
if uint f ∈ {0,1,2,3,5,6,7} then True
else False
else False
"
definition mmu_writable:: "word3 ⇒ asi_type ⇒ bool" where
"mmu_writable f asi ≡
if uint asi ∈ {8, 10} then
if uint f ∈ {1,3} then True
else False
else if uint asi ∈ {9, 11} then
if uint f ∈ {1,3,5,7} then True
else False
else False
"
definition virt_to_phys :: "virtua_address ⇒ MMU_state ⇒ mem_context ⇒
(phys_address × PTE_flags) option"
where
"virt_to_phys va mmu m ≡
let ctp_val = mmu_reg_val mmu (0x100);
cnr_val = mmu_reg_val mmu (0x200);
mmu_cr_val = (registers mmu) CR
in
if (AND) mmu_cr_val 1 ≠ 0 then
case (ctp_val,cnr_val) of
(Some v1, Some v2) ⇒
let context_table_entry = (OR) ((v1 >> 11) << 11)
(((AND) v2 0b00000000000000000000000111111111) << 2);
context_table_data = mem_context_val_w32 (word_of_int 9)
(ucast context_table_entry) m
in (
case context_table_data of
Some lvl1_page_table ⇒
ptd_lookup va lvl1_page_table m 1
|None ⇒ None)
|_ ⇒ None
else Some ((ucast va), ((0b11101111)::word8))
"
text ‹
\newpage
The below function gives the initial values of MMU registers.
In particular, the MMU context register CR is 0 because:
We don't know the bits for IMPL, VER, and SC;
the bits for PSO are 0s because we use TSO;
the reserved bits are 0s;
we assume NF bits are 0s;
and most importantly, the E bit is 0 because when the machine
starts up, MMU is disabled.
An initial boot procedure (bootloader or something like that) should
configure the MMU and then enable it if the OS uses MMU.›
definition MMU_registers_init :: "MMU_context"
where "MMU_registers_init r ≡ 0"
definition mmu_setup :: "MMU_state"
where "mmu_setup ≡ ⦇registers=MMU_registers_init⦈"
end
end