• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
        • Tlb-key
          • !tlb-key->implicit-supervisor-access
          • Tlb-key-fast
          • Tlb-key-p
          • !tlb-key->r-w-x
          • !tlb-key->vpn
          • !tlb-key->smep
          • !tlb-key->smap
          • !tlb-key->cpl
          • !tlb-key->nxe
          • Tlb-key->implicit-supervisor-access
          • !tlb-key->wp
          • !tlb-key->ac
          • Tlb-key->vpn
          • Tlb-key->smep
          • Tlb-key->smap
          • Tlb-key->r-w-x
          • Tlb-key->cpl
          • Tlb-key-fix
          • Tlb-key->wp
          • Tlb-key->nxe
          • Tlb-key->ac
          • Good-tlb-key-p
        • Tlbp
        • Tlb-entryp
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Tlb-key

Tlb-key-fast

A faster constructor for tlb-keys.

Signature

(tlb-key-fast wp smep 
              smap ac nxe implicit-supervisor-access 
              r-w-x cpl vpn) 
 
  → 
*

The defbitstruct book creates a tlb-key function and make-tlb-key macro to construct TLB keys, but it is very slow because it uses logapp, which can't be inlined, and doesn't put in all the type declarations.

This version is faster because it uses a macro which expands to a composition of logior, ash, logand, and 1- instead of logapp (declaring it as an inlineable function instead of a macro wouldn't get inlined by CCL) and puts in the correct type declarations. Using this functions instead of tlb-key provided a ~20% speed up in model execution. We also declare a make-tlb-key-fast macro which is just like make-tlb-key but uses tlb-key-fast under the hood to construct the tlb-key.

We use mbe and leave this enabled so it rewrites to tlb-key. This allows us to reason about that function instead while getting the execution performance of this implementation.

Definitions and Theorems

Function: tlb-key-fast

(defun tlb-key-fast (wp smep
                        smap ac nxe implicit-supervisor-access
                        r-w-x cpl vpn)
 (declare (type (unsigned-byte 1) wp)
          (type (unsigned-byte 1) smep)
          (type (unsigned-byte 1) smap)
          (type (unsigned-byte 1) ac)
          (type (unsigned-byte 1) nxe)
          (type (unsigned-byte 1)
                implicit-supervisor-access)
          (type (unsigned-byte 2) r-w-x)
          (type (unsigned-byte 2) cpl)
          (type (unsigned-byte 36) vpn))
 (let ((__function__ 'tlb-key-fast))
  (declare (ignorable __function__))
  (mbe
   :logic (tlb-key wp smep
                   smap ac nxe implicit-supervisor-access
                   r-w-x cpl vpn)
   :exec
   (the
    (unsigned-byte 46)
    (logapp-inline
     1 wp
     (the
      (unsigned-byte 45)
      (logapp-inline
       1 smep
       (the
        (unsigned-byte 44)
        (logapp-inline
         1 smap
         (the
          (unsigned-byte 43)
          (logapp-inline
           1 ac
           (the
            (unsigned-byte 42)
            (logapp-inline
             1 nxe
             (the
              (unsigned-byte 41)
              (logapp-inline
               1 implicit-supervisor-access
               (the
                (unsigned-byte 40)
                (logapp-inline
                    2 r-w-x
                    (the (unsigned-byte 38)
                         (logapp-inline 2 cpl
                                        (the (unsigned-byte 36)
                                             vpn))))))))))))))))))))