The physical memory models we support and when to use which
We support the bigmem::bigmem and bigmem-asymmetric::bigmem-asymmetric memory models for physical memory. Both of these are equivalent in reasoning, so for proofs it doesn't matter which you use. However, in execution, they have different performance characteristics.
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, edit
; The orginal three-level memory model. +; (include-book "centaur/bigmem/bigmem" :dir :system) -(include-book "centaur/bigmem/bigmem" :dir :system) ; Asymmetric memory model; faster for "small" addresses, and otherwise slower. +(include-book "centaur/bigmem-asymmetric/bigmem-asymmetric" :dir :system) -; (include-book "centaur/bigmem-asymmetric/bigmem-asymmetric" :dir :system) ... (mem :type (array (unsigned-byte 8) (,*mem-size-in-bytes*)) ;; 2^52 :initially 0 :fix (acl2::loghead 8 (ifix x)) + :child-stobj bigmem-asymmetric::mem + :child-accessor bigmem-asymmetric::read-mem + :child-updater bigmem-asymmetric::write-mem - :child-stobj bigmem::mem - :child-accessor bigmem::read-mem - :child-updater bigmem::write-mem :accessor memi :updater !memi)