Hitting Families of Schedules for Asynchronous Programs

DOI10.1007/978-3-319-41540-6_9MaRDI QIDQ4633553zbMATH OpenOpenAlexFDO

Authors Rupak Majumdar, Filip Niksic, Dmitry Chistikov

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1602.03755, http://wrap.warwick.ac.uk/97737/1/WRAP-hitting-families-schedules-asynchronous-programs-Chistikov-2016.pdf

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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.

Recommendations

• Asymptotic scheduling
• A family of scheduling algorithms for hybrid parallel platforms
• scientific article; zbMATH DE number 1760079
• Schedulability of asynchronous real-time concurrent objects
• Mixed Pfair/ERfair scheduling of asynchronous periodic tasks
• Scheduling computations with provably low synchronization overheads
• Efficient execution of nondeterministic parallel programs on asynchronous systems

Cited in

(1)

• Delay-bounded scheduling

This page was built for publication: Hitting Families of Schedules for Asynchronous Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4633553)