Embedded Systems Group (ES)

Testing Weak Memory Consistency Models

This tool can be used to check whether a given sequence of read/write actions of different threads is consistent with certain weak memory models. Each thread must be given a name (after keyword thread) and then the read/write actions of the thread follow. Actions consist of a label, a read/write action that specifies that an integer value is read from or written to a variable. In addition to the threads with their read/write actions, we can also list a couple of causality constraints w->r that assert that a write action w is the reason why a read action r reads the specified value.

Examples for execution sequences to demonstrate the differences of the various weak memory models are also available.