Library Pip.Model.MMU


Summary

Memory Management Unit : the specification of the translation of virtual memory addresses to physical addresses

Require Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.Lib Pip.Model.MALInternal.
Require Import Arith Bool NPeano List.
The 'comparePageToNull' returns true if the given page is equal to the fixed default page (null)
Definition comparePageToNull (p :page) : LLI bool :=
  perform nullPaddr := getDefaultPage in
  MALInternal.Page.eqb nullPaddr p.
The 'getIndexOfAddr' function returns the index of va that corresponds to l
Definition getIndexOfAddr (va : vaddr) (l : level) : LLI index:=
  ret ( nth ((length va) - (l + 2)) va defaultIndex ).

Definition readPhyEntry (paddr : page) (idx : index) : LLI page :=
  perform s := get in
  let entry := lookup paddr idx s.(memory) beqPage beqIndex in
  match entry with
  | Some (PE a) ⇒ ret a.(pa)
  | Some _ ⇒ undefined 9
  | None ⇒ undefined 8
  end.

Definition readPresent (paddr : page) (idx : index) : LLI bool:=
perform s := get in
let entry := lookup paddr idx s.(memory) beqPage beqIndex in
match entry with
  | Some (PE a) ⇒ ret a.(present)
  | Some _ ⇒ undefined 18
  | None ⇒ undefined 17
end.

Definition readAccessible (paddr : page) (idx : index) : LLI bool:=
perform s := get in
let entry := lookup paddr idx s.(memory) beqPage beqIndex in
match entry with
  | Some (PE a) ⇒ ret a.(user)
  | Some _ ⇒ undefined 12
  | None ⇒ undefined 11
end.

The 'getTableAddrAux' returns the reference to the last page table
Fixpoint translateAux timeout (pd : page) (va : vaddr) (l : level) :=
  match timeout with
  | 0 ⇒ getDefaultPage
  |S timeout1 ⇒
  perform isFstLevel := MALInternal.Level.eqb l fstLevel in
    if isFstLevel
    then ret pd
    else
      perform idx := getIndexOfAddr va l in
      perform addr := readPhyEntry pd idx in
      perform isNull := comparePageToNull addr in
      if isNull then getDefaultPage else
      perform p := MALInternal.Level.pred l in
      translateAux timeout1 addr va p
  end .

The 'translate'
Definition translate (pd : page) (va : vaddr) (l : level) : LLI (option page) :=
  perform lastTable := translateAux nbLevel pd va l in
  perform isNull := comparePageToNull lastTable in
  if isNull then ret None else
  perform idx := getIndexOfAddr va fstLevel in
  perform ispresent := readPresent lastTable idx in
  perform isaccessible := readAccessible lastTable idx in
  if (ispresent && isaccessible) then
  perform phypage := readPhyEntry lastTable idx in
  ret (Some phypage)
  else ret None.