400
S. Akshay et al.
6 Implementation and Experiments
We implemented a tool BHIM (Bounded Holes In MPDA) in C++ based on
Algorithm 1, which takes an MPDA and a constant K as input and returns True
iff there exists a K-hole bounded run from the start state to an accepting state of
the MPDA. In case there is such an accepting run, BHIM generates one such, with
minimal number of holes. For a given hole bound K, BHIM first tries to produce
a witness with 0 holes, and iteratively tries to obtain a witness by increasing the
bound on holes till K. In most cases, BHIM found the witness before reaching
the bound K. Whenever BHIM’s witness had K holes, it is guaranteed that there
are no witnesses with a smaller number of holes.
To evaluate the performance of BHIM, we looked at some available benchmarks and modeled them as MPDA. We also added timing constraints to some
examples such that they can be modeled as TMPDA. Our tests were run on a
GNU/Linux system with Intel
R
Core
TM i7–4770K CPU @ 3.50GHz, and 16GB
of RAM. Details of all examples here, as well as an additional example of a linux
kernel bug can be found [4].
• Bluetooth Driver [25]. The Bluetooth device driver example [25], has an
arbitrary number of threads, working with a shared memory. We model this
using a 2-stack pushdown system, where a system state represents the current
valuation of the global variables, and the stacks are used to maintain the callreturn between different functions, as well as to keep track of context switches
between threads. A known error as pointed out in [25] is a race condition between
two threads where one thread tries to write to a global variable and the other
thread tries to read from it. BHIM found this error, with a well-nested witness.
A timed extension of this example was also considered, where, a witness was
obtained again with hole bound 0.
• Bluetooth Driver v2 [11,23]. A modified version of Bluetooth driver is considered [11,23], where a counter is maintained to count the number of threads
actively using the driver. We model this with a A two stack MPDA. With a wellnested witness, BHIM found the error of interrupted I/O, where the stopping
thread kills the driver while the other thread is busy with I/O.
• A Multi-threaded Producer Consumer Problem. The producer consumer problem (see e.g., [26]) is a classic example of concurrency and synchronization. An interesting scenario is when there are multiple producers and consumers. Assume that two ingredients called ’A’ and ’B’ are produced in a production line in batches (of M and N respectively). These parameters M and
N are fixed for each day but may vary across days. There is another consumer
machine that (1) consumes one unit of ’A’ and one unit of ’B’ in that order; (2)
repeats this process until all ingredients are consumed. In between if one of the
ingredients runs out, then we non-deterministically produce more batches of the
ingredient and then continue. To avoid wastage the factory aims to consume all
ingredients produced in a day, hence the problem of interest is to check if all
A’s and B’s produced in a day are consumed. We can model this factory using
a two-stack pushdown system, one stack per product, A, B, where the sizes of
the batches, M > 0 and N > 0 respectively, are parameters. The production
S. Akshay et al.
6 Implementation and Experiments
We implemented a tool BHIM (Bounded Holes In MPDA) in C++ based on
Algorithm 1, which takes an MPDA and a constant K as input and returns True
iff there exists a K-hole bounded run from the start state to an accepting state of
the MPDA. In case there is such an accepting run, BHIM generates one such, with
minimal number of holes. For a given hole bound K, BHIM first tries to produce
a witness with 0 holes, and iteratively tries to obtain a witness by increasing the
bound on holes till K. In most cases, BHIM found the witness before reaching
the bound K. Whenever BHIM’s witness had K holes, it is guaranteed that there
are no witnesses with a smaller number of holes.
To evaluate the performance of BHIM, we looked at some available benchmarks and modeled them as MPDA. We also added timing constraints to some
examples such that they can be modeled as TMPDA. Our tests were run on a
GNU/Linux system with Intel
R
Core
TM i7–4770K CPU @ 3.50GHz, and 16GB
of RAM. Details of all examples here, as well as an additional example of a linux
kernel bug can be found [4].
• Bluetooth Driver [25]. The Bluetooth device driver example [25], has an
arbitrary number of threads, working with a shared memory. We model this
using a 2-stack pushdown system, where a system state represents the current
valuation of the global variables, and the stacks are used to maintain the callreturn between different functions, as well as to keep track of context switches
between threads. A known error as pointed out in [25] is a race condition between
two threads where one thread tries to write to a global variable and the other
thread tries to read from it. BHIM found this error, with a well-nested witness.
A timed extension of this example was also considered, where, a witness was
obtained again with hole bound 0.
• Bluetooth Driver v2 [11,23]. A modified version of Bluetooth driver is considered [11,23], where a counter is maintained to count the number of threads
actively using the driver. We model this with a A two stack MPDA. With a wellnested witness, BHIM found the error of interrupted I/O, where the stopping
thread kills the driver while the other thread is busy with I/O.
• A Multi-threaded Producer Consumer Problem. The producer consumer problem (see e.g., [26]) is a classic example of concurrency and synchronization. An interesting scenario is when there are multiple producers and consumers. Assume that two ingredients called ’A’ and ’B’ are produced in a production line in batches (of M and N respectively). These parameters M and
N are fixed for each day but may vary across days. There is another consumer
machine that (1) consumes one unit of ’A’ and one unit of ’B’ in that order; (2)
repeats this process until all ingredients are consumed. In between if one of the
ingredients runs out, then we non-deterministically produce more batches of the
ingredient and then continue. To avoid wastage the factory aims to consume all
ingredients produced in a day, hence the problem of interest is to check if all
A’s and B’s produced in a day are consumed. We can model this factory using
a two-stack pushdown system, one stack per product, A, B, where the sizes of
the batches, M > 0 and N > 0 respectively, are parameters. The production