VYRD: verifYing concurrent programs by runtime refinement-violation detection

ABSTRACT

We present a runtime technique for checking that a concurrently-accessed data structure implementation, such as a file system or the storage management module of a database, conforms to an executable specification that contains an atomic method per data structure operation. The specification can be provided separately or a non-concurrent, "atomized" interpretation of the implementation can serve as the specification. The technique consists of two phases. In the first phase, the implementation is instrumented in order to record information into a log during execution. In the second, a separate verification thread uses the logged information to drive an instance of the specification and to check whether the logged execution conforms to it. We paid special attention to the general applicability and scalability of the techniques and to minimizing their concurrency and performance impact. The result is a lightweight verification method that provides a significant improvement over testing for concurrent programs.We formalize conformance to a specification using the notion of refinement: Each trace of the implementation must be equivalent to some trace of the specification. Among the novel features of our work are two variations on the definition of refinement appropriate for runtime checking: I/O and "view" refinement. These definitions were motivated by our experience with two industrial-scale concurrent data structure implementations: the Boxwood project, a B-link tree data structure built on a novel storage infrastructure [10] and the Scan file system [9]. I/O and view refinement checking were implemented as a verification tool named VRYD (VerifYing concurrent programs by Runtime Refinement-violation Detection). VYRD was applied to the verification of Boxwood, Java class libraries, and, previously, to the Scan filesystem. It was able to detect previously unnoticed subtle concurrency bugs in Boxwood and the Scan file system, and the known bugs in the Java class libraries and manually constructed examples. Experimental results indicate that our techniques have modest computational cost.

REFERENCES

• 1: M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3rd Annual Symposium on Logic in Computer Science, pp. 165--175. IEEE Computer Society Press, 1988.
• 2: F. Chen and G. Rosu. Towards monitoring-oriented programming: A paradigm combining specification and implementation. In Electronic Notes in Theoretical Computer Science, Vol. 89. Elsevier, 2003.
• 3: M. L. Crane and J. Dingel. Runtime conformance checking of objects using Alloy. In Electronic Notes in Theoretical Computer Science, Vol. 89. Elsevier, 2003.
• 4: C. Flanagan. Verifying Commit-Atomicity Using Model-Checking. In SPIN '04: The SPIN Workshop on Model Checking of Software. Springer-Verlag, 2004.
• 5: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting purity for atomicity, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 6: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 7: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990 [doi>10.1145/78969.78972]
• 9: M. Ji and E. Felten. Scan-based scheduling and layout in a reliable write-optimized file system. Technical Report TR-661-02, Princeton University, Department of Computer Science, 2002.
• 10: J. MacCormick, N. Murphy, M. Najork, C. A. Thekkath, and L. Zhou. Boxwood: Abstractions as the foundation for storage infrastructure. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation (OSDI 2004), San Francisco, CA, USA, December 2004, pages 105--120. http://research.microsoft.com/research/sv/Boxwood
• 11: S. Park and D. L. Dill. Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems, 31(4):355--376, 1998.
• 12: Yehoshua Sagiv, Concurrent operations on B*-trees with overtaking, Journal of Computer and System Sciences, v.33 n.2, p.275-296, Oct. 1986 [doi>10.1016/0022-0000(86)90021-8]
• 13: S. Tasiran, A. Bogdanov, and M. Ji. Detecting concurrency errors in file systems by runtime refinement checking. Technical Report HPL-2004-177, HP Laboratories, 2004.
• 14: S. Tasiran and S. Qadeer. Runtime refinement verification of concurrent data structures. In Proc. Runtime Verification '04 (ETAPS '04). Electronic Notes in Theoretical Computer Science. Elsevier, 2004.
• 15: Serdar Tasiran , Yuan Yu , Brannon Batson, Using a formal specification and a model checker to monitor and direct simulation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775926]
• 16: L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Electronic Notes in Theoretical Computer Science, Vol.89. Elsevier, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation
      D.2.5 Testing and Debugging
          Subjects: Debugging aids; Tracing; Diagnostics; Monitors

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques; Mechanical verification

General Terms:
Algorithms, Verification

Keywords:
concurrent data structures, refinement, runtime verification