Monitors: Automated Reasoning.

Argonne has long been in the forefront of automated reasoning research. The parallelization of our primary theorem prover presented a particular problem because of its central shared data structures. The tight interweaving of indices and shared substructures makes this an intrinsically shared-memory application. We used p4's shared-memory operations, in particular the p4_askfor monitor, to implement the algorithm presented in [26] and got excellent results [20], even for the very fine-grained parallelism necessary for this application. We developed it on a Sequent Symmetry and ran it for peak performance on an Alliant FX/2800.