Static Detection of Atomic-Set-Serializability Violations

Abstract

Vaziri et al. [1] propose a data-centric approach to synchronization. The key underlying concept of their work is the atomic set, which specifies the existence of an invariant that holds on a set of fields of an object type. In addition, they formalize a set of eleven data-access scenarios that completely specify the set of non-serializable interleaving patterns that can lead to an atomic-set serializability violation of the expressed invariant. We present an algorithm that uses state-space exploration techniques to statically detect atomic-set serializability violations. The key idea is that the data-access scenarios can be used as a property specification for a software model checker. We tested our technique on programs with known serialiability violations from the concurrency-testing benchmark created by Eytani et al. Of the ten programs analyzed, our tool reported eight atomic-set serializability violations, with seven of them being true bugs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2007
Accession Number
AD1006567

Entities

People

  • Julian Dolby
  • Mandana Vaziri
  • Nicholas Kidd
  • Thomas Reps

Organizations

  • University of Wisconsin–Madison

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Computer Programming
  • Computer Programs
  • Construction
  • Databases
  • Debugging
  • Detection
  • Detectors
  • Instructions
  • Language
  • Monitors
  • Multithreading
  • Operating Systems
  • Software Development
  • Software Testing
  • Specifications

Fields of Study

  • Computer science

Readers

  • Defense Financial Management and Audit.
  • Neural Network Machine Learning.
  • Parallel and Distributed Computing.

Technology Areas

  • Space