The Library
Hitting families of schedules for asynchronous programs
Tools
Chistikov, Dmitry, Majumdar, Rupak and Niksic, Filip (2016) Hitting families of schedules for asynchronous programs. In: 28th International Conference, CAV 2016, Toronto, ON, Canada, 17-23 Jul 2016. Published in: Computer Aided Verification. CAV 2016., 9780 pp. 157-176. ISBN 9783319415390. doi:10.1007/978-3-319-41540-6_9 ISSN 0302-9743.
|
PDF
WRAP-hitting-families-schedules-asynchronous-programs-Chistikov-2016.pdf - Accepted Version - Requires a PDF viewer. Download (1376Kb) | Preview |
Official URL: http://dx.doi.org/10.1007/978-3-319-41540-6_9
Abstract
We consider the following basic task in the testing of concurrent systems. The input to the task is a partial order of events, which models actions performed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these events can result in a bug. The number of schedules to be explored can, in general, be exponential.
Empirically, many bugs in concurrent programs have been observed to have small bug depth; that is, these bugs are exposed by every schedule that orders d specific events in a particular way, irrespective of how the other events are ordered, and d is small compared to the total number of events. To find all bugs of depth d, one needs to only test a d-hitting family of schedules: we call a set of schedules a d-hitting family if for each set of d events, and for each allowed ordering of these events, there is some schedule in the family that executes these events in this ordering. The size of a d-hitting family may be much smaller than the number of all possible schedules, and a natural question is whether one can find d-hitting families of schedules that have small size.
In general, finding the size of optimal d-hitting families is hard, even for d = 2. We show, however, that when the partial order is a tree, one can explicitly construct d-hitting families of schedules of small size. When the tree is balanced, our constructions are polylogarithmic in the number of events.
Item Type: | Conference Item (Paper) | ||||
---|---|---|---|---|---|
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Series Name: | Lecture Notes in Computer Science | ||||
Journal or Publication Title: | Computer Aided Verification. CAV 2016. | ||||
Publisher: | Springer | ||||
ISBN: | 9783319415390 | ||||
ISSN: | 0302-9743 | ||||
Book Title: | Computer Aided Verification | ||||
Official Date: | 2016 | ||||
Dates: |
|
||||
Volume: | 9780 | ||||
Page Range: | pp. 157-176 | ||||
DOI: | 10.1007/978-3-319-41540-6_9 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Date of first compliant deposit: | 19 March 2019 | ||||
Date of first compliant Open Access: | 19 March 2019 | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 28th International Conference, CAV 2016 | ||||
Type of Event: | Conference | ||||
Location of Event: | Toronto, ON, Canada | ||||
Date(s) of Event: | 17-23 Jul 2016 | ||||
Related URLs: | |||||
Open Access Version: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year