|
|
|---|
|
|
|
|---|
A short history of the definition of the x86 state
Before bigmems::bigmems and rstobj2::defrstobj were used to
define the x86 state, the x86 state's definition was rather tedious. (For
future reference, the following git revision has that old definition:
This current file
The old x86isa memory model was based on the FMCAD'2012 paper "A
Formal Model of a Large Memory that Supports Efficient Execution".
The following comment from the old file
....
;; For our ACL2 model, we define a paging-like mechanism to
;; model the complete x86 52-bit address space. The memory is
;; laid out in a flat array, to be viewed as back-to-back
;; "pseudo-pages" each of size 2^27 bytes (128MB). The address
;; of a byte is split into two pieces: a 25-bit pseudo-page
;; address and a 27-bit offset within a page. The mem-table
;; data structure is of size *mem-table-size* = 2^25 -- thus,
;; indices are 25 bits -- and it maps these indices to 25-bit
;; pseudo-page addresses. However, the mem-table values are
;; actually 26-bit values: the least significant bit is
;; initially 1, but is 0 when the entry is valid, in which case
;; the most significant 25 bits represent a pseudo-page address.
;; The offset of a byte address is a 27-bit wide address, which
;; when added to (ash pseudo-page-address 27), gives the "real"
;; address of a byte stored in mem-array. Mem-array-next-addr
;; keeps track of the 25-bit index of the pseudo-page to be
;; allocated next.
;; Here is an example of how this works. Suppose we have the
;; following, where again, the least significant bit of 0
;; indicates a valid entry, and where {i, 1'bx} denotes
;; concatenation of the bit-vector i with the single bit x.
;; mem-table[#x0654321] = {0, 1'b0}
;; mem-table[#x16789ab] = {1, 1'b0}
;; mem-table[#x0111111] = {2, 1'b0}
;; All additional values in mem-table are the initial value of
;; 1, which means "page is not present".
;; Then mem-array starts as follows.
;; 2^27 bytes corresponding to byte addresses with top 25 bits = #x0654321
;; 2^27 bytes corresponding to byte addresses with top 25 bits = #x16789ab
;; 2^27 bytes corresponding to byte addresses with top 25 bits = #x0111111
(mem-table :type (array (unsigned-byte #.*mem-table-size-bits+1*)
;; *mem-table-size-bits* of pseudo-page
;; address, followed by 1 extra bit
;; (LSB) to indicate the
;; absence/presence of pseudo-pages
(#.*mem-table-size*))
:initially 1
:resizable nil)
(mem-array :type (array (unsigned-byte 8)
(#.*initial-mem-array-length*))
:initially 0
:resizable t)
(mem-array-next-addr :type (integer 0 #.*mem-table-size*)
:initially 0)
...
The proof of correctness of this memory model was pretty
involved (see the old file
All of this was finished before nested stobjs were supported in ACL2, so there was not much incentive to simplify the memory model or the state definition.
We used a neat trick for all the accessors and updaters of
the
Signature: (RGFI* index x86)
We also defined a universal accessor function
Signature: (XR fld-name index x86)
We then defined another function,
(RGFI index x86) :=
(mbe :logic (XR :RGF index x86)
:exec (RGFI* index x86))
We then used
The consequence of this was that whenever an