bits 64
    
    db 0xf3, 0x0f, 0x01, 0xfe   ; rmpadjust
    db 0xf2, 0x0f, 0x01, 0xfe   ; rmpupdate
    db 0xf3, 0x0f, 0x01, 0xff   ; psmash
    db 0xf2, 0x0f, 0x01, 0xff   ; pvalidate
    db 0xf3, 0x0f, 0x01, 0xfd   ; rmpquery
    db 0xf2, 0x0f, 0x01, 0xfd   ; rmpread