NemosFinder

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.

• The implementation of the Itanium memory model is written in both GNU Prolog and SICStus Prolog: 

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

• The SAT instance generator is written in SICStus Prolog: 

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

• Specifications of SC, Coherence, PRAM, Causal Memory, and Processor Consistency: 

  Source Code (SICStus Prolog version)