Multithreaded reasoning

[Shea Levy]

Hi all,

Is it possible to prove properties about multithreaded programs, such as
"no deadlocks", with ATS's type system? Are there any examples if so?

~Shea

[Hongwei Xi]

Well, this is part of our ongoing research :)

Absence of deadlocks is a so-called liveness property(in contrast to
safety property). Termination is also a liveness property.

Types are usually used to capture safety properties; they are in general
not good for capturing liveness properties. We plan to incorporate into ATS

some form of model-checking for verifying liveness properties.

~Shea

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/20141004214250.GA2060%40nixos.hsd1.nh.comcast.net.

[Shea Levy]

Ah, cool! Do you have any pointers to papers about liveness properties
and model checking?

~Shea

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqxe0wtN8jhFZXkBcis49DDaAM9gDk%3D_gacHSJUD8QrKA%40mail.gmail.com.

[Yannick Duchêne]

Le dimanche 5 octobre 2014 00:18:28 UTC+2, Shea Levy a écrit :

Ah, cool! Do you have any pointers to papers about liveness properties
and model checking?

~Shea

On Sat, Oct 04, 2014 at 05:57:09PM -0400, Hongwei Xi wrote:
> Well, this is part of our ongoing research :)
>
> Absence of deadlocks is a so-called liveness property(in contrast to
> safety property). Termination is also a liveness property.
>
> Types are usually used to capture safety properties; they are in general
> not good for capturing liveness properties.

Even with constructive logic? Constructive logic is known to be good at handling termination. Or may be it's not really or it is specifically not the case any‑more with locking?

 

[Yannick Duchêne]

As words matters: so this is precisely about concurrency (threading is too wide / broad)

[Hongwei Xi]

Right now there isn't anything formally written yet. Maybe in a year or two.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/20141004221821.GA2263%40nixos.hsd1.nh.comcast.net.

[Hongwei Xi]

>>Constructive logic is known to be good at handling termination

Usually it goes like this:

Every program written in some constructive logic (such as System F)
is terminating but it is very difficult to write practical programs in that logic.

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/d9c4b8c9-a152-4afd-aff4-0baf089aad25%40googlegroups.com.

[Zhiqiang Ren]

I think it's relatively easy to prove that a system would enter a certain state (termination). But it's difficult to prove that a system would not enter a certain state (no deadlock).