René Maseli
René Maseli
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...
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...
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...
This PR started as a rework for `FieldSensitiveAlias`. It now features a third implementation `InclusionBasedPointerAnalysis`. - It manages pointer modifiers of the type (`int` static offset‘,`List` dynamic offsets). This should...
Reduces the memory usage of the Relation Analysis. The initial knowledge of base relations like `ext`, `int`, `po` and `X*Y` is not explicitly stored. This comes with hopefully-negligible runtime costs.
This PR decouples an interface for `Dependency` and `UseDefAnalysis`, and adds an alternative implementation for it, `BackwardsReachingDefinitionsAnalysis` (BRDA). It takes into account, that readers on uninitialized registers are unlikely, while...
This PR extends the compile script for the Yices2j JNI-wrapper to support a Darwin-based system. The wrapper is statically linked with its dependencies to produce the single file `libyices2j.dylib`. I...
Removes two sources of non-determinism of the model checker: - Identity-based iteration order of phi nodes in the LLVM parser - Identity-based iteration order of relations in the memory model