Abstract

Many runtime assertion checkers are only built for sequential programs and do not guarantee correct behaviour if they are used in a multithreaded environment. We will show that runtime assertion checkers in a multithreaded environment can sometimes report errors that do not exist in the program or fail to detect problems that exist, both of which is problematic. To solve this problem, we build an extension to the STROBE framework. STROBE is built to accelerate runtime assertion checking with the use of asynchronous assertions: checks that are executed in parallel to the program itself. This framework performs this checking correctly with the use of snapshots, that evaluatesciently save the previous states of a program. We extend the STROBE framework into the e-STROBE framework, that uses these snapshots in a multithreaded program, to protect the program from unwanted interference during runtime assertion checking. We apply the snapshots in the e-STROBE framework to OpenJML, to show that existing runtime assertion checkers can be modified to work correctly in a multithreaded environment. We will give several examples to show that our solution works, and gives the expected results in both single-threaded and multithreaded programs.

Additional Resources

1. The paper