Hernan Ponce de Leon
Hernan Ponce de Leon
- [ ] fflush - [ ] fprintf - [x] llvm.smul.with.overflow.i32, llvm.smul.with.overflow.i64 - [ ] strerror - [ ] time - [ ] __isoc99_scanf - [ ] ffs - [...
Our alias analysis is very slow when run on [this program](https://github.com/hernanponcedeleon/Dat3M/files/10474776/client-code-opt.zip). These are the times I get (running this requires `GlobalSettings.ARCH_PRECISION = 64`) ``` [22.01.2023] 16:43:34 [INFO] AliasAnalysis.fromConfig - Selected...
There seem to be some subtle issues with the Release-Acquire tags of LR and SC instructions in RISC-V (see [this](https://github.com/herd/herdtools7/pull/576) and [this](https://github.com/herd/herdtools7/pull/577)). We need to be sure that we are...
The following litmus test has a trivial deadlock ``` C lock { } P0(int *a, int *b, spinlock_t *l) { spin_lock(l); WRITE_ONCE(*a, 1); } P1(int *a, int *b, spinlock_t *l)...
Some tools (cseq, deagle, infer) generate "violation witnesses" even if they report that the program is safe. Some witnesses (deagle) do not have a violation state so we might avoid...
We are getting some counter intuitive behaviors related to non-atomic accesses and rmw. Consider this example // Both read-modify-write instructions read the value stored by a non-atomic write instruction preceding...
I'm working on extending Dartagnan for validation (currently with emphasis in violation witnesses for concurrency reachability where we only have one validator) and I have a couple of questions about...
This PR updates JavaSMT to the latest version and adds support for the new bitwuzla solver. I did some basic performance testing for bitwuzla and it does not look good...