{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/87955"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/87955","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Testing, runtime verification, and analysis of concurrent programs","abstract":"With the development of multi-core processors, concurrent programs are becoming more and more popular. Among several models, the multithreaded shared-memory model is the predominant programming paradigm for developing concurrent programs. However, because of non-deterministic scheduling, multithreaded code is hard to develop and test. Concurrency bugs, such as data races, atomicity violations, and deadlocks, are hard to detect and fix in multithreaded programs. To test and verify multithreaded programs, two sets of techniques are needed. The first one is to enforce thread schedules and runtime properties efficiently. Being able to enforce desired thread schedules and runtime properties would greatly help developers to develop reliable multithreaded code. The second one is to explore the state space of multithreaded programs efficiently. Systematic state-space exploration could guarantee correctness for mul- tithreaded code, however, it is usually time consuming and thus infeasible in most cases. This dissertation presents several techniques to address challenges arising in testing and runtime verification of multithreaded programs. The first two techniques are the IMUnit framework for enforcing testing schedules and the EnforceMOP system for enforcing runtime properties for multithreaded programs. An experimental evaluation shows that our techniques can enforce thread schedules and runtime properties effectively and efficiently, and have their own advantages over existing techniques. The other techniques are the RV-Causal framework and the CAPP technique in the ReEx framework for efficient state-space exploration of multithreaded code. RV-Causal employs the idea of the maximal causal model for state-space exploration in a novel way to reduce the exploration cost, without losing the ability to detect certain types of concurrency bugs. The results show that RV-Causal outperforms existing techniques by finding concurrency bugs and exploring the entire state space much more efficiently.","abstract_html":"With the development of multi-core processors, concurrent programs are becoming more and more popular. Among several models, the multithreaded shared-memory model is the predominant programming paradigm for developing concurrent programs. However, because of non-deterministic scheduling, multithreaded code is hard to develop and test. Concurrency bugs, such as data races, atomicity violations, and deadlocks, are hard to detect and fix in multithreaded programs. To test and verify multithreaded programs, two sets of techniques are needed. The first one is to enforce thread schedules and runtime properties efficiently. Being able to enforce desired thread schedules and runtime properties would greatly help developers to develop reliable multithreaded code. The second one is to explore the state space of multithreaded programs efficiently. Systematic state-space exploration could guarantee correctness for mul- tithreaded code, however, it is usually time consuming and thus infeasible in most cases. This dissertation presents several techniques to address challenges arising in testing and runtime verification of multithreaded programs. The first two techniques are the IMUnit framework for enforcing testing schedules and the EnforceMOP system for enforcing runtime properties for multithreaded programs. An experimental evaluation shows that our techniques can enforce thread schedules and runtime properties effectively and efficiently, and have their own advantages over existing techniques. The other techniques are the RV-Causal framework and the CAPP technique in the ReEx framework for efficient state-space exploration of multithreaded code. RV-Causal employs the idea of the maximal causal model for state-space exploration in a novel way to reduce the exploration cost, without losing the ability to detect certain types of concurrency bugs. The results show that RV-Causal outperforms existing techniques by finding concurrency bugs and exploring the entire state space much more efficiently.","abstract_has_math":false,"creators":["Luo, Qingzhou"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Rosu, Grigore","Marinov, Darko","Xie, Tao","Havelund, Klaus"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-09-29T20:37:38Z","date_published":"2015-09-29T20:37:38Z","updated_at":"2026-07-22T22:26:31Z","subjects":["Runtime verification","concurrency","testing"],"languages":["en"],"rights":["Copyright 2015 Qingzhou Luo"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/87955","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rosu, Grigore","Marinov, Darko","Xie, Tao","Havelund, Klaus"]},{"key":"dc:creator","label":"Author","values":["Luo, Qingzhou"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2015-09-29T20:37:38Z","2015-08","2015-06-02","2015-8"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Runtime verification","concurrency","testing"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2015 Qingzhou Luo"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/87955"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["With the development of multi-core processors, concurrent programs are becoming more and more popular. Among several models, the multithreaded shared-memory model is the predominant programming paradigm for developing concurrent programs. However, because of non-deterministic scheduling, multithreaded code is hard to develop and test. Concurrency bugs, such as data races, atomicity violations, and deadlocks, are hard to detect and fix in multithreaded programs. To test and verify multithreaded programs, two sets of techniques are needed. The first one is to enforce thread schedules and runtime properties efficiently. Being able to enforce desired thread schedules and runtime properties would greatly help developers to develop reliable multithreaded code. The second one is to explore the state space of multithreaded programs efficiently. Systematic state-space exploration could guarantee correctness for mul- tithreaded code, however, it is usually time consuming and thus infeasible in most cases. This dissertation presents several techniques to address challenges arising in testing and runtime verification of multithreaded programs. The first two techniques are the IMUnit framework for enforcing testing schedules and the EnforceMOP system for enforcing runtime properties for multithreaded programs. An experimental evaluation shows that our techniques can enforce thread schedules and runtime properties effectively and efficiently, and have their own advantages over existing techniques. The other techniques are the RV-Causal framework and the CAPP technique in the ReEx framework for efficient state-space exploration of multithreaded code. RV-Causal employs the idea of the maximal causal model for state-space exploration in a novel way to reduce the exploration cost, without losing the ability to detect certain types of concurrency bugs. The results show that RV-Causal outperforms existing techniques by finding concurrency bugs and exploring the entire state space much more efficiently.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2015-09-29 without embargo terms","The student, Qingzhou Luo, accepted the attached license on 2015-06-01 at 22:55.","The student, Qingzhou Luo, submitted this Dissertation for approval on 2015-06-01 at 23:03.","This Dissertation was approved for publication on 2015-06-02 at 08:59.","DSpace SAF Submission Ingestion Package generated from Vireo submission #8256 on 2015-09-29 at 13:21:25","Made available in DSpace on 2015-09-29T20:37:38Z (GMT). No. of bitstreams: 2 LUO-DISSERTATION-2015.pdf: 1183472 bytes, checksum: 0255f89f266a7568ca53574536e7655b (MD5) LICENSE.txt: 4209 bytes, checksum: f66d2d4e5bb093a6e00c59a7883ea9ab (MD5) Previous issue date: 2015-06-02"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Testing, runtime verification, and analysis of concurrent programs"]}]}],"canonical_facts":{"dc:contributor":["Rosu, Grigore","Marinov, Darko","Xie, Tao","Havelund, Klaus"],"dc:creator":["Luo, Qingzhou"],"dc:date":["2015-09-29T20:37:38Z","2015-08","2015-06-02","2015-8"],"dc:description":["With the development of multi-core processors, concurrent programs are becoming more and more popular. Among several models, the multithreaded shared-memory model is the predominant programming paradigm for developing concurrent programs. However, because of non-deterministic scheduling, multithreaded code is hard to develop and test. Concurrency bugs, such as data races, atomicity violations, and deadlocks, are hard to detect and fix in multithreaded programs. To test and verify multithreaded programs, two sets of techniques are needed. The first one is to enforce thread schedules and runtime properties efficiently. Being able to enforce desired thread schedules and runtime properties would greatly help developers to develop reliable multithreaded code. The second one is to explore the state space of multithreaded programs efficiently. Systematic state-space exploration could guarantee correctness for mul- tithreaded code, however, it is usually time consuming and thus infeasible in most cases. This dissertation presents several techniques to address challenges arising in testing and runtime verification of multithreaded programs. The first two techniques are the IMUnit framework for enforcing testing schedules and the EnforceMOP system for enforcing runtime properties for multithreaded programs. An experimental evaluation shows that our techniques can enforce thread schedules and runtime properties effectively and efficiently, and have their own advantages over existing techniques. The other techniques are the RV-Causal framework and the CAPP technique in the ReEx framework for efficient state-space exploration of multithreaded code. RV-Causal employs the idea of the maximal causal model for state-space exploration in a novel way to reduce the exploration cost, without losing the ability to detect certain types of concurrency bugs. The results show that RV-Causal outperforms existing techniques by finding concurrency bugs and exploring the entire state space much more efficiently.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2015-09-29 without embargo terms","The student, Qingzhou Luo, accepted the attached license on 2015-06-01 at 22:55.","The student, Qingzhou Luo, submitted this Dissertation for approval on 2015-06-01 at 23:03.","This Dissertation was approved for publication on 2015-06-02 at 08:59.","DSpace SAF Submission Ingestion Package generated from Vireo submission #8256 on 2015-09-29 at 13:21:25","Made available in DSpace on 2015-09-29T20:37:38Z (GMT). No. of bitstreams: 2 LUO-DISSERTATION-2015.pdf: 1183472 bytes, checksum: 0255f89f266a7568ca53574536e7655b (MD5) LICENSE.txt: 4209 bytes, checksum: f66d2d4e5bb093a6e00c59a7883ea9ab (MD5) Previous issue date: 2015-06-02"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/87955"],"dc:language":["en"],"dc:rights":["Copyright 2015 Qingzhou Luo"],"dc:subject":["Runtime verification","concurrency","testing"],"dc:title":["Testing, runtime verification, and analysis of concurrent programs"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:31Z"}