Re: performance considerations of patsopt

2020-11-28 Thread Dambaev Alexander 
In case if someone will hit the same issue: there was an option to dig into
source code of patscc and to try to speed up constraint solving, but for
now I am not too confident in ATS to perform that, so instead, I had
splitted my function on 2 separate parts, like this:
the original function's type (after the first simplification of
constraints) was:
```
fn
appendC
{l_len, l_offset, l_cap, l_ucap: nat}{l_dynamic:bool}{l_p:addr}
{r_len, r_offset, r_cap, r_ucap: nat}{r_dynamic:bool}{r_p:addr}
( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, 0, l_dynamic, l_p)
, r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, r_dynamic, r_p)
):
[offset, cap, ucap: nat | (l_len > 0 || r_len > 0) && (cap > 0)]
[l:addr | l > null]
[dynamic:bool]
[l:addr | (l_len > 0 || r_len > 0) && l > null]
Bytestring_vtype( l_len+r_len, offset, cap, ucap, 0, dynamic, l)

overload + with appendC
```
which means, that in different cases the result will be different, so I had
decided to have 2 separate functions:
1. for creating new buffer
```
fn
  appendC
  {l_len, l_offset, l_cap, l_ucap: nat | *l_len > 0*}{l_dynamic:bool}
*{l_p:agz*}
  {r_len, r_offset, r_cap, r_ucap: nat | *r_len > 0*}{r_dynamic:bool}{
*r_p:agz*}
  ( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, 0, l_dynamic, l_p)
  , r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, r_dynamic, r_p)
  ):
  *[l:addr | l > null]*
  Bytestring_vtype( l_len+r_len, 0, l_len+r_len, 0, 0, true, *l*)

overload + with appendC

```
2. for filling unused parts of buffer
```
(* O(r_len)
 this function appends 'r' at the end of 'l''s unused buffer.
 See test17 for example of usage.\
 this usage does not perform allocation, but does consumes 'r', so it will
call 'free' in case if 'r' had been dynamically allocated.
 *)
fn
  growC
  {r_len, r_offset, r_cap, r_ucap, l_refcnt: nat | *r_len > 0*
}{r_dynamic:bool}{*r_p:agz*}
  {l_len, l_offset, l_cap, l_ucap: nat | *l_ucap >= r_len*
}{l_dynamic:bool}{*l_p:agz*}
  ( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, l_refcnt,
l_dynamic, l_p)
  , r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, r_dynamic, r_p)
  ):
  Bytestring_vtype( l_len+r_len, l_offset, l_cap, l_ucap - r_len, l_refcnt,
l_dynamic, l_p)

symintr ++
infixl (+) ++
overload ++ with growC
```
so by limiting the usage cases and splitting 1 function on 2, I was able to
get rid of excessive constraints on output and now I get reasonable
compilation time of user's code. Plus the caller now is able to explicitly
choose the behavior of appending: either to create new buffer or use unused
part of some existing buffer.

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kwv3HCUr8hPvM92OnMvBXib1YXsrURtqB7nPkOp4FCDHQ%40mail.gmail.com.

Re: performance considerations of patsopt

2020-10-04 Thread Dambaev Alexander 
Thanks for your answer.

with --constraint-ignore flag compilation is fast. At the same time, I am
not sure if disabling of constraint solving is reasonable in the sense,
that constraints are there in order to be checked :)

I guess, I should try to refactor in order to keep SATS file clean from too
many constraints and move them into DATS file, so only this file will take
long time to compile


вс, 4 окт. 2020 г. в 13:05, Hongwei Xi :

> In this case, the long time compilation of your ATS code is most likely
> caused
> by constraint-solving. You may try to use the following flag to skip
> constraint-solving:
>
> --constraint-ignore
>
> This will tell you if constraint-solving is indeed the culprit here.
>
> Using an external constraint-solver like Z3 may improve. However,
> constraint-solving
> is inherently of exponential-time.
>
>
>
> On Sun, Oct 4, 2020 at 8:15 AM Dambaev Alexander 
> wrote:
>
>> Hi,
>> I have noticed, that patsopt takes huge amount of time, to compile
>> relatively small library https://github.com/dambaev/ats-bytestring
>>
>> ``
>> [nix-shell:/data/devel/ats2/bytestring]$ $(which time) make test1
>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o SATS/bytestring_sats.o
>> SATS/bytestring.sats
>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o
>> DATS/bytestring_flat_dats.o DATS/bytestring_flat.dats
>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test1
>> SATS/bytestring_sats.o DATS/bytestring_flat_dats.o TEST/test1.dats
>> 39.00user 0.43system *0:39.44*elapsed 99%CPU (0avgtext+0avgdata *215060*
>> maxresident)k
>> 0inputs+1024outputs (0major+140589minor)pagefaults 0swaps
>> ```
>>
>> and one project, that uses this library take forever to compile:
>>
>> ```
>> $ $(which time) make
>> make -C src
>> make[1]: Entering directory '/data/devel/smartplants/lora2mqtt/src'
>> patscc -O2 -DATS_MEMALLOC_LIBC
>> -I"/nix/store/cqynqsas6nwk3gbn8m2pi9lx4m0shr0y-ats2-0.3.13/lib/ats2-postiats-0.3.13/contrib/atscntrb/"
>> -I"../libs/" -c -o DATS/logging_dats.o DATS/logging.dats
>> /data/devel/smartplants/lora2mqtt/src/DATS/logging.dats: 3255(line=92,
>> offs=24) -- 3255(line=92, offs=24): error(3): unsolved constraint:
>> C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>);
>> S2EVar(5345->S2Evar(refcnt$8767$8777$8786$8794$8801$8807$8812$8816$8819(14823))),
>> S2Eintinf(0)))
>> ^Cmake[1]: *** [Makefile:71: DATS/logging_dats.o] Error 1
>> make: *** [Makefile:2: all] Interrupt
>> Command terminated by signal 2
>> 202.80user 0.28system *3:23.13*elapsed 99%CPU (0avgtext+0avgdata *384768*
>> maxresident)k
>> 0inputs+0outputs (0major+97710minor)pagefaults 0swaps
>>
>> $ cat src/DATS/logging.dats | wc -l
>> 120
>> ```
>> I had interrupted when the first error had been reported.
>>
>> What are the best practice to get reasonable performance of patsopt?
>>
>> --
>> 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-users+unsubscr...@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwdMZNSdJhtypDjpZyLDfqR2zZpca8LH-81UYyrk4UMzQ%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-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoy0jdo884-_JD%3DmHLdad7ytsSiWg%2BMsGjp5iH9BM2Yng%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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Ky73E1QY_tLSwfUtQf7oiuw9D34QEG1hq-JLXtvT%3DeY_Q%40mail.gmail.com.

Re: performance considerations of patsopt

2020-10-04 Thread Hongwei Xi 
In this case, the long time compilation of your ATS code is most likely
caused
by constraint-solving. You may try to use the following flag to skip
constraint-solving:

--constraint-ignore

This will tell you if constraint-solving is indeed the culprit here.

Using an external constraint-solver like Z3 may improve. However,
constraint-solving
is inherently of exponential-time.



On Sun, Oct 4, 2020 at 8:15 AM Dambaev Alexander 
wrote:

> Hi,
> I have noticed, that patsopt takes huge amount of time, to compile
> relatively small library https://github.com/dambaev/ats-bytestring
>
> ``
> [nix-shell:/data/devel/ats2/bytestring]$ $(which time) make test1
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o SATS/bytestring_sats.o
> SATS/bytestring.sats
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o
> DATS/bytestring_flat_dats.o DATS/bytestring_flat.dats
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test1
> SATS/bytestring_sats.o DATS/bytestring_flat_dats.o TEST/test1.dats
> 39.00user 0.43system *0:39.44*elapsed 99%CPU (0avgtext+0avgdata *215060*
> maxresident)k
> 0inputs+1024outputs (0major+140589minor)pagefaults 0swaps
> ```
>
> and one project, that uses this library take forever to compile:
>
> ```
> $ $(which time) make
> make -C src
> make[1]: Entering directory '/data/devel/smartplants/lora2mqtt/src'
> patscc -O2 -DATS_MEMALLOC_LIBC
> -I"/nix/store/cqynqsas6nwk3gbn8m2pi9lx4m0shr0y-ats2-0.3.13/lib/ats2-postiats-0.3.13/contrib/atscntrb/"
> -I"../libs/" -c -o DATS/logging_dats.o DATS/logging.dats
> /data/devel/smartplants/lora2mqtt/src/DATS/logging.dats: 3255(line=92,
> offs=24) -- 3255(line=92, offs=24): error(3): unsolved constraint:
> C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>);
> S2EVar(5345->S2Evar(refcnt$8767$8777$8786$8794$8801$8807$8812$8816$8819(14823))),
> S2Eintinf(0)))
> ^Cmake[1]: *** [Makefile:71: DATS/logging_dats.o] Error 1
> make: *** [Makefile:2: all] Interrupt
> Command terminated by signal 2
> 202.80user 0.28system *3:23.13*elapsed 99%CPU (0avgtext+0avgdata *384768*
> maxresident)k
> 0inputs+0outputs (0major+97710minor)pagefaults 0swaps
>
> $ cat src/DATS/logging.dats | wc -l
> 120
> ```
> I had interrupted when the first error had been reported.
>
> What are the best practice to get reasonable performance of patsopt?
>
> --
> 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-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwdMZNSdJhtypDjpZyLDfqR2zZpca8LH-81UYyrk4UMzQ%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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoy0jdo884-_JD%3DmHLdad7ytsSiWg%2BMsGjp5iH9BM2Yng%40mail.gmail.com.

performance considerations of patsopt

2020-10-04 Thread Dambaev Alexander 
Hi,
I have noticed, that patsopt takes huge amount of time, to compile
relatively small library https://github.com/dambaev/ats-bytestring

``
[nix-shell:/data/devel/ats2/bytestring]$ $(which time) make test1
patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o SATS/bytestring_sats.o
SATS/bytestring.sats
patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o
DATS/bytestring_flat_dats.o DATS/bytestring_flat.dats
patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test1 SATS/bytestring_sats.o
DATS/bytestring_flat_dats.o TEST/test1.dats
39.00user 0.43system *0:39.44*elapsed 99%CPU (0avgtext+0avgdata *215060*
maxresident)k
0inputs+1024outputs (0major+140589minor)pagefaults 0swaps
```

and one project, that uses this library take forever to compile:

```
$ $(which time) make
make -C src
make[1]: Entering directory '/data/devel/smartplants/lora2mqtt/src'
patscc -O2 -DATS_MEMALLOC_LIBC
-I"/nix/store/cqynqsas6nwk3gbn8m2pi9lx4m0shr0y-ats2-0.3.13/lib/ats2-postiats-0.3.13/contrib/atscntrb/"
-I"../libs/" -c -o DATS/logging_dats.o DATS/logging.dats
/data/devel/smartplants/lora2mqtt/src/DATS/logging.dats: 3255(line=92,
offs=24) -- 3255(line=92, offs=24): error(3): unsolved constraint:
C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>);
S2EVar(5345->S2Evar(refcnt$8767$8777$8786$8794$8801$8807$8812$8816$8819(14823))),
S2Eintinf(0)))
^Cmake[1]: *** [Makefile:71: DATS/logging_dats.o] Error 1
make: *** [Makefile:2: all] Interrupt
Command terminated by signal 2
202.80user 0.28system *3:23.13*elapsed 99%CPU (0avgtext+0avgdata *384768*
maxresident)k
0inputs+0outputs (0major+97710minor)pagefaults 0swaps

$ cat src/DATS/logging.dats | wc -l
120
```
I had interrupted when the first error had been reported.

What are the best practice to get reasonable performance of patsopt?

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwdMZNSdJhtypDjpZyLDfqR2zZpca8LH-81UYyrk4UMzQ%40mail.gmail.com.