Koşut-zamanlı yazılım bileşenleri için çalışma zamanı arıtma denetimi

In this thesis, we present a runtime technique for checking that a con-currently accessed data structure implementation, such as a file system orthe storage management module of a database, conforms to an executablespecification that contains an atomic method per data structure operation.The specification can be provided separately or a non-concurrent, ?atom-ized? interpretation of the implementation can serve as the specification.The technique consists of two phases. In the first phase, the implementationis instrumented in order to record information into a log during execution.In the second, a separate verification thread uses the logged information todrive an instance of the specification and to check whether the logged exe-cution conforms to it. We paid special attention to the general applicabilityand scalability of the techniques and to minimizing their concurrency andperformance impact. The result is a lightweight verification method thatprovides a significant improvement over testing for concurrent programs.We formalize conformance to a specification using the notion of refine-ment: Each trace of the implementation must be equivalent to some trace ofthe specification. Among the novel features of our work are two variationson the definition of refinement appropriate for runtime checking: I/O andview refinement. These definitions were motivated by our experience withindustrial-scale concurrent data structure implementations in the Boxwoodproject, a novel storage infrastructure. I/O and view refinement checkingwere implemented as a verification tool named VYRD (VerifYing concurrentprograms by Runtime Refinement-violation Detection). VYRD was appliedto the verification of Boxwood, Java class libraries. It was able to detectpreviously unnoticed subtle concurrency bugs in Boxwood, the known bugsin the Java class libraries and manually constructed examples. Experimentalresults indicate that our techniques have modest computational cost.