OSX-only multithreaded Z3 crash #1080
Comments
arifogel
changed the title
|
Some relevant Java code: public Set<Flow> computeNodOutput(List<NodJob> jobs) {
_logger.info("\n*** EXECUTING NOD JOBS ***\n");
resetTimer();
Set<Flow> flows = new TreeSet<>();
BatfishJobExecutor<NodJob, NodAnswerElement, NodJobResult, Set<Flow>> executor = new BatfishJobExecutor<>(
_settings, _logger, true, "NOD");
// todo: do something with nod answer element
executor.executeJobs(jobs, flows, new NodAnswerElement());
printElapsedTime();
return flows;
}NodJob.java:call (work done by each job): @Override
public NodJobResult call() throws Exception {
long startTime = System.currentTimeMillis();
long elapsedTime;
try (Context ctx = new Context()) {
NodProgram baseProgram = _dataPlaneSynthesizer
.synthesizeNodDataPlaneProgram(ctx);
NodProgram queryProgram = _querySynthesizer.getNodProgram(baseProgram);
NodProgram program = baseProgram.append(queryProgram);
Params p = ctx.mkParams();
p.add("fixedpoint.engine", "datalog");
p.add("fixedpoint.datalog.default_relation", "doc");
p.add("fixedpoint.print_answer", true);
Fixedpoint fix = ctx.mkFixedpoint();
fix.setParameters(p);
for (FuncDecl relationDeclaration : program.getRelationDeclarations()
.values()) {
fix.registerRelation(relationDeclaration);
}
for (BoolExpr rule : program.getRules()) {
fix.addRule(rule, null);
}
for (BoolExpr query : program.getQueries()) {
Status status = fix.query(query);
switch (status) {
case SATISFIABLE:
break;
case UNKNOWN:
throw new BatfishException("Query satisfiability unknown");
case UNSATISFIABLE:
break;
default:
throw new BatfishException("invalid status");
}
}
Expr answer = fix.getAnswer();
BoolExpr solverInput;
if (answer.getArgs().length > 0) {
List<Expr> reversedVarList = new ArrayList<>();
reversedVarList.addAll(program.getVariablesAsConsts().values());
Collections.reverse(reversedVarList);
Expr[] reversedVars = reversedVarList.toArray(new Expr[] {});
Expr substitutedAnswer = answer.substituteVars(reversedVars);
solverInput = (BoolExpr) substitutedAnswer;
}
else {
solverInput = (BoolExpr) answer;
}
if (_querySynthesizer.getNegate()) {
solverInput = ctx.mkNot(solverInput);
}
Solver solver = ctx.mkSolver();
solver.add(solverInput);
Status solverStatus = solver.check();
switch (solverStatus) {
case SATISFIABLE:
break;
case UNKNOWN:
throw new BatfishException("Stage 2 query satisfiability unknown");
case UNSATISFIABLE:
elapsedTime = System.currentTimeMillis() - startTime;
return new NodJobResult(elapsedTime, _logger.getHistory());
default:
throw new BatfishException("invalid status");
}
Model model = solver.getModel();
Map<String, Long> constraints = new LinkedHashMap<>();
for (FuncDecl constDecl : model.getConstDecls()) {
String name = constDecl.getName().toString();
BitVecExpr varConstExpr = program.getVariablesAsConsts().get(name);
long val = ((BitVecNum) model.getConstInterp(varConstExpr))
.getLong();
constraints.put(name, val);
}
Set<Flow> flows = new HashSet<>();
for (Pair<String, String> nodeVrf : _nodeVrfSet) {
String node = nodeVrf.getFirst();
String vrf = nodeVrf.getSecond();
Flow flow = createFlow(node, vrf, constraints);
flows.add(flow);
}
elapsedTime = System.currentTimeMillis() - startTime;
return new NodJobResult(elapsedTime, _logger.getHistory(), flows);
}
catch (Z3Exception e) {
elapsedTime = System.currentTimeMillis() - startTime;
return new NodJobResult(elapsedTime, _logger.getHistory(),
new BatfishException(
"Error running NoD on concatenated data plane", e));
}
} |
|
Will you also gift us a shiny new Mac to test it (requires a 5K monitor, of course) :-). |
|
@arifogel I got to step 6. |
|
@arifogel This may be a long shot but have you tried building Z3 with the ThreadSanitizer? Because you are using Z3 from Java you may have to pull some tricks to get the sanitizer runtime library to be loaded. |
|
batfish_build_all is a function defined in batfish_functions.sh
You must source that file using bash (might need brew bash with modern
version) to get that function.
Also, some other brew utilities may be necessary: findutils coreutils (and
whatever provides greadlink - may be coreutils)
…On Jun 22, 2017 4:42 AM, "Christoph M. Wintersteiger" < ***@***.***> wrote:
@arifogel <https://github.com/arifogel> I got to step 6. batfish_build_all,
but I can't find any script of that name. Did that change name in the
meanwhile?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1080 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AHYSErwU1s_EqFAxm46pavYZDaHuhqHsks5sGlMMgaJpZM4N85qi>
.
|
|
Ah! Alright, that's probably it, I'm definitely not using the latest version of bash. |
|
I was wondering if more thoughts & efforts were put into this issue. We might have the same one with epfl-lara/stainless, or at least the symptoms look really similar. Just checking before investing more time into this. :) |
|
@mantognini A random thought of mine... Z3 uses OpenMP primitives for locking (now that we use C+11 it might be better to use the C++ standard library locks). IIRC Clang shiped with Xcode on macOS does not support OpenMP. Therefore if you use that as your compiler you have no locks and using Z3 in a multi-threaded manner is likely unsafe. If you use a Clang (from homebrew that supports OpenMP) or gcc with OpenMP support to build Z3 do you run into the same problem? |
I don't know if this has changed, but I think you get an error from Apple's clang. Anyway, I'll give a shot at this idea next week and report here. |
|
@mantognini Both build systems (CMake and python/Makefile) try to detect on the first configure if the compiler supports OpenMP. If the compiler does not support it on this first configure, OpenMP support is disabled. You will not see any warnings from Clang. If you ask the CMake build system to explicitly enable OpenMP (pass |
|
Oh, okay, didn't know that. Thanks for the info. |
|
Here's a concise Java unit test that reproduces "usually" on my Macbook (mid-2017, 4 cores): package com.microsoft.z3.parallelism;
import static org.hamcrest.Matchers.equalTo;
import static org.junit.Assert.assertThat;
import com.microsoft.z3.Context;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import java.util.stream.IntStream;
import org.junit.Test;
public class Z3ParallelismTest {
private static void trivialZ3Program(int i) {
try (Context ctx = new Context()) {
Solver solver = ctx.mkSolver();
solver.add(ctx.mkEq(ctx.mkInt(3), ctx.mkInt(4)));
assertThat(solver.check(), equalTo(Status.UNSATISFIABLE));
}
}
@Test
public void testParallelism() {
IntStream.rangeClosed(1, Runtime.getRuntime().availableProcessors() * 2)
.parallel()
.forEach(Z3ParallelismTest::trivialZ3Program);
}
}The crash messages vary: Hope this is useful. |
|
Is openmp available on your platform? |
|
@NikolajBjorner yes, but I'm using the OS X released z3 binary. |
|
(It seems like undesirable behavior for that binary to just be broken.) |
|
Ok, so I should take our build machine is basically not well configured or it is producing binaries that are useless for multithreading. |
|
@delcypher Does the default clang on OSX now support OpenMP or would it take more effort than that to update our builds? |
|
No. We had to use |
|
OpenMP is now no longer with us. Z3 uses C++11 threads for everything |
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:
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)allinone -runmode interactiveinit-testrig test_rigs/exampleget reachabilityThe text was updated successfully, but these errors were encountered: