Workshop Program

We present the design and initial evaluation of a resilient operating system architecture that leverages HW architectures combining few resilient with many non-resilient CPU cores. To this end, we build our system around a Reliable Computing Base (RCB) consisting of those software components that must work for reliable operation, and run the RCB on the resilient cores. The remainder of the system runs replicated on unreliable cores. Our system’s RCB consists of an L4 microkernel, a runtime environment and a replication manager. In this paper we state and justify assumptions about the hardware architecture, motivate the corresponding software architecture and evaluate communication mechanisms between the RCB and the replicas.

The Linux kernel can be a threat to the dependability of systems because of its sheer size. A simple approach to produce smaller kernels is to manually configure the Linux kernel. However, the more than 11; 000 configuration options available in recent Linux versions render this a demanding task. We report on designing and implementing the first automated generation of a workload-tailored kernel configuration and discuss the security gains such an approach offers in terms of reduction of the Trusted Computing Base (TCB) size. Our results show that the approach prevents the inclusion of 10% of functions known to be vulnerable in the past.

Modern concurrent software is riddled with data races and these races constitute the source of many problems. Data races are hard to detect accurately before software is shipped and, once they cause failures in production, developers find it challenging to reproduce and debug them. 

Ideally, all data races should be known before software ships. Static data race detectors are fast, have few false negatives, but unfortunately have many false positives. Conversely, dynamic data race detectors do not have false positives, but have many false negatives and incur high runtime overhead. There is no silver bullet and, as a result, modern software still ships with numerous data races.

We present CoRD, a collaborative distributed testing framework that aims to combine the best of the two approaches: CoRD first statically detects races and then dynamically validates them via crowdsourced executions of the program. Our initial results show that CoRD is more effective than static or dynamic detectors alone, and it introduces negligible runtime overhead.

We aim to detect and diagnose code misbehavior that wastes energy, which we call energy bugs. This paper describes a method and implementation, called Carat, for performing such diagnosis on mobile devices. Carat takes a collaborative, black-box approach. A non-invasive client app sends intermittent, coarse-grained measurements to a server, which identifies correlations between higher expected energy use and client properties like the running apps, device model, and operating system. Carat successfully detected all energy bugs in a controlled experiment and, during a deployment to 883 users, identified 5434 instances of apps exhibiting buggy behavior in the wild.

On August 5 at 10:18 p.m. PDT, a large rover named Curiosity made a soft landing on the surface of Mars. Given the one-way light-time to Mars, the controllers on Earth learned about the successful touchdown 14 minutes later, at 10:32 p.m. PDT. As can be expected, all functions on the rover, and on the spacecraft that brought it to Mars, are controlled by software. In this talk we review the process that was followed to secure the reliability of this code.
Gerard Holzmann is a senior research scientist and a fellow at NASA's Jet Propulsion Laboratory, the lab responsible for the design of the Mars Science Laboratory Mission to Mars and its Curiosity Rover. He is best known for designing the Logic Model Checker Spin, a broadly used tool for the logic verification of multi-threaded software systems. Holzmann is a fellow of the ACM and a member of the National Academy of Engineering.

This paper describes ShadowDB, a replicated version of the BerkeleyDB database. ShadowDB is a primary-backup based replication protocol where failure handling, the critical part of the protocol, is taken care of by a synthesized consensus service that is correct by construction. The service has been proven correct semi-automatically by the Nuprl proof assistant. We describe the design and process to prove the consensus protocol correct and present the database replication protocol. The performance of ShadowDB is good in the normal case and recovering from a failure only takes seconds. Our approach offers simplified means to diversify the code in a way that preserves correctness.

An attractive approach to leveraging the ability of cloudcomputing platforms to provide resources on demand is to build elastic applications, which can scale up or down based on resource requirements. To ease the development of elastic applications, it is useful for programmers to write applications with simple, inelastic semantics and rely on runtime systems to provide elasticity. While this approach has been useful in restricted domains, such as MapReduce, we argue in this paper that adding elasticity to general distributed applications introduces new fault-tolerance challenges that must be addressed at the programming model and run-time level. We discuss a programming model for writing elastic, distributed applications, and describe an approach to fault-tolerance that integrates with the elastic run-time to provide transparent elasticity and fault-tolerance.