ABSTRACT. Many tasks for understanding and managing the execution of systems such as debugging, snapshotting, monitoring, accounting, and providing performance guarantees, are much harder in distributed settings. Correspondingly, many techniques such as distributed timestamps, end-to-end tracing, and taint tracking have been successfully used to help with these tasks. Their deployment, however, is usually fraught with difficulties, including intrusive instrumentation and lack of pervasiveness. In this talk I describe some of the recent successes we’ve had with these mechanisms, including Pivot Tracing (SOSP 2015) and Retro (NSDI 2015), and will outline a vision for the Tracing Plane, a layered architecture that distills primitives that are common to all these techniques — most importantly the causal propagation of generic metadata — making traceability a first-class concept in distributed systems. The Tracing Plane simplifies the instrumentation of current and new systems, and lowers the barrier for the adoption of existing and novel introspection and management techniques.
Combining Symbolic Runtime Enforcers for Cyber-Physical Systems
SPEAKER: unknown
ABSTRACT. The problem of composing multiple, possibly conflicting, runtime
enforcers for a cyber-physical system (CPS) is considered. A formal
definition of utility-agnostic and utility-maximizing CPS enforcers is
presented, followed by an algorithm to combine multiple enforcers, and
resolve their conflicts based on a design-time prioritization. To
implement this combination in an efficient manner, enforcers are
encoded symbolically using SMT formulas, and the combination is
reduced to a set of SMT satisfiabilty and optimization
operations. Further performance gains are achieved by using the SMT
solvers incrementally. Schedulbality of enforcers is achieved by
assigning them the highest criticality level and using a
mixed-criticality scheduled called ZSRM. The approach is validated
via experiments in an indoor arena with Parrot minidrones. The
incremental enforcer combination is shown to achieve an order of
magnitude speedup, and no deadline misses under extended operation.
ABSTRACT. Unmanned Aerial Vehicles (UAV) with autonomous decision-making capabilities are of increasing interest for a wide area of applications such as logistics and disaster recovery. In order to ensure the correct behavior of the system and to recognize hazardous situations or system faults, we applied stream runtime monitoring techniques within the DLR ARTIS (Autonomous Research Testbed for Intelligent System) family of unmanned aircrafts. We present our experience from specification elicitation, instrumentation, offline log file analysis, and online monitoring on the flight computer on a test rig. The debugging and health management support through stream runtime monitoring techniques have proven highly beneficial for system design and development. At the same time, the project has identified usability improvements to the specification language, and has influenced the design of the language.
Hierarchical Non-Intrusive In-Situ Requirements Monitoring for Embedded Systems
SPEAKER: unknown
ABSTRACT. Accounting for all operating conditions of a system at the design stage is typically infeasible for complex systems. In-situ runtime monitoring and verification can enable a system to introspectively ensure the system is operating correctly in the presence of dynamic environment, to rapidly detect failures, and to provide detailed execution traces to find the root cause thereof. In this paper, we seek to address two challenges faced in using in-situ runtime verification for embedded systems, including 1) efficiently defining and automatically constructing a requirements model for embedded system software and 2) minimizing the runtime overhead of observing and verifying the runtime execution adheres to the requirements model. We present a methodology to construct a hierarchical runtime monitoring graph from system requirements specified using multiple UML sequence diagrams, which are already commonly used in software development. We further present the design of on-chip hardware that nonintrusively monitors the system at runtime to ensure the execution matches the requirements model. We evaluate the proposed methodology using a case study of a fail-safe autonomous vehicle subsystem and analyze the relationship between event coverage, detection rate, and hardware requirements.
ABSTRACT. Interpreters and just-in-time (JIT) compilers are ubiquitous in
modern computer systems, making it important to have
good program analyses for reasoning about
such systems. Control dependence, which plays a
fundamental role in a number of program analyses, is an
important contender in this regard. Existing
algorithms for (dynamic) control dependence analysis do
not take into account some important runtime characteristics of
interpretive computations, and as a result produce results that
may be imprecise and/or unsound.
This paper describes a new notion of control dependence
and analysis algorithm for interpretive systems.
This significantly improves dynamic control dependence
information, with corresponding improvements in client analyses
such as dynamic program slicing and reverse engineering. To the best of our
knowledge, this is the first proposal to reason about low-level dynamic control dependencies
in interpretive systems in the presence of dynamic code generation
and optimization.
Combining Model Checking and Runtime Verification for Safe Robotics
SPEAKER: unknown
ABSTRACT. A major challenge towards large scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation.
To this end, we present a framework for building safe robots.
Our approach for validating the end-to-end correctness of robotics system
consists of two parts:
1) a high-level programming language for implementing and systematically testing the reactive robotics software via model checking;
2) a signal temporal logic (STL) based online monitoring system to ensure that the assumptions about the low-level
controllers (discrete models) used during model checking hold at runtime.
Combining model checking with runtime verification helps us bridge the gap between software verification (discrete) that makes assumptions about the low-level controllers and the physical world, and the actual execution of the software on a real robotic platform in the physical world.
To demonstrate the efficacy of our methods, we build a safe adaptive surveillance system and present software-in-the-loop simulations of the application.
From Model Checking to Runtime Verification and Back
SPEAKER: unknown
ABSTRACT. In this paper, we describe a novel approach for adapting an existing
software model checker to perform precise runtime verification. The
software under test is allowed to communicate with the wider environment
(including the file system and network). The modifications to the model
checker are small and self-contained, making this a viable strategy for
re-using existing model checking tools in a new context.
Additionally, from the data that is gathered during a single execution in
the runtime verification mode, we automatically re-construct a description
of the execution environment which can then be used in the standard,
full-blown model checker. This additional verification step can further
improve coverage, especially in the case of parallel programs, without
introducing substantial overhead into the process of runtime verification.
Annotation Guided Collection of Context-Sensitive Parallel Execution Profiles
SPEAKER: unknown
ABSTRACT. Studying the relative behavior of an application’s threads is critical to identifying performance bottlenecks and understanding their root causes. We present context-sensitive parallel (CSP) execution profiles, that capture the relative behavior of parallel threads in terms of the user selected code regions they execute. CSPs can be easily analyzed to compute execution times spent by the application in interesting behavior states. The user is provided with a simple and versatile suite of annotations to mark code regions of interest and name them statically or dynamically to capture their execution context. The CSP divides the execution time of a multithreaded application into time intervals or a sequence of frames during which the code regions being executed in parallel by application threads remain unchanged. We show that by appropriate selection and naming of code regions, the user can obtain a CSP that captures all occurrences of relevant behavior states. We provide the user with a powerful query language to facilitate the analysis of CSPs. Our implementation for collection of CSPs of C++ programs has low overhead and high accuracy. Collection of CSPs of full executions of eight Parsec programs incurred overhead of 0% to 7% in execution time.The accuracy of CSPs was validated in the context of common performance problems such as lock contention, load imbalance in pipeline stages, and the presence of straggler threads.
ABSTRACT. Current runtime verification tools seldom make use of multi-threading to speed up the evaluation of a property on a large event trace. In this paper, we present an extension to the BeepBeep 3 event stream engine that allows the use of multiple threads during the evaluation of a query. The extension requires minimal changes to an existing query to enable multi-threading. Various parallelization strategies are presented and described on simple examples. The implementation of these strategies is then evaluated empirically on a sample of problems taken from the Competition on Runtime Verification. Compared to the previous, single-threaded version of the BeepBeep engine, the allocation of just a few threads to specific portions of a query provides dramatic improvement in terms of running time.
EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM
SPEAKER: unknown
ABSTRACT. In this paper, we propose EmbedSanitizer, a tool for detecting
concurrency data races in 32-bit ARM-based multithreaded C/C++
applications. Moreover, we motivate the idea of detecting data
races in embedded systems software natively; without virtualization
or emulation or use of alternative architecture. Detecting data
races in applications on a target hardware provides more precise
results and increased throughput and hence more developer productivity.
EmbedSanitizer extends ThreadSanitizer, a race detection tool for
64-bit applications, to do race detection for 32-bit ARM applications.
We evaluate EmbedSanitizer using PARSEC benchmarks in an ARMv7
CPU with 4 logical cores and 933MB of RAM. Our race detection results
precisely match with results when the same benchmarks run on 64-bit
machine using ThreadSanitizer. Moreover, the performance overhead of
EmbedSanitizer is relatively low as compared to running race detection in
an emulator which is a common platform for embedded software
development.
Space Efficient Breadth-First and Level Traversals of Consistent Global States of Parallel Programs
SPEAKER: unknown
ABSTRACT. Enumerating consistent global states of a computation is a
fundamental problem in parallel computing with applications to debug-
ging, testing and runtime verification of parallel programs. Breadth-first
search (BFS) enumeration is especially useful for these applications as it
finds an erroneous consistent global state with the least number of events
possible. The total number of executed events in a global state is called
its rank. BFS also allows enumeration of all global states of a given rank
or within a range of ranks. If a computation on n processes has m events
per process on average, then the traditional BFS (Cooper-Marzullo and
its variants) requires O(m^{n−1} /n ) space in the worst case, whereas our algorithm performs the BFS requires O(m^2.n^2) space. Thus, we reduce the space complexity for BFS enumeration of consistent global states exponentially. and give the first polynomial space algorithm for this task. In our experimental evaluation of seven benchmarks, traditional BFS fails in many cases by exhausting the 2 GB heap space allowed to the JVM. In contrast, our implementation uses less than 60 MB memory and is also faster in many cases.