Handle more inputs

[margnus1]

• [ ] Mutexes
• [x] Compare-exchange
• [x] Atomic RMW

[margnus1]

For Atomic RMW, we don't need any new saturation rules or SMT encodings, just refactor the code so that a single event can be both a read and a write, correct?

[PhongNgo]

I think that we do not need new saturation rules. But when we generate new executions, the code for calculating the causal cons should cover RMW case.

You can check with some tests. For example, I will test with 2 tests:

Test 1: / 6 weak traces / T1: RMW(x,1) T2: RMW(x.2) T3: RMW(x,3)

Test 2: / 5 weak traces / T1: CAS(x,0,1) T2: CAS(x,1,2) T3: CAS(x,2,3)

I will put more tests to GitHub when I commit.

[margnus1]

c29be43e0d7 implemented possibly working RMW support, mutexes and CAS still pending but should be easier (touch wood).

[margnus1]

Mutexes might be hard in general with our current RMW exploration strategy; consider (two threads concurrently executing) this:

void critical_section() {
    pthread_mutex_lock(&m);
    if (atomic_fetch_add(&x, 1) == tid)
        pthread_mutex_unlock(&m);
}

When we try to "reverse" the two RMWs, we are fundamentally unable to predict the appearance of the second RMW, since it might not (and does not, in this example) appear at all due to deadlock or more writes to x before the mutex is unlocked.

[margnus1]

Phong, Faouzi, and I decided that the best course of action is to abandon the idea of having no coherence order on mutex aquisition and instead start by implementing totally ordered mutex aquisitions. This makes implementing mutexes much easier, and is actually what competing techniques, like DCDPOR, are doing right now. I will update count-weak-traces to count these finer (i.e. more numerous) equivalence classes.