|
|
|---|
|
|
|
|---|
How to change physical memory models
We use the bigmems::bigmems library to model the memory. The default model is bigmem::bigmem. This model is "attachable," which allows one to replace it in execution with a logically equivalent stobj. Here's why you'd want to replace it:
bigmem::bigmem provides constant access time for the entire address space. However, accessing a byte requires walking a 3 level hierarchy.
bigmem-asymmetric::bigmem-asymmetric provides faster access to the lower 6GB of physical memory, because those values are stored in an array, but slower access to the rest of the address space, since it stores the rest of the values in in an ordered alist.
If you're only going to be using the lower 6GB of memory (or mostly using the lower 6 GB) of memory, using the bigmem-asymmetric::bigmem-asymmetric makes sense, otherwise use bigmem::bigmem
By default, the model uses bigmem::bigmem. To switch to bigmem-asymmetric::bigmem-asymmetric, submit the following events to ACL2 before including the x86 books:
(include-book "centaur/bigmems/bigmem-asymmetric/bigmem-asymmetric" :dir :system) (include-book "centaur/bigmems/bigmem/portcullis" :dir :system) (attach-stobj bigmem::mem bigmem-asymmetric::mem)