[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Has anyone tried using tla+ and clang for source level model checking?

TLA+ is a rich specification language used to design and reason about discrete systems. There is a model checker for TLA+ called TLC, but there are *many* model checkers for C, as well as other programming or specification languages. If you're interested in a code-level model checker, and not interested in writing specifications at all, there is little reason to use TLC. Just use a model checker for C. The reason some people are interested in compiling code to TLA+ is that they could reason about it at a higher level by use of refinement mappings. If that's not something that interests you, there is little reason to go through TLA+.

- Ron

On Tuesday, December 10, 2019 at 2:17:38 PM UTC, Chenkan Yu wrote:
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.

On Tue, Dec 10, 2019 at 5:07 AM Ron Pressler <ron.p...@xxxxxxxxx> wrote:
> There have been a few research project to verifying C and Java bytecode with TLA+, and there are, of course, quite a few model checkers for C (e.g. CPAChecker), but all approaches and all tools suffer from the same fundamental problem: we are limited in the scale of specification we can verify against arbitrary properties. We can either verify, say, 3000 lines of code or 3000 lines of a high-level spec representing a 100KLOC program, but we can't directly verify large programs (except for very simple, local properties, as sound static analyzers or type systems do). I think that, at least as far as mainstream software goes, people have found that there is more value in verifying high-level specs of large programs vs. verifying very small programs.
> For low-level code, you can look at the C2TLA work mentioned above, or, for something less research-grade, see this talk about using TLA+ to specify concurrent algorithms in the Linux kernel.
> - Ron
> On Saturday, December 7, 2019 at 11:41:22 PM UTC, imran...@xxxxxxxxx wrote:
>> I understand Tla+ is supposed to be above the code level. I  work mainly with finding issue with existing code base.
>> What I would do is read the code and abstract away non important part and build model in tla+.
>> I was wondering if any one has used tool like clang to extract relevant information from code like thread created, mutex and whatnot and try to show absent of any concurrent issue.
>> I would appreciate if any one has any lead and share their experience in this arena.
> --
> 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 tla...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ed675566-59be-4a55-acc9-878adeb0b66f%40googlegroups.com.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/423c8e80-49ef-474f-879b-e57e91e6bec4%40googlegroups.com.