debugging segfaults; any suggestions?
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:
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.
More information about the Cvs-ghc