6 ms·
It would be interesting to see this interact with the lower-level ISA memory model work in diy, litmus, etc. Could you validate your ISA memory models against
by sdbbp 2y ago
It would be interesting to see this interact with the lower-level ISA memory model work in diy, litmus, etc. Could you validate your ISA memory models against the generated litmus tests in https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test6.pdf https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test6.pdf, https://github.com/litmus-tests/litmus-tests-riscv https://github.com/litmus-tests/litmus-tests-riscv?
- reitzensteinm 2y agoIt should be quite possible to validate this way, although I would need to implement more ISA specific fences and features. As mentioned in a sibling comment, I've moved away from the idea of building a model in Clojure and implementing separately, to a system in Rust where the model is the program with a compile time switch. There were too many ways to introduce careless errors when doing a port. Although the opposite approach would have been to ingest compiled programs directly, or move to something higher level like WASM (once it gets more than SeqCst atomics).