Hi,

can I login to your account and try to reproduce the problem?

Kind Regards, H.-J. Schnitzer

On 3/3/19 8:52 PM, Gereon Kremer wrote:

Hi,

thanks for the idea. Unfortunately once the program is finished parsing I essentially have no more syscalls. I've let the second one run until the output was (way) longer than the one of the working one.

Except for the pointer addresses (which I shortened to 0x) I get the following differences which I would expect:

• Different paths in the initial execve call.

• Different st_size when I stat my cwd.

• Different return value of set_tid_address

• Different path when I open() the input file.

At the very end (output-wise, not sure when the mmap() calls actually happen), the first (correct) process does the following:

mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x mmap(NULL, 4198400, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x write(2, "(error "", 8(error ")                = 8 write(2, "expected sat, but returned unsat", 32expected sat, but returned unsat) = 32 write(2, "")\n", 3") )                    = 3 munmap(0x, 4198400)         = 0 munmap(0x, 4460544)         = 0 exit_group(5)                           = ? +++ exited with 5 +++

This is what I would expect: some memory stuff, write the result, free memory, exit.

The other process looks like this:

mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x mmap(NULL, 4198400, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x mmap(NULL, 8392704, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x munmap(0x, 4198400)         = 0 brk(NULL)                               = 0x brk(0x)                          = 0x

As we can see there is an additional mmap(), the second mmap'ed memory is freed and the last two lines repeat indefinitely.

What I learn from it, and what I still don't (fully) understand:

Both processes seem to read the same file. Both reads succeed, the snippets that I see in the strace output are identical, the behaviour while parsing and computing is identical... until the first one terminates.

I understand that brk() is called whenever malloc runs out of heap space and increases the heap size of this process, correct? So I essentially see that the process continues to allocate memory? (Though not that much, I don't see the process to use a lot of memory in top...)

What would trigger mmap? I know how (and why) to use it manually, but what could be the reason for the mmap()? I.e.: What is the reason for the additional mmap()? I'm reasonably sure that I don't do mmap() in my code... maybe in a library though...

Thanks!

Gereon

On 01.03.19 08:54, Hans-Juergen Schnitzer wrote:

...

Hi,

can you try to run your programm under the control of strace and see if it is hanging anywhere? I.e.

strace -f ./smtrat_2 ...

Kind Regards, H.-J. Schnitzer

On 2/28/19 11:49 AM, Gereon Kremer wrote:

...

Hi,

I observe a weird behaviour when using different paths to a binary and an input file. As we know $HOME and $WORK resolve to /home/.../ and /work/... though /home/ and /work/ are symlinks to /rwthfs/rz/cluster/... So it should not make a difference, right?

I have a (statically linked) binary that behaves in a certain way (that I want to debug...) If I call it with the canonical paths I get:

% time /rwthfs/rz/cluster/home/gk809425/smtrat_aklima/build/smtrat_2 /rwthfs/rz/cluster/work/gk809425/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2

(error "expected sat, but returned unsat") /rwthfs/rz/cluster/home/gk809425/smtrat_aklima/build/smtrat_2 64.78s user 0.14s system 99% cpu 1:05.08 total

So it terminates after about 65 seconds. (repeatably)

Now I use the non-canonical paths: % pwd /home/gk809425/smtrat_aklima/build % time ./smtrat_2 $WORK/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2

Which does not terminate for more than four minutes... Also it is CPU-bound, so it does not seem to wait for IO.

Just to be sure: those commands were executed in the same session, so it is the same environment in terms of loaded modules, env variables, etc.

Can anyone guess what is going on here?

Best, Gereon

---

claix18-slurm-pilot mailing list -- claix18-slurm-pilot@lists.rwth-aachen.de To unsubscribe send an email to claix18-slurm-pilot-leave@lists.rwth-aachen.de

Hi,

I forgot to mention one thing...

This code will not compile with the intel compiler and uses boost etc.

You need to load the proper environment by

source ~/load_environment

On 3/5/19 3:10 PM, Gereon Kremer wrote:

Hi,

sure!

My Account is gk809425. I had to move on in the folder inspected earlier, but I reconstructed the issue in ~/smtrat_aklima_debug/build. There you find a binary smtrat-static

time ./smtrat-static /rwthfs/rz/cluster/work/gk809425/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2 yields (error "expected sat, but returned unsat") ./smtrat-static 64.18s user 0.16s system 99% cpu 1:04.51 total

time ./smtrat-static $WORK/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2 does not terminate for a couple of minutes.

Note that I now use a relative path for the binary...

I will not touch the _debug folder until I have heard back from you...

Best, Gereon

On 3/5/19 11:09 AM, Hans-Juergen Schnitzer wrote:

...

Hi,

can I login to your account and try to reproduce the problem?

Kind Regards, H.-J. Schnitzer

On 3/3/19 8:52 PM, Gereon Kremer wrote:

...

Hi,

thanks for the idea. Unfortunately once the program is finished parsing I essentially have no more syscalls. I've let the second one run until the output was (way) longer than the one of the working one.

Except for the pointer addresses (which I shortened to 0x) I get the following differences which I would expect:

• Different paths in the initial execve call.

• Different st_size when I stat my cwd.

• Different return value of set_tid_address

• Different path when I open() the input file.

At the very end (output-wise, not sure when the mmap() calls actually happen), the first (correct) process does the following:

mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x mmap(NULL, 4198400, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x write(2, "(error "", 8(error ")                = 8 write(2, "expected sat, but returned unsat", 32expected sat, but returned unsat) = 32 write(2, "")\n", 3") )                    = 3 munmap(0x, 4198400)         = 0 munmap(0x, 4460544)         = 0 exit_group(5)                           = ? +++ exited with 5 +++

This is what I would expect: some memory stuff, write the result, free memory, exit.

The other process looks like this:

mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x mmap(NULL, 4198400, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x mmap(NULL, 8392704, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x munmap(0x, 4198400)         = 0 brk(NULL)                               = 0x brk(0x)                          = 0x

As we can see there is an additional mmap(), the second mmap'ed memory is freed and the last two lines repeat indefinitely.

What I learn from it, and what I still don't (fully) understand:

Both processes seem to read the same file. Both reads succeed, the snippets that I see in the strace output are identical, the behaviour while parsing and computing is identical... until the first one terminates.

I understand that brk() is called whenever malloc runs out of heap space and increases the heap size of this process, correct? So I essentially see that the process continues to allocate memory? (Though not that much, I don't see the process to use a lot of memory in top...)

What would trigger mmap? I know how (and why) to use it manually, but what could be the reason for the mmap()? I.e.: What is the reason for the additional mmap()? I'm reasonably sure that I don't do mmap() in my code... maybe in a library though...

Thanks!

Gereon

On 01.03.19 08:54, Hans-Juergen Schnitzer wrote:

...

Hi,

can you try to run your programm under the control of strace and see if it is hanging anywhere? I.e.

strace -f ./smtrat_2 ...

Kind Regards, H.-J. Schnitzer

On 2/28/19 11:49 AM, Gereon Kremer wrote:

...

Hi,

I observe a weird behaviour when using different paths to a binary and an input file. As we know $HOME and $WORK resolve to /home/.../ and /work/... though /home/ and /work/ are symlinks to /rwthfs/rz/cluster/... So it should not make a difference, right?

I have a (statically linked) binary that behaves in a certain way (that I want to debug...) If I call it with the canonical paths I get:

% time /rwthfs/rz/cluster/home/gk809425/smtrat_aklima/build/smtrat_2 /rwthfs/rz/cluster/work/gk809425/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2

(error "expected sat, but returned unsat") /rwthfs/rz/cluster/home/gk809425/smtrat_aklima/build/smtrat_2 64.78s user 0.14s system 99% cpu 1:05.08 total

So it terminates after about 65 seconds. (repeatably)

Now I use the non-canonical paths: % pwd /home/gk809425/smtrat_aklima/build % time ./smtrat_2 $WORK/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2

Which does not terminate for more than four minutes... Also it is CPU-bound, so it does not seem to wait for IO.

Just to be sure: those commands were executed in the same session, so it is the same environment in terms of loaded modules, env variables, etc.

Can anyone guess what is going on here?

Best, Gereon

---

claix18-slurm-pilot mailing list -- claix18-slurm-pilot@lists.rwth-aachen.de To unsubscribe send an email to claix18-slurm-pilot-leave@lists.rwth-aachen.de

---

claix18-slurm-pilot mailing list -- claix18-slurm-pilot@lists.rwth-aachen.de To unsubscribe send an email to claix18-slurm-pilot-leave@lists.rwth-aachen.de