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

[Chenkan Yu <yuchenkan@xxxxxxxxx>]

Thanks for pointing out the refinement mapping. I'm not aware of that before.

On Tue, Dec 10, 2019 at 10:23 PM Ron Pressler <ron.pressler@xxxxxxxxx> wrote:
>
> 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...@xxxxxxxxxxxxxxxx.
>> > 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.

-- 
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/CAPJ174ohNrgwXLtCRGKGYq1qcfW27PC7SfJ5vvucMKk6-8QMKg%40mail.gmail.com.