[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