Bigmem-asymmetric
A 2^64-byte memory model that is logically a record but
provides array-like performance for a fixed amount of emulated memory
and slow(er) performance for the remaining (higher) memory locations.
The bigmem library implements the idea in the
following paper using nested and abstract STOBJs, which leads to a simpler
implementation of a large memory. This bigmem-asymmetric library
provides faster access/update performance for some amount of low-address
memory, and slow (alist-style) performance for high-address memory
locations. For spiritual discussion of this kind of memory modeling, please
see the reference below.
Warren A. Hunt, Jr. and Matt Kaufmann. A Formal Model of a Large
Memory that Supports Efficient Execution. In Proceedings of the 12th
International Conference on Formal Methods in Computer-Aided Design (FMCAD
2012, Cambrige, UK, October 22-25), 2012
These books define an abstract STOBJ called mem that exports an
accessor function read-mem and an updater function write-mem.
mem is logically a typed record that models 2^64 bytes. The
corresponding concrete STOBJ for mem is bm, which is a STOBJ
containing STOBJs that provides an array for the first part (0...) of
the natural-number-addressed memory and for essentially allocates chunks of
bytes on demand; see bigmem-concrete-asymmetric for implementation
details.
An obvious application of bigmem-asymmetric is to model memory;
mem can be used as a child STOBJ to define a field representing the
memory (up to 2^64 bytes) in a parent STOBJ that models some machine's
state. See projects/x86isa/machine/state.lisp for one such example.
Subtopics
- Bigmem-concrete-asymmetric
- A byte memory model that is logically a record but provides
array-like performance for a (low-address) region of memory and association
list lookup and update for memory modeled above a certain address limit.
- Get-mem-aux
- Get-mem
- Get the entire contents of the memory in the form of a linear list
- Xor-mem-region
- Ordered-bytes
- Alists with ordered keys.
