Verifying Atomicity-violation Fixes For Concurrent Programs

An existing study reported that 66% non-deadlock Heisenbugs are known as atomicity violation,which means that the isolation of a work unit(i.e.,a sequence of related events in a thread)is destroyed by events from other threads.However,ensuring atomicity is often very challenging due to complex thread interactions.In practice,to ensure atomicity,it is very easy to introduce insufficient synchronization and privatization,because developers usually cannot fully understand a concurrency bug and are not aware of what code area they should preserve the property of atomicity.In the thesis,we present an approach to verifying whether an atomicity violation has been sufficiently fixed by either synchronization or privatization.In the thesis,we firstly present our large-scale empirical study on atomicity violation and its fixing methods in practice.Via the investigation on the bug databases of open-source software,the empirical study summarize the methods of fixing concurrency bugs in practice as well as the reason why it is difficult to correctly fix concurrency bugs.These findings sets a practical foundation for the verification method proposed in the paper.Our approach takes the advantage of exiting advances of record and reply techniques.Before a bug is fixed,we can always reproduce the bug according to the recorded thread interleaving information.If a bug is correctly fixed,we then cannot reproduce the buggy thread interactions any more.According to this observation,in our approach,we generate suspicious thread interactions according to the recorded bugtriggering thread-interleaving information,so that we can easily trigger the bug again if it is not correctly fixed.A key feature of our approach is that it combines the fortes of both bug-driven and change-aware techniques,which enables it to effectively verify fixes by testing only a minimal set of suspicious atomicity violations.Our approach also provides guidance on how to select program inputs in addition to investigating how to schedule threads.This is necessary because testing a concurrent program also needs diversified program inputs to run the program.To the end,we provide a simple but very effective methods to select a small but sufficient subset of test inputs.The core of this test selection technique is a measurement called ”distance entropy”,which measures the sufficiency of a test set based on the observation of”diversity”.We demonstrate via extensive evaluation that our approach is much more effective and efficient than the state of the arts.Meanwhile,we show that although there have existed sound automatic fixing techniques for atomicity violations,our approach is still necessary and useful for quality assurance of concurrent programs,because the assumptions behind our approach are much weaker.