[SMT-COMP] SMT-COMP 2016: Application Track Testing
Clark Barrett
barrett at cs.nyu.edu
Sun Jun 12 13:06:42 EDT 2016
Hi all - I believe we had this exact problem in the 2014 competition. The
default stack size for a thread is 2 mb unless you explicitly set it to be
more. We fixed it by using the boost threading library and explicitly
setting the stack size. For the competition, we asked David Cok to rerun
our patched executable as a noncompetitive entry (i.e. just for comparison
purposes) which he did. Perhaps a similar compromise would be appropriate
here. Sorry you guys got bit by this - I know how frustrating that is.
-Clark
On Sunday, June 12, 2016, Mate Soos <soos.mate at gmail.com> wrote:
> 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
> <javascript:;>
> > <mailto:aaron-stump at uiowa.edu <javascript:;>>> 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 <javascript:;> <mailto:SMT-COMP at cs.nyu.edu
> <javascript:;>>
> > http://cs.nyu.edu/mailman/listinfo/smt-comp
> >
> >
>
>
>
--
-Clark
More information about the SMT-COMP
mailing list