Open Kernel Labs, NICTA and UNSW Present at the 2007 HotOS XI Conference on May 7th and 9th

May 03, 2007

MEDIA ALERT Who: Open Kernel Labs and Researchers from National ICT Australia (NICTA) and the University of New South Wales Present at the 2007 HotOS XI Conference What: “Hype and Virtue” “Towards a Practical, Verified Kernel” Where: 2007 HotOS XI Conference Location: Catamaran Resort Hotel, San Diego, CA When: May 7th and 9th, 2007 Information: http://www.usenix.org/events/hotos07/index.html

About the Presentation

Open Kernel Labs (www.ok-labs.com), NICTA (www.nicta.com.au) and Researchers from the University of New South Wales are co-presenting papers at the upcoming HotOS XI Conference in San Diego, CA. The authors believe the presentations will be provocative and informative, the first asking the question ’Have hypervisors acted as a disruptive force or has the focus on this technology slowed the design of kernel research?” The second paper will discuss the issue of designing, specifying, implementing and formally verifying a small operating system by providing a productive and iterative development methodology for both operating system developers and formal methods practitioners.  Here’s a brief description of the content of the papers: “Hype and Virtue” (Monday, May 7 at 2 pm) This paper is being presented by Professor Timothy Roscoe of ETH Zurich and is co-authored by Dr. Kevin Elphinstone of National ICT Australia (NICTA) and Dr. Gernot Heiser, Program Leader at NICTA and Co-Founder and CTO of OK and Professor of Operating Systems at the University of New South Wales. It is currently available on the NICTA website. (http://www.ertos.nicta.com.au/publications/home.pml).  The paper will question whether hypervisors are really acting as a disruptive force in OS research and argue that, to date, they have changed very little at a technical level. With virtualization, OS researchers have retained the conventional Unix-like OS interface and added a new API based on PC hardware that is highly unsuitable for most purposes. Despite commercial excitement, focus on hypervisor design may be leading OS research astray. However, adopting a different approach to virtualization and recognizing its value to research holds the prospect of opening up kernel research to new directions. “Towards a Practical, Verified Kernel” (Wednesday, May 9th at 11:00 am) This paper, which will be presented by Dr. Kevin Elphinstone is co-authored by Gerwin Klein of NICTA and University of New South Wales; Philip Derrin of NICTA; Professor Timothy Roscoe of Zürich, and Dr. Gernot Heiser, Program Leader at NICTA, Co-Founder and CTO of OK and Professor of Operating Systems at the University of New South Wales. It is currently available on the NICTA website. (http://www.ertos.nicta.com.au/publications/home.pml).  This paper will examine one of the issues in designing, specifying, implementing and formally verifying a small operating system kernel — how to provide a productive and iterative development methodology for both operating system developers and formal methods practitioners. It espouses the use of functional programming languages as a medium for prototyping that is readily amenable to formalization with a low barrier to entry for kernel developers. It will also report early experience in the process of designing and building sel4: a new, practical, and formally verified microkernel .

About HotOS XI

Continuing the HotOS tradition, the 11th Workshop on Hot Topics in Operating Systems will be a place to present and discuss new ideas about computer systems and how technological advances and new applications are shaping our computational infrastructure. The conference is sponsored by the USENIX organization in collaboration with the IEEE Technical Committee on Operating Systems. The event is invitation only. For more information about the conference visit: http://www.usenix.org/event/hotos07/tech/ Press Contacts:  Pat Arcand (US) Arcand & Madison for Open Kernel Labs (617-576-7777) pat@am-pr.com

« View All Press Releases