#4805: segfault in Data.HashTable, triggered by long Agda runs
-------------------------------+--------------------------------------------
Reporter: wkahl | Owner:
Type: bug | Status: new
Priority: normal | Component: libraries/base
Version: 7.0.1 | Keywords: Data.HashTable segfault
Testcase: | Blockedby:
Os: Linux | Blocking:
Architecture: x86_64 (amd64) | Failure: Runtime crash
-------------------------------+--------------------------------------------
Agda uses {{{Data.HashTable}}} for interface (*.agdai) serialisation.
I have been able to localise a reproducible segfault (with one of the many
theories in a sizeable Agda develoment) in
{{{Agda.TypeChecking.Serialise.encode}}} inside the {{{icode}}} call,
which essentially limits the possible source of the segfault to the Agda
module {{{Agda.TypeChecking.Serialise}}} and to {{{Data.HashTable}}}.
Then I replaced all hash table uses in {{{encode}}} with {{{Data.Map}}},
and the Agda run in question finishes successfully.
(I confirmed with a selection of the theories that already could be type-
checked with {{{Data.HashTable}}} that the {{Data.Map}}}-based version
generates the same interface files.)
(Agda interface serialisation maintains four partial maps; their
respective sizes at the end of this run are 151796,733,3319,0.)
I consider this as a (non-constructive) proof that there is a bug in
{{{Data.HashTable}}}.
(For the time being, I need to make some long-delayed progress in my Agda
developments and won't have time to try to debug {{{Data.HashTable}}}, but
I should be able to occasionally test potential fixes.)
Wolfram
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4805>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
