3 ;; This file is part of the Palacios Virtual Machine Monitor developed
4 ;; by the V3VEE Project with funding from the United States National
5 ;; Science Foundation and the Department of Energy.
7 ;; The V3VEE Project is a joint project between Northwestern University
8 ;; and the University of New Mexico. You can find out more at
9 ;; http://www.v3vee.org
11 ;; Copyright (c) 2008, Jack Lange <jarusl@cs.northwestern.edu>
12 ;; Copyright (c) 2008, The V3VEE Project <http://www.v3vee.org>
13 ;; All rights reserved.
15 ;; Author: Jack Lange <jarusl@cs.northwestern.edu>
17 ;; This is free software. You are permitted to use,
18 ;; redistribute, and modify it as specified in the file "V3VEE_LICENSE"
24 %include "vmm_symbol.asm"
98 ; cpuid_edx - return the edx register from cpuid
120 ; cpuid_ecx - return the ecx register from cpuid
141 ; cpuid_eax - return the eax register from cpuid
161 ; Set_MSR - Set the value of a given MSR
179 ; Get_MSR - Get the value of a given MSR
180 ; void Get_MSR(int MSR, void * high_byte, void * low_byte);