Jones optimality and hardware virtualization: a report on work in progress

ABSTRACT

The growing popularity of hardware virtualization (VMware and Xen being two prominent implementations) leads us to examine the common ground between this yet-again vibrant technology and partial evaluation. A virtual machine executes on host hardware and presents to its guest program a replica of that host environment, complete with CPU, memory, and I/O devices. A virtual machine can be seen as a self-interpreter.

A program specializer is considered Jones-optimal if it is capable of removing a layer of interpretational overhead. We propose a formulation of Jones optimality which coincides with a well-known virtualization efficiency criterion.

A fully abstract programming language translation (an idea put forward by Abadi) is one that preserves program equivalences. We may translate a program by specializing a self-interpreter with respect to it. We argue that full abstraction for such translations captures the notion of transparency (whether or not a program can determine if it is running on a virtual machine) in virtual machine folklore.

We hope that this discussion will encourage wider exchange of ideas between the virtualization and partial evaluation communities.

REFERENCES

• 1: VMware Website. http://www.vmware.com/.
• 2: Martín Abadi, Protection in Programming-Language Translations, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.868-883, July 13-17, 1998
• 3: Keith Adams , Ole Agesen, A comparison of software and hardware techniques for x86 virtualization, Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, October 21-25, 2006, San Jose, California, USA
• 4: Andrew W. Appel, Foundational Proof-Carrying Code, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.247, June 16-19, 2001
• 5: Paul Barham , Boris Dragovic , Keir Fraser , Steven Hand , Tim Harris , Alex Ho , Rolf Neugebauer , Ian Pratt , Andrew Warfield, Xen and the art of virtualization, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 6: Bryan M. Cantrill , Michael W. Shapiro , Adam H. Leventhal, Dynamic instrumentation of production systems, Proceedings of the annual conference on USENIX Annual Technical Conference, p.2-2, June 27-July 02, 2004, Boston, MA
• 7: Olivier Danvy and Pablo E. Martínez López. Tagging, encoding, and Jones optimality. In Proceedings of ESOP, volume 2618 of LNCS, pages 335- 347, 2003.
• 8: Johan Gade and Robert Glück. On Jones-optimal specializers: A case study using Unmix. In Proceedings of APLAS, volume 4279 of LNCS, pages 406--422, 2006.
• 9: Tal Garfinkel , Keith Adams , Andrew Warfield , Jason Franklin, Compatibility is not transparency: VMM detection myths and realities, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
• 10: Robert Glück. The translation power of the Futamura projections. In Perspectives of Systems Informatics, volume 2890 of LNCS, pages 133--147, 2003.
• 11: N. D. Jones, Challenging problems in partial evaluation and mixed computation, New Generation Computing, v.6 n.2-3, p.291-302, March-April 1988 [doi>10.1007/BF03037143]
• 12: Neil D. Jones, Transformation by interpreter specialisation, Science of Computer Programming, v.52 n.1-3, p.307-339, August 2004 [doi>10.1016/j.scico.2004.03.010]
• 13: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 14: Andrew Kennedy, Securing the .NET programming model, Theoretical Computer Science, v.364 n.3, p.311-317, 8 November 2006 [doi>10.1016/j.tcs.2006.08.014]
• 15: Henning Makholm, On Jones-Optimal Specialization for Strongly Typed Languages, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.129-148, September 20, 2000
• 16: John C. Mitchell, On abstraction and the expressive power of programming languages, Science of Computer Programming, v.21 n.2, p.141-163, Oct. 1993
• 17: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 18: Gil Neiger, Amy Santoni, Felix Leung, Dion Rodgers, and Rich Uhlig. Intel Virtualization Technology: Hardware support for efficient processor virtualization. Intel Technology Journal, 10(3):167--177, 2006. http://dx.doi.org/10.1535/itj.1003.01.
• 19: Nicholas Nethercote , Julian Seward, Valgrind: a framework for heavyweight dynamic binary instrumentation, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 20: Gerald J. Popek , Robert P. Goldberg, Formal requirements for virtualizable third generation architectures, Communications of the ACM, v.17 n.7, p.412-421, July 1974 [doi>10.1145/361011.361073]
• 21: John C. Reynolds, Definitional Interpreters for Higher-Order Programming Languages, Higher-Order and Symbolic Computation, v.11 n.4, p.363-397, December 1998 [doi>10.1023/A:1010027404223]
• 22: John Scott Robin , Cynthia E. Irvine, Analysis of the Intel Pentium's ability to support a secure virtual machine monitor, Proceedings of the 9th conference on USENIX Security Symposium, p.10-10, August 14-17, 2000, Denver, Colorado
• 23: Jeffrey Mark Siskind , Barak A. Pearlmutter, First-class nonstandard interpretations by opening closures, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 24: Jim Smith , Ravi Nair, Virtual Machines: Versatile Platforms for Systems and Processes (The Morgan Kaufmann Series in Computer Architecture and Design), Morgan Kaufmann Publishers Inc., San Francisco, CA, 2005
• 25: Ken Thompson, Reflections on trusting trust, Communications of the ACM, v.27 n.8, p.761-763, Aug 1984 [doi>10.1145/358198.358210]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Interpreters
  D.4 OPERATING SYSTEMS
      D.4.8 Performance
          Subjects: Modeling and prediction

General Terms:
Languages, Performance

Keywords:
Jones optimality, full abstraction, virtual machines, virtualization