Dat3M
Dat3M copied to clipboard
hernanponcedeleon
A verification tool for many memory models
If CP is enabled, the assertion in [this benchmark](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/pthread-demo-datarace-2.c/c/pthread-C-DAC/pthread-demo-datarace-2.c) is completely removed, making the program trivially safe (which is not).
This PR is a massive restructuring of the package `com.dat3m.dartagnan.wmm`. It contains several interface changes. Be careful! ### Summary The following changes - ~~`PropertyEncoder` is now responsible of 'LastCoConstraints', since...
Right now, Dartagnan overapproximates the set of all possible addresses but to do so, it uses two assumptions: - There is a fixed and known number of mallocs - Each...
The following static fields are modified regularly and exhibit race conditions: - `solvers.caat.constraints.AcyclicityConstraint.SET_COLLECTION_POOL` - `solvers.caat.constraints.AcyclicityConstraint.TEMP_LIST` - `solvers.caat.misc.PathAlgorithm.queue1` and `queue2` - `solvers.caat.misc.PathAlgorithm.parentMap1` and `parentMap2` I recommend wrapping them with `ThreadLocal`.
Adds reusability to syntactic objects of the verification task, so that they may be used in a parallel environment. Implemented: - No instances of `Relation` or `Axiom` hold information that...
This PR adds a pass that simplifies the following types of code ``` lbl1; // Any jump to lbl1 can get forwarded to jump directly to lbl2 lbl2; ``` and...
Rcu-Sync should be treated as an await-loop, in order to model executions in programs that use it incorrectly, like [C-RW-GR+RW-R+RW-R](https://github.com/hernanponcedeleon/Dat3M/tree/master/litmus/LKMM/auto/C-RW-GR+RW-R+RW-R.litmus). The current encoding scheme applied to the linux-kernel memory model...
Code that contains multiple labels with the same name causes various problems: - The parsing generates bogus code if the same label name is used in _different_ threads. This should...
I took a look into the special events we generate for C-Litmus (Linux) tests as they do not compile to our internal LISA-like core language. These special events consist of...
We currently report a wrong result for this test ``` C C-atomic-cmpxchg-failure-02 { atomic_t x = ATOMIC_INIT(0); atomic_t z = ATOMIC_INIT(0); } P0(atomic_t *x, atomic_t *z) { int r0; int...
Metadata
Owner
Metadata
A verification tool for many memory models