[SMT-COMP] SMT-COMP 2016: Application Track Testing
Mate Soos
soos.mate at gmail.com
Sun Jun 12 06:48:22 EDT 2016
Hi All,
First of all, thank you for that investigation, Armin! Here is the
issue, and it's reproducible on my Ubuntu 14.04. Let's take this CNF:
https://github.com/msoos/cryptominisat/files/296796/output_0.zip
Every SCC (strongly connected component) implementation I know uses
recursion, and this CNF exercises an extreme case of that. So I run my
solver with:
$ ulimit -a
[..]
stack size (kbytes, -s) 8192
$ ./cryptominisat 4 --threads 4
[..]
s SATISFIABLE
now I set unlimited:
$ ulimit -a
[...]
stack size (kbytes, -s) unlimited
$ ./cryptominisat4 --threads 4 output_0.cnf
[...]
Segmentation fault (core dumped)
(Note that cryptominisat is valgrind-clean and so is this run)
On this crash, GDB shows a backtrace of exactly 32672 (~2**15) depth.
I think something is wrong with pthreads (and maybe the way the
implementation of C++11 is using pthreads) here. Trevor Hansen was
looking into this and he observed that pthreads seems to allocate only
2MB of stack per thread in case of 'unlimited' stack. I don't know why
that is the case. Note that setting ulimit -s 2048 crashes, but -s 3072
doesn't.
So this seems to only happen if you use threads (pthreads in case of
UNIX), and it might also have to do with how C++11 is using pthreads in
this particular case (I'm using default Ubuntu 14.04 gcc,
4.8.4-2ubuntu1~14.04.3).
As for who tracked this down, it was Trevor, mostly, I am most certainly
_not_ this good to guess the 'unlimited'. He also guessed that
pthread_attr_setstacksize() would probably work. I'm just not happy
about using that, because it's nonportable. I'm using C++11 threads, so
it works everywhere where C++11 works, which is not the case for that
pthread call.
I hope the above helps,
Mate
On 06/12/2016 11:13 AM, Armin Biere wrote:
> I thought I check this for our cluster set-up too. On default Ubuntu
> (14.04 and 16.04)
> the stack default limit is 8192. On our cluster which runs 14.04 the
> master also has
> this but the jobs submitted through sun-grid-engine have unlimited. So
> I wrote the
> following script which checks stack overflow. On the master and other
> Ubuntu machines
> calling this script gives very fast a stack overflow (as it should be)
> and then runs
> forever eating up all the (virtual) memory before getting a stack
> overflow. On the
> cluster (under grid-engine control) it is unlimited from the beginning
> and then eats
> up the full memory (16 GB virtual 8 GB actual memory) before it runs
> into the stack
> overflow. So to make it short, in 'unlimited' both on Ubuntu 14.04 and
> 16.04 as well
> as when submitted on our cluster through Sun-Grid-Engine will really be
> unlimited.
> So I can not confirm what Mate wrote (in my environment). BTW, I did
> have exactly
> this issue with the IIMC model checker in the HWMCC and reran their tool
> with much
> larger stack limit. I think I got a specific error message which did
> only appear
> for that tool on a specific set of benchmarks deterministically. So I
> thought it is
> fair to rerun. But I understand that this might be more difficult here
> (in particular
> somebody could have checked the stack size and depending on that enable
> disable, or limit certain optimizations / rewrites, but Boolector does
> not do that).
>
> Here is the the script:
>
>
> !/bin/sh
> set -x
> cat << EOF > /tmp/stack-overflow.c
> #include <stdio.h>
> void f (int i) { printf ("%d\n", i); fflush (stdout); f (i+1); }
> int main () { f (0); }
> EOF
> ulimit -s
> gcc -o /tmp/stack-overflow /tmp/stack-overflow.c
> time -f %E /tmp/stack-overflow|tail -1
> ulimit -s unlimited
> ulimit -s
> time -f %E /tmp/stack-overflow|tail -1
>
>
> On a standard ubuntu installation it gives:
>
> + ulimit -s
> 8192
> + gcc -o /tmp/stack-overflow /tmp/stack-overflow.c
> + time -f %E /tmp/stack-overflow
> + tail -1
> Command terminated by signal 11
> 0:00.30
> 261874
> + ulimit -s unlimited
> + ulimit -s
> unlimited
> + time -f %E /tmp/stack-overflow
> + tail -1
> ...
> (then I pressed control-c)
>
>
> So you can do 261,874 recursive invocations by default
> (so never implement unlimited recursion on data structures
> like a list which might have a million elements).
>
>
> On the cluster nodes the output is split in stderr and stdout:
>
> stdout:
>
> unlimited
> 518808577
> unlimited
> 518813922
>
>
> stderr:
>
>
> + cat
> + ulimit -s
> + gcc -o /tmp/stack-overflow /tmp/stack-overflow.c
> + time -f %E /tmp/stack-overflow
> + tail -1
> Command terminated by signal 11
> 9:23.40
> + ulimit -s unlimited
> + ulimit -s
> + tail -1
> + time -f %E /tmp/stack-overflow
> Command terminated by signal 11
> 9:11.67
>
> So it takes more than 9 minutes to eat up that virtual
> memory of 16GB (8GB real). Note that I did not use
> 'runlim' or something similar to limit memory.
>
>
>
> Maybe on StarExec there is a different behaviour?
>
>
> Armin
>
> On Sun, Jun 12, 2016 at 4:22 AM, Aaron Stump <aaron-stump at uiowa.edu
> <mailto:aaron-stump at uiowa.edu>> wrote:
>
> Hello, Mate.
>
> On 06/11/2016 07:59 AM, Mate Soos wrote:
>
> Hi Aaron,
>
> First of all, thanks for getting back to me!
>
> Sure, I am happy to discuss this matter with you.
>
>
> On 06/10/2016 09:11 PM, Aaron Stump wrote:
>
> I am sorry you ran into a problem with stack size. We are
> actually not
> setting the stack limit explicitly in our jobscript. What
> are you
> seeing that makes you think it is lower than what is shown
> with "ulimit
> -s" (namely, 8192KB)? This value should have been something
> one could
> see with the VM instance (though we are due to update that
> in the next
> week or so, but I don't expect major changes).
>
> Certainly one could ask for a higher stack limit than 8MB,
> and I would
> be happy to have us raise this or make it configurable.
>
> I think the stack limit was about 2MB -- and I think it might
> have been
> because it was set to:
>
> ulimit -s unlimited
>
> Out of curiosity: what are you seeing that makes you think that we
> are setting "ulimit -s unlimited"?
>
>
> Yep -- unlimited stack is actually more limiting for whatever
> reason. I
> have default 8MB (Ubuntu/Debian default), RedHat Linux default
> has 10MB.
> Can you please create an example run with the system that ran
> the SMT
> Competition that simply runs
>
> ulimit -a
>
> please? That would clear things up :)
>
> I agree that this would help clear up this issue. Here is the
> output from a single job pair that just calls ulimit -a
> (the job is
> https://www.starexec.org/starexec/secure/details/job.jsp?id=16269):
>
> 0.00/0.00 core file size (blocks, -c) unlimited
> 0.00/0.00 data seg size (kbytes, -d) unlimited
> 0.00/0.00 scheduling priority (-e) 0
> 0.00/0.00 file size (blocks, -f) 629145600
> 0.00/0.00 pending signals (-i) 1030922
> 0.00/0.00 max locked memory (kbytes, -l) 64
> 0.00/0.00 max memory size (kbytes, -m) unlimited
> 0.00/0.00 open files (-n) 1024
> 0.00/0.00 pipe size (512 bytes, -p) 8
> 0.00/0.00 POSIX message queues (bytes, -q) 819200
> 0.00/0.00 real-time priority (-r) 0
> 0.00/0.00 stack size (kbytes, -s) unlimited
> 0.00/0.00 cpu time (seconds, -t) 90
> 0.00/0.00 max user processes (-u) 4096
> 0.00/0.00 virtual memory (kbytes, -v) 1099776
> 0.00/0.00 file locks (-x) unlimited
>
>
> So indeed, the stack size is unlimited. Our code does not seem to
> be setting this explicitly, so I am not sure where it is getting set.
>
> I was not aware that ulimit -s unlimited would actually impose a
> default limit. Do you mind sharing a reference for that? This ulimit
> is different from what I see when I log in to a compute node and run
> "ulimit -a" (there, the stack size is set to 8MB). So it is getting
> set somehow differently in the system when job pairs are getting run
> on the compute nodes.
>
> This stack size limit is something we will surely want to change,
> though I would like additional confirmation that ulimit -s unlimited
> on linux will actually (and quite counterintuitively) impose this
> low default limit.
>
> Cheers, and thanks for your investigation,
> Aaron
>
>
> Thanks a lot in advance,
>
> Mate
>
>
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu <mailto:SMT-COMP at cs.nyu.edu>
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5524 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-comp/attachments/20160612/48683a22/attachment-0001.p7s>
More information about the SMT-COMP
mailing list