Can Runtime Assertion Checking Work for Concurrency?

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.

Issues include:

1. An automated test generation strategy that is inherently single-threaded
2. No knob for exploring different schedules when executing the tests (byproduct of the first issue)
3. 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?