OSX-only multithreaded Z3 crash #1080
Description
Likely related to #698
I meant to report this a long time ago. Basically, the batfish project uses multiple contexts in parallel during some of its queries. This causes crashes ONLY in OSX. It works on Linux and Windows with no issue.
The master branch of batfish disables this parallelism only in OSX. I have created a topic branch that reenables this parallelism to reproduce the bug:
https://github.com/batfish/batfish/tree/ari/z3-osx-double-free
You can reproduce by:
- (Install brew coreutils and JDK 8 on OSX and perhaps other dependencies)
git clone https://github.com/batfish/batfishcd batfishgit checkout origin/ari/z3-osx-double-free. tools/batfish_functions.shbatfish_build_allcd tools && ./install_z3_osx.sh(may require root -- replaces any z3 libs on system with 4.5.0. If you want to test with latest master or development branch, skip this step)- (from root of batfish repository)
allinone -runmode interactive - (inside allinone CLI):
init-testrig test_rigs/example - (inside allinone CLI):
get reachability
arifogel@XXXXXX:~/git/batfish$allinone -runmode interactive
batfish> init-testrig test_rigs/example
Init'ed and set active container
Uploaded testrig. Parsing now.
Status: SUCCESS
PARSING SUMMARY
STATISTICS
Parsing results:
Parsed successfully: 17
batfish> get reachability
java(46891,0x70000ee52000) malloc: *** error for object 0x7fcfcb411f00: pointer being freed was not allocated
*** set a breakpoint in malloc_error_break to debug
java(46891,0x70000f058000) malloc: *** error for object 0x7fcfcb411f00: pointer being freed was not allocated
*** set a breakpoint in malloc_error_break to debug
java(46891,0x70000ef55000) malloc: *** error for object 0x7fcfcb411f00: pointer being freed was not allocated
*** set a breakpoint in malloc_error_break to debug
/Users/arifogel/git/batfish/projects/allinone/allinone: line 16: 46891 Abort trap: 6 java $ALLINONE_JAVA_ARGS -DbatfishQuestionPluginDir="${BATFISH_JAVA_QUESTION_PLUGIN_DIR}" -jar "$ALLINONE_JAR" "$@"