|
Workshop Program
Time |
Topic |
Presentation |
8:30–10:00 |
Session 1: Welcome and Keynote |
|
|
Welcome and Introductions
The PLOS 2011 Organizing Committee
|
|
|
Keynote Address: “The Role of Language Technology in
Trustworthy Operating Systems”
Gernot Heiser, University of New South Wales and NICTA
Recently, programming-language technology has generated strong interest
among the designers of operating systems that are to be highly
dependable. Several projects are using type-safe/managed language for
the implementation of OS kernels. The reader of the literature could
be forgiven to think that a memory-safe implementation is a
trustworthy implementation.
We argue that this is misleading, and trustworthiness requires much
more: specifically, functional correctness. The use of type-safe
languages alone does not achieve this, and, given the complexity of the
runtime system of such languages, may actually make it harder to
achieve. We therefore argue that different levels of the software
stack call for different PL technologies: simplicity (i.e.,
C + assembler) is king for building a trustworthy bottom
layer, which can then be leveraged to provide a truly trustworthy
runtime for managed languages, which in turn should be used to
implement higher layers of system software.
Gernot Heiser is Scientia Professor and John Lions Chair of
Operating Systems at the University of New South Wales (UNSW), and
leads the Software Systems Research Group at NICTA, Australia's
National Centre of Excellence for ICT Research. He joined NICTA at its
creation in 2002, and before that he was a full-time member of academic
staff at UNSW from 1991. His past work included the Mungi
single-address-space operating system (OS), several unbroken
records in IPC performance, and the best-ever reported performance for
user-level device drivers.
In 2006, Gernot with a number of his students founded Open Kernel
Labs, now the market leader in secure operating-systems and
virtualization technology for mobile wireless devices. The company's
OKL4 operating system, a descendant of L4 kernels developed by his
group at UNSW and NICTA, is deployed in more than 1.5 billion mobile
devices. This includes the Motorola Evoke, the first (and to date
only) mobile phone running a high-level OS (Linux) and a modem stack on
the same processor core.
|
|
10:00–10:30 |
Break |
|
10:30–12:00 |
Session 2a: Static Analyses |
Presentation |
|
Finding
Resource-Release Omission Faults in Linux
Suman Saha
(LIP6-Regal),
Julia Lawall
(DIKU, University of Copenhagen),
and
Gilles Muller
(INRIA/LIP6-Regal)
|
|
|
Configuration
Coverage in the Analysis of Large-Scale System Software
Reinhard Tartler,
Daniel Lohmann,
Christian Dietrich,
Christoph Egger,
and
Julio Sincero
(Friedrich-Alexander University)
|
|
|
Session 2b: Security |
|
|
Rounding
Pointers — Type Safe Capabilities with C++ Meta
Programming
Alexander Warg
and
Adam Lackorzynski
(Technische Universität Dresden)
|
|
|
Preliminary
Design of the SAFE Platform
André DeHon,
Ben Karel
(University of Pennsylvania),
Thomas F. Knight, Jr.
(BAE Systems),
Gregory Malecha
(Harvard University),
Benoît Montagu
(University of Pennsylvania),
Robin Morisset
(École Normale Supérieure Paris),
Greg Morrisett
(Harvard University),
Benjamin C. Pierce
(University of Pennsylvania),
Randy Pollack
(Harvard University),
Sumit Ray
(BAE Systems),
Olin Shivers
(Northeastern University),
Jonathan M. Smith
(University of Pennsylvania),
and
Gregory Sullivan
(BAE Systems)
|
|
12:00–1:30 |
Lunch |
1:30–3:00 |
Session 3a: Dynamic Safety and Performance |
Presentation |
|
Dynamic
Deadlock Avoidance in Systems Code Using Statically Inferred
Effects
Prodromos Gerakios,
Nikolaos Papaspyrou
(National Technical University of Athens),
Konstantinos Sagonas
(National Technical University of Athens and
Uppsala University),
and
Panagiotis Vekris
(National Technical University of Athens)
|
|
|
Using
Declarative Invariants for Protecting File-System
Integrity
Jack Sun,
Daniel Fryer,
Ashvin Goel,
and
Angela Demke Brown
(University of Toronto)
|
|
|
Assessing
the Scalability of Garbage Collectors on Many Cores
Lokesh Gidra,
Gaël Thomas,
Julien Sopena,
and
Marc Shapiro
(Regal-LIP6/INRIA)
|
|
|
Session 3b: Reversible Debugging |
|
|
URDB:
A Universal Reversible Debugger Based on Decomposing Debugging
Histories
Ana-Maria Visan,
Kapil Arya,
Gene Cooperman,
and
Tyler Denniston
(Northeastern University)
|
|
3:00–3:30 |
Break |
|
3:30–5:00 |
Session 4a: Demonstrations and Working Groups |
|
|
Demonstrations
Workshop attendees participate in demonstrations of the languages and
systems presented in earlier sessions. (Approximately 45 minutes.)
|
|
|
Working Groups
Workshop attendees participate in semi-structured discussion groups on
PLOS topics, according to their interests. The workshop organizers will
use the accepted papers and input from participants to compile a list of
topics for working groups.
|
|
5:00–6:30 |
Session 4b: Working Groups and Wrap Up |
|
|
Each working group concludes by preparing and presenting an
“outbrief” that summarizes its discussion: achievements,
positions, opinions, common themes, open issues, closed issues, solved
problems, challenge problems, ideas for future activities and
collaborations, …
|
|
6:30–9:30 |
SOSP 2011 Buffet Reception |
|
|