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
Ah, cool! Do you have any pointers to papers about liveness properties
and model checking?
~SheaOn 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. We plan to incorporate into ATS
some form of model-checking for verifying liveness properties.On Sat, Oct 4, 2014 at 5:42 PM, Shea Levy sh...@shealevy.com wrote:
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
–
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
.–
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/CAPPSPLqxe0wtN8jhFZXkBcis49DDaAM9gDk%3D_gacHSJUD8QrKA%40mail.gmail.com.
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).On Saturday, October 4, 2014 7:57:20 PM UTC-4, Yannick Duchêne wrote:
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?
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.On Sat, Oct 4, 2014 at 5:42 PM, Shea Levy sh...@shealevy.com wrote:
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
–
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
.
Ah, cool! Do you have any pointers to papers about liveness properties
and model checking?~Shea
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?
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.On Sat, Oct 4, 2014 at 7:57 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
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?–
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
https://groups.google.com/d/msgid/ats-lang-users/d9c4b8c9-a152-4afd-aff4-0baf089aad25%40googlegroups.com?utm_medium=email&utm_source=footer
.
Right now there isn’t anything formally written yet. Maybe in a year or two.On Sat, Oct 4, 2014 at 6:18 PM, Shea Levy sh...@shealevy.com wrote:
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. We plan to incorporate into
ATS
some form of model-checking for verifying liveness properties.On Sat, Oct 4, 2014 at 5:42 PM, Shea Levy sh...@shealevy.com wrote:
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
–
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 visithttps://groups.google.com/d/msgid/ats-lang-users/20141004214250.GA2060%40nixos.hsd1.nh.comcast.net
.
–
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/CAPPSPLqxe0wtN8jhFZXkBcis49DDaAM9gDk%3D_gacHSJUD8QrKA%40mail.gmail.com
.–
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/20141004221821.GA2263%40nixos.hsd1.nh.comcast.net
.
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
As words matters: so this is precisely about concurrency (threading is too
wide / broad)