27 Jan
2022
27 Jan
'22
8:47 a.m.
Hi, I'm building some automatons using spot's python interface. Simply,
codes like:
for i in n:
temp_aut = spot.automaton(aut.to_str()) # copy an automaton
...something
del temp_aut
But I found that whenever it enters a new loop, the memory of the automaton
assigned to temp_aut is not freed. And it leads to a memory overflow.
I thought this might be solved with 'delete temp_aut' in the C++ version
spot, but in the python interface 'del temp' doesn't seem to work.
Is there any interface in Python or other operations to make it possible?
27 Jan
27 Jan
5:30 p.m.
Yechuan Xia <xiaozi465(a)gmail.com> writes:
Hi, I'm building some automatons using
spot's python interface.
Simply, codes like:
for i in n:
temp_aut = spot.automaton(aut.to_str()) # copy an automaton
...something
del temp_aut
But I found that whenever it enters a new loop, the memory of the
automaton assigned to temp_aut is not freed. And it leads to a memory
overflow.
I thought this might be solved with 'delete temp_aut' in the C++
version spot, but in the python interface 'del temp' doesn't seem to
work.
Using "del temp_aut", or "temp_aut = None" should cause the
automaton's
destructor to be called, unless "...something" stores are reference to
that automaton somewhere.
Can you provide a test-case that demonstrates the problem?
I can't reproduce it from your example, trying something like:
for i in range(100):
newaut = spot.automaton(aut.to_str())
del newaut
print(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss)
I see that ru_maxrss is not growing.
28 Jan
28 Jan
4:25 a.m.
Thank you for your reply!
And I've found that it's not the memory of the automaton not being freed,
but the containers acquired by 'aut.out(i)' not being freed in
'...something'.
This problem can be solved by using aut.out_iteraser(i).
So I'm just wondering why there are two methods for getting out edges, and
aut.out(i) doesn't allow erasure? And it seems that the aut.out(i) method
is used by default in the spot's code examples.
On Fri, Jan 28, 2022 at 12:30 AM Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
wrote:
Yechuan Xia <xiaozi465(a)gmail.com> writes:
Hi, I'm building some automatons using
spot's python interface.
Simply, codes like:
for i in n:
temp_aut = spot.automaton(aut.to_str()) # copy an automaton
...something
del temp_aut
But I found that whenever it enters a new loop, the memory of the
automaton assigned to temp_aut is not freed. And it leads to a memory
overflow.
I thought this might be solved with 'delete temp_aut' in the C++
version spot, but in the python interface 'del temp' doesn't seem to
work.
Using "del temp_aut", or "temp_aut = None" should cause the
automaton's
destructor to be called, unless "...something" stores are reference to
that automaton somewhere.
Can you provide a test-case that demonstrates the problem?
I can't reproduce it from your example, trying something like:
for i in range(100):
newaut = spot.automaton(aut.to_str())
del newaut
print(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss)
I see that ru_maxrss is not growing.
10:58 a.m.
Yechuan Xia <xiaozi465(a)gmail.com> writes:
Thank you for your reply!
And I've found that it's not the memory of the automaton not being
freed, but the containers acquired by 'aut.out(i)' not being freed in
'...something'.
This problem can be solved by using aut.out_iteraser(i).
Please provide a small example to reproduce the problem so it can be
fixed. What you describe sound unexpected.
Adding
for i in newaut.out(0):
pass
to my previous example does not leak.
So I'm just wondering why there are two methods
for getting out
edges, and aut.out(i) doesn't allow erasure? And it seems that the
aut.out(i) method is used by default in the spot's code examples.
out_iteraser does not follow C++'s and Python's convention for
iteration, so it is a bit cumbersome to use. There are very few cases
where out_iteraser() is needed.
5:45 p.m.
On my machine, an example like this results in a leak:
aut = spot.translate(spot.formula('(F(p & X(p & Xh)) & G((!h | Xp) &
(!m |
X!p))) | (F(h & X!p) & G((!m | X!p) & (!p | X(!p | X!h))))'))
for i in range(100):
newaut = spot.automaton(aut.to_str())
for i in range(0, 10):
for t in newaut.out(i):
pass
del newaut
print(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss)
Indeed, the out_iteraser method is really a bit inconvenient to use ; )
On Fri, Jan 28, 2022 at 5:58 PM Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
wrote:
Yechuan Xia <xiaozi465(a)gmail.com> writes:
Thank you for your reply!
And I've found that it's not the memory of the automaton not being
freed, but the containers acquired by 'aut.out(i)' not being freed in
'...something'.
This problem can be solved by using aut.out_iteraser(i).
Please provide a small example to reproduce the problem so it can be
fixed. What you describe sound unexpected.
Adding
for i in newaut.out(0):
pass
to my previous example does not leak.
So I'm just wondering why there are two
methods for getting out
edges, and aut.out(i) doesn't allow erasure? And it seems that the
aut.out(i) method is used by default in the spot's code examples.
out_iteraser does not follow C++'s and Python's convention for
iteration, so it is a bit cumbersome to use. There are very few cases
where out_iteraser() is needed.
9 p.m.
Yechuan Xia <xiaozi465(a)gmail.com> writes:
On my machine, an example like this results in a
leak:
aut = spot.translate(spot.formula('(F(p & X(p & Xh)) & G((!h | Xp) &
(!m | X!p))) | (F(h & X!p) & G((!m | X!p) & (!p | X(!p | X!h))))'))
for i in range(100):
newaut = spot.automaton(aut.to_str())
for i in range(0, 10):
for t in newaut.out(i):
pass
del newaut
print(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss)
Indeed, the out_iteraser method is really a bit inconvenient to use ;
)
The attached example always print the same value for me, so no leak.
Do you see those values increasing?
Can you tell me more about your setup? What version of Spot do
you use ? did you build it yourself (and if so how), or did you use some
precompiled binaries ?
29 Jan
29 Jan
12:54 p.m.
The foo.py example prints increasing values for me. I attach the output.
I am using a WSL environment(Linux version 4.4.0-19041-Microsoft).
I use gcc version 9.3.0 to compile the tarball.
The Spot version I used was Spot-2.9.7, now I have updated to Spot-2.10.3
and they produce the same output.
On Sat, Jan 29, 2022 at 4:00 AM Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
wrote:
Yechuan Xia <xiaozi465(a)gmail.com> writes:
On my machine, an example like this results in a
leak:
aut = spot.translate(spot.formula('(F(p & X(p & Xh)) & G((!h | Xp) &
(!m | X!p))) | (F(h & X!p) & G((!m | X!p) & (!p | X(!p | X!h))))'))
for i in range(100):
newaut = spot.automaton(aut.to_str())
for i in range(0, 10):
for t in newaut.out(i):
pass
del newaut
print(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss)
Indeed, the out_iteraser method is really a bit inconvenient to use ;
)
The attached example always print the same value for me, so no leak.
Do you see those values increasing?
Can you tell me more about your setup? What version of Spot do
you use ? did you build it yourself (and if so how), or did you use some
precompiled binaries ?
3:17 p.m.
Hi everyone,
I think I can recreate the behaviour (wsl2, ubuntu 20.04, kernel
4.19.104-microsoft-standard).
I pumped the loop in foo.py from 100 to 10000 and the used ressource
climbs steadily from ~30k to 60k.
This happens under g++9.3 and clang++-12.
I'll investigate further when I have the time.
Best regards,
Philipp
Le 2022-01-29 12:54, Yechuan Xia a écrit :
The foo.py example prints increasing values for me. I
attach the
output.
I am using a WSL environment(Linux version 4.4.0-19041-Microsoft).
I use gcc version 9.3.0 to compile the tarball.
The Spot version I used was Spot-2.9.7, now I have updated to
Spot-2.10.3 and they produce the same output.
On Sat, Jan 29, 2022 at 4:00 AM Alexandre Duret-Lutz
<adl(a)lrde.epita.fr> wrote:
Yechuan Xia <xiaozi465(a)gmail.com> writes:
_______________________________________________
Spot mailing list -- spot(a)lrde.epita.fr
To unsubscribe send an email to spot-leave(a)lrde.epita.fr On my machine, an example like this results in a
leak:
aut = spot.translate(spot.formula('(F(p & X(p & Xh)) & G((!h | Xp)
&
(!m | X!p))) | (F(h & X!p) & G((!m | X!p)
& (!p | X(!p |
X!h))))'))
for i in range(100):
newaut = spot.automaton(aut.to_str())
for i in range(0, 10):
for t in newaut.out(i):
pass
del newaut
print(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss)
Indeed, the out_iteraser method is really a bit inconvenient to
use ;
)
The attached example always print the same value for me, so no leak.
Do you see those values increasing?
Can you tell me more about your setup? What version of Spot do
you use ? did you build it yourself (and if so how), or did you use
some
precompiled binaries ?
10:25 a.m.
Alexandre Duret-Lutz <adl(a)lrde.epita.fr> writes:
I'm looking into it.
The following patch seems to fix it:
https://gitlab.lrde.epita.fr/spot/spot/-/commit/a8cfcd2cc272166427dfdf90e25…
(You need to have Swig installed if you want to try this patch.)
I'll try to release 2.10.4 this week, even if that's the only fix.
I can't believe we never noticed this leak before...
1247
days inactive
1251
days old
9 comments
3 participants
participants (3)
-
Alexandre Duret-Lutz -
philipp -
Yechuan Xia