{"id":{"repo_id":"vt","oai_identifier":"oai:vtechworks.lib.vt.edu:10919/23222"},"canonical_url":"https://search.dev.ndltd.org/etd/vt/oai:vtechworks.lib.vt.edu:10919/23222","repository":{"repo_id":"vt","name":"Virginia Tech","base_url":"https://vtechworks.lib.vt.edu/oai/request"},"display":{"title":"Verifying a Quantitative Relaxation of Linearizability via Refinement","abstract":"Concurrent 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.","abstract_html":"Concurrent 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.","abstract_has_math":false,"creators":["Adhikari, Kiran"],"institution":"Virginia Tech","degree_name":"Master of Science","degree_level":"masters","degree_discipline":"Computer Engineering","degree_department":"Electrical and Computer Engineering","school":null,"contributors":[],"advisors":[],"committee_chairs":["Wang, Chao"],"committee_members":["Hsiao, Michael S.","Schaumont, Patrick R."],"year":2013,"date_issued":"2013-06-13","date_published":"2013-06-13","updated_at":"2026-07-22T22:19:54Z","subjects":["Quasi Linearizability","Refinement","Model Checking"],"languages":[],"rights":["In Copyright"],"rights_urls":["http://rightsstatements.org/vocab/InC/1.0/"],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["vt_gsexam:1078"],"render_values":[{"text":"vt_gsexam:1078","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/10919/23222","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeechair","label":"Committee Chair","values":["Wang, Chao"]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Hsiao, Michael S.","Schaumont, Patrick R."]},{"key":"dc:contributor.department","label":"Department","values":["Electrical and Computer Engineering"]},{"key":"dc:creator","label":"Author","values":["Adhikari, Kiran"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2013-06-14T08:00:17Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2013-06-14T08:00:17Z"]},{"key":"dc:date.issued","label":"Date","values":["2013-06-13"]},{"key":"dc:publisher","label":"Institution","values":["Virginia Tech"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Virginia Polytechnic Institute and State University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Quasi Linearizability","Refinement","Model Checking"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/vocab/InC/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["vt_gsexam:1078"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10919/23222"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Concurrent 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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Master of Science"]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["ETD"]},{"key":"dc:title","label":"Title","values":["Verifying a Quantitative Relaxation of Linearizability via Refinement"]}]}],"canonical_facts":{"dc:contributor.committeechair":["Wang, Chao"],"dc:contributor.committeemember":["Hsiao, Michael S.","Schaumont, Patrick R."],"dc:contributor.department":["Electrical and Computer Engineering"],"dc:creator":["Adhikari, Kiran"],"dc:date.accessioned":["2013-06-14T08:00:17Z"],"dc:date.available":["2013-06-14T08:00:17Z"],"dc:date.issued":["2013-06-13"],"dc:description.abstract":["Concurrent 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."],"dc:description.degree":["Master of Science"],"dc:format.medium":["ETD"],"dc:identifier.other":["vt_gsexam:1078"],"dc:identifier.uri":["http://hdl.handle.net/10919/23222"],"dc:publisher":["Virginia Tech"],"dc:rights":["In Copyright"],"dc:rights.uri":["http://rightsstatements.org/vocab/InC/1.0/"],"dc:subject":["Quasi Linearizability","Refinement","Model Checking"],"dc:title":["Verifying a Quantitative Relaxation of Linearizability via Refinement"],"dc:type":["Thesis"],"thesis:degree_discipline":["Computer Engineering"],"thesis:degree_level":["masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Virginia Polytechnic Institute and State University"]},"updated_at":"2026-07-22T22:19:54Z"}