Wednesday, March 1, 2017
Speaker: Filip Nikšić
Venue: IST Austria
In systematic testing of concurrent systems, if the goal is to expose
bugs of “small depth,” one only needs to test a hitting family of
schedules. More precisely, in a system given as a partially ordered set
of events, we say a bug has depth $d$ if it is exposed by ordering $d$
specific events in a particular way, irrespective of how the other
events are ordered. A set of schedules is called a $d$-hitting family if
for every admissible ordering of $d$ events, there is a schedule in the
family that schedules these events in this order. We showed previously
that when the partial order forms a tree, we can explicitly construct
hitting families of size polynomial in the height of the tree, and
therefore polylogarithmic in the number of events when the tree is balanced.
In the follow-up work, which I will present in this talk, we consider an
extended setting where an event can be executed correctly or with a
fault. A fault does not necessarily entail a bug, as the developer may
have included fault-handling mechanisms. Faults merely mean that the
space of possible schedules is now much larger. Our preliminary results
show that even with faults, there are hitting families of size
polylogarithmic in the number of events.
In the talk I will also present COFIT—Concurrency and Fault Injection
Testing framework for .NET applications, which incorporates
constructions of hitting families.