Runtime verification of concurrency-specific correctness criteria

We give an overview of correctness criteria specific to concurrent shared-memory programs and runtime verification techniques for verifying these criteria. We cover a spectrum of criteria, from ones focusing on low-level thread interference such as races to higher-level ones such as linearizability. We contrast these criteria in the context of runtime verification. We present the key ideas underlying the runtime verification techniques for these criteria and summarize the state of the art. Finally, we discuss the issue of coverage for runtime verification for concurrency and present techniques that improve the set of covered thread interleavings.     

Linking simulation with formal verification at a higher level

We use simulation to bridge the gap between specification and formal verification of high-level models and simulation of RTL models. The authors apply their practical, two-phase procedure for defining the refinement map to the Alpha 21364 multiprocessing hardware. The methodology and tools they present can improve simulation coverage. Our technique verifies that a hardware design described at the RTL is a correct implementation of an algorithm-level, executable formal specification. We use a high-level formal specification as the basis for monitoring functional correctness, measuring simulation coverage, and generating test cases.     

Coverage metrics for functional validation of hardware designs

Software simulation remains the primary means of functional validation for hardware designs. Coverage metrics ensure optimal use of simulation resources, measure the completeness of validation, and direct simulations toward unexplored areas of the design. This article surveys the literature, and discusses the experiences of verification practitioners, regarding coverage metrics     

VyrdMC: Driving Runtime Refinement Checking with Model Checkers

This paper presents VyrdMC, a runtime verification tool we are building for concurrent software components. The correctness criterion checked by VyrdMC is refinement: Each execution of the implementation must be consistent with an atomic execution of the specification. VyrdMC combines testing, model checking, and Vyrd, the runtime refinement checker we developed earlier. A test harness first drives the component to a non-trivial state which serves as the starting state for a number of simple, very small multi-threaded test cases. An execution-based model checker explores for each test case all distinct thread interleavings while Vyrd monitors executions for refinement violations. This combined approach has the advantage of improving the coverage of runtime refinement checking at modest additional computational cost, since model checkers are only used to explore thread interleavings of a small, fixed test program. The visibility and detailed checking offered by using refinement as the correctness criterion differentiate our approach from simply being a restricted application of model checking. An important side benefit is the reduction in program instrumentation made possible if VyrdMC is built using a model checker with its own virtual machine, such as Java PathFinder [Guillaume Brat, Klaus Havelund, Seung-Joon Park, and Willem Visser. Model Checking Programs. In IEEE International Conference on Automated Software Engineering (ASE), September 2000]. We are investigating the use of two different model checkers for building VyrdMC: Java PathFinder, an explicit-state model checker and Verisoft, a “stateless” model checker [P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997].     

Checking Cache-Coherence Protocols with TLA+

We have a great deal of experience using the specification language TLA⁺ and its model checker TLC to analyze protocols designed at Digital and Compaq (both now part of HP). The tools and techniques we have developed apply equally well to software and hardware designs. In this paper, we describe our experience using TLA⁺ and TLC to verify cache-coherence protocols.     

Location pairs: a test coverage metric for shared-memory concurrent programs

We present a coverage metric targeted at shared-memory concurrent programs: the Location Pairs (LP) coverage metric. The goals of this metric are (i) to measure how thoroughly a program has been tested from a concurrency standpoint, i.e., whether enough qualitatively different thread interleavings have been explored, and (ii) to guide testing towards unexplored concurrency scenarios. This metric was inspired by an access pattern known to lead to high-level concurrency errors in industrial software and in the literature. We built a monitoring tool to measure LP coverage of test programs. We used the LP metric for interactive debugging, and compared LP coverage with other concurrency coverage metrics on Java benchmarks. We demonstrated that LP coverage corresponds better to concurrency errors, is a better measure of how well a program is exercised concurrency-wise by a test set, reaches saturation later than other coverage metrics, and is viable and useful as an interactive testing and debugging tool.     

Wavelength selective optical logic and interconnects

A wavelength selective optical logic (WSOL) element that uses monolithically integrated wavelength selective optical input and output elements is described. Input optical signals are detected by photothyristors situated in an optical cavity which provides a highly selective response of a wavelength determined by the fabrication process. Output signals are generated by vertical cavity surface emitting lasers, whose lasing wavelengths can also be specified during the fabrication process. A vertical integration of these input and output elements that is suitable for wavelength selective optical logic and wavelength selective optical interconnect applications is proposed. The proposed circuitry is easily cascadable so that arbitrarily complex optical logic functions can be performed by WSOL devices in series. Several of the possible logic functions are described, including OR and AND gates, an adder, and a flip-flop