debugging segfaults; any suggestions?

Adam Megacz megacz at cs.berkeley.edu
Wed Apr 20 21:04:42 CEST 2011


So, I have a situation where my modified GHC is segfaulting.  All
compilation is done with -O0.  I'm sort of hoping for suggestions on how
to continue figuring this out.

I've tried all of the suggestions on these pages, short of using gdb:

  http://hackage.haskell.org/trac/ghc/wiki/Debugging
  http://hackage.haskell.org/trac/ghc/wiki/Debugging/CompiledCode

The code which segfaults is a Haskell extraction of a Coq program.  Now,
this is a tricky situation because:

  1. In theory, Coq extractions should never segfault, since they've
     been type-checked by Coq.  To my understanding, the correctness
     proof for the extraction is based on type-erased dynamic semantics
     (i.e. proves type-ignorant reduction never gets stuck) rather than
     any sort of reduction to the static semantics of Haskell (which
     probably isn't possible).

  2. Coq extractions use unsafeCoerce, since Haskell doesn't have
     full-spectrum dependent types.  Using unsafeCoerce is sort of a
     "all bets are off" situation.

The really strange part is this: if I modify the extraction machinery
and wrap every subexpression "e" as "(trace e)" where trace is:

  trace x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x

Everything works perfectly (though very slowly)!  I stumbled upon this
solution in the process of inserting tracing code.  I guess this makes
it a Heisenbug.

Perhaps the "trace" calls are defeating some GHC optimization (which is
enabled even at -O0), and that optimization indirectly relies on the
fact that there are no value-indexed types in Haskell?

FWIW, the segfault happens even in ghc-stage1, built using 6.12, so this
isn't a behavior introduced by GHC7.

Thanks in advance for any hints, no matter how vague.  I'm anxious to
get rid of the nasty hack above.

  - a





More information about the Cvs-ghc mailing list