I'm also very interested in this topic. I'm working on a project that
may achieve similar checking at C/assembly level for the concurrent
issue. I don't have much experience in using TLA+, so kindly correct
me if I'm wrong.
The goal for my project is not to translate the C code into
specification language, but to explore the state by executing the
binary directly. It has very strong connection with deterministic
record/replay, and this is also the first step I want to achieve and
partially done.
The project is initially designed to be comprehensive. I hope it can
cope with different kind of softwares on Linux-x86-64 platform. Along
with other decisions, this makes the implementation very complicated,
but for a controlled code base, I believe it can be much easier.
From my understanding, the state space exposed by TLA+ represents the
different interleaving of the contexts. At C level, it represents the
different order of acquiring the locks among threads. At assembly
level, it means the different order of accessing the shared memory.
Therefore, by replacing the locks or the atomic instructions with an
implementation that allow you to pick the next thread to acquire or
access, you will be able to enumerate different states of the
execution. You may also add the assertions to check properties during
the exploration. I believe all this can be done all by modifying the
source code if you don't have to check for the undefined behavior. I
thinks this approach shows very strong similarity to TLA+, and it has
very good potential in preventing the state explosion as this may
match very well with the model developers use.
The project is at
https://github.com/yuchenkan/ers, but it's still
very far away from what I stated above.
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/ed675566-59be-4a55-acc9-878adeb0b66f%40googlegroups.com.