RV 2017: 17TH INTERNATIONAL CONFERENCE ON RUNTIME VERIFICATION
PROGRAM FOR SATURDAY, SEPTEMBER 16TH
Days:
previous day
all days

View: session overviewtalk overview

09:00-10:00 Session 16: Invited Talk
09:00
The Design and Applications for a Tracing Plane for Distributed Systems

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.

10:00-10:30Coffee Break
10:30-12:00 Session 17: Cyber-Physical Systems
10:30
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.

11:00
Stream Runtime Monitoring on UAS

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.

11:30
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.

12:00-13:30Lunch Break
13:30-15:00 Session 18: Program Analysis
13:30
Control Dependencies in Interpretive Systems
SPEAKER: unknown

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.

14:00
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.

14:30
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.

15:00-15:30Coffee Break
15:30-17:00 Session 19: Concurrency
15:30
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.

16:00
Event Stream Processing with Multiple Threads
SPEAKER: unknown

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.

16:15
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.

16:30
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.