Abstract
dc:description.abstractConcurrent data structures have found increasingly widespread use in both multicore and distributed computing environments, thereby escalating the priority for verifying their correctness. The thread safe behavior of these concurrent objects is often described using formal semantics known as linearizability, which requires that every operation in a concurrent object appears to take effect between its invocation and response. Quasi linearizability is a quantitative relaxation of linearizability to allow more implementation freedom for performance optimization. However, ensuring the quantitative aspects of this new correctness condition is an arduous task. We propose the first method for formally verifying quasi linearizability of the implementation model of a concurrent data structure. The method is based on checking the refinement relation between the implementation model and a specification model via explicit state model checking. It can directly handle multi-threaded programs where each thread can make infinitely many method calls, without requiring the user to manually annotate for the linearization points. We have implemented and evaluated our method in the PAT model checking toolkit. Our experiments show that the method is effective in verifying quasi linearizability and in detecting its violations.
Degree
thesis:*- Name thesis:degree_name
- Master of Science
- Level thesis:degree_level
- masters
- Discipline thesis:degree_discipline
- Computer Engineering
- Department dc:contributor.department
- Electrical and Computer Engineering
- Grantor dc:publisher
- Virginia Tech
- Year dc:date.issued
- 2013
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Adhikari, Kiran
- Chair dc:contributor.committeechair
-
- Wang, Chao
- Committee members dc:contributor.committeemember
-
- Hsiao, Michael S.
- Schaumont, Patrick R.
Subjects
dc:subject × 3Rights
dc:rights- Statement dc:rights
-
- In Copyright
- Licence dc:rights.uri
Identifiers
dc:identifier.*- Dc Identifier Other
- vt_gsexam:1078
- OAI identifier oai:identifier
- oai:vtechworks.lib.vt.edu:10919/23222