Linear types + Exceptions

[aditya siram]

Is the linear type system exception safe, i.e can exceptions be safely thrown without the GC? For example, in the tutorial (http://ats-lang.github.io/DOCUMENT/ATS2TUTORIAL/HTML/c625.html) the found element `x` is thrown with `Found(x)`. How would this example change if `xs` was a viewtype?
Thanks!
-deech

[Richard]

Hello Aditya,

I know this is not identical but checkout this example,
https://github.com/githwxi/atslangweb/blob/master/ats2-lang/doc/EXAMPLE/INTRO/sieve_llazy.dats#L53

The tilde tells the compiler to free the empty stream in this example.

Is this similar to what you have in mind?

[aditya siram]

Hi,
That is closer but what I had in mind is what happens with an exception carries a linear resource, so in that example, imagine the exception was on the '~(x :: xs)' case and looked something like '$raise Exception(x)'. Here 'x' of type 'a' must be consumed whenever the exception is handled. My question is if the linear type system detects such cases.

[aditya siram]

This program for instance compiles:

exception MyException of (list_vt(int))

fun test(l : list_vt(int)): void =
    $raise MyException(l)

implement main0(argc,argv) =
  test(list0_vt_cons(1,list0_vt_nil()))

but results in:

exit(ATS): uncaught exception at run-time:

I expect that but would also have expected that the type system would require me to free 'l' at some point.

[aditya siram]

Valgrind shows a memory leak:

==465== Memcheck, a memory error detector
==465== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==465== Using Valgrind-3.14.0 and LibVEX; rerun with -h for copyright info
==465== Command: ./test
==465==

exit(ATS): uncaught exception at run-time:

test.dats:MyException(1024)
==465==
==465== HEAP SUMMARY:
==465==     in use at exit: 40 bytes in 2 blocks
==465==   total heap usage: 2 allocs, 0 frees, 40 bytes allocated
==465==
==465== LEAK SUMMARY:
==465==    definitely lost: 24 bytes in 1 blocks
==465==    indirectly lost: 0 bytes in 0 blocks
==465==      possibly lost: 0 bytes in 0 blocks
==465==    still reachable: 16 bytes in 1 blocks
==465==         suppressed: 0 bytes in 0 blocks
==465== Rerun with --leak-check=full to see details of leaked memory
==465==
==465== For counts of detected and suppressed errors, rerun with: -v
==465== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)

[Chris Double]

On Fri, Jun 21, 2019 at 6:41 AM aditya siram <aditya...@gmail.com> wrote:
>
> Valgrind shows a memory leak:

Unfortunately exceptions and linear types do not mix. There is no
compile time checking that linear types are consumed when an exception
is thrown. For this reason I avoid exceptions in non-GC code.

--
https://bluishcoder.co.nz

[Hongwei Xi]

Yes, raising exceptions may result in resource being leaked.

Speaking of implementation, raising an exception means jumping from

one stack location to another; and all the linear resources between these two

locations are leaked.

--
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 https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6ba9272d-424a-431f-b33e-482483653b23%40googlegroups.com.

[Raoul Duke]

Worthy of being a faq type entry? High level question would be, under what-all conditions do we hit such potential leaks?

[aditya siram]

Cool, that's good to know.

My follow up question: even if I did handle the exception how do I free the resource? The following doesn't work:

exception MyException of (list_vt(int))

fun test(l : list_vt(int)): void =
    $raise MyException(l)

implement main0(argc,argv) =

  try
    test(list0_vt_cons(1,list0_vt_nil()))
  with
    ~MyException(l) => free l

[Hongwei Xi]

What is the issue you are having with the code?

--

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 https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/366889e9-e88b-471f-8237-92b3c86923d4%40googlegroups.com.

[Richard]

Did you use the flag, -D_GNU_SOURCE ?

[Richard]

On Thursday, June 20, 2019 at 7:38:57 PM UTC-4, Raoul Duke wrote:
> Worthy of being a faq type entry? High level question would be, under what-all conditions do we hit such potential leaks?

When the linear resource is not freed before calling 'exit', unhandled exceptions, and unsafe casts.

From what I understand exit is akin to a backdoor. It inherits the return value of an expression. In other words, exit can be any type. I assume that unhandled exceptions are treated similarly.

[aditya siram]

Yes you're right that does work, I had to do:

%{
  #include <alloca.h>
%}
#include "share/HATS/temptory_staload_bucs320.hats"

exception MyException of (list_vt(int))

fun test(l : list_vt(int)): void =
    $raise MyException(l)

implement main0(argc,argv) =

  try
    test(list0_vt_cons(1,list0_vt_nil()))
  with
    ~MyException(l) => free l