As cloud computing and big data gain prominence in today's economic landscape, the challenge of effectively articulating complex algorithms in distributed environments becomes ever more important. In this paper we describe MBrace; a novel programming model/framework for performing large scale computation in the cloud. Based on the .NET software stack, it utilizes the power of the F# programming language. MBrace introduces a declarative style for specifying and composing parallelism patterns, in what is known as cloud workflows or a cloud monad. MBrace is also a distributed execution runtime that handles orchestration of cloud workflows in the data centre.
Today file system tools and file-system aware storage applications are tightly coupled with file system implementations. Developing these applications is challenging because it requires detailed knowledge of the file system format, and the code for interpreting file system metadata has to be written manually. This code is complex and file-system specific, and so the application requires significant re-engineering to support different file systems. We propose a file system annotation language for specifying a file system's on-disk metadata format. File system developers are asked to annotate the data structure definitions of a file system's metadata. The annotated code is parsed and used by tool-specific code templates to create interpretation routines (e.g., a metadata parser) for the desired file system tool. The benefit is that different tools can reuse the interpretation routines, and they are much less dependent on file system formats and implementations. We show the feasibility of this approach by implementing a compiler that generates a runtime metadata interpreter for an annotated toy file system. The generated code has low overhead (roughly 3%) compared to a hand-written version of the same application.
Building server software in a large-scale setting, where systems exhibit a high degree of concurrency and environmental variability, is a challenging task to even the most experienced programmer. Efficiency, safety, and robustness are paramount-goals which have traditionally conflicted with modularity, reusability, and flexibility. We describe three abstractions which combine to present a powerful programming model for building safe, modular, and efficient server software: Composable futures are used to relate concurrent, asynchronous actions; services and filters are specialized functions used for the modular composition of our complex server software. Finally, we discuss our experiences using these abstractions and techniques throughout Twitter's serving infrastructure.
NICs are increasingly complex and diverse, offering a wide range of hardware functionality to aid network protocol processing. Harnessing the power of NIC hardware requires the ability to control and reason about a variety of different feature sets in the network stack. Towards this goal, we propose Unicorn, a language for describing modern NICs. Unicorn offers a simple set of abstractions for modeling both NIC functionality and the state of a protocol stack. To evaluate its expressivity and potential, we present a non-trivial model for the Intel i82599 10GbE NIC, and an algorithm that uses graph embedding to optimize the use of NIC hardware in the network stack.
Attempts have been made to understand driver development in terms of code clones. In this paper, we propose an alternate view, based on the metaphor of a gene. Guided by this metaphor, we study the structure of Linux 3.10 ethernet platform driver probe functions.
Operating systems and programming languages are often informally evaluated on their conduciveness towards composition. We revisit Dan Ingalls' Smalltalk-inspired position that "an operating system is a collection of things that don't fit inside a language; there shouldn't be one", discussing what it means, why it appears not to have materialised, and how we might work towards the same effect in the postmodern reality of today's systems. We argue that the trajectory of the "file" abstraction through Unix and Plan 9 culminates in a Smalltalk-style object, with other filesystem calls as a primitive metasystem. Meanwhile, the key features of Smalltalk have many analogues in the fragmented world of Unix programming (including techniques at the library, file and socket level). Based on the themes of unifying OS- and language-level mechanisms, and increasing the expressiveness of the meta-system, we identify some evolutionary approaches to a postmodern realisation of Ingalls' vision, arguing that an operating system is still necessary after all.
This paper describes ongoing work on a new technique for reducing the cost of assurance of large software systems by building on a verified component platform. From a component architecture description, we automatically derive a formal model of the system and a semantics for the runtime behaviour of generated inter-component communication code. We can prove wellformedness properties of the architecture automatically and provide a framework in which users can reason about their component code and its behaviour. By leveraging the isolation properties and communication guarantees of a formally verified platform, correctness arguments for critical components will be able to be derived independently and composed together to reason about system-level correctness.
For modern software systems, performance analysis can be a challenging task. The software stack can be a complex, multi-layer, multi-component, concurrent, and parallel environment with multiple contexts of execution and multiple sources of performance data. Although much performance data is available, because modern systems incorporate many mature data-collection mechanisms, analysis algorithms suffer from the lack of a unifying programming environment for processing the collected performance data, potentially from multiple sources, in a convenient and script-like manner. This paper presents Weir, a streaming language for systems performance analysis. Weir is based on the insight that performanceanalysis algorithms can be naturally expressed as stream-processing pipelines. In Weir, an analysis algorithm is implemented as a graph composed of stages, where each stage operates on a stream of events that represent collected performance measurements. Weir is an imperative streaming language with a syntax designed for the convenient construction of stream pipelines that utilize composable and reusable analysis stages. To demonstrate practical application, this paper presents the authors' experience in using Weir to analyze performance in systems based on the Xen virtualization platform.
The management of the releasing of allocated resources is a continual problem in ensuring the robustness of systems code. Missing resource-releasing operations lead to memory leaks and deadlocks. A number of approaches have been proposed to detect such problems, but they often have a high rate of false positives, or focus only on commonly used functions. In this paper we observe that resource-releasing operations are often found in error-handling code, and that the choice of resource-releasing operation may depend on the context in which it is to be used. We propose an approach to finding resource-release omission faults in C code that takes into account these issues. We use our approach to find over 100 faults in the drivers directory of Linux 2.6.34, with a false positive rate of only 16%, well below the 30% that has been found to be acceptable to developers.
We have been developing a framework, called Recon, that uses runtime checking to protect the integrity of file-system metadata on disk. Recon performs consistency checks at commit points in transaction-based file systems. We define declarative statements called consistency invariants for a file system, which must be satisfied by each transaction being committed to disk. By checking each transaction before it commits, we prevent any corruption to file-system metadata from reaching the disk. Our prototype system required writing the consistency invariants in C. In this paper, we argue that using a declarative language to express and check these invariants improves the clarity of the rules, making them easier to reason about, verify, and port to new file systems. We describe how file system invariants can be written and checked using the Datalog declarative language in the Recon framework.
System software, especially operating systems, tends to be highly configurable. Like every complex piece of software, a considerable amount of bugs in the implementation has to be expected. In order to improve the general code quality, tools for static analysis provide means to check for source code defects without having to run actual test cases on real hardware. Still, for proper type checking a specific configuration is required so that all header include paths are available and all types are properly resolved. In order to find as many bugs as possible, usually a "full configuration" is used for the check. However, mainly because of alternative blocks in form of #else-blocks, a single configuration is insufficient to achieve full coverage. In this paper, we present a metric for configuration coverage (CC) and explain the challenges for (properly) calculating it. Furthermore, we present an efficient approach for determining a sufficiently small set of configurations that achieve (nearly) full coverage and evaluate it on a recent Linux kernel version.
Reversible debuggers have existed since the early 1970s. A novel approach, URDB, is introduced based on checkpoint/re-execute. It adds reversibility to a debugger, while still placing the end user within the familiar environment of their preferred debugger. The URDB software layer currently includes modes that understand the syntax for four debuggers: GDB for C/C++/Java/Fortran, Python (pdb), MATLAB, and Perl (perl -d). It does so by adding a thin URDB software layer on top of the DMTCP checkpoint-restart package. URDB passes native debugging commands between the end user and the underlying debugging session. URDB models the four common debugging primitives that form the basis for most debuggers: step, next, continue, break. For example, given a debugging history of the form [step, next, step], URDB's reverse-step produces a new history, [step, next]. Further, subtle algorithms are described for reverse-xxx. For example, reverse-step operates correctly when the last instruction of the history is next or continue. URDB calls DMTCP to create a checkpoint during a de-bugging session, and then replays the history from there. An essential novelty of this work is the extension of DMTCP to be the first checkpointing package capable of checkpointing a GDB sesssion to disk (through checkpointing the Linux ptrace system call). This was a significant barrier to earlier attempts toward checkpoint/re-execute for GDB. Support for the GDB debugger is important to any reversible debugger claiming universality. Experimental results are described for GDB, MATLAB, Python (pdb), and Perl.
Deadlocks can have devastating effects in systems code. We have developed a type and effect system that provably avoids them and in this paper we present a tool that uses a sound static analysis to instrument multithreaded C programs and then links these programs with a run-time system that avoids possible deadlocks. In contrast to most other purely static tools for deadlock freedom, our tool does not insist that programs adhere to a strict lock acquisition order or use lock primitives in a block-structured way, thus it is appropriate for systems code and OS applications. We also report some very promising benchmark results which show that all possible deadlocks can automatically be avoided with only a small run-time overhead. More importantly, this is done without having to modify the original source program by altering the order of resource acquisition operations or by adding annotations.
Recent trends in secure operating systems indicate that an object-capability system is the security model with pre-eminent characteristics and practicality. Unlike traditional operating systems, which use a single global name space, object-capability systems name objects per protection domain. This allows a fine-grained isolation of the domains and follows the principle of least authority. Programming in such an environment differs considerably from traditional programming models. The fine-grained access to functionality requires a programming environment that supports the programmer when using a capability system. In this paper, we present an object-oriented framework that uses the C++ programming language to offer a frame-work for building and using operating-system components and applications.
Safe is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assembled a set of basic architectural choices that we believe will yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.
In this paper, we present CatchAndRetry, an extension of the traditional exception mechanism to provide language-level support for common recovery techniques in distributed systems. We motivate and justify our design by analyzing several cases studies taken from the context of Facebook. CatchAndRetry is a language mechanism that is general enough to apply to multiple tiers of a distributed application; throughout this paper, we illustrate CatchAndRetry with examples of its use within both a large-scale distributed server-side application running in a data center as well as a JavaScript clients-side application running within a web browser.
Debuggers and instrumentation tools have been proven valuable for understanding the inner workings of software systems. Although these tools are essential for various people, e.g. , system administrators, developers, or teachers, they have one major drawback, especially in multi-threaded environments: They completely ignore data races. Within this paper, we present KStruct, a holistic approach for inspecting state information of a system while running. We therefore use a multi-level approach: First KStruct Access, our domain-specific language, can be used to model lock dependencies. Second, based on that model, we generate an access driver that dynamically attaches to the system under investigation and leverages that model to access state information. Our proposed approach can therefore improve quality in two dimensions: The code by making locking first-class primitives, and second the retrieved data is more reliable to be consistent.
Code-Partitioning Gossip (CPG) is a novel technique to facilitate implementation and analysis of gossip protocols. A gossip exchange is a pair-wise transaction between two nodes; a gossip system executes an endless sequence of exchanges between nodes chosen by a randomized procedure. Using CPG, the effects of a gossip exchange are succinctly defined by a single function that atomically updates a pair of node states based on their previous values. This function is automatically partitioned via program slicing into executable code for the roles of gossip-initiator and gossip-recipient, and networking code is added automatically. CPG may have concrete benefits for protocol analysis and authoring composite gossip protocols.
