1. Add
#include <relacy/relacy_std.hpp>

2. For atomic variables use type std::atomic<T>:
std::atomic<void*> head;

3. For usual non-atomic variables use type rl::var<T>:
rl::var<int> data;
Such vars will be checked for races and included into trace.

4. All accesses to std::atomic<T> and rl::var<T> variables postfix with '($)':
std::atomic<void*> head;
rl::var<int> data;
head($).store(0);
data($) = head($).load();

5. Strictly thread-private variables use can leave as-is:
for (int i = 0; i != 10; ++i)
Such vars will be NOT checked for races NOR included into trace. But they will accelerate verification.

6. Describe test-suite: number of threads, thread function, before/after/invariant functions. See example below.

7. Place asserts:
int x = g($).load();
RL_ASSERT(x > 0);

8. Start verification:
rl::simulate<test_suite_t>();

Here is complete example:

#include <relacy/relacy_std.hpp>

// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
    std::atomic<int> a;
    rl::var<int> x;

    // executed in single thread before main thread function
    void before()
    {
        a($) = 0;
        x($) = 0;
    }

    // main thread function
    void thread(unsigned thread_index)
    {
        if (0 == thread_index)
        {
            x($) = 1;
            a($).store(1, rl::memory_order_relaxed);
        }
        else
        {
            if (1 == a($).load(rl::memory_order_relaxed))
                x($) = 2;
        }
    }

    // executed in single thread after main thread function
    void after()
    {
    }

    // executed in single thread after every 'visible' action in main threads
    // disallowed to modify any state
    void invariant()
    {
    }
};

int main()
{
    rl::simulate<race_test>();
}