File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: Efficient deterministic multithreading through schedule relaxation

TitleEfficient deterministic multithreading through schedule relaxation
Authors
Keywordssymbolic execution
deterministic multithreading
program simplification
program slicing
Issue Date2011
Citation
SOSP'11 - Proceedings of the 23rd ACM Symposium on Operating Systems Principles, 2011, p. 337-351 How to Cite?
AbstractDeterministic multithreading (DMT) eliminates many pernicious software problems caused by nondeterminism. It works by constraining a program to repeat the same thread interleavings, or schedules, when given same input. Despite much recent research, it remains an open challenge to build both deterministic and efficient DMT systems for general programs on commodity hardware. To deterministically resolve a data race, a DMT system must enforce a deterministic schedule of shared memory accesses, or mem-schedule, which can incur prohibitive overhead. By using schedules consisting only of synchronization operations, or sync-schedule, this overhead can be avoided. However, a sync-schedule is deterministic only for race-free programs, but most programs have races. Our key insight is that races tend to occur only within minor portions of an execution, and a dominant majority of the execution is still race-free. Thus, we can resort to a mem-schedule only for the "racy" portions and enforce a sync-schedule otherwise, combining the efficiency of sync-schedules and the determinism of mem-schedules. We call these combined schedules hybrid schedules. Based on this insight, we have built Peregrine, an efficient deterministic multithreading system. When a program first runs on an input, Peregrine records an execution trace. It then relaxes this trace into a hybrid schedule and reuses the schedule on future compatible inputs efficiently and deterministically. Peregrine further improves efficiency with two new techniques: determinism-preserving slicing to generalize a schedule to more inputs while preserving determinism, and schedule-guided simplification to precisely analyze a program according to a specific schedule. Our evaluation on a diverse set of programs shows that Peregrine is deterministic and efficient, and can frequently reuse schedules for half of the evaluated programs. © 2011 ACM.
Persistent Identifierhttp://hdl.handle.net/10722/207913

 

DC FieldValueLanguage
dc.contributor.authorCui, H-
dc.contributor.authorWu, J-
dc.contributor.authorGallagher, JP-
dc.contributor.authorGuo, H-
dc.contributor.authorYang, J-
dc.date.accessioned2015-01-26T11:46:42Z-
dc.date.available2015-01-26T11:46:42Z-
dc.date.issued2011-
dc.identifier.citationSOSP'11 - Proceedings of the 23rd ACM Symposium on Operating Systems Principles, 2011, p. 337-351-
dc.identifier.urihttp://hdl.handle.net/10722/207913-
dc.description.abstractDeterministic multithreading (DMT) eliminates many pernicious software problems caused by nondeterminism. It works by constraining a program to repeat the same thread interleavings, or schedules, when given same input. Despite much recent research, it remains an open challenge to build both deterministic and efficient DMT systems for general programs on commodity hardware. To deterministically resolve a data race, a DMT system must enforce a deterministic schedule of shared memory accesses, or mem-schedule, which can incur prohibitive overhead. By using schedules consisting only of synchronization operations, or sync-schedule, this overhead can be avoided. However, a sync-schedule is deterministic only for race-free programs, but most programs have races. Our key insight is that races tend to occur only within minor portions of an execution, and a dominant majority of the execution is still race-free. Thus, we can resort to a mem-schedule only for the "racy" portions and enforce a sync-schedule otherwise, combining the efficiency of sync-schedules and the determinism of mem-schedules. We call these combined schedules hybrid schedules. Based on this insight, we have built Peregrine, an efficient deterministic multithreading system. When a program first runs on an input, Peregrine records an execution trace. It then relaxes this trace into a hybrid schedule and reuses the schedule on future compatible inputs efficiently and deterministically. Peregrine further improves efficiency with two new techniques: determinism-preserving slicing to generalize a schedule to more inputs while preserving determinism, and schedule-guided simplification to precisely analyze a program according to a specific schedule. Our evaluation on a diverse set of programs shows that Peregrine is deterministic and efficient, and can frequently reuse schedules for half of the evaluated programs. © 2011 ACM.-
dc.languageeng-
dc.relation.ispartofSOSP'11 - Proceedings of the 23rd ACM Symposium on Operating Systems Principles-
dc.subjectsymbolic execution-
dc.subjectdeterministic multithreading-
dc.subjectprogram simplification-
dc.subjectprogram slicing-
dc.titleEfficient deterministic multithreading through schedule relaxation-
dc.typeConference_Paper-
dc.description.naturelink_to_subscribed_fulltext-
dc.identifier.doi10.1145/2043556.2043588-
dc.identifier.scopuseid_2-s2.0-82655162762-
dc.identifier.spage337-
dc.identifier.epage351-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats