I was reading this article Programs that Test Themselves in Computer magazine (unfortunately, link requires payment to access... Bertrand Meyer has a different but equally fascinating fascinating article which is now free to access: Seven Principles of Software Testing), and noticed that once again, the testing strategy described doesn't work out of the box for concurrent software.
The article describes an end-to-end scenario for automated+manual testing called AutoTest. It has an automated test generation strategy, a mechanism to run these automatically generated tests, and a way to automatically check the tests (pass/fail). They use the trick of runtime assertion checking of postconditions as an oracle (a technique I also used in my thesis). They paint a very attractive picture of testing that fully integrated automated and manually written unit tests that can check their own correctness. Problem is, it doesn't *quite* work for concurrent software.
- An automated test generation strategy that is inherently single-threaded
- No knob for exploring different schedules when executing the tests (byproduct of the first issue)
- Runtime assertion of postconditions don't work in concurrent systems.
The first issue is probably easy to fix, one can imagine a variant of their test generation strategy but on multiple threads. The second can be fixed by running a test multiple times, each with a different thread schedule such as the CHESS tool does. But the last one is quite problematic.
AutoTest relies on the fact that you can evaluate design-by-contract postconditions at runtime to see whether they hold or not. But in concurrent systems, DBC runtime checking is a lot more tricky. Imagine that you have a simple concurrent stack type that had a Push() method: a typical postcondition for a stack would assert that after the Push(), the size of the stack grew by one element. But what if there was a Pop() running concurrently with the Push()--it is now possible that by the time the Push method returns, the stack did not grow at all!
I kind of recall a JML related paper where they try to solve this by putting in safe points--locations inside the code where pre- and postconditions can be checked safely. It wasn't clear to me that this is doable in general. Plus, we now have to muddy the implementation with contract stuff--which isn't very clean at all.
The idea of self-checking software components is certainly very appealing to me, but how do we make it work for concurrency components? Can we make dbc-style runtime checking work? Or do we need something else?