Virtual machines become popular tools for providing features like security, server consolidation, fault tolerance, and availability. One of the trickiest parts of efficiently virtualizing a PC is virtualizing the x86/x64 TLB, particularly when sharing shadow page tables between concurrently executing processors.
We describe a simple x86-like TLB model and a sequence of increasingly sophisticated virtualization algorithms. For each algorithm, we propose a simulation relation wrt. the model, and use this relation to either justify the algorithm or identify where it breaks down. One of the lessons of this exercise is that engineers can enjoy benefits from the use of formal programming methodology without having to use mathematics.
| Ernie Cohen |
| Microsoft |
| Date: | Mon Feb 6 2006 |
| Time: | 2 to 3pm |
| Location: | Level 1 Seminar Room, UNSW L5 Building, NICTA Kensington Lab |
| Convened by: | Gerwin Klein |
Last updated by tbourke at Mon Apr 3 14:49:00 2006 GMT+1000