Memory model verification tools

  • Promela + mmlib + trio additions
    • Promela is architecture-agnostic so this is quite a stretch
  • c11tester-llvm
    • unmaintained
    • the pass can be compiled against llvm8
      • rumored to compile angainst llvm11 but I could not
      • there is an llvm12 branch; I have not tried it
      • seems to be possible to compile it as an out-of-tree but I have not tried it
      • llvm17 and later has a new pass manager - this would be the end of life for the c11tester pass
  • cdschecker
    • prefer relacy; too many false positives (see the shared_mutex tests)
    • useable but not with coroutines
    • original is unmaintained
  • relacy
    • to be preferred over other tools
    • still maintained: dvyukov and ccotter
    • dated codebase but useable
  • genmc
    • maintained
    • llvm C11 only
  • cppmem
  • nitpick
Written on September 6, 2024