Manticore sometimes hangs when a worker exits unexpectedly

[bradlarsen]

Sometimes Manticore hangs indefinitely when one of its workers exits unexpectedly, such as with an out-of-memory error.

For example, I saw this backtrace when running python -mmanticore /home/blarsen/coreutils-install/bin/expand on an Ubuntu 18.04 machine:

2020-02-20 13:09:27,165: [24106] m.c.worker:INFO: [6] Debug Concretize()
[Errno 12] Cannot allocate memory Probably too many cached expressions? visitors._cache...
2020-02-20 13:09:27,172: [24106] m.c.worker:ERROR: Exception in state 6: Z3NotFoundError()
Traceback (most recent call last):
  File "/home/blarsen/manticore/manticore/native/state.py", line 29, in execute
    result = self._platform.execute()
  File "/home/blarsen/manticore/manticore/platforms/linux.py", line 2438, in execute
    self.current.execute()
  File "/home/blarsen/manticore/manticore/native/cpu/abstractcpu.py", line 969, in execute
    raise ConcretizeRegister(self, "PC", policy="ALL")
manticore.native.cpu.abstractcpu.ConcretizeRegister: (<manticore.native.cpu.x86.AMD64Cpu object at 0x7f5587a62640>, 'PC')

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/blarsen/manticore/manticore/core/worker.py", line 121, in run
    current_state.execute()
  File "/home/blarsen/manticore/manticore/native/state.py", line 41, in execute
    raise Concretize(str(e), expression=expression, setstate=setstate, policy=e.policy)
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/blarsen/manticore/manticore/core/smtlib/solver.py", line 215, in _start_proc
    self._proc = Popen(
  File "/usr/lib/python3.8/subprocess.py", line 854, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "/usr/lib/python3.8/subprocess.py", line 1637, in _execute_child
    self.pid = _posixsubprocess.fork_exec(
OSError: [Errno 12] Cannot allocate memory

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/blarsen/manticore/manticore/core/worker.py", line 142, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate)
  File "/home/blarsen/manticore/manticore/core/manticore.py", line 361, in _fork
    solutions = state.concretize(expression, policy)
  File "/home/blarsen/manticore/manticore/core/state.py", line 297, in concretize
    vals = self._solver.get_all_values(
  File "/home/blarsen/manticore/manticore/core/smtlib/solver.py", line 451, in get_all_values
    self._reset(temp_cs.to_string(related_to=var))
  File "/home/blarsen/manticore/manticore/core/smtlib/solver.py", line 294, in _reset
    self._start_proc()
  File "/home/blarsen/manticore/manticore/core/smtlib/solver.py", line 229, in _start_proc
    raise Z3NotFoundError  # TODO(mark) don't catch this exception in two places
manticore.exceptions.Z3NotFoundError

At this point, the top-level Manticore process was forever waiting, until I forcibly killed it. It would be much preferable if Manticore didn't hang.

I have seen this kind of hang other times when a worker has exited uncleanly, not just for out-of-memory reasons. Let me see if I can produce a small, reliable reproducer of this hanging behavior.

[bradlarsen]

Note additionally that the Z3NotFoundError is spurious: Z3 is definitely found.

[bradlarsen]

It looks like the top-level Manticore process is getting stuck somewhere in this loop:

manticore/manticore/core/worker.py

Lines 74 to 180 in 32f79f2

	# If CTRL+C is received at any worker lets abort exploration via m.kill()
	# kill will set m._killed flag to true and then each worker will slowly
	# get out of its mainloop and quit.
	with WithKeyboardInterruptAs(m.kill):
	# The worker runs until the manticore is killed
	while not m._killed.value:
	# STARTED - Will try to consume states until a STOP event is received
	# Outer loop, Keep getting states until someone request us to STOP
	try: # handle fatal errors even exceptions in the exception handlers
	try: # handle Concretize and TerminateState
	# At RUNNING
	# The START has been requested, we operate with under the assumption
	# that manticore we will let us stay at this phase for a _while_
	# Requests to STOP will we honored ASAP (i.e. Not immediately)
	# Select a single state
	# wait for other worker to add states to the READY list
	# This momentarily get the main lock and then releases
	# it while waiting for changes
	# Raises an Exception if manticore gets cancelled
	# while waiting or if there are no more potential states
	logger.debug("[%r] Waiting for states", self.id)
	# If at STANDBY wait for any change
	current_state = m._get_state(wait=True)
	# there are no more states to process
	# states can come from the ready list or by forking
	# states currently being analyzed in the busy list
	if current_state is None:
	logger.debug("[%r] No more states", self.id)
	break
	# assert current_state is not None
	# Allows to terminate manticore worker on user request
	# even in the middle of an execution
	logger.debug("[%r] Running", self.id)
	assert (
	current_state.id in m._busy_states
	and current_state.id not in m._ready_states
	)
	# This does not hold the lock so we may loss some event
	# flickering
	while not m._killed.value:
	current_state.execute()
	else:
	logger.debug("[%r] Stopped and/or Killed", self.id)
	# On going execution was stopped or killed. Lets
	# save any progress on the current state using the
	# same id. No other worker will use this state in
	# this run
	m._save(current_state, state_id=current_state.id)
	m._revive_state(current_state.id)
	current_state = None
	assert current_state is None
	# Handling Forking and terminating exceptions
	except Concretize as exc:
	logger.info("[%r] Debug %r", self.id, exc)
	# The fork() method can decides which state to keep
	# exploring. For example when the fork results in a
	# single state it is better to just keep going.
	# Though, normally fork() saves the spawned childs,
	# returns a None and let _get_state choose what to explore
	# next
	m._fork(current_state, exc.expression, exc.policy, exc.setstate)
	current_state = None
	except TerminateState as exc:
	logger.debug("[%r] Debug State %r %r", self.id, current_state, exc)
	# Notify this state is done
	m._publish("will_terminate_state", current_state, exc)
	# Update the stored version of the current state
	current_state._terminated_by = exc
	m._save(current_state, state_id=current_state.id)
	# Add the state to the terminated state list re-using
	# the same id. No other worker will use this state in
	# this run
	m._terminate_state(current_state.id)
	m._publish("did_terminate_state", current_state, exc)
	current_state = None
	except (Exception, AssertionError) as exc:
	import traceback
	formatted = traceback.format_exc()
	logger.error("Exception in state %r: %r\n%s ", self.id, exc, formatted)
	# Internal Exception
	# Add the state to the terminated state list
	if current_state is not None:
	# Drop any work on this state in case it is inconsistent
	# Update the stored version of the current state
	# Saved to a fresh id in case other worker have an old
	# version this state cached over the old id
	m._publish("will_kill_state", current_state, exc)
	m._save(current_state, state_id=current_state.id)
	m._kill_state(current_state.id)
	m._publish("did_kill_state", current_state, exc)
	current_state = None
	break

[feliam]

There is not heartbeat implemented to check if a worker hangs (when using multiprocessing).

[gustavo-grieco]

@bradlarsen can you check if this helps: #2450 ?