University of Utah
School of Computing


NemosFinder is a tool that implements the techniques of the Nemos (Non-Operational yet Executable Memory Ordering Specification) framework. It uses Prolog to encode the memory model constraints. With the built-in finite domain constraint solver from Prolog, this tool provides an incremental and interactive testing environment for analyzing multithreaded programs under a given memory model. Users can selectively disable/enable certain constraints to study their implications. Alternatively, the overall memory ordering requirement can be generated as a propositional formula and a SAT solver can be used to find the result.

          Source Code (GNU version), Source Code (SICStus version).

          Source Code. (Both zChaff and berkmin have been used as our SAT engines.)

School of Computing • 50 S. Central Campus Dr. Rm. 3190 • Salt Lake City, UT 84112
801-581-8224 • Send comments to

Home People Research Admissions Site Map